Structure term_grammar


Source File Identifier index Theory binding index

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


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14