login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for ProgrammingSPAD revision 3 of 28

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
Editor: hemmecke
Time: 2014/02/14 02:02:19 GMT+0
Note:

added:

  Supposed the above code goes into a file 'mymonoid.spad', then this file can be compiled via::

    )compile mymonoid.spad

  indide a FriCAS session.

  Now comes the corresponding domain definition.

changed:
-)abbrev category MYMON MyMonoid
-XHashTable(Key : SetCategory, Entry : Type):
-  Join(TableAggregate(Key, Entry), finiteAggregate, shallowlyMutable) with
-    table : (Key -> SingleInteger) -> %
-      ++ table(h) creates an empty hash table that uses h instead of
-      ++ hash$Key. Note that h should be a mathematical function in
-      ++ the sense that from k1=k2 follows h(k1)=h(k2). If that is not
-      ++ the case, k1 and k2 will internally be considered as being
-      ++ different keys.
)abbrev domain MYFUN MyFun
MyFun(S: SetCategory): MyMonoid with
    myfun:  (S -> S) -> %
    coerce: % -> (S -> S)

changed:
-    Marker ==> None
-    toMarker mk ==> mk@Marker -- note that MKey==Marker==UMKE
-    VACANT : Marker := (HASHTABLEVACANT$Lisp)  pretend Marker -- pos never used
-    DELETED : Marker := (HASHTABLEDELETED$Lisp) pretend Marker -- pos is deleted
-    vacant?(mk)  ==> EQ(toMarker mk, VACANT)$Lisp
-    deleted?(mk) ==> EQ(toMarker mk, DELETED)$Lisp
-    key?(mk) ==> not (vacant? mk or deleted? mk)
-    MKey ==> None
-    UMKE ==> None
-    Buckets ==> PrimitiveArray UMKE
-    numOfBuckets(a) ==> shift(#a, -1)
-    toUMKE x ==> x pretend UMKE
-    toKey k ==> (k@UMKE) pretend Key
-    getMKey(a, i)    ==> ((a.i)@UMKE) pretend MKey
-    setKey!(a, i, k) ==> (a.i := toUMKE k) pretend Key
-    getEntry(a, n, i)     ==> a(n+i) pretend Entry
-    setEntry!(a, n, i, e)  ==> (a(n+i) := toUMKE e) pretend Entry
-    setKeyEntry!(a, n, i, k, e) ==> (setKey!(a, i, k); setEntry!(a, n, i, e))
-    -- deleteKeyEntry!(a, n, i) ==> setKeyEntry!(a, n, i, DELETED, VACANT)
-    deleteKeyEntry!(a, n, i) ==> (a.i := toUMKE DELETED; a(n+i) := toUMKE VACANT)
-    KE ==> Record(key : Key, entry : Entry)
-    UE ==> Union(Entry, "failed")
-    maxLoad n ==> n*7 quo 10 -- load factor
-    maxVirtualLoad n ==> n*9 quo 10  -- virtual load factor
-    Rep ==> Record(_
-        numOfEntries : Z, _
-        maxNumOfEntries : Z, _
-        numOfDeletedEntries : Z, _
-        maxNumOfVirtualEntries : Z, _
-        idx : Z, _
-        arr : Buckets, _
-        hashFunction : Key -> I)
-    localSearch(a : Buckets, k : Key, h : Key -> I) : Z ==
-        n : Z := numOfBuckets a
-        h1 : Z := (h k)::Z
-        p : Z := positiveRemainder(h1, n) -- position in array
-        h2 : Z := 1 + positiveRemainder(h1, n-2)
-        mk : MKey := getMKey(a, p)
-        deletedPosition? : Boolean := false
-        while not vacant? mk repeat
-            deleted? mk => (deletedPosition? := true; break)
-            k = toKey mk => return p -- key found
-            p := p + h2
-            if p>=n then p := p-n
-            mk := getMKey(a, p)
-        q := p -- first position of a free entry
-        -- We ignore DELETED entries when looking for the key.
-        while not vacant? mk repeat
-            not deleted? mk and k = toKey mk =>
-                setKeyEntry!(a, n, q, k, getEntry(a, n, p))
-                deleteKeyEntry!(a, n, p)
-                return q -- entry has been copied to previous DELETED position
-            p := p + h2
-            if p>=n then p := p-n
-            mk := getMKey(a, p)
-        if deletedPosition? then q := q-n
-        q-n -- KEY not found.
    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) )

added:
  Now we can use our little program.

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


