doc-src/Tutorial/CodeGen/CodeGen.thy
 changeset 5377 efb799c5ed3c
equal inserted replaced
5376:60b31a24f1a6 5377:efb799c5ed3c
`       `
`     1 CodeGen = Main +`
`       `
`     2 types 'v binop = 'v => 'v => 'v`
`       `
`     3 datatype ('a,'v) expr = Cex 'v`
`       `
`     4                       | Vex 'a`
`       `
`     5                       | Bex ('v binop)  (('a,'v) expr) (('a,'v) expr)`
`       `
`     6 consts value :: ('a => 'v) => ('a,'v)expr => 'v`
`       `
`     7 primrec`
`       `
`     8 "value env (Cex v) = v"`
`       `
`     9 "value env (Vex a) = env a"`
`       `
`    10 "value env (Bex f e1 e2) = f (value env e1) (value env e2)"`
`       `
`    11 datatype ('a,'v) instr = Const 'v`
`       `
`    12                        | Load 'a`
`       `
`    13                        | Apply ('v binop)`
`       `
`    14 consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list`
`       `
`    15 primrec`
`       `
`    16 "exec s vs [] = vs"`
`       `
`    17 "exec s vs (i#is) = (case i of`
`       `
`    18     Const v  => exec s (v#vs) is`
`       `
`    19   | Load a   => exec s ((s a)#vs) is`
`       `
`    20   | Apply f  => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"`
`       `
`    21 consts comp :: ('a,'v) expr => (('a,'v) instr) list`
`       `
`    22 primrec`
`       `
`    23 "comp (Cex v)       = [Const v]"`
`       `
`    24 "comp (Vex a)       = [Load a]"`
`       `
`    25 "comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"`
`       `
`    26 end`