Prove Expr.typeCheck_complete for full language with Var, Lam, App

README.md

@@ -71,18 +71,25 @@ You can see the returned integer in the `pre` element.
 ### Syntax
 
 ```ebnf
-            ws = { " " | "\n" | "\r" | "\t" } ;
+             ws = { " " | "\n" | "\r" | "\t" } ;
 
-non-zero-digit = "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
-         digit = "0" | non-zero-digit ;
-    nat-number = "0"
-               | non-zero-digit , { digit } ;
+ non-zero-digit = "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
+          digit = "0" | non-zero-digit ;
+     nat-number = "0"
+                | non-zero-digit , { digit } ;
 
-          sign = "+" | "-" ;
-    int-number = sign , nat-number ;
+           sign = "+" | "-" ;
+     int-number = sign , nat-number ;
 
-          expr = nat-number , ws
-               | int-number , ws;
+     identifier = ( letter | "_" ) , { letter | digit | "_" } ;
+         letter = "a" | ... | "z" | "A" | ... | "Z" ;
+
+           expr = nat-number , ws
+                | int-number , ws
+                | identifier , ws                              (* variable -- not yet implemented in parser *)
+                | "\" , identifier , "." , ws , expr , ws     (* lambda abstraction -- not yet implemented in parser *)
+                | expr , expr , ws                            (* function application -- not yet implemented in parser *)
+                ;
 ```
 
 <!--

Tibi/Compiler.lean

@@ -8,16 +8,21 @@ open Wasm.Value
 
 inductive CompileError
 | OutOfBounds_Int64 (n : Int)
+| Unimplemented
 
-def Expr.compile : Expr → Except CompileError (List Wasm.Instr)
+def Expr.compile : Expr ctx ty → Except CompileError (List Wasm.Instr)
 | .Const n =>
     if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then
       .ok [.i64__const <| Int64.mk ⟨n, h.right, h.left⟩]
     else
       .error <| .OutOfBounds_Int64 n
+| .Var _ =>
+    .error .Unimplemented -- TODO: implement compilation of variable expressions
+| _ => .error .Unimplemented -- TODO: implement compilation of lambda and application expressions
 
 def CompileError.toString : CompileError → String
 | .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}"
+| .Unimplemented => "Unimplemented"
 
 instance : ToString CompileError where
   toString := CompileError.toString

Tibi/Interpreter.lean

@@ -5,11 +5,26 @@ import Tibi.Util
 
 namespace Tibi
 
-def Expr.eval : (e : Expr) → {{ r | Eval e r }}
-| .Const n =>
+def Expr.eval (env : Env ctx) : {ty : Ty} → (e : Expr ctx ty) → ty.dom → {{ r | Eval e r }}
+| _, .Const n, _ =>
     if h : (-Int64.size : Int) ≤ n ∧ n < Int64.size then
       .found (.ok <| Int64.mk ⟨n, h.right, h.left⟩) <| Eval.Const h.right h.left
     else
       Decidable.not_and_iff_or_not_not.mp h |>.by_cases
         (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_ge h)
         (fun h => .found (.error <| .OutOfBounds_Int64 n) <| Eval.ConstErr_lt h)
+| _, .Var x, _ =>
+    .found (.ok <| env.lookup x) <| .Var x env
+| _, .Lam e', x =>
+    match e'.eval (x :: env) x with
+    | .found (.ok v) h => .found (.ok <| fun _ => v) <| .Lam h
+    | .unknown => .unknown
+| .int, .App (dom := .int) (.Lam e₁) e₂, _ =>
+    match e₂.eval env () with
+    | .found (.ok v) h₂ =>
+        match e₁.eval (v :: env) v with
+        | .found (.ok v) h₁ =>
+            .found (.ok <| v) <| .App h₁ h₂
+        | _ => .unknown
+    | _ => .unknown
+| _, _, _ => .unknown

Tibi/Parser.lean

@@ -62,7 +62,7 @@ private def intNumber : Parser Int :=
         | _ => sgn n
   )
 
