--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,46 @@
+CodeGenIf = List +
+types 'v binop = 'v => 'v => 'v
+      'v test = 'v => bool
+datatype ('a,'v) expr = Vex 'a 
+                      | Cex 'v
+                      | Bex ('v binop) (('a,'v) expr) (('a,'v) expr)
+                      | Ifex ('v test) (('a,'v)expr) (('a,'v)expr) (('a,'v)expr)
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec value expr
+"value env (Vex a) = env a"
+"value env (Cex v) = v"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
+"value env (Ifex t b e1 e2) =
+   (if t(value env b) then value env e1 else value env e2)"
+datatype ('a,'v) instr = Load 'a
+                       | Const 'v
+                       | Apply ('v binop)
+                       | Jump nat
+                       | Test ('v test) nat
+consts exec :: "('a => 'v) * 'v list * (('a,'v) instr) list => 'v list"
+recdef exec "measure(%(s,vs,is).length is)"
+simpset "simpset() addsimps [diff_less_Suc]"
+"exec(s, vs, []) = vs"
+"exec(s, vs, i#is) = (case i of
+    Load a   => exec(s,(s a)#vs,is)
+  | Const v  => exec(s,v#vs,is)
+  | Apply f  => exec(s, (f (hd vs) (hd(tl vs)))#(tl(tl vs)), is)
+  | Jump n   => exec(s, vs, drop n is)
+  | Test t n => (if t(hd vs) then exec(s,tl vs, drop n is)
+                             else exec(s,tl vs, is)))"
+consts comp :: ('a,'v) expr => (('a,'v) instr) list
+primrec comp expr
+"comp (Vex a) = [Load a]"
+"comp (Cex v) = [Const v]"
+"comp (Bex f e1 e2) = (comp e2)@(comp e1)@[Apply f]"
+"comp (Ifex t b e1 e2) = (let is1 = comp e1; is2 = comp e2
+                          in comp b @ [Test t (Suc(length is2))] @
+                             is2 @ [Jump (length is1)] @ is1)"
+
+consts wf :: ('a,'v)instr list => bool
+primrec wf list
+"wf [] = True"
+"wf (i#is) = (wf is & (case i of Load a => True | Const v => True
+  | Apply f  => True | Jump n => n <= length is | Test t n => n <= length is))"
+
+end