1structure ConstMapML :> ConstMapML =
2struct
3
4local open boolTheory in end;
5
6open HolKernel
7
8val ERR = mk_HOL_ERR "ConstMapML";
9
10fun LEX c1 c2 ((x1,x2),(y1,y2)) =
11  case c1 (x1,y1)
12   of EQUAL => c2 (x2,y2)
13    | other => other;
14
15val qmk_vartype = with_flag (Feedback.emit_WARNING,false) mk_vartype;
16
17val eq_alpha = qmk_vartype "''a";
18
19(* ----------------------------------------------------------------------
20    The initial constant map has equality, conjunction, disjunction,
21    negation, true, and false in it. The range is 4-tuples of the form
22    (is_constructor,structure name,value name, type).
23   ---------------------------------------------------------------------- *)
24
25
26
27structure CMap :> sig
28  type 'a dict
29  val empty : unit -> 'a dict
30  val insert : ('a dict * term * 'a) -> 'a dict
31  val peek : 'a dict * term -> 'a option
32  val exact_peek : 'a dict * term -> 'a option
33end =
34struct
35  structure RBM = Redblackmap
36  fun tstamp () = Time.toReal (Time.now())
37  type 'a dict = ({Name:string,Thy:string}, ('a * real) TypeNet.typenet)RBM.dict
38  fun insert (d,k,v) = let
39    val v = (v,tstamp())
40    val {Name,Thy,Ty} = dest_thy_const k
41    val rbk = {Name = Name, Thy = Thy}
42  in
43    case RBM.peek(d, rbk) of
44      NONE => RBM.insert(d,rbk,TypeNet.insert(TypeNet.empty,Ty,v))
45    | SOME tynet => let
46        val tynet' = TypeNet.insert(tynet,Ty,v)
47      in
48        RBM.insert(d,rbk,tynet')
49      end
50  end
51
52  fun peek(d,k) = let
53    val {Name,Thy,Ty} = dest_thy_const k
54    val rbk = {Name = Name, Thy = Thy}
55  in
56    case RBM.peek(d,rbk) of
57      NONE => NONE
58    | SOME tynet => let
59      in
60        case TypeNet.match(tynet, Ty) of
61          [] => NONE
62        | possresults => let
63            fun possmatch (pat,data) =
64                case Lib.total (fn ty => raw_match_type pat ty ([],[])) Ty of
65                  NONE => NONE
66                | SOME (inst,eqs) => SOME (map (fn ty => ty |-> ty) eqs @ inst,
67                                           data)
68            val insts0 = List.mapPartial possmatch possresults
69            fun isize sigma =
70                List.foldl (fn ({residue,...},acc) => acc + type_size residue)
71                           0
72                           sigma
73            val icmp0 = pair_compare (measure_cmp isize,
74                                      flip_order o Real.compare)
75            val icmp = inv_img_cmp (fn (i,(d,t)) => (i,t)) icmp0
76            val insts = Listsort.sort icmp insts0
77          in
78            case insts of
79              [] => NONE
80            | (i,(d,t)) :: _ => SOME d
81          end
82      end
83  end
84  fun cmp ({Name=n1,Thy=t1},{Name=n2,Thy=t2}) =
85      pair_compare(String.compare,String.compare) ((n1,t1),(n2,t2))
86  fun empty() = RBM.mkDict cmp
87
88  fun exact_peek (d : 'a dict,k) = let
89    val {Name,Thy,Ty} = dest_thy_const k
90    val rbk = {Name = Name, Thy = Thy}
91  in
92    case RBM.peek(d,rbk) of
93      NONE => NONE
94    | SOME tynet => Option.map #1 (TypeNet.peek(tynet,Ty))
95  end
96
97end (* struct *)
98
99open CMap
100
101type constmap = (bool*string*string*hol_type)dict
102
103
104(*---------------------------------------------------------------------------*)
105(* Need to call same_const in order to get the notion of equality desired,   *)
106(* otherwise could just use Term.compare.                                    *)
107(*---------------------------------------------------------------------------*)
108
109val initConstMap : constmap = empty()
110
111local val equality = prim_mk_const{Name="=",Thy="min"}
112      val negation = prim_mk_const{Name="~",Thy="bool"}
113      val T        = prim_mk_const{Name="T",Thy="bool"}
114      val F        = prim_mk_const{Name="F",Thy="bool"}
115      val conj     = prim_mk_const{Name="/\\",Thy="bool"}
116      val disj     = prim_mk_const{Name="\\/",Thy="bool"}
117in
118val ConstMapRef = ref
119  (insert(insert(insert(insert(insert(insert
120    (initConstMap,
121     equality, (false,"","=",    eq_alpha-->eq_alpha-->bool)),
122     negation, (false,"","not",  bool-->bool)),
123     T,        (false,"","true", bool)),
124     F,        (false,"","false",bool)),
125     conj,     (false,"","andalso",bool-->bool-->bool)),
126     disj,     (false,"","orelse", bool-->bool-->bool)))
127end;
128
129fun theConstMap () = !ConstMapRef;
130
131(*---------------------------------------------------------------------------*)
132(* Checks for "*" are to avoid situation where prefix multiplication has an  *)
133(* open paren just before it ... which is interpreted as beginning of a      *)
134(* comment.                                                                  *)
135(*---------------------------------------------------------------------------*)
136
137local fun check_name(is_type_cons,Thy,Name,Ty) =
138       let val Name' = if String.sub(Name,0) = #"*" orelse
139                          String.sub(Name,String.size Name -1) = #"*"
140                       then " "^Name^" "
141                       else Name
142       in (is_type_cons,Thy,Name',Ty)
143       end
144in
145fun prim_insert (c,t) = (ConstMapRef := insert(theConstMap(),c,check_name t))
146end;
147
148
149fun insert c =
150 let val {Name,Thy,Ty} = dest_thy_const c
151 in prim_insert(c,(false,Thy,Name,Ty))
152 end;
153
154fun insert_cons c =
155 let val {Name,Thy,Ty} = dest_thy_const c
156 in prim_insert(c,(true,Thy,Name,Ty))
157 end;
158
159fun apply c =
160 case peek(theConstMap(),c)
161   of SOME triple => triple
162    | NONE => let val {Name,Thy,Ty} = dest_thy_const c
163              in raise ERR "apply"
164                       ("no binding found for "^Lib.quote(Thy^"$"^Name))
165              end
166
167fun exact_peek c = CMap.exact_peek(theConstMap(), c)
168
169end
170