-private def parser : Parser Expr :=
+private def parser : Parser (Expr .nil .int) :=
   (
     natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
       |>.map fun (n, _) => .Const n
@@ -72,10 +72,10 @@ private def parser : Parser Expr :=
       |>.map fun (n, _) => .Const n
   )
 
-instance : Inhabited (Parser Expr) where
+instance : Inhabited (Parser (Expr .nil .int)) where
   default := parser
 
-private partial def parse' : ReaderT (IO String) Parser Expr := do
+private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do
   fun getLine cs =>
     match parser cs with
     | .error .UnexpectedEndOfInput => do

Tibi/Props/Compiler.lean

@@ -5,14 +5,14 @@ import Tibi.Wasm.Semantics
 namespace Tibi
 
 theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok -- Expr.compile_ok_of_has_type_of_eval
-: {e : Expr} → HasType e _ty → Eval e (.ok v) → {_ : e.compile = .ok instrs}
+: {e : Expr ctx .int} → HasType e _ty → Eval e (.ok v) → e.compile = .ok instrs
 → Wasm.Reduction
     { instrs := instrs ++ K, stack,                                      store, framestate }
     { instrs := K,           stack := .Value (.Num (.Int64 v)) :: stack, store, framestate }
-| .Const n, .Int64 hLt hGe, .Const _ _, hc => by
-    have : (Expr.Const n).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by
-      -- dsimp [Expr.compile]
+| .Const n, .Int64 _ _, .Const hLt hGe, hc => by
+    have : (Expr.Const n : Expr ctx .int).compile = .ok [.i64__const (Int64.mk ⟨n, hLt, hGe⟩)] := by
       apply dite_cond_eq_true <| eq_true <| And.intro hGe hLt
     have : instrs = [.i64__const ⟨n, hLt, hGe⟩ ] := Except.ok.inj <| Eq.trans hc.symm this
     rw [this]
     exact .i64__const
+| .App _ _, _, _, hc => by simp [Expr.compile] at hc

Tibi/Props/Typing.lean

@@ -4,26 +4,38 @@ import Tibi.Typing
 namespace Tibi
 
 theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
-  cases h₁ <;> cases h₂ <;> rfl
+  induction h₁ generalizing t₂ with
+  | Int64 => cases h₂; rfl
+  | Var => cases h₂; rfl
+  | Lam _ ih => cases h₂ with | Lam h' => exact congrArg (Typ.Fn (.Var 0)) (ih h')
+  | App _ _ ihf _ =>
+      cases h₂ with
+      | App hf' _ =>
+          have h := ihf hf'
+          simp only [Typ.Fn.injEq] at h
+          exact h.2
 
-theorem Expr.typeCheck_correct {e : Expr}
-: (ht : HasType e ty) → e.typeCheck = .found ty ht
+theorem Expr.typeCheck_correct : (ht : HasType e t) → e.typeCheck = .found t ht
 | .Int64 (n := n) hLt hGe =>
     have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
     dite_cond_eq_true this
+| .Var => rfl
+| .Lam h => by
+    have ih := typeCheck_correct h
+    simp only [Expr.typeCheck, ih]
+| .App hf hv => by
+    have ihf := typeCheck_correct hf
+    have ihv := typeCheck_correct hv
+    simp [Expr.typeCheck, ihf, ihv]
 
-theorem Expr.typeCheck_complete {e : Expr}
-: e.typeCheck = .unknown → ¬ HasType e ty
-:= by
-  dsimp [Expr.typeCheck]
-  intro h (ht : HasType e ty)
-  match ht with
-  | .Int64 hLt hGe =>
-      have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
-      have := h ▸ dite_cond_eq_true this
-      exact Maybe.noConfusion this
+theorem Expr.typeCheck_complete {e : Expr ctx ty}
+: e.typeCheck = .unknown → ¬ HasType e t
+:= fun h ht => by
+    have := typeCheck_correct ht
+    rw [h] at this
+    exact Maybe.noConfusion this
 
-instance (e : Expr) (t : Typ) : Decidable (HasType e t) :=
+instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
   match h : e.typeCheck with
   | .found t' ht' =>
       if heq : t = t' then
