Lean IR

lean_ir.lean

import data.buffer

namespace lean_ir
/-- A simple type system based on memory representation -/
inductive type : Type
| ptr : type → type -- 4/8 bytes: pointer to data of type X
| array : type → type -- (sizeof X)*n bytes for some n: raw array of data of type X
| unit : type -- 0 bytes
| prod : type → type → type -- unboxed tuple, sizeof X + sizeof Y bytes
| bool : type -- 1 byte
--| u1 : type -- fixed width numeric types
--| u2 : type
--| u4 : type
--| u8 : type
| nat : type
| int : type
| arrow : type → type → type -- code for a closed function (with tupled arguments), unknown size
| any : type -- unknown data, unknown size (no discriminator)

namespace type
def size_of : type → option ℕ
| (ptr X) := some 8
| (array X) := none
| unit := some 0
| (prod X Y) := do x ← size_of X, y ← size_of Y, some (x + y)
| bool := some 1
--| u1 := some 1
--| u2 := some 2
--| u4 := some 4
--| u8 := some 8
| nat := some 4
| int := some 4
| (arrow Γ X) := none
| any := none

def mk_list : list type → type
| [] := unit
| (X::Γ) := prod X (mk_list Γ)
end type

section
open type

inductive unop : Type
| pi1
| pi2
| deref
| new
| int_neg
| not

inductive binop : Type
| nth
| nat_add
| nat_sub
| nat_mul
| nat_div
| nat_lt
| nat_le
| nat_eq
| int_add
| int_sub
| int_mul
| int_div
| int_lt
| int_le
| int_eq
| and
| or

inductive unopT : unop → type → type → Prop
| pi1 {X Y} : unopT unop.pi1 (ptr (prod X Y)) (ptr X)
| pi2 {X Y} : unopT unop.pi2 (ptr (prod X Y)) (ptr Y)
| deref {X} : unopT unop.deref (ptr X) X
| new {X} : unopT unop.pi1 X (ptr X)
| int_neg : unopT unop.int_neg int int
| not : unopT unop.not bool bool

inductive binopT : binop → type → type → type → Prop
| nth {X} : binopT binop.nth (ptr (array X)) nat (ptr X)
| nat_add : binopT binop.nat_add nat nat nat
| nat_sub : binopT binop.nat_sub nat nat nat
| nat_mul : binopT binop.nat_mul nat nat nat
| nat_div : binopT binop.nat_div nat nat nat
| nat_lt : binopT binop.nat_lt nat nat bool
| nat_le : binopT binop.nat_le nat nat bool
| nat_eq : binopT binop.nat_eq nat nat bool
| int_add : binopT binop.int_add int int int
| int_sub : binopT binop.int_sub int int int
| int_mul : binopT binop.int_mul int int int
| int_div : binopT binop.int_div int int int
| int_lt : binopT binop.int_lt int int bool
| int_le : binopT binop.int_le int int bool
| int_eq : binopT binop.int_eq int int bool
| and : binopT binop.and bool bool bool
| or : binopT binop.or bool bool bool

/-- A model of pointers using lenses into memory. In reality
  these would just be indexes into memory giving the start
  of the block, with the end of the block derived from the type's
  size_of, when applicable. -/
inductive addr : Type
| idx : ℕ → addr
| nth : addr → ℕ → addr
| pi1 : addr → addr
| pi2 : addr → addr

mutual inductive value, expr
with value : Type
| var : ℕ → value
| ptr : addr → value
| nil : value
| cons : value → value → value
| star : value
| pair : value → value → value
| bool : _root_.bool → value
| nat : ℕ → value
| int : ℤ → value
| lam : list type → expr → value
| box : type → value → value
with expr : Type
| elet : value → expr → expr -- let x := v in e
| unop : unop → value → expr → expr -- let x := op v in e
| binop : binop → value → value → expr → expr -- let x := op v1 v2 in e
| app : value → value → expr → expr -- let x := f v in e
| set : value → value → expr → expr -- &v1 := v2; e
| unbox : type → value → expr → expr -- let x : T := unbox v in e
| cond : value → expr → expr → expr -- if v then e else e'
| return : value → expr -- return v

