working/0.2/cpsScript.sml

40    `CPS f = \k arg. k (f arg)`;
54  ``CPS f k = \arg. let z = f arg in k z``,
64  `(!f g. (f = CPS g) ==> (f = (CPS (\arg. f (\x.x) arg)))) /\
65   (!f. f arg = (CPS f) (\x.x) arg)`,
76    `CPS2 f = \k1 k2 arg. if f arg then k1 T else k2 F`;
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)`,
91    `CPS_SEQ f g = \k arg. f (\ret. g k ret) arg`;
105    `CPS_PAR f g = \k arg. f (\ret2. g (\ret. k (ret2, ret)) arg) arg`;
119    `CPS_ITE e f g = \k arg. let k2 = k in e (\ret. f k2 arg) (\ret. g k2 arg) arg`;
129    `CPS_TEST f = \k1 k2 arg. f (\ret. if ret then k1 ret else k2 ret) arg`;
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`;
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))   *)
157 (*      0. !arg k ret. R (ret,k) (arg,k)                                     *)
161 (*    applying g to arg.  We only need to do this if e is false.             *)
180      \CPS_REC. \(k, arg). e (\ret. f k arg)
181                             (\ret. g (\ret. CPS_REC (k, ret)) arg)
182                             arg`;
190             !k arg. ~(e' arg) ==> R (k,g' arg) (k,arg))`;
201 (`!R e f g arg k.
204   (CPS_REC_PRIM e f g (arg, k) =
205    CPS_REC_fn e f g (CPS_REC_PRIM e f g) (arg, k))`,
218    `CPS_REC e f g k arg = CPS_REC_PRIM e f g (k,arg)`;
224 (*        !arg k. ~e' arg ==> R (g' arg,k) (arg,k),                          *)
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))                     *)
276   THEN Q.ID_SPEC_TAC `arg`
290 `CPS_REC e f g = \k arg. k (Rec (e (\x.x)) (f (\x.x)) (g (\x.x)) arg)`