1(*--------------------------------------------------------------------------- 2 Raising basic lambda calculus conversions to handle pairs 3 ---------------------------------------------------------------------------*) 4 5structure PairedLambda :> PairedLambda = 6struct 7 8open HolKernel boolLib pairTheory pairSyntax; 9 10val ERR = mk_HOL_ERR "PairedLambda"; 11 12fun is_uncurry_tm c = same_const uncurry_tm c; 13fun is_uncurry x = is_uncurry_tm (rator x) handle HOL_ERR _ => false; 14 15(* ---------------------------------------------------------------------*) 16(* PAIRED_BETA_CONV: Generalized beta conversions for tupled lambda *) 17(* abstractions applied to tuples (i.e. redexes) *) 18(* *) 19(* Given the term: *) 20(* *) 21(* "(\(x1, ... ,xn).t) (t1, ... ,tn)" *) 22(* *) 23(* PAIRED_BETA_CONV proves that: *) 24(* *) 25(* |- (\(x1, ... ,xn).t) (t1, ... ,tn) = t[t1, ... ,tn/x1, ... ,xn] *) 26(* *) 27(* where t[t1,...,tn/x1,...,xn] is the result of substituting ti for xi *) 28(* in parallel in t, with suitable renaming of variables to prevent *) 29(* free variables in t1,...,tn becoming bound in the result. *) 30(* *) 31(* The conversion works for arbitrarily nested tuples. For example: *) 32(* *) 33(* PAIRED_BETA_CONV "(\((a,b),(c,d)).t) ((1,2),(3,4))" *) 34(* *) 35(* gives: *) 36(* *) 37(* |- (\((a,b),(c,d)).t) ((1,2),(3,4)) = t[1,2,3,4/a,b,c,d] *) 38(* *) 39(* Bugfix: INST used instead of SPEC to avoid priming. [TFM 91.04.17]*) 40(* ---------------------------------------------------------------------*) 41 42 43val PAIRED_BETA_CONV = pairTheory.PAIRED_BETA_CONV; 44 45 46(*-------------------------------------------------------*) 47(* PAIRED_ETA_CONV "\(x1,.(..).,xn). P (x1,.(..).,xn)" = *) 48(* |- \(x1,.(..).,xn). P (x1,.(..).,xn) = P *) 49(* [JRH 91.07.17] *) 50(*-------------------------------------------------------*) 51 52local val pthm = GEN_ALL (SYM (SPEC_ALL pairTheory.PAIR)) 53 fun pairify tm = 54 let val step = ISPEC tm pthm 55 val (Rator,r) = dest_comb (rhs (concl step)) 56 val (pop,l) = dest_comb Rator 57 in 58 TRANS step (MK_COMB(AP_TERM pop (pairify l), pairify r)) 59 end 60 handle HOL_ERR _ => REFL tm 61in 62fun PAIRED_ETA_CONV tm = 63 let val (varstruct,body) = dest_pabs tm 64 val (f,Rand) = dest_comb body 65 val _ = assert (aconv varstruct) Rand 66 val xv = mk_var("x", type_of varstruct) 67 val peq = pairify xv 68 val par = rhs (concl peq) 69 val bth = PAIRED_BETA_CONV (mk_comb(tm, par)) 70 in 71 EXT (GEN xv (SUBS [SYM peq] bth)) 72 end 73 handle HOL_ERR {message, ...} => raise ERR "PAIRED_ETA_CONV" message 74end; 75 76(*--------------------------------------------------------------------*) 77(* GEN_BETA_CONV - reduces single or paired abstractions, introducing *) 78(* arbitrarily nested "FST" and "SND" if the rand is not sufficiently *) 79(* paired. Example: *) 80(* *) 81(* #GEN_BETA_CONV "(\(x,y). x + y) numpair"; *) 82(* |- (\(x,y). x + y)numpair = (FST numpair) + (SND numpair) *) 83(* [JRH 91.07.17] *) 84(*--------------------------------------------------------------------*) 85 86local val pair = CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) pairTheory.PAIR 87 val uncth = SPEC_ALL pairTheory.UNCURRY_DEF 88in 89val GEN_BETA_CONV = 90 let fun gbc tm = 91 let val (abst,arg) = dest_comb tm 92 in if Term.is_abs abst 93 then BETA_CONV tm 94 else let val _ = assert is_uncurry abst 95 val eqv = if can dest_pair arg then REFL arg else ISPEC arg pair 96 val _ = dest_pair (rhs (concl eqv)) 97 val res = AP_TERM abst eqv 98 val rt0 = TRANS res (PART_MATCH lhs uncth (rhs (concl res))) 99 val (tm1a,tm1b) = dest_comb (rhs (concl rt0)) 100 val rt1 = AP_THM (gbc tm1a) tm1b 101 val rt2 = gbc (rhs (concl rt1)) 102 in 103 TRANS rt0 (TRANS rt1 rt2) 104 end 105 end 106 in 107 fn tm => gbc tm handle HOL_ERR _ => raise ERR "GEN_BETA_CONV" "" 108 end 109end; 110 111 112val GEN_BETA_RULE = CONV_RULE (DEPTH_CONV GEN_BETA_CONV) 113val GEN_BETA_TAC = CONV_TAC (DEPTH_CONV GEN_BETA_CONV) 114 115 116(*--------------------------------------------------------------------------- 117 Let reduction 118 ---------------------------------------------------------------------------*) 119 120(* ---------------------------------------------------------------------*) 121(* Internal function: ITER_BETA_CONV (iterated, tupled beta-conversion).*) 122(* *) 123(* The conversion ITER_BETA_CONV reduces terms of the form: *) 124(* *) 125(* (\v1 v2...vn.tm) x1 x2 ... xn xn+1 ... xn+i *) 126(* *) 127(* where the v's can be varstructs. The behaviour is similar to *) 128(* LIST_BETA_CONV, but this function also does paired abstractions. *) 129(* ---------------------------------------------------------------------*) 130 131fun ITER_BETA_CONV tm = 132 let 133 val (Rator, Rand) = dest_comb tm 134 val thm = AP_THM (ITER_BETA_CONV Rator) Rand 135 val redex = rand (concl thm) 136 val red = TRY_CONV (BETA_CONV ORELSEC PAIRED_BETA_CONV) redex 137 in 138 TRANS thm red 139 end 140 handle HOL_ERR _ => REFL tm 141 142(* ---------------------------------------------------------------------*) 143(* Internal function: ARGS_CONV (apply a list of conversions to the *) 144(* arguments of a curried function application). *) 145(* *) 146(* ARGS_CONV [conv1;...;convn] "f a1 ... an" applies convi to ai. *) 147(* ---------------------------------------------------------------------*) 148 149local 150 fun appl [] [] = [] 151 | appl (f :: frst) (a :: arest) = f a :: appl frst arest 152 | appl _ _ = raise ERR "ARGS_CONV" "appl" 153in 154 fun ARGS_CONV cs tm = 155 let 156 val (f,ths) = (I ## appl cs) (strip_comb tm) 157 in 158 rev_itlist (C (curry MK_COMB)) ths (REFL f) 159 end 160end 161 162(* ---------------------------------------------------------------------*) 163(* Internal function RED_WHERE. *) 164(* *) 165(* Given the arguments "f" and "tm[f]", this function produces a *) 166(* conversion that will apply ITER_BETA_CONV to its argument at all *) 167(* subterms that correspond to occurrences of f (bottom-up). *) 168(* ---------------------------------------------------------------------*) 169 170fun RED_WHERE fnn body = 171 if is_var body orelse is_const body 172 then REFL 173 else let 174 val (_, Body) = Term.dest_abs body 175 in 176 ABS_CONV (RED_WHERE fnn Body) 177 end 178 handle HOL_ERR _ => 179 let 180 val (f, args) = strip_comb body 181 in 182 if aconv f fnn then 183 ARGS_CONV (map (RED_WHERE fnn) args) THENC ITER_BETA_CONV 184 else let 185 val (Rator,Rand) = dest_comb body 186 in 187 RAND_CONV (RED_WHERE fnn Rand) 188 THENC RATOR_CONV (RED_WHERE fnn Rator) 189 end 190 end 191 192(* ---------------------------------------------------------------------*) 193(* Internal function: REDUCE *) 194(* *) 195(* This function does the appropriate beta-reductions in the result of *) 196(* expanding a let-term. For terms of the form: *) 197(* *) 198(* "let f x1 ... xn = t in tm[f]" *) 199(* *) 200(* we have that: *) 201(* *) 202(* th |- <let term> = tm[\x1 ... xn. t/f] *) 203(* *) 204(* And the arguments x and f will be: *) 205(* *) 206(* x = \x1 ... xn. t *) 207(* f = \f. tm[f] *) 208(* *) 209(* REDUCE searches in tm[f] for places in which f occurs, and then does *) 210(* an iterated beta-reduction (possibly of varstruct-abstractions) in *) 211(* the right-hand side of the input theorem th, at the places that *) 212(* correspond to occurrences of f in tm[f]. *) 213(* ---------------------------------------------------------------------*) 214 215fun REDUCE f x th = 216 if not (is_abs x orelse pairSyntax.is_uncurry x) then th 217 else let 218 val (Bvar, Body) = Term.dest_abs f 219 in 220 CONV_RULE (RAND_CONV (RED_WHERE Bvar Body)) th 221 end 222 223(* ---------------------------------------------------------------------*) 224(* let_CONV: conversion for reducing "let" terms. *) 225(* *) 226(* Given a term: *) 227(* *) 228(* "let v1 = x1 and ... and vn = xn in tm[v1,...,vn]" *) 229(* *) 230(* let_CONV proves that: *) 231(* *) 232(* |- let v1 = x1 and ... and vn = xn in tm[v1,...,vn] *) 233(* = *) 234(* tm[x1,...,xn/v1,...,vn] *) 235(* *) 236(* where t[t1,...,tn/x1,...,xn] is the result of "substituting" the *) 237(* value xi for vi in parallel in tm (see below). *) 238(* *) 239(* Note that the vi's can take any one of the following forms: *) 240(* *) 241(* Variables: "x" etc. *) 242(* Tuples: "(x,y)" "(a,b,c)" "((a,b),(c,d))" etc. *) 243(* Applications: "f (x,y) z" "f x" etc. *) 244(* *) 245(* Variables are just substituted for. With tuples, the substitution is *) 246(* done component-wise, and function applications are effectively *) 247(* rewritten in the body of the let-term. *) 248(* ---------------------------------------------------------------------*) 249 250local 251 fun conv bconv = 252 fn tm => 253 let 254 val (func, arg) = boolSyntax.dest_let tm 255 val (ty1, ty2) = Type.dom_rng (Term.type_of func) 256 val defn = Thm.INST_TYPE [alpha |-> ty1, beta |-> ty2] LET_DEF 257 val thm = RIGHT_BETA (AP_THM (RIGHT_BETA (AP_THM defn func)) arg) 258 in 259 if Term.is_abs func 260 then REDUCE func arg (RIGHT_BETA thm) 261 else if pairSyntax.is_uncurry func 262 then CONV_RULE (RAND_CONV bconv) thm 263 else CONV_RULE 264 (RAND_CONV (conv bconv)) 265 (AP_THM 266 (AP_TERM (rator (rator tm)) (conv bconv func)) arg) 267 end 268 handle HOL_ERR _ => raise ERR "let_CONV" "cannot reduce the let" 269in 270 val let_CONV = conv PAIRED_BETA_CONV 271 val GEN_LET_CONV = conv GEN_BETA_CONV 272end 273 274(* ---------------------------------------------------------------------*) 275(* LET_SIMP_CONV: conversion for eliminating unused lets *) 276(* *) 277(* Given a term: *) 278(* *) 279(* "let (v1, v2) = (x1,x2) in tm[v1]" *) 280(* *) 281(* LET_SIMP_CONV gen *) 282(* *) 283(* |- let (v1, v2) = (x1,x2) in tm[v1] *) 284(* = *) 285(* let v1 = x1 in tm[v1] *) 286(* *) 287(* Pairs of arbitrary nestings can be handled and more than one *) 288(* variable might be removed. If all variables are unused, the let *) 289(* is eliminated completely. *) 290(* *) 291(* The parameter gen determines, whether FST and SND are introduced *) 292(* to handle values that are not explicitly pairs *) 293(* ---------------------------------------------------------------------*) 294 295fun LET_SIMP_CONV gen tm = 296let 297 (*destruct the original term ``let vars = v in b vars``, 298 ab = \vars. b vars*) 299 val (ab, v) = dest_let tm; 300 val (vars,b) = dest_pabs ab 301 302 (*check which variables are used / unused. Abort if 303 all variables are really needed*) 304 val vars_set = FVL [vars] empty_tmset; 305 val unused_vars_set = HOLset.difference (vars_set, FVL [b] empty_tmset); 306 val _ = if HOLset.isEmpty unused_vars_set then raise UNCHANGED else (); 307 308 val used_vars_list = HOLset.listItems ( 309 HOLset.difference (vars_set, unused_vars_set)); 310 311 val beta_conv = if gen then GEN_BETA_CONV else 312 (PAIRED_BETA_CONV ORELSEC BETA_CONV); 313 314 (*generate the new result term 315 if no variable is needed just return b*) 316 val result_term = if null used_vars_list then b else 317 let 318 (*otherwise abstract with just the needed variables 319 and get the new value of v by using GEN_BETA_CONV*) 320 val new_vars = list_mk_pair used_vars_list; 321 val new_ab = mk_pabs (new_vars, b); 322 val new_v0 = mk_comb (mk_pabs (vars, new_vars), v); 323 val new_v_thm = beta_conv new_v0 324 val new_v = (rhs o concl) new_v_thm 325 in 326 mk_let (new_ab, new_v) 327 end; 328 329 (*prove equality between the original term and the constructed one by 330 removing LET and simplifying using GEN_BETA_CONV. if LET was removed, 331 an error will occur, so use reflexivity in that case*) 332 fun my_let_CONV t = 333 (REWR_CONV LET_THM THENC beta_conv) t handle HOL_ERR _ => 334 REFL t 335 336 val tm_thm = my_let_CONV tm 337 val result_thm = my_let_CONV result_term 338in 339 TRANS tm_thm (GSYM result_thm) 340end handle HOL_ERR _ => raise UNCHANGED; 341 342 343end 344