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 : {thyname:string} -> grammarDB_info option 19 val set_grammar_ancestry : string list -> unit 20 21 (* Parsing Types *) 22 23 val type_grammar : unit -> type_grammar.grammar 24 val Type : hol_type frag list -> hol_type 25 val == : hol_type frag list -> 'a -> hol_type 26 27 val add_type : string -> unit 28 val add_qtype : {Thy:string,Name:string} -> unit 29 val temp_add_type : string -> unit 30 val temp_add_qtype : {Thy:string,Name:string} -> unit 31 val add_infix_type : {Prec : int, 32 ParseName : string option, 33 Name : string, 34 Assoc : associativity} -> unit 35 val temp_add_infix_type : {Prec : int, 36 ParseName : string option, 37 Name : string, 38 Assoc : associativity} -> unit 39 40 val temp_thytype_abbrev : KernelSig.kernelname * hol_type * bool -> unit 41 val thytype_abbrev : KernelSig.kernelname * hol_type * bool -> unit 42 val temp_type_abbrev : string * hol_type -> unit 43 val type_abbrev : string * hol_type -> unit 44 val temp_disable_tyabbrev_printing : string -> unit 45 val disable_tyabbrev_printing : string -> unit 46 val remove_type_abbrev : string -> unit 47 val temp_remove_type_abbrev : string -> unit 48 val temp_type_abbrev_pp : string * hol_type -> unit 49 val type_abbrev_pp : string * hol_type -> 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_strliteral_form : {ldelim:string,inj:term} -> unit 101 val remove_strliteral_form : {tmnm : string} -> unit 102 val add_bare_numeral_form : (char * string option) -> unit 103 val give_num_priority : char -> unit 104 val remove_numeral_form : char -> unit 105 val associate_restriction : (string * string) -> unit 106 val prefer_form_with_tok : {term_name : string, tok : string} -> unit 107 val set_fixity : string -> fixity -> unit 108 val set_mapped_fixity : {term_name : string, tok : string, fixity : fixity} -> 109 unit 110 111 val remove_rules_for_term : string -> unit 112 val remove_termtok : {term_name : string, tok : string} -> unit 113 114 (* overloading and records *) 115 116 val overload_on : string * term -> unit 117 val inferior_overload_on : string * term -> unit 118 val overload_on_by_nametype : string -> {Name: string, Thy: string} -> unit 119 val send_to_back_overload : string -> {Name: string, Thy: string} -> unit 120 val bring_to_front_overload : string -> {Name: string, Thy: string} -> unit 121 val clear_overloads_on : string -> unit 122 val remove_ovl_mapping : string -> {Name:string, Thy:string} -> unit 123 val gen_remove_ovl_mapping : string -> term -> unit 124 val add_record_field : string * term -> unit 125 val add_record_fupdate : string * term -> unit 126 127 (* information about overloads and abbreviations; 128 call interactively for information printed to stdout *) 129 val overload_info_for : string -> unit 130 131 (* printing without overloads or abbreviations *) 132 val pp_term_without_overloads_on : string list -> term pprinter 133 val pp_term_without_overloads : (string * term) list -> term pprinter 134 val pp_type_without_abbrevs : string list -> hol_type pprinter 135 136 (* adding and removing user parsers and printers to the grammar *) 137 138 val add_user_printer : (string * term) -> unit 139 val remove_user_printer : string -> (term * term_grammar.userprinter) option 140 val constant_string_printer : string -> term_grammar.userprinter 141 142 (* the following functions affect the grammar, but not so that the 143 grammar exported to disk will be modified *) 144 145 val temp_set_grammars : (type_grammar.grammar * term_grammar.grammar) -> unit 146 val temp_add_rule : 147 {term_name : string, fixity : fixity, 148 pp_elements: pp_element list, paren_style : ParenStyle, 149 block_style : PhraseBlockStyle * block_info} -> unit 150 val temp_add_infix : (string * int * associativity) -> unit 151 val temp_add_listform : {separator : pp_element list, 152 leftdelim : pp_element list, 153 rightdelim : pp_element list, cons : string, 154 nilstr : string, block_info : block_info} -> unit 155 val temp_add_numeral_form : (char * string option) -> unit 156 val temp_add_bare_numeral_form : (char * string option) -> unit 157 val temp_give_num_priority : char -> unit 158 val temp_add_strliteral_form : {ldelim:string,inj:term} -> unit 159 val temp_remove_strliteral_form : {tmnm : string} -> unit 160 val temp_remove_numeral_form : char -> unit 161 val temp_associate_restriction : (string * string) -> unit 162 val temp_prefer_form_with_tok : {term_name : string, tok : string} -> unit 163 val temp_set_fixity : string -> fixity -> unit 164 val temp_set_mapped_fixity : 165 {term_name : string, tok : string, fixity : fixity} -> unit 166 167 val temp_remove_rules_for_term : string -> unit 168 val temp_remove_termtok : {term_name : string, tok : string} -> unit 169 val temp_set_associativity : (int * associativity) -> unit 170 171 val temp_overload_on : string * term -> unit 172 val temp_inferior_overload_on : string * term -> unit 173 val temp_overload_on_by_nametype : string -> {Name:string,Thy:string} -> unit 174 val temp_send_to_back_overload : string -> {Name:string,Thy:string} -> unit 175 val temp_bring_to_front_overload : string -> {Name:string,Thy:string} -> unit 176 val temp_clear_overloads_on : string -> unit 177 val temp_remove_ovl_mapping : string -> {Name:string, Thy:string} -> unit 178 val temp_gen_remove_ovl_mapping : string -> term -> unit 179 180 val temp_add_record_field : string * term -> unit 181 val temp_add_record_fupdate : string * term -> unit 182 183 val temp_add_user_printer : (string * term * term_grammar.userprinter) -> 184 unit 185 val temp_remove_user_printer : string -> 186 (term * term_grammar.userprinter) option 187 188 val try_grammar_extension : ('a -> 'b) -> 'a -> 'b 189 190 191 (* Pretty printing *) 192 val current_backend : PPBackEnd.t ref 193 val interactive_ppbackend : unit -> PPBackEnd.t 194 val mlower : (term_pp_types.printing_info,'a)smpp.t -> HOLPP.pretty 195 val pp_term : term pprinter 196 val pp_type : hol_type pprinter 197 val pp_thm : thm pprinter 198 val stdprinters : ((term -> string) * (hol_type -> string)) option 199 200 val term_pp_with_delimiters : term pprinter -> term pprinter 201 val type_pp_with_delimiters : hol_type pprinter -> hol_type pprinter 202 val get_term_printer : unit -> term pprinter 203 val set_term_printer : term pprinter -> term pprinter 204 205 val minprint : term -> string 206 val rawterm_pp : ('a -> 'b) -> 'a -> 'b 207 val add_style_to_string : PPBackEnd.pp_style list -> string -> string 208 val print_with_style : PPBackEnd.pp_style list -> string -> unit 209 val term_to_string : term -> string 210 val type_to_string : hol_type -> string 211 val thm_to_string : thm -> string 212 213 val print_thm : thm -> unit 214 val print_type : hol_type -> unit 215 val print_term : term -> unit 216 217 218 val export_theorems_as_docfiles : string -> (string * thm) list -> unit 219 220 val hide : string -> ({Name : string, Thy : string} list * 221 {Name : string, Thy : string} list) 222 val update_overload_maps : 223 string -> ({Name : string, Thy : string} list * 224 {Name : string, Thy : string} list) -> unit 225 226 val reveal : string -> unit 227 val hidden : string -> bool 228 val known_constants : unit -> string list 229 val set_known_constants : string list -> unit 230 val is_constname : string -> bool 231 232 val LEFT : associativity 233 val RIGHT : associativity 234 val NONASSOC : associativity 235 236 val Infixl : int -> fixity 237 val Infixr : int -> fixity 238 val fixity : string -> fixity option 239 240 (* more constructors/values that come across from term_grammar *) 241 242 val TM : pp_element 243 val TOK : string -> pp_element 244 val BreakSpace : int * int -> pp_element 245 val HardSpace : int -> pp_element 246 val BeginFinalBlock : block_info -> pp_element 247 val EndInitialBlock : block_info -> pp_element 248 val PPBlock : pp_element list * block_info -> pp_element 249 val ListForm : {separator:pp_element list, cons : string, 250 nilstr : string, block_info : block_info} -> 251 pp_element 252 253 val OnlyIfNecessary : ParenStyle 254 val ParoundName : ParenStyle 255 val ParoundPrec : ParenStyle 256 val Always : ParenStyle 257 val NotEvenIfRand : ParenStyle 258 259 val AroundEachPhrase : PhraseBlockStyle 260 val AroundSamePrec : PhraseBlockStyle 261 val AroundSameName : PhraseBlockStyle 262 val NoPhrasing : PhraseBlockStyle 263 264 val min_grammars : type_grammar.grammar * term_grammar.grammar 265 val merge_grammars : string list -> 266 type_grammar.grammar * term_grammar.grammar 267 val current_grammars : unit -> type_grammar.grammar * term_grammar.grammar 268 269 structure Unicode : sig 270 val unicode_version : {u:string,tmnm:string} -> unit 271 val temp_unicode_version : {u:string,tmnm:string} -> unit 272 273 structure UChar : UnicodeChars 274 end 275 276 277end 278