From 1c4f38e5eb76fd3442f4b3042e836c9027d1d6c7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 13:04:00 -0800 Subject: [PATCH 1/6] refactor: Rename {Serial,Delate}.lean --- Pantograph.lean | 2 +- Pantograph/{Serial.lean => Delate.lean} | 0 Pantograph/Environment.lean | 2 +- Pantograph/Library.lean | 2 +- Test/{Serial.lean => Delate.lean} | 6 +++--- Test/Environment.lean | 2 +- Test/Main.lean | 4 ++-- Test/Metavar.lean | 2 +- Test/Proofs.lean | 2 +- 9 files changed, 11 insertions(+), 11 deletions(-) rename Pantograph/{Serial.lean => Delate.lean} (100%) rename Test/{Serial.lean => Delate.lean} (98%) diff --git a/Pantograph.lean b/Pantograph.lean index 292efb9..72c4906 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -4,5 +4,5 @@ import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Version diff --git a/Pantograph/Serial.lean b/Pantograph/Delate.lean similarity index 100% rename from Pantograph/Serial.lean rename to Pantograph/Delate.lean diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 040d801..87e3a2f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,5 +1,5 @@ import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Lean open Lean diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 23a2046..8a5db24 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -2,7 +2,7 @@ import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Version import Lean diff --git a/Test/Serial.lean b/Test/Delate.lean similarity index 98% rename from Test/Serial.lean rename to Test/Delate.lean index 1c00501..57411e8 100644 --- a/Test/Serial.lean +++ b/Test/Delate.lean @@ -1,10 +1,10 @@ import LSpec -import Pantograph.Serial +import Pantograph.Delate import Test.Common import Lean open Lean -namespace Pantograph.Test.Serial +namespace Pantograph.Test.Delate open Pantograph @@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Instance", test_instance env), ] -end Pantograph.Test.Serial +end Pantograph.Test.Delate diff --git a/Test/Environment.lean b/Test/Environment.lean index 6b418f7..79d04ed 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Environment import Test.Common import Lean diff --git a/Test/Main.lean b/Test/Main.lean index 0fde5fa..25bb0d9 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -5,7 +5,7 @@ import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Serial +import Test.Delate import Test.Tactic -- Test running infrastructure @@ -50,7 +50,7 @@ def main (args: List String) := do ("Library", Library.suite env_default), ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), - ("Serial", Serial.suite env_default), + ("Delate", Delate.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Metavar.lean b/Test/Metavar.lean index dbaf2cc..84860b3 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -1,6 +1,6 @@ import LSpec import Pantograph.Goal -import Pantograph.Serial +import Pantograph.Delate import Test.Common import Lean diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1da21ae..437bb64 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies -/ import LSpec import Pantograph.Goal -import Pantograph.Serial +import Pantograph.Delate import Test.Common namespace Pantograph.Test.Proofs From 0d570276816185df141518e66a74b5f9292975c3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 13:05:48 -0800 Subject: [PATCH 2/6] refactor: Merge Condensed into Delate --- Pantograph.lean | 1 - Pantograph/Condensed.lean | 95 --------------------------------------- Pantograph/Delate.lean | 85 ++++++++++++++++++++++++++++++++++- Pantograph/Library.lean | 1 - Test/Common.lean | 1 - 5 files changed, 84 insertions(+), 99 deletions(-) delete mode 100644 Pantograph/Condensed.lean diff --git a/Pantograph.lean b/Pantograph.lean index 72c4906..bad5f2a 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,4 +1,3 @@ -import Pantograph.Condensed import Pantograph.Environment import Pantograph.Frontend import Pantograph.Goal diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean deleted file mode 100644 index 125b69c..0000000 --- a/Pantograph/Condensed.lean +++ /dev/null @@ -1,95 +0,0 @@ -/- structures for FFI based interface -/ -import Lean -import Pantograph.Goal -import Pantograph.Expr - -open Lean - -namespace Pantograph -namespace Condensed - --- Mirrors Lean's LocalDecl -structure LocalDecl where - -- Default value is for testing - fvarId: FVarId := { name := .anonymous } - userName: Name - - -- Normalized expression - type : Expr - value? : Option Expr := .none - -structure Goal where - mvarId: MVarId := { name := .anonymous } - userName: Name := .anonymous - context: Array LocalDecl - target: Expr - -@[export pantograph_goal_is_lhs] -def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome - --- Functions for creating contexts and states -@[export pantograph_elab_context] -def elabContext: Elab.Term.Context := { - errToSorry := false - } - -end Condensed - --- Get the list of visible (by default) free variables from a goal -@[export pantograph_visible_fvars_of_mvar] -protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do - let mvarDecl ← mctx.findDecl? mvarId - let lctx := mvarDecl.lctx - return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with - | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId - | none => r - -@[export pantograph_to_condensed_goal_m] -def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do - let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions) - let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions) - let mvarDecl ← mvarId.getDecl - let lctx := mvarDecl.lctx - let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } - Meta.withLCtx lctx mvarDecl.localInstances do - let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do - match localDecl with - | .cdecl _ fvarId userName type _ _ => - let type ← instantiate type - return { fvarId, userName, type } - | .ldecl _ fvarId userName type value _ _ => do - let userName := userName.simpMacroScopes - let type ← instantiate type - let value ← instantiate value - return { fvarId, userName, type, value? := .some value } - let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do - let skip := !ppAuxDecls && localDecl.isAuxDecl || - !ppImplDetailHyps && localDecl.isImplementationDetail - if skip then - return acc - else - let var ← ppVar localDecl - return var::acc - return { - mvarId, - userName := mvarDecl.userName, - context := vars.reverse.toArray, - target := ← instantiate mvarDecl.type - } - where - instantiate := instantiateAll - -@[export pantograph_goal_state_to_condensed_m] -protected def GoalState.toCondensed (state: GoalState): - CoreM (Array Condensed.Goal):= do - let metaM := do - let goals := state.goals.toArray - goals.mapM fun goal => do - match state.mctx.findDecl? goal with - | .some _ => - let serializedGoal ← toCondensedGoal goal - pure serializedGoal - | .none => throwError s!"Metavariable does not exist in context {goal.name}" - metaM.run' (s := state.savedState.term.meta.meta) - -end Pantograph diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 3a9efa4..c5954f0 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -4,7 +4,6 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without using `Scope`s. -/ import Lean -import Pantograph.Condensed import Pantograph.Expr import Pantograph.Goal import Pantograph.Protocol @@ -14,7 +13,91 @@ open Lean -- Symbol processing functions -- namespace Pantograph +namespace Condensed +-- Mirrors Lean's LocalDecl +structure LocalDecl where + -- Default value is for testing + fvarId: FVarId := { name := .anonymous } + userName: Name + + -- Normalized expression + type : Expr + value? : Option Expr := .none + +structure Goal where + mvarId: MVarId := { name := .anonymous } + userName: Name := .anonymous + context: Array LocalDecl + target: Expr + +@[export pantograph_goal_is_lhs] +def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome + +-- Functions for creating contexts and states +@[export pantograph_elab_context] +def elabContext: Elab.Term.Context := { + errToSorry := false + } + +end Condensed + +-- Get the list of visible (by default) free variables from a goal +@[export pantograph_visible_fvars_of_mvar] +protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do + let mvarDecl ← mctx.findDecl? mvarId + let lctx := mvarDecl.lctx + return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with + | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId + | none => r + +@[export pantograph_to_condensed_goal_m] +def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do + let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions) + let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions) + let mvarDecl ← mvarId.getDecl + let lctx := mvarDecl.lctx + let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances do + let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do + match localDecl with + | .cdecl _ fvarId userName type _ _ => + let type ← instantiate type + return { fvarId, userName, type } + | .ldecl _ fvarId userName type value _ _ => do + let userName := userName.simpMacroScopes + let type ← instantiate type + let value ← instantiate value + return { fvarId, userName, type, value? := .some value } + let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do + let skip := !ppAuxDecls && localDecl.isAuxDecl || + !ppImplDetailHyps && localDecl.isImplementationDetail + if skip then + return acc + else + let var ← ppVar localDecl + return var::acc + return { + mvarId, + userName := mvarDecl.userName, + context := vars.reverse.toArray, + target := ← instantiate mvarDecl.type + } + where + instantiate := instantiateAll + +@[export pantograph_goal_state_to_condensed_m] +protected def GoalState.toCondensed (state: GoalState): + CoreM (Array Condensed.Goal):= do + let metaM := do + let goals := state.goals.toArray + goals.mapM fun goal => do + match state.mctx.findDecl? goal with + | .some _ => + let serializedGoal ← toCondensedGoal goal + pure serializedGoal + | .none => throwError s!"Metavariable does not exist in context {goal.name}" + metaM.run' (s := state.savedState.term.meta.meta) --- Input Functions --- diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 8a5db24..a082f4b 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,4 +1,3 @@ -import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol diff --git a/Test/Common.lean b/Test/Common.lean index 2d98aca..3670cba 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,7 +1,6 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol -import Pantograph.Condensed import Lean import LSpec From 70f86f6e93856ee7e57ed6c0e24c184fd66d0615 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 14:34:15 -0800 Subject: [PATCH 3/6] doc: Update delation documentation --- Pantograph/Delate.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index c5954f0..a4f20d7 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -1,7 +1,5 @@ /- -All serialisation functions; -This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without -using `Scope`s. +This file handles "Delation": The conversion of Kernel view into Search view. -/ import Lean import Pantograph.Expr From ee8063e1f524894e196a5d13cb138568bb7e039a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 14:41:24 -0800 Subject: [PATCH 4/6] refactor: Merge all Delation functions --- Pantograph.lean | 3 +- Pantograph/Delate.lean | 197 +++++++++++++++++++++++++++++------- Pantograph/Elab.lean | 40 ++++++++ Pantograph/Environment.lean | 3 +- Pantograph/Expr.lean | 162 ----------------------------- Pantograph/Library.lean | 2 +- Repl.lean | 2 +- Test/Common.lean | 4 +- Test/Delate.lean | 4 +- Test/Metavar.lean | 2 +- Test/Proofs.lean | 2 +- 11 files changed, 210 insertions(+), 211 deletions(-) create mode 100644 Pantograph/Elab.lean delete mode 100644 Pantograph/Expr.lean diff --git a/Pantograph.lean b/Pantograph.lean index bad5f2a..822824c 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,7 +1,8 @@ +import Pantograph.Delate +import Pantograph.Elab import Pantograph.Environment import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol -import Pantograph.Delate import Pantograph.Version diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index a4f20d7..be17729 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -2,7 +2,7 @@ This file handles "Delation": The conversion of Kernel view into Search view. -/ import Lean -import Pantograph.Expr +import Std.Data.HashMap import Pantograph.Goal import Pantograph.Protocol @@ -11,6 +11,163 @@ open Lean -- Symbol processing functions -- namespace Pantograph + +structure ProjectionApplication where + projector: Name + numParams: Nat + inner: Expr + +@[export pantograph_expr_proj_to_app] +def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication := + let (typeName, idx, inner) := match e with + | .proj typeName idx inner => (typeName, idx, inner) + | _ => panic! "Argument must be proj" + let ctor := getStructureCtor env typeName + let fieldName := getStructureFields env typeName |>.get! idx + let projector := getProjFnForField? env typeName fieldName |>.get! + { + projector, + numParams := ctor.numParams, + inner, + } + +def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ + +/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ +@[export pantograph_unfold_aux_lemmas] +def unfoldAuxLemmas (e : Expr) : CoreM Expr := do + Lean.Meta.deltaExpand e Lean.Name.isAuxLemma + +/-- +Force the instantiation of delayed metavariables even if they cannot be fully +instantiated. This is used during resumption to provide diagnostic data about +the current goal. + +Since Lean 4 does not have an `Expr` constructor corresponding to delayed +metavariables, any delayed metavariables must be recursively handled by this +function to ensure that nested delayed metavariables can be properly processed. +The caveat is this recursive call will lead to infinite recursion if a loop +between metavariable assignment exists. + +This function ensures any metavariable in the result is either +1. Delayed assigned with its pending mvar not assigned in any form +2. Not assigned (delay or not) + -/ +partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do + --let padding := String.join $ List.replicate level "│ " + --IO.println s!"{padding}Starting {toString eOrig}" + let mut result ← Meta.transform (← instantiateMVars eOrig) + (pre := fun e => e.withApp fun f args => do + let .mvar mvarId := f | return .continue + --IO.println s!"{padding}├V {e}" + let mvarDecl ← mvarId.getDecl + + -- This is critical to maintaining the interdependency of metavariables. + -- Without setting `.syntheticOpaque`, Lean's metavariable elimination + -- system will not make the necessary delayed assigned mvars in case of + -- nested mvars. + mvarId.setKind .syntheticOpaque + + mvarId.withContext do + let lctx ← MonadLCtx.getLCtx + if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then + let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with + | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name] + | .none => acc) [] + panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}" + + if let .some assign ← getExprMVarAssignment? mvarId then + --IO.println s!"{padding}├A ?{mvarId.name}" + assert! !(← mvarId.isDelayedAssigned) + return .visit (mkAppN assign args) + else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList + --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]" + + if args.size < fvars.size then + throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments End" + if !(← mvarIdPending.isAssignedOrDelayedAssigned) then + --IO.println s!"{padding}├T1" + let result := mkAppN f args + return .done result + + let pending ← mvarIdPending.withContext do + let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) + --IO.println s!"{padding}├Pre: {inner}" + pure <| (← inner.abstractM fvars).instantiateRev args + + -- Tail arguments + let result := mkAppRange pending fvars.size args.size args + --IO.println s!"{padding}├MD {result}" + return .done result + else + assert! !(← mvarId.isAssigned) + assert! !(← mvarId.isDelayedAssigned) + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments End" + + --IO.println s!"{padding}├M ?{mvarId.name}" + return .done (mkAppN f args)) + --IO.println s!"{padding}└Result {result}" + return result + where + self e := instantiateDelayedMVars e --(level := level + 1) + +/-- +Convert an expression to an equiavlent form with +1. No nested delayed assigned mvars +2. No aux lemmas +3. No assigned mvars + -/ +@[export pantograph_instantiate_all_m] +def instantiateAll (e: Expr): MetaM Expr := do + let e ← instantiateDelayedMVars e + let e ← unfoldAuxLemmas e + return e + +structure DelayedMVarInvocation where + mvarIdPending: MVarId + args: Array (FVarId × (Option Expr)) + -- Extra arguments applied to the result of this substitution + tail: Array Expr + +-- The pending mvar of any delayed assigned mvar must not be assigned in any way. +@[export pantograph_to_delayed_mvar_invocation_m] +def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do + let .mvar mvarId := e.getAppFn | return .none + let .some decl ← getDelayedMVarAssignment? mvarId | return .none + let mvarIdPending := decl.mvarIdPending + let mvarDecl ← mvarIdPending.getDecl + -- Print the function application e. See Lean's `withOverApp` + let args := e.getAppArgs + + assert! args.size ≥ decl.fvars.size + assert! !(← mvarIdPending.isAssigned) + assert! !(← mvarIdPending.isDelayedAssigned) + let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList + let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do + let fvarId := localDecl.fvarId + let a := fvarArgMap[fvarId]? + return acc ++ [(fvarId, a)] + + assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome) + + return .some { + mvarIdPending, + args := subst.toArray, + tail := args.toList.drop decl.fvars.size |>.toArray, + } + +-- Condensed representation + namespace Condensed -- Mirrors Lean's LocalDecl @@ -32,12 +189,6 @@ structure Goal where @[export pantograph_goal_is_lhs] def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome --- Functions for creating contexts and states -@[export pantograph_elab_context] -def elabContext: Elab.Term.Context := { - errToSorry := false - } - end Condensed -- Get the list of visible (by default) free variables from a goal @@ -97,38 +248,6 @@ protected def GoalState.toCondensed (state: GoalState): | .none => throwError s!"Metavariable does not exist in context {goal.name}" metaM.run' (s := state.savedState.term.meta.meta) ---- Input Functions --- - -/-- Read syntax object from string -/ -def parseTerm (env: Environment) (s: String): Except String Syntax := - Parser.runParserCategory - (env := env) - (catName := `term) - (input := s) - (fileName := "") - -def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do - return Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := s) - (fileName := "") - -/-- Parse a syntax object. May generate additional metavariables! -/ -def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do - try - let expr ← Elab.Term.elabType syn - return .ok expr - catch ex => return .error (← ex.toMessageData.toString) -def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do - try - let expr ← Elab.Term.elabTerm (stx := syn) expectedType? - return .ok expr - catch ex => return .error (← ex.toMessageData.toString) - - ---- Output Functions --- - def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do Meta.forallTelescope expr fun arr body => do let binders ← arr.mapM fun fvar => do diff --git a/Pantograph/Elab.lean b/Pantograph/Elab.lean new file mode 100644 index 0000000..3c3b3cd --- /dev/null +++ b/Pantograph/Elab.lean @@ -0,0 +1,40 @@ +import Lean +open Lean + +namespace Pantograph + +-- Functions for creating contexts and states +@[export pantograph_default_elab_context] +def defaultElabContext: Elab.Term.Context := { + errToSorry := false + } + +/-- Read syntax object from string -/ +def parseTerm (env: Environment) (s: String): Except String Syntax := + Parser.runParserCategory + (env := env) + (catName := `term) + (input := s) + (fileName := "") + +def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do + return Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := "") + +/-- Parse a syntax object. May generate additional metavariables! -/ +def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do + try + let expr ← Elab.Term.elabType syn + return .ok expr + catch ex => return .error (← ex.toMessageData.toString) +def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do + try + let expr ← Elab.Term.elabTerm (stx := syn) expectedType? + return .ok expr + catch ex => return .error (← ex.toMessageData.toString) + + +end Pantograph diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 87e3a2f..40b3386 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,5 +1,6 @@ -import Pantograph.Protocol import Pantograph.Delate +import Pantograph.Elab +import Pantograph.Protocol import Lean open Lean diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean deleted file mode 100644 index a13ffec..0000000 --- a/Pantograph/Expr.lean +++ /dev/null @@ -1,162 +0,0 @@ -import Lean -import Std.Data.HashMap - -open Lean - -namespace Pantograph - -structure ProjectionApplication where - projector: Name - numParams: Nat - inner: Expr - -@[export pantograph_expr_proj_to_app] -def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication := - let (typeName, idx, inner) := match e with - | .proj typeName idx inner => (typeName, idx, inner) - | _ => panic! "Argument must be proj" - let ctor := getStructureCtor env typeName - let fieldName := getStructureFields env typeName |>.get! idx - let projector := getProjFnForField? env typeName fieldName |>.get! - { - projector, - numParams := ctor.numParams, - inner, - } - -def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ - -/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ -@[export pantograph_unfold_aux_lemmas] -def unfoldAuxLemmas (e : Expr) : CoreM Expr := do - Lean.Meta.deltaExpand e Lean.Name.isAuxLemma - -/-- -Force the instantiation of delayed metavariables even if they cannot be fully -instantiated. This is used during resumption to provide diagnostic data about -the current goal. - -Since Lean 4 does not have an `Expr` constructor corresponding to delayed -metavariables, any delayed metavariables must be recursively handled by this -function to ensure that nested delayed metavariables can be properly processed. -The caveat is this recursive call will lead to infinite recursion if a loop -between metavariable assignment exists. - -This function ensures any metavariable in the result is either -1. Delayed assigned with its pending mvar not assigned in any form -2. Not assigned (delay or not) - -/ -partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do - --let padding := String.join $ List.replicate level "│ " - --IO.println s!"{padding}Starting {toString eOrig}" - let mut result ← Meta.transform (← instantiateMVars eOrig) - (pre := fun e => e.withApp fun f args => do - let .mvar mvarId := f | return .continue - --IO.println s!"{padding}├V {e}" - let mvarDecl ← mvarId.getDecl - - -- This is critical to maintaining the interdependency of metavariables. - -- Without setting `.syntheticOpaque`, Lean's metavariable elimination - -- system will not make the necessary delayed assigned mvars in case of - -- nested mvars. - mvarId.setKind .syntheticOpaque - - mvarId.withContext do - let lctx ← MonadLCtx.getLCtx - if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then - let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with - | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name] - | .none => acc) [] - panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}" - - if let .some assign ← getExprMVarAssignment? mvarId then - --IO.println s!"{padding}├A ?{mvarId.name}" - assert! !(← mvarId.isDelayedAssigned) - return .visit (mkAppN assign args) - else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then - --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList - --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]" - - if args.size < fvars.size then - throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments Begin" - let args ← args.mapM self - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments End" - if !(← mvarIdPending.isAssignedOrDelayedAssigned) then - --IO.println s!"{padding}├T1" - let result := mkAppN f args - return .done result - - let pending ← mvarIdPending.withContext do - let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) - --IO.println s!"{padding}├Pre: {inner}" - pure <| (← inner.abstractM fvars).instantiateRev args - - -- Tail arguments - let result := mkAppRange pending fvars.size args.size args - --IO.println s!"{padding}├MD {result}" - return .done result - else - assert! !(← mvarId.isAssigned) - assert! !(← mvarId.isDelayedAssigned) - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments Begin" - let args ← args.mapM self - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments End" - - --IO.println s!"{padding}├M ?{mvarId.name}" - return .done (mkAppN f args)) - --IO.println s!"{padding}└Result {result}" - return result - where - self e := instantiateDelayedMVars e --(level := level + 1) - -/-- -Convert an expression to an equiavlent form with -1. No nested delayed assigned mvars -2. No aux lemmas -3. No assigned mvars - -/ -@[export pantograph_instantiate_all_m] -def instantiateAll (e: Expr): MetaM Expr := do - let e ← instantiateDelayedMVars e - let e ← unfoldAuxLemmas e - return e - -structure DelayedMVarInvocation where - mvarIdPending: MVarId - args: Array (FVarId × (Option Expr)) - -- Extra arguments applied to the result of this substitution - tail: Array Expr - --- The pending mvar of any delayed assigned mvar must not be assigned in any way. -@[export pantograph_to_delayed_mvar_invocation_m] -def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do - let .mvar mvarId := e.getAppFn | return .none - let .some decl ← getDelayedMVarAssignment? mvarId | return .none - let mvarIdPending := decl.mvarIdPending - let mvarDecl ← mvarIdPending.getDecl - -- Print the function application e. See Lean's `withOverApp` - let args := e.getAppArgs - - assert! args.size ≥ decl.fvars.size - assert! !(← mvarIdPending.isAssigned) - assert! !(← mvarIdPending.isDelayedAssigned) - let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList - let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do - let fvarId := localDecl.fvarId - let a := fvarArgMap[fvarId]? - return acc ++ [(fvarId, a)] - - assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome) - - return .some { - mvarIdPending, - args := subst.toArray, - tail := args.toList.drop decl.fvars.size |>.toArray, - } - -end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index a082f4b..20c7c9b 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -41,7 +41,7 @@ namespace Pantograph def runMetaM { α } (metaM: MetaM α): CoreM α := metaM.run' def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α := - termElabM.run' (ctx := Condensed.elabContext) |>.run' + termElabM.run' (ctx := defaultElabContext) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } diff --git a/Repl.lean b/Repl.lean index 7e8f0e4..041c0a6 100644 --- a/Repl.lean +++ b/Repl.lean @@ -22,7 +22,7 @@ abbrev CR α := Except Protocol.InteractionError α def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := metaM.run' def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := - termElabM.run' (ctx := Condensed.elabContext) |>.run' + termElabM.run' (ctx := defaultElabContext) |>.run' def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := diff --git a/Test/Common.lean b/Test/Common.lean index 3670cba..3998293 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -89,9 +89,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq := runCoreMSeq env metaM.run' def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := - termElabM.run' (ctx := Condensed.elabContext) + termElabM.run' (ctx := defaultElabContext) def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq := - runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext) + runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e diff --git a/Test/Delate.lean b/Test/Delate.lean index 57411e8..227ab24 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do | .ok expr => pure expr | .error e => return elabFailure e return LSpec.check source ((← serializeExpressionSexp expr) = target) - let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext) + let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext) return LSpec.TestSeq.append suites (← runMetaMSeq env metaM)) LSpec.TestSeq.done @@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let testCaseName := target.take 10 let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done - runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext) + runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext) -- Instance parsing def test_instance (env: Environment): IO LSpec.TestSeq := diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 84860b3..506e963 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -66,7 +66,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let coreContext: Lean.Core.Context ← createCoreContext #[] - let metaM := termElabM.run' (ctx := Condensed.elabContext) + let metaM := termElabM.run' (ctx := defaultElabContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 437bb64..8e3e2a2 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -74,7 +74,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let coreContext: Lean.Core.Context ← createCoreContext #[] - let metaM := termElabM.run' (ctx := Condensed.elabContext) + let metaM := termElabM.run' (ctx := defaultElabContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => From 495ea1ac144f524fe585979f7561470010599180 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 14:49:49 -0800 Subject: [PATCH 5/6] feat: Environment pickling --- Pantograph.lean | 1 + Pantograph/Environment.lean | 4 +- Pantograph/Serial.lean | 75 +++++++++++++++++++++++++++++++++++++ 3 files changed, 79 insertions(+), 1 deletion(-) create mode 100644 Pantograph/Serial.lean diff --git a/Pantograph.lean b/Pantograph.lean index 822824c..2c334b6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -5,4 +5,5 @@ import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol +import Pantograph.Serial import Pantograph.Version diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 40b3386..ad21284 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,7 +1,9 @@ import Pantograph.Delate import Pantograph.Elab import Pantograph.Protocol -import Lean +import Pantograph.Serial +import Lean.Environment +import Lean.Replay open Lean open Pantograph diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean new file mode 100644 index 0000000..c6aecae --- /dev/null +++ b/Pantograph/Serial.lean @@ -0,0 +1,75 @@ +import Lean.Environment +import Lean.Replay +import Std.Data.HashMap + +/-! +Input/Output functions + +# Pickling and unpickling objects + +By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk. +-/ + +open Lean + +namespace Pantograph + +/-- +Save an object to disk. +If you need to write multiple objects from within a single declaration, +you will need to provide a unique `key` for each. +-/ +def pickle {α : Type} (path : System.FilePath) (x : α) (key : Name := by exact decl_name%) : IO Unit := + saveModuleData path key (unsafe unsafeCast x) + +/-- +Load an object from disk. +Note: The returned `CompactedRegion` can be used to free the memory behind the value +of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are +released). Ignoring the `CompactedRegion` results in the data being leaked. +Use `withUnpickle` to call `CompactedRegion.free` automatically. + +This function is unsafe because the data being loaded may not actually have type `α`, and this +may cause crashes or other bad behavior. +-/ +unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × CompactedRegion) := do + let (x, region) ← readModuleData path + pure (unsafeCast x, region) + +/-- Load an object from disk and run some continuation on it, freeing memory afterwards. -/ +unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type} + (path : System.FilePath) (f : α → m β) : m β := do + let (x, region) ← unpickle α path + let r ← f x + region.free + pure r +end Pantograph + +namespace Lean.Environment + +/-- +Pickle an `Environment` to disk. + +We only store: +* the list of imports +* the new constants from `Environment.constants` +and when unpickling, we build a fresh `Environment` from the imports, +and then add the new constants. +-/ +@[export pantograph_env_pickle_m] +def pickle (env : Environment) (path : System.FilePath) : IO Unit := + Pantograph.pickle path (env.header.imports, env.constants.map₂) + +/-- +Unpickle an `Environment` from disk. + +We construct a fresh `Environment` with the relevant imports, +and then replace the new constants. +-/ +@[export pantograph_env_unpickle_m] +def unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do + let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path + let env ← importModules imports {} 0 + return (← env.replay (Std.HashMap.ofList map₂.toList), region) + +end Lean.Environment From 2790553180384fbed97d7707178f8dc72d95b1bb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 13 Nov 2024 19:50:31 -0800 Subject: [PATCH 6/6] feat: Environment save/load commands --- Pantograph/Protocol.lean | 6 +++++ Pantograph/Serial.lean | 10 +++----- Repl.lean | 54 ++++++++++++++++++++++++++-------------- 3 files changed, 45 insertions(+), 25 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 2ba073e..08c67ef 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -183,6 +183,12 @@ structure EnvAdd where structure EnvAddResult where deriving Lean.ToJson +structure EnvSaveLoad where + path: System.FilePath + deriving Lean.FromJson +structure EnvSaveLoadResult where + deriving Lean.ToJson + /-- Set options; See `Options` struct above for meanings -/ structure OptionsSet where printJsonPretty?: Option Bool diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index c6aecae..2f04bdb 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -1,5 +1,6 @@ import Lean.Environment import Lean.Replay +import Init.System.IOError import Std.Data.HashMap /-! @@ -43,9 +44,6 @@ unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type} let r ← f x region.free pure r -end Pantograph - -namespace Lean.Environment /-- Pickle an `Environment` to disk. @@ -57,7 +55,7 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def pickle (env : Environment) (path : System.FilePath) : IO Unit := +def env_pickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) /-- @@ -67,9 +65,9 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do +def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) -end Lean.Environment +end Pantograph diff --git a/Repl.lean b/Repl.lean index 041c0a6..e162f05 100644 --- a/Repl.lean +++ b/Repl.lean @@ -24,6 +24,7 @@ def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := termElabM.run' (ctx := defaultElabContext) |>.run' +/-- Main loop command of the REPL -/ def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with @@ -32,28 +33,35 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .ok result => return Lean.toJson result | .error ierror => return Lean.toJson ierror | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" - match command.cmd with - | "reset" => run reset - | "stat" => run stat - | "expr.echo" => run expr_echo - | "env.catalog" => run env_catalog - | "env.inspect" => run env_inspect - | "env.add" => run env_add - | "options.set" => run options_set - | "options.print" => run options_print - | "goal.start" => run goal_start - | "goal.tactic" => run goal_tactic - | "goal.continue" => run goal_continue - | "goal.delete" => run goal_delete - | "goal.print" => run goal_print - | "frontend.process" => run frontend_process - | cmd => - let error: Protocol.InteractionError := - errorCommand s!"Unknown command {cmd}" - return Lean.toJson error + try + match command.cmd with + | "reset" => run reset + | "stat" => run stat + | "expr.echo" => run expr_echo + | "env.catalog" => run env_catalog + | "env.inspect" => run env_inspect + | "env.add" => run env_add + | "env.save" => run env_save + | "env.load" => run env_load + | "options.set" => run options_set + | "options.print" => run options_print + | "goal.start" => run goal_start + | "goal.tactic" => run goal_tactic + | "goal.continue" => run goal_continue + | "goal.delete" => run goal_delete + | "goal.print" => run goal_print + | "frontend.process" => run frontend_process + | cmd => + let error: Protocol.InteractionError := + errorCommand s!"Unknown command {cmd}" + return Lean.toJson error + catch ex => do + let error ← ex.toMessageData.toString + return Lean.toJson $ errorIO error where errorCommand := errorI "command" errorIndex := errorI "index" + errorIO := errorI "io" newGoalState (goalState: GoalState) : MainM Nat := do let state ← get let stateId := state.nextId @@ -80,6 +88,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.inspect args state.options env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do Environment.addDecl args + env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do + let env ← Lean.MonadEnv.getEnv + env_pickle env args.path + return .ok {} + env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do + let (env, _) ← env_unpickle args.path + Lean.setEnv env + return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)