Absyn : term quotation -> Absyn.absyn
STRUCTURE
Parse
SYNOPSIS
Implements the first phase of term parsing; the removal of special syntax.
LIBRARY
Parse
DESCRIPTION
Absyn takes a quotation and parses it into an abstract syntax tree of type absyn, using the current term and type grammars. This phase of parsing is unconcerned with types, and will happily parse meaningless expressions that are syntactically valid.
EXAMPLE
Absyn will parse the expression `let x = e1 in e2` into 
   APP(APP(IDENT "LET", LAM(VIDENT "x", IDENT "e2")), IDENT "e1")
The record syntax `rec.fld1` is converted into something of the form 
   APP(IDENT "....fld1", IDENT "rec")
where the dots will actually be equal to the value of GrammarSpecials.recsel_special (a string).
FAILURE
Fails if the quotation has a syntax error.
USES
Absyn is not often used, but may be handy for implementing some weird and wonderful concrete syntax that surpasses the functionality of the HOL parser.
SEEALSO
Term, term_grammar
HOL  Kananaskis-14