add a mk command to typecheck a declaration

Main.lean

@@ -1,3 +1,4 @@
+import Yatima.Cli.MakeCmd
 import Yatima.Cli.ContAddrCmd
 import Yatima.Cli.TypecheckCmd
 import Yatima.Cli.CodeGenCmd
@@ -14,6 +15,7 @@ def yatimaCmd : Cli.Cmd := `[Cli|
   "A tool for content-addressing and generating Lurk code from Lean 4 code"
 
   SUBCOMMANDS:
+    makeCmd;
     contAddrCmd;
     typecheckCmd;
     codeGenCmd;

README.md

@@ -17,6 +17,7 @@ Running the setup script will also compile the Yatima typechecker and store it i
 
 The subcommands planned to be available for the `yatima` CLI are:
 * Main commands
+    * `mk`: generates Lurk code for typechecking a declaration
     * `ca`: content-addresses Lean 4 code to Yatima IR
     * `prove`: generates Lurk code for typechecking a content-addressed declaration
 * Auxiliary commands

Yatima/Cli/ContAddrCmd.lean

@@ -29,7 +29,7 @@ def contAddrRun (p : Cli.Parsed) : IO UInt32 := do
 
   -- dump the env
   let envFileName := p.flag? "env" |>.map (·.value) |>.getD defaultEnv
-  dumpData stt.env ⟨envFileName⟩  
+  dumpData stt.env ⟨envFileName⟩
 
   return 0
 

Yatima/Cli/MakeCmd.lean

@@ -0,0 +1,61 @@
+import Cli.Basic
+import Yatima.Cli.Utils
+import Yatima.ContAddr.ContAddr
+import Yatima.Common.GenTypechecker
+import Lurk.LDON
+
+open Yatima.ContAddr Lurk.LDON.Macro in
+def makeRun (p : Cli.Parsed) : IO UInt32 := do
+  -- Get Lean source file name
+  let some source := p.positionalArg? "source" |>.map (·.value)
+    | IO.eprintln "No source was provided"; return 1
+  let some decl := p.flag? "decl" |>.map (·.value.toNameSafe)
+    | IO.eprintln "No declaration provided"; return 1
+  let out := match p.flag? "out" |>.map (·.value) with
+    | some out => ⟨out⟩
+    | none => ⟨s!"{decl}.lurk"⟩
+
+  -- Run Lean frontend
+  let mut cronos ← Cronos.new.clock "Run Lean frontend"
+  Lean.setLibsPaths
+  let path := ⟨source⟩
+  let leanEnv ← Lean.runFrontend (← IO.FS.readFile path) path
+  let constMap := leanEnv.constants
+  cronos ← cronos.clock! "Run Lean frontend"
+
+  -- Start content-addressing
+  cronos ← cronos.clock "Content-address"
+  let stt ← match ← mkConsts constMap decl with
+    | .error err => IO.eprintln err; return 1
+    | .ok stt => pure stt
+  cronos ← cronos.clock! "Content-address"
+
+  let commExprs := stt.commits.keysList.map fun c => ~[.sym "COMMIT", c.toLDON]
+  let commExprsStr := String.intercalate "\n" $ commExprs.map (·.toString false)
+
+  cronos ← cronos.clock "Generate typechecker"
+  let tcExpr ← match ← genTypechecker with
+    | .error msg => IO.eprintln msg; return 1
+    | .ok expr' => pure expr'
+  cronos ← cronos.clock! "Generate typechecker"
+
+  -- simply apply the typechecker to the constant hash
+  let declComm := stt.env.consts.find! decl
+  let expr := mkRawTypecheckingExpr tcExpr declComm
+
+  IO.println s!"Writing output to {out}"
+  IO.FS.writeFile out s!"{commExprsStr}\n{expr.toString}"
+
+  return 0
+
+def makeCmd : Cli.Cmd := `[Cli|
+  mk VIA makeRun;
+  "Generates Lurk code to typecheck a declaration"
+
+  FLAGS:
+    d, "decl" : String; "Declaration to typecheck"
+    o, "out"  : String; "Output Lurk file (defaults to '<decl>.lurk')"
+
+  ARGS:
+    source : String; "Lean source file"
+]

Yatima/CodeGen/CodeGen.lean

@@ -315,8 +315,7 @@ def codeGen (leanEnv : Lean.Environment) (decl : Name) : Except String Expr :=
   match CodeGenM.run ⟨leanEnv.patchUnsafeRec, .empty⟩ default (codeGenM decl) with
   | .error e _ => .error e
   | .ok _ s => do
-    let bindings := Expr.mutualize $
-      s.appendedBindings.data.map fun (n, x) => (n.toString false, x)
+    let bindings := s.appendedBindings.data.map fun (n, x) => (n.toString false, x)
     let expr := mkLetrec bindings (.sym $ decl.toString false)
     let (expr, ssa) ← expr.toSSA
     let expr ← expr.inlineOfSSA ssa.recursive

Yatima/ContAddr/ContAddr.lean

@@ -470,4 +470,16 @@ def contAddr (constMap : Lean.ConstMap) (delta : List Lean.ConstantInfo)
   | (.ok _, stt) => return .ok stt
   | (.error e, _) => return .error e
 
+def mkConsts (constMap : Lean.ConstMap) (decl : Name) :
+    IO $ Except ContAddrError ContAddrState := do
+  let some const := constMap.find? decl
+    | return .error $ ContAddrError.unknownConstant decl
+  let ldonHashState := (← loadData LDONHASHCACHE).getD default
+  let (quick, persist) := (false, true)
+  IO.FS.createDirAll STOREDIR
+  match ← StateT.run (ReaderT.run (contAddrM [const])
+    (.init constMap quick persist)) (.init ldonHashState) with
+  | (.ok _, stt) => return .ok stt
+  | (.error e, _) => return .error e
+
 end Yatima.ContAddr