Functions

.github/workflows/todo-to-issue.yml

@@ -0,0 +1,27 @@
+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:
+          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
+

.todo-to-issue-languages.json

@@ -0,0 +1,21 @@
+[
+  {
+    "language": "Lean 4",
+    "extensions": [
+      ".lean"
+    ],
+    "markers": [
+      {
+        "type": "line",
+        "pattern": "--"
+      },
+      {
+        "type": "block",
+        "pattern": {
+          "start": "/-",
+          "end": "-/"
+        }
+      }
+    ]
+  }
+]

Tibi/Compiler.lean

@@ -8,16 +8,21 @@ open Wasm.Value
 
 inductive CompileError
 | OutOfBounds_Int64 (n : Int)
-
-def Expr.compile : Expr → 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
+| 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 =>
+    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 x =>
+    .ok [.local.get x.idx]
+| _ => .error .Unimplemented

Tibi/Interpreter.lean

@@ -5,11 +5,31 @@ 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
+      .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) <| .Var x env
+| .fn _ .int, .Lam e', x =>
+    match e'.eval (x :: env) () with
+    | .found (.ok v) h => .found (.ok <| fun _ => v) <| .Lam h
+    | _                => .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

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
@@ -62,41 +66,91 @@ private def intNumber : Parser Int :=
         | _ => sgn n
   )
 
-private def parser : Parser Expr :=
+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 :=
   (
-    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
+    asciiAlpha >> ParserT.repeatGreedily asciiAlphanum
+      |>.map fun (c, cs) => String.mk (c :: cs)
   )
 
-instance : Inhabited (Parser Expr) where
-  default := parser
-
-private partial def parse' : ReaderT (IO String) Parser Expr := do
+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 dom) :=
+    (
+      var >> ws
+        |>.map fun _ => .Var x
+    )
+
+  partial def fn : Parser (Expr ctx (.fn .int .int)) :=
+    (
+      var >> 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
+    )
+    <|> (
+      enclose "(" 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
-    | .error .UnexpectedEndOfInput => do
+    match expr cs with
+    | .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
 
--- #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) :=
+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) :=
+def parseLine (line : String) : Option (ParserT.Result Char Parser.Error Id (Expr .nil .int)) :=
   match line.data with
   | [] => none
   | cs => some <| parse' (pure "") cs

Tibi/ParserT/Combinator.lean

@@ -13,6 +13,12 @@ def hAndThen (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : Parser
 instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m β) (ParserT σ ε m (α × β)) where
   hAndThen := hAndThen
 
+instance : HAndThen (ParserT σ ε m Unit) (ParserT σ ε m β) (ParserT σ ε m β) where
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.snd
+
+instance : HAndThen (ParserT σ ε m α) (ParserT σ ε m Unit) (ParserT σ ε m α) where
+  hAndThen p q := p.hAndThen q >>= pure ∘ Prod.fst
+
 -- def hOrElse (p : ParserT σ ε m α) (q : Unit → ParserT σ ε m β) : ParserT σ ε m (α ⊕ β) :=
 --   fun cs =>
 --     ExceptT.tryCatch

Tibi/Props/Compiler.lean

@@ -4,15 +4,36 @@ 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}
+-- TODO prove Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok
+/-
+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
+-/