1signature term_grammar = 2sig 3 4 type block_info = term_grammar_dtype.block_info 5 type overload_info = Overload.overload_info 6 type associativity = term_grammar_dtype.associativity 7 type grule = term_grammar_dtype.grule 8 9 datatype rule_element = datatype term_grammar_dtype.rule_element 10 val RE_compare : rule_element * rule_element -> order 11 12 datatype pp_element = datatype term_grammar_dtype.pp_element 13 datatype PhraseBlockStyle = datatype term_grammar_dtype.PhraseBlockStyle 14 datatype ParenStyle = datatype term_grammar_dtype.ParenStyle 15 16 val rule_elements : pp_element list -> rule_element list 17 val pp_elements_ok : pp_element list -> bool 18 val first_rtok : rule_element list -> string 19 val first_tok : pp_element list -> string 20 21 val reltoString : rule_element -> string 22 23 datatype binder = datatype term_grammar_dtype.binder 24 datatype prefix_rule = datatype term_grammar_dtype.prefix_rule 25 datatype suffix_rule = datatype term_grammar_dtype.suffix_rule 26 datatype infix_rule = datatype term_grammar_dtype.infix_rule 27 datatype grammar_rule = datatype term_grammar_dtype.grammar_rule 28 datatype fixity = datatype term_grammar_dtype.fixity 29 datatype user_delta = datatype term_grammar_dtype.user_delta 30 type listspec = term_grammar_dtype.listspec 31 type rule_record = term_grammar_dtype.rule_record 32 33 type grammar 34 35 val grule_toks : grule -> string list 36 val grule_name : grule -> string 37 38 val stdhol : grammar 39 val min_grammar : grammar 40 41 val binder_grule : {term_name : string, tok : string} -> grule 42 val standard_mapped_spacing : 43 {term_name:string,tok:string,fixity:fixity} -> grule 44 val standard_spacing : string -> fixity -> grule 45 46 val merge_grammars : grammar * grammar -> grammar 47 val fupdate_overload_info : 48 (overload_info -> overload_info) -> grammar -> grammar 49 val mfupdate_overload_info : 50 (overload_info -> overload_info * 'a) -> grammar -> grammar * 'a 51 52 53 (* User code additions *) 54 (* Users can add special-purpose printers and parsers to grammars *) 55 type term = Term.term 56 type userprinter = 57 (type_grammar.grammar * grammar,grammar) term_pp_types.userprinter 58 val add_user_printer : 59 (string * term * userprinter) -> grammar -> 60 grammar 61 val remove_user_printer : 62 string -> grammar -> (grammar * (term * userprinter) option) 63 val user_printers : 64 grammar -> (term * string * userprinter)FCNet.t 65 66 type absyn_postprocessor = grammar -> Absyn.absyn -> Absyn.absyn 67 type AbPTME = Absyn.absyn -> Parse_supportENV.preterm_in_env 68 type preterm_processor = grammar -> AbPTME -> AbPTME 69 70 structure userSyntaxFns : 71 sig 72 type 'a getter = string -> 'a 73 type 'a setter = {name : string, code : 'a} -> unit 74 val register_userPP : userprinter setter 75 val get_userPP : userprinter getter 76 val get_absynPostProcessor : absyn_postprocessor getter 77 val register_absynPostProcessor : absyn_postprocessor setter 78 end 79 80 val absyn_postprocessors : 81 grammar -> (string * absyn_postprocessor) list 82 val new_absyn_postprocessor : 83 string * absyn_postprocessor -> grammar -> grammar 84 val remove_absyn_postprocessor : 85 string -> grammar -> (grammar * absyn_postprocessor option) 86 87 val preterm_processor : 88 grammar -> string * int -> preterm_processor option 89 val new_preterm_processor : 90 string * int -> preterm_processor -> grammar -> grammar 91 val remove_preterm_processor : 92 string * int -> grammar -> grammar * preterm_processor option 93 94 95 type special_info = {type_intro : string, 96 lambda : string list, 97 endbinding : string, 98 restr_binders : (string option * string) list, 99 res_quanop : string} 100 val fupd_lambda : (string list -> string list) -> special_info -> 101 special_info 102 103 type ruleset 104 val rules : grammar -> (int option * grammar_rule) list 105 val ruleset : grammar -> ruleset 106 val grammar_rules : grammar -> grammar_rule list 107 val specials : grammar -> special_info 108 val fupdate_specials : (special_info -> special_info) -> grammar -> grammar 109 val numeral_info : grammar -> (char * string option) list 110 val overload_info : grammar -> overload_info 111 val grammar_name : grammar -> term -> string option 112 113 (*------------------------------------------------------------------------ 114 * known constants are those strings that the parsing process will 115 * attempt to turn into constants. Known constants are those strings 116 * that are in the domain of the overloading map (this map being from 117 * strings to non-empty sets of constants. 118 *-------------------------------------------------------------------------*) 119 120 val known_constants : grammar -> string list 121 122 val binders : grammar -> string list 123 val is_binder : grammar -> string -> bool 124 val binder_to_string : grammar -> binder -> string 125 126 val resquan_op : grammar -> string 127 val associate_restriction : grammar -> 128 {binder : string option, 129 resbinder : string} -> grammar 130 131 val grammar_tokens : grammar -> string list 132 val rule_tokens : grammar -> grammar_rule -> string list 133 134 val add_binder : {term_name:string,tok:string} -> grammar -> grammar 135 val add_listform : grammar -> listspec -> grammar 136 val listform_to_rule : listspec -> grule 137 138 val fixityToString : fixity -> string 139 val add_rule : grule -> grammar -> grammar 140 val add_delta : user_delta -> grammar -> grammar 141 val add_deltas : user_delta list -> grammar -> grammar 142 143 val add_numeral_form : grammar -> (char * string option) -> grammar 144 val give_num_priority : grammar -> char -> grammar 145 val remove_numeral_form : grammar -> char -> grammar 146 147 val add_strlit_injector: {ldelim: string, tmnm: string} -> grammar -> grammar 148 val remove_strlit_injector : {tmnm:string} -> grammar -> grammar 149 val strlit_map : grammar -> {tmnm:string} -> string option 150 151 (*------------------------------------------------------------------------* 152 * this removes all those rules which give special status to the * 153 * given string. If there is a rule saying that COND is written * 154 * if _ then _ else _ * 155 * you could get rid of it with * 156 * remove_standard_form G "COND" * 157 *------------------------------------------------------------------------*) 158 159 val remove_standard_form : grammar -> string -> grammar 160 161 (* ---------------------------------------------------------------------- 162 these two remove rules relating to the term which also include 163 a token, or the exact token list of the form given. 164 Thus, if you had two rules for COND, and you wanted to get rid of 165 the one with the "if" token in it, you would use 166 167 remove_form_with_tok G {term_name = "COND", tok = "if"} 168 ---------------------------------------------------------------------- *) 169 170 val remove_form_with_tok : grammar -> {term_name : string, tok: string} -> 171 grammar 172 val remove_form_with_toklist : {term_name : string, toklist : string list} -> 173 grammar -> grammar 174 175 (* this one is the nuclear option, and just removes every rule that uses 176 the given token *) 177 val remove_rules_with_tok : string -> grammar -> grammar 178 179 val clear_overloads : grammar -> grammar 180 181 (*-----------------------------------------------------------------------* 182 * Pretty-printing * 183 *-----------------------------------------------------------------------*) 184 185 val prefer_form_with_tok : {term_name : string, tok : string} -> grammar -> 186 grammar 187 val prefer_form_with_toklist : {term_name : string, toklist : string list} -> 188 grammar -> grammar 189 190 191 val set_associativity_at_level : grammar -> int * associativity -> grammar 192 val get_precedence : grammar -> string -> fixity option 193 val rules_for : grammar -> string -> (int * user_delta) list 194 195 196 val prettyprint_grammar_rules 197 : (grammar -> term -> term_pp_types.uprinter) -> 198 ruleset -> term_pp_types.uprinter 199 val prettyprint_grammar : (grammar -> term -> term_pp_types.uprinter) -> 200 grammar -> term_pp_types.uprinter 201 202 val debugprint : grammar -> term -> string 203 204end 205