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