diff options
Diffstat (limited to 'web/spiderweb/src/larch/l.spider')
-rw-r--r-- | web/spiderweb/src/larch/l.spider | 245 |
1 files changed, 245 insertions, 0 deletions
diff --git a/web/spiderweb/src/larch/l.spider b/web/spiderweb/src/larch/l.spider new file mode 100644 index 0000000000..3a275f2711 --- /dev/null +++ b/web/spiderweb/src/larch/l.spider @@ -0,0 +1,245 @@ +# 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 Larch extension larch + +comment begin <"%"> end newline +line begin <"%line"> + +at_sign @ + +default mathness yes + +ilk all_like category all +ilk by_like category by +ilk constrains_like category constrains +ilk converts_like category gclause +ilk div_like category binop +ilk fi_like category fi +ilk for_like category for +ilk gen_like category gen +ilk if_like category if +ilk implies_like translation <*-indent> +ilk imports_like category imports +ilk intro_like category intro translation <*-indent> +ilk is_like category is +ilk then_like category then +ilk trait_like category trait +ilk with_like category with + +reserved all +reserved assumes ilk imports_like +reserved by +reserved constrains +reserved converts ilk converts_like +reserved div ilk div_like +reserved else ilk then_like +reserved exempts +reserved fi +reserved for +reserved generated ilk gen_like +reserved if +reserved implies +reserved imports +reserved includes ilk imports_like +reserved introduces ilk intro_like +reserved is +reserved mod ilk div_like +reserved partitioned ilk gen_like +reserved rem ilk div_like +reserved so +reserved that +reserved then +reserved trait +reserved with + +ilk and_like category binop translation <"\\wedge"> mathness yes +ilk or_like category binop translation <"\\vee"> mathness yes +ilk not_like category unop translation <"\\neg"> mathness yes + +reserved and +reserved or +reserved not + +ilk forall_like category unop translation <"\\forall"> mathness yes +reserved forall + + +simp colon trait <indent> --> tbegin +tbegin ? <outdent-force> tbegin --> tbegin +tbegin <force> decl --> tbegin + +[ intro <outdent-force> ] constrains --> decl constrains +intro <force> decl --> intro +math colon --> mcolon +mcolon (simp|comma) --> mcolon +mcolon arrow simp --> decl + +imports simp with open --> sublist + +# following special for David +imports simp open --> imbrace +imbrace (math|comma) --> imbrace +imbrace close with open --> sublist +imbrace close --> decl +# end David + +imports simp --> decl + +sublist for --> subfor +sublist ? --> sublist +subfor comma --> sublist +subfor close --> decl +subfor ? --> subfor + + +constrains open --> conslist +conslist math comma <opt-5> --> conslist +conslist math close so that <indent> --> consintro + +consintro <force> decl --> consintro +[ consintro ] (implies|tbegin) --> decl (implies|tbegin) + +simp is gen by --> gclause +gclause open --> glist +glist math comma --> glist +glist math close comma <opt-5> --> gclause +# do the following because converts is also a gclause +glist math close <indent-force> exempts --> exemptions +glist math close --> decl + +exemptions math comma <opt-7> --> exemptions +exemptions math <outdent> --> decl + +for all open --> forlist +forlist (simp|comma|colon) --> forlist +forlist semi <opt-3> --> forlist +forlist close <indent> --> forintro + +[ forintro <outdent-force> ] (implies|tbegin|gclause) --> decl (implies|tbegin|gclause) +[ forintro <outdent> ] simp is gen by --> decl simp is gen by +forintro <force> (relation|decl) --> forintro +forintro <outdent-force> forintro --> forintro + +consintro <force> forintro --> consfor +consfor <outdent-force> forintro --> consfor + +[ consfor <outdent-outdent-force> ] (implies|tbegin|gclause) --> decl (implies|tbegin|gclause) +[ consfor <outdent> ] simp is gen by --> consintro simp is gen by +consfor <force> (relation|decl) --> consfor + +implies <force> (decl|relation) --> implies +[ implies ] tbegin --> decl tbegin + +math rel --> mathrel +mathrel math (binop|rel) --> mathrel +mathrel [ math open ] --> mathrel open +[ mathrel open math close ] open --> relation open +mathrel math --> relation +math open --> open +math binop math --> math +unop math --> math +open math comma --> open +open math close --> math +open [ relation ] --> open math +open [ math <"\\&{WEAVE\\_ERROR!}"> math ] --> open math +[ math ] math --> relation math + +if (math|relation) then --> if +if (math|relation) fi --> math + + +decl <force> (decl|relation) --> decl +relation <force> relation --> relation +relation <force> decl --> decl + +module definition decl use math + +token identifier category simp mathness yes +token number category math mathness yes +token newline category ignore_scrap mathness maybe translation <> +token pseudo_semi category ignore_scrap mathness maybe translation <> + +default mathness yes translation <*> + +# use backslash for subscripts +token \ category backslash translation <"_"> tangleto <"_"> mathness yes +math backslash <"{"> math <"}"> --> math + +token + category binop +token - category binop +token * category binop +token / category binop +token ** category binop translation <"\\mathbin{{*}{*}}"> +token . category binop + +token & category binop translation <"\\wedge"> +token | category binop translation <"\\vee"> +token ~ category unop translation <"\\neg"> + +token < category rel +token > category rel +token = category rel +token != translation <"\\I"> category rel +token <= translation <"\\L"> category rel +token >= translation <"\\G"> category rel +token => translation <"\\Rightarrow"> category rel + +token # translation <"\\#"> category simp +token ( category open +token [ category open +token [[ category open translation <"\\dsl"> +token {[ category open translation <"\\dcl"> +token { category open translation <"\\{"> +token << category open translation <"\\LN"> +token ) category close +token ] category close +token ]] category close translation <"\\dsr"> +token ]} category close translation <"\\dcr"> +token } category close translation <"\\}"> +token >> category close translation <"\\RN"> + +macros begin +\let\LN\langle +\let\RN\rangle +\def\dsl{[\![} +\def\dsr{]\!]} +\def\dcl{\{\![} +\def\dcr{]\!\}} +macros end + +token , category comma mathness yes translation <",\\,"> +token ; category semi +token : category colon +token -> translation <"\\MG"> category arrow +macros begin +\let\MG\rightarrow +macros end + + +### Hacks for David: is, when +default mathness yes +token <- category binop translation <"\\leftarrow"> +token .. category binop translation <".."> +token ... category ignore_scrap translation <"\\ldots"> +token /= translation <"\\I"> category rel +token ^ category hat translation <> mathness maybe +token :: category binop translation <":"> mathness maybe + +hat <"\\"-space> (simp|is) <"\\"-space> hat --> binop +simp <"\\"-space> hat hat --> unop + +open close --> math + +########################## +# the following must be last + +simp --> math + +# if semi is not in a for list, treat it as a binary operator +semi --> binop + + + +? ignore_scrap --> #1 + |