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