1structure flookupLib :> flookupLib = 2struct 3 4open HolKernel boolLib bossLib finite_mapSyntax 5 6val ERR = mk_HOL_ERR "flookupLib" 7 8(* ------------------------------------------------------------------------- *) 9 10fun memoize size cmp f = 11 let 12 val d = ref (Redblackmap.mkDict cmp) 13 val k = ref [] 14 val finite = 0 < size 15 in 16 fn v => 17 case Redblackmap.peek (!d, v) of 18 SOME r => r 19 | NONE => 20 let 21 val r = f v 22 in 23 if finite 24 then (k := !k @ [v] 25 ; if size < Redblackmap.numItems (!d) 26 then case List.getItem (!k) of 27 SOME (h, t) => 28 (d := fst (Redblackmap.remove (!d, h)) 29 ; k := t) 30 | NONE => raise ERR "memoize" "empty" 31 else ()) 32 else () 33 ; d := Redblackmap.insert (!d, v, r) 34 ; r 35 end 36 end 37 38local 39 fun one_ones ty = 40 Option.getOpt (Lib.total (CONJUNCTS o TypeBase.one_one_of) ty, []) 41 val eqf_into = List.map (EQF_INTRO o SPEC_ALL) o CONJUNCTS 42in 43 val datatype_eq_conv = 44 memoize 20 Type.compare 45 (fn ty => 46 case Lib.total TypeBase.distinct_of ty of 47 SOME th => 48 PURE_REWRITE_CONV 49 (one_ones ty @ eqf_into th @ eqf_into (GSYM th)) 50 | NONE => EVAL) 51end 52 53fun eq_conv ty = 54 (!Defn.const_eq_ref) 55 ORELSEC (datatype_eq_conv ty 56 THENC (fn tm => 57 case Lib.total boolSyntax.dest_eq tm of 58 SOME (l, r) => 59 if l = r 60 then Drule.ISPEC l boolTheory.REFL_CLAUSE 61 else eq_conv (Term.type_of l) tm 62 | NONE => ALL_CONV tm)) 63 64local 65 val not_F_imp = DECIDE ``(~F ==> a) = a`` 66in 67 fun neqs_rule ty = 68 let 69 val neqs_rule = 70 Conv.CONV_RULE (Conv.LAND_CONV (Conv.RAND_CONV (eq_conv ty)) 71 THENC Conv.REWR_CONV not_F_imp) 72 in 73 fn thm => 74 List.foldl (neqs_rule o Lib.uncurry Thm.DISCH) thm (Thm.hyp thm) 75 end 76end 77 78local 79 val flookup_id = Q.prove( 80 `FLOOKUP (fm |+ (a:'a, b)) a = SOME b`, 81 REWRITE_TAC [finite_mapTheory.FLOOKUP_UPDATE] 82 ) 83 val flookup_rest = Q.prove( 84 `a <> x ==> (FLOOKUP (fm |+ (a, b)) x = FLOOKUP fm x)`, 85 SIMP_TAC std_ss [finite_mapTheory.FLOOKUP_UPDATE] 86 ) 87 |> UNDISCH_ALL 88 val updates = List.rev o List.map (fst o pairSyntax.dest_pair) o snd o 89 finite_mapSyntax.strip_fupdate 90 val err = ERR "extend_flookup_thms" "not an extension" 91 fun get_delta tm1 tm2 = 92 let 93 val u1 = updates tm1 94 val u2 = updates tm2 95 val l1 = List.length u1 96 val l2 = List.length u2 97 val d = l2 - l1 98 in 99 if 0 <= d 100 then ( List.drop (u2, d) = u1 orelse raise err 101 ; (List.take (u2, d), u1) ) 102 else raise err 103 end 104 fun get_b rest = 105 let 106 val t = boolSyntax.lhs (Thm.concl rest) 107 in 108 case Lib.total finite_mapSyntax.dest_flookup t of 109 SOME (fmap, _) => fmap 110 | NONE => t 111 end 112 fun is_refl th = 113 case Lib.total boolSyntax.dest_eq (Thm.concl th) of 114 SOME (l, r) => l = r 115 | NONE => false 116in 117 fun extend_flookup_thms (dict, rest) tm = 118 let 119 val base = get_b rest 120 val (dty, rty) = finite_mapSyntax.dest_fmap_ty (Term.type_of base) 121 val (tms, old_tms) = get_delta base tm 122 val inst_ty = Thm.INST_TYPE [alpha |-> dty, beta |-> rty] 123 val flookup_id = inst_ty flookup_id 124 val flookup_rest = inst_ty flookup_rest 125 val id_rule = Conv.RIGHT_CONV_RULE (Conv.REWR_CONV flookup_id) 126 val rule = neqs_rule dty 127 val a = Term.mk_var ("a", dty) 128 val x = Term.mk_var ("x", dty) 129 val th = Thm.REFL (finite_mapSyntax.mk_flookup (tm, x)) 130 val (dict', rest') = 131 List.foldl 132 (fn (t, (d, th)) => 133 (case Lib.total (rule o id_rule o Thm.INST [x |-> t]) th of 134 SOME r => Redblackmap.insert (d, t, r) 135 | NONE => d, 136 Conv.RIGHT_CONV_RULE 137 (Conv.REWR_CONV (Thm.INST [a |-> t] flookup_rest)) th)) 138 (Redblackmap.mkDict Term.compare, th) tms 139 val dict'' = 140 List.foldl 141 (fn (t, d) => 142 case Redblackmap.peek (dict, t) of 143 SOME r => Redblackmap.insert 144 (d, t, 145 (rule o 146 Conv.RIGHT_CONV_RULE (Conv.REWR_CONV r)) 147 (Thm.INST [x |-> t] rest')) 148 | NONE => raise err) dict' old_tms 149 val rest'' = if is_refl rest 150 then rest' 151 else Conv.RIGHT_CONV_RULE (Conv.REWR_CONV rest) rest' 152 in 153 (dict'', rest'') 154 end 155end 156 157val const_name = ref "gen_fmap_" 158val new_const_size = ref 100 159 160(* -------------------------------------------------------------------------- 161 FLOOKUP_DEFN_CONV 162 163 Conversion for term of the form ``FLOOKUP fmap i``. 164 165 Will abbreviate "fmap" when it contains lots of updates. Otherwise it 166 will employ a database to lookup values. 167 168 To activate in the context of EVAL do: 169 170 val () = 171 ( computeLib.del_consts [finite_mapSyntax.flookup_t] 172 ; computeLib.add_convs 173 [(finite_mapSyntax.flookup_t, 2, FLOOKUP_DEFN_CONV)] ) 174 175 -------------------------------------------------------------------------- *) 176 177local 178 val completed_fmap_convs = 179 ref (Redblackmap.mkDict Term.compare: (term, conv) Redblackmap.dict) 180 val head_fmaps = 181 ref (Redblackmap.mkDict Term.compare: 182 (term, (term, thm) Redblackmap.dict * thm) Redblackmap.dict) 183 fun introduce_fmap_consts _ = ALL_CONV 184 val const_number = ref 0 185 val flookup_fallback_conv = 186 Conv.REWR_CONV finite_mapTheory.FLOOKUP_UPDATE 187 ORELSEC Conv.REWR_CONV finite_mapTheory.FLOOKUP_EMPTY 188 val rwts = ref ([] : thm list) 189 val rwt_cnv = ref ALL_CONV 190 val err = ERR "FLOOKUP_DEFN_CONV" "" 191 fun DICT_REST_CONV (dr as (dict, rest)) tm = 192 let 193 val i = snd (finite_mapSyntax.dest_flookup tm) 194 in 195 case Redblackmap.peek (dict, i) of 196 SOME thm => Conv.REWR_CONV thm tm 197 | NONE => let 198 val x = Term.rand (boolSyntax.rhs (Thm.concl rest)) 199 in 200 neqs_rule (Term.type_of x) (Thm.INST [x |-> i] rest) 201 end 202 end 203 fun introduce_fmap_consts (x as (base, _)) = 204 let 205 val ty = Term.type_of base 206 fun new_var () = 207 Term.mk_var (!const_name ^ Int.toString (!const_number), ty) before 208 Portable.inc const_number 209 fun iter a (c, l) = 210 let 211 val r = List.take (l, !new_const_size) 212 val v = new_var() 213 val s = fst (Term.dest_var v) 214 val t = finite_mapSyntax.list_mk_fupdate (c, r) 215 val def = Definition.new_definition (s, boolSyntax.mk_eq (v, t)) 216 val () = print ("Defined " ^ quote s ^ "\n") 217 val sym_def = SYM def 218 val (c', tm) = boolSyntax.dest_eq (Thm.concl def) 219 val (dict, rest) = 220 extend_flookup_thms 221 (Redblackmap.mkDict Term.compare, Thm.REFL c) tm 222 val cnv = Conv.REWR_CONV sym_def 223 val rule = 224 Conv.CONV_RULE 225 (Conv.LAND_CONV (Conv.RATOR_CONV (Conv.RAND_CONV cnv))) 226 val dict = Redblackmap.transform rule dict 227 val rest = rule rest 228 val () = 229 completed_fmap_convs := 230 Redblackmap.insert 231 (!completed_fmap_convs, c', DICT_REST_CONV (dict, rest)) 232 in 233 iter (sym_def :: a) (c', List.drop (l, !new_const_size)) 234 end 235 handle General.Subscript => a 236 val defs = iter [] x 237 in 238 rwts := defs @ (!rwts); rwt_cnv := PURE_REWRITE_CONV (!rwts) 239 end 240in 241 fun FLOOKUP_DEFN_CONV tm = 242 let 243 val fm = Lib.with_exn (fst o finite_mapSyntax.dest_flookup) tm err 244 val (base, ups) = finite_mapSyntax.strip_fupdate fm 245 val n = List.length ups 246 in 247 if not (List.null (Term.free_vars tm)) 248 then flookup_fallback_conv tm 249 else if List.null ups 250 then case Redblackmap.peek (!completed_fmap_convs, base) of 251 SOME cnv => cnv tm 252 | NONE => flookup_fallback_conv tm 253 else if n < !new_const_size 254 then let 255 val dr = 256 case Redblackmap.peek (!head_fmaps, base) of 257 SOME dr => dr 258 | NONE => 259 (Redblackmap.mkDict Term.compare, Thm.REFL base) 260 in 261 case Lib.total (extend_flookup_thms dr) fm of 262 SOME dr' => 263 ( head_fmaps := 264 Redblackmap.insert (!head_fmaps, base, dr') 265 ; DICT_REST_CONV dr' tm 266 ) 267 | NONE => flookup_fallback_conv tm 268 end 269 else Conv.RATOR_CONV (Conv.RAND_CONV (!rwt_cnv)) tm 270 handle Conv.UNCHANGED => 271 ( introduce_fmap_consts (base, ups) 272 ; FLOOKUP_DEFN_CONV ) tm 273 end 274end 275 276end 277 278(* ----------------------------------------------------------------------- *) 279 280(* Testing... 281 282open flookupLib wordsLib 283open flookupLib 284 285val () = 286 ( computeLib.del_consts [finite_mapSyntax.flookup_t] 287 ; computeLib.add_convs [(finite_mapSyntax.flookup_t, 2, FLOOKUP_DEFN_CONV)] ) 288 289val fempty_tm = 290 Term.inst [alpha |-> numSyntax.num, beta |-> numSyntax.num] 291 finite_mapSyntax.fempty_t 292 293fun mk_fmap t b n = 294 finite_mapSyntax.list_mk_fupdate 295 (t, List.tabulate 296 (n, fn i => let 297 val j = numLib.term_of_int (b + i) 298 in 299 pairSyntax.mk_pair (j, j) 300 end)) 301 302Count.apply EVAL ``FLOOKUP (FEMPTY |+ (a, 1)) a`` 303 304Count.apply EVAL ``FLOOKUP ^(mk_fmap fempty_tm 0 1000) 999`` 305 306Count.apply EVAL ``FLOOKUP gen_fmap_0 44`` 307Count.apply EVAL ``FLOOKUP (gen_fmap_0 |+ (1000, 1000)) 44`` 308Count.apply EVAL ``FLOOKUP (gen_fmap_0 |+ (44, 45)) 44`` 309Count.apply EVAL ``FLOOKUP gen_fmap_1 99`` 310Count.apply EVAL ``FLOOKUP gen_fmap_9 99`` 311Count.apply EVAL ``FLOOKUP gen_fmap_9 901`` 312Count.apply EVAL ``FLOOKUP gen_fmap_9 801`` 313 314val () = Hol_datatype `enum = One | Two | Three | Four | Five` 315 316val () = Hol_datatype` 317 data = Num of num 318 | String of string 319 | Word of word32 320 | Enum of enum 321 | Other1 322 | Other2` 323 324val dict2_def = Define `dict2 = ^(mk_fmap fempty_tm 0 1000)` 325val dict3_def = Define `dict3 = ^(mk_fmap ``dict2`` 1000 400)` 326val dict4_def = Define `dict4 = FEMPTY |+ (1, 1) |+ (2, 2) |+ (2, 3)` 327val dict5_def = Define` 328 dict5 = 329 FEMPTY |+ (Num 1, 1) 330 |+ (String "s", 2) 331 |+ (Other1, 3) 332 |+ (Other2, 4) 333 |+ (Num 2, 1) 334 |+ (Enum One, 5) 335 |+ (Enum Two, 6) 336 |+ (Word 32w, 7) 337 |+ (Word 31w, 8)` 338 339val d2_conv = Count.apply FLOOKUP_DEFN_CONV dict2_def 340val d3_conv = Count.apply FLOOKUP_DEFN_CONV dict3_def 341val d4_conv = Count.apply FLOOKUP_DEFN_CONV dict4_def 342val d5_conv = Count.apply FLOOKUP_DEFN_CONV dict5_def 343 344Count.apply d3_conv ``FLOOKUP dict3 1``; 345Count.apply d3_conv ``FLOOKUP dict3 1000``; 346Count.apply d4_conv ``FLOOKUP dict4 1``; 347Count.apply d5_conv ``FLOOKUP dict5 (Num 1)``; 348 349*) 350