From dmason@plg.uwaterloo.ca Wed Aug 5 17:08:26 1992 Received: from Princeton.EDU by fs.Princeton.EDU (4.1/1.105) id AA10701; Wed, 5 Aug 92 17:08:21 EDT Received: from plg.uwaterloo.ca by Princeton.EDU (5.65b/2.93/princeton) id AA23362; Wed, 5 Aug 92 17:07:44 -0400 Received: by plg.uwaterloo.ca id <29115>; Wed, 5 Aug 1992 17:07:32 -0400 From: Dave Mason To: Norman Ramsey Subject: spiderweb Message-Id: <92Aug5.170732edt.29115@plg.uwaterloo.ca> Date: Wed, 5 Aug 1992 17:07:26 -0400 Status: R 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)) @@; /*spider*/ ! else if (isalpha(c) || (c=='_' && (*loc=='_' || isalpha(*loc)))) @@;/*spider*/ else if (c=='\'' || c=='"') @@;/*spider*/ else if (c==at_sign) @@; else if (c==' ' || c==tab_mark) continue; /* ignore spaces and tabs */ --- 543,549 ---- } } if (isdigit(c)) @@; /*spider*/ ! else if (isalpha(c) || c=='_') @@;/*spider*/ else if (c=='\'' || c=='"') @@;/*spider*/ else if (c==at_sign) @@; else if (c==' ' || c==tab_mark) continue; /* ignore spaces and tabs */ *************** *** 557,563 **** @ @= {/*spider*/ id_first=--loc; ! while (isalpha(*++loc) || isdigit(*loc) || *loc=='_' || *loc=='\''); id_loc=loc; return(identifier); } --- 557,563 ---- @ @= {/*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 translation <"\\SL{"> mathness maybe token .] category close tangleto <")"> translation <"}"> mathness maybe token [= category open tangleto 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 translation <"\\'{"> mathness maybe token '' category tick tangleto 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 mathness yes translation <"\\wedge"> token || category binop tangleto 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 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 dec end --> sig_body signature <"\\"-space> id* equal sig_body --> dec functor [ <"\\"-space> id* ] --> functor funhead functor funhead pat equal struct_object --> dec struct dec 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 ] (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 multimath ] (semi|val|fun|type|let|struct|openop|and|end|close|in) --> val valbody (semi|val|fun|type|let|struct|openop|and|end|close|in) val valbody and --> val val valbody --> dec datatop <"\\"-space-indent> codeuse --> datahead datatop <"\\"-space> ty* <"\\"-space-indent> equal --> 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* choice ] id of --> datam id of datam <"\\"-space> id* 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 choice --> datam [ (datat|datam) <"\\"-space> id ] (semi|val|fun|type|datatype|let|struct|openop|end|in) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in) [ datahead ] (semi|val|fun|type|datatype|let|struct|openop|end|in) --> dec (semi|val|fun|type|datatype|let|struct|openop|end|in) datat <"\\"-space> id (and|withtype) --> datatop datahead (and|withtype) --> datatop datatype --> datatop abstype --> datatop datahead with dec 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) [ let ] --> (equal|arrow) letf !(ignore_scrap|equal|arrow) [ let ] --> !(ignore_scrap|equal|arrow) letf letf dec in (math|multimath) end --> multimath local dec in dec end --> dec dec semi --> dec [ (math|multimath) semi ] dec --> dec dec [ (math|multimath) ] dec --> dec dec dec [ (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 dec ] !(semi|ignore_scrap) --> dec !(semi|ignore_scrap) [ case <"\\"-space> (math|multimath) of multimatch ] (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) [ fn (multimatch|match) ] (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) handle (multimatch|match) ] (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 math ] (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 multimath ] (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) 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 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 and --> fun fun [ funhead <"\\"-space> pat <"\\"-space> equal math ] !(binop|handle|math|id|open|multimath|ignore_scrap) --> fun funbody !(binop|handle|math|id|open|multimath|ignore_scrap) fun [ funhead <"\\"-space> pat <"\\"-space> equal multimath ] !(binop|handle|math|id|open|multimath|ignore_scrap) --> fun funbody !(binop|handle|math|id|open|multimath|ignore_scrap) equal [ multimath ] --> equal math [ if <"\\"-space> (math|multimath) <"\\"-space> then (math|multimath) else (math|multimath) ] (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 <"\\"-space> (math|multimath) ] (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) comma (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 math close ] !(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 math 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) 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 multimath close ] --> (then|semi|else|in|equal|arrow) multimath !(then|semi|else|in|equal|arrow) [ open multimath close ] --> !(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 }} } \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 % % %; % % 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. %= datatype Decl = Var_Decl of string * Term | Val_Decl of string * Term | Rec_Decl of string * Term and %; %*|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 = Var of string % $\Me{\Sy}\En\Co\St=\Co\Tp{\En\ME{\Sy}}{\St}$ %= fun Me (Var x) e c s = c (lookup x e ,s) |; % Integer constants. %= |: Numeral of int % $\Me{\Nu}\En\Co\St=\Co\Tp{{\bf V}\ME{\Nu}}{\St}$ %= |= 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. %= |: 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]$ %= |= 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$ %= |= 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. %= |= 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. %= |: 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}$ %= |= 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. %= |: 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. %= |= 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. %= |: 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. %= |= 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. %= |: 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}$ %= |= 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. %= |: Fst of Term % $\Me{{\tt fst}~\Ex}\En\Co\St=\Co\Tp{\pi_1(\Me{\Ex}\En\CO\St)}{\St}$ %= |= 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. %= |: Snd of Term % $\Me{{\tt snd}~\Ex}\En\Co\St=\Co\Tp{\pi_2(\Me{\Ex}\En\CO\St)}{\St}$ %= |= 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. %= |: 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$ %= |= 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. %= |: Seq of Term * Term % $\Me{\Ex_1{\tt ;}\Ex_2}\En\Co\St=\Me{\Ex_1}\En\{\Me{\Ex_2}\En\Co\}\St$ %= |= 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}. %= |: 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$ %= |= 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. %= |: Ref of Term % $\Me{{\tt ref}~\Ex}\En\Co\St=\Co\Tp{\Lo}{\St[\Me{\Ex}\En\CO\St/\Lo]}$ %= |= 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. %= |: Deref of Term % $\Me{{\tt .}\Ex}\En\Co\St=\Co\Tp{\St\ME{\Me{\Ex}\En\CO\St}}{\St}$ %= |= 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. %= |: 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]}$ %= |= 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. %= |: 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}$ %= |= 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. %= |: 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}$ %= |= 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. %= |: Neg of Term % $\Me{{\tt -}\Ex}\En\Co\St=\Co\Tp{-\Me{\Ex}\En\CO\St}{\St}$ %= |= 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. %= |: 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}$ %= |= Me (Less (E1,E2)) e c s = Me E1 e (fn (intValue V1,_) => Me E2 e (fn (intValue V2,_) => c (boolValue (V1 raise NotInteger) s |_ => raise NotInteger) s |; % Calculate the boolean complement of the expression. %= |: Not of Term % $\Me{\neg\Ex}\En\Co\St=\Co\Tp{\neg\Me{\Ex}\En\CO\St}{\St}$ %= |= 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. %= 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. %= 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 '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. %= 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. %= 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. %=fun fix f x = f (fix f) x; % The empty continuation. %=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. %= 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 (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. %= 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. %= 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 %= 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 (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-------------