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 : {knm : kernelname, ty : Type.hol_type, print : bool} -> 40 grammar -> grammar 41 val remove_abbreviation : grammar -> string -> grammar 42 val num_params : type_structure -> int 43 44 val merge_grammars : grammar * grammar -> grammar 45 46 val apply_delta : delta -> grammar -> grammar 47 val apply_deltas : delta list -> grammar -> grammar 48 val delta_toString : delta -> string 49 50 val prettyprint_grammar : grammar -> HOLPP.pretty 51 val initialise_typrinter 52 : (grammar -> Type.hol_type -> HOLPP.pretty) -> unit 53 54end 55