From b8649575091908ecc91d853978858d512efad311 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sun, 8 Jan 2023 15:22:30 -0300
Subject: [PATCH 01/16] Yul AST

---
 Yatima/Compiler/yul.lean | 56 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 Yatima/Compiler/yul.lean

diff --git a/Yatima/Compiler/yul.lean b/Yatima/Compiler/yul.lean
new file mode 100644
index 00000000..5979b9a0
--- /dev/null
+++ b/Yatima/Compiler/yul.lean
@@ -0,0 +1,56 @@
+-- This is based on Yul's specification https://docs.soliditylang.org/en/v0.8.17/yul.html#specification-of-yul
+namespace Yul
+
+-- Yul currently only supports the u256 type, but other types might be added in the future
+inductive PrimType where
+| u256
+
+def Identifier := String
+structure TypedIdentifier where
+  identifier : Identifier
+  type       : Option PrimType
+
+inductive Literal where
+-- Actually it should be a u256
+| number : PrimType → Nat → Literal
+| string : PrimType → String → Literal
+| true   : PrimType → Literal
+| false  : PrimType → Literal
+
+inductive Expression where
+| functionCall : Identifier → List Expression → Expression
+| identifier   : Identifier → Expression
+| literal      : Literal → Expression
+
+inductive BreakContinue
+| «break»
+| «continue»
+
+structure NonemptyList (α : Type u) where
+  head : α
+  tail : List α
+
+mutual
+
+inductive Block where
+| mk : List Statement → Block
+
+inductive Switch where
+| case    : Expression → NonemptyList (Literal × Block) → Option Block → Switch
+| default : Expression → Block → Switch
+
+inductive Statement where
+| block               : Block → Statement
+| functionDefinition  : Identifier → List TypedIdentifier → List TypedIdentifier → Block → Statement
+| variableDeclaration : NonemptyList TypedIdentifier → Option Expression → Statement
+| assignment          : NonemptyList Identifier → Expression → Statement
+| «if»                : Expression → Block → Statement
+| expression          : Expression → Statement
+| switch              : Switch → Statement
+| forLoop             : Block → Expression → Block → Block → Statement
+| breakContinue       : BreakContinue → Statement
+| leave               : Statement
+
+end
+
+end Yul

From cd9cd3db7696e5b9a8e0580051e582096f617e85 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sun, 8 Jan 2023 21:23:32 -0300
Subject: [PATCH 02/16] Renaming

---
 Yatima.lean                            | 1 +
 Yatima/Compiler/{yul.lean => Yul.lean} | 0
 2 files changed, 1 insertion(+)
 rename Yatima/Compiler/{yul.lean => Yul.lean} (100%)

diff --git a/Yatima.lean b/Yatima.lean
index 1db1390f..b9ff6bde 100644
--- a/Yatima.lean
+++ b/Yatima.lean
@@ -30,6 +30,7 @@ import Yatima.CodeGen.Preloads
 import Yatima.CodeGen.PrettyPrint
 import Yatima.CodeGen.Simp
 import Yatima.CodeGen.Test
+import Yatima.Compiler.Yul
 import Yatima.ContAddr.ContAddr
 import Yatima.ContAddr.ContAddrError
 import Yatima.ContAddr.ContAddrM
diff --git a/Yatima/Compiler/yul.lean b/Yatima/Compiler/Yul.lean
similarity index 100%
rename from Yatima/Compiler/yul.lean
rename to Yatima/Compiler/Yul.lean

From 7638e346b6eacf75fb4932f44028d05362db4279 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Wed, 18 Jan 2023 23:46:24 -0300
Subject: [PATCH 03/16] WIP Yul to code

---
 Yatima/Compiler/Yul.lean | 50 ++++++++++++++++++++++++++++++++++++----
 1 file changed, 45 insertions(+), 5 deletions(-)

diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index 5979b9a0..0958d0ec 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -22,14 +22,12 @@ inductive Expression where
 | identifier   : Identifier → Expression
 | literal      : Literal → Expression
 
-inductive BreakContinue
-| «break»
-| «continue»
-
 structure NonemptyList (α : Type u) where
   head : α
   tail : List α
 
+def NonemptyList.toList (xs : NonemptyList α) : List α := xs.head :: xs.tail
+
 mutual
 
 inductive Block where
@@ -48,9 +46,51 @@ inductive Statement where
 | expression          : Expression → Statement
 | switch              : Switch → Statement
 | forLoop             : Block → Expression → Block → Block → Statement
-| breakContinue       : BreakContinue → Statement
+| «break»             : Statement
+| «continue»          : Statement
 | leave               : Statement
 
 end
 
+mutual
+
+-- Should not be partial functions, but Lean fails to prove termination
+partial def blockToCode (alreadyIndented : Bool) (indent : String) : Block → String
+| .mk statements =>
+  let firstIndent := if alreadyIndented then "" else indent
+  let left := firstIndent ++ "{\n"
+  let inner := statements.foldr
+    (fun statement acc => statementToCode ("    " ++ indent) statement ++ "\n" ++ acc)
+    ""
+  let right := indent ++ "}"
+  left ++ inner ++ right
+
+partial def statementToCode (indent : String) : Statement → String
+| .block block => blockToCode false indent block
+| .functionDefinition  name args rets body => sorry
+| .variableDeclaration names expr => sorry
+| .assignment          name expr => sorry
+| .«if»                expr block =>
+  let ifPart := indent ++ "if " ++ expressionToCode true indent expr
+  let inner  := blockToCode true indent block
+  ifPart ++ inner
+| .expression          expr => expressionToCode false indent expr
+| .switch              switch => switchToCode indent switch
+| .forLoop             init expr inc body =>
+  let forPart := indent ++ "for " ++
+    blockToCode true indent init ++
+    expressionToCode true indent expr ++
+    blockToCode true indent inc
+  let inner := blockToCode true indent body
+  forPart ++ inner
+| .«break»             => indent ++ "break"
+| .«continue»          => indent ++ "continue"
+| .leave               => indent ++ "leave"
+
+partial def expressionToCode (alreadyIndented : Bool) (indent : String) : Expression → String := sorry
+
+partial def switchToCode (indent : String) : Switch → String := sorry
+
+end
+
 end Yul

From 38bffbc810bd331503f7fe99cdbbd72766d5b1d5 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Jan 2023 09:43:07 -0300
Subject: [PATCH 04/16] Progress on Yul to code

---
 Yatima/Compiler/Yul.lean | 75 ++++++++++++++++++++++++++++++----------
 1 file changed, 57 insertions(+), 18 deletions(-)

diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index 0958d0ec..b6bde240 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -5,7 +5,7 @@ namespace Yul
 inductive PrimType where
 | u256
 
-def Identifier := String
+abbrev Identifier := String
 structure TypedIdentifier where
   identifier : Identifier
   type       : Option PrimType
@@ -52,44 +52,83 @@ inductive Statement where
 
 end
 
+abbrev Code := String
+def Code.inc (code : Code) : Code := "    " ++ code
+
+def PrimType.toCode : PrimType → Code
+| .u256 => "u256"
+
+def Identifier.toCode (id : Identifier) : Code := id
+
+def TypedIdentifier.toCode (id : TypedIdentifier) : Code :=
+  match id.type with
+  | none => id.identifier
+  | some type => id.identifier ++ " : " ++ type.toCode
+
 mutual
 
 -- Should not be partial functions, but Lean fails to prove termination
-partial def blockToCode (alreadyIndented : Bool) (indent : String) : Block → String
+partial def Block.toCode (alreadyIndented : Bool) (indent : Code) : Block → Code
 | .mk statements =>
   let firstIndent := if alreadyIndented then "" else indent
   let left := firstIndent ++ "{\n"
   let inner := statements.foldr