/-- Static typing for `value` and `expr` (with untyped store) -/
mutual inductive valueT, exprT
with valueT : list type → value → type → Prop
| var0 {X Γ} : valueT (X::Γ) (value.var 0) X
| varS {n X Γ Y} : valueT Γ (value.var n) Y → valueT (X::Γ) (value.var (n+1)) Y
| ptr {Γ} (X a) : valueT Γ (value.ptr a) (ptr X) -- possibly invalid
| nil {Γ X} : valueT Γ value.nil (array X)
| cons {Γ X x y} : valueT Γ x X → valueT Γ y (array X) → valueT Γ (value.cons x y) (array X)
| star {Γ} : valueT Γ value.star unit
| pair {Γ X Y x y} : valueT Γ x X → valueT Γ y Y → valueT Γ (value.pair x y) (prod X Y)
| boolval {Γ} (b) : valueT Γ (value.bool b) bool
| natval {Γ} (n) : valueT Γ (value.nat n) nat
| intval {Γ} (n) : valueT Γ (value.int n) int
| lam {Γ'} (Γ X e) : exprT Γ e X → valueT Γ' (value.lam Γ e) (arrow (mk_list Γ) X)
| box {Γ X x} : valueT Γ x X → valueT Γ (value.box X x) any
with exprT : list type → expr → type → Prop
| elet {Γ X Y x e} : valueT Γ x X →
  exprT (X::Γ) e Y → exprT Γ (expr.elet x e) Y -- let x := v in e
| unop {op Γ X Y Z x e} : unopT op X Y → valueT Γ x X →
  exprT (Y::Γ) e Z → exprT Γ (expr.unop op x e) Z -- let x := op v in e
| binop {op Γ A B C Z a b e} : binopT op A B C → valueT Γ a A → valueT Γ b B →
  exprT (C::Γ) e Z → exprT Γ (expr.binop op a b e) Z -- let x := op v1 v2 in e
| app {Γ X Y Z f x e} : valueT Γ f (arrow X Y) → valueT Γ x X →
  exprT (Y::Γ) e Z → exprT Γ (expr.app f x e) Z -- let y := f x in e
| set {Γ X Y p x e} : valueT Γ p (ptr X) → valueT Γ x X →
  exprT Γ e Y → exprT Γ (expr.set p x e) Y -- &p := x; e
| unbox {Γ X Z x e} : valueT Γ x any →
  exprT (X::Γ) e Z → exprT Γ (expr.unbox X x e) Z -- let x : X := unbox v in e
| cond {Γ X b e e'} : valueT Γ b bool →
  exprT Γ e X → exprT Γ e' X → exprT Γ (expr.cond b e e') X -- if v then e else e'
| return {Γ X x} : valueT Γ x X → exprT Γ (expr.return x) X -- return v

inductive state : Type
| normal (mem : buffer value) (stk : list (list value × expr)) (ctx : list value) (e : expr) : state
| return (mem : buffer value) (stk : list (list value × expr)) (exit : value) : state
open lean_ir.state

def value.nth : value → ℕ → option value
| (value.cons a l) 0 := some a
| (value.cons a l) (n+1) := value.nth l n
| _ n := none

def value.modify_nth (f : value → option value) : ℕ → value → option value
| 0     (value.cons a l) := do a' ← f a, some (value.cons a' l)
| (n+1) (value.cons a l) := do l' ← value.modify_nth n l, some (value.cons a l')
| n _ := none

def modify_ptr (m : buffer value) : addr → (value → option value) → option (buffer value)
| (addr.idx n) f :=
  if h : _ then m.write ⟨n, h⟩ <$> f (m.read ⟨n, h⟩) else none
| (addr.pi1 a) f := modify_ptr a $ λ v,
  do value.pair x y ← some v | none,
     x' ← f x, some (value.pair x' y)
| (addr.pi2 a) f := modify_ptr a $ λ v,
  do value.pair x y ← some v | none,
     y' ← f y, some (value.pair x y')
| (addr.nth a n) f := modify_ptr a (value.modify_nth f n)

def get_ptr (m : buffer value) : addr → option value
| (addr.idx n) := if h : _ then m.read ⟨n, h⟩ else none
| (addr.pi1 a) :=
  match get_ptr a with
  | some (value.pair x y) := some x
  | _ := none
  end
| (addr.pi2 a) :=
  match get_ptr a with
  | some (value.pair x y) := some y
  | _ := none
  end
| (addr.nth a n) := do v ← get_ptr a, v.nth n

def ptr_val : value → option addr
| (value.ptr a) := some a
| _ := none

def nat_val : value → option ℕ
| (value.nat n) := some n
| _ := none

def int_val : value → option ℤ
| (value.int n) := some n
| _ := none

def bool_val : value → option _root_.bool
| (value.bool b) := some b
| _ := none

def untuple : list type → value → option (list value)
| []     value.star := some []
| (X::Γ) (value.pair x v) := do l ← untuple Γ v, some (x::l)
| _ _ := none

