From ef94b71230f5c0bb11b07e45e97b26c7aa8561f4 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Wed, 1 Jan 2025 00:39:36 +0000
Subject: [PATCH 01/13] local.get

---
 Tibi/Compiler.lean                 |  6 +++--
 Tibi/Interpreter.lean              |  3 ++-
 Tibi/Parser.lean                   | 14 +++++++----
 Tibi/Props/Compiler.lean           | 30 +++++++++++++++++++----
 Tibi/Props/Typing.lean             | 27 +++++++++++----------
 Tibi/Semantics.lean                | 20 ++-------------
 Tibi/Semantics/Env.lean            | 14 +++++++++++
 Tibi/Semantics/Eval.lean           | 24 ++++++++++++++++++
 Tibi/Syntax/Expr.lean              | 39 ++++++++++++++++++++++++++----
 Tibi/Top.lean                      |  6 ++---
 Tibi/Typing.lean                   | 13 +++++++---
 Tibi/Util.lean                     |  6 +++++
 Tibi/Wasm/Instruction.lean         | 15 ++++++++----
 Tibi/Wasm/Module/Basic.lean        |  2 +-
 Tibi/Wasm/Semantics/Basic.lean     |  3 +++
 Tibi/Wasm/Semantics/Reduction.lean | 11 ++++++---
 16 files changed, 168 insertions(+), 65 deletions(-)
 create mode 100644 Tibi/Semantics/Env.lean
 create mode 100644 Tibi/Semantics/Eval.lean

diff --git a/Tibi/Compiler.lean b/Tibi/Compiler.lean
index c137d64..83f173b 100644
--- a/Tibi/Compiler.lean
+++ b/Tibi/Compiler.lean
@@ -9,12 +9,14 @@ open Wasm.Value
 inductive CompileError
 | OutOfBounds_Int64 (n : Int)
 
-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⟩]
+      .ok [.i64.const <| Int64.mk ⟨n, h.right, h.left⟩]
     else
       .error <| .OutOfBounds_Int64 n
+| .Var x =>
+    .ok [.local.get x.idx]
 
 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}"
diff --git a/Tibi/Interpreter.lean b/Tibi/Interpreter.lean
index 57a1892..7b5a826 100644
--- a/Tibi/Interpreter.lean
+++ b/Tibi/Interpreter.lean
@@ -5,7 +5,7 @@ import Tibi.Util
 
 namespace Tibi
 
-def Expr.eval : (e : Expr) → {{ r | Eval e r }}
+def Expr.eval (env : Env ctx) : (e : Expr ctx ty) → {{ r | Eval env 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
@@ -13,3 +13,4 @@ def Expr.eval : (e : Expr) → {{ r | Eval e r }}
       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) <| Eval.Var x
diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index 69ca398..0151c40 100644
--- a/Tibi/Parser.lean
+++ b/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 :: .nil)-/ ty) :=
   (
     natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
       |>.map fun (n, _) => .Const n
@@ -71,11 +71,15 @@ private def parser : Parser Expr :=
     intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
       |>.map fun (n, _) => .Const n
   )
+  -- <|> (
+  --   keyword "it" >> ws
+  --     |>.map fun _ => .Var .stop
+  -- )
 
-instance : Inhabited (Parser Expr) where
+instance : Inhabited (Parser (Expr .nil/-(.int :: .nil)-/ ty)) where
   default := parser
 
-private partial def parse' : ReaderT (IO String) Parser Expr := do
+private partial def parse' : ReaderT (IO String) Parser (Expr .nil/-(.int :: .nil)-/ ty) := do
   fun getLine cs =>
     match parser cs with
     | .error .UnexpectedEndOfInput => do
@@ -90,13 +94,13 @@ private partial def parse' : ReaderT (IO String) Parser Expr := do
 -- #eval parse' (pure "9223372036854775808") "".data
 -- #eval parse' (pure "0120") "123".data
 
-def parse (stream : IO.FS.Stream) :=
+def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil/-(.int :: .nil)-/ .int))) :=
   stream.getLine >>= pure ∘ fun s =>
     match s.data with
     | [] => none
     | cs => some <| parse' stream.getLine cs
 
-def parseLine (line : String) :=
+def parseLine (line : String) : Option (ParserT.Result Char Parser.Error Id (Expr .nil/-(.int :: .nil)-/ .int)) :=
   match line.data with
   | [] => none
   | cs => some <| parse' (pure "") cs
diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean
index ac6793f..99cd74e 100644
--- a/Tibi/Props/Compiler.lean
+++ b/Tibi/Props/Compiler.lean
@@ -4,15 +4,35 @@ 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}
+/-
+type mismatch
+  Wasm.Reduction.local__get ↑x.idx
+has type
+  Wasm.Reduction
+    { stack := ?m.4159, store := ?m.4160, framestate := ?m.4161, instrs := Wasm.Instr.local.get ↑x.idx :: ?m.4162 }
+    { stack := Wasm.StackValue.Value (?m.4161.locals.get! ↑x.idx) :: ?m.4159, store := ?m.4160, framestate := ?m.4161,
+      instrs := ?m.4162 } : Prop
+but is expected to have type
+  Wasm.Reduction
+    { stack := stack, store := store, framestate := framestate, instrs := [Wasm.Instr.local.get ↑x.idx] ++ K }
+    { stack := Wasm.StackValue.Value (Wasm.Value.Num (Wasm.Num.Int64 (Env.lookup x env))) :: stack, store := store,
+      framestate := framestate, instrs := K } : Prop
+
+theorem Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok
+: {e : Expr ctx ty} → HasType env e _ty → Eval env 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
+    have : (Expr.Const n : Expr ctx ty).compile = .ok [.i64.const (Int64.mk ⟨n, hLt, hGe⟩)] := by
       -- dsimp [Expr.compile]
       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
+    have : instrs = [.i64.const ⟨n, hLt, hGe⟩] := Except.ok.inj <| Eq.trans hc.symm this
+    rw [this]
+    exact .i64.const
+| .Var x, .Var, .Var _, hc => by
+    have : (Expr.Var x : Expr ctx ty).compile = .ok [.local.get x.idx] := rfl
+    have : instrs = [.local.get x.idx] := Except.ok.inj <| Eq.trans hc.symm this
     rw [this]
-    exact .i64__const
+    exact .local.get x.idx
+-/
diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index ad1ca9a..480f047 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -3,28 +3,28 @@ import Tibi.Typing
 
 namespace Tibi
 
-theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+theorem HasType.det (h₁ : HasType rnv e t₁) (h₂ : HasType env e t₂) : t₁ = t₂ := by
   cases h₁ <;> cases h₂ <;> rfl
 
-theorem Expr.typeCheck_correct {e : Expr}
-: (ht : HasType e ty) → e.typeCheck = .found ty ht
+theorem Expr.typeCheck_correct {e : Expr ctx ty}
+: (ht : HasType env e t) → e.typeCheck env = .found ty.toTyp ht
 | .Int64 (n := n) hLt hGe =>
     have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
     dite_cond_eq_true this
+| .Var => rfl
 
-theorem Expr.typeCheck_complete {e : Expr}
-: e.typeCheck = .unknown → ¬ HasType e ty
+theorem Expr.typeCheck_complete {e : Expr ctx ty}
+: e.typeCheck env = .unknown → ¬ HasType env e ty.toTyp
 := by
   dsimp [Expr.typeCheck]