A very brief introduction to programming in SPAD

  • SPAD is an ordinary programming language, just like C, Java, and Python.
  • SPAD programs are compiled to machine code by the SPAD compiler that comes with FriCAS?.
  • SPAD is a statically typed language with type levels.
    1. Elements: These are the basic data objects. Examples are: 42, 3.14159265, "abc", [3,5,11]. It is one one usually consideres as values in other programming languages.
    2. Domains: These are the types of elements. For example, Integer is a type for 42, 3.14 is of type Float, "abc" is of type String, [1,2,4,8] is of type List(Integer).

      Domains are comparable to classes in object oriented programming languages.

    3. Categories: These are the types of domains. For example, Integer is of type IntegerNumberSystem, String is of type StringCategory, List(Integer) is of type ListAggregate(Integer).

      Categories are somewhat comparable to interfaces in Java, but are much more powerful.

    4. The highest type level is the constant keyword Category. In other words, IntegerNumberSystem, StringCategory, ListAggregate(Integer) are of type Category.
  • SPAD programs are usually definitions of categories and domains whose functionality will later be used in an interactive session or by other definitions.
  • While categories define the exports of domains, i.e. which function are provided, domains themselves implement the corresponding functions.
  • Domains form a type hierarchy where only inheritance from one other domain is allowed.
  • Categories form a type hierarchy with a multiple inheritance mechanism.
  • Categories and domains are often called constructors and (as shown above) can be parametrized.
  • SPAD has only very few built-in constructors. Most of the constructors are defined in a library. Builtin are Record, Tuple, Join, Mapping (abbreviated via ->). Library defined are Integer, List, String, Symbol, Monoid, Field, etc.

A running example

Let us start with a little program. We try not to rely on any previously defined library, but we prefix every constructor with My in order to avoid name conflicts with existing names.

Our goal is to provide a domain MyFun that is parametrized by a domain S and represents functions from S into itself. We would like to be able to turn any function of type S -> S into an element of the MyFun(S) domain. Furthermore, we want to turn this domain into a monoid MyMonoid.

First we define the category MyMonoid.

spad
)abbrev category MYMON MyMonoid
MyMonoid: Category == with
    1: %
    _*: (%, %) -> %
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3904508595934233674-25px001.spad
      using old system compiler.
   MYMON abbreviates category MyMonoid 
------------------------------------------------------------------------
   initializing NRLIB MYMON for MyMonoid 
   compiling into NRLIB MYMON 
;;; *** |MyMonoid| REDEFINED Time: 0.01 SEC.
finalizing NRLIB MYMON Processing MyMonoid for Browser database: --->-->MyMonoid(constructor): Not documented!!!! --->-->MyMonoid(((One) (%) constant)): Not documented!!!! --->-->MyMonoid((* (% % %))): Not documented!!!! --->-->MyMonoid(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.lsp" (written 14 FEB 2014 02:02:18 AM):
; /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.fasl written ; compilation finished in 0:00:00.005 ------------------------------------------------------------------------ MyMonoid is now explicitly exposed in frame initial MyMonoid will be automatically loaded when needed from /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON

Every constructor needs an )abbrev line where one specifies whether the constructore to come is a category or domain. Then follows a capitalized identifier of at most 7 characters and finally the identifier for the constructor.

By convention, constructors begin with an uppercase letter and capitalize the first letter of each new word. Underscores are not commonly used.

Supposed the above code goes into a file mymonoid.spad, then this file can be compiled via:

    )compile mymonoid.spad

indide a FriCAS? session.

Now comes the corresponding domain definition.

spad
rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %
)abbrev domain MYFUN MyFun MyFun(S: SetCategory): MyMonoid 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/2899365196648008240-25px002.spad
      using old system compiler.
   MYFUN abbreviates domain MyFun 
------------------------------------------------------------------------
   initializing NRLIB MYFUN for MyFun 
   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)
;;; *** |MyFun| REDEFINED
;;; *** |MyFun| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor MyFun Time: 0 seconds
finalizing NRLIB MYFUN Processing MyFun for Browser database: --->-->MyFun(constructor): Not documented!!!! --->-->MyFun((myfun (% (Mapping S S)))): Not documented!!!! --->-->MyFun((coerce ((Mapping S S) %))): Not documented!!!! --->-->MyFun(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.lsp" (written 14 FEB 2014 02:02:18 AM):
; /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.fasl written ; compilation finished in 0:00:00.018 ------------------------------------------------------------------------ MyFun is now explicitly exposed in frame initial MyFun will be automatically loaded when needed from /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN

Now we can use our little program.

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    := myfun inc
fricas
Compiling function inc with type Integer -> Integer 
LISP output: (#<FUNCTION |*1;inc;1;initial|>)
Type: MyFun?(Integer)
fricas
mdouble := myfun double
fricas
Compiling function double with type Integer -> Integer 
LISP output: (#<FUNCTION |*1;double;1;initial|>)
Type: MyFun?(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?