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