-  intro h (ht : HasType e ty)
+  intro h (ht : HasType env e ty.toTyp)
   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
+      simp at h
+      exact h hGe hLt
 
-instance (e : Expr) (t : Typ) : Decidable (HasType e t) :=
-  match h : e.typeCheck with
+instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType env e t) :=
+  match h : e.typeCheck env with
   | .found t' ht' =>
       if heq : t = t' then
         isTrue (heq ▸ ht')
@@ -32,8 +32,9 @@ 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}
-: HasType e t → Eval e r → ∃ v, r = .ok v
+theorem type_safe {e : Expr ctx ty}
+: HasType env e t → Eval env e r → ∃ v, r = .ok v
 | .Int64 hLt hGe, .Const ..      => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩
 | .Int64 hLt _,   .ConstErr_lt h => absurd hLt h
 | .Int64 _   hGe, .ConstErr_ge h => absurd hGe h
+| .Var,           .Var x => ⟨env.lookup x, rfl⟩
diff --git a/Tibi/Semantics.lean b/Tibi/Semantics.lean
index f668ba3..0b88a11 100644
--- a/Tibi/Semantics.lean
+++ b/Tibi/Semantics.lean
@@ -1,18 +1,2 @@
-import Tibi.FinInt
-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)
-
-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}"
-
-instance : ToString EvalError where
-  toString := EvalError.toString
+import Tibi.Semantics.Env
+import Tibi.Semantics.Eval
diff --git a/Tibi/Semantics/Env.lean b/Tibi/Semantics/Env.lean
new file mode 100644
index 0000000..07dfeff
--- /dev/null
+++ b/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.interp
+| .stop,  x :: _  => x
+| .pop k, _ :: xs => xs.lookup k
diff --git a/Tibi/Semantics/Eval.lean b/Tibi/Semantics/Eval.lean
new file mode 100644
index 0000000..8923869
--- /dev/null
+++ b/Tibi/Semantics/Eval.lean
@@ -0,0 +1,24 @@
+import Tibi.FinInt
+import Tibi.Semantics.Env
+import Tibi.Syntax
+
+namespace Tibi
+
+inductive EvalError
+| OutOfBounds_Int64 (n : Int)
+
+inductive Eval (env : Env ctx) : (Expr ctx ty) → Except EvalError Int64 → Prop
+| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
+  : Eval env (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
+| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
+  : Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
+| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
+  : Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
+| Var (x : Locals i ctx ty)
+  : Eval env (.Var x) (.ok (env.lookup x))
+
+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}"
+
+instance : ToString EvalError where
+  toString := EvalError.toString
diff --git a/Tibi/Syntax/Expr.lean b/Tibi/Syntax/Expr.lean
index f04d64e..9dbe863 100644
--- a/Tibi/Syntax/Expr.lean
+++ b/Tibi/Syntax/Expr.lean
@@ -1,10 +1,39 @@
 import Tibi.FinInt
+import Tibi.Util
 
 namespace Tibi
 
-inductive Expr
-| Const : Int → Expr
+inductive Ty where
+| int
 
-instance : ToString Expr where
-  toString
-  | .Const n => s!"<Const {n}>"
+@[reducible]
+def Ty.interp : Ty → Type
+| int => Int64
+
+def Ty.toString : Ty → String
+| int => "Int"
+
+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 ty
+
+def Expr.toString : Expr ctx ty → String
+| Const n => s!"<Const {n}>"
+| Var x   => s!"<Var {x} @{ty}>"
+
+instance : ToString (Expr ctx ty) where
+  toString := Expr.toString
diff --git a/Tibi/Top.lean b/Tibi/Top.lean
index abab511..173f55e 100644
--- a/Tibi/Top.lean
+++ b/Tibi/Top.lean
@@ -12,9 +12,9 @@ partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
     if let some r := parseLine line then
       match r with
       | .ok (expr, []) =>
-          match expr.typeCheck with
+          match expr.typeCheck .nil 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 _ _)) =>
       match e with
       | .none   => pure Wasm.empty
       | .some e =>
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index a367b7e..5a9e65c 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -1,4 +1,5 @@
 import Tibi.FinInt
+import Tibi.Semantics
 import Tibi.Syntax
 import Tibi.Util
 
@@ -14,12 +15,18 @@ def Typ.toString : Typ → String
 instance : ToString Typ where
   toString := Typ.toString
 
-inductive HasType : Expr → Typ → Prop
-| Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType (.Const n) .Int64
+def Ty.toTyp : Ty → Typ
+| int => .Int64
 
-def Expr.typeCheck : (e : Expr) → {{ t | HasType e t }}
+inductive HasType (env : Env ctx) : Expr ctx ty → Typ → Prop
+| Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType env (.Const n) .Int64
+| Var {x : Locals i ctx ty} : HasType env (.Var x) ty.toTyp
+
+def Expr.typeCheck (env : Env ctx) : (e : Expr ctx ty) → {{ t | HasType env e t }}
 | .Const n =>
     if h : -Int64.size ≤ n ∧ n < Int64.size then
       .found .Int64 <| .Int64 h.right h.left
     else
       .unknown
+| .Var _ =>
+      .found ty.toTyp .Var
diff --git a/Tibi/Util.lean b/Tibi/Util.lean
index 0c46d05..ed546ec 100644
--- a/Tibi/Util.lean
+++ b/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
+
+infix:67 " :: " => Vec.cons
diff --git a/Tibi/Wasm/Instruction.lean b/Tibi/Wasm/Instruction.lean
index b463e9f..10e3c4d 100644
--- a/Tibi/Wasm/Instruction.lean
+++ b/Tibi/Wasm/Instruction.lean
@@ -10,10 +10,15 @@ open Wasm.Value
 
 inductive Instr
 -- Numeric Instructions
-| i32__const (i : Int32)
-| i64__const (i : Int64)
+| i32.const (i : Int32)
+| i64.const (i : Int64)
+-- Variable Instructions
+| local.get (i : Nat)
+
+def Instr.encode : Instr → List UInt8
+| i32.const i => 0x41 :: i.encode
+| i64.const i => 0x42 :: i.encode
+| local.get i => 0x42 :: (Encoder.encode 128) ++ 0x21 :: Encoder.encode i ++ 0x20 :: Encoder.encode i
 
 instance : Encoder Instr where
-  encode
-    | .i32__const i => 0x41 :: i.encode
-    | .i64__const i => 0x42 :: i.encode
+  encode := Instr.encode
diff --git a/Tibi/Wasm/Module/Basic.lean b/Tibi/Wasm/Module/Basic.lean
index 43fa22c..4a7ecb3 100644
--- a/Tibi/Wasm/Module/Basic.lean
+++ b/Tibi/Wasm/Module/Basic.lean
@@ -49,7 +49,7 @@ def Wasm.simple (c : List Instr) : Wasm :=
   .mk
     [⟨[], [Wasm.ValType.NumType .Int64]⟩]
     [0]
-    [⟨[], c⟩]
+    [⟨[(1, Wasm.ValType.NumType .Int64)], c⟩]
     [⟨"main", .Func 0⟩]
 
 def Wasm.build (w : Wasm) : ByteArray :=
