----------------------------------------------------------------------
Absyn                                                          (Parse)
----------------------------------------------------------------------
Absyn : term quotation -> Absyn.absyn

SYNOPSIS
Implements the first phase of term parsing; the removal of special syntax.

KEYWORDS
Parsing

LIBRARY
Parse

DESCRIBE
{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
Parse.Term, Parse.term_grammar.

----------------------------------------------------------------------