1(*===========================================================================*) 2(* Applying CPS to semantics-based ASTs for a simple WHILE language *) 3(*===========================================================================*) 4 5open HolKernel Parse boolLib bossLib relationTheory; 6 7val _ = new_theory "cps"; 8 9(*---------------------------------------------------------------------------*) 10(* Combinator-based pseudo-ASTs for simple programs *) 11(*---------------------------------------------------------------------------*) 12 13val Seq_def = 14 Define 15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`; 16 17val Par_def = 18 Define 19 `Par f1 f2 = \x. (f1 x, f2 x)`; 20 21val Ite_def = 22 Define 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 24 25val Rec_def = 26 TotalDefn.DefineSchema 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 28 29val Rec_ind = fetch "-" "Rec_ind"; 30 31 32(*---------------------------------------------------------------------------*) 33(* CPS definitions. The invocation "CPS f" wraps a function in a CPS, in *) 34(* analogy with DEV for hardware. CPS-ified functions are intended to be *) 35(* representatives for lower-level implementations. *) 36(*---------------------------------------------------------------------------*) 37 38val CPS_def = 39 Define 40 `CPS f = \k arg. k (f arg)`; 41 42val CPS_ID = store_thm 43("CPS_ID", 44 ``CPS (\x.x) = \k x. k x``, 45 SIMP_TAC std_ss [CPS_def]); 46 47val CPS_CONST = store_thm 48("CPS_CONST", 49 ``CPS (\x.c) = \k x. k c``, 50 SIMP_TAC std_ss [CPS_def]); 51 52val UNCPS = store_thm 53("UNCPS", 54 ``CPS f k = \arg. let z = f arg in k z``, 55 METIS_TAC [CPS_def]); 56 57(*---------------------------------------------------------------------------*) 58(* Passing the identity function to a CPS function is the inverse of *) 59(* CPSing the function *) 60(*---------------------------------------------------------------------------*) 61 62val CPS_INV = Q.store_thm 63("CPS_INV", 64 `(!f g. (f = CPS g) ==> (f = (CPS (\arg. f (\x.x) arg)))) /\ 65 (!f. f arg = (CPS f) (\x.x) arg)`, 66 RW_TAC std_ss [CPS_def] THEN METIS_TAC []); 67 68 69(*---------------------------------------------------------------------------*) 70(* Wrapping a function in a CPS interface that takes 2 continuations. *) 71(* Used in the test expression of an if-then-else *) 72(*---------------------------------------------------------------------------*) 73 74val CPS2_def = 75 Define 76 `CPS2 f = \k1 k2 arg. if f arg then k1 T else k2 F`; 77 78val CPS2_INV = Q.store_thm 79("CPS2_INV", 80 `(!f. (?f'. f = CPS2 f') ==> (f = (CPS2 (\arg. f (\x.x) (\x.x) arg)))) /\ 81 (!f. f arg = (CPS2 f) (\x.x) (\x.x) arg)`, 82 RW_TAC std_ss [CPS2_def] THEN METIS_TAC []); 83 84 85(*---------------------------------------------------------------------------*) 86(* CPSing sequential composition *) 87(*---------------------------------------------------------------------------*) 88 89val CPS_SEQ_def = 90 Define 91 `CPS_SEQ f g = \k arg. f (\ret. g k ret) arg`; 92 93val CPS_SEQ_INTRO = Q.store_thm 94("CPS_SEQ_INTRO", 95 `!f g. CPS (Seq f g) = CPS_SEQ (CPS f) (CPS g)`, 96 RW_TAC std_ss [CPS_def, Seq_def, CPS_SEQ_def, FUN_EQ_THM]); 97 98 99(*---------------------------------------------------------------------------*) 100(* CSPing parallel composition *) 101(*---------------------------------------------------------------------------*) 102 103val CPS_PAR_def = 104 Define 105 `CPS_PAR f g = \k arg. f (\ret2. g (\ret. k (ret2, ret)) arg) arg`; 106 107val CPS_PAR_INTRO = Q.store_thm 108("CPS_PAR_INTRO", 109 `!f g. CPS (Par f g) = CPS_PAR (CPS f) (CPS g)`, 110 RW_TAC std_ss [CPS_def, Par_def, CPS_PAR_def, FUN_EQ_THM]) 111 112 113(*---------------------------------------------------------------------------*) 114(* CPSing if-then-else *) 115(*---------------------------------------------------------------------------*) 116(* 117val CPS_ITE_def = 118 Define 119 `CPS_ITE e f g = \k arg. let k2 = k in e (\ret. f k2 arg) (\ret. g k2 arg) arg`; 120 121val CPS_ITE_INTRO = Q.store_thm 122("CPS_ITE_INTRO", 123 `!e f g. CPS (Ite e f g) = CPS_ITE (CPS2 e) (CPS f) (CPS g)`, 124 RW_TAC std_ss [CPS_def, CPS2_def, Ite_def, 125 CPS_ITE_def, FUN_EQ_THM, COND_RAND, LET_THM]) 126 127val CPS_TEST_def = 128 Define 129 `CPS_TEST f = \k1 k2 arg. f (\ret. if ret then k1 ret else k2 ret) arg`; 130 131val CPS2_INTRO = Q.store_thm 132("CPS2_INTRO", 133 `!f. CPS2 f = CPS_TEST (CPS f)`, 134 RW_TAC std_ss [CPS_def, CPS2_def, CPS_TEST_def, FUN_EQ_THM]); 135*) 136 137val CPS_ITE_def = 138 Define 139 `CPS_ITE e f g = \k arg. e (\ret. let k2 = k in if ret then f k2 arg else g k2 arg) arg`; 140 141val CPS_ITE_INTRO = Q.store_thm 142("CPS_ITE_INTRO", 143 `!e f g. CPS (Ite e f g) = CPS_ITE (CPS e) (CPS f) (CPS g)`, 144 RW_TAC std_ss [CPS_def, Ite_def, CPS_ITE_def, FUN_EQ_THM, COND_RAND, LET_THM]) 145 146 147(* 148(*---------------------------------------------------------------------------*) 149(* Recursion. We want *) 150(* *) 151(* CPS_REC e f g = \arg k. e arg (\ret. f arg k) *) 152(* (\ret. g arg (\ret. CPS_REC e f g ret k)) *) 153(* *) 154(* The termination conditions synthesized by TFL are un-provable. *) 155(* *) 156(* Termination conditions : *) 157(* 0. !arg k ret. R (ret,k) (arg,k) *) 158(* 1. WF R : defn *) 159(* *) 160(* If e is a CPS2 term and g is CPS, then ret is the result of *) 161(* applying g to arg. We only need to do this if e is false. *) 162(* *) 163(*---------------------------------------------------------------------------*) 164 165(*---------------------------------------------------------------------------*) 166(* The types become heavy in the following, so we introduce some abbrevs *) 167(*---------------------------------------------------------------------------*) 168 169val _ = type_abbrev ("cps_fun", ``:('b -> 'c) -> ('a -> 'c)``) 170val _ = type_abbrev ("cps2_fun", ``:(bool->'b) -> (bool->'b) -> 'a -> 'b``); 171 172(*---------------------------------------------------------------------------*) 173(* We'll make a series of definitions, purely for sanity's sake. *) 174(*---------------------------------------------------------------------------*) 175 176val CPS_REC_fn_def = Define 177`CPS_REC_fn (e: ('a,'b) cps2_fun) 178 (f: ('a,'a,'b) cps_fun) 179 (g: ('a,'a,'b) cps_fun) = 180 \CPS_REC. \(k, arg). e (\ret. f k arg) 181 (\ret. g (\ret. CPS_REC (k, ret)) arg) 182 arg`; 183 184val CPS_REC_TCS_def = Define 185`CPS_REC_TCS (R: (('a->'b) # 'a) -> (('a->'b) # 'a) -> bool) 186 (e: ('a,'b) cps2_fun) 187 (g: ('a,'a,'b) cps_fun) = 188 WF R /\ 189 (?e' g'. (e = CPS2 e') /\ (g = CPS g') /\ 190 !k arg. ~(e' arg) ==> R (k,g' arg) (k,arg))`; 191 192val CPS_REC_PRIM_def = 193 Define 194 `CPS_REC_PRIM e f g = WFREC (@R. CPS_REC_TCS R e g) (CPS_REC_fn e f g)`; 195 196val CPS_REC_PRIM_THM = 197(UNDISCH_ALL o 198 SIMP_RULE std_ss [GSYM AND_IMP_INTRO, CPS_REC_TCS_def, CPS_REC_fn_def] o 199 SPEC_ALL) 200(Q.prove 201(`!R e f g arg k. 202 CPS_REC_TCS R e g 203 ==> 204 (CPS_REC_PRIM e f g (arg, k) = 205 CPS_REC_fn e f g (CPS_REC_PRIM e f g) (arg, k))`, 206 RW_TAC std_ss [Once CPS_REC_PRIM_def] 207 THEN `CPS_REC_TCS (@R. CPS_REC_TCS R e g) e g` by METIS_TAC [SELECT_THM] 208 THEN POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [Once CPS_REC_TCS_def]) 209 THEN RW_TAC std_ss [WFREC_THM, GSYM CPS_REC_PRIM_def] 210 THEN RW_TAC std_ss [Once CPS_REC_fn_def] 211 THEN FULL_SIMP_TAC std_ss [CPS_def, CPS2_def] 212 THEN RW_TAC std_ss [RESTRICT_LEMMA] 213 THEN RW_TAC std_ss [CPS_REC_fn_def]) 214); 215 216val CPS_REC_def = 217 Define 218 `CPS_REC e f g k arg = CPS_REC_PRIM e f g (k,arg)`; 219 220(*---------------------------------------------------------------------------*) 221(* The laborious model-building above finally yields *) 222(* *) 223(* [?e' g'. (e = CPS2 e') /\ (g = CPS g') /\ *) 224(* !arg k. ~e' arg ==> R (g' arg,k) (arg,k), *) 225(* WF R *) 226(* ] *) 227(* |- *) 228(* CPS_REC e f g arg k = *) 229(* e arg (\ret. f arg k) *) 230(* (\ret. g arg (\ret. CPS_REC e f g ret k)) *) 231(* *) 232(*---------------------------------------------------------------------------*) 233 234val CPS_REC_THM = SIMP_RULE std_ss [GSYM CPS_REC_def] CPS_REC_PRIM_THM; 235 236val _ = save_thm("CPS_REC_THM",CPS_REC_THM); 237 238 239(*---------------------------------------------------------------------------*) 240(* We want to connect CPS_REC with while-loops, and need to make their *) 241(* respective termination conditions relate to each other. *) 242(*---------------------------------------------------------------------------*) 243 244val TC_RELATION = Q.prove 245(`(!x:'a. ~e x ==> R (g x) x) /\ WF R ==> 246 CPS_REC_TCS (\(x1, y1) (x2, y2). R y1 y2) (CPS2 e) (CPS g)`, 247 RW_TAC std_ss [CPS_REC_TCS_def,CPS2_def,CPS_def] 248 THENL 249 [WEAKEN_TAC is_forall 250 THEN IMP_RES_TAC 251 (Q.ISPEC `SND:('a->'b)#'a->'a` 252 (Q.ID_SPEC 253 (INST_TYPE [alpha |-> Type `:('a->'b)#'a`, 254 beta |-> alpha] WF_inv_image))) 255 THEN FULL_SIMP_TAC std_ss [pairTheory.LAMBDA_PROD,inv_image_def], 256 Q.EXISTS_TAC `e` THEN Q.EXISTS_TAC `g` THEN METIS_TAC[]]); 257 258val lemma = 259 (REWRITE_RULE [GSYM CPS_REC_TCS_def, AND_IMP_INTRO] o DISCH_ALL) CPS_REC_THM; 260 261(*---------------------------------------------------------------------------*) 262(* How to CPS While-loops *) 263(* *) 264(* Note that f has type :'a -> 'a, instead of :'a -> 'b. *) 265(*---------------------------------------------------------------------------*) 266 267val CPS_REC_INTRO = Q.store_thm 268("CPS_REC_INTRO", 269 `!e f g. 270 (?R. WF R /\ !x. ~e x ==> R (g x) x) 271 ==> 272 (CPS (Rec e f g) = CPS_REC (CPS2 e) (CPS f) (CPS g))`, 273 REPEAT STRIP_TAC 274 THEN REWRITE_TAC [Once CPS_def] 275 THEN RW_TAC std_ss [Rec_def, FUN_EQ_THM] 276 THEN Q.ID_SPEC_TAC `arg` 277 THEN IMP_RES_TAC (DISCH_ALL Rec_ind) 278 THEN POP_ASSUM HO_MATCH_MP_TAC 279 THEN RW_TAC std_ss [] 280 THEN IMP_RES_TAC (INST_TYPE [beta |-> alpha] (DISCH_ALL Rec_def)) 281 THEN POP_ASSUM (fn x => ONCE_REWRITE_TAC [x]) 282 THEN IMP_RES_TAC TC_RELATION 283 THEN IMP_RES_TAC lemma 284 THEN POP_ASSUM (fn x => ONCE_REWRITE_TAC [x]) 285 THEN RW_TAC std_ss [] 286 THEN FULL_SIMP_TAC std_ss [CPS_def, CPS2_def]); 287*) 288 289val CPS_REC_def = Define 290`CPS_REC e f g = \k arg. k (Rec (e (\x.x)) (f (\x.x)) (g (\x.x)) arg)` 291 292val CPS_REC_INTRO = Q.store_thm 293("CPS_REC_INTRO", 294 `!e f g. CPS (Rec e f g) = CPS_REC (CPS e) (CPS f) (CPS g)`, 295 RW_TAC std_ss [CPS_def, CPS_REC_def] THEN 296 METIS_TAC []) 297 298(*---------------------------------------------------------------------------*) 299(* Support for translation into combinator form. *) 300(*---------------------------------------------------------------------------*) 301 302val Rec_INTRO = store_thm 303("Rec_INTRO", 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 306 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x)) 307 ==> (f:'a->'b = Rec f1 f2 f3)``, 308 REPEAT (GEN_TAC ORELSE STRIP_TAC) 309 THEN ONCE_REWRITE_TAC [FUN_EQ_THM] 310 THEN HO_MATCH_MP_TAC Rec_ind 311 THEN GEN_TAC THEN STRIP_TAC 312 THEN IMP_RES_TAC (DISCH_ALL Rec_def) 313 THEN POP_ASSUM (fn th => ONCE_REWRITE_TAC[th]) 314 THEN METIS_TAC[]); 315 316(*---------------------------------------------------------------------------*) 317(* Misc. lemmas *) 318(*---------------------------------------------------------------------------*) 319 320val MY_LET_RAND = 321 save_thm 322 ("MY_LET_RAND", 323 METIS_PROVE [] 324 ``!f M N. (let x = M in f (N x)) = f (let x = M in N x)``); 325 326val UNLET = 327 save_thm 328 ("UNLET", 329 METIS_PROVE [] ``!f M. (let f2 = f in f2 M) = f M``); 330 331 332val _ = export_theory(); 333