diff --git a/Tibi/Wasm/Semantics/Basic.lean b/Tibi/Wasm/Semantics/Basic.lean
index e83ffc5..78e2ac5 100644
--- a/Tibi/Wasm/Semantics/Basic.lean
+++ b/Tibi/Wasm/Semantics/Basic.lean
@@ -18,6 +18,9 @@ inductive Num
 inductive Value
 | Num (n : Num)
 
+instance : Inhabited Value where
+  default := .Num (.Int64 (Tibi.Int64.ofFin 0))
+
 /- ### Activation Frames -/
 
 structure FrameState where
diff --git a/Tibi/Wasm/Semantics/Reduction.lean b/Tibi/Wasm/Semantics/Reduction.lean
index 6d102e0..c5932a0 100644
--- a/Tibi/Wasm/Semantics/Reduction.lean
+++ b/Tibi/Wasm/Semantics/Reduction.lean
@@ -9,9 +9,12 @@ open Wasm.Value
 /- # Wasm Reduction -/
 
 inductive Reduction : Configuration → Configuration → Prop
-| i32__const {i : Int32} : Reduction
-    { instrs := .i32__const i :: K, stack := s,                             store, framestate }
+| i32.const {i : Int32} : Reduction
+    { instrs := .i32.const i :: K, stack := s,                             store, framestate }
     { instrs := K,                  stack := .Value (.Num (.Int32 i)) :: s, store, framestate }
-| i64__const {i : Int64} : Reduction
-    { instrs := .i64__const i :: K, stack := s,                             store, framestate }
+| i64.const {i : Int64} : Reduction
+    { instrs := .i64.const i :: K, stack := s,                             store, framestate }
     { instrs := K,                  stack := .Value (.Num (.Int64 i)) :: s, store, framestate }
+| local.get (n : Nat) : Reduction
+    { instrs := .local.get n :: K, stack := s,                                      store, framestate }
+    { instrs := K,                  stack := .Value (framestate.locals.get! n) :: s, store, framestate }

From b2e47cdbd2a786c074cecbe9e2c6adda8e044159 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Wed, 1 Jan 2025 19:35:27 +0000
Subject: [PATCH 02/13] lam,app

---
 Tibi/Compiler.lean       | 15 ++++++----
 Tibi/Interpreter.lean    | 22 ++++++++++++---
 Tibi/Parser.lean         | 61 ++++++++++++++++++++++++++--------------
 Tibi/Props/Typing.lean   | 16 ++++++-----
 Tibi/Semantics/Env.lean  |  2 +-
 Tibi/Semantics/Eval.lean | 26 ++++++++++-------
 Tibi/Syntax/Expr.lean    | 22 +++++++++++++--
 Tibi/Top.lean            |  4 +--
 Tibi/Typing.lean         | 33 +++++++++++++++++-----
 Tibi/Util.lean           |  2 +-
 10 files changed, 141 insertions(+), 62 deletions(-)

diff --git a/Tibi/Compiler.lean b/Tibi/Compiler.lean
index 83f173b..7a93743 100644
--- a/Tibi/Compiler.lean
+++ b/Tibi/Compiler.lean
@@ -8,6 +8,14 @@ open Wasm.Value
 
 inductive CompileError
 | OutOfBounds_Int64 (n : Int)
+| Unimplemented
+
+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
 
 def Expr.compile : Expr ctx ty → Except CompileError (List Wasm.Instr)
 | .Const n =>
@@ -17,9 +25,4 @@ def Expr.compile : Expr ctx ty → Except CompileError (List Wasm.Instr)
       .error <| .OutOfBounds_Int64 n
 | .Var x =>
     .ok [.local.get x.idx]
-
-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}"
-
-instance : ToString CompileError where
-  toString := CompileError.toString
+| _ => .error .Unimplemented
diff --git a/Tibi/Interpreter.lean b/Tibi/Interpreter.lean
index 7b5a826..0eb20ff 100644
--- a/Tibi/Interpreter.lean
+++ b/Tibi/Interpreter.lean
@@ -5,12 +5,26 @@ import Tibi.Util
 
 namespace Tibi
 
-def Expr.eval (env : Env ctx) : (e : Expr ctx ty) → {{ r | Eval env 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
+      .found (.ok <| Int64.mk ⟨n, h.right, h.left⟩) <| .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) <| Eval.Var x
+| _, .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
diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index 0151c40..fddde20 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -62,26 +62,45 @@ private def intNumber : Parser Int :=
         | _ => sgn n
   )
 
-private def parser : Parser (Expr .nil/-(.int :: .nil)-/ ty) :=
-  (
-    natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-      |>.map fun (n, _) => .Const n
-  )
-  <|> (
-    intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-      |>.map fun (n, _) => .Const n
-  )
-  -- <|> (
-  --   keyword "it" >> ws
-  --     |>.map fun _ => .Var .stop
-  -- )
-
-instance : Inhabited (Parser (Expr .nil/-(.int :: .nil)-/ ty)) where
-  default := parser
-
-private partial def parse' : ReaderT (IO String) Parser (Expr .nil/-(.int :: .nil)-/ ty) := do
+instance : Inhabited (Parser (Expr .nil .int)) where
+  default := intNumber.map Expr.Const
+
+mutual
+
+  partial def cls (x : Locals i ctx ran) : Parser (Expr ctx <| .cls ran ran) :=
+    (
+      keyword "x" >> ws
+        |>.map fun _ => .Var x
+    )
+
+  partial def fn : Parser (Expr .nil <| .fn .int .int) :=
+    (
+      keyword "fun" >> ws >> keyword "x" >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
+        |>.map fun (_, _, _, _, _, _, e, _) => Expr.Lam e
+    )
+
+  partial def expr : Parser (Expr .nil .int) :=
+    (
+      natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
+        |>.map fun (n, _) => .Const n
+    )
+    <|> (
+      intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
+        |>.map fun (n, _) => .Const n
+    )
+    <|> (
+      fn >> ws >> expr >> ws
+        |>.map fun (f, _, e, _) => .App f e
+    )
+    -- <|> (
+    --   keyword "it" >> ws
+    --     |>.map fun _ => .Var .stop
+    -- )
+end
+
+private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do
   fun getLine cs =>
-    match parser cs with
+    match expr cs with
     | .error .UnexpectedEndOfInput => do
         match getLine () with
         | .ok s _    => parse' getLine <| cs.append s.data
@@ -94,13 +113,13 @@ private partial def parse' : ReaderT (IO String) Parser (Expr .nil/-(.int :: .ni
 -- #eval parse' (pure "9223372036854775808") "".data
 -- #eval parse' (pure "0120") "123".data
 
-def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil/-(.int :: .nil)-/ .int))) :=
+def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil .int))) :=
   stream.getLine >>= pure ∘ fun s =>
     match s.data with
     | [] => none
     | cs => some <| parse' stream.getLine cs
 
-def parseLine (line : String) : Option (ParserT.Result Char Parser.Error Id (Expr .nil/-(.int :: .nil)-/ .int)) :=
+def parseLine (line : String) : Option (ParserT.Result Char Parser.Error Id (Expr .nil .int)) :=
   match line.data with
   | [] => none
   | cs => some <| parse' (pure "") cs
diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index 480f047..bc3b069 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -3,18 +3,19 @@ import Tibi.Typing
 
 namespace Tibi
 
