From 6d999f94e9b7d486cc899902d2ffb8a73f6fd617 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 6 Nov 2024 21:55:48 -0300 Subject: [PATCH] add a mk command to typecheck a declaration --- Main.lean | 2 ++ README.md | 1 + Yatima/Cli/ContAddrCmd.lean | 2 +- Yatima/Cli/MakeCmd.lean | 61 +++++++++++++++++++++++++++++++++++ Yatima/CodeGen/CodeGen.lean | 3 +- Yatima/ContAddr/ContAddr.lean | 12 +++++++ 6 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 Yatima/Cli/MakeCmd.lean diff --git a/Main.lean b/Main.lean index 5dbfea97..7960f4b9 100644 --- a/Main.lean +++ b/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; diff --git a/README.md b/README.md index 3cfea6fb..2b9ff884 100644 --- a/README.md +++ b/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 diff --git a/Yatima/Cli/ContAddrCmd.lean b/Yatima/Cli/ContAddrCmd.lean index 3481c56a..fe283e66 100644 --- a/Yatima/Cli/ContAddrCmd.lean +++ b/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 diff --git a/Yatima/Cli/MakeCmd.lean b/Yatima/Cli/MakeCmd.lean new file mode 100644 index 00000000..af19c7b0 --- /dev/null +++ b/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 '.lurk')" + + ARGS: + source : String; "Lean source file" +] diff --git a/Yatima/CodeGen/CodeGen.lean b/Yatima/CodeGen/CodeGen.lean index 51a1d5f9..d989e81d 100644 --- a/Yatima/CodeGen/CodeGen.lean +++ b/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 diff --git a/Yatima/ContAddr/ContAddr.lean b/Yatima/ContAddr/ContAddr.lean index ab86ab31..d9ae4897 100644 --- a/Yatima/ContAddr/ContAddr.lean +++ b/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