Parse.Term

The parsing process for terms divides into four distinct phases.

The first phase converts the quotation argument into abstract syntax, a relatively simple parse tree datatype, with the following datatype definition (from Absyn):

   datatype vstruct
       = VAQ    of term
       | VIDENT of string
       | VPAIR  of vstruct * vstruct
       | VTYPED of vstruct * pretype
   datatype absyn
       = AQ    of term
       | IDENT of string
       | APP   of absyn * absyn
       | LAM   of vstruct * absyn
       | TYPED of absyn * pretype

This phase of parsing is concerned with the treatment of the rawest concrete syntax. It has no notion of whether or not a term corresponds to a constant or a variable, so all preterm leaves are ultimately either IDENTs or AQs (anti-quotations).

This first phase converts infixes, mixfixes and all the other categories of syntactic rule from the global grammar into simple structures built up using APP. For example, `x op y` (where op is an infix) will turn into

   APP(APP(IDENT "op", IDENT "x"), IDENT "y")

and `tok1 x tok2 y` (where tok1 _ tok2 has been declared as a Prefix form for the term f) will turn into

   APP(APP(IDENT "f", IDENT "x"), IDENT "y")

The special syntaxes for “let” and record expressions are also handled at this stage. For more details on how this is done see the reference entry for Absyn, which function can be used in isolation to see what is done at this phase.

The second phase of parsing consists of the resolution of names, identifying what were just VARs as constants or genuine variables (whether free or bound). This phase also annotates all leaves of the data structure (given in the entry for Preterm) with type information.

The third phase of parsing works over the Preterm datatype and does type-checking, though ignoring overloaded values. The datatype being operated over uses reference variables to allow for efficiency, and the type-checking is done “in place”. If type-checking is successful, the resulting value has consistent type annotations.

The final phase of parsing resolves overloaded constants. The type-checking done to this point may completely determine which choice of overloaded constant is appropriate, but if not, the choice may still be completely determined by the interaction of the possible types for the overloaded possibilities.

Finally, depending on the value of the global flags guessing_tyvars and guessing_overloads, the parser will make choices about how to resolve any remaining ambiguities.

The parsing process is entirely driven by the global grammar. This value can be inspected with the term_grammar function.