src/HolSmt/SmtLib_Parser.sml

28      token. 4. Parsing a function symbol in some cases requires that
31      indexed identifiers, i.e., "(_ token m n ...)". 6. Parsing must
42      results from applying the (function corresponding to the) token
54      dictionary entry for a token (or every parsing function in its
58      indexed identifiers (which are instead keyed by the first token
60      catch-all entry. The token itself is passed verbatim.
76   fun t_with_args dict (token : string) (nums : Arbnum.num list)
78     Lib.tryfind (fn f => f token nums args) (Redblackmap.find (dict, token)
82     Lib.tryfind (fn f => f token nums args) (Redblackmap.find (dict, "_")
85       raise ERR "t_with_args" ("failed to parse '" ^ token ^
94       val token = get_token ()
96       if token = ")" then
99         get_tokens (token :: acc)
113     val token = get_token ()
115     if token = ")" then
120         val operand = parse_type_aux get_token tydict token []
126   and parse_compound_type get_token tydict (token : string) : Type.hol_type =
128     val headfn = parse_type_aux get_token tydict token
137     val token = get_token ()
139     if token = "_" then
143         val t = parse_compound_type get_token tydict token
152   and parse_type_aux get_token tydict (token : string)
154     if token = "(" then
157       t_with_args tydict token []
178       val token = get_token ()
180       if token = ")" then
184           val _ = Library.expect_token "(" token
202     fun parsefn var token nums args =
221       val token = get_token ()
223       if token = ")" then
227           val _ = Library.expect_token "(" token
244     fun parsefn var token nums args =
265       val token = get_token ()
267       if token = ")" then
269       else if token = "(" then
281     val token = get_token ()
283     if token = ")" then
288         val operand = parse_term_aux get_token (tydict, tmdict) token []
294   and parse_compound_term get_token (tydict, tmdict) (token : string)
297     val headfn = parse_term_aux get_token (tydict, tmdict) token
306     val token = get_token ()
308     if token = "_" then
312         val t = if token = "let" then
314           else if token = "forall" then
317           else if token = "exists" then
320           else if token = "!" then
323             parse_compound_term get_token (tydict, tmdict) token
332   and parse_term_aux get_token (tydict, tmdict) (token : string)
334     if token = "(" then
337       t_with_args tmdict token []
377     fun parsefn token nums args =
396     fun parsefn token nums args =
414     fun var_parsefn var token nums args =
428     fun parsefn token nums args =
561         WARNING "parse_file" ("ignoring token '" ^ get_token () ^