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