-theorem HasType.det (h₁ : HasType rnv e t₁) (h₂ : HasType env e t₂) : t₁ = t₂ := by
-  cases h₁ <;> cases h₂ <;> rfl
+-- theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+--   cases h₁ <;> cases h₂ <;> rfl
 
+/-
 theorem Expr.typeCheck_correct {e : Expr ctx ty}
-: (ht : HasType env e t) → e.typeCheck env = .found ty.toTyp ht
+: (ht : HasType e t) → e.typeCheck = .found ty.toTyp ht
 | .Int64 (n := n) hLt hGe =>
     have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
     dite_cond_eq_true this
 | .Var => rfl
 
 theorem Expr.typeCheck_complete {e : Expr ctx ty}
-: e.typeCheck env = .unknown → ¬ HasType env e ty.toTyp
+: e.typeCheck = .unknown → ¬ HasType e ty.toTyp
 := by
   dsimp [Expr.typeCheck]
   intro h (ht : HasType env e ty.toTyp)
@@ -23,8 +24,8 @@ theorem Expr.typeCheck_complete {e : Expr ctx ty}
       simp at h
       exact h hGe hLt
 
-instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType env e t) :=
-  match h : e.typeCheck env with
+instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
+  match h : e.typeCheck with
   | .found t' ht' =>
       if heq : t = t' then
         isTrue (heq ▸ ht')
@@ -33,8 +34,9 @@ instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType env e t) :=
   | .unknown => isFalse (Expr.typeCheck_complete h)
 
 theorem type_safe {e : Expr ctx ty}
-: HasType env e t → Eval env e r → ∃ v, r = .ok v
+: HasType e t → Eval e r → ∃ v, r = .ok v
 | .Int64 hLt hGe, .Const ..      => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩
 | .Int64 hLt _,   .ConstErr_lt h => absurd hLt h
 | .Int64 _   hGe, .ConstErr_ge h => absurd hGe h
 | .Var,           .Var x => ⟨env.lookup x, rfl⟩
+-/
diff --git a/Tibi/Semantics/Env.lean b/Tibi/Semantics/Env.lean
index 07dfeff..295e7a3 100644
--- a/Tibi/Semantics/Env.lean
+++ b/Tibi/Semantics/Env.lean
@@ -9,6 +9,6 @@ inductive Env : Vec Ty n → Type where
 
 infix:67 " :: " => Env.cons
 
-def Env.lookup : Locals i ctx ty → Env ctx → ty.interp
+def Env.lookup : Locals i ctx ty → Env ctx → (Ty.cls ty ty).interp
 | .stop,  x :: _  => x
 | .pop k, _ :: xs => xs.lookup k
diff --git a/Tibi/Semantics/Eval.lean b/Tibi/Semantics/Eval.lean
index 8923869..782f389 100644
--- a/Tibi/Semantics/Eval.lean
+++ b/Tibi/Semantics/Eval.lean
@@ -7,18 +7,24 @@ namespace Tibi
 inductive EvalError
 | OutOfBounds_Int64 (n : Int)
 
-inductive Eval (env : Env ctx) : (Expr ctx ty) → Except EvalError Int64 → Prop
-| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
-  : Eval env (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
-| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
-  : Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
-| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
-  : Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
-| Var (x : Locals i ctx ty)
-  : Eval env (.Var x) (.ok (env.lookup x))
-
 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}"
 
 instance : ToString EvalError where
   toString := EvalError.toString
+
+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' (env : Env (α :: .nil)) (a : α.interp) -- {x : Locals 0 (a :: ctx) a}
+--   : Eval (.Var Locals.stop) (.ok <| a)
+| 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₁)
diff --git a/Tibi/Syntax/Expr.lean b/Tibi/Syntax/Expr.lean
index 9dbe863..e54b8e6 100644
--- a/Tibi/Syntax/Expr.lean
+++ b/Tibi/Syntax/Expr.lean
@@ -5,13 +5,25 @@ namespace Tibi
 
 inductive Ty where
 | int
+| fn (a b : Ty)
+| cls (a b : Ty)
 
 @[reducible]
 def Ty.interp : Ty → Type
-| int => Int64
+| 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"
+| int    => "Int"
+| fn a b => s!"{a.toString} -> {b.toString}"
+| cls _ b => s!"{b.toString}"
 
 instance : ToString Ty where
   toString := Ty.toString
@@ -29,11 +41,15 @@ instance : ToString (Locals n ctx ty) where
 
 inductive Expr : Vec Ty n → Ty → Type where
 | Const : Int → Expr ctx .int
-| Var   : Locals i ctx ty → Expr ctx ty
+| 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
diff --git a/Tibi/Top.lean b/Tibi/Top.lean
index 173f55e..b7b9f71 100644
--- a/Tibi/Top.lean
+++ b/Tibi/Top.lean
@@ -12,9 +12,9 @@ partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
     if let some r := parseLine line then
       match r with
       | .ok (expr, []) =>
-          match expr.typeCheck .nil with
+          match expr.typeCheck with
           | .found t _ =>
-              match expr.eval .nil 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)"
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index 5a9e65c..d35d7f5 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -7,26 +7,45 @@ namespace Tibi
 
 inductive Typ
 | Int64
+| Fn (a : Typ) (b : Typ)
 deriving DecidableEq
 
 def Typ.toString : Typ → String
-| Int64 => "Int"
+| Int64  => "Int"
+| Fn a b => s!"{a.toString} -> {b.toString}"
 
 instance : ToString Typ where
   toString := Typ.toString
 
 def Ty.toTyp : Ty → Typ
-| int => .Int64
+| int     => .Int64
+| fn a b  => .Fn a.toTyp b.toTyp
+| cls _ b => b.toTyp
 
-inductive HasType (env : Env ctx) : Expr ctx ty → Typ → Prop
-| Int64 {n : Int} (hLt : n < Int64.size) (hGe : n ≥ -Int64.size) : HasType env (.Const n) .Int64
-| Var {x : Locals i ctx ty} : HasType env (.Var x) ty.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 dom t)
+| App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran
 
