1(* non-interactive mode 2*) 3structure ho_basicTools :> ho_basicTools = 4struct 5open HolKernel Parse boolLib; 6 7(* interactive mode 8val () = loadPath := union ["..", "../finished"] (!loadPath); 9val () = app load 10 ["bossLib", 11 "realLib", 12 "rich_listTheory", 13 "arithmeticTheory", 14 "numTheory", 15 "pred_setTheory", 16 "pairTheory", 17 "combinTheory", 18 "listTheory", 19 "dividesTheory", 20 "primeTheory", 21 "gcdTheory", 22 "probLib", 23 "hoTools"]; 24val () = show_assums := true; 25 26*) 27 28open hurdUtils; 29 30infixr 0 ## 31 32(* ------------------------------------------------------------------------- *) 33(* Debugging. *) 34(* ------------------------------------------------------------------------- *) 35 36val trace_level = ref 0; 37val _ = Feedback.register_trace ("ho_basicTools", trace_level, 10); 38fun trace l s = if l > !trace_level then () else say (s ^ "\n"); 39fun trace_x l s f x = 40 if l > !trace_level then () else say (s ^ ":\n" ^ f x ^ "\n"); 41fun trace_CONV l s tm = (trace_x l s term_to_string tm; QCONV ALL_CONV tm); 42 43(* ------------------------------------------------------------------------- *) 44(* Type/term substitutions *) 45(* ------------------------------------------------------------------------- *) 46 47val empty_raw_subst : raw_substitution = (([], empty_tmset), ([], [])); 48 49fun raw_match' tm1 tm2 ((tmS, tmIds), (tyS, tyIds)) = 50 raw_match tyIds tmIds tm1 tm2 (tmS, tyS); 51 52fun type_raw_match ty1 ty2 (sub : raw_substitution) = 53 let 54 val tm1 = mk_const ("NIL", mk_type ("list", [ty1])) 55 val tm2 = mk_const ("NIL", mk_type ("list", [ty2])) 56 in 57 raw_match' tm1 tm2 sub 58 end; 59 60val finalize_subst : raw_substitution -> substitution = norm_subst; 61 62(* ------------------------------------------------------------------------- *) 63(* Higher-order matching. *) 64(* ------------------------------------------------------------------------- *) 65 66fun dest_ho_pat bvs tm = 67 if is_var tm andalso not (is_bv bvs tm) then 68 (tm, []) 69 else 70 let 71 val (a, b) = dest_comb tm 72 val bi = dest_bv bvs b 73 in 74 (I ## cons bi) (dest_ho_pat bvs a) 75 end; 76fun is_ho_pat bvs = can (dest_ho_pat bvs); 77fun mk_ho_pat bvs (var, []) = var 78 | mk_ho_pat bvs (var, b::bs) = 79 mk_comb (mk_ho_pat bvs (var, bs), mk_bv bvs b); 80 81local 82 fun beta [] tm = (tm, fn () => REFL tm) 83 | beta (v::vs) tm = 84 let 85 val tm_abs = mk_abs (v, tm) 86 val (match_tm, th1) = beta vs tm_abs 87 in 88 (match_tm, 89 fn () => 90 TRANS (MK_COMB (th1 (), REFL v)) (QCONV BETA_CONV (mk_comb (tm_abs, v)))) 91 end 92 93 fun eta_beta [] tm = (tm, fn () => REFL tm) 94 | eta_beta (v::vs) tm = 95 let 96 val body = eta_conv (mk_abs (v, tm)) 97 val (match_tm, th) = eta_beta vs body 98 in 99 (match_tm, fn () => MK_COMB (th (), REFL v)) 100 end 101 handle HOL_ERR _ => beta (v::vs) tm 102in 103 fun ho_pat_match bvs pat_bvs tm = 104 let 105 val tm_bvs = filter (is_bv bvs) (free_vars tm) 106 val _ = assert (forall (is_bv pat_bvs) tm_bvs) 107 (ERR "ho_pat_match" "var pattern doesn't have all bound vars used") 108 in 109 eta_beta pat_bvs tm 110 end 111 112 fun ho_raw_match (var, bs) (bvs, tm) sub = 113 let 114 val var_bvs = map (mk_bv bvs) bs 115 in 116 (C (raw_match' var) sub ## I) (ho_pat_match bvs var_bvs tm) 117 end 118end; 119 120local 121 fun check_off_bvs _ tm [] = tm 122 | check_off_bvs bvs tm (b :: bs) = 123 let 124 val (a, v) = dest_comb tm 125 val _ = assert (dest_bv bvs v = b) (ERR "fo_pat_match" "wrong bound vars") 126 in 127 check_off_bvs bvs a bs 128 end 129in 130 fun fo_raw_match (var, bs) (bvs, tm) sub = 131 let 132 val body = check_off_bvs bvs tm bs 133 val bvfvs = listset bvs Isct FVs body 134 val _ = assert (HOLset.isEmpty bvfvs) 135 (ERR "fo_pat_match" "term to be matched contains bound vars") 136 in 137 raw_match' var body sub 138 end; 139end; 140 141local 142 fun match (bvs, tm) (bvs', tm') sub = 143 if is_bv bvs tm then 144 let 145 val _ = assert (dest_bv bvs tm = dest_bv bvs' tm') 146 (ERR "ho_match" "bound var in pattern does not match") 147 in 148 (sub, fn () => REFL tm') 149 end 150 else if is_ho_pat bvs tm then 151 ho_raw_match (dest_ho_pat bvs tm) (bvs', tm') sub 152 else 153 (case Df dest_term (tm, tm') of 154 (COMB (Rator, Rand), COMB (Rator', Rand')) => 155 let 156 val (sub', rator_th) = match (bvs, Rator) (bvs', Rator') sub 157 val (sub'', rand_th) = match (bvs, Rand) (bvs', Rand') sub' 158 in 159 (sub'', fn () => MK_COMB (rator_th (), rand_th ())) 160 end 161 | (LAMB (Bvar, Body), LAMB (Bvar', Body')) => 162 let 163 val sub' = type_raw_match (type_of Bvar) (type_of Bvar') sub 164 val (sub'', thk) = match (Bvar::bvs, Body) (Bvar'::bvs', Body') sub' 165 in 166 (sub'', fn () => MK_ABS (GEN Bvar' (thk ()))) 167 end 168 | (CONST _, CONST _) 169 => (raw_match' tm tm' sub, fn () => REFL tm') 170 | (VAR _, _) 171 => raise BUG "ho_match" "var in pattern shouldn't be possible" 172 | _ => raise ERR "ho_match" "fundamentally different terms") 173in 174 fun ho_match_bvs (bvs, tm) (bvs', tm') : ho_substitution = 175 (finalize_subst ## (fn thk => fn () => SYM (thk ()))) 176 (match (bvs, tm) (bvs', tm') empty_raw_subst) 177 178 fun ho_match tm tm' : ho_substitution = ho_match_bvs ([], tm) ([], tm') 179end; 180 181fun var_ho_match_bvs vars (bvs, tm) (bvs', tm') = 182 let 183 val ho_sub as (sub, _) = ho_match_bvs (bvs, tm) (bvs', tm') 184 val _ = assert (subst_vars_in_set sub vars) 185 (ERR "var_ho_match_bvs" "subst vars not contained in set") 186 in 187 ho_sub 188 end; 189 190fun var_ho_match vars tm tm' = var_ho_match_bvs vars ([], tm) ([], tm'); 191 192(* 193val tm = ``\(x : num). f``; 194val tm' = ``\(n : num). T``; 195val (sub, th) = try (ho_match tm) tm'; 196 197val tm = ``!x y. f x y``; 198val tm' = ``!a b. f a a b``; 199val (sub, th) = try (ho_match tm) tm'; 200pinst sub tm; 201REWR_CONV (th ()) tm'; 202 203val tm = ``!x y z. f x z``; 204val tm' = ``!a b c. P (f a c) (g a)``; 205val (sub, th) = try (ho_match tm) tm'; 206pinst sub tm; 207REWR_CONV (th ()) tm'; 208 209val tm = ``\ (v : 'a). a v (b v)``; 210val tm' = ``\ (y : 'a). f y``; 211val (sub, th) = try (ho_match tm) tm'; 212pinst sub tm; 213REWR_CONV (th ()) tm'; 214 215val tm = ``\ (v : 'a). v``; 216val tm' = ``\ (y : 'b). y``; 217val (sub, th) = try (ho_match tm) tm'; 218pinst sub tm; 219REWR_CONV (th ()) tm'; 220*) 221 222(* ------------------------------------------------------------------------- *) 223(* Higher-order rewriting. *) 224(* ------------------------------------------------------------------------- *) 225 226(* Normal rewriting *) 227 228fun ho_subst_REWR th (sub, thk) = TRANS (thk ()) (PINST sub th); 229 230fun ho_REWR_CONV th = 231 let 232 val (vars, th') = thm_to_vthm th 233 val pat = LHS th' 234 in 235 ho_subst_REWR th' o var_ho_match vars pat 236 end; 237 238fun ho_REWRITE_CONV ths = QCONV (TOP_DEPTH_CONV (FIRSTC (map ho_REWR_CONV ths))); 239 240fun ho_REWRITE_TAC ths = CONV_TAC (ho_REWRITE_CONV ths); 241 242(* Conditional rewriting, pass in a prover *) 243 244fun ho_subst_COND_REWR th = 245 let 246 val (cond, _) = (dest_imp o concl) th 247 in 248 fn prover => fn (sub, thk) => 249 let 250 val goal = pinst sub cond 251 val _ = trace_x 2 "ho_subst_COND_REWR: goal" term_to_string goal 252 val proved_cond = prover goal 253 in 254 TRANS (thk ()) (MP (PINST sub th) proved_cond) 255 handle h as HOL_ERR _ => raise err_BUG 256 ("ho_subst_COND_REWR: using crw\n" ^ thm_to_string th ^ 257 "\nand proved_cond\n" ^ thm_to_string proved_cond) h 258 end 259 end; 260 261fun ho_COND_REWR_CONV th = 262 let 263 val (vars, th') = thm_to_vthm th 264 val pat = (lhs o snd o dest_imp o concl) th' 265 val f = ho_subst_COND_REWR th' 266 in 267 fn prover => f prover o var_ho_match vars pat 268 end; 269 270(* non-interactive mode 271*) 272end; 273