def subst : value → list value → option value
| (value.var n) Γ := Γ.nth n
| (value.cons a l) Γ := value.cons <$> subst a Γ <*> subst l Γ
| (value.pair a l) Γ := value.pair <$> subst a Γ <*> subst l Γ
| (value.box X v) Γ := value.box X <$> subst v Γ
| v Γ := some v

def step_unop (m : buffer value) (S : list (list value × expr)) (Γ : list value)
  (v : value) (e : expr) : unop → option state
| unop.pi1 := do a ← ptr_val v, some (normal m S (value.ptr a.pi1 :: Γ) e)
| unop.pi2 := do a ← ptr_val v, some (normal m S (value.ptr a.pi2 :: Γ) e)
| unop.deref := do a ← ptr_val v, v' ← get_ptr m a, some (normal m S (v' :: Γ) e)
| unop.new := let a := addr.idx m.size, m' := m.push_back v in
  some (normal m' S (value.ptr a :: Γ) e)
| unop.int_neg := do n ← int_val v, some (normal m S (value.int (-n) :: Γ) e)
| unop.not := do b ← bool_val v, some (normal m S (value.bool (bnot b) :: Γ) e)

def step_binop (m : buffer value) (S : list (list value × expr)) (Γ : list value)
  (v₁ v₂ : value) (e : expr) : binop → option state
| binop.nth := do a ← ptr_val v₁, n ← nat_val v₂, some (normal m S (value.ptr (a.nth n) :: Γ) e)
| binop.nat_add := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.nat (v₁ + v₂) :: Γ) e)
| binop.nat_sub := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.nat (v₁ - v₂) :: Γ) e)
| binop.nat_mul := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.nat (v₁ * v₂) :: Γ) e)
| binop.nat_div := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.nat (v₁ / v₂) :: Γ) e)
| binop.nat_lt := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.bool (v₁ < v₂) :: Γ) e)
| binop.nat_le := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.bool (v₁ ≤ v₂) :: Γ) e)
| binop.nat_eq := do v₁ ← nat_val v₁, v₂ ← nat_val v₂, some (normal m S (value.bool (v₁ = v₂) :: Γ) e)
| binop.int_add := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.int (v₁ + v₂) :: Γ) e)
| binop.int_sub := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.int (v₁ - v₂) :: Γ) e)
| binop.int_mul := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.int (v₁ * v₂) :: Γ) e)
| binop.int_div := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.int (v₁ / v₂) :: Γ) e)
| binop.int_lt := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.bool (v₁ < v₂) :: Γ) e)
| binop.int_le := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.bool (v₁ ≤ v₂) :: Γ) e)
| binop.int_eq := do v₁ ← int_val v₁, v₂ ← int_val v₂, some (normal m S (value.bool (v₁ = v₂) :: Γ) e)
| binop.and := do v₁ ← bool_val v₁, v₂ ← bool_val v₂, some (normal m S (value.bool (v₁ && v₂) :: Γ) e)
| binop.or := do v₁ ← bool_val v₁, v₂ ← bool_val v₂, some (normal m S (value.bool (v₁ || v₂) :: Γ) e)

/-- Dynamic semantics. The step function transitions the state, and
  returns `none` if something goes wrong. The end state has the form
  `return m [] v`, in which case `v` is the output of the program. -/
def step : state → option state
| (normal m S Γ (expr.elet x e)) := do x ← subst x Γ, some (normal m S (x :: Γ) e)
| (normal m S Γ (expr.unop op v e)) := do v ← subst v Γ, step_unop m S Γ v e op
| (normal m S Γ (expr.binop op v₁ v₂ e)) :=
  do v₁ ← subst v₁ Γ, v₂ ← subst v₂ Γ, step_binop m S Γ v₁ v₂ e op
| (normal m S Γ (expr.app f x e)) :=
  do value.lam Γ' e' ← subst f Γ | none,
     l ← subst x Γ >>= untuple Γ', some (normal m ((Γ, e)::S) l e')
| (normal m S Γ (expr.set p x e)) :=
  do a ← subst p Γ >>= ptr_val, x ← subst x Γ,
     m' ← modify_ptr m a (λ _, some x), some (normal m' S Γ e)
| (normal m S Γ (expr.unbox X x e)) := do x ← subst x Γ, some (normal m S (x :: Γ) e)
| (normal m S Γ (expr.cond b e e')) :=
  do b ← subst b Γ >>= bool_val, some (normal m S Γ $ if b then e else e')
| (normal m S Γ' (expr.return v)) := do v ← subst v Γ', some (return m S v)
| (return m ((Γ, e)::S) v) := some (normal m S (v::Γ) e)
| (return m [] v) := none -- halt state

end

end lean_ir