login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
ProgrammingSPAD
PascalTriangleNopile  ← ↑ →  SimpleSpadExamples

SandBoxTryOutSPAD
  
last edited 10 years ago by hemmecke

Edit detail for SandBoxTryOutSPAD revision 1 of 2
1 2
Editor: hemmecke
Time: 2014/02/14 11:23:29 GMT+0
Note: 
changed:
-
Everyone is allowed to try out SPAD by editing this page.
Don't be affraid to destroy anything. The purpose of this page
is exactly to give a place for everyone to experiment.

Just hit the "edit" link in the upper right corner.

\begin{spad}
)abbrev category MYMON rhxMonoid
rhxMonoid: Category == with
    1: %
    _*: (%, %) -> %

rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %

)abbrev domain MYFUN rhxFun
rhxFun(S: SetCategory): rhxMonoid with
    myfun:  (S -> S) -> %
    coerce: % -> (S -> S)
 == add
    Rep ==> S -> S
    myfun(f: S -> S): % == per f
    coerce(x: %): S -> S == rep x
    1: % == per((s: S): S +-> s)
    ((x: %) * (y: %)): % == per( (s: S): S +-> (rep x)(rep y)s )
\end{spad}

\begin{axiom}
I ==> Integer
II ==> I -> I
inc(i: I): I == i+1
double(i: I): I == 2*i
minc: rhxFun(I) := myfun inc
mdouble: rhxFun(I) := myfun double
f := (mdouble * minc) :: II
g := (minc * mdouble) :: II

f 1
g 1
\end{axiom}

Everyone is allowed to try out SPAD by editing this page. Don't be affraid to destroy anything. The purpose of this page is exactly to give a place for everyone to experiment.

Just hit the "edit" link in the upper right corner.

spad
)abbrev category MYMON rhxMonoid
rhxMonoid: Category == with
    1: %
    _*: (%, %) -> %

rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %

)abbrev domain MYFUN rhxFun
rhxFun(S: SetCategory): rhxMonoid with
    myfun:  (S -> S) -> %
    coerce: % -> (S -> S)
 == add
    Rep ==> S -> S
    myfun(f: S -> S): % == per f
    coerce(x: %): S -> S == rep x
    1: % == per((s: S): S +-> s)
    ((x: %) * (y: %)): % == per( (s: S): S +-> (rep x)(rep y)s )
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8795110988096797882-25px001.spad
      using old system compiler.
   MYMON abbreviates category rhxMonoid 
------------------------------------------------------------------------
   initializing NRLIB MYMON for rhxMonoid 
   compiling into NRLIB MYMON 

;;;     ***       |rhxMonoid| REDEFINED
Time: 0 SEC.

   finalizing NRLIB MYMON 
   Processing rhxMonoid for Browser database:
--->-->rhxMonoid(constructor): Not documented!!!!
--->-->rhxMonoid(((One) (%) constant)): Not documented!!!!
--->-->rhxMonoid((* (% % %))): Not documented!!!!
--->-->rhxMonoid(): Missing Description
; compiling file "/var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.lsp" (written 14 FEB 2014 11:23:29 AM):

; /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.fasl written
; compilation finished in 0:00:00.005
------------------------------------------------------------------------
   rhxMonoid is now explicitly exposed in frame initial 
   rhxMonoid will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON

   MYFUN abbreviates domain rhxFun 
------------------------------------------------------------------------
   initializing NRLIB MYFUN for rhxFun 
   compiling into NRLIB MYFUN 
   processing macro definition Rep ==> S -> S 
   compiling exported myfun : S -> S -> $
      MYFUN;myfun;M$;1 is replaced by f 
Time: 0 SEC.

   compiling exported coerce : $ -> S -> S
      MYFUN;coerce;$M;2 is replaced by x 
Time: 0 SEC.

   compiling exported One : () -> $
Time: 0 SEC.

   compiling exported * : ($,$) -> $
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |rhxFun| REDEFINED

;;;     ***       |rhxFun| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor rhxFun
      Time: 0 seconds

   finalizing NRLIB MYFUN 
   Processing rhxFun for Browser database:
--->-->rhxFun(constructor): Not documented!!!!
--->-->rhxFun(((One) (%) constant)): Not documented!!!!
--->-->rhxFun((* (% % %))): Not documented!!!!
--->-->rhxFun(constructor): Not documented!!!!
--->-->rhxFun((myfun (% (Mapping S S)))): Not documented!!!!
--->-->rhxFun((coerce ((Mapping S S) %))): Not documented!!!!
--->-->rhxFun(): Missing Description
; compiling file "/var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.lsp" (written 14 FEB 2014 11:23:29 AM):

; /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.fasl written
; compilation finished in 0:00:00.018
------------------------------------------------------------------------
   rhxFun is now explicitly exposed in frame initial 
   rhxFun will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN

fricas
I ==> Integer
Type: Void
fricas
II ==> I -> I
Type: Void
fricas
inc(i: I): I == i+1

   Function declaration inc : Integer -> Integer has been added to 
      workspace.
Type: Void
fricas
double(i: I): I == 2*i

   Function declaration double : Integer -> Integer has been added to 
      workspace.
Type: Void
fricas
minc: rhxFun(I) := myfun inc
fricas
Compiling function inc with type Integer -> Integer 

 LISP output:
(#<FUNCTION |*1;inc;1;initial|>)
Type: rhxFun(Integer)
fricas
mdouble: rhxFun(I) := myfun double
fricas
Compiling function double with type Integer -> Integer 

 LISP output:
(#<FUNCTION |*1;double;1;initial|>)
Type: rhxFun(Integer)
fricas
f := (mdouble * minc) :: II
\label{eq1}\mbox{theMap (...)}(1)
Type: (Integer -> Integer)
fricas
g := (minc * mdouble) :: II
\label{eq2}\mbox{theMap (...)}(2)
Type: (Integer -> Integer)
fricas
f 1
\label{eq3}4(3)
Type: PositiveInteger?
fricas
g 1
\label{eq4}3(4)
Type: PositiveInteger?