-def Expr.typeCheck (env : Env ctx) : (e : Expr ctx ty) → {{ t | HasType env 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 ty.toTyp .Var
+    .found _ .Var
+| .Lam e =>
+    match e.typeCheck with
+    | .found t h => .found (.Fn .Int64 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
+-- | _ => .unknown
diff --git a/Tibi/Util.lean b/Tibi/Util.lean
index ed546ec..f088589 100644
--- a/Tibi/Util.lean
+++ b/Tibi/Util.lean
@@ -14,4 +14,4 @@ inductive Vec (α : Type u) : Nat → Type u
 | nil : Vec α 0
 | cons : α → Vec α n → Vec α n.succ
 
-infix:67 " :: " => Vec.cons
+infixr:67 " :: " => Vec.cons

From f8db994bb38da2c54cd3468539e47e01339243ad Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Wed, 1 Jan 2025 19:49:52 +0000
Subject: [PATCH 03/13] fold Unit results

---
 Tibi/Parser.lean             |  8 ++++----
 Tibi/ParserT/Combinator.lean | 16 ++++++++++++++++
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index fddde20..ab4c5a9 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -76,21 +76,21 @@ mutual
   partial def fn : Parser (Expr .nil <| .fn .int .int) :=
     (
       keyword "fun" >> ws >> keyword "x" >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
-        |>.map fun (_, _, _, _, _, _, e, _) => Expr.Lam e
+        |>.map fun e => Expr.Lam e
     )
 
   partial def expr : Parser (Expr .nil .int) :=
     (
       natNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-        |>.map fun (n, _) => .Const n
+        |>.map fun n => .Const n
     )
     <|> (
       intNumber >> ws -- >> ParserT.optional ((ParserT.char '@' : Parser _) >> keyword "Int" >> ws)
-        |>.map fun (n, _) => .Const n
+        |>.map fun n => .Const n
     )
     <|> (
       fn >> ws >> expr >> ws
-        |>.map fun (f, _, e, _) => .App f e
+        |>.map fun (f, e) => .App f e
     )
     -- <|> (
     --   keyword "it" >> ws
diff --git a/Tibi/ParserT/Combinator.lean b/Tibi/ParserT/Combinator.lean
index 1ec96dd..5e7190e 100644
--- a/Tibi/ParserT/Combinator.lean
+++ b/Tibi/ParserT/Combinator.lean
@@ -13,6 +13,22 @@ def hAndThen (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : Parser
 instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m β) (ParserT σ ε m (α × β)) where
   hAndThen := hAndThen
 
+def hAndThen' (p : ParserT σ ε m Unit) (q : Unit → ParserT σ ε m β) : ParserT σ ε m β :=
+  p
+  >>= fun _ => q ()
+  >>= fun b => ParserT.ok b
+
+instance : HAndThen (ParserT σ ε m Unit) (ParserT σ ε m β) (ParserT σ ε m β) where
+  hAndThen := hAndThen'
+
+def hAndThen'' (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m Unit) : ParserT σ ε m α :=
+  p
+  >>= fun a => q ()
+  >>= fun _ => ParserT.ok a
+
+instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m Unit) (ParserT σ ε m α) where
+  hAndThen := hAndThen''
+
 -- def hOrElse (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : ParserT σ ε m (α ⊕ β) :=
 --   fun cs =>
 --     ExceptT.tryCatch

From e22c88f87a8707b011581852f45b9aa57124c8b1 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Wed, 1 Jan 2025 19:54:38 +0000
Subject: [PATCH 04/13] refactoring

---
 Tibi/ParserT/Combinator.lean | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/Tibi/ParserT/Combinator.lean b/Tibi/ParserT/Combinator.lean
index 5e7190e..5ea43ee 100644
--- a/Tibi/ParserT/Combinator.lean
+++ b/Tibi/ParserT/Combinator.lean
@@ -13,21 +13,11 @@ def hAndThen (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : Parser
 instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m β) (ParserT σ ε m (α × β)) where
   hAndThen := hAndThen
 
-def hAndThen' (p : ParserT σ ε m Unit) (q : Unit → ParserT σ ε m β) : ParserT σ ε m β :=
-  p
-  >>= fun _ => q ()
-  >>= fun b => ParserT.ok b
-
 instance : HAndThen (ParserT σ ε m Unit) (ParserT σ ε m β) (ParserT σ ε m β) where
-  hAndThen := hAndThen'
-
-def hAndThen'' (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m Unit) : ParserT σ ε m α :=
-  p
-  >>= fun a => q ()
-  >>= fun _ => ParserT.ok a
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.snd
 
 instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m Unit) (ParserT σ ε m α) where
-  hAndThen := hAndThen''
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.fst
 
 -- def hOrElse (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : ParserT σ ε m (α ⊕ β) :=
 --   fun cs =>

From c6182dffb69aacf1d03fbd30b8fda8fb7ee107f8 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Thu, 2 Jan 2025 02:27:55 +0000
Subject: [PATCH 05/13] HasType.det

---
 Tibi/Props/Typing.lean |  7 +++++--
 Tibi/Typing.lean       | 10 ++++++----
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index bc3b069..27d3d19 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -3,8 +3,11 @@ import Tibi.Typing
 
 namespace Tibi
 
--- theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
---   cases h₁ <;> cases h₂ <;> rfl
+theorem HasType.det : HasType e t₁ → HasType e t₂ → t₁ = t₂
+| .Int64 ..,  .Int64 ..    => rfl
+| .Var,       .Var         => rfl
+| .Lam h,     .Lam h'      => by rw [h.det h']
+| .App h₁ h₂, .App h₁' h₂' => h₂.det h₂' ▸ h₁.det h₁' |> Typ.Fn.inj |>.right
 
 /-
 theorem Expr.typeCheck_correct {e : Expr ctx ty}
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index d35d7f5..cbf84e9 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -6,13 +6,15 @@ 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"
-| Fn a b => s!"{a.toString} -> {b.toString}"
+| Var idx => s!"α{idx}"
+| Int64   => "Int"
+| Fn a b  => s!"{a.toString} -> {b.toString}"
 
 instance : ToString Typ where
   toString := Typ.toString
@@ -25,7 +27,7 @@ def Ty.toTyp : Ty → Typ
 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 dom t)
+| 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 ctx ty) → {{ t | HasType e t }}
@@ -38,7 +40,7 @@ def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }}
     .found _ .Var
 | .Lam e =>
     match e.typeCheck with
-    | .found t h => .found (.Fn .Int64 t) <| .Lam h
+    | .found t h => .found (.Fn (.Var 0) t) <| .Lam h
     | .unknown   => .unknown
 | .App f v =>
     match f.typeCheck, v.typeCheck with

From 2c413cab96b8b37023ac809b947ca1fb19654794 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Thu, 2 Jan 2025 02:36:29 +0000
Subject: [PATCH 06/13] typeCheck_correct

---
 Tibi/Props/Typing.lean | 28 ++++++++++++++++++++++------
 1 file changed, 22 insertions(+), 6 deletions(-)

diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index 27d3d19..803c02c 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -9,14 +9,30 @@ theorem HasType.det : HasType e t₁ → HasType e t₂ → t₁ = t₂
 | .Lam h,     .Lam h'      => by rw [h.det h']
 | .App h₁ h₂, .App h₁' h₂' => h₂.det h₂' ▸ h₁.det h₁' |> Typ.Fn.inj |>.right
 
-/-
+/--
+Reference: [A Certified Type Checker \- Lean Documentation Overview](https://lean-lang.org/lean4/doc/examples/tc.lean.html)
+-/
 theorem Expr.typeCheck_correct {e : Expr ctx ty}
-: (ht : HasType e t) → e.typeCheck = .found ty.toTyp ht
-| .Int64 (n := n) hLt hGe =>
-    have := eq_true <| And.intro (ge_iff_le.mp hGe) hLt
-    dite_cond_eq_true this
-| .Var => rfl
+  (ht : HasType e t)
+  (h : e.typeCheck ≠ .unknown)
+: e.typeCheck = .found t ht
+:= by
+  revert h
+  match e.typeCheck with
+  | .found ty' h₁' => intro ; have := ht.det h₁' ; subst this ; rfl
+  | .unknown       => intros; contradiction
+/-
+Try this: (match e.typeCheck with
+  | Maybe.found ty' h₁' => fun h =>
+    let_fun this := HasType.det ht h₁';
+    Eq.ndrec (motive := fun ty' =>
+      ∀ (h₁' : HasType e ty'), Maybe.found ty' h₁' ≠ Maybe.unknown → Maybe.found ty' h₁' = Maybe.found t ht)
+      (fun h₁' h => Eq.refl (Maybe.found t h₁')) this h₁' h
+  | Maybe.unknown => fun h => absurd (Eq.refl Maybe.unknown) h)
+  h
+-/
 
