Absyn : term quotation -> Absyn.absyn
STRUCTURE
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
HOL  Kananaskis-10