File size: 2,072 Bytes
f5deffb | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 | import BCPL.Semantics
/-!
# BCPL.Compile
Lowering of BCPL to Universal Word IR. There is no BCPL runtime: variables are memory cells
at `addr x`, expressions leave their value on the data stack, and statements leave the data
stack as they found it.
-/
namespace WordDialect
namespace BCPL
open IR
def binCode {n : Nat} : BinOp → List (Instr n)
| .add => [.add]
| .sub => [.sub]
| .mul => [.mul]
| .div => [.sdiv]
| .and => [.and]
| .or => [.or]
| .neqv => [.xor]
| .shl => [.shl]
| .shr => [.shr]
| .eq => cmpFlagCode .eq
| .ne => cmpFlagCode .ne
| .lt => cmpFlagCode .slt
| .gt => cmpFlagCode .sgt
| .le => cmpFlagCode .sle
| .ge => cmpFlagCode .sge
/-- `neg`: compute `0 - v` as `v 0 SWAP SUB`. -/
def unCode {n : Nat} : UnOp → List (Instr n)
| .neg => [.word 0#n, .swap, .sub]
| .not => [.not]
def compileE {n : Nat} (addr : Var → Word n) : Expr → List (Instr n)
| .num z => [.word (BitVec.ofInt n z)]
| .var x => [.word (addr x), .load]
| .addrOf x => [.word (addr x)]
| .rv e => compileE addr e ++ [.load]
| .un o e => compileE addr e ++ unCode o
| .bin o a b => compileE addr a ++ compileE addr b ++ binCode o
/-- Right-hand side first, then (for an indirect target) the address, then `STORE`. -/
def assignCode {n : Nat} (addr : Var → Word n) : LVal → Expr → List (Instr n)
| .var x, e => compileE addr e ++ [.word (addr x), .store]
| .rv a, e => compileE addr e ++ compileE addr a ++ [.store]
def compile {n : Nat} (addr : Var → Word n) : Stmt → Frag n
| .skip => Frag.empty
| .assign l e => Frag.ofCode (assignCode addr l e)
| .seq a b => (compile addr a).seq (compile addr b)
| .test c t e => (Frag.ofCode (compileE addr c)).seq (Frag.ite (compile addr t) (compile addr e))
| .while c body => Frag.whileLoop (Frag.ofCode (compileE addr c)) (compile addr body)
/-- A complete program: the statement at address 0, followed by `HALT`. -/
def compileProgram {n : Nat} (addr : Var → Word n) (s : Stmt) : Prog n :=
(compile addr s).emit 0 ++ [.halt]
end BCPL
end WordDialect
|