+/-
 theorem Expr.typeCheck_complete {e : Expr ctx ty}
 : e.typeCheck = .unknown → ¬ HasType e ty.toTyp
 := by

From 9d8834d32a5ce765b4e7491915d711caf94b3a39 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 00:49:31 +0000
Subject: [PATCH 07/13] try to prove Expr.typeCheck_complete but now incomplete
 yet...

---
 Tibi/Props/Typing.lean | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index 803c02c..c65c440 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -34,15 +34,28 @@ Try this: (match e.typeCheck with
 
 /-
 theorem Expr.typeCheck_complete {e : Expr ctx ty}
-: e.typeCheck = .unknown → ¬ HasType e ty.toTyp
+: e.typeCheck = .unknown → ¬HasType e t
 := by
-  dsimp [Expr.typeCheck]
-  intro h (ht : HasType env e ty.toTyp)
-  match ht with
-  | .Int64 hLt hGe =>
-      simp at h
-      exact h hGe hLt
+  induction e with simp [Expr.typeCheck]
+  | Const n =>
+      intro h ht
+      match ht with
+      | .Int64 hLt hGe =>
+          have := h hGe hLt
+          contradiction
+  | Lam e ih =>
+      match h : e.typeCheck with
+      | .found t' ht' => intro ; contradiction
+      | .unknown =>
+          have : ¬HasType e t := ih h
+          intro _ ht'
+          match ht' with
+          | .Lam h' =>
+              sorry
+  | App e₁ e₂ ih₁ ih₂ => sorry
+-/
 
+/-
 instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
   match h : e.typeCheck with
   | .found t' ht' =>
@@ -51,7 +64,9 @@ instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
       else
         isFalse fun ht => heq (HasType.det ht ht')
   | .unknown => isFalse (Expr.typeCheck_complete h)
+-/
 
+/-
 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⟩

From 58ea6126316a4ed4cf29c7b2aa7a9aa77bee90a3 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 03:39:31 +0000
Subject: [PATCH 08/13] add todos

---
 .github/workflows/todo-to-issue.yml | 11 +++++++++++
 .todo-to-issue-languages.json       | 21 +++++++++++++++++++++
 Tibi/Props/Compiler.lean            |  1 +
 Tibi/Props/Typing.lean              |  3 +++
 Tibi/Wasm/Module/Basic.lean         |  2 +-
 5 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/todo-to-issue.yml
 create mode 100644 .todo-to-issue-languages.json

diff --git a/.github/workflows/todo-to-issue.yml b/.github/workflows/todo-to-issue.yml
new file mode 100644
index 0000000..da1919f
--- /dev/null
+++ b/.github/workflows/todo-to-issue.yml
@@ -0,0 +1,11 @@
+name: "Run TODO to Issue"
+on: [ "push" ]
+jobs:
+  build:
+    runs-on: "ubuntu-latest"
+    steps:
+      - uses: "actions/checkout@v4"
+      - name: "TODO to Issue"
+        uses: "alstr/todo-to-issue-action@v5"
+        with:
+            LANGUAGES: ".todo-to-issue-languages.json"
diff --git a/.todo-to-issue-languages.json b/.todo-to-issue-languages.json
new file mode 100644
index 0000000..e787115
--- /dev/null
+++ b/.todo-to-issue-languages.json
@@ -0,0 +1,21 @@
+[
+  {
+    "language": "Lean 4",
+    "extensions": [
+      ".lean"
+    ],
+    "markers": [
+      {
+        "type": "line",
+        "pattern": "--"
+      },
+      {
+        "type": "block",
+        "pattern": {
+          "start": "/-",
+          "end": "-/"
+        }
+      }
+    ]
+  }
+]
\ No newline at end of file
diff --git a/Tibi/Props/Compiler.lean b/Tibi/Props/Compiler.lean
index 99cd74e..707f6b3 100644
--- a/Tibi/Props/Compiler.lean
+++ b/Tibi/Props/Compiler.lean
@@ -4,6 +4,7 @@ import Tibi.Wasm.Semantics
 
 namespace Tibi
 
+-- TODO prove Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok
 /-
 type mismatch
   Wasm.Reduction.local__get ↑x.idx
diff --git a/Tibi/Props/Typing.lean b/Tibi/Props/Typing.lean
index c65c440..d8e3b97 100644
--- a/Tibi/Props/Typing.lean
+++ b/Tibi/Props/Typing.lean
@@ -32,6 +32,7 @@ Try this: (match e.typeCheck with
   h
 -/
 
+-- TODO prove Expr.typeCheck_complete
 /-
 theorem Expr.typeCheck_complete {e : Expr ctx ty}
 : e.typeCheck = .unknown → ¬HasType e t
@@ -55,6 +56,7 @@ theorem Expr.typeCheck_complete {e : Expr ctx ty}
   | App e₁ e₂ ih₁ ih₂ => sorry
 -/
 
+-- TODO prove : Decidable (HasType e t)
 /-
 instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
   match h : e.typeCheck with
@@ -66,6 +68,7 @@ instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
   | .unknown => isFalse (Expr.typeCheck_complete h)
 -/
 
+-- TODO prove type_safe
 /-
 theorem type_safe {e : Expr ctx ty}
 : HasType e t → Eval e r → ∃ v, r = .ok v
diff --git a/Tibi/Wasm/Module/Basic.lean b/Tibi/Wasm/Module/Basic.lean
index 4a7ecb3..4d13cbf 100644
--- a/Tibi/Wasm/Module/Basic.lean
+++ b/Tibi/Wasm/Module/Basic.lean
@@ -36,7 +36,7 @@ open Wasm (Code Export FuncType Section)
 def Wasm.magic : List UInt8 := [0x00, 0x61, 0x73, 0x6D]
 def Wasm.version : List UInt8 := [0x01, 0x00, 0x00, 0x00]
 
--- TODO https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module
+-- XXX https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module
 structure Wasm where
   types : List FuncType
   funcs : List Nat

From 0c8fdff0ef4d84c2240d4084dc4477180a1ff04e Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 03:43:23 +0000
Subject: [PATCH 09/13] enable URL insertion and closing TODOs

---
 .github/workflows/todo-to-issue.yml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/todo-to-issue.yml b/.github/workflows/todo-to-issue.yml
index da1919f..fe89a87 100644
--- a/.github/workflows/todo-to-issue.yml
+++ b/.github/workflows/todo-to-issue.yml
@@ -8,4 +8,20 @@ jobs:
       - name: "TODO to Issue"
         uses: "alstr/todo-to-issue-action@v5"
         with:
-            LANGUAGES: ".todo-to-issue-languages.json"
+          INSERT_ISSUE_URLS: "true"
+          CLOSE_ISSUES: "true"
+          LANGUAGES: ".todo-to-issue-languages.json"
+      - name: Set Git user
+        run: |
+          git config --global user.name "github-actions[bot]"
+          git config --global user.email "github-actions[bot]@users.noreply.github.com"
+      - name: Commit and Push Changes
+        run: |
+          git add -A
+          if [[ `git status --porcelain` ]]; then
+            git commit -m "Automatically added GitHub issue links to TODOs"
+            git push origin main
+          else
+            echo "No changes to commit"
+          fi
+

From 73ef4136b5eedc29bf7940b821c7fbfd08b4720a Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 03:48:45 +0000
Subject: [PATCH 10/13] fix

---
 Tibi/Wasm/Module/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Tibi/Wasm/Module/Basic.lean b/Tibi/Wasm/Module/Basic.lean
index 4d13cbf..64bc885 100644
--- a/Tibi/Wasm/Module/Basic.lean
+++ b/Tibi/Wasm/Module/Basic.lean
@@ -49,7 +49,7 @@ def Wasm.simple (c : List Instr) : Wasm :=
   .mk
     [⟨[], [Wasm.ValType.NumType .Int64]⟩]
     [0]
-    [⟨[(1, Wasm.ValType.NumType .Int64)], c⟩]
+    [⟨[], c⟩]
     [⟨"main", .Func 0⟩]
 
 def Wasm.build (w : Wasm) : ByteArray :=

From 445809d45c88e137b6903be0d47008479f4f0d0d Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 06:31:29 +0000
Subject: [PATCH 11/13] wip

---
 Tibi/Parser.lean | 21 +++++++++------------
 Tibi/Top.lean    |  2 +-
 Tibi/Typing.lean |  4 ++--
 3 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index ab4c5a9..bb6c8d3 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -62,20 +62,23 @@ private def intNumber : Parser Int :=
         | _ => sgn n
   )
 
-instance : Inhabited (Parser (Expr .nil .int)) where
+private def enclose (pre : String) (p : Parser α) (post : String) : Parser α :=
+  keyword pre >> ws >> p >> ws >> keyword post
+
+instance : Inhabited (Parser (Expr ctx .int)) where
   default := intNumber.map Expr.Const
 
 mutual
 
-  partial def cls (x : Locals i ctx ran) : Parser (Expr ctx <| .cls ran ran) :=
+  partial def cls (x : Locals i ctx dom) : Parser (Expr ctx (.cls dom dom)) :=
     (
-      keyword "x" >> ws
+      keyword "$x" >> ws
         |>.map fun _ => .Var x
     )
 
-  partial def fn : Parser (Expr .nil <| .fn .int .int) :=
+  partial def fn : Parser (Expr ctx (.fn .int .int)) :=
     (
-      keyword "fun" >> ws >> keyword "x" >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
+      keyword "$" >> keyword "x" >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
         |>.map fun e => Expr.Lam e
     )
 
@@ -89,7 +92,7 @@ mutual
         |>.map fun n => .Const n
     )
     <|> (
-      fn >> ws >> expr >> ws
+      enclose "(" fn ")" >> ws >> expr >> ws
         |>.map fun (f, e) => .App f e
     )
     -- <|> (
@@ -107,12 +110,6 @@ private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do
         | .error e _ => Except.error <| Parser.Error.IOError e
     | v => v
 
--- #eval parse' (pure "0120") "123".data
--- #eval parse' (pure "-1") "".data
--- #eval parse' (pure "9223372036854775808") "".data
--- #eval parse' (pure "9223372036854775808") "".data
--- #eval parse' (pure "0120") "123".data
-
 def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil .int))) :=
   stream.getLine >>= pure ∘ fun s =>
     match s.data with
