1signature Overload = 2sig 3 type hol_type = HolKernel.hol_type 4 type term = HolKernel.term 5 6 type nthy_rec = {Name : string, Thy : string} 7 type overloaded_op_info = {base_type : hol_type, actual_ops : term list, 8 tyavoids : hol_type list} 9 10 11 type overload_info 12 type printmap_data = term * string * int 13 14 val null_oinfo : overload_info 15 16 (* the parse map, taking strings to possible constants *) 17 val oinfo_ops : overload_info -> (string * overloaded_op_info) list 18 19 (* the print map, taking constants to at most one string *) 20 val print_map : overload_info -> (nthy_rec * string) list 21 22 structure PrintMap : LV_TERM_NET where type value = printmap_data 23 val raw_print_map : overload_info -> PrintMap.lvtermnet 24 25 val fupd_actual_ops : 26 (term list -> term list) -> overloaded_op_info -> 27 overloaded_op_info 28 29 exception OVERLOAD_ERR of string 30 31 val remove_overloaded_form : 32 string -> overload_info -> overload_info * (term list * term list) 33 34 val raw_map_insert : 35 string -> (nthy_rec list * nthy_rec list) -> 36 overload_info -> overload_info 37 38 val info_for_name : overload_info -> string -> overloaded_op_info option 39 val is_overloaded : overload_info -> string -> bool 40 val overloading_of_term : overload_info -> Term.term -> string option 41 val overloading_of_termP : overload_info -> (string -> bool) -> Term.term -> 42 string option 43 val overloading_of_nametype : 44 overload_info -> {Name : string, Thy : string} -> 45 string option 46 47 val add_overloading : string * term -> overload_info -> overload_info 48 val add_inferior_overloading : string * term -> overload_info -> overload_info 49 50 val send_to_back_overloading: 51 {opname: string, realname: string, realthy : string} -> 52 overload_info -> overload_info 53 54 val bring_to_front_overloading: 55 {opname: string, realname: string, realthy : string} -> 56 overload_info -> overload_info 57 58 val merge_oinfos : overload_info -> overload_info -> overload_info 59 60 val known_constants : overload_info -> string list 61 62 val remove_mapping : 63 string -> {Name:string, Thy:string} -> overload_info -> overload_info 64 val gen_remove_mapping : string -> term -> overload_info -> overload_info 65 66 val oi_strip_comb : overload_info -> term -> (term * term list) option 67 val oi_strip_combP : overload_info -> (string -> bool) -> term -> 68 (term * term list) option 69 70end 71 72(* [oi_strip_comb oinfo t] returns SOME(f, args, pattern) if the the term t 73 matches the pattern orig in the overload info's print-map, and this pattern 74 decomposes t into operator f applied to arguments args. 75 76 Further, this is the best such match, according to the heuristics 77 that overloading uses. 78*) 79