blob: 3a275f2711741a39f45ec81814695bee279ec767 (
plain)
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
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
|