diff --git a/Tibi/Top.lean b/Tibi/Top.lean
index b7b9f71..3c613b3 100644
--- a/Tibi/Top.lean
+++ b/Tibi/Top.lean
@@ -6,7 +6,7 @@ import Tibi.Typing
 namespace Tibi
 
 partial def repl (stream : IO.FS.Stream) (n : Nat := 0) : IO UInt32 := do
-  IO.print s!"{n}:> "
+  if ← stream.isTty then IO.print s!"{n}:> "
   let line ← stream.getLine
   if not line.isEmpty then
     if let some r := parseLine line then
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index cbf84e9..6108431 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -27,7 +27,7 @@ def Ty.toTyp : Ty → Typ
 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)
+| Lam (h : HasType e t) : HasType (.Lam e) (.Fn .Int64/-(.Var 0)-/ t)
 | App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran
 
 def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }}
@@ -40,7 +40,7 @@ def Expr.typeCheck : (e : Expr ctx ty) → {{ t | HasType e t }}
     .found _ .Var
 | .Lam e =>
     match e.typeCheck with
-    | .found t h => .found (.Fn (.Var 0) t) <| .Lam h
+    | .found t h => .found (.Fn .Int64/-(.Var 0)-/ t) <| .Lam h
     | .unknown   => .unknown
 | .App f v =>
     match f.typeCheck, v.typeCheck with

From 7b6689b9356bb5bb9383bf033d1c934d7aeeac20 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 07:38:43 +0000
Subject: [PATCH 12/13] fix EOF

---
 Tibi/Parser.lean | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index bb6c8d3..756a345 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -104,10 +104,25 @@ end
 private partial def parse' : ReaderT (IO String) Parser (Expr .nil .int) := do
   fun getLine cs =>
     match expr cs with
-    | .error .UnexpectedEndOfInput => do
+    | .ok (e, []) =>
         match getLine () with
-        | .ok s _    => parse' getLine <| cs.append s.data
-        | .error e _ => Except.error <| Parser.Error.IOError e
+        | .ok s _    =>
+            if s.isEmpty then
+              .ok (e, [])
+            else
+              .error $ .ExpectedEndOfInput s.trimRight.data
+        | .error e _ =>
+            .error $ Parser.Error.IOError e
+    | .ok (_, cs) =>
+        .error $ .ExpectedEndOfInput cs
+    | .error .UnexpectedEndOfInput => -- continue to parse furthermore
+        match getLine () with
+        | .ok s _    =>
+            if s.isEmpty then
+              .error $ .UnexpectedEndOfInput
+            else
+              parse' getLine $ cs.append s.data
+        | .error e _ => .error $ Parser.Error.IOError e
     | v => v
 
 def parse (stream : IO.FS.Stream): IO (Option (ParserT.Result Char Parser.Error Id (Expr .nil .int))) :=

From 4fcfb7618f5e2034d6838776005b1f38fb6163a1 Mon Sep 17 00:00:00 2001
From: Junichi Hayashi <2093896+nahcnuj@users.noreply.github.com>
Date: Fri, 3 Jan 2025 09:48:57 +0000
Subject: [PATCH 13/13] fix lam,app

---
 Tibi/Interpreter.lean    | 29 ++++++++++++++++------------
 Tibi/Parser.lean         | 41 +++++++++++++++++++++++++++++-----------
 Tibi/Semantics/Env.lean  |  2 +-
 Tibi/Semantics/Eval.lean |  4 ++--
 Tibi/Syntax/Expr.lean    | 20 ++++++++------------
 Tibi/Typing.lean         |  3 +--
 6 files changed, 59 insertions(+), 40 deletions(-)

