Module CodeGen

Generic support for writing (privileged) concrete machine programs. These functions implement some basic structured programming primitives. Like most of the instructions, some of them take no explicit arguments, and use whatever is on the stack (e.g. genAnd and genOr below).

Require Import ZArith.
Require Import List.
Require Import Utils.
Import ListNotations.

Require Import Instr.

Local Open Scope Z_scope.
Set Implicit Arguments.

Section CodeGeneration.

Definition code := list Instr.

Definition pop: code := [Pop].
Definition nop: code := [].
Definition push v: code := [Push v].

Definition storeAt loc :=
  push loc ++ [Store].

Definition loadFrom loc: code :=
  push loc ++ [Load].

Definition skipNZ (n : nat) : code :=
  BranchNZ (Z_of_nat (S n)) :: nil.

Definition skip (n : nat) : code :=
  push 1 ++ skipNZ n.

Definition ifNZ t f :=
  let f' := f ++ skip (length t)
  in skipNZ (length f')
     ++ f'
     ++ t.

Definition ite (c t f : code) : code :=
  c ++ ifNZ t f.

Fixpoint cases (cbs : list (code * code)) (default: code) : code :=
  match cbs with
  | nil => default
  | (c,b) :: cbs' => ite c b (cases cbs' default)
  end.

Definition indexed_cases {I} (cnil: code) (genC genB: I -> code) (indices: list I): code :=
  cases (map (fun i => (genC i, genB i)) indices) cnil.

Definition boolToZ (b: bool): Z := if b then 1 else 0.

Definition genFalse :=
  push (boolToZ false).

Definition genTrue :=
  push (boolToZ true).

Definition genAnd :=
  ifNZ nop (pop ++ genFalse).

Definition genOr :=
  ifNZ (pop ++ genTrue) nop.

Definition genNot :=
  ifNZ genFalse genTrue.

Definition genImpl :=
  genNot ++ genOr.

Definition some c: code := c ++ push 1.
Definition none: code := push 0.

Definition sub: code := [Sub].

Definition genTestEqual (c1 c2: code): code :=
  c1 ++
  c2 ++
  sub ++
  genNot.

End CodeGeneration.