1\DOC parse_from_grammars
2
3\BLTYPE
4parse_from_grammars :
5  (type_grammar.grammar * term_grammar.grammar) ->
6  ((hol_type frag list -> hol_type) * (term frag list -> term))
7\ELTYPE
8
9\SYNOPSIS
10Returns parsing functions based on the supplied grammars.
11
12\KEYWORDS
13parsing
14
15\DESCRIBE
16When given a pair consisting of a type and a term grammar, this
17function returns parsing functions that use those grammars to turn
18strings (strictly, quotations) into types and terms respectively.
19
20\FAILURE
21Can't fail immediately.  However, when the precedence matrix for the
22term parser is built on first application of the term parser, this may
23generate precedence conflict errors depending on the rules in the
24grammar.
25
26\EXAMPLE
27First the user loads {arithmeticTheory} to augment the built-in
28grammar with the ability to lex numerals and deal with symbols such as
29{+} and {-}:
30{
31   - load "arithmeticTheory";
32   > val it = () : unit
33   - val t = Term`2 + 3`;
34   > val t = `2 + 3` : term
35}
36Then the {parse_from_grammars} function is used to make the
37values {Type} and {Term} use the grammar present in the simpler theory
38of booleans.  Using this function fails to parse numerals or even the
39{+} infix:
40{
41   - val (Type,Term) = parse_from_grammars boolTheory.bool_grammars;
42   > val Type = fn : hol_type frag list -> hol_type
43     val Term = fn : term frag list -> term
44   - Term`2 + 3`;
45   <<HOL message: No numerals currently allowed.>>
46   ! Uncaught exception:
47   ! HOL_ERR <poly>
48   - Term`x + y`;
49   <<HOL message: inventing new type variable names: 'a, 'b.>>
50   > val it = `x $+ y` : term
51}
52But, as the last example above also demonstrates, the installed
53pretty-printer is still dependent on the global grammar, and the
54global value of {Term} can still be accessed through the {Parse}
55structure:
56{
57   - t;
58   > val it = `2 + 3` : term
59
60   - Parse.Term`2 + 3`;
61   > val it = `2 + 3` : term
62}
63
64
65\USES
66This function is used to ensure that library code has access to a term
67parser that is a known quantity.  In particular, it is not good form
68to have library code that depends on the default parsers {Term} and
69{Type}.  When the library is loaded, which may happen at any stage,
70these global values may be such that the parsing causes quite
71unexpected results or failures.
72
73\SEEALSO
74Parse.add_rule, Parse.print_from_grammars, Parse.Term.
75\ENDDOC
76