diff --git a/Tibi/Interpreter.lean b/Tibi/Interpreter.lean
index 0eb20ff..2a86948 100644
--- a/Tibi/Interpreter.lean
+++ b/Tibi/Interpreter.lean
@@ -15,16 +15,21 @@ def Expr.eval (env : Env ctx) : {ty : Ty} → (e : Expr ctx ty) → ty.dom → {
         (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
+| .fn _ .int, .Lam e', x =>
+    match e'.eval (x :: env) () 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
+    | _                => .unknown
+| .int, .App (dom := dom) e₁ e₂, _ =>
+    match dom with
+    | .int => -- dom.dom = Unit
+        match e₂.eval env () with
+        | .found (.ok v) h₂ =>
+            match e₁.eval env v with
+            | .found (.ok f) h₁ => .found (.ok (f v)) <| .App h₁ h₂
+            | _                 => .unknown
+        | _ =>
+            .unknown
+    | _ =>
+        .unknown
+| _, _, _ =>
+    .unknown
diff --git a/Tibi/Parser.lean b/Tibi/Parser.lean
index 756a345..0616655 100644
--- a/Tibi/Parser.lean
+++ b/Tibi/Parser.lean
@@ -4,16 +4,20 @@ import Tibi.Syntax
 namespace Tibi
 
 inductive Parser.Error
-| ExpectedDigit (got : Char)
-| ExpectedNonZeroDigit (got : Char)
-| IOError (e : IO.Error)
+| ExpectedAsciiAlpha    (got : Char)
+| ExpectedAsciiAlphaNum (got : Char)
+| ExpectedDigit         (got : Char)
+| ExpectedNonZeroDigit  (got : Char)
+| IOError               (e : IO.Error)
 | Unconsumed (rest : String)
 
 def Parser.Error.toString : Parser.Error → String
-| ExpectedDigit got        => s!"Expected a digit, got '{got}'"
-| ExpectedNonZeroDigit got => s!"Expected a non-zero digit, got '{got}'"
-| IOError e                => s!"IO Error: {e}"
-| Unconsumed rest          => s!"\"{rest}\" was not consumed"
+| ExpectedAsciiAlpha got    => s!"Expected an ASCII alphabet character, got '{got}'"
+| ExpectedAsciiAlphaNum got => s!"Expected an ASCII alphanumeric character, got '{got}'"
+| ExpectedDigit got         => s!"Expected a digit, got '{got}'"
+| ExpectedNonZeroDigit got  => s!"Expected a non-zero digit, got '{got}'"
+| IOError e                 => s!"IO Error: {e}"
+| Unconsumed rest           => s!"\"{rest}\" was not consumed"
 
 instance : ToString Parser.Error where
   toString := Parser.Error.toString
@@ -65,21 +69,36 @@ private def intNumber : Parser Int :=
 private def enclose (pre : String) (p : Parser α) (post : String) : Parser α :=
   keyword pre >> ws >> p >> ws >> keyword post
 
+private def asciiAlpha : Parser Char :=
+  ParserT.satisfy Char.isAlpha .ExpectedAsciiAlpha
+
+private def asciiAlphanum : Parser Char :=
+  ParserT.satisfy Char.isAlphanum .ExpectedAsciiAlphaNum
+
+private def ident : Parser String :=
+  (
+    asciiAlpha >> ParserT.repeatGreedily asciiAlphanum
+      |>.map fun (c, cs) => String.mk (c :: cs)
+  )
+
+private def var : Parser String :=
+  keyword "$" >> ident
+
 instance : Inhabited (Parser (Expr ctx .int)) where
   default := intNumber.map Expr.Const
 
 mutual
 
-  partial def cls (x : Locals i ctx dom) : Parser (Expr ctx (.cls dom dom)) :=
+  partial def cls (x : Locals i ctx dom) : Parser (Expr ctx dom) :=
     (
-      keyword "$x" >> ws
+      var >> ws
         |>.map fun _ => .Var x
     )
 
   partial def fn : Parser (Expr ctx (.fn .int .int)) :=
     (
-      keyword "$" >> keyword "x" >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
-        |>.map fun e => Expr.Lam e
+      var >> ws >> keyword "." >> ws >> cls (Locals.stop) >> ws
+        |>.map fun (_, e) => Expr.Lam e
     )
 
   partial def expr : Parser (Expr .nil .int) :=
diff --git a/Tibi/Semantics/Env.lean b/Tibi/Semantics/Env.lean
index 295e7a3..07dfeff 100644
--- a/Tibi/Semantics/Env.lean
+++ b/Tibi/Semantics/Env.lean
@@ -9,6 +9,6 @@ inductive Env : Vec Ty n → Type where
 
 infix:67 " :: " => Env.cons
 
-def Env.lookup : Locals i ctx ty → Env ctx → (Ty.cls ty ty).interp
+def Env.lookup : Locals i ctx ty → Env ctx → ty.interp
 | .stop,  x :: _  => x
 | .pop k, _ :: xs => xs.lookup k
diff --git a/Tibi/Semantics/Eval.lean b/Tibi/Semantics/Eval.lean
index 782f389..8d79037 100644
--- a/Tibi/Semantics/Eval.lean
+++ b/Tibi/Semantics/Eval.lean
@@ -26,5 +26,5 @@ inductive Eval : (Expr ctx ty) → Except EvalError ty.interp → Prop
   : 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₁)
+| App (d₁ : Eval e₁ (.ok f)) (d₂ : Eval e₂ (.ok x))
+  : Eval (.App e₁ e₂) (.ok <| f x)
diff --git a/Tibi/Syntax/Expr.lean b/Tibi/Syntax/Expr.lean
index e54b8e6..795ebbc 100644
--- a/Tibi/Syntax/Expr.lean
+++ b/Tibi/Syntax/Expr.lean
@@ -6,24 +6,20 @@ namespace Tibi
 inductive Ty where
 | int
 | fn (a b : Ty)
-| cls (a b : Ty)
 
 @[reducible]
 def Ty.interp : Ty → Type
-| int    => Int64
-| fn a b => a.interp → b.interp
-| cls _ b => b.interp
+| int     => Int64
+| fn a b  => a.interp → b.interp
 
 @[reducible]
 def Ty.dom : Ty → Type
-| int => Unit
-| fn a _ => a.interp
-| cls a _ => a.interp
+| int     => Unit
+| fn a _  => a.interp
 
 def Ty.toString : Ty → String
-| int    => "Int"
-| fn a b => s!"{a.toString} -> {b.toString}"
-| cls _ b => s!"{b.toString}"
+| int     => "Int"
+| fn a b  => s!"{a.toString} -> {b.toString}"
 
 instance : ToString Ty where
   toString := Ty.toString
@@ -41,8 +37,8 @@ instance : ToString (Locals n ctx ty) where
 
 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)
+| Var   : Locals i ctx ty → Expr ctx ty
+| Lam   : Expr (dom :: ctx) 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
diff --git a/Tibi/Typing.lean b/Tibi/Typing.lean
index 6108431..3812676 100644
--- a/Tibi/Typing.lean
+++ b/Tibi/Typing.lean
@@ -22,11 +22,10 @@ instance : ToString Typ where
 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
+| Var {x : Locals i ctx ty} : HasType (.Var x) ty.toTyp
 | Lam (h : HasType e t) : HasType (.Lam e) (.Fn .Int64/-(.Var 0)-/ t)
 | App (hf : HasType f (.Fn dom ran)) (hv : HasType v dom) : HasType (.App f v) ran