@@ -32,8 +44,11 @@ instance (e : Expr) (t : Typ) : Decidable (HasType e t) :=
         isFalse fun ht => heq (HasType.det ht ht')
   | .unknown => isFalse (Expr.typeCheck_complete h)
 
-theorem type_safe {e : Expr}
+theorem type_safe {e : Expr ctx ty}
 : HasType e t → Eval e r → ∃ v, r = .ok v
-| .Int64 hLt hGe, .Const ..      => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩
+| .Int64 hLt hGe, .Const ..      => ⟨_, rfl⟩
 | .Int64 hLt _,   .ConstErr_lt h => absurd hLt h
 | .Int64 _   hGe, .ConstErr_ge h => absurd hGe h
+| .Var,           .Var ..        => ⟨_, rfl⟩
+| .Lam _,         .Lam ..        => ⟨_, rfl⟩
+| .App _ _,       .App ..        => ⟨_, rfl⟩

Tibi/Semantics.lean

@@ -1,15 +1,25 @@
 import Tibi.FinInt
+import Tibi.Semantics.Env
 import Tibi.Syntax
 
 namespace Tibi
 
 inductive EvalError
 | OutOfBounds_Int64 (n : Int)
 
-inductive Eval : Expr → Except EvalError Int64 → Prop
-| Const       {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size) : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
-| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)   : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
-| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size) : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
+inductive Eval : (Expr ctx ty) → Except EvalError ty.interp → Prop
+| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
+  : Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
+| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
+  : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
+| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
+  : Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
+| Var (x : Locals k ctx ty) (env : Env ctx)
+  : Eval (.Var x) (.ok <| env.lookup x)
+| Lam (d : Eval e (.ok v))
+  : Eval (.Lam e) (.ok <| fun _ => v)
+| App (d₁ : Eval e₁ (.ok v₁)) (d₂ : Eval e₂ (.ok v₂))
+  : Eval (.App (.Lam e₁) e₂) (.ok <| v₁)
 
 def EvalError.toString : EvalError → String
 | .OutOfBounds_Int64 n => s!"{n} is out of Int64 bounds, should be satisfied that -2{Nat.toSuperscriptString 63} ≤ n < 2{Nat.toSuperscriptString 63}"

Tibi/Semantics/Env.lean

@@ -0,0 +1,14 @@
+import Tibi.Syntax
+import Tibi.Util
+
+namespace Tibi
+
+inductive Env : Vec Ty n → Type where
+| nil  : Env Vec.nil
+| cons : Ty.interp a → Env ctx → Env (a :: ctx)
+
+infix:67 " :: " => Env.cons
+
+def Env.lookup : Locals i ctx ty → Env ctx → (Ty.cls ty ty).interp
+| .stop,  x :: _  => x
+| .pop k, _ :: xs => xs.lookup k

Tibi/Syntax/Expr.lean

@@ -1,10 +1,55 @@
 import Tibi.FinInt
+import Tibi.Util
 
 namespace Tibi
 
-inductive Expr
-| Const : Int → Expr
+inductive Ty where
+| int
+| fn (a b : Ty)
+| cls (a b : Ty)
 
-instance : ToString Expr where
-  toString
-  | .Const n => s!"<Const {n}>"
+@[reducible]
+def Ty.interp : Ty → Type
+| int    => Int64
+| fn a b => a.interp → b.interp
+| cls _ b => b.interp
+
+@[reducible]
+def Ty.dom : Ty → Type
+| int => Unit
+| fn a _ => a.interp
+| cls a _ => a.interp
+
+def Ty.toString : Ty → String
+| int    => "Int"
+| fn a b => s!"{a.toString} -> {b.toString}"
+| cls _ b => s!"{b.toString}"
+
+instance : ToString Ty where
+  toString := Ty.toString
+
+inductive Locals : Fin n → Tibi.Vec Ty n → Ty → Type where
+| stop : Locals 0 (ty :: ctx) ty
+| pop  : Locals k ctx ty → Locals k.succ (u :: ctx) ty
+
+def Locals.idx : Locals n ctx ty → Fin n.succ
+| stop  => Fin.mk 0 (Fin.succ_pos _)
+| pop k => k.idx.succ
+
+instance : ToString (Locals n ctx ty) where
+  toString x := s!"${x.idx}"
+
+inductive Expr : Vec Ty n → Ty → Type where
+| Const : Int → Expr ctx .int
+| Var   : Locals i ctx ty → Expr ctx (.cls ty ty)
+| Lam   : Expr (dom :: ctx) (.cls dom ran) → Expr ctx (.fn dom ran)
+| App   : Expr ctx (.fn dom ran) → Expr ctx dom → Expr ctx ran
+
+def Expr.toString : Expr ctx ty → String
+| Const n => s!"<Const {n}>"
+| Var x   => s!"<Var {x} @{ty}>"
+| Lam e   => s!"<Lam {e.toString}>"
+| App e₁ e₂ => s!"<App {e₁.toString} {e₂.toString}>"
+
+instance : ToString (Expr ctx ty) where
+  toString := Expr.toString

Tibi/Top.lean

@@ -14,7 +14,7 @@ partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
       | .ok (expr, []) =>
           match expr.typeCheck with
           | .found t _ =>
-              match expr.eval with
+              match expr.eval .nil () with
               | .found (.ok v) _    => IO.println s!"- : {t} = {v}"
               | .found (.error _) _ => panic! "TODO: prove that this branch cannot be reached (type-safe)"
               | .unknown            => panic! "TODO: prove that this branch cannot be reached (type-safe)"
@@ -37,7 +37,7 @@ def run (inStream : IO.FS.Stream) : IO ByteArray :=
       | .some <| .error e       => .throw e.toString
   )
   >>= (
-    fun (e : Option Expr) =>
+    fun (e : Option (Expr .nil .int)) =>
       match e with
       | .none   => pure Wasm.empty
       | .some e =>

Tibi/Typing.lean

@@ -1,25 +1,52 @@
 import Tibi.FinInt
+import Tibi.Semantics
 import Tibi.Syntax
 import Tibi.Util
 
 namespace Tibi
 
 inductive Typ
+| Var (idx : Nat)
 | Int64
+| Fn (a : Typ) (b : Typ)
 deriving DecidableEq
 
 def Typ.toString : Typ → String
-| Int64 => "Int"
+| Var idx => s!"α{idx}"
+| Int64   => "Int"
+| Fn a b  => s!"{a.toString} -> {b.toString}"
 
 instance : ToString Typ where
   toString := Typ.toString
 
-inductive HasType : Expr → Typ → Prop
+def Ty.toTyp : Ty → Typ
+| int     => .Int64
+| fn a b  => .Fn a.toTyp b.toTyp
+| cls _ b => b.toTyp
+
+inductive HasType : Expr ctx ty → Typ → Prop
 | Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType (.Const n) .Int64
+| Var {x : Locals i ctx ty} : HasType (.Var x) (Ty.cls ty ty).toTyp
+| Lam (h : HasType e t) : HasType (.Lam e) (.Fn (.Var 0) t)
+| App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran
 
-def Expr.typeCheck : (e : Expr) → {{ t | HasType e t }}
+def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }}
 | .Const n =>
     if h : -Int64.size ≤ n ∧ n < Int64.size then
       .found .Int64 <| .Int64 h.right h.left
     else
       .unknown
+| .Var _ =>
+    .found _ .Var
+| .Lam e =>
+    match e.typeCheck with
+    | .found t h => .found (.Fn (.Var 0) t) <| .Lam h
+    | .unknown   => .unknown
+| .App f v =>
+    match f.typeCheck, v.typeCheck with
+    | .found (.Fn a b) hf, .found a' hv =>
+        if h : a = a' then
+          .found b <| .App hf (h ▸ hv)
+        else
+          .unknown
+    | _, _ => .unknown

Tibi/Util.lean

@@ -9,3 +9,9 @@ inductive Maybe (p : α → Prop)
 | found (a : α) : p a → Maybe p
 
 notation "{{ " x " | " p " }}" => Maybe (fun x => p)
+
+inductive Vec (α : Type u) : Nat → Type u
+| nil : Vec α 0
+| cons : α → Vec α n → Vec α n.succ
+
+infixr:67 " :: " => Vec.cons