1signature Parse = sig
2
3  type term = Term.term
4  type hol_type = Type.hol_type
5  type thm = Thm.thm
6  type associativity = HOLgrammars.associativity
7  type pp_element = term_grammar.pp_element
8  type PhraseBlockStyle = term_grammar.PhraseBlockStyle
9  type ParenStyle = term_grammar.ParenStyle
10  type block_info = term_grammar.block_info
11  type 'a frag = 'a PP.frag
12  type 'a pprinter = 'a -> HOLPP.pretty
13
14  datatype fixity = datatype term_grammar_dtype.fixity
15  val fixityToString : fixity -> string
16
17  type grammarDB_info = type_grammar.grammar * term_grammar.grammar
18  val grammarDB_insert : string * grammarDB_info -> unit
19  val grammarDB_fold : (string * grammarDB_info * 'a -> 'a) -> 'a -> 'a
20  val grammarDB : string -> grammarDB_info option
21  val set_grammar_ancestry : string list -> unit
22
23  (* Parsing Types *)
24
25  val type_grammar : unit -> type_grammar.grammar
26  val Type         : hol_type frag list -> hol_type
27  val ==           : hol_type frag list -> 'a -> hol_type
28
29  val add_type : string -> unit
30  val add_qtype : {Thy:string,Name:string} -> unit
31  val temp_add_type : string -> unit
32  val temp_add_qtype : {Thy:string,Name:string} -> unit
33  val add_infix_type : {Prec : int,
34                        ParseName : string option,
35                        Name : string,
36                        Assoc : associativity} -> unit
37  val temp_add_infix_type : {Prec : int,
38                             ParseName : string option,
39                             Name : string,
40                             Assoc : associativity} -> unit
41
42  val temp_thytype_abbrev : KernelSig.kernelname * hol_type -> unit
43  val thytype_abbrev : KernelSig.kernelname * hol_type -> unit
44  val temp_type_abbrev : string * hol_type -> unit
45  val type_abbrev : string * hol_type -> unit
46  val temp_disable_tyabbrev_printing : string -> unit
47  val disable_tyabbrev_printing : string -> unit
48  val remove_type_abbrev : string -> unit
49  val temp_remove_type_abbrev : string -> unit
50
51  (* Parsing terms *)
52
53  val post_process_term: (term -> term) ref
54  val add_absyn_postprocessor : string -> unit
55  val temp_add_absyn_postprocessor :
56      (string * term_grammar.absyn_postprocessor) -> unit
57  val temp_remove_absyn_postprocessor :
58      string -> term_grammar.absyn_postprocessor option
59  val temp_add_preterm_processor :
60      string * int -> term_grammar.preterm_processor -> unit
61  val temp_remove_preterm_processor :
62      string * int -> term_grammar.preterm_processor option
63
64  val absyn_to_term    : term_grammar.grammar -> Absyn.absyn -> term
65  val absyn_to_preterm : Absyn.absyn -> Preterm.preterm Pretype.in_env
66  val Absyn            : term frag list -> Absyn.absyn
67  val Preterm          : term frag list -> Preterm.preterm
68  val Term             : term frag list -> term
69  val typedTerm        : term frag list -> hol_type -> term
70  val ty_antiq         : hol_type -> term
71  val parse_in_context : term list -> term frag list -> term
72  val typed_parse_in_context : hol_type -> term list -> term frag list -> term
73  val parse_from_grammars :
74      (type_grammar.grammar * term_grammar.grammar) ->
75      ((hol_type frag list -> hol_type) * (term frag list -> term))
76  val print_from_grammars :
77      (type_grammar.grammar * term_grammar.grammar) ->
78      (hol_type pprinter * term pprinter)
79  val print_term_by_grammar :
80        (type_grammar.grammar * term_grammar.grammar) -> term -> unit
81  val print_without_macros : term -> unit
82
83  val term_grammar : unit -> term_grammar.grammar
84
85  val print_term_grammar : unit -> unit
86
87  (* the following functions modify the grammar, and do so in such a
88     way that the exported theory will have the same grammar  *)
89
90  val add_const  : string -> unit
91  val add_infix  : string * int * associativity -> unit
92  val std_binder_precedence : int
93  val add_rule   : {term_name : string, fixity :fixity,
94                    pp_elements: pp_element list, paren_style : ParenStyle,
95                    block_style : PhraseBlockStyle * block_info} -> unit
96  val add_listform : {separator : pp_element list, leftdelim : pp_element list,
97                      rightdelim : pp_element list, cons : string,
98                      nilstr : string, block_info : block_info} -> unit
99  val add_numeral_form : (char * string option) -> unit
100  val add_bare_numeral_form : (char * string option) -> unit
101  val give_num_priority : char -> unit
102  val remove_numeral_form : char -> unit
103  val associate_restriction : (string * string) -> unit
104  val prefer_form_with_tok : {term_name : string, tok : string} -> unit
105  val set_fixity : string -> fixity -> unit
106  val set_mapped_fixity : {term_name : string, tok : string, fixity : fixity} ->
107                          unit
108
109  val remove_rules_for_term : string -> unit
110  val remove_termtok : {term_name : string, tok : string} -> unit
111
112  (* overloading and records *)
113
114  val overload_on : string * term -> unit
115  val inferior_overload_on : string * term -> unit
116  val overload_on_by_nametype : string -> {Name: string, Thy: string} -> unit
117  val send_to_back_overload : string -> {Name: string, Thy: string} -> unit
118  val bring_to_front_overload : string -> {Name: string, Thy: string} -> unit
119  val clear_overloads_on : string -> unit
120  val remove_ovl_mapping : string -> {Name:string, Thy:string} -> unit
121  val gen_remove_ovl_mapping : string -> term -> unit
122  val add_record_field : string * term -> unit
123  val add_record_fupdate : string * term -> unit
124
125  (* information about overloads and abbreviations;
126     call interactively for information printed to stdout *)
127  val overload_info_for : string -> unit
128
129  (* printing without overloads or abbreviations *)
130  val pp_term_without_overloads_on : string list -> term pprinter
131  val pp_term_without_overloads : (string * term) list -> term pprinter
132  val pp_type_without_abbrevs : string list -> hol_type pprinter
133
134  (* adding and removing user parsers and printers to the grammar *)
135
136  val add_user_printer : (string * term) -> unit
137  val remove_user_printer : string -> (term * term_grammar.userprinter) option
138  val constant_string_printer : string -> term_grammar.userprinter
139
140 (* the following functions affect the grammar, but not so that the
141    grammar exported to disk will be modified *)
142
143  val temp_set_grammars : (type_grammar.grammar * term_grammar.grammar) -> unit
144  val temp_add_rule :
145    {term_name : string, fixity : fixity,
146     pp_elements: pp_element list, paren_style : ParenStyle,
147     block_style : PhraseBlockStyle * block_info}  -> unit
148  val temp_add_infix : (string * int * associativity) -> unit
149  val temp_add_listform : {separator : pp_element list,
150                           leftdelim : pp_element list,
151                           rightdelim : pp_element list, cons : string,
152                           nilstr : string, block_info : block_info} -> unit
153  val temp_add_numeral_form : (char * string option) -> unit
154  val temp_add_bare_numeral_form : (char * string option) -> unit
155  val temp_give_num_priority : char -> unit
156  val temp_remove_numeral_form : char -> unit
157  val temp_associate_restriction : (string * string) -> unit
158  val temp_prefer_form_with_tok : {term_name : string, tok : string} -> unit
159  val temp_set_fixity : string -> fixity -> unit
160  val temp_set_mapped_fixity :
161      {term_name : string, tok : string, fixity : fixity} -> unit
162
163  val temp_remove_rules_for_term : string -> unit
164  val temp_remove_termtok : {term_name : string, tok : string} -> unit
165  val temp_set_associativity : (int * associativity) -> unit
166
167  val temp_overload_on : string * term -> unit
168  val temp_inferior_overload_on : string * term -> unit
169  val temp_overload_on_by_nametype : string -> {Name:string,Thy:string} -> unit
170  val temp_send_to_back_overload : string -> {Name:string,Thy:string} -> unit
171  val temp_bring_to_front_overload : string -> {Name:string,Thy:string} -> unit
172  val temp_clear_overloads_on : string -> unit
173  val temp_remove_ovl_mapping : string -> {Name:string, Thy:string} -> unit
174  val temp_gen_remove_ovl_mapping : string -> term -> unit
175
176  val temp_add_record_field : string * term -> unit
177  val temp_add_record_fupdate : string * term -> unit
178
179  val temp_add_user_printer : (string * term * term_grammar.userprinter) ->
180                              unit
181  val temp_remove_user_printer : string ->
182                                 (term * term_grammar.userprinter) option
183
184  val try_grammar_extension : ('a -> 'b) -> 'a -> 'b
185
186
187  (* Pretty printing *)
188  val current_backend : PPBackEnd.t ref
189  val interactive_ppbackend : unit -> PPBackEnd.t
190  val mlower : (term_pp_types.printing_info,'a)smpp.t -> HOLPP.pretty
191  val pp_term : term pprinter
192  val pp_type : hol_type pprinter
193  val pp_thm : thm pprinter
194  val stdprinters : ((term -> string) * (hol_type -> string)) option
195
196  val term_pp_with_delimiters : term pprinter -> term pprinter
197  val type_pp_with_delimiters : hol_type pprinter -> hol_type pprinter
198  val get_term_printer : unit -> term pprinter
199  val set_term_printer : term pprinter -> term pprinter
200
201  val minprint               : term -> string
202  val rawterm_pp             : ('a -> 'b) -> 'a -> 'b
203  val add_style_to_string    : PPBackEnd.pp_style list -> string -> string
204  val print_with_style       : PPBackEnd.pp_style list -> string -> unit
205  val term_to_string         : term -> string
206  val type_to_string         : hol_type -> string
207  val thm_to_string          : thm -> string
208
209  val print_thm              : thm -> unit
210  val print_type             : hol_type -> unit
211  val print_term             : term -> unit
212
213
214  val export_theorems_as_docfiles : string -> (string * thm) list -> unit
215
216  val hide   : string -> ({Name : string, Thy : string} list *
217                          {Name : string, Thy : string} list)
218  val update_overload_maps :
219    string -> ({Name : string, Thy : string} list *
220               {Name : string, Thy : string} list) -> unit
221
222  val reveal : string -> unit
223  val hidden : string -> bool
224  val known_constants     : unit -> string list
225  val set_known_constants : string list -> unit
226  val is_constname : string -> bool
227
228  val LEFT       : associativity
229  val RIGHT      : associativity
230  val NONASSOC   : associativity
231
232  val Infixl     : int -> fixity
233  val Infixr     : int -> fixity
234  val fixity     : string -> fixity option
235
236  (* more constructors/values that come across from term_grammar *)
237
238  val TM               : pp_element
239  val TOK              : string -> pp_element
240  val BreakSpace       : int * int -> pp_element
241  val HardSpace        : int -> pp_element
242  val BeginFinalBlock  : block_info -> pp_element
243  val EndInitialBlock  : block_info -> pp_element
244  val PPBlock          : pp_element list * block_info -> pp_element
245  val ListForm         : {separator:pp_element list, cons : string,
246                          nilstr : string, block_info : block_info} ->
247                         pp_element
248
249  val OnlyIfNecessary  : ParenStyle
250  val ParoundName      : ParenStyle
251  val ParoundPrec      : ParenStyle
252  val Always           : ParenStyle
253  val NotEvenIfRand    : ParenStyle
254
255  val AroundEachPhrase : PhraseBlockStyle
256  val AroundSamePrec   : PhraseBlockStyle
257  val AroundSameName   : PhraseBlockStyle
258  val NoPhrasing       : PhraseBlockStyle
259
260  val min_grammars : type_grammar.grammar * term_grammar.grammar
261  val merge_grammars : string list ->
262                       type_grammar.grammar * term_grammar.grammar
263  val current_grammars : unit -> type_grammar.grammar * term_grammar.grammar
264
265  structure Unicode : sig
266    val unicode_version : {u:string,tmnm:string} -> unit
267    val temp_unicode_version : {u:string,tmnm:string} -> unit
268
269    structure UChar : UnicodeChars
270  end
271
272
273end
274