Searched refs:get_token (Results 1 - 4 of 4) sorted by path

/seL4-l4v-master/HOL4/src/HolSmt/
H A DLibrary.sml68 fun get_token (get_char : unit -> char) : unit -> string = function
108 raise Feedback.mk_HOL_ERR "Library" "get_token" "invalid '|'"
112 raise Feedback.mk_HOL_ERR "Library" "get_token" "invalid '\"'"
H A DSmtLib_Parser.sml89 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 tydic
558 val get_token = Library.get_token (Library.get_buffered_char instream) value
[all...]
H A DZ3_ProofParser.sml319 fun parse_definition get_token (tydict, tmdict, proof) =
321 val _ = Library.expect_token "(" (get_token ())
322 val _ = Library.expect_token "(" (get_token ())
323 val name = get_token ()
324 val t = SmtLib_Parser.parse_term get_token (tydict, tmdict)
325 val _ = Library.expect_token ")" (get_token ())
326 val _ = Library.expect_token ")" (get_token ())
344 fun parse_proof get_token (tydict, tmdict, proof) (rpars : int) =
346 val _ = Library.expect_token "(" (get_token ())
347 val head = get_token ()
392 val get_token = Library.get_token (Library.get_buffered_char instream) value
[all...]
/seL4-l4v-master/graph-refine/
H A Dsolver.py442 return solv.get_token (expr.name)
1803 def get_token (self, string): member in class:Solver

Completed in 63 milliseconds