dev/sw2/NormalScript.sml

26   `(if c1 /\ c2 then e1 else e2) =
27      let x = e2 in
38   `(if c1 \/ c2 then e1 else e2) =
41        if c2 then x else e2)`,
110  `!f e1 e2. C (f e1 e2) = \k. C e1 (\x. C e2 (\y. C (f x y) k))`,
115    `(C (e1 + e2) =  \k. C e1 (\x. C e2 (\y. C (x + y) k))) /\
116     (C (e1 - e2) =  \k. C e1 (\x. C e2 (\y. C (x - y) k))) /\
117     (C (e1 * e2) =  \k. C e1 (\x. C e2 (\y. C (x * y) k))) /\
118     (C (e1 ** e2) = \k. C e1 (\x. C e2 (\y. C (x ** y) k)))`,
124    `(C (e1 + e2) =  \k. C e1 (\x. C e2 (\y. C (y + x) k))) /\
125     (C (e1 - e2) =  \k. C e2 (\x. C e1 (\y. C (y - x) k))) /\
126     (C (e1 * e2) =  \k. C e1 (\x. C e2 (\y. C (y * x) k))) /\
127     (C (e1 ** e2) = \k. C e1 (\x. C e2 (\y. C (x ** y) k)))`,
133   `C (e1, e2) = \k. C e1 (\x. C e2 (\y. k (x,y)))`,
247    `C (if cmpop c1 c2 then e1 else e2) =
250             else C e2 (\y.y)) (\z. k z)))`,
256    `C (if cmpop c1 c2 then e1 else e2) =
259             else C e2 (\y.y)
276    `(let x = e1 in e2) = e2`,
282    `(let x = (let y = e1 in e2 y) in e3 x) =
283     (let y = e1 in let x = e2 y in e3 x)`,
302   ``(let f = fun e1 in e2 f) = e2 e1``,
315   ``(let v = atom v in let f = fun (e1 v) in e2 f) =
316     let f = fun (\v. e1 v) in e2 (f v)``,
332   ``(let f = fun e1 in e2 f) = e2 e1``,
339   ``(\x. let f = fun e1 in e2 f) = (let f = fun e1 in (\x. e2 f))``,
345   ``(let v = e1 in let f = fun e2 in e3 v f) =
346     (let f = fun e2 in let v = e1 in e3 v f)``,
352   ``(if e1 then let f = fun k1 in e2 f else e3) =
353         (let f = fun k1 in if e1 then e2 f else e3)``,
359   ``(if e1 then e2 else let f = fun k1 in e3 f) =
360         (let f = fun k1 in if e1 then e2 else e3 f)``,