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