Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/branches/SMLNJ/src/eXene/demos/tactic-tree/examples/fol/fol.grm.sml
ViewVC logotype

Annotation of /sml/branches/SMLNJ/src/eXene/demos/tactic-tree/examples/fol/fol.grm.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 181 - (view) (download)

1 : monnier 180 functor folLrValsFun(structure Token : TOKEN)
2 :     =
3 :     struct
4 :     structure ParserData=
5 :     struct
6 :     structure Header =
7 :     struct
8 :    
9 :    
10 :     end
11 :     structure LrTable = Token.LrTable
12 :     structure Token = Token
13 :     local open LrTable in
14 :     val table=let val actionRows =
15 :     "\
16 :     \\001\000\001\000\008\000\002\000\007\000\017\000\006\000\000\000\
17 :     \\001\000\001\000\016\000\002\000\007\000\008\000\015\000\014\000\014\000\
18 :     \\015\000\013\000\017\000\012\000\000\000\
19 :     \\001\000\001\000\016\000\002\000\007\000\017\000\012\000\000\000\
20 :     \\001\000\001\000\032\000\000\000\
21 :     \\001\000\001\000\033\000\000\000\
22 :     \\001\000\003\000\063\000\004\000\063\000\005\000\036\000\006\000\063\000\
23 :     \\007\000\063\000\009\000\063\000\017\000\035\000\018\000\063\000\
24 :     \\020\000\063\000\021\000\063\000\022\000\063\000\023\000\063\000\000\000\
25 :     \\001\000\003\000\063\000\004\000\063\000\006\000\063\000\007\000\063\000\
26 :     \\009\000\063\000\010\000\063\000\011\000\063\000\012\000\063\000\
27 :     \\018\000\063\000\019\000\063\000\020\000\063\000\021\000\063\000\
28 :     \\022\000\063\000\023\000\063\000\026\000\063\000\000\000\
29 :     \\001\000\003\000\064\000\004\000\064\000\006\000\064\000\007\000\064\000\
30 :     \\009\000\064\000\010\000\064\000\011\000\064\000\012\000\064\000\
31 :     \\018\000\064\000\019\000\064\000\020\000\064\000\021\000\064\000\
32 :     \\022\000\064\000\023\000\064\000\026\000\064\000\000\000\
33 :     \\001\000\003\000\065\000\004\000\065\000\006\000\065\000\007\000\065\000\
34 :     \\009\000\065\000\010\000\065\000\011\000\065\000\012\000\065\000\
35 :     \\018\000\065\000\019\000\065\000\020\000\065\000\021\000\065\000\
36 :     \\022\000\065\000\023\000\065\000\026\000\065\000\000\000\
37 :     \\001\000\003\000\020\000\004\000\066\000\006\000\018\000\007\000\017\000\
38 :     \\009\000\066\000\010\000\066\000\011\000\066\000\012\000\066\000\
39 :     \\018\000\066\000\019\000\066\000\020\000\066\000\021\000\066\000\
40 :     \\022\000\066\000\023\000\066\000\026\000\066\000\000\000\
41 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
42 :     \\009\000\067\000\010\000\067\000\011\000\067\000\012\000\067\000\
43 :     \\018\000\067\000\019\000\067\000\020\000\067\000\021\000\067\000\
44 :     \\022\000\067\000\023\000\067\000\026\000\067\000\000\000\
45 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
46 :     \\009\000\068\000\010\000\068\000\011\000\068\000\012\000\068\000\
47 :     \\018\000\068\000\019\000\068\000\020\000\068\000\021\000\068\000\
48 :     \\022\000\068\000\023\000\068\000\026\000\068\000\000\000\
49 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
50 :     \\009\000\069\000\010\000\069\000\011\000\069\000\012\000\069\000\
51 :     \\018\000\069\000\019\000\069\000\020\000\069\000\021\000\069\000\
52 :     \\022\000\069\000\023\000\069\000\026\000\069\000\000\000\
53 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
54 :     \\009\000\026\000\018\000\041\000\020\000\025\000\021\000\024\000\
55 :     \\022\000\023\000\023\000\022\000\000\000\
56 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
57 :     \\009\000\026\000\020\000\025\000\021\000\024\000\022\000\023\000\
58 :     \\023\000\022\000\000\000\
59 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
60 :     \\010\000\079\000\011\000\079\000\012\000\079\000\018\000\079\000\
61 :     \\026\000\079\000\000\000\
62 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
63 :     \\010\000\080\000\011\000\080\000\012\000\080\000\018\000\080\000\
64 :     \\026\000\080\000\000\000\
65 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
66 :     \\010\000\081\000\011\000\081\000\012\000\081\000\018\000\081\000\
67 :     \\026\000\081\000\000\000\
68 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
69 :     \\010\000\082\000\011\000\082\000\012\000\082\000\018\000\082\000\
70 :     \\026\000\082\000\000\000\
71 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
72 :     \\010\000\083\000\011\000\083\000\012\000\083\000\018\000\083\000\
73 :     \\026\000\083\000\000\000\
74 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
75 :     \\018\000\070\000\019\000\058\000\000\000\
76 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
77 :     \\018\000\041\000\000\000\
78 :     \\001\000\003\000\020\000\004\000\019\000\006\000\018\000\007\000\017\000\
79 :     \\026\000\062\000\000\000\
80 :     \\001\000\010\000\072\000\011\000\072\000\012\000\027\000\018\000\072\000\
81 :     \\026\000\072\000\000\000\
82 :     \\001\000\010\000\073\000\011\000\073\000\018\000\073\000\026\000\073\000\000\000\
83 :     \\001\000\010\000\076\000\011\000\076\000\018\000\076\000\026\000\076\000\000\000\
84 :     \\001\000\010\000\084\000\011\000\084\000\012\000\084\000\018\000\084\000\
85 :     \\026\000\084\000\000\000\
86 :     \\001\000\010\000\085\000\011\000\085\000\012\000\085\000\018\000\085\000\
87 :     \\026\000\085\000\000\000\
88 :     \\001\000\010\000\086\000\011\000\086\000\012\000\086\000\018\000\086\000\
89 :     \\026\000\086\000\000\000\
90 :     \\001\000\010\000\029\000\011\000\028\000\018\000\074\000\026\000\074\000\000\000\
91 :     \\001\000\010\000\029\000\011\000\028\000\018\000\075\000\026\000\075\000\000\000\
92 :     \\001\000\010\000\029\000\011\000\028\000\018\000\077\000\026\000\077\000\000\000\
93 :     \\001\000\010\000\029\000\011\000\028\000\018\000\078\000\026\000\078\000\000\000\
94 :     \\001\000\010\000\029\000\011\000\028\000\018\000\050\000\000\000\
95 :     \\001\000\010\000\029\000\011\000\028\000\026\000\061\000\000\000\
96 :     \\001\000\013\000\051\000\000\000\
97 :     \\001\000\013\000\052\000\000\000\
98 :     \\001\000\018\000\071\000\000\000\
99 :     \\001\000\018\000\057\000\000\000\
100 :     \\001\000\024\000\004\000\025\000\003\000\000\000\
101 :     \\001\000\026\000\000\000\000\000\
102 :     \"
103 :     val actionRowNumbers =
104 :     "\039\000\000\000\001\000\022\000\
105 :     \\000\000\007\000\006\000\014\000\
106 :     \\023\000\034\000\001\000\003\000\
107 :     \\004\000\002\000\005\000\000\000\
108 :     \\000\000\000\000\000\000\021\000\
109 :     \\000\000\000\000\000\000\000\000\
110 :     \\000\000\001\000\001\000\001\000\
111 :     \\013\000\033\000\035\000\036\000\
112 :     \\024\000\000\000\028\000\012\000\
113 :     \\010\000\009\000\011\000\008\000\
114 :     \\018\000\019\000\017\000\016\000\
115 :     \\015\000\025\000\030\000\029\000\
116 :     \\027\000\001\000\001\000\038\000\
117 :     \\020\000\031\000\032\000\026\000\
118 :     \\000\000\037\000\040\000"
119 :     val gotoT =
120 :     "\
121 :     \\001\000\058\000\000\000\
122 :     \\004\000\003\000\000\000\
123 :     \\002\000\009\000\003\000\008\000\004\000\007\000\000\000\
124 :     \\000\000\
125 :     \\004\000\019\000\000\000\
126 :     \\000\000\
127 :     \\000\000\
128 :     \\000\000\
129 :     \\000\000\
130 :     \\000\000\
131 :     \\002\000\029\000\003\000\008\000\004\000\028\000\000\000\
132 :     \\000\000\
133 :     \\000\000\
134 :     \\003\000\032\000\004\000\007\000\000\000\
135 :     \\000\000\
136 :     \\004\000\035\000\000\000\
137 :     \\004\000\036\000\000\000\
138 :     \\004\000\037\000\000\000\
139 :     \\004\000\038\000\000\000\
140 :     \\000\000\
141 :     \\004\000\040\000\000\000\
142 :     \\004\000\041\000\000\000\
143 :     \\004\000\042\000\000\000\
144 :     \\004\000\043\000\000\000\
145 :     \\004\000\044\000\000\000\
146 :     \\002\000\045\000\003\000\008\000\004\000\007\000\000\000\
147 :     \\002\000\046\000\003\000\008\000\004\000\007\000\000\000\
148 :     \\002\000\047\000\003\000\008\000\004\000\007\000\000\000\
149 :     \\000\000\
150 :     \\000\000\
151 :     \\000\000\
152 :     \\000\000\
153 :     \\000\000\
154 :     \\004\000\052\000\005\000\051\000\000\000\
155 :     \\000\000\
156 :     \\000\000\
157 :     \\000\000\
158 :     \\000\000\
159 :     \\000\000\
160 :     \\000\000\
161 :     \\000\000\
162 :     \\000\000\
163 :     \\000\000\
164 :     \\000\000\
165 :     \\000\000\
166 :     \\000\000\
167 :     \\000\000\
168 :     \\000\000\
169 :     \\000\000\
170 :     \\002\000\053\000\003\000\008\000\004\000\007\000\000\000\
171 :     \\002\000\054\000\003\000\008\000\004\000\007\000\000\000\
172 :     \\000\000\
173 :     \\000\000\
174 :     \\000\000\
175 :     \\000\000\
176 :     \\000\000\
177 :     \\004\000\052\000\005\000\057\000\000\000\
178 :     \\000\000\
179 :     \\000\000\
180 :     \"
181 :     val numstates = 59
182 :     val numrules = 26
183 :     val s = ref "" and index = ref 0
184 :     val string_to_int = fn () =>
185 :     let val i = !index
186 :     in index := i+2; ordof(!s,i) + ordof(!s,i+1) * 256
187 :     end
188 :     val string_to_list = fn s' =>
189 :     let val len = String.length s'
190 :     fun f () =
191 :     if !index < len then string_to_int() :: f()
192 :     else nil
193 :     in index := 0; s := s'; f ()
194 :     end
195 :     val string_to_pairlist = fn (conv_key,conv_entry) =>
196 :     let fun f () =
197 :     case string_to_int()
198 :     of 0 => EMPTY
199 :     | n => PAIR(conv_key (n-1),conv_entry (string_to_int()),f())
200 :     in f
201 :     end
202 :     val string_to_pairlist_default = fn (conv_key,conv_entry) =>
203 :     let val conv_row = string_to_pairlist(conv_key,conv_entry)
204 :     in fn () =>
205 :     let val default = conv_entry(string_to_int())
206 :     val row = conv_row()
207 :     in (row,default)
208 :     end
209 :     end
210 :     val string_to_table = fn (convert_row,s') =>
211 :     let val len = String.length s'
212 :     fun f ()=
213 :     if !index < len then convert_row() :: f()
214 :     else nil
215 :     in (s := s'; index := 0; f ())
216 :     end
217 :     local
218 :     val memo = Array.array(numstates+numrules,ERROR)
219 :     val _ =let fun g i=(Array.update(memo,i,REDUCE(i-numstates)); g(i+1))
220 :     fun f i =
221 :     if i=numstates then g i
222 :     else (Array.update(memo,i,SHIFT (STATE i)); f (i+1))
223 :     in f 0 handle Subscript => ()
224 :     end
225 :     in
226 :     val entry_to_action = fn 0 => ACCEPT | 1 => ERROR | j => Array.sub(memo,(j-2))
227 :     end
228 :     val gotoT=Array.arrayoflist(string_to_table(string_to_pairlist(NT,STATE),gotoT))
229 :     val actionRows=string_to_table(string_to_pairlist_default(T,entry_to_action),actionRows)
230 :     val actionRowNumbers = string_to_list actionRowNumbers
231 :     val actionT = let val actionRowLookUp=
232 :     let val a=Array.arrayoflist(actionRows) in fn i=>Array.sub(a,i) end
233 :     in Array.arrayoflist(map actionRowLookUp actionRowNumbers)
234 :     end
235 :     in LrTable.mkLrTable {actions=actionT,gotos=gotoT,numRules=numrules,
236 :     numStates=numstates,initialState=STATE 0}
237 :     end
238 :     end
239 :     local open Header in
240 :     type pos = int
241 :     type arg = unit
242 :     structure MlyValue =
243 :     struct
244 :     datatype svalue = VOID | ntVOID of unit | NUM of (int)
245 :     | IDENT of (string) | TERMLIST of (Fol.term list)
246 :     | TERM of (Fol.term) | ATOMICFORM of (Fol.form)
247 :     | FORM of (Fol.form) | START of (Fol.form_or_term)
248 :     end
249 :     type svalue = MlyValue.svalue
250 :     type result = Fol.form_or_term
251 :     end
252 :     structure EC=
253 :     struct
254 :     open LrTable
255 :     val is_keyword =
256 :     fn _ => false
257 :     val preferred_insert =
258 :     fn _ => false
259 :     val preferred_subst =
260 :     fn _ => nil
261 :     val noShift =
262 :     fn (T 25) => true | _ => false
263 :     val showTerminal =
264 :     fn (T 0) => "IDENT"
265 :     | (T 1) => "NUM"
266 :     | (T 2) => "TIMES"
267 :     | (T 3) => "PLUS"
268 :     | (T 4) => "QUOTE"
269 :     | (T 5) => "MINUS"
270 :     | (T 6) => "DIVIDE"
271 :     | (T 7) => "NEG"
272 :     | (T 8) => "EQUAL"
273 :     | (T 9) => "AND"
274 :     | (T 10) => "OR"
275 :     | (T 11) => "IMPLIES"
276 :     | (T 12) => "DOT"
277 :     | (T 13) => "FORALL"
278 :     | (T 14) => "EXISTS"
279 :     | (T 15) => "COLON"
280 :     | (T 16) => "LPAREN"
281 :     | (T 17) => "RPAREN"
282 :     | (T 18) => "COMMA"
283 :     | (T 19) => "LANGLE"
284 :     | (T 20) => "RANGLE"
285 :     | (T 21) => "LEQ"
286 :     | (T 22) => "GEQ"
287 :     | (T 23) => "FORMPREFIX"
288 :     | (T 24) => "TERMPREFIX"
289 :     | (T 25) => "EOF"
290 :     | _ => "bogus-term"
291 :     val errtermvalue=
292 :     let open Header in
293 :     fn _ => MlyValue.VOID
294 :     end
295 :     val terms = (T 2) :: (T 3) :: (T 4) :: (T 5) :: (T 6) :: (T 7) :: (T 8
296 :     ) :: (T 9) :: (T 10) :: (T 11) :: (T 12) :: (T 13) :: (T 14) :: (T 15)
297 :     :: (T 16) :: (T 17) :: (T 18) :: (T 19) :: (T 20) :: (T 21) :: (T 22)
298 :     :: (T 23) :: (T 24) :: (T 25) :: nil
299 :     end
300 :     structure Actions =
301 :     struct
302 :     exception mlyAction of int
303 :     val actions =
304 :     let open Header
305 :     in
306 :     fn (i392,defaultPos,stack,
307 :     (()):arg) =>
308 :     case (i392,stack)
309 :     of (0,(_,(MlyValue.FORM FORM,_,FORM1right))::(_,(_,FORMPREFIX1left,_))
310 :     ::rest671) => let val result=MlyValue.START((Fol.Form FORM))
311 :     in (LrTable.NT 0,(result,FORMPREFIX1left,FORM1right),rest671) end
312 :     | (1,(_,(MlyValue.TERM TERM,_,TERM1right))::(_,(_,TERMPREFIX1left,_))
313 :     ::rest671) => let val result=MlyValue.START((Fol.Term TERM))
314 :     in (LrTable.NT 0,(result,TERMPREFIX1left,TERM1right),rest671) end
315 :     | (2,(_,(MlyValue.IDENT IDENT,IDENT1left,IDENT1right))::rest671) =>
316 :     let val result=MlyValue.TERM((Fol.Var IDENT))
317 :     in (LrTable.NT 3,(result,IDENT1left,IDENT1right),rest671) end
318 :     | (3,(_,(MlyValue.NUM NUM,NUM1left,NUM1right))::rest671) => let val
319 :     result=MlyValue.TERM((Fol.IntTerm NUM))
320 :     in (LrTable.NT 3,(result,NUM1left,NUM1right),rest671) end
321 :     | (4,(_,(_,_,RPAREN1right))::(_,(MlyValue.TERM TERM,_,_))::(_,(_,
322 :     LPAREN1left,_))::rest671) => let val result=MlyValue.TERM((TERM))
323 :     in (LrTable.NT 3,(result,LPAREN1left,RPAREN1right),rest671) end
324 :     | (5,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
325 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.TERM((
326 :     Fol.Fun(Fol.Constant "+",[TERM1,TERM2])))
327 :     in (LrTable.NT 3,(result,TERM1left,TERM2right),rest671) end
328 :     | (6,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
329 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.TERM((
330 :     Fol.Fun(Fol.Constant "-",[TERM1,TERM2])))
331 :     in (LrTable.NT 3,(result,TERM1left,TERM2right),rest671) end
332 :     | (7,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
333 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.TERM((
334 :     Fol.Fun(Fol.Constant "*",[TERM1,TERM2])))
335 :     in (LrTable.NT 3,(result,TERM1left,TERM2right),rest671) end
336 :     | (8,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
337 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.TERM((
338 :     Fol.Fun(Fol.Constant "/",[TERM1,TERM2])))
339 :     in (LrTable.NT 3,(result,TERM1left,TERM2right),rest671) end
340 :     | (9,(_,(MlyValue.TERM TERM,TERM1left,TERM1right))::rest671) => let
341 :     val result=MlyValue.TERMLIST(([TERM]))
342 :     in (LrTable.NT 4,(result,TERM1left,TERM1right),rest671) end
343 :     | (10,(_,(MlyValue.TERMLIST TERMLIST,_,TERMLIST1right))::_::(_,(
344 :     MlyValue.TERM TERM,TERM1left,_))::rest671) => let val result=
345 :     MlyValue.TERMLIST((TERM :: TERMLIST))
346 :     in (LrTable.NT 4,(result,TERM1left,TERMLIST1right),rest671) end
347 :     | (11,(_,(MlyValue.ATOMICFORM ATOMICFORM,ATOMICFORM1left,
348 :     ATOMICFORM1right))::rest671) => let val result=MlyValue.FORM((
349 :     ATOMICFORM))
350 :     in (LrTable.NT 1,(result,ATOMICFORM1left,ATOMICFORM1right),rest671)
351 :     end
352 :     | (12,(_,(MlyValue.ATOMICFORM ATOMICFORM,_,ATOMICFORM1right))::(_,(_,
353 :     NEG1left,_))::rest671) => let val result=MlyValue.FORM((
354 :     Fol.Conn("~",[ATOMICFORM])))
355 :     in (LrTable.NT 1,(result,NEG1left,ATOMICFORM1right),rest671) end
356 :     | (13,(_,(MlyValue.FORM FORM2,_,FORM2right))::_::(_,(MlyValue.FORM
357 :     FORM1,FORM1left,_))::rest671) => let val result=MlyValue.FORM((
358 :     Fol.Conn("&",[FORM1,FORM2])))
359 :     in (LrTable.NT 1,(result,FORM1left,FORM2right),rest671) end
360 :     | (14,(_,(MlyValue.FORM FORM2,_,FORM2right))::_::(_,(MlyValue.FORM
361 :     FORM1,FORM1left,_))::rest671) => let val result=MlyValue.FORM((
362 :     Fol.Conn("|",[FORM1,FORM2])))
363 :     in (LrTable.NT 1,(result,FORM1left,FORM2right),rest671) end
364 :     | (15,(_,(MlyValue.FORM FORM,_,FORM1right))::_::(_,(
365 :     MlyValue.ATOMICFORM ATOMICFORM,ATOMICFORM1left,_))::rest671) => let
366 :     val result=MlyValue.FORM((Fol.Conn("->",[ATOMICFORM,FORM])))
367 :     in (LrTable.NT 1,(result,ATOMICFORM1left,FORM1right),rest671) end
368 :     | (16,(_,(MlyValue.FORM FORM,_,FORM1right))::_::(_,(MlyValue.IDENT
369 :     IDENT1,_,_))::(_,(_,EXISTS1left,_))::rest671) => let val result=
370 :     MlyValue.FORM((Fol.Quant("exists",[(IDENT1,Fol.IntType)],FORM)))
371 :     in (LrTable.NT 1,(result,EXISTS1left,FORM1right),rest671) end
372 :     | (17,(_,(MlyValue.FORM FORM,_,FORM1right))::_::(_,(MlyValue.IDENT
373 :     IDENT1,_,_))::(_,(_,FORALL1left,_))::rest671) => let val result=
374 :     MlyValue.FORM((Fol.Quant("forall",[(IDENT1,Fol.IntType)],FORM)))
375 :     in (LrTable.NT 1,(result,FORALL1left,FORM1right),rest671) end
376 :     | (18,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
377 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((
378 :     Fol.Pred("=",[TERM1,TERM2]) ))
379 :     in (LrTable.NT 2,(result,TERM1left,TERM2right),rest671) end
380 :     | (19,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
381 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((
382 :     Fol.Pred("<",[TERM1,TERM2]) ))
383 :     in (LrTable.NT 2,(result,TERM1left,TERM2right),rest671) end
384 :     | (20,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
385 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((
386 :     Fol.Pred(">",[TERM1,TERM2]) ))
387 :     in (LrTable.NT 2,(result,TERM1left,TERM2right),rest671) end
388 :     | (21,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
389 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((
390 :     Fol.Pred(">=",[TERM1,TERM2]) ))
391 :     in (LrTable.NT 2,(result,TERM1left,TERM2right),rest671) end
392 :     | (22,(_,(MlyValue.TERM TERM2,_,TERM2right))::_::(_,(MlyValue.TERM
393 :     TERM1,TERM1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((
394 :     Fol.Pred("<=",[TERM1,TERM2]) ))
395 :     in (LrTable.NT 2,(result,TERM1left,TERM2right),rest671) end
396 :     | (23,(_,(_,_,RPAREN1right))::(_,(MlyValue.TERMLIST TERMLIST,_,_))::_
397 :     ::(_,(MlyValue.IDENT IDENT,IDENT1left,_))::rest671) => let val result=
398 :     MlyValue.ATOMICFORM((Fol.Pred(IDENT,TERMLIST) ))
399 :     in (LrTable.NT 2,(result,IDENT1left,RPAREN1right),rest671) end
400 :     | (24,(_,(_,_,RPAREN1right))::(_,(MlyValue.FORM FORM,_,_))::(_,(_,
401 :     LPAREN1left,_))::rest671) => let val result=MlyValue.ATOMICFORM((FORM)
402 :     )
403 :     in (LrTable.NT 2,(result,LPAREN1left,RPAREN1right),rest671) end
404 :     | (25,(_,(_,_,QUOTE1right))::(_,(MlyValue.IDENT IDENT,IDENT1left,_))::
405 :     rest671) => let val result=MlyValue.ATOMICFORM((
406 :     Fol.Pred(IDENT ^ "'",[]) ))
407 :     in (LrTable.NT 2,(result,IDENT1left,QUOTE1right),rest671) end
408 :     | _ => raise (mlyAction i392)
409 :     end
410 :     val void = MlyValue.VOID
411 :     val extract = fn a => (fn MlyValue.START x => x
412 :     | _ => let exception ParseInternal
413 :     in raise ParseInternal end) a
414 :     end
415 :     end
416 :     structure Tokens : fol_TOKENS =
417 :     struct
418 :     type svalue = ParserData.svalue
419 :     type ('a,'b) token = ('a,'b) Token.token
420 :     fun IDENT (i,p1,p2) = Token.TOKEN (ParserData.LrTable.T 0,(
421 :     ParserData.MlyValue.IDENT i,p1,p2))
422 :     fun NUM (i,p1,p2) = Token.TOKEN (ParserData.LrTable.T 1,(
423 :     ParserData.MlyValue.NUM i,p1,p2))
424 :     fun TIMES (p1,p2) = Token.TOKEN (ParserData.LrTable.T 2,(
425 :     ParserData.MlyValue.VOID,p1,p2))
426 :     fun PLUS (p1,p2) = Token.TOKEN (ParserData.LrTable.T 3,(
427 :     ParserData.MlyValue.VOID,p1,p2))
428 :     fun QUOTE (p1,p2) = Token.TOKEN (ParserData.LrTable.T 4,(
429 :     ParserData.MlyValue.VOID,p1,p2))
430 :     fun MINUS (p1,p2) = Token.TOKEN (ParserData.LrTable.T 5,(
431 :     ParserData.MlyValue.VOID,p1,p2))
432 :     fun DIVIDE (p1,p2) = Token.TOKEN (ParserData.LrTable.T 6,(
433 :     ParserData.MlyValue.VOID,p1,p2))
434 :     fun NEG (p1,p2) = Token.TOKEN (ParserData.LrTable.T 7,(
435 :     ParserData.MlyValue.VOID,p1,p2))
436 :     fun EQUAL (p1,p2) = Token.TOKEN (ParserData.LrTable.T 8,(
437 :     ParserData.MlyValue.VOID,p1,p2))
438 :     fun AND (p1,p2) = Token.TOKEN (ParserData.LrTable.T 9,(
439 :     ParserData.MlyValue.VOID,p1,p2))
440 :     fun OR (p1,p2) = Token.TOKEN (ParserData.LrTable.T 10,(
441 :     ParserData.MlyValue.VOID,p1,p2))
442 :     fun IMPLIES (p1,p2) = Token.TOKEN (ParserData.LrTable.T 11,(
443 :     ParserData.MlyValue.VOID,p1,p2))
444 :     fun DOT (p1,p2) = Token.TOKEN (ParserData.LrTable.T 12,(
445 :     ParserData.MlyValue.VOID,p1,p2))
446 :     fun FORALL (p1,p2) = Token.TOKEN (ParserData.LrTable.T 13,(
447 :     ParserData.MlyValue.VOID,p1,p2))
448 :     fun EXISTS (p1,p2) = Token.TOKEN (ParserData.LrTable.T 14,(
449 :     ParserData.MlyValue.VOID,p1,p2))
450 :     fun COLON (p1,p2) = Token.TOKEN (ParserData.LrTable.T 15,(
451 :     ParserData.MlyValue.VOID,p1,p2))
452 :     fun LPAREN (p1,p2) = Token.TOKEN (ParserData.LrTable.T 16,(
453 :     ParserData.MlyValue.VOID,p1,p2))
454 :     fun RPAREN (p1,p2) = Token.TOKEN (ParserData.LrTable.T 17,(
455 :     ParserData.MlyValue.VOID,p1,p2))
456 :     fun COMMA (p1,p2) = Token.TOKEN (ParserData.LrTable.T 18,(
457 :     ParserData.MlyValue.VOID,p1,p2))
458 :     fun LANGLE (p1,p2) = Token.TOKEN (ParserData.LrTable.T 19,(
459 :     ParserData.MlyValue.VOID,p1,p2))
460 :     fun RANGLE (p1,p2) = Token.TOKEN (ParserData.LrTable.T 20,(
461 :     ParserData.MlyValue.VOID,p1,p2))
462 :     fun LEQ (p1,p2) = Token.TOKEN (ParserData.LrTable.T 21,(
463 :     ParserData.MlyValue.VOID,p1,p2))
464 :     fun GEQ (p1,p2) = Token.TOKEN (ParserData.LrTable.T 22,(
465 :     ParserData.MlyValue.VOID,p1,p2))
466 :     fun FORMPREFIX (p1,p2) = Token.TOKEN (ParserData.LrTable.T 23,(
467 :     ParserData.MlyValue.VOID,p1,p2))
468 :     fun TERMPREFIX (p1,p2) = Token.TOKEN (ParserData.LrTable.T 24,(
469 :     ParserData.MlyValue.VOID,p1,p2))
470 :     fun EOF (p1,p2) = Token.TOKEN (ParserData.LrTable.T 25,(
471 :     ParserData.MlyValue.VOID,p1,p2))
472 :     end
473 :     end

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0