doc-src/Tutorial/CodeGen/CodeGen.thy
 author nipkow Wed, 26 Aug 1998 17:27:27 +0200 changeset 5377 efb799c5ed3c permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 5377 efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 1` ```CodeGen = Main + ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 2` ```types 'v binop = 'v => 'v => 'v ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 3` ```datatype ('a,'v) expr = Cex 'v ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 4` ``` | Vex 'a ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 5` ``` | Bex ('v binop) (('a,'v) expr) (('a,'v) expr) ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 6` ```consts value :: ('a => 'v) => ('a,'v)expr => 'v ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 7` ```primrec ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 8` ```"value env (Cex v) = v" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 9` ```"value env (Vex a) = env a" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 10` ```"value env (Bex f e1 e2) = f (value env e1) (value env e2)" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 11` ```datatype ('a,'v) instr = Const 'v ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 12` ``` | Load 'a ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 13` ``` | Apply ('v binop) ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 14` ```consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 15` ```primrec ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 16` ```"exec s vs [] = vs" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 17` ```"exec s vs (i#is) = (case i of ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 18` ``` Const v => exec s (v#vs) is ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 19` ``` | Load a => exec s ((s a)#vs) is ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 20` ``` | Apply f => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 21` ```consts comp :: ('a,'v) expr => (('a,'v) instr) list ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 22` ```primrec ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 23` ```"comp (Cex v) = [Const v]" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 24` ```"comp (Vex a) = [Load a]" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 25` ```"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]" ``` efb799c5ed3c *** empty log message *** nipkow parents: diff changeset ` 26` ```end ```