Structure type_grammar

signature type_grammar =
sig

  type kernelname = KernelSig.kernelname

  datatype grammar_rule =
           INFIX of {opname : string, parse_string : string} list *
                    HOLgrammars.associativity

  datatype type_structure
    = TYOP of {Thy : string, Tyop : string, Args : type_structure list}
    | PARAM of int

  type grammar

  val structure_to_type : type_structure -> Type.hol_type

  val empty_grammar    : grammar
  val min_grammar      : grammar
  val rules            : grammar -> {infixes: (int * grammar_rule) list,
                                     suffixes : string list}
  val abbreviations    : grammar -> (kernelname,type_structure) Binarymap.dict
  val privileged_abbrevs : grammar -> (string,string) Binarymap.dict

  val abb_dest_type : grammar -> Type.hol_type ->
                      {Thy : string option, Tyop : string,
                       Args : Type.hol_type list}
  val disable_abbrev_printing : string -> grammar -> grammar

  val new_binary_tyop  : grammar
                          -> {precedence : int,
                              infix_form : string option,
                              opname : string,
                              associativity : HOLgrammars.associativity}
                          -> grammar

  val remove_binary_tyop : grammar -> string -> grammar
  (* removes by infix symbol, i.e. "+", not "sum" *)

  val new_tyop         : grammar -> string -> grammar
  val new_abbreviation : grammar -> kernelname * type_structure -> grammar
  val remove_abbreviation : grammar -> string -> grammar
  val num_params : type_structure -> int

  val merge_grammars   : grammar * grammar -> grammar

  val prettyprint_grammar   : Portable.ppstream -> grammar -> unit
  val initialise_typrinter
    : (grammar -> Portable.ppstream -> Type.hol_type -> unit) -> unit

end

HOL 4, Kananaskis-11