1(*===================================================================== *) 2(* FILE : quantHeuristicsLibParameters.sml *) 3(* DESCRIPTION : some code to find instantations for quantified *) 4(* variables *) 5(* *) 6(* AUTHORS : Thomas Tuerk *) 7(* DATE : December 2008 *) 8(* ===================================================================== *) 9 10 11structure quantHeuristicsLibParameters :> quantHeuristicsLibParameters = 12struct 13 14(* 15quietdec := true; 16loadPath := 17 (concat [Globals.HOLDIR, "/src/quantHeuristics"]):: 18 !loadPath; 19 20map load ["quantHeuristicsTheory"]; 21load "ConseqConv" 22show_assums := true; 23quietdec := true; 24*) 25 26open HolKernel Parse boolLib Drule ConseqConv quantHeuristicsLibBase 27open rich_listTheory quantHeuristicsTheory 28 29(* 30quietdec := false; 31*) 32 33 34(* quantHeuristicsLib contains the core functionality to eliminate 35 quantifiers. However the heuristics contained in this lib are just 36 concerned with equations and basic boolean expressions. This 37 file contains heuristics for common construcs like lists, pairs, 38 option-types, etc. 39*) 40 41 42 43(******************************************************************* 44 * Pairs 45 *******************************************************************) 46 47 48(* val v = ``x:('a # 'b)``; 49 val fv = [``y:'a``]:term list; 50 val t = ``FST (x:('a # 'b)) = y`` 51 fun P v (t:term) = SOME (enumerate_pair true v) 52 val given = ["aaaa"] 53 *) 54 55fun enumerate_pair do_rec v = 56if not ((can pairSyntax.dest_prod) (type_of v)) then v else 57let 58 val (vn,vt) = dest_var v 59 val tL = pairSyntax.spine_prod vt; 60 61 val ntL = enumerate 1 tL 62 val vars = map (fn (n, ty) => (mk_var (vn^"_"^(Int.toString n), ty))) ntL 63 val vars' = if do_rec then (map (enumerate_pair do_rec) vars) else vars 64 val p = (pairSyntax.list_mk_pair vars') 65in 66 p 67end; 68 69val GUESS_PAIR_THM = prove ( 70``!P (i:'b -> 'a). (!v. ?x. v = i x) ==> 71 (GUESS_EXISTS_GAP i P /\ GUESS_FORALL_GAP i P)``, 72simpLib.SIMP_TAC numLib.std_ss [GUESS_REWRITES]) 73 74 75fun QUANT_INSTANTIATE_HEURISTIC___SPLIT_PAIR_GEN PL (sys:quant_heuristic_base) v t = 76let 77 (*check whether something should be done*) 78 val _ = pairSyntax.dest_prod (type_of v) handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 79 80 fun P v t = first_opt (fn x => fn p => (p v t)) PL 81 val vars = case (P v t) of NONE => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 82 | some => valOf some; 83 val fvL = rev (free_vars vars) 84 85 val ip = pairLib.mk_pabs (pairLib.list_mk_pair fvL, vars); 86 val ip' = rhs (concl ((pairTools.PABS_ELIM_CONV ip) handle UNCHANGED => REFL ip)); 87 88 val gthm = ISPECL[mk_abs (v, t), ip'] GUESS_PAIR_THM 89 val pre = rand (rator (concl gthm)) 90 val pre_thm = prove (pre, 91 simpLib.SIMP_TAC numLib.std_ss [ 92 pairTheory.EXISTS_PROD, pairTheory.FORALL_PROD]) 93 val gthmL = BODY_CONJUNCTS (MP gthm pre_thm) 94in 95 {rewrites = [], 96 general = [], 97 exists_point = [], 98 forall_point = [], 99 forall = [], 100 exists = [], 101 forall_gap = [guess_thm (gty_forall_gap, vars, fvL, el 2 gthmL)], 102 exists_gap = [guess_thm (gty_exists_gap, vars, fvL, el 1 gthmL)]} 103end; 104 105 106fun split_pair___FST_SND___pred depth_split v t = 107let 108 val t1 = pairSyntax.mk_fst v; 109 val t2 = pairSyntax.mk_snd v; 110 111 val do_split = not (null (find_terms (fn t' => (t' = t1) orelse (t' = t2)) t)) 112in 113 if do_split then (SOME (enumerate_pair depth_split v)) else NONE 114end; 115 116 117(* val v = ``x:('a # 'b # 'c)``; 118 val t = ``(\ (a,b,c). P a b c) ^v`` 119 *) 120local 121 fun is_var_pabs v t = 122 let 123 val (b,v') = dest_comb t; 124 in 125 (v = v') andalso (pairSyntax.is_pabs b) 126 end handle HOL_ERR _ => false; 127in 128 129fun split_pair___PABS___pred v t = 130let 131 val p = hd (find_terms (is_var_pabs v) t); 132 val vars = fst (pairSyntax.dest_pabs (fst (dest_comb p))) 133in 134 (SOME vars) 135end handle Empty => NONE 136 | HOL_ERR _ => NONE; 137end; 138 139 140fun split_pair___ALL___pred v = K (SOME (enumerate_pair true v)); 141 142 143 144(* val v = ``x:('a # 'b # 'c)`` 145 val fv = []:term list; 146 val t = ``(\ (a1, a2, a3). P a1 a2 a3) (x:('a # 'b # 'c))`` 147 *) 148 149fun pair_qp pL = combine_qps 150 [rewrite_qp [PAIR_EQ_EXPAND, pairTheory.FST, pairTheory.SND], 151 heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___SPLIT_PAIR_GEN pL], 152 final_rewrite_qp [pairTheory.FST, pairTheory.SND, PAIR_EQ_SIMPLE_EXPAND]] 153 154val pair_default_qp = pair_qp [split_pair___PABS___pred, 155 split_pair___FST_SND___pred false] 156 157val pair_ty_filter = type_match_filter [``:('a # 'b)``] 158 159(* 160val PAIR_QUANT_INSTANTIATE_CONV = QUANT_INSTANTIATE_CONV [pair_default_qp] 161 162val t = ``?p. (x = FST p) /\ Q p``; 163val thm = PAIR_QUANT_INSTANTIATE_CONV t; 164 165val t = ``?p. (7 = (SND p)) /\ Q p`` 166val thm = PAIR_QUANT_INSTANTIATE_CONV t; 167 168val t = ``?p1 p2. (p1 = 7) /\ Q (p1,p2)`` 169val thm = PAIR_QUANT_INSTANTIATE_CONV t 170 171 172val t = ``?v. (v,X) = Z`` 173val thm = PAIR_QUANT_INSTANTIATE_CONV t; 174 175val t = ``!x. a /\ (\ (a1, t3, a2). P a1 a2 t3) x /\ b x`` 176val thm = PAIR_QUANT_INSTANTIATE_CONV t 177 178val t = ``?x. (x = 2) /\ P x``; 179val thm = PAIR_QUANT_INSTANTIATE_CONV t 180 181val t = ``!x. ((f t = x) /\ P x) ==> Q x``; 182val thm = PAIR_QUANT_INSTANTIATE_CONV t 183 184val t = ``?v. (v,X) = (a,9)``; 185val thm = PAIR_QUANT_INSTANTIATE_CONV t 186 187*) 188 189 190val stateful_qp = quantHeuristicsLibBase.stateful_qp; 191val pure_stateful_qp = quantHeuristicsLibBase.pure_stateful_qp; 192val TypeBase_qp = quantHeuristicsLibBase.TypeBase_qp; 193 194 195(******************************************************************* 196 * Option types 197 *******************************************************************) 198 199val option_qp = combine_qps [ 200 distinct_qp [optionTheory.NOT_NONE_SOME], 201 202 cases_qp [optionTheory.option_nchotomy], 203 204 rewrite_qp [optionTheory.SOME_11, optionTheory.IS_NONE_EQ_NONE, 205 optionTheory.IS_NONE_EQ_NONE, 206 IS_SOME_EQ_NOT_NONE], 207 208 final_rewrite_qp [optionTheory.option_CLAUSES] 209 ] 210 211val option_ty_filter = type_match_filter [``:'a option``] 212 213 214(******************************************************************* 215 * Sum types 216 *******************************************************************) 217 218val sum_qp = combine_qps [ 219 get_qp___for_types [``:('a + 'b)``], 220 cases_qp [sumTheory.ISL_OR_ISR], 221 rewrite_qp [ISL_exists, ISR_exists, sumTheory.NOT_ISR_ISL, sumTheory.NOT_ISL_ISR, INL_NEQ_ELIM, INR_NEQ_ELIM], 222 223 final_rewrite_qp [sumTheory.OUTR, sumTheory.OUTL, sumTheory.ISL, sumTheory.ISR, sumTheory.INR_INL_11] 224] 225 226val sum_ty_filter = type_match_filter [``:('a + 'b)``] 227 228 229(******************************************************************* 230 * Nums 231 *******************************************************************) 232 233val num_qp = combine_qps [ 234 distinct_qp [prim_recTheory.SUC_ID], 235 236 cases_qp [arithmeticTheory.num_CASES], 237 238 rewrite_qp [prim_recTheory.INV_SUC_EQ, 239 arithmeticTheory.EQ_ADD_RCANCEL,arithmeticTheory.EQ_ADD_LCANCEL, 240 arithmeticTheory.ADD_CLAUSES], 241 242 final_rewrite_qp [numTheory.NOT_SUC, GSYM numTheory.NOT_SUC] 243] 244 245val num_ty_filter = type_filter [``:num``] 246 247 248(******************************************************************* 249 * Lists 250 *******************************************************************) 251 252 253val list_no_len_qp = combine_qps [ 254 distinct_qp [rich_listTheory.NOT_CONS_NIL], 255 256 cases_qp [listTheory.list_CASES], 257 258 rewrite_qp [listTheory.CONS_11, 259 listTheory.NULL_EQ, 260 listTheory.APPEND_11, 261 listTheory.APPEND_eq_NIL], 262 263 final_rewrite_qp [listTheory.NULL_DEF, 264 listTheory.TL, listTheory.HD, 265 rich_listTheory.NOT_CONS_NIL, 266 GSYM rich_listTheory.NOT_CONS_NIL] 267] 268 269val list_qp = combine_qp (rewrite_qp [LIST_LENGTH_COMPARE_SUC, 270 LIST_LENGTH_1]) list_no_len_qp; 271 272val list_len_qp = combine_qp (rewrite_qp [LIST_LENGTH_COMPARE_SUC, 273 LIST_LENGTH_20]) list_no_len_qp; 274 275val list_ty_filter = type_match_filter [``:'a list``] 276 277 278(******************************************************************* 279 * Records 280 *******************************************************************) 281 282fun get_record_type_rewrites ty = 283let 284 fun type_rewrites ty = 285 let 286 val ty_info = valOf (TypeBase.fetch ty) 287 val (thyname,typename) = TypeBasePure.ty_name_of ty_info 288 in 289 if null (TypeBasePure.fields_of ty_info) then [] else 290 (map (fn s => (DB.fetch thyname (typename^"_"^(fst s)))) 291 (TypeBasePure.fields_of ty_info)) @ 292 (map (fn s => (DB.fetch thyname (typename^s))) [ 293 "_fupdfupds_comp", "_accessors", "_fn_updates", 294 "_literal_11", "_component_equality", 295 "_accfupds"])@ 296 ((valOf (TypeBasePure.one_one_of ty_info)):: 297 ((TypeBasePure.case_def_of ty_info):: 298 ((TypeBasePure.accessors_of ty_info)@(TypeBasePure.updates_of ty_info)))) 299 end; 300 301 val constructor = hd (TypeBase.constructors_of ty) 302 val (typ, types) = let 303 fun domtys acc ty = let 304 val (d1, rty) = dom_rng ty 305 in 306 domtys (d1::acc) rty 307 end handle HOL_ERR _ => (ty, List.rev acc) 308 in 309 domtys [] (type_of constructor) 310 end 311in 312 [combinTheory.K_THM, combinTheory.o_THM]@ 313 (flatten (map type_rewrites (typ::types))) 314end; 315 316 317(* 318 319Hol_datatype `my_record = <| field1 : bool ; 320 field2 : num ; 321 field3 : bool |>` 322 323val do_rewrites = false 324fun P v t = true 325 326val v = ``r1:my_record`` 327val t = ``r1.field1`` 328 329*) 330 331fun QUANT_INSTANTIATE_HEURISTIC___RECORDS do_rewrites P sys v t = 332let 333 (*check whether something should be done*) 334 val v_info = case TypeBase.fetch (type_of v) of NONE => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 335 | SOME x => x 336 val _ = if null (TypeBasePure.fields_of v_info) orelse not (P v t) then 337 raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else () 338 val (thyname,typename) = TypeBasePure.ty_name_of v_info 339 340 val vars = let 341 val (v_name,_) = dest_var v 342 fun mk_new_var (s, ty) = mk_var (s, ty); 343 in 344 map mk_new_var (TypeBasePure.fields_of v_info) 345 end; 346 347 val thm0 = 348 let 349 val xthm0 = DB.fetch thyname (typename^"_literal_nchotomy") 350 val xthm1 = CONV_RULE (RENAME_VARS_CONV (map (fst o dest_var) (v :: vars))) xthm0 351 in xthm1 352 end; 353 val gc = QUANT_INSTANTIATE_HEURISTIC___one_case thm0 sys v t 354in 355 if do_rewrites then 356 (guess_collection_append gc 357 (guess_list2collection (get_record_type_rewrites (type_of v), []))) 358 else gc 359end 360 361fun record_qp do_rewrites P = heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___RECORDS do_rewrites P]; 362 363 364val record_default_qp = record_qp false (K (K true)) 365 366(******************************************************************* 367 * Heuristic for implications that considers just the right hand side 368 * and conjunctions that just assume everything 369 *******************************************************************) 370 371(* 372 val v = ``x:num`` 373 val t = ``Q x ==> (x = 2) /\ P x`` 374 val sys = debug_sys 375*) 376fun QUANT_INSTANTIATE_HEURISTIC___DEST_HEU dest sys v t = 377let 378 val tL = dest t; 379 380 (* get guesses form right hand side *) 381 val gcL = map (fn t => SOME (sys v t) handle HOL_ERR _ => NONE 382 | QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE) tL 383 val gc = guess_collection_flatten gcL 384 val (rw_thms, gL) = guess_collection2list gc 385 386 (* just assume without justification that these are valid guesses for the full implication, 387 this might be wrong! *) 388 fun guess_lift g = let 389 val (i, fvL) = guess_extract g 390 val ty_opt = guess_extract_type g 391 val g' = mk_guess_opt ty_opt v t i fvL 392 in g' end 393 val gL' = map guess_lift gL 394in 395 guess_list2collection (rw_thms, gL') 396end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp 397 398fun dest_lift_qp dest = heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___DEST_HEU dest] 399 400val implication_concl_qp = dest_lift_qp (fn t => [snd (dest_imp_only t)]) 401val conj_lift_qp = dest_lift_qp (fn t => (let val (t1,t2) = dest_conj t in [t1, t2] end)) 402 403 404(******************************************************************* 405 * Combinations 406 *******************************************************************) 407 408val std_qps = [num_qp, option_qp, pair_default_qp, list_qp, sum_qp, record_default_qp] 409 410val no_ctxt_std_qp = combine_qps std_qps 411val direct_ctxt_std_qp = combine_qps (std_qps @ [direct_context_qp]) 412val std_qp = combine_qps (std_qps @ [context_qp]) 413 414 415 416end 417