-    (fun statement acc => statementToCode ("    " ++ indent) statement ++ "\n" ++ acc)
+    (fun statement acc => Statement.toCode indent.inc statement ++ "\n" ++ acc)
     ""
   let right := indent ++ "}"
   left ++ inner ++ right
 
-partial def statementToCode (indent : String) : Statement → String
-| .block block => blockToCode false indent block
-| .functionDefinition  name args rets body => sorry
-| .variableDeclaration names expr => sorry
-| .assignment          name expr => sorry
+partial def Statement.toCode (indent : Code) : Statement → Code
+| .block block => block.toCode false indent
+| .functionDefinition  name args rets body =>
+  let header := indent ++ "function " ++ name.toCode
+  let args := match args with
+    | .nil => "()"
+    | .cons arg args' =>
+      args'.foldr
+        (fun arg' acc => ", " ++ TypedIdentifier.toCode arg' ++ acc)
+        ("(" ++ arg.toCode)
+      ++ ")"
+  let rets := match rets with
+    | .nil => ""
+    | .cons ret rets' =>
+      rets'.foldr
+        (fun ret' acc => ", " ++ TypedIdentifier.toCode ret' ++ acc)
+        ("-> " ++ ret.toCode)
+  let body := body.toCode true indent.inc
+  header ++ args ++ rets ++ body
+| .variableDeclaration names expr =>
+  let firstVar := indent ++ "let " ++ names.head.toCode
+  let otherVars := names.tail.foldr (fun name acc => ", " ++ name.toCode ++ acc) ""
+  match expr with
+  | none => firstVar ++ otherVars
+  | some expr => firstVar ++ otherVars ++ " := " ++ expr.toCode true indent.inc
+| .assignment          names expr =>
+  let firstVar := indent ++ names.head.toCode
+  let otherVars := names.tail.foldr (fun name acc => ", " ++ name.toCode ++ acc) ""
+  firstVar ++ otherVars ++ " := " ++ expr.toCode true indent.inc
 | .«if»                expr block =>
-  let ifPart := indent ++ "if " ++ expressionToCode true indent expr
-  let inner  := blockToCode true indent block
+  let indent' := indent.inc
+  let ifPart := indent ++ "if " ++ expr.toCode true indent'
+  let inner  := block.toCode true indent'
   ifPart ++ inner
-| .expression          expr => expressionToCode false indent expr
-| .switch              switch => switchToCode indent switch
+| .expression          expr => expr.toCode false indent
+| .switch              switch => switch.toCode indent
 | .forLoop             init expr inc body =>
+  let indent' := indent.inc
   let forPart := indent ++ "for " ++
-    blockToCode true indent init ++
-    expressionToCode true indent expr ++
-    blockToCode true indent inc
-  let inner := blockToCode true indent body
+    init.toCode true indent' ++
+    expr.toCode true indent' ++
+    inc.toCode true indent'
+  let inner := body.toCode true indent'
   forPart ++ inner
 | .«break»             => indent ++ "break"
 | .«continue»          => indent ++ "continue"
 | .leave               => indent ++ "leave"
 
-partial def expressionToCode (alreadyIndented : Bool) (indent : String) : Expression → String := sorry
+partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) : Expression → Code := default
 
-partial def switchToCode (indent : String) : Switch → String := sorry
+partial def Switch.toCode (indent : Code) : Switch → Code := default
 
 end
 

From 4a24c68cd378bf521ce4e804b85a43bd748bf2c4 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Jan 2023 10:01:09 -0300
Subject: [PATCH 05/16] More progress on Yul to code

---
 Yatima/Compiler/Yul.lean | 44 +++++++++++++++++++++++++++++++++-------
 1 file changed, 37 insertions(+), 7 deletions(-)

diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index b6bde240..4f0d5fe3 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -12,10 +12,10 @@ structure TypedIdentifier where
 
 inductive Literal where
 -- Actually it should be a u256
-| number : PrimType → Nat → Literal
-| string : PrimType → String → Literal
-| true   : PrimType → Literal
-| false  : PrimType → Literal
+| number : Option PrimType → Nat → Literal
+| string : Option PrimType → String → Literal
+| true   : Option PrimType → Literal
+| false  : Option PrimType → Literal
 
 inductive Expression where
 | functionCall : Identifier → List Expression → Expression
@@ -126,9 +126,39 @@ partial def Statement.toCode (indent : Code) : Statement → Code
 | .«continue»          => indent ++ "continue"
 | .leave               => indent ++ "leave"
 
-partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) : Expression → Code := default
-
-partial def Switch.toCode (indent : Code) : Switch → Code := default
+partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) (expr : Expression) : Code :=
+  let firstIndent := if alreadyIndented then "" else indent
+  match expr with
+  | .functionCall name args =>
+    let indent' := indent.inc
+    let args := match args with
+      | .nil => "()"
+      | .cons arg args' =>
+        args'.foldr
+          (fun arg' acc => ", " ++ Expression.toCode true indent' arg' ++ acc)
+          ("(" ++ arg.toCode true indent')
+        ++ ")"
+    firstIndent ++ name ++ args
+  | .identifier   name => firstIndent ++ name
+  | .literal lit =>
+    let (typ, lit) := match lit with
+      | .true typ => (typ, "true")
+      | .false typ => (typ, "false")
+      | .string typ str => (typ, str)
+      | .number typ num => (typ, s!"{num}")
+    match typ with
+    | none => firstIndent ++ lit
+    | some typ => firstIndent ++ lit ++ " : " ++ typ.toCode
+
+partial def Switch.toCode (indent : Code) : Switch → Code
+| .case expr caseList block? =>
+  let indent' := indent.inc
+  let header := indent ++ "switch " ++ expr.toCode true indent'
+  header
+| .default expr block =>
+  let indent' := indent.inc
+  let header := indent ++ "switch " ++ expr.toCode true indent'
+  header
 
 end
 

From 026f501fa00f510eeb56e802b67133c80e7b6464 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Jan 2023 11:43:19 -0300
Subject: [PATCH 06/16] Finished Yul to code

---
 Yatima/Compiler/Yul.lean | 34 +++++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 13 deletions(-)

diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index 4f0d5fe3..0ab31255 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -65,6 +65,16 @@ def TypedIdentifier.toCode (id : TypedIdentifier) : Code :=
   | none => id.identifier
   | some type => id.identifier ++ " : " ++ type.toCode
 
+def Literal.toCode (lit : Literal) : Code :=
+  let (typ, lit) := match lit with
+    | .true typ => (typ, "true")
+    | .false typ => (typ, "false")
+    | .string typ str => (typ, str)
+    | .number typ num => (typ, s!"{num}")
+  match typ with
+  | none => lit
+  | some typ => lit ++ " : " ++ typ.toCode
+
 mutual
 
 -- Should not be partial functions, but Lean fails to prove termination
@@ -140,25 +150,23 @@ partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) (expr : E
         ++ ")"
     firstIndent ++ name ++ args
   | .identifier   name => firstIndent ++ name
-  | .literal lit =>
-    let (typ, lit) := match lit with
-      | .true typ => (typ, "true")
-      | .false typ => (typ, "false")
-      | .string typ str => (typ, str)
-      | .number typ num => (typ, s!"{num}")
-    match typ with
-    | none => firstIndent ++ lit
-    | some typ => firstIndent ++ lit ++ " : " ++ typ.toCode
+  | .literal lit => firstIndent ++ lit.toCode
 
 partial def Switch.toCode (indent : Code) : Switch → Code
 | .case expr caseList block? =>
   let indent' := indent.inc
-  let header := indent ++ "switch " ++ expr.toCode true indent'
-  header
+  let header := indent ++ "switch " ++ expr.toCode true indent' ++ "\n"
+  let cases := caseList.toList.foldr
+    (fun (lit, block) acc => indent ++ "case " ++ lit.toCode ++ block.toCode true indent' ++ acc) ""
+  let default := match block? with
+    | none => ""
+    | some block => indent ++ "default " ++ block.toCode true indent'
+  header ++ cases ++ default
 | .default expr block =>
   let indent' := indent.inc
-  let header := indent ++ "switch " ++ expr.toCode true indent'
-  header
+  let header := indent ++ "switch " ++ expr.toCode true indent' ++ "\n"
+  let default := indent ++ "default " ++ block.toCode true indent'
+  header ++ default
 
 end
 

From fd095be392adab209f73588e2c7a5b1fdf59bb45 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 19 Jan 2023 14:34:18 -0300
Subject: [PATCH 07/16] Yul objects added

---
 Yatima/Compiler/Yul.lean | 71 ++++++++++++++++++++++++++++++----------
 1 file changed, 53 insertions(+), 18 deletions(-)

diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index 0ab31255..38e15397 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -1,3 +1,5 @@
+import Init.Data.Repr
+
 -- This is based on Yul's specification https://docs.soliditylang.org/en/v0.8.17/yul.html#specification-of-yul
 namespace Yul
 
@@ -52,6 +54,16 @@ inductive Statement where
 
 end
 
+abbrev StringLiteral := String
+abbrev HexLiteral := Nat
+
+inductive Data where
+| str : StringLiteral → StringLiteral → Data
+| hex : StringLiteral → HexLiteral → Data
+
+inductive Object where
+| object : StringLiteral → Block → List (Sum Object Data) → Object
+
 abbrev Code := String
 def Code.inc (code : Code) : Code := "    " ++ code
 
@@ -69,15 +81,31 @@ def Literal.toCode (lit : Literal) : Code :=
   let (typ, lit) := match lit with
     | .true typ => (typ, "true")
     | .false typ => (typ, "false")
-    | .string typ str => (typ, str)
+    | .string typ str => (typ, s!"\"{str}\"")
     | .number typ num => (typ, s!"{num}")
   match typ with
   | none => lit
   | some typ => lit ++ " : " ++ typ.toCode
 
+-- Should not be partial functions, but Lean fails to prove termination
+partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) (expr : Expression) : Code :=
+  let firstIndent := if alreadyIndented then "" else indent
+  match expr with
+  | .functionCall name args =>
+    let indent' := indent.inc
+    let args := match args with
+      | .nil => "()"
+      | .cons arg args' =>
+        args'.foldr
+          (fun arg' acc => ", " ++ Expression.toCode true indent' arg' ++ acc)
+          ("(" ++ arg.toCode true indent')
+        ++ ")"
+    firstIndent ++ name ++ args
+  | .identifier   name => firstIndent ++ name
+  | .literal lit => firstIndent ++ lit.toCode
+
 mutual
 
--- Should not be partial functions, but Lean fails to prove termination
 partial def Block.toCode (alreadyIndented : Bool) (indent : Code) : Block → Code
 | .mk statements =>
   let firstIndent := if alreadyIndented then "" else indent
@@ -136,22 +164,6 @@ partial def Statement.toCode (indent : Code) : Statement → Code
 | .«continue»          => indent ++ "continue"
 | .leave               => indent ++ "leave"
 
-partial def Expression.toCode (alreadyIndented : Bool) (indent : Code) (expr : Expression) : Code :=
-  let firstIndent := if alreadyIndented then "" else indent
-  match expr with
-  | .functionCall name args =>
-    let indent' := indent.inc
-    let args := match args with
-      | .nil => "()"
-      | .cons arg args' =>
-        args'.foldr
-          (fun arg' acc => ", " ++ Expression.toCode true indent' arg' ++ acc)
-          ("(" ++ arg.toCode true indent')
-        ++ ")"
-    firstIndent ++ name ++ args
-  | .identifier   name => firstIndent ++ name
-  | .literal lit => firstIndent ++ lit.toCode
-
 partial def Switch.toCode (indent : Code) : Switch → Code
 | .case expr caseList block? =>
   let indent' := indent.inc
@@ -170,4 +182,27 @@ partial def Switch.toCode (indent : Code) : Switch → Code
 
 end
 
+def HexLiteral.toCode (hex : HexLiteral) : Code :=
+  let base := 16
+  let num := (base.toDigits hex).asString
+  s!"hex\"{num}\""
+
+def StringLiteral.toCode (str : StringLiteral) : Code :=
+  s!"\"{str}\""
+
+def Data.toCode : Data → Code
+| .hex name hexLit => "data " ++ name.toCode ++ hexLit.toCode
+| .str name strLit => "data " ++ name.toCode ++ strLit.toCode
+
+partial def Object.toCode (indent : Code) : Object → Code
+| .object name code args =>
+  let objHeader := indent ++ "object " ++ name.toCode ++ " {\n"
+  let indent' := indent.inc
+  let codeHeader := indent' ++ "code " ++ name.toCode ++ code.toCode true indent'.inc
+  let argToCode arg := match arg with
+  | .inl obj => obj.toCode indent'
+  | .inr data => indent' ++ data.toCode
+  let args := args.foldr (fun arg acc => "\n" ++ argToCode arg ++ acc) "\n"
+  objHeader ++ codeHeader ++ args ++ indent ++ "}"
+
 end Yul

From 5abc2cd9ef353ca272a12e78ec16e48dd8a97aa9 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sat, 21 Jan 2023 17:23:45 -0300
Subject: [PATCH 08/16] Updated YatimaStdLib and started Grin AST

---
 Main.lean                 |  8 +-------
 Yatima.lean               |  1 +
 Yatima/Compiler/Grin.lean | 16 ++++++++++++++++
 Yatima/Compiler/Yul.lean  | 13 ++++---------
 lake-manifest.json        |  4 ++--
 lakefile.lean             |  2 +-
 6 files changed, 25 insertions(+), 19 deletions(-)
 create mode 100644 Yatima/Compiler/Grin.lean

diff --git a/Main.lean b/Main.lean
index 29206ada..1cb501b7 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,10 +1,4 @@
-import Yatima.Cli.ContAddrCmd
-import Yatima.Cli.TypecheckCmd
-import Yatima.Cli.CodeGenCmd
-import Yatima.Cli.ProveCmd
-import Yatima.Cli.VerifyCmd
-import Yatima.Cli.IpfsCmd
-import Yatima.Cli.PrintPrimsCmd
+import Yatima
 
 opaque VERSION : String :=
   s!"{Lean.versionString}|0.0.1"
diff --git a/Yatima.lean b/Yatima.lean
index 65f2db48..f50e83c8 100644
--- a/Yatima.lean
+++ b/Yatima.lean
@@ -32,6 +32,7 @@ import Yatima.CodeGen.PrettyPrint
 import Yatima.CodeGen.Simp
 import Yatima.CodeGen.Test
 import Yatima.Compiler.Yul
+import Yatima.Compiler.Grin
 import Yatima.ContAddr.ContAddr
 import Yatima.ContAddr.ContAddrError
 import Yatima.ContAddr.ContAddrM
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
new file mode 100644
index 00000000..f250ada7
--- /dev/null
+++ b/Yatima/Compiler/Grin.lean
@@ -0,0 +1,16 @@
+namespace Grin
+
+inductive Tag where
+-- Suspended full applications
+| F : Tag
+-- Partial applications
+| P : Tag
+-- Saturated constructors
+| C : Tag
+
+inductive Binding where
+
+inductive Program where
+| bindings : Binding → List Binding → Program
+
+end Grin
diff --git a/Yatima/Compiler/Yul.lean b/Yatima/Compiler/Yul.lean
index 38e15397..0acee701 100644
--- a/Yatima/Compiler/Yul.lean
+++ b/Yatima/Compiler/Yul.lean
@@ -1,4 +1,5 @@
 import Init.Data.Repr
+import YatimaStdLib.NonEmpty
 
 -- This is based on Yul's specification https://docs.soliditylang.org/en/v0.8.17/yul.html#specification-of-yul
 namespace Yul
@@ -24,26 +25,20 @@ inductive Expression where
 | identifier   : Identifier → Expression
 | literal      : Literal → Expression
 
-structure NonemptyList (α : Type u) where
-  head : α
-  tail : List α
-
-def NonemptyList.toList (xs : NonemptyList α) : List α := xs.head :: xs.tail
-
 mutual
 
 inductive Block where
 | mk : List Statement → Block
 
 inductive Switch where
-| case    : Expression → NonemptyList (Literal × Block) → Option Block → Switch
+| case    : Expression → NEList (Literal × Block) → Option Block → Switch
 | default : Expression → Block → Switch
 
 inductive Statement where
 | block               : Block → Statement
 | functionDefinition  : Identifier → List TypedIdentifier → List TypedIdentifier → Block → Statement
-| variableDeclaration : NonemptyList TypedIdentifier → Option Expression → Statement
-| assignment          : NonemptyList Identifier → Expression → Statement
+| variableDeclaration : NEList TypedIdentifier → Option Expression → Statement
+| assignment          : NEList Identifier → Expression → Statement
 | «if»                : Expression → Block → Statement
 | expression          : Expression → Statement
 | switch              : Switch → Statement
diff --git a/lake-manifest.json b/lake-manifest.json
index 52cb5e0d..51d8dd77 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/yatima-inc/YatimaStdLib.lean",
     "subDir?": null,
-    "rev": "704823e421b333ea9960347e305c60f654618422",
+    "rev": "b3084d5fb020975555dabe507e6a4db659b0733d",
     "name": "YatimaStdLib",
-    "inputRev?": "704823e421b333ea9960347e305c60f654618422"}},
+    "inputRev?": "b3084d5fb020975555dabe507e6a4db659b0733d"}},
   {"git":
    {"url": "https://github.com/yatima-inc/Lurk.lean",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index f89a1ad2..4ad05ddc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,7 +18,7 @@ require LSpec from git
   "https://github.com/yatima-inc/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
 
 require YatimaStdLib from git
-  "https://github.com/yatima-inc/YatimaStdLib.lean" @ "704823e421b333ea9960347e305c60f654618422"
+  "https://github.com/yatima-inc/YatimaStdLib.lean" @ "b3084d5fb020975555dabe507e6a4db659b0733d"
 
 require Cli from git
   "https://github.com/yatima-inc/Cli.lean" @ "b76218dbaa20ac51cf4e6789407e42b76dd3061f"

From 0ca73cccf572cae41a9922e971d33799d9e2665a Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Mon, 23 Jan 2023 20:34:22 -0300
Subject: [PATCH 09/16] Finished Grin AST

---
 Yatima/Compiler/Grin.lean | 57 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 51 insertions(+), 6 deletions(-)

diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index f250ada7..245e8e32 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -1,16 +1,61 @@
+import YatimaStdLib.NonEmpty
+
+-- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
 namespace Grin
 
+abbrev Var := String
+abbrev Id := String
+
 inductive Tag where
 -- Suspended full applications
-| F : Tag
+| F : Id → Tag
 -- Partial applications
-| P : Tag
+| P : Id → Tag
 -- Saturated constructors
-| C : Tag
+| C : Id → Tag
+
+inductive SVal where
+  | str : String → SVal
+  | num : Nat → SVal
+  | var : Var → SVal
+
+inductive Val where
+  | ctag : Tag → List SVal → Val
+  | cvar : Var → List SVal → Val
+  | stag : Tag → Val
+  | empty : Val
+  | sval : SVal → Val
+
+inductive CPat where
+  | ctag : Tag → List Var → CPat
+  | stag : Tag → CPat
+  | str : String → CPat
+  | num : Nat → CPat
+
+abbrev LPat := Val
+
+mutual
+inductive Expr where
+  | seq : SExpr → LPat → Expr → Expr
+  | case : Val → NEList (CPat × Expr) → Expr
+  | «if» : Val → Expr → Expr → Expr
+  | op : SExpr → Expr
+
+inductive SExpr where
+  | app : Var → NEList SVal → SExpr
+  | unit : Val → SExpr
+  | store : Val → SExpr
+  | fetch : Var → Option Nat → SExpr
+  | update : Var → Val → SExpr
+  | expr : Expr → SExpr
+end
 
-inductive Binding where
+structure Binding where
+  defn : Var
+  args : NEList Var
+  body : Expr
+  
 
-inductive Program where
-| bindings : Binding → List Binding → Program
+abbrev Prog := NEList Binding 
 
 end Grin

From 368f69ca1c2f3e9f8b9500cdb7113ac014f609d3 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 26 Jan 2023 12:17:17 -0300
Subject: [PATCH 10/16] Redefinition of Grin AST

---
 Yatima/Compiler/Grin.lean | 56 ++++++++++++++++++++++-----------------
 1 file changed, 32 insertions(+), 24 deletions(-)

diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index 245e8e32..d2823208 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -3,58 +3,66 @@ import YatimaStdLib.NonEmpty
 -- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
 namespace Grin
 
-abbrev Var := String
-abbrev Id := String
+/-- Var represents a variable binding, such as in a function definition in a pattern -/
+structure Var where
+  data : Lean.FVarId
+/-- Id represents a known definition, such as a function or constructor -/
+structure Id where
+  data : Lean.FVarId
 
 inductive Tag where
 -- Suspended full applications
 | F : Id → Tag
 -- Partial applications
-| P : Id → Tag
+| P : Id → Nat → Tag
 -- Saturated constructors
 | C : Id → Tag
 
+inductive Literal
+  | str : String → Literal
+  | num : Nat → Literal
+
 inductive SVal where
-  | str : String → SVal
-  | num : Nat → SVal
+  | lit : Literal → SVal
   | var : Var → SVal
 
 inductive Val where
-  | ctag : Tag → List SVal → Val
-  | cvar : Var → List SVal → Val
-  | stag : Tag → Val
+  | ctag  : Tag → List SVal → Val
+  | cvar  : Var → List SVal → Val
+  | stag  : Tag → Val
   | empty : Val
-  | sval : SVal → Val
+  | sval  : SVal → Val
 
 inductive CPat where
+  -- Complete tag pattern
   | ctag : Tag → List Var → CPat
+  -- Single tag pattern
   | stag : Tag → CPat
-  | str : String → CPat
-  | num : Nat → CPat
+  | lit  : Literal → CPat
 
 abbrev LPat := Val
 
-mutual
+inductive SExpr where
+  | store  : Val → SExpr
+  | fetch  : Var → Option Nat → SExpr
+  | update : Var → Val → SExpr
+  -- Known function call
+  | call   : Id → NEList SVal → SExpr
+  -- Evaluation of unknown expression
+  | eval   : Var → SExpr
+  -- Application of unknown function to a list of arguments
+  | apply  : Var → NEList SVal → SExpr
+
 inductive Expr where
-  | seq : SExpr → LPat → Expr → Expr
+  | unit : Val → Expr
+  | seq  : SExpr → LPat → Expr → Expr
   | case : Val → NEList (CPat × Expr) → Expr
   | «if» : Val → Expr → Expr → Expr
-  | op : SExpr → Expr
-
-inductive SExpr where
-  | app : Var → NEList SVal → SExpr
-  | unit : Val → SExpr
-  | store : Val → SExpr
-  | fetch : Var → Option Nat → SExpr
-  | update : Var → Val → SExpr
-  | expr : Expr → SExpr
-end
 
 structure Binding where
   defn : Var
   args : NEList Var
   body : Expr
-  
 
 abbrev Prog := NEList Binding 
 

From 2954c5e8dc96c4a4cd84fb18bdaa60025ad5d115 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sat, 28 Jan 2023 11:16:25 -0300
Subject: [PATCH 11/16] Conversion WIP

---
 Yatima/Compiler/Grin.lean | 36 +++++++++++++++++++++++++++++++-----
 1 file changed, 31 insertions(+), 5 deletions(-)

diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index d2823208..e26553d7 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -1,4 +1,6 @@
 import YatimaStdLib.NonEmpty
+import Lean.Expr
+import Lean.Compiler.LCNF
 
 -- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
 namespace Grin
@@ -8,7 +10,7 @@ structure Var where
   data : Lean.FVarId
 /-- Id represents a known definition, such as a function or constructor -/
 structure Id where
-  data : Lean.FVarId
+  data : Lean.Name
 
 inductive Tag where
 -- Suspended full applications
@@ -28,7 +30,6 @@ inductive SVal where
 
 inductive Val where
   | ctag  : Tag → List SVal → Val
-  | cvar  : Var → List SVal → Val
   | stag  : Tag → Val
   | empty : Val
   | sval  : SVal → Val
@@ -40,7 +41,11 @@ inductive CPat where
   | stag : Tag → CPat
   | lit  : Literal → CPat
 
-abbrev LPat := Val
+inductive LPat where
+  | ctag  : Tag → List SVal → LPat
+  | cvar  : Var → List SVal → LPat
+  | stag  : Tag → LPat
+  | svar  : Var → LPat
 
 inductive SExpr where
   | store  : Val → SExpr
@@ -55,15 +60,36 @@ inductive SExpr where
 
 inductive Expr where
   | unit : Val → Expr
-  | seq  : SExpr → LPat → Expr → Expr
+  | seq  : Expr → LPat → Expr → Expr
+  | op   : SExpr → LPat → Expr → Expr
   | case : Val → NEList (CPat × Expr) → Expr
   | «if» : Val → Expr → Expr → Expr
 
 structure Binding where
-  defn : Var
+  defn : Id
   args : NEList Var
   body : Expr
 
 abbrev Prog := NEList Binding 
 
+open Lean.Compiler
+
+def Expr.fromLCNF : LCNF.Code → Expr
+| .let decl k => sorry
+| .fun decl k => sorry
+| .jp decl k => sorry
+| .jmp fvarId args => sorry
+| .cases cases => sorry
+| .return fvarId => sorry
+| .unreach type => sorry
+
+def Binding.fromLCNF (decl : LCNF.Decl) : Binding :=
+  let defn := ⟨decl.name⟩
+  match decl.params.toList.map (fun param => Var.mk param.fvarId) with
+  | [] => sorry
+  | arg :: args =>
+    let args := arg :| args
+    let body := sorry
+    { defn, args, body }
+
 end Grin

From cce663f3f37882a383fc533d563aea2bcac0c5ab Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Fri, 3 Feb 2023 14:53:58 -0300
Subject: [PATCH 12/16] Progress in the Grin compiler

---
 Yatima/Compiler/Compiler.lean | 51 +++++++++++++++++++++++++++++++++
 Yatima/Compiler/Grin.lean     | 48 +++++++++++--------------------
 Yatima/Compiler/GrinM.lean    | 53 +++++++++++++++++++++++++++++++++++
 3 files changed, 120 insertions(+), 32 deletions(-)
 create mode 100644 Yatima/Compiler/Compiler.lean
 create mode 100644 Yatima/Compiler/GrinM.lean

diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
new file mode 100644
index 00000000..b0091e1a
--- /dev/null
+++ b/Yatima/Compiler/Compiler.lean
@@ -0,0 +1,51 @@
+import Yatima.Compiler.GrinM
+
+open Lean.Compiler.LCNF
+
+namespace Yatima.Grin
+
+def RScheme : Code → GrinM Expr
+| .let decl k => match decl.value with
+  | .erased => RScheme k
+  | .value val => do
+    let op := .unit $ .sval $ .lit val
+    let pat := sorry
+    let expr ← RScheme k
+    pure $ .seq op pat expr
+  | .proj _ idx struct => do
+    let op := sorry
+    let pat := sorry
+    let expr ← RScheme k
+    pure $ .seq op pat expr
+  | .const name _ args => do
+    let op := sorry
+    let pat := sorry
+    let expr ← RScheme k
+    pure $ .seq op pat expr
+  | .fvar var args => do
+    let op := sorry
+    let pat := sorry
+    let expr ← RScheme k
+    pure $ .seq op pat expr
+| .cases _cases => throw "TODO"
+| .return fvarId => do
+  -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
+  -- will either be a `fetch` or `unit` instruction depending on whether the variable is a
+  -- pointer or basic value
+  match ← varKind fvarId with
+  | .pointer => pure $ .ret $ .fetch ⟨fvarId⟩ .none
+  | .basic => pure $ .ret $ .unit $ .sval $ .var ⟨fvarId⟩
+| .fun _decl _k => throw "Should not happen (?)"
+-- We need to figure out a way to implement join points
+| .jp _decl _k => throw "TODO"
+| .jmp _fvarId _args => throw "TODO"
+| .unreach _type => throw "Should not happen"
+
+def compileDeclaration (decl : Decl) : GrinM Binding := do
+  let defn := ⟨decl.name⟩
+  let args := decl.params.toList.map (fun param => Var.mk param.fvarId)
+  let body ← RScheme decl.value
+  let binding := { defn, args, body }
+  pure binding
+
+end Yatima.Grin
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index e26553d7..8d21fa89 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -1,9 +1,11 @@
-import YatimaStdLib.NonEmpty
 import Lean.Expr
 import Lean.Compiler.LCNF
+import YatimaStdLib.NonEmpty
+
+open Lean.Compiler.LCNF
 
 -- Based on https://nbviewer.org/github/grin-compiler/grin/blob/master/papers/boquist.pdf
-namespace Grin
+namespace Yatima.Grin
 
 /-- Var represents a variable binding, such as in a function definition in a pattern -/
 structure Var where
@@ -11,6 +13,10 @@ structure Var where
 /-- Id represents a known definition, such as a function or constructor -/
 structure Id where
   data : Lean.Name
+/-- VarKind tells us whether a variable is a pointer or a basic value -/
+inductive VarKind
+| pointer
+| basic
 
 inductive Tag where
 -- Suspended full applications
@@ -20,9 +26,7 @@ inductive Tag where
 -- Saturated constructors
 | C : Id → Tag
 
-inductive Literal
-  | str : String → Literal
-  | num : Nat → Literal
+abbrev Literal := LitValue
 
 inductive SVal where
   | lit : Literal → SVal
@@ -48,6 +52,7 @@ inductive LPat where
   | svar  : Var → LPat
 
 inductive SExpr where
+  | unit   : Val → SExpr
   | store  : Val → SExpr
   | fetch  : Var → Option Nat → SExpr
   | update : Var → Val → SExpr
@@ -59,37 +64,16 @@ inductive SExpr where
   | apply  : Var → NEList SVal → SExpr
 
 inductive Expr where
-  | unit : Val → Expr
-  | seq  : Expr → LPat → Expr → Expr
-  | op   : SExpr → LPat → Expr → Expr
+  | ret  : SExpr → Expr
+  | seq  : SExpr → LPat → Expr → Expr
+  | join : Expr → LPat → Expr → Expr
   | case : Val → NEList (CPat × Expr) → Expr
-  | «if» : Val → Expr → Expr → Expr
 
 structure Binding where
   defn : Id
-  args : NEList Var
+  args : List Var
   body : Expr
 
-abbrev Prog := NEList Binding 
-
-open Lean.Compiler
-
-def Expr.fromLCNF : LCNF.Code → Expr
-| .let decl k => sorry
-| .fun decl k => sorry
-| .jp decl k => sorry
-| .jmp fvarId args => sorry
-| .cases cases => sorry
-| .return fvarId => sorry
-| .unreach type => sorry
-
-def Binding.fromLCNF (decl : LCNF.Decl) : Binding :=
-  let defn := ⟨decl.name⟩
-  match decl.params.toList.map (fun param => Var.mk param.fvarId) with
-  | [] => sorry
-  | arg :: args =>
-    let args := arg :| args
-    let body := sorry
-    { defn, args, body }
+abbrev Prog := NEList Binding
 
-end Grin
+end Yatima.Grin
diff --git a/Yatima/Compiler/GrinM.lean b/Yatima/Compiler/GrinM.lean
new file mode 100644
index 00000000..05384f22
--- /dev/null
+++ b/Yatima/Compiler/GrinM.lean
@@ -0,0 +1,53 @@
+import Yatima.Compiler.Grin
+
+open Lean.Compiler.LCNF
+
+namespace Yatima.Grin
+
+-- The Grin compiler monad
+structure GrinEnv where
+  varKind : Lean.NameMap VarKind
+  env : Lean.Environment
+
+structure GrinState where
+  bindings : Lean.NameMap Binding
+  visited  : Lean.NameSet
+  ngen     : Lean.NameGenerator
+  deriving Inhabited
+
+abbrev GrinM := ReaderT GrinEnv $ EStateM String GrinState
+
+instance : Lean.MonadNameGenerator GrinM where
+  getNGen := return (← get).ngen
+  setNGen ngen := modify fun s => { s with ngen := ngen }
+
+def visit (name : Lean.Name) : GrinM Unit :=
+  modify fun s => { s with visited := s.visited.insert name }
+
+@[inline] def isVisited (n : Lean.Name) : GrinM Bool :=
+  return (← get).visited.contains n
+
+@[inline] def varKind (n : Lean.FVarId) : GrinM VarKind := do
+  match (← read).varKind.find? n.name with
+  | some kind => pure kind
+  | none => throw "Unknown variable"
+
+@[inline] def getBinding (n : Lean.FVarId) : GrinM Binding := do
+  match (← get).bindings.find? n.name with
+  | some binding => pure binding
+  | none => throw "Unknown variable"
+
+@[inline] def addBinding (n : Lean.FVarId) (binding : Binding) : GrinM Unit :=
+  modify (fun state => { state with bindings := state.bindings.insert n.name binding })
+
+def GrinM.run (env : GrinEnv) (s : GrinState) (m : GrinM α) :
+    EStateM.Result String GrinState α :=
+  m env |>.run s
+
+def getDecl (declName : Lean.Name) : GrinM Decl := do
+  let env := (← read).env
+  let some decl := getDeclCore? env monoExt declName
+    | throw s!"environment does not contain {declName}"
+  pure decl
+
+end Yatima.Grin

From ae910a6c9a63e8d46ad720396bf2e5f7d2c6a0e5 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Mon, 6 Feb 2023 14:07:56 -0300
Subject: [PATCH 13/16] WIP

---
 Yatima/CodeGen/CodeGen.lean   | 27 ++++++++++++++++++++++-----
 Yatima/Compiler/Compiler.lean | 30 ++++++++++++++++++++++++------
 Yatima/Compiler/Grin.lean     |  2 +-
 3 files changed, 47 insertions(+), 12 deletions(-)

diff --git a/Yatima/CodeGen/CodeGen.lean b/Yatima/CodeGen/CodeGen.lean
index 5e9b5270..0bdb6383 100644
--- a/Yatima/CodeGen/CodeGen.lean
+++ b/Yatima/CodeGen/CodeGen.lean
@@ -256,18 +256,23 @@ mutual
       let (name, decl) ← mkLetDecl decl
       let k ← mkCode k
       return .let name decl k
-    | .fun decl k | .jp decl k => do -- `.fun` and `.jp` are the same case to Lurk
-      -- dbg_trace s!">> mkCode fun"
+    | .fun decl k => do
+      dbg_trace s!">> mkCode fun"
+      let (name, decl) ← mkFunDecl decl
+      let k ← mkCode k
+      return .let name decl k
+    | .jp decl k => do
+      dbg_trace s!">> mkCode jp"
       let (name, decl) ← mkFunDecl decl
       let k ← mkCode k
       return .let name decl k
     | .jmp fvarId args => do
-      -- dbg_trace s!">> mkCode jmp"
+      dbg_trace s!">> mkCode jmp"
       let fvarId ← mkFVarId fvarId
       let args ← args.mapM mkArg
       return mkApp fvarId args.data
     | .cases cases =>
-      -- dbg_trace s!">> mkCode cases"
+      dbg_trace s!">> mkCode cases"
       mkCases cases
     | .return fvarId =>
       -- dbg_trace s!">> mkCode return {fvarId.name}"
@@ -279,8 +284,20 @@ mutual
     let ⟨name, _, _, params, value, _, _, _⟩ := decl
     visit name
     let ⟨params⟩ := params.map fun p => p.fvarId.name.toString false
+    let which := match value with
+    | .let .. => "let"
+    | .fun .. => "fun"
+    | .jp .. => "jp"
+    | .jmp .. => "jmp"
+    | .cases .. => "cases"
+    | .return .. => "return"
+    | .unreach .. => "unreach"
     let value : Expr ← mkCode value
-    let body := if params.isEmpty then value else mkLambda params value
+    let body := if params.isEmpty
+      then dbg_trace "`{decl.name}` params empty"; value
+      else
+        dbg_trace "`{decl.name}` params size {params.length}, the code is\n{which}"
+        mkLambda params value
     appendBinding (name, body)
 
   partial def appendName (name : Name) : CodeGenM Unit := do
diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
index b0091e1a..d8bdaad7 100644
--- a/Yatima/Compiler/Compiler.lean
+++ b/Yatima/Compiler/Compiler.lean
@@ -1,9 +1,22 @@
 import Yatima.Compiler.GrinM
-
+import Lean.Expr
 open Lean.Compiler.LCNF
 
+def Lean.FVarId.toVar (id : Lean.FVarId) : Yatima.Grin.Var := .mk id.name
+
 namespace Yatima.Grin
 
+def mkFreshVar : GrinM Var := do
+  pure ⟨← Lean.mkFreshId⟩
+
+def fetch? (id : Lean.FVarId) : GrinM SExpr := do
+  match ← varKind id with
+  | .pointer => pure $ .fetch id.toVar .none
+  | .basic => pure $ .unit $ .sval $ .var id.toVar
+
+def PScheme : Alt → GrinM Expr :=
+  sorry
+
 def RScheme : Code → GrinM Expr
 | .let decl k => match decl.value with
   | .erased => RScheme k
@@ -27,14 +40,19 @@ def RScheme : Code → GrinM Expr
     let pat := sorry
     let expr ← RScheme k
     pure $ .seq op pat expr
-| .cases _cases => throw "TODO"
+| .cases case => do
+  -- Since every variable is initially strict, we don't need to eval before
+  let new_var ← mkFreshVar
+  let expr := .seq (← fetch? case.discr) (.svar new_var) sorry
+  -- let val := .sval $ .var ⟨cases.discr⟩
+  -- let nelistPatExpr := sorry
+  -- pure $ .case val nelistPatExpr
+  pure expr
 | .return fvarId => do
   -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
   -- will either be a `fetch` or `unit` instruction depending on whether the variable is a
   -- pointer or basic value
-  match ← varKind fvarId with
-  | .pointer => pure $ .ret $ .fetch ⟨fvarId⟩ .none
-  | .basic => pure $ .ret $ .unit $ .sval $ .var ⟨fvarId⟩
+  pure $ .ret $ ← fetch? fvarId
 | .fun _decl _k => throw "Should not happen (?)"
 -- We need to figure out a way to implement join points
 | .jp _decl _k => throw "TODO"
@@ -43,7 +61,7 @@ def RScheme : Code → GrinM Expr
 
 def compileDeclaration (decl : Decl) : GrinM Binding := do
   let defn := ⟨decl.name⟩
-  let args := decl.params.toList.map (fun param => Var.mk param.fvarId)
+  let args := decl.params.toList.map (fun param => param.fvarId.toVar)
   let body ← RScheme decl.value
   let binding := { defn, args, body }
   pure binding
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index 8d21fa89..0b639b87 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -9,7 +9,7 @@ namespace Yatima.Grin
 
 /-- Var represents a variable binding, such as in a function definition in a pattern -/
 structure Var where
-  data : Lean.FVarId
+  data : Lean.Name
 /-- Id represents a known definition, such as a function or constructor -/
 structure Id where
   data : Lean.Name

From cc94e3f0f1e50b79345b36c25fc864f86af62754 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Wed, 8 Feb 2023 18:00:10 -0300
Subject: [PATCH 14/16] Compilation of cases

---
 Yatima/Compiler/Compiler.lean | 35 ++++++++++++++++++++++++-----------
 Yatima/Compiler/Grin.lean     |  2 ++
 2 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
index d8bdaad7..39bb19b1 100644
--- a/Yatima/Compiler/Compiler.lean
+++ b/Yatima/Compiler/Compiler.lean
@@ -9,15 +9,26 @@ namespace Yatima.Grin
 def mkFreshVar : GrinM Var := do
   pure ⟨← Lean.mkFreshId⟩
 
+def paramsToVars (params : Array Param) : List Var :=
+  params.toList.map (fun param => param.fvarId.toVar)
+
 def fetch? (id : Lean.FVarId) : GrinM SExpr := do
   match ← varKind id with
   | .pointer => pure $ .fetch id.toVar .none
   | .basic => pure $ .unit $ .sval $ .var id.toVar
 
-def PScheme : Alt → GrinM Expr :=
-  sorry
+mutual
+partial def PScheme : Alt → GrinM (CPat × Expr)
+| .default code => do
+  let expr ← RScheme code
+  pure (.default, expr)
+| .alt ctor params code  => do
+  let args := paramsToVars params
+  let tag := .C ⟨ ctor ⟩
+  let expr ← RScheme code
+  pure (.ctag tag args, expr)
 
-def RScheme : Code → GrinM Expr
+partial def RScheme : Code → GrinM Expr
 | .let decl k => match decl.value with
   | .erased => RScheme k
   | .value val => do
@@ -43,25 +54,27 @@ def RScheme : Code → GrinM Expr
 | .cases case => do
   -- Since every variable is initially strict, we don't need to eval before
   let new_var ← mkFreshVar
-  let expr := .seq (← fetch? case.discr) (.svar new_var) sorry
-  -- let val := .sval $ .var ⟨cases.discr⟩
-  -- let nelistPatExpr := sorry
-  -- pure $ .case val nelistPatExpr
-  pure expr
+  let caseVal := .sval $ .var new_var
+  let some patExprs := NEList.nonEmpty (← case.alts.toList.mapM PScheme)
+    | throw "Empty pattern"
+  let caseExpr := .case caseVal patExprs
+  pure $ .seq (← fetch? case.discr) (.svar new_var) caseExpr
+  -- pure expr
 | .return fvarId => do
   -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
   -- will either be a `fetch` or `unit` instruction depending on whether the variable is a
   -- pointer or basic value
   pure $ .ret $ ← fetch? fvarId
-| .fun _decl _k => throw "Should not happen (?)"
+| .fun _decl _k => throw "Should not find function definition here (?)"
 -- We need to figure out a way to implement join points
 | .jp _decl _k => throw "TODO"
 | .jmp _fvarId _args => throw "TODO"
-| .unreach _type => throw "Should not happen"
+| .unreach _type => throw "Unreach found"
+end
 
 def compileDeclaration (decl : Decl) : GrinM Binding := do
   let defn := ⟨decl.name⟩
-  let args := decl.params.toList.map (fun param => param.fvarId.toVar)
+  let args := paramsToVars decl.params
   let body ← RScheme decl.value
   let binding := { defn, args, body }
   pure binding
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index 0b639b87..e8875f13 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -43,6 +43,8 @@ inductive CPat where
   | ctag : Tag → List Var → CPat
   -- Single tag pattern
   | stag : Tag → CPat
+  -- Default case
+  | default : CPat
   | lit  : Literal → CPat
 
 inductive LPat where

From ebf11828c36f89a4d7acaea7284d04c5f64e81d4 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Thu, 9 Feb 2023 22:13:16 -0300
Subject: [PATCH 15/16] Application of unknown function

---
 Yatima/Compiler/Compiler.lean | 49 ++++++++++++++++++-----------------
 Yatima/Compiler/Grin.lean     |  6 ++++-
 2 files changed, 30 insertions(+), 25 deletions(-)

diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
index 39bb19b1..beec656e 100644
--- a/Yatima/Compiler/Compiler.lean
+++ b/Yatima/Compiler/Compiler.lean
@@ -15,7 +15,17 @@ def paramsToVars (params : Array Param) : List Var :=
 def fetch? (id : Lean.FVarId) : GrinM SExpr := do
   match ← varKind id with
   | .pointer => pure $ .fetch id.toVar .none
-  | .basic => pure $ .unit $ .sval $ .var id.toVar
+  | .basic => pure $ svar id.toVar
+
+def applyArgs (fnc : Var) : (args : List Arg) → GrinM Expr
+| [] => pure $ .ret $ svar fnc
+| .erased :: args => applyArgs fnc args
+| .type _ :: args => applyArgs fnc args
+| .fvar id :: args => do
+  let apply := .apply fnc (.var id.toVar)
+  let newVar ← mkFreshVar
+  let rest ← applyArgs newVar args
+  pure $ .seq apply (.svar newVar) rest
 
 mutual
 partial def PScheme : Alt → GrinM (CPat × Expr)
@@ -32,33 +42,24 @@ partial def RScheme : Code → GrinM Expr
 | .let decl k => match decl.value with
   | .erased => RScheme k
   | .value val => do
-    let op := .unit $ .sval $ .lit val
-    let pat := sorry
-    let expr ← RScheme k
-    pure $ .seq op pat expr
+    pure $ .ret $ slit val
   | .proj _ idx struct => do
-    let op := sorry
-    let pat := sorry
-    let expr ← RScheme k
-    pure $ .seq op pat expr
-  | .const name _ args => do
-    let op := sorry
-    let pat := sorry
-    let expr ← RScheme k
-    pure $ .seq op pat expr
-  | .fvar var args => do
-    let op := sorry
-    let pat := sorry
-    let expr ← RScheme k
-    pure $ .seq op pat expr
+    let structPtr := struct.toVar
+    let proj := .fetch structPtr (some idx)
+    pure $ .ret proj
+  | .const _name _ _args => throw "TODO"
+  | .fvar fnc args => do
+    let fncVal ← fetch? fnc
+    let newVar ← mkFreshVar
+    pure $ .seq fncVal (.svar newVar) (← applyArgs newVar args.toList)
 | .cases case => do
-  -- Since every variable is initially strict, we don't need to eval before
-  let new_var ← mkFreshVar
-  let caseVal := .sval $ .var new_var
   let some patExprs := NEList.nonEmpty (← case.alts.toList.mapM PScheme)
     | throw "Empty pattern"
-  let caseExpr := .case caseVal patExprs
-  pure $ .seq (← fetch? case.discr) (.svar new_var) caseExpr
+  -- Since every variable is initially strict, we don't need to eval before
+  let caseVal ← fetch? case.discr
+  let newVar ← mkFreshVar
+  let caseExpr := .case (.sval $ .var newVar) patExprs
+  pure $ .seq caseVal (.svar newVar) caseExpr
   -- pure expr
 | .return fvarId => do
   -- In the lazy case, a return is a call to eval, but since we chose strict semantics this
diff --git a/Yatima/Compiler/Grin.lean b/Yatima/Compiler/Grin.lean
index e8875f13..414a704f 100644
--- a/Yatima/Compiler/Grin.lean
+++ b/Yatima/Compiler/Grin.lean
@@ -63,7 +63,7 @@ inductive SExpr where
   -- Evaluation of unknown expression
   | eval   : Var → SExpr
   -- Application of unknown function to a list of arguments
-  | apply  : Var → NEList SVal → SExpr
+  | apply  : Var → SVal → SExpr
 
 inductive Expr where
   | ret  : SExpr → Expr
@@ -78,4 +78,8 @@ structure Binding where
 
 abbrev Prog := NEList Binding
 
+-- Helper functions
+def svar (var : Var) : SExpr := .unit $ .sval $ .var var
+def slit (lit : Literal) : SExpr := .unit $ .sval $ .lit lit
+
 end Yatima.Grin

From 3445c833a176818bd32a0083d358030d5a57f453 Mon Sep 17 00:00:00 2001
From: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
Date: Sat, 11 Feb 2023 12:07:05 -0300
Subject: [PATCH 16/16] `ToString` instance to LCNF for debugging

---
 Yatima/CodeGen/CodeGen.lean   | 27 +++-------------
 Yatima/Compiler/Compiler.lean |  1 +
 Yatima/Compiler/Debug.lean    | 59 +++++++++++++++++++++++++++++++++++
 3 files changed, 65 insertions(+), 22 deletions(-)
 create mode 100644 Yatima/Compiler/Debug.lean

diff --git a/Yatima/CodeGen/CodeGen.lean b/Yatima/CodeGen/CodeGen.lean
index 0bdb6383..5e9b5270 100644
--- a/Yatima/CodeGen/CodeGen.lean
+++ b/Yatima/CodeGen/CodeGen.lean
@@ -256,23 +256,18 @@ mutual
       let (name, decl) ← mkLetDecl decl
       let k ← mkCode k
       return .let name decl k
-    | .fun decl k => do
-      dbg_trace s!">> mkCode fun"
-      let (name, decl) ← mkFunDecl decl
-      let k ← mkCode k
-      return .let name decl k
-    | .jp decl k => do
-      dbg_trace s!">> mkCode jp"
+    | .fun decl k | .jp decl k => do -- `.fun` and `.jp` are the same case to Lurk
+      -- dbg_trace s!">> mkCode fun"
       let (name, decl) ← mkFunDecl decl
       let k ← mkCode k
       return .let name decl k
     | .jmp fvarId args => do
-      dbg_trace s!">> mkCode jmp"
+      -- dbg_trace s!">> mkCode jmp"
       let fvarId ← mkFVarId fvarId
       let args ← args.mapM mkArg
       return mkApp fvarId args.data
     | .cases cases =>
-      dbg_trace s!">> mkCode cases"
+      -- dbg_trace s!">> mkCode cases"
       mkCases cases
     | .return fvarId =>
       -- dbg_trace s!">> mkCode return {fvarId.name}"
@@ -284,20 +279,8 @@ mutual
     let ⟨name, _, _, params, value, _, _, _⟩ := decl
     visit name
     let ⟨params⟩ := params.map fun p => p.fvarId.name.toString false
-    let which := match value with
-    | .let .. => "let"
-    | .fun .. => "fun"
-    | .jp .. => "jp"
-    | .jmp .. => "jmp"
-    | .cases .. => "cases"
-    | .return .. => "return"
-    | .unreach .. => "unreach"
     let value : Expr ← mkCode value
-    let body := if params.isEmpty
-      then dbg_trace "`{decl.name}` params empty"; value
-      else
-        dbg_trace "`{decl.name}` params size {params.length}, the code is\n{which}"
-        mkLambda params value
+    let body := if params.isEmpty then value else mkLambda params value
     appendBinding (name, body)
 
   partial def appendName (name : Name) : CodeGenM Unit := do
diff --git a/Yatima/Compiler/Compiler.lean b/Yatima/Compiler/Compiler.lean
index beec656e..5c887145 100644
--- a/Yatima/Compiler/Compiler.lean
+++ b/Yatima/Compiler/Compiler.lean
@@ -1,4 +1,5 @@
 import Yatima.Compiler.GrinM
+import Yatima.Compiler.Debug
 import Lean.Expr
 open Lean.Compiler.LCNF
 
diff --git a/Yatima/Compiler/Debug.lean b/Yatima/Compiler/Debug.lean
new file mode 100644
index 00000000..a27ca694
--- /dev/null
+++ b/Yatima/Compiler/Debug.lean
@@ -0,0 +1,59 @@
+import Lean.Compiler.LCNF
+open Lean.Compiler.LCNF
+
+namespace Lean.Compiler.LCNF
+
+instance : ToString FVarId where
+  toString x := toString x.name
+
+instance : ToString Param where
+  toString x := s!"{x.fvarId}"
+
+instance [ToString K] : ToString (AltCore K) where
+  toString
+    | .alt ctor params k => s!"{ctor} {params} => {k}"
+    | .default k => s!"_ => {k}"
+
+instance : ToString LitValue where
+  toString
+  | .natVal x => s!"{x}"
+  | .strVal x => s!"\"{x}\""
+
+instance : ToString Arg where
+  toString
+  | .erased => "ε"
+  | .type .. => "τ"
+  | .fvar id => s!"{id}"
+
+instance : ToString LetValue where
+  toString
+    | .value lit => s!"{lit}"
+    | .erased .. => "ε"
+    | .proj _ idx struct => s!"(π {idx} {struct})"
+    | .const cnst _ args => s!"(const {cnst} {args})"
+    | .fvar id args => s!"(fvar {id} {args})"
+
+instance : ToString LetDecl where
+  toString decl := s!"{decl.fvarId} := {decl.value}"
+
+instance [ToString K] : ToString (FunDeclCore K) where
+  toString decl := s!"{decl.fvarId} {decl.params} := {decl.value}"
+
+instance [ToString K] : ToString (CasesCore K) where
+  toString cases := s!"{cases.discr} {cases.alts}"
+
+partial def Code.toString (code : Code) : String :=
+  let _ : ToString Code := ⟨toString⟩
+  match code with
+  | .let decl k => s!"(let {decl} in {k})"
+  | .fun decl k => s!"(fun {decl} in {k})"
+  | .jp decl k => s!"(jp {decl} in {k})"
+  | .jmp id args => s!"(jmp {id} {args})"
+  | .cases case => s!"(match {case})"
+  | .return id => s!"(return {id.name})"
+  | .unreach _ => "unreach"
+
+instance : ToString Code where
+  toString code := code.toString
+
+end Lean.Compiler.LCNF