Structure term_grammar
signature term_grammar =
sig
type block_info = term_grammar_dtype.block_info
type overload_info = Overload.overload_info
type associativity = term_grammar_dtype.associativity
type grule = term_grammar_dtype.grule
datatype rule_element = datatype term_grammar_dtype.rule_element
val RE_compare : rule_element * rule_element -> order
datatype pp_element = datatype term_grammar_dtype.pp_element
datatype PhraseBlockStyle = datatype term_grammar_dtype.PhraseBlockStyle
datatype ParenStyle = datatype term_grammar_dtype.ParenStyle
val rule_elements : pp_element list -> rule_element list
val pp_elements_ok : pp_element list -> bool
val first_rtok : rule_element list -> string
val first_tok : pp_element list -> string
val reltoString : rule_element -> string
datatype binder = datatype term_grammar_dtype.binder
datatype prefix_rule = datatype term_grammar_dtype.prefix_rule
datatype suffix_rule = datatype term_grammar_dtype.suffix_rule
datatype infix_rule = datatype term_grammar_dtype.infix_rule
datatype grammar_rule = datatype term_grammar_dtype.grammar_rule
datatype fixity = datatype term_grammar_dtype.fixity
datatype user_delta = datatype term_grammar_dtype.user_delta
type listspec = term_grammar_dtype.listspec
type rule_record = term_grammar_dtype.rule_record
type grammar
val grule_toks : grule -> string list
val grule_name : grule -> string
val stdhol : grammar
val min_grammar : grammar
val binder_grule : {term_name : string, tok : string} -> grule
val standard_mapped_spacing :
{term_name:string,tok:string,fixity:fixity} -> grule
val standard_spacing : string -> fixity -> grule
val merge_grammars : grammar * grammar -> grammar
val fupdate_overload_info :
(overload_info -> overload_info) -> grammar -> grammar
val mfupdate_overload_info :
(overload_info -> overload_info * 'a) -> grammar -> grammar * 'a
(* User code additions *)
(* Users can add special-purpose printers and parsers to grammars *)
type term = Term.term
type userprinter =
(type_grammar.grammar * grammar,grammar) term_pp_types.userprinter
val add_user_printer :
(string * term * userprinter) -> grammar ->
grammar
val remove_user_printer :
string -> grammar -> (grammar * (term * userprinter) option)
val user_printers :
grammar -> (term * string * userprinter)FCNet.t
type absyn_postprocessor = grammar -> Absyn.absyn -> Absyn.absyn
type AbPTME = Absyn.absyn -> Parse_supportENV.preterm_in_env
type preterm_processor = grammar -> AbPTME -> AbPTME
structure userSyntaxFns :
sig
type 'a getter = string -> 'a
type 'a setter = {name : string, code : 'a} -> unit
val register_userPP : userprinter setter
val get_userPP : userprinter getter
val get_absynPostProcessor : absyn_postprocessor getter
val register_absynPostProcessor : absyn_postprocessor setter
end
val absyn_postprocessors :
grammar -> (string * absyn_postprocessor) list
val new_absyn_postprocessor :
string * absyn_postprocessor -> grammar -> grammar
val remove_absyn_postprocessor :
string -> grammar -> (grammar * absyn_postprocessor option)
val preterm_processor :
grammar -> string * int -> preterm_processor option
val new_preterm_processor :
string * int -> preterm_processor -> grammar -> grammar
val remove_preterm_processor :
string * int -> grammar -> grammar * preterm_processor option
type special_info = {type_intro : string,
lambda : string list,
endbinding : string,
restr_binders : (string option * string) list,
res_quanop : string}
val fupd_lambda : (string list -> string list) -> special_info ->
special_info
type ruleset
val rules : grammar -> (int option * grammar_rule) list
val ruleset : grammar -> ruleset
val grammar_rules : grammar -> grammar_rule list
val specials : grammar -> special_info
val fupdate_specials : (special_info -> special_info) -> grammar -> grammar
val numeral_info : grammar -> (char * string option) list
val overload_info : grammar -> overload_info
val grammar_name : grammar -> term -> string option
(*------------------------------------------------------------------------
* known constants are those strings that the parsing process will
* attempt to turn into constants. Known constants are those strings
* that are in the domain of the overloading map (this map being from
* strings to non-empty sets of constants.
*-------------------------------------------------------------------------*)
val known_constants : grammar -> string list
val binders : grammar -> string list
val is_binder : grammar -> string -> bool
val binder_to_string : grammar -> binder -> string
val resquan_op : grammar -> string
val associate_restriction : grammar ->
{binder : string option,
resbinder : string} -> grammar
val grammar_tokens : grammar -> string list
val rule_tokens : grammar -> grammar_rule -> string list
val add_binder : {term_name:string,tok:string} -> grammar -> grammar
val add_listform : grammar -> listspec -> grammar
val listform_to_rule : listspec -> grule
val fixityToString : fixity -> string
val add_rule : grule -> grammar -> grammar
val add_delta : user_delta -> grammar -> grammar
val add_deltas : user_delta list -> grammar -> grammar
val add_numeral_form : grammar -> (char * string option) -> grammar
val give_num_priority : grammar -> char -> grammar
val remove_numeral_form : grammar -> char -> grammar
val add_strlit_injector: {ldelim: string, tmnm: string} -> grammar -> grammar
val remove_strlit_injector : {tmnm:string} -> grammar -> grammar
val strlit_map : grammar -> {tmnm:string} -> string option
(*------------------------------------------------------------------------*
* this removes all those rules which give special status to the *
* given string. If there is a rule saying that COND is written *
* if _ then _ else _ *
* you could get rid of it with *
* remove_standard_form G "COND" *
*------------------------------------------------------------------------*)
val remove_standard_form : grammar -> string -> grammar
(* ----------------------------------------------------------------------
these two remove rules relating to the term which also include
a token, or the exact token list of the form given.
Thus, if you had two rules for COND, and you wanted to get rid of
the one with the "if" token in it, you would use
remove_form_with_tok G {term_name = "COND", tok = "if"}
---------------------------------------------------------------------- *)
val remove_form_with_tok : grammar -> {term_name : string, tok: string} ->
grammar
val remove_form_with_toklist : {term_name : string, toklist : string list} ->
grammar -> grammar
(* this one is the nuclear option, and just removes every rule that uses
the given token *)
val remove_rules_with_tok : string -> grammar -> grammar
val clear_overloads : grammar -> grammar
(*-----------------------------------------------------------------------*
* Pretty-printing *
*-----------------------------------------------------------------------*)
val prefer_form_with_tok : {term_name : string, tok : string} -> grammar ->
grammar
val prefer_form_with_toklist : {term_name : string, toklist : string list} ->
grammar -> grammar
val set_associativity_at_level : grammar -> int * associativity -> grammar
val get_precedence : grammar -> string -> fixity option
val rules_for : grammar -> string -> (int * user_delta) list
val prettyprint_grammar_rules
: (grammar -> term -> term_pp_types.uprinter) ->
ruleset -> term_pp_types.uprinter
val prettyprint_grammar : (grammar -> term -> term_pp_types.uprinter) ->
grammar -> term_pp_types.uprinter
val debugprint : grammar -> term -> string
end
HOL 4, Kananaskis-14