1signature ConstMapML =
2sig
3
4  type constmap
5
6  type hol_type = Type.hol_type
7  type term     = Term.term
8
9  val theConstMap : unit -> constmap
10  val prim_insert : term * (bool * string * string * hol_type) -> unit
11  val insert      : term -> unit
12  val insert_cons : term -> unit
13  val apply       : term -> bool * string * string * hol_type
14  val exact_peek  : term -> (bool * string * string * hol_type) option
15
16  (* [apply] peforms a lookup and returns the most specific match.  Thus,
17     if the map has data for both
18       APPEND : 'a list -> 'a list -> 'a list
19     and
20       APPEND : char list -> char list -> char list
21     Then, you will get the data for the latter rather than the former when
22     you ask for APPEND : string -> string -> string.  But you will get the
23     former if you ask for data on APPEND : num list -> num list -> num list.
24
25     [exact_peek] does an exact lookup on the term.  Thus, if you have the
26     situation as above, and exact_peek on
27       APPEND : num list -> num list -> num list
28     you will get back NONE.
29   *)
30end
31