1signature type_grammar =
2sig
3
4  type kernelname = KernelSig.kernelname
5
6  datatype grammar_rule = datatype type_grammar_dtype.grammar_rule
7  datatype type_structure = datatype type_grammar_dtype.type_structure
8  datatype delta = datatype type_grammar_dtype.delta
9
10  type grammar
11
12  val structure_to_type : type_structure -> Type.hol_type
13
14  val empty_grammar    : grammar
15  val min_grammar      : grammar
16  val rules            : grammar -> {infixes: (int * grammar_rule) list,
17                                     suffixes : string list}
18  val parse_map    : grammar -> (kernelname,type_structure) Binarymap.dict
19  val print_map    : grammar -> (int * kernelname) TypeNet.typenet
20  val privileged_abbrevs : grammar -> (string,string) Binarymap.dict
21
22  val abb_dest_type : grammar -> Type.hol_type ->
23                      {Thy : string option, Tyop : string,
24                       Args : Type.hol_type list}
25  val disable_abbrev_printing : string -> grammar -> grammar
26
27  val new_binary_tyop  : grammar
28                          -> {precedence : int,
29                              infix_form : string,
30                              opname : string,
31                              associativity : HOLgrammars.associativity}
32                          -> grammar
33
34  val remove_binary_tyop : grammar -> string -> grammar
35  (* removes by infix symbol, i.e. "+", not "sum" *)
36
37  val new_qtyop        : kernelname -> grammar -> grammar
38  val hide_tyop        : string -> grammar -> grammar
39  val new_abbreviation : grammar -> kernelname * Type.hol_type -> grammar
40  val remove_abbreviation : grammar -> string -> grammar
41  val num_params : type_structure -> int
42
43  val merge_grammars   : grammar * grammar -> grammar
44
45  val apply_delta : delta -> grammar -> grammar
46  val apply_deltas : delta list -> grammar -> grammar
47
48  val prettyprint_grammar   : grammar -> HOLPP.pretty
49  val initialise_typrinter
50    : (grammar -> Type.hol_type -> HOLPP.pretty) -> unit
51
52end
53