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