Lines Matching refs:get_token
89 fun parse_indexed_t get_token dict : 'a list -> 'a =
94 val token = get_token ()
111 fun parse_type_operands get_token tydict acc : Type.hol_type list =
113 val token = get_token ()
120 val operand = parse_type_aux get_token tydict token []
122 parse_type_operands get_token tydict (operand :: acc)
126 and parse_compound_type get_token tydict (token : string) : Type.hol_type =
128 val headfn = parse_type_aux get_token tydict token
129 val operands = parse_type_operands get_token tydict []
134 and parse_indexed_or_compound_type get_token tydict
137 val token = get_token ()
140 parse_indexed_t get_token tydict
143 val t = parse_compound_type get_token tydict token
152 and parse_type_aux get_token tydict (token : string)
155 parse_indexed_or_compound_type get_token tydict
159 fun parse_type get_token tydict : Type.hol_type =
160 parse_type_aux get_token tydict (get_token ()) []
162 fun parse_type_list get_token tydict : Type.hol_type list =
164 Library.expect_token "(" (get_token ());
165 parse_type_operands get_token tydict []
172 fun parse_var_bindings get_token (tydict, tmdict)
175 val _ = Library.expect_token "(" (get_token ())
178 val token = get_token ()
185 val symbol = get_token ()
186 val term = parse_term get_token (tydict, tmdict)
187 val _ = Library.expect_token ")" (get_token ())
196 and parse_let_term get_token (tydict, tmdict) : Term.term =
198 val bindings = parse_var_bindings get_token (tydict, tmdict)
210 val body = parse_term get_token (tydict, tmdict)
211 val _ = Library.expect_token ")" (get_token ())
216 and parse_sorted_vars get_token tydict : (string * Type.hol_type) list =
218 val _ = Library.expect_token "(" (get_token ())
221 val token = get_token ()
228 val symbol = get_token ()
229 val typ = parse_type get_token tydict
230 val _ = Library.expect_token ")" (get_token ())
239 and parse_binder_term get_token (tydict, tmdict) mk_binder : Term.term =
241 val vars = parse_sorted_vars get_token tydict
252 val body = parse_term get_token (tydict, tmdict)
253 val _ = Library.expect_token ")" (get_token ())
258 and parse_annotated_term get_token (tydict, tmdict) : Term.term =
260 val term = parse_term get_token (tydict, tmdict)
265 val token = get_token ()
279 and parse_term_operands get_token (tydict, tmdict) acc : Term.term list =
281 val token = get_token ()
288 val operand = parse_term_aux get_token (tydict, tmdict) token []
290 parse_term_operands get_token (tydict, tmdict) (operand :: acc)
294 and parse_compound_term get_token (tydict, tmdict) (token : string)
297 val headfn = parse_term_aux get_token (tydict, tmdict) token
298 val operands = parse_term_operands get_token (tydict, tmdict) []
303 and parse_indexed_or_compound_term get_token (tydict, tmdict)
306 val token = get_token ()
309 parse_indexed_t get_token tmdict
313 parse_let_term get_token (tydict, tmdict)
315 parse_binder_term get_token (tydict, tmdict)
318 parse_binder_term get_token (tydict, tmdict)
321 parse_annotated_term get_token (tydict, tmdict)
323 parse_compound_term get_token (tydict, tmdict) token
332 and parse_term_aux get_token (tydict, tmdict) (token : string)
335 parse_indexed_or_compound_term get_token (tydict, tmdict)
339 and parse_term get_token (tydict, tmdict) : Term.term =
340 parse_term_aux get_token (tydict, tmdict) (get_token ()) []
342 fun parse_term_list get_token (tydict, tmdict) : Term.term list =
344 Library.expect_token "(" (get_token ());
345 parse_term_operands get_token (tydict, tmdict) []
353 fun parse_set_info get_token =
354 if get_token () = ")" then
357 parse_set_info get_token
360 fun parse_set_logic get_token =
362 val logic = get_token ()
364 val _ = Library.expect_token ")" (get_token ())
371 fun parse_declare_sort get_token tydict =
373 val name = get_token ()
374 val _ = Library.expect_token "0" (get_token ())
375 val _ = Library.expect_token ")" (get_token ())
387 fun parse_declare_fun get_token (tydict, tmdict) =
389 val name = get_token ()
390 val domain_types = parse_type_list get_token tydict
391 val range_type = parse_type get_token tydict
392 val _ = Library.expect_token ")" (get_token ())
406 fun parse_define_fun get_token (tydict, tmdict) =
408 val name = get_token ()
409 val vars = parse_sorted_vars get_token tydict
411 val range_type = parse_type get_token tydict
422 val definiens = parse_term get_token (tydict, definiens_tmdict)
423 val _ = Library.expect_token ")" (get_token ())
444 fun parse_commands get_token state =
450 val _ = Library.expect_token "(" (get_token ())
451 val command = get_token ()
455 val _ = parse_set_info get_token
457 parse_commands get_token state
463 val (logic, tydict, tmdict) = parse_set_logic get_token
465 parse_commands get_token (SOME (logic, tydict, tmdict, []))
470 val tydict = parse_declare_sort get_token tydict
472 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
477 val tmdict = parse_declare_fun get_token (tydict, tmdict)
479 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
484 val (tmdict, def) = parse_define_fun get_token (tydict, tmdict)
487 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
492 val asserted = parse_term get_token (tydict, tmdict) :: asserted
493 val _ = Library.expect_token ")" (get_token ())
495 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
500 val _ = Library.expect_token ")" (get_token ())
502 parse_commands get_token state
507 val _ = Library.expect_token ")" (get_token ())
509 parse_commands get_token state
514 val _ = Library.expect_token ")" (get_token ())
523 fun parse_benchmark get_token =
524 parse_commands get_token NONE
558 val get_token = Library.get_token (Library.get_buffered_char instream)
559 val result = parse_benchmark get_token
561 WARNING "parse_file" ("ignoring token '" ^ get_token () ^