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