Subject: spiderweb

From: Dave Mason <[email-masked]>
Date: Wed, 5 Aug 1992 17:07:26 -0400

I talked to you at PLDI about SML spiderweb.  I haven't had any time to work
on it, so I decided to send you what I had.

Included is a diff of weave.web to treat _ as a non-identifier, and to treat
' as part of an identifier if it immediately follows something that is
already treated as an identifier.

Also included is sml.spider.  It isn't perfect, but it works fairly well.
There are 3 special tokens: |: |= and |; that are useful to have different
paragraphs be working on a common function or datatype.  Sorry I don't have
documentation, but I am not 100% happy with the system yet.  BTW, the |;
could be removed, and the grammar made *much* simpler if there were a
special token for the END of a code block.

Finally, I've included a web file for a denotational semantics that I wrote.
It exhibits the three special tokens.

Are you, or anyone else, working on moving spiderweb so it would work with
LaTeX?  I would *love* to be able to import small (or not so small) code
segments into my latex documents (particularly for overheads).

I'm off for vacation most of the rest of the month.  I plan to do the LaTeX
thing when I get back, if no-one else is working on it.  I will also be
doing a fair bit of sml hacking in the fall, and I'm likely to be using web,
so the sml stuff will get cleaned up some.

	../Dave

------------------------------------start of diff-------------------
*** weave.web   Sun Mar 29 02:54:59 1992
--- weave.webO  Wed Nov 13 19:48:26 1991
***************
*** 85,93 ****
  @d max_refs = 20000 /* number of cross-references; must be less than 65536 */
  @d max_toks = 20000 /* number of symbols in \cee\ texts being parsed;
    must be less than 65536 */
! @d max_texts = 4000 /* number of phrases in \cee\ texts being parsed;
    must be less than 10240 */
! @d max_scraps = 2000 /* number of tokens in \cee\ texts being parsed */
  @d stack_size = 400 /* number of simultaneous output levels */

  @i common.h
--- 85,93 ----
  @d max_refs = 20000 /* number of cross-references; must be less than 65536 */
  @d max_toks = 20000 /* number of symbols in \cee\ texts being parsed;
    must be less than 65536 */
! @d max_texts = 2000 /* number of phrases in \cee\ texts being parsed;
    must be less than 10240 */
! @d max_scraps = 1000 /* number of tokens in \cee\ texts being parsed */
  @d stack_size = 400 /* number of simultaneous output levels */

  @i common.h
***************
*** 543,549 ****
        }
      }
      if (isdigit(c)) @<Get a constant@>@; /*spider*/
!     else if (isalpha(c) || (c=='_' && (*loc=='_' || isalpha(*loc)))) @<Get an
identifier@>@;/*spider*/
      else if (c=='\'' || c=='"') @<Get a string@>@;/*spider*/
      else if (c==at_sign) @<Get control code and possible module name@>@;
      else if (c==' ' || c==tab_mark) continue; /* ignore spaces and tabs */
--- 543,549 ----
        }
      }
      if (isdigit(c)) @<Get a constant@>@; /*spider*/
!     else if (isalpha(c) || c=='_') @<Get an identifier@>@;/*spider*/
      else if (c=='\'' || c=='"') @<Get a string@>@;/*spider*/
      else if (c==at_sign) @<Get control code and possible module name@>@;
      else if (c==' ' || c==tab_mark) continue; /* ignore spaces and tabs */
***************
*** 557,563 ****

  @ @<Get an identifier@>= {/*spider*/
    id_first=--loc;
!   while (isalpha(*++loc) || isdigit(*loc) || *loc=='_' || *loc=='\'');
    id_loc=loc; return(identifier);
  }

--- 557,563 ----

  @ @<Get an identifier@>= {/*spider*/
    id_first=--loc;
!   while (isalpha(*++loc) || isdigit(*loc) || *loc=='_');
    id_loc=loc; return(identifier);
  }

------------------------------------end of diff-------------------
---------------------------------start of sml.spider-------------
# Copyright 1989 by Norman Ramsey, Odyssey Research Associates
# Not to be sold, but may be used freely for any purpose
# For more information, see file COPYRIGHT in the parent directory
language SML extension sml

at_sign %

module definition codedef use codeuse

comment begin <"(*"> end <"*)">

line begin <"(*line"> end <"*)">

default translation <*> mathness yes

token identifier category id mathness maybe
token number category const mathness yes
token newline category ignore_scrap translation <> mathness maybe 
token pseudo_semi translation <> category semi mathness maybe

macros begin
\let\R\relax
\def\SS{\relax\ifmmode\>\else$\>$\fi}
\def\UL{\relax\ifmmode\_\!\_\,\else$\_\!\_\,$\fi}
\def\FL.#1#2#3(#4){\relax\ifmmode#4^{\rm{#2}}\else$#4^{\rm{#2}}$\fi}
\def\SL#1{\relax\ifmmode{}_{#1}\else${}_{#1}$\fi}
\def\LA{\relax\ifmmode\leftarrow\else$\leftarrow$\fi}
\def\GK#1#2{\if#2a\alpha\else\if#2b\beta\else\if#2c\gamma\else\if#2d\delta\else\if#2e\varepsilon\else\if#2f\zeta\else\if#2g\eta\fi\fi\fi\fi\fi\fi\fi^{^{#1}}}
\def\'#1#2#3{\relax\ifmmode\GK{#1}{#3}\else$\GK{#1}{#3}$\fi}
\def\"#1#2{\relax\ifmmode\GK{=}{#2}\else$\GK{=}{#2}$\fi}
\def\ST#1{\relax\ifmmode\times\else$\times$\fi}
macros end

# Delimiters
#token & category binop translation <"\\amp">
token ( category open 
token ) category close 
token [ category open 
token ] category close 
token { category ocurly translation <"\\{">
token } category ccurly translation <"\\}">
token [. category open tangleto <space-"sub("> translation <"\\SL{"> mathness maybe
token .] category close tangleto <")"> translation <"}"> mathness maybe
token [= category open tangleto <space-"assign("> translation <"\\SL{"> mathness maybe
token =] category close tangleto <")"> translation <"}\\LA"> mathness maybe
token * category star mathness maybe
token + category binop
token , category comma translation <",\\,"-opt-5>
token - category binop
token ^ category binop translation <"\\^">
token ! category unop
token ~ category unop
token . category dot
token @ category binop
token # category unop translation <"\\FL.">
token / category binop
token : category tylook
token ; category semi
token < category binop
token = category equal
token > category binop
token | category choice translation <"\\mid"> 
token |: category datam translation <"\\mid"> tangleto <"|">
token |= category fun translation <"\\mid"> tangleto <"|">
token |; category semi translation <""> tangleto <""> mathness maybe
token _ category underline translation <"\\UL"> mathness no
token ' category tick tangleto <space-"'"> translation <"\\'{"> mathness maybe
token '' category tick tangleto <space-"''"> translation <"\\'{="> mathness maybe
token ... category labpat translation <"\\cdots"> mathness yes

# Compound delimiters

token := category binop translation <"\\mathbin{:=}">
token :: category binop translation <"\\mathbin{::}">
token => category arrow translation <"\\Rightarrow">
token -> category fnarrow translation <"\\mapsto">
#token /= translation <"\\I"> category binop 
token >= translation <"\\G"> category binop 
token <= translation <"\\L"> category binop 
#token << translation <"\\LL"> category openlabel 
#token >> translation <"\\GG"> category closelabel 
#token <> translation <"\\LG"> category math

#token # category math translation <"\\#"> 

token && category binop tangleto <space-"andalso"-space> mathness yes translation <"\\wedge">
token || category binop tangleto <space-"orelse"-space> mathness yes translation <"\\vee">

default mathness maybe translation <*>

reserved abstraction ilk abstraction_like
reserved abstype ilk abstype_like
reserved and ilk and_like
reserved andalso ilk andalso_like
reserved array ilk math_like
reserved as ilk as_like
reserved case ilk case_like
reserved datatype ilk datatype_like
reserved do ilk do_like
reserved else ilk else_like
reserved end ilk end_like
reserved eqtype ilk type_like
reserved exception ilk ex_like
reserved false ilk const_like
reserved fn ilk fn_like
reserved fun ilk fun_like
reserved functor ilk functor_like
reserved handle ilk handle_like
reserved if ilk if_like
reserved in ilk in_like
reserved int ilk int_like
#reserved infix ilk infix_like 
#reserved infixr ilk infix_like 
reserved let ilk let_like
reserved list ilk list_like
reserved local ilk local_like
#reserved nonfix ilk infix_like 
reserved not ilk unop_like
reserved nil ilk const_like
reserved of ilk of_like
#reserved op ilk op_like
reserved open ilk open_like
reserved orelse ilk orelse_like
reserved overload ilk overload_like
reserved raise ilk raise_like
reserved rec ilk rec_like
reserved ref ilk ref_like
#reserved sharing ilk sharing_like
reserved sig ilk sig_like
reserved signature ilk signature_like
reserved string ilk int_like
reserved struct ilk struct_like
reserved structure ilk structure_like
reserved then ilk then_like
reserved true ilk const_like
reserved type ilk type_like
reserved unit ilk int_like
reserved val ilk val_like
reserved while ilk while_like
reserved with ilk with_like
reserved withtype ilk withtype_like
reserved orelse ilk binop_like

ilk overload_like translation <*> category keyword
ilk abstraction_like translation <*> category keyword

ilk abstype_like translation <*> category abstype
ilk and_like translation <*> category and
ilk andalso_like category binop mathness yes translation <"\\wedge">
ilk as_like translation <*> category id
ilk binop_like translation <"\\"-space-*-"\\"-space> category binop
ilk case_like translation <*> category case
ilk const_like translation <*> category const
ilk datatype_like translation <*> category datatype
ilk do_like translation <*> category do
ilk else_like translation <*> category else
ilk end_like translation <*> category end
ilk ex_like translation <*> category exception
ilk fn_like category fn mathness yes translation <"\\lambda\\"-space>

ilk fun_like translation <*> category fun
ilk functor_like translation <*> category functor
ilk handle_like translation <*> category handle
ilk if_like translation <*> category if
ilk in_like translation <*> category in
ilk int_like translation <*> category ty
ilk let_like translation <*> category let
ilk list_like translation <*> category id
ilk local_like translation <*> category local
ilk math_like translation <*> category math
ilk of_like translation <*> category of
ilk open_like translation <*> category openop
ilk orelse_like category binop  mathness yes translation <"\\vee">
ilk raise_like translation <*> category raise
ilk rec_like translation <*> category rec
ilk ref_like translation <*> category id
ilk sig_like translation <*> category sig
ilk signature_like translation <*> category signature
ilk struct_like translation <*> category struct
ilk structure_like translation <*> category val
ilk then_like translation <*> category then
ilk type_like translation <*> category type
ilk unop_like translation <*-"\\"-space> category unop
#ilk unorbinop_like translation <"\\"-space-*-"\\"-space> category resunorbinop
ilk val_like translation <*> category val
ilk while_like translation <*> category while
ilk with_like translation <*> category with
ilk withtype_like translation <*> category withtype

# \MC means ``math close'' and sets \MS to ``math set''
macros begin
\def\MC{\ifmmode\global\let\MS$\else\global\let\MS\relax\fi\relax\MS}
\def\LG{\mathord{<}\mathord{>}}
\let\IG=\ignorespaces
macros end

codedef dec --> dec
[ codedef (math|multimath) ] semi --> dec semi
codeuse <force> codeuse --> codeuse
codeuse semi  --> codeuse
!ignore_scrap [ codeuse ] !(codeuse|ignore_scrap|semi|val|fun|type|let|struct|openop|end|in) --> !ignore_scrap multimath !(codeuse|ignore_scrap|semi|val|fun|type|let|struct|openop|end|in)
 [ codeuse ] (dec|end|in) --> dec (dec|end|in)
 [ codeuse ] semi (dec|end|in) --> dec semi (dec|end|in)

id dot id --> id
ty dot id --> ty

sig <indent-force> dec <outdent-force> end --> sig_body
signature <"\\"-space> id* equal <indent-force> sig_body <outdent> --> dec
functor [ <"\\"-space> id* ] --> functor funhead
functor funhead pat equal <force-indent> struct_object <outdent>  --> dec
struct <force-indent> dec <force-outdent> end --> struct_object
openop <"\\"-space> id --> dec

exception <"\\"-space> --> exlook
exlook eb --> dec
exlook [ id* ] !(of|equal) --> exlook eb !(of|equal)
exlook [ id* <"\\"-space> of <"\\"-space> ] --> exlook tylook
exlook [ tylook <"\\"-space> ty ] --> exlook eb
exlook [ id* equal id ] --> exlook eb
eb and --> exlook

(tylook|tyopen|tys|tya|datatop|datarest) [ id ] --> (tylook|tyopen|tys|tya|datatop|datarest) ty
(tylook|tyopen|tys|tya|datatop|datarest) [ ty <"\\"-space> id ] --> (tylook|tyopen|tys|tya|datatop|datarest) ty
(tylook|tyopen|tys|tya|datatop|datarest) [ ocurly labty ccurly ] --> (tylook|tyopen|tys|tya|datatop|datarest) ty
(tylook|tyopen|tys|tya|datatop|datarest) ocurly [ id tylook ty ] !id --> (tylook|tyopen|tys|tya|datatop|datarest) ocurly labty !id
(tylook|tyopen|tys|tya|datatop|datarest) [ ocurly labty comma ] --> (tylook|tyopen|tys|tya|datatop|datarest) ocurly
(tylook|tyopen|tys|tya|datatop|datarest) [ open ] --> (tylook|tyopen|tys|tya|datatop|datarest) tyopen
(tylook|tyopen|tys|tya|datatop|datarest) [ tyopen ty close ] --> (tylook|tyopen|tys|tya|datatop|datarest) ty
(tylook|tyopen|tys|tya|datatop|datarest) [ tys ty close <"\\"-space> id ] --> (tylook|tyopen|tys|tya|datatop|datarest) ty
tys ty comma --> tys
tys ty <"\\ST"> star --> tys
tys ty close --> ty
(tylook|tyopen|tys|tya|datatop|datarest) [ tyopen ty comma ] --> (tylook|tyopen|tys|tya|datatop|datarest) tys
(tylook|tyopen|tys|tya|datatop|datarest) [ tyopen ty <"\\ST"> star ] --> (tylook|tyopen|tys|tya|datatop|datarest) tys
tick const <"}"> id --> ty
tick <"}"> id --> ty
(tylook|tyopen|tys|tya|datatop|datarest) [ ty fnarrow ] --> (tylook|tyopen|tys|tya|datatop|datarest) tya
tya ty --> ty

val <"\\"-space> rec --> val
val [ <"\\"-space> pat* <"\\"-space> equal <"\\"-space-indent-opt-1> math <outdent> ] (semi|val|fun|type|let|struct|openop|and|end|close|in|val) --> val valbody (semi|val|fun|type|let|struct|openop|and|end|close|in|val)
val [ <"\\"-space> pat* ] (semi|val|fun|type|let|struct|openop|and|end|close|in|val) --> val valbody (semi|val|fun|type|let|struct|openop|and|end|close|in|val)
val [ <"\\"-space> pat* <"\\"-space> equal <indent-force> multimath <outdent> ] (semi|val|fun|type|let|struct|openop|and|end|close|in) --> val valbody (semi|val|fun|type|let|struct|openop|and|end|close|in)
<force> val valbody <force> and  --> val
<force> val valbody --> dec
datatop <"\\"-space-indent> codeuse <force> --> datahead
datatop <"\\"-space> ty* <"\\"-space-indent> equal <force> --> datat
datarest <"\\"-space> ty* <"\\"-space> equal <"\\"-space-indent-opt-2> id <"\\"-space> of <"\\"-space> --> datarest
(datat|datam) <"\\"-space> id <"\\"-space> of <"\\"-space> --> datarest
[ datat <"\\"-space> id* <"\\"-space-opt-1> choice ] id !of --> datat id !of
[ datat <"\\"-space> id* <force> choice ] id of --> datam id of
datam <"\\"-space> id* <force> choice --> datam
[ datat <"\\"-space> ty ] comma --> datahead comma
[ datat <"\\"-space> ty ] <"\\ST"> star --> datahead star
[ datarest ty ] !(equal|ignore_scrap) --> datahead !(equal|ignore_scrap)
datahead comma --> datarest
datahead <"\\ST"> star --> datarest
datahead <force> choice --> datam
[ (datat|datam) <"\\"-space> id <outdent-outdent> ] (semi|val|fun|type|datatype|let|struct|openop|end|in) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in)
[ datahead <outdent-outdent> ] (semi|val|fun|type|datatype|let|struct|openop|end|in) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in)
datat <"\\"-space> id <outdent-force> (and|withtype) --> datatop
datahead <outdent-force> (and|withtype) --> datatop
datatype <indent> --> datatop
abstype <indent> --> datatop
datahead <outdent-outdent-force> with <indent-force> dec <outdent-force> end --> dec
type <"\\"-space> ty --> type
type pat [ equal ] --> type pat tylook
[ type <"\\"-space> pat* tylook ty ] (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)
[ type <"\\"-space> pat* ] (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)

(equal|arrow) [ <cancel-"\\SS"-space> let ] --> (equal|arrow) letf
!(ignore_scrap|equal|arrow) [ let ] --> !(ignore_scrap|equal|arrow) letf
letf <indent-force> dec <outdent-force> in <indent-force> (math|multimath) <outdent-force> end --> multimath
local <indent-force> dec <outdent-force> in <indent-force> dec <outdent-force> end --> dec

dec <cancel> semi <force> --> dec
[ (math|multimath) <cancel> semi ] dec --> dec dec
[ (math|multimath) ] dec --> dec dec
dec [ <force> (math|multimath) ] (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> dec dec (semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)
[ dec <force> dec ] !(semi|ignore_scrap) --> dec !(semi|ignore_scrap)

[ case <"\\"-space> (math|multimath) <indent-force> of multimatch <outdent> ] (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> multimath (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)
[ <indent-force> fn (multimatch|match) <outdent> ] (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> multimath (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)
[ (math|multimath) <indent-indent-force> handle <indent-indent-indent> (multimatch|match) <outdent-outdent-outdent-outdent-outdent> ] (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and) --> multimath (close|semi|val|fun|type|datatype|let|struct|openop|end|in|with|withtype|and)

[ <"\\"-space> pat <"\\"-space> arrow <indent-indent-"\\"-space-opt-3> math <outdent-outdent-opt-1> ] (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and) --> match (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and)
[ <"\\"-space> pat <"\\"-space> arrow <indent-indent-force> multimath <outdent-outdent> ] (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and) --> multimatch (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and)
(match|multimatch) <force-"\\"-space> choice (match|multimatch) --> multimatch
[ match ] (semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and) --> multimatch (semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and)

fun [ <"\\"-space> id* ] --> fun funhead
fun funbody <force-"\\"-space-"\\"-space> choice <"\\"-space> --> fun
[ fun funbody ] (in|semi|val|fun|type|datatype|let|struct|openop|end) --> dec (in|semi|val|fun|type|datatype|let|struct|openop|end)
fun funbody <force> and --> fun
fun [ funhead <"\\"-space> pat <"\\"-space> equal <indent-indent-"\\"-space-opt-1> math <outdent-outdent> ] !(binop|handle|math|id|open|multimath|ignore_scrap) --> fun funbody !(binop|handle|math|id|open|multimath|ignore_scrap)
fun [ funhead <"\\"-space> pat <"\\"-space> equal <indent-indent-force> multimath <outdent-outdent-force> ] !(binop|handle|math|id|open|multimath|ignore_scrap) --> fun funbody !(binop|handle|math|id|open|multimath|ignore_scrap)

equal [ <force> multimath ] --> equal math
[ if <"\\"-space> (math|multimath) <"\\"-space> then <indent-force> (math|multimath) <outdent-force> else <indent-force> (math|multimath) <outdent> ] (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and) --> multimath (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and)

[ while <"\\"-space> (math|multimath) <"\\"-space> do <indent-force> <"\\"-space> (math|multimath) <outdent> ] (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and) --> multimath (choice|semi|val|fun|type|datatype|let|struct|openop|end|close|in|with|withtype|and)

apat --> pat
(choice|funhead|of|fn|handle|val|type) [ (pat|id) <"\\"-space> (apat|id) ] --> (choice|funhead|of|fn|handle|val|type) pat
[ pat tylook ty ] !(fnarrow|id|dot|ignore_scrap) --> pat !(fnarrow|id|dot|ignore_scrap)
pat (binop|star) (math|pat) --> pat
pat <"\\"-space> pat --> pat

underline --> apat
(choice|funhead|of|fn|handle|val|type|opat|pat) [ id ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) apat
(choice|funhead|of|fn|handle|val|type|opat|pat) [ const ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) apat
(choice|funhead|of|fn|handle|val|type|opat|pat) [ open ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) opat
(choice|funhead|of|fn|handle|val|type|opat|pat) [ open <"\\,"> close ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) apat
opat close --> apat
opat pat close --> apat
opat pat comma --> opat
[ open ] pat --> opat pat

ocurly id equal math --> ocmath
(ocurly|ocurlym) id equal multimath --> ocmulti
ocmath comma --> ocurly
ocmath ccurly --> math
ocmulti comma --> ocurlym
ocmulti ccurly --> multimath
ocurly ccurly --> const
(choice|funhead|of|fn|handle|val|type|opat|pat) [ ocurly labpat ccurly ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) apat
(choice|funhead|of|fn|handle|val|type|opat|pat) ocurly id [ equal ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) ocurly id choice
(choice|funhead|of|fn|handle|val|type|opat|pat) ocurly [ id choice pat ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) ocurly labpat
(choice|funhead|of|fn|handle|val|type|opat|pat) ocurly [ id ] !equal --> (choice|funhead|of|fn|handle|val|type|opat|pat) ocurly labpat !equal
(choice|funhead|of|fn|handle|val|type|opat|pat) [ ocurly labpat comma ] --> (choice|funhead|of|fn|handle|val|type|opat|pat) ocurly

raise <"\\"-space> math --> math
math comma math --> math
math (binop|star) math --> math
unop math --> math
(math|multimath) <cancel-space-force> comma <cancel> (multimath|math) --> multimath
(math|multimath) (binop|star) (math|multimath) --> multimath
unop (math|multimath) --> multimath
math <"\\"-space> math --> math
(math|multimath) <"\\"-space> (math|multimath) --> multimath

open <"\\,"> close --> const
[ open <indent> math <outdent> close <opt-1> ] !(ignore_scrap|close|semi|val|fun|type|datatype|let|struct|openop|in|with|withtype|end) --> math !(ignore_scrap|close|semi|val|fun|type|datatype|let|struct|openop|in|with|withtype|end)
[ open <indent-opt-3> math <outdent> close ] (close|semi|val|fun|type|datatype|let|struct|openop|in|with|withtype|end) --> math (close|semi|val|fun|type|datatype|let|struct|openop|in|with|withtype|end)
[ (math|multimath) <force-backup-"\\SS\\SS"> semi <"\\SS"> (math|multimath) ] (semi|val|fun|type|datatype|let|struct|openop|close|end) --> multimath (semi|val|fun|type|datatype|let|struct|openop|close|end)
(then|semi|else|in|equal|arrow) [ open <indent-"\\"-space-"\\"-space> multimath <outdent-force-"\\SS\\SS"> close ] --> (then|semi|else|in|equal|arrow) multimath
!(then|semi|else|in|equal|arrow) [ open <indent-indent-force> multimath <outdent-force-"\\"-space-"\\"-space> close <outdent> ] --> !(then|semi|else|in|equal|arrow) multimath

math [ equal ] --> math binop
[ math tylook ty ] !(ignore_scrap|id|dot|fnarrow) --> pat !(ignore_scrap|id|dot|fnarrow)
id <"\\"-space> math --> math
(multimath|semi|equal|dec|while|do|case|then|else|if|in|with|withtype|open|raise|arrow|comma|math|binop|star|unop) [ id ] !dot --> (multimath|semi|equal|dec|while|do|case|then|else|if|in|with|withtype|open|raise|arrow|comma|math|binop|star|unop) math !dot
(multimath|semi|equal|dec|while|do|case|then|else|if|in|with|withtype|open|raise|arrow|comma|math|binop|star|unop) [ const ] --> (multimath|semi|equal|dec|while|do|case|then|else|if|in|with|withtype|open|raise|arrow|comma|math|binop|star|unop) math

? ignore_scrap --> #1
ignore_scrap ? --> #2

macros begin
\let\AR=\Longrightarrow
macros end
---------------------------------end of sml.spider-------------
---------------------------------start of denote.web-------------
\def\topofcontents{\relax\ifodd\pageno\else\null\vfill\eject\null\fi\titletrue\null\vfill
	\centerline{\titlefont Denotional Semantics and}
	\centerline{\titlefont an {\ttitlefont ML} Interpreter}
	\centerline{\titlefont for a Functional Programming Language}
	\vfill
	\centerline{Table of Contents}
}
\def\botofcontents{\null\vfill
	\centerline{\copyright\ 1991, Dave Mason {\tt <[email-masked]>}}
}
\let\contentspagenumber=\pageno

\def\ME#1{{\ifmmode\lbrack\!\lbrack#1\rbrack\!\rbrack\else$\lbrack\!\lbrack$#1$\rbrack\!\rbrack$\fi}}
\def\Me#1{{\bf Me}\ME{#1}}
\def\St{\relax\ifmmode\sigma\else$\sigma$\fi}
\def\Co{\relax\ifmmode\theta\else$\theta$\fi}
\def\CO{\relax\ifmmode\Theta\else$\Theta$\fi}
\def\IV{\relax\ifmmode\Xi\else$\Xi$\fi}
\def\En{\relax\ifmmode\rho\else$\rho$\fi}
\def\Ex{\relax\ifmmode\varepsilon\else$\varepsilon$\fi}
\def\Sy{\relax\ifmmode\xi\else$\xi$\fi}
\def\Nu{\relax\ifmmode\nu\else$\nu$\fi}
\def\Lo{\relax\ifmmode\phi\else$\phi$\fi}
\def\Tp#1#2{\langle{#1},{#2}\rangle}
 %*Denotational Semantics.  Denotational semantics is a formal method
to specify the meaning of programming languages.  We define an
abstract syntax for the language (|Term|), a meaning function (|Me|),
a polymorphic store (|store|) and a polymorphic environment (|env|).

The code is laid out in this document in a logical form (rather than
slavishly following the order the compiler wants), but we
must force the \.{ML} code into the right order to make sure that
things are defined before use.
 %c
 %<Type Definitions%>
 %<Functions%>
 %<Meaning Function%>;
 %<Test Cases%>

 % This is the type of possible declarations, along with the start of
the definition of possible terms.  They are mutually recursive
definitions so they must be connected by an |and|.  The actual
declaration type are explained below in the definition of the semantic
function for declarations.
 %<Type Definitions%>=
datatype Decl =
        Var_Decl of string * Term
 |      Val_Decl of string * Term
 |      Rec_Decl of string * Term
and
	%<Term Definition%>;

 %*|Term| and |Me|.  We define the datatype for the abstract syntax
tree and the meaning function in parallel.  \.{Web} will worry about
putting it all together in the right order.

The meaning function has to have type:

 |Me : Term -> (Value env) -> (Value continuation) -> (Value store) -> (Value * (Value store)) |.

 That is, it maps abstract syntax trees, environments, continuations,
and stores to a value,store pair.

 % The denotational semantics are given in terms of the following:
 \medskip
 \itemitem {\bf Me} - this is the meaning function itself.
 \itemitem {\IV} - is an invalid value
 \itemitem {\Ex} - an expression
 \itemitem {\Sy} - a symbol
 \itemitem {\Nu} - a number
 \itemitem {\En} - the environment (bindings from names to values)
 \itemitem {\Co} - this is the continuation
 \itemitem {\CO} - this is a null continuation that simply returns the value
 \itemitem {\St} - this is the store of values
 \itemitem {\Lo} - a location in the store
 \itemitem {$x[e/v]$} - a substitution of the expression $e$ for the name
(or whatever) $v$, where $x$ is usually \En\ or \St
 \itemitem {$x\ME{v}$} - $v$ in the context of $x$, where $x$ is {\bf Me},
\En, \St, {\bf O} or {\bf V}
 \itemitem {$\Tp{x}{y}$} - the tuple composed of $x$ and $y$
 \itemitem {$\{e\}$} - a continuation that evaluates $e$ in the current
context
 \medskip
 \noindent When either of the environment or store are omitted, the
environment or store from the enclosing environment is assumed.

 % The first type of term is the name of a variable or constant.  The
meaning of a name is the value that the environment contains for that
name.  For variables, this value is the location in the store where
the value may be found.
 %<Term Definition%>=
 Term =         Var of string
 % $\Me{\Sy}\En\Co\St=\Co\Tp{\En\ME{\Sy}}{\St}$
 %<Meaning Function%>=
 fun Me (Var x) e c s = c (lookup x e ,s)
 |;

 % Integer constants.
 %<Term Definition%>=
 |:      Numeral of int
 % $\Me{\Nu}\En\Co\St=\Co\Tp{{\bf V}\ME{\Nu}}{\St}$
 %<Meaning Function%>=
 |= Me (Numeral n) e c s = c (intValue n,s)
 |;

 %*Declarations.

Declarations come in 3 flavours: {\tt val}, {\tt rec}, and {\tt
var}. For all three, the declaration only holds for the evaluation of
the expression with which it is composed.  {\tt val} introduces a
constant. {\tt rec} is similar but the symbol is introduced into the
environment of the expression (which must be a function) to allow for
recursive calls. {\tt var} introduces a variable.
 %<Term Definition%>=
 |:      Decl of Decl * Term
 % $\Me{{\tt var}~\Sy~{\tt =}~\Ex_1~{\tt ;}~\Ex_2}\En\Co\St=\Me{\Ex_2}\En[\Lo/\Sy]\Co\St[\Me{\Ex_1}\En\CO\St/\Lo]$
 %<Meaning Function%>=
 |= Me (Decl (Var_Decl (x,V),E)) e c s =
	Me V e (fn (R,_) => let
	val (S,L) = new s R;
 	val nE = bind x (lvalueValue L) e;
	in Me E nE c S end) s
 |;

 % $\Me{{\tt val}~\Sy~{\tt =}~\Ex_1~{\tt ;}~\Ex_2}\En\Co\St=\Me{\Ex_2}\En[\Me{\Ex_1}\En\CO\St/\Sy]\Co\St$
 %<Meaning Function%>=
 |= Me (Decl (Val_Decl (x,V),E)) e c s =
	Me V e (fn (R,_) => Me E (bind x R e) c s)s
 |;

 % The interpretation of the recursive declaration ($\Me{{\tt
rec}~\Sy~{\tt =}~\Ex_1~{\tt ;}~\Ex_2}\En\Co\St$) is fairly difficult
to describe, short of translating the ML code.  There are a couple of
ways of doing this, but the one I chose is to implement the Y
combinator ({\tt fix}) in the language and then apply it to the
functional we want to make recursive.  To bootstrap the process, we
put an entry for {\tt fix} into the environment as a var name with an
initial binding to an invalid value, which we replace once we have a
definition for the function proper.  If we were looking for
efficiency, we'd put these in the initial environment and store.
 %<Meaning Function%>=
 |= Me (Decl (Rec_Decl (x,V),E)) e c s = let
	val fixpoint=Proc ("fix-f",
		Proc ("fix-x", App	(App	(Var "fix-f",
				App (Deref (Var "fix"),Var "fix-f"))
			,Var "fix-x")));
	val (S,L) = new s invalidValue;
 	val nE = bind "fix" (lvalueValue L) e;
	in
	Me fixpoint nE (
	    fn (FIX,_) => Me (App (Deref (Var "fix"),Proc(x,V))) nE (
		fn (funcValue R,S) => Me E (bind x (funcValue R) e) c S
		|_=>raise NotFuncDecl) (update S L FIX)
	  ) S
	end

 |;

 %*Function operations.

 Function abstraction.  Define a function of one parameter bound in
the scope of the expression.
 %<Term Definition%>=
 |:      Proc of string * Term
 % $\Me{{\tt proc}~\Sy~{\tt =>}~\Ex}\En\Co\St=\Co\Tp{\lambda\Co'.\lambda\Tp{V}{\St'}.\Me{\Ex}\En[V/\Sy]\Co'\St'}{\St}$
 %<Meaning Function%>=
 |= Me (Proc (x,E)) e c s =  
	c (funcValue (fn C => fn (V,S) => Me E (bind x V e) C S ),s)
 |;

 % Function Application.  Supply one parameter to the function and
execute the function.
 %<Term Definition%>=
 |:      App of Term * Term
 % The interpretation of function application
($\Me{\Ex_1{\tt(}\Ex_2{\tt)}}\En\Co\St$) is basically going to be a translation
of the ML code.
 %<Meaning Function%>=
 |= Me (App (E1,E2)) e c s =
	Me E1 e (fn (funcValue f,_) =>
			Me E2 e (fn VS => f c VS) s
		 |_ =>raise NotFunc
	) s
 |;

 % Call the specified function passing our continuation as a
functional parameter.
 %<Term Definition%>=
 |:      Callcc of Term

 % The interpretation of function application
($\Me{{\tt callcc}~\Ex}\En\Co\St$) is basically going to be a translation
of the ML code.
 %<Meaning Function%>=
 |= Me (Callcc E) e c s =
	Me E e (fn (funcValue f,_) =>
			f c (funcValue (fn (C:Value continuation) => c),s)
		 |_ =>raise NotFunc
	)s
 |;

 %*Operations on Pairs.

 Create a pair from the values of two expressions.
 %<Term Definition%>=
 |:      Pair of Term * Term
 % $\Me{{\tt <}\Ex_1{\tt ,}\Ex_2{\tt >}}\En\Co\St=\Co\Tp{\Me{\Ex_1}\En\CO\St}{\Me{\Ex_2}\En\CO\St}$
 %<Meaning Function%>=
 |= Me (Pair (E1,E2)) e c s =
	Me E1 e (fn (V1,_) =>
		Me E2 e (fn (V2,S) => c (pairValue (V1,V2),s)) s
	) s
 |;

 % Get the first element from a pair.
 %<Term Definition%>=
 |:      Fst of Term
 % $\Me{{\tt fst}~\Ex}\En\Co\St=\Co\Tp{\pi_1(\Me{\Ex}\En\CO\St)}{\St}$
 %<Meaning Function%>=
 |= Me (Fst T) e c s =
	Me T e (fn 
		(pairValue (T1,T2),_) => c (T1,s)
	 |	_ => raise NotPair) s
 |;

 % Get the second element from a pair.
 %<Term Definition%>=
 |:      Snd of Term
 % $\Me{{\tt snd}~\Ex}\En\Co\St=\Co\Tp{\pi_2(\Me{\Ex}\En\CO\St)}{\St}$
 %<Meaning Function%>=
 |= Me (Snd T) e c s =
	Me T e (fn 
		(pairValue (T1,T2),_) => c (T2,s)
	 |	_ => raise NotPair) s
 |;

 %*Flow of control.

 Conditional execution.  Only one of the then or else expressions
will be executed.
 %<Term Definition%>=
 |:      Cond of Term * Term * Term
 % $\Me{{\tt if}~\Ex_1~{\tt then}~\Ex_2~{\tt else}~\Ex_3~{\tt
fi}}\En\Co\St=
(if~\Me{\Ex_1}\En\CO\St={\tt true}~then~\Me{\Ex_2}~else~\Me{\Ex_3})\En\Co\St$
 %<Meaning Function%>=
 |= Me (Cond (E1,E2,E3)) e c s =
	Me E1 e (fn (boolValue true,_) => Me E2 e c s
		|(boolValue false,_)=> Me E3 e c s
		|_ => raise NotBool
	) s
 |;

 % Expression composition.  Execute the expressions sequentially.
 %<Term Definition%>=
 |:      Seq of Term * Term
 % $\Me{\Ex_1{\tt ;}\Ex_2}\En\Co\St=\Me{\Ex_1}\En\{\Me{\Ex_2}\En\Co\}\St$
 %<Meaning Function%>=
 |= Me (Seq (E1,E2)) e c s =
	Me E1 e (fn (V,S) => Me E2 e c S) s
 |;

 % Indefinite iteration.  Execute the second expression as long as the
first expression evaluates to {\tt true}.
 %<Term Definition%>=
 |:      While of Term * Term
 % $\Me{{\tt while}~\Ex_1~{\tt do}~\Ex_2~{\tt od}}\En\Co\St=(if~
\Me{\Ex_1}\CO\St={\tt true}~then~\Me{\Ex_2}\En\{\Me{{\tt
while}\ldots}\En\Co\}~else~\Co)\St$
 %<Meaning Function%>=
 |= Me (While (E1,E2)) e c s =
	Me E1 e (fn (boolValue true,S) => Me E2 e (fn (V,S) =>
						Me (While (E1,E2)) e c S
						) S 
		|(boolValue false,S)=> c (invalidValue,S)
		|_ => raise NotBool
	) s
 |;

 %*Storage References and Updates.

 Allocate storage for a value and return the location of the value
in the store.
 %<Term Definition%>=
 |:      Ref of Term
 % $\Me{{\tt ref}~\Ex}\En\Co\St=\Co\Tp{\Lo}{\St[\Me{\Ex}\En\CO\St/\Lo]}$
 %<Meaning Function%>=
 |= Me (Ref E) e c s =
	Me E e (fn (V,_) => let
		val (nS,L) = new s V;
		in 
			c (lvalueValue L,nS)
		end
	) s
 |;

 % Given the location of a datum, get the value currently stored there.
 %<Term Definition%>=
 |:      Deref of Term
 % $\Me{{\tt .}\Ex}\En\Co\St=\Co\Tp{\St\ME{\Me{\Ex}\En\CO\St}}{\St}$
 %<Meaning Function%>=
 |= Me (Deref E) e c s = 
	Me E e (fn 
		(lvalueValue V,S) => c (access S V,s)
		|_=>raise NotLValue) s
 |;

 % Modify the storage at the location specified by the first
expression to have the value of the second expression.
 %<Term Definition%>=
 |:      Assign of Term * Term
 % $\Me{\Ex_1{\tt :=}\Ex_2}\En\Co\St=\Co\Tp{\Me{\Ex_2}\En\CO\St}{\St[\Me{\Ex_2}\En\CO\St/\Me{\Ex_1}\En\CO\St]}$
 %<Meaning Function%>=
 |=  Me (Assign (E1,E2)) e c s = 
	Me E1 e (fn 
		(lvalueValue L,_) => Me E2 e (fn (V,_) =>
					c (V,update s L V)) s
		|_=>raise NotLValue

	) s
 |;

 %*Integer Operations.

 Add two integers together.
 %<Term Definition%>=
 |:     Add of Term * Term
 % $\Me{\Ex_1{\tt +}\Ex_2}\En\Co\St=\Co\Tp{{\bf O}\ME{+}(\Me{\Ex_1}\En\CO\St,\Me{\Ex_2}\En\CO\St)}{\St}$
 %<Meaning Function%>=
 |= Me (Add (E1,E2)) e c s = 
	Me E1 e (fn (intValue V1,_) =>
		   Me E2 e (fn (intValue V2,_) => c (intValue (V1+V2),s)
				|_ => raise NotInteger) s
		|_ => raise NotInteger) s
 |;

 % Multiply two integers.
 %<Term Definition%>=
 |:     Mult of Term * Term
 % $\Me{\Ex_1{\tt *}\Ex_2}\En\Co\St=\Co\Tp{{\bf O}\ME{\times}(\Me{\Ex_1}\En\CO\St,\Me{\Ex_2}\En\CO\St)}{\St}$
 %<Meaning Function%>=
 |= Me (Mult (E1,E2)) e c s = 
	Me E1 e (fn (intValue V1,_) =>
		   Me E2 e (fn (intValue V2,_) => c (intValue (V1*V2),s)
				|_ => raise NotInteger) s
		|_ => raise NotInteger) s
 |;

 % Calculate the negative of an integer.
 %<Term Definition%>=
 |:      Neg of Term
 % $\Me{{\tt -}\Ex}\En\Co\St=\Co\Tp{-\Me{\Ex}\En\CO\St}{\St}$
 %<Meaning Function%>=
 |= Me (Neg E) e c s =
 Me E e ( fn (intValue V,_) => c (intValue (0-V),s)
		|_ => raise NotInteger) s
 |;

 %* Boolean Operations.
Determine if the first integer expression is lower in value than
the second.  Return a boolean truth value.
 %<Term Definition%>=
 |:      Less of Term * Term
 % $\Me{\Ex_1{\tt <}\Ex_2}\En\Co\St=\Co\Tp{{\bf O}\ME{<}(\Me{\Ex_1}\En\CO\St,\Me{\Ex_2}\En\CO\St)}{\St}$
 %<Meaning Function%>=
 |= Me (Less (E1,E2)) e c s = 
	Me E1 e (fn (intValue V1,_) =>
		   Me E2 e (fn (intValue V2,_) => c (boolValue (V1<V2),s)
				|_ => raise NotInteger) s
		|_ => raise NotInteger) s
 |;

 % Calculate the boolean complement of the expression.
 %<Term Definition%>=
 |:      Not of Term
 % $\Me{\neg\Ex}\En\Co\St=\Co\Tp{\neg\Me{\Ex}\En\CO\St}{\St}$
 %<Meaning Function%>=
 |= Me (Not E) e c s =
	Me E e ( fn	(boolValue true,_) => c (boolValue false,s)
		|(boolValue false,_) => c (boolValue true,s)
		|_ => raise NotBool ) s
 |;

 %*Environments.  An environment captures the bindings of names to
values (in this case locations).  This trivial implementation has
dreadful performance, but it is at least fairly obviously correct.
 %<Type Definitions%>=
abstype 'a env = Env of string->'a with
        exception unbound_variable of string;
        val newenv = Env (fn x => raise unbound_variable x);
        fun bind x t (Env f) = Env(fn y => if x=y then t else f y);
        fun lookup x (Env f) = f x
end;

 %*Stores.  A store binds locations to values.  Once again, this is
just about the most inefficient implementation you could come up with
(although there actually was a bug in the first version).  A store can
be thought of as a mapping from locations to values, where new
locations are created on demand.
 %<Type Definitions%>=
abstype 'a store = Store of int * (int->'a)
and     lvalue = lvalue of int
with
        exception segmentation_violation;
        val newstore = Store (0, fn x => raise segmentation_violation);
        fun new (Store (avail,f)) v = 
            (Store (avail+1, fn l=>if l=avail then v else f l), lvalue(avail));
        fun access (Store (_,f)) (lvalue loc) = f loc;
        fun update (Store (avail,f)) (lvalue loc) v = 
            Store (avail, fn l=>if l=loc then v else f l);
    end;

 %*Values and Miscellaneous Definitions.  Define a continuation to be
a mapping from a value,state pair to a resulting value,state.
 %<Type Definitions%>=
type 'a continuation = ('a * 'a store) -> ('a * 'a store);

 % Values.  These are the set of values that can result from a
computation.  Only the first 3 of these were in the original problem
description.  I added the others to make the language/interpreter more
useful and to catch and report errors.
 %<Type Definitions%>=
datatype Value =
   intValue of int
 | lvalueValue of lvalue
 | funcValue of Value continuation -> Value continuation
 | boolValue of bool
 | pairValue of Value*Value
 | invalidValue
 |Missing_Name of string
 ;

 % These are exceptions that are raised by the semantic function when
values are inappropriate.
 %<Type Definitions%>=
 exception NotImplemented;
 exception NotCorrect;
 exception NotPair;
 exception NotLValue;
 exception NotBool;
 exception NotInteger;
 exception NotFunc;
 exception NotFuncDecl;

 % Here is an \.{ML} version of the Y fix point operator.  We could use it
for to implement recursion.  It would only be a minor change to make
the semantic function use this rather than use \.{ML}'s builtin recursion.
 %<Functions%>=fun fix f x = f (fix f) x;
    
 % The empty continuation.
 %<Functions%>=fun nullContinuation x = x;
    
 %*Test of the Machine.  Testing is no substitute for correct
implementation, but it is somewhat heartwarming to see such an
abstract interpreter actually work.

 First of all define a |test| function that will accept any program in
the language and execute it, returning the result.
 %<Test Cases%>=
 fun test n = let
	val (V,S) =Me n newenv nullContinuation newstore handle
			unbound_variable x => (Missing_Name x,newstore);
	in V end;
 % A few dead simple tests to show that integers and pairs work
properly.
 %<Test Cases%>=
 test (Numeral 3);
 test (Neg (Add (Numeral 3,Numeral 39)));
 test (Fst (Pair (Numeral 3,Numeral 4)));
 test (Snd (Pair (Numeral 3,Numeral 4)));
 test (Seq (Numeral 3,Numeral 4));

 % Test binding names, both through value declarations and $\lambda$
bindings.  Also verify that function abstraction, function application,
and call-with-current-continuation work.
 %<Test Cases%>=
 val X="x";val Y="y";val FIX="fix" and F="f";
 test (Decl (Val_Decl (X,Numeral 29),Var X));
 test (App (Proc (X,Numeral 17),Numeral 7));
 test (App (Proc (X,Add (Var X,Numeral 1)),Numeral 7));
 test (Decl	(Val_Decl (X,Proc (Y,Var Y))
		,Add (Numeral 3,App (Var X,Numeral 55))));
 test (Decl	(Val_Decl (X,Proc (Y,
			Seq (App (Var Y,Numeral 33),Numeral 44)))
		,Add (Numeral 3,Callcc (Var X))));
 % Now for some real excitement: recursive functions.  Surprise!
Surprise! They actually work.
 %<Test Cases%>=
 val fact=Rec_Decl (X,Proc (Y,
	Cond 	(Less	(Var Y
			,Numeral 2)
		,Numeral 1
		,Mult	(App	(Var X
				,Add	(Var Y
					,Neg (Numeral 1)
					)
				)
			,Var Y
			)
		)));
 test (Decl	(fact
		,App	(Var X
			,Numeral 1)));
 test (Decl	(fact
		,App (Var X,Numeral 5)));
 % Ok, so let's use some CPU time!  Try fibonacci
 %<Test Cases%>=
 val fib=Rec_Decl (X,Proc (Y,
	Cond 	(Less	(Var Y
			,Numeral 2)
		,Numeral 1
		,Add	(App	(Var X
				,Add	(Var Y
					,Neg (Numeral 1)
					)
				)
			,App	(Var X
				,Add	(Var Y
					,Neg (Numeral 2)
					)
				)
			)
		)));
 test (Decl	(fib
		,App	(Var X
			,Numeral 1)));
 test (Decl	(fib
		,App (Var X,Numeral 5)));
 test (Decl	(fib
		,App (Var X,Numeral 10)));
 test (Decl	(fib
		,App (Var X,Numeral 15)));
 test (Decl	(fib
		,App (Var X,Numeral 20)));
 test (Decl	(fib
		,App (Var X,Numeral 25)));
 test (Decl	(fib
		,App (Var X,Numeral 28)));
 % Finally test that reference bindings and iteration work properly.
 %<Test Cases%>=
 test (Assign (Ref (Numeral 2),Numeral 3));
 test (Decl	(Var_Decl (X,Numeral 1)
		,Deref (Var X)));
 test (Decl	(Var_Decl (X,Numeral 1)
		,Seq	(Assign	(Var X
				,Add	(Numeral 22,Deref (Var X)))
			,Deref (Var X))));
 test	(Decl	(Var_Decl (X,Numeral 1)
	,(Decl	(Var_Decl (Y,Numeral 0)
		,Seq (While
			(Less (Deref (Var X),Numeral 11)
			,Seq	(Assign	(Var Y
					,Add	(Deref (Var Y),Deref (Var X)))
				,(Assign (Var X
					,Add	(Numeral 1,Deref (Var X)))))
			)
		     ,Deref (Var Y))
	 ))));

 %*Index.
---------------------------------end of denote.web-------------

.