From ffbea41f627741e70e2b1d01ac8663b9acd12777 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 15:13:58 -0400 Subject: [PATCH 01/26] feat: Condensed interface --- Pantograph/Condensed.lean | 42 ++++++++++++++++++++++++++++++ Pantograph/Serial.lean | 54 ++++++++++++++++++++++++++++++++++++--- Test/Common.lean | 11 ++++++++ 3 files changed, 104 insertions(+), 3 deletions(-) create mode 100644 Pantograph/Condensed.lean diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean new file mode 100644 index 0000000..57a8517 --- /dev/null +++ b/Pantograph/Condensed.lean @@ -0,0 +1,42 @@ +/- structures for FFI based interface -/ +import Lean + +open Lean + +namespace Pantograph.Condensed + +/- +These two functions are for user defiend names. For internal names such as +`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to +construct hash maps for Lean names. +-/ +@[export pantograph_str_to_name] +def strToName (s: String) : Name := s.toName +@[export pantograph_name_to_str] +def nameToStr (s: String) : Name := s.toName +@[export pantograph_name_is_inaccessible] +def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName + +-- 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 + + + + +end Pantograph.Condensed diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index e729bee..2cdf3d6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -4,10 +4,10 @@ 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.Protocol import Pantograph.Goal +import Pantograph.Protocol open Lean @@ -201,6 +201,55 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol. dependentMVars?, } +@[export pantograph_to_condensed_goal] +def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do + let options: Protocol.Options := {} + let ppAuxDecls := options.printAuxDecls + let ppImplDetailHyps := options.printImplementationDetailHyps + 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] +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) + /-- Adapted from ppGoal -/ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) : MetaM Protocol.Goal := do @@ -214,7 +263,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do match localDecl with | .cdecl _ fvarId userName _ _ _ => - let userName := userName.simpMacroScopes return { name := ofName fvarId.name, userName:= ofName userName.simpMacroScopes, diff --git a/Test/Common.lean b/Test/Common.lean index c656309..e4e1d4c 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -8,6 +8,17 @@ open Lean namespace Pantograph +deriving instance Repr for Expr +-- Use strict equality check for expressions +--instance : BEq Expr := ⟨Expr.equal⟩ +instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) := + if h : Expr.equal x y then + .isTrue h + else + .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'" + +def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n + -- Auxiliary functions namespace Protocol def Goal.devolatilizeVars (goal: Goal): Goal := -- 2.44.1 From 8e78718447456d20b5c54e36384223ffad577bc3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 15:54:55 -0400 Subject: [PATCH 02/26] feat: Extract MetaM context and state from goal --- Pantograph/Goal.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 46888e7..2723c4f 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -63,9 +63,16 @@ protected def GoalState.mctx (state: GoalState): MetavarContext := protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env +@[export pantograph_goal_state_meta_context_of_goal] +protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do + let mvarDecl ← state.mctx.findDecl? mvarId + return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } +@[export pantograph_goal_state_meta_state] +protected def GoalState.metaState (state: GoalState): Meta.State := + state.savedState.term.meta.meta + protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do - let metaM := mvarId.withContext m - metaM.run' (← read) state.savedState.term.meta.meta + mvarId.withContext m |>.run' (← read) state.metaState protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do state.withContext state.parentMVar?.get! m @@ -82,6 +89,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac state.savedState.restore Elab.Tactic.setGoals [goal] + private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId := mctxNew.decls.foldl (fun acc mvarId mvarDecl => if let .some prevMVarDecl := mctxOld.decls.find? mvarId then -- 2.44.1 From 193d94e7986fef4779f5ce171616a1bc3ad0d068 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Jul 2024 11:42:02 -0700 Subject: [PATCH 03/26] feat: Expression creation and pretty printing --- Pantograph/Condensed.lean | 7 +++++++ Pantograph/Library.lean | 7 ++++--- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 57a8517..f6f4cdb 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -17,6 +17,13 @@ def nameToStr (s: String) : Name := s.toName @[export pantograph_name_is_inaccessible] def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName +@[export pantograph_mk_app_meta_m] +def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs + +@[export pantograph_pp_expr] +def ppExpr (e: Expr) := Meta.ppExpr e + + -- Mirrors Lean's LocalDecl structure LocalDecl where -- Default value is for testing diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 8036103..eb34614 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -78,9 +78,10 @@ def createCoreState (imports: Array String): IO Core.State := do (trustLevel := 1) return { env := env } -@[export pantograph_create_meta_context] -def createMetaContext: IO Lean.Meta.Context := do - return {} +@[export pantograph_meta_context] +def metaContext: Lean.Meta.Context := {} +@[export pantograph_meta_state] +def metaState: Lean.Meta.State := {} @[export pantograph_env_catalog_m] def envCatalog: CoreM Protocol.EnvCatalogResult := -- 2.44.1 From 94c7b021f77c02376ad0219cdef97b1a06bc0d1b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Jul 2024 12:22:47 -0700 Subject: [PATCH 04/26] fix: Signature of ppExpr --- Pantograph/Condensed.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index f6f4cdb..8b3de4f 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -20,8 +20,8 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName @[export pantograph_mk_app_meta_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs -@[export pantograph_pp_expr] -def ppExpr (e: Expr) := Meta.ppExpr e +@[export pantograph_pp_expr_meta_m] +def ppExpr (e: Expr): MetaM String := toString<$> Meta.ppExpr e -- Mirrors Lean's LocalDecl -- 2.44.1 From eb5ee8c57c395f60c6c7108e629ac248a3625c89 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Jul 2024 17:34:14 -0700 Subject: [PATCH 05/26] feat: Expose TermElab context and state --- Pantograph/Condensed.lean | 20 ++++++++++++++++---- Pantograph/Library.lean | 7 ++----- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 8b3de4f..a1688f1 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -13,15 +13,15 @@ construct hash maps for Lean names. @[export pantograph_str_to_name] def strToName (s: String) : Name := s.toName @[export pantograph_name_to_str] -def nameToStr (s: String) : Name := s.toName +def nameToStr (s: Name) : String := s.toString @[export pantograph_name_is_inaccessible] def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName -@[export pantograph_mk_app_meta_m] +@[export pantograph_mk_app_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs -@[export pantograph_pp_expr_meta_m] -def ppExpr (e: Expr): MetaM String := toString<$> Meta.ppExpr e +@[export pantograph_pp_expr_m] +def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e -- Mirrors Lean's LocalDecl @@ -44,6 +44,18 @@ structure Goal where def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome +-- Functions for creating contexts and states +@[export pantograph_meta_context] +def metaContext: Meta.Context := {} +@[export pantograph_meta_state] +def metaState: Meta.State := {} +@[export pantograph_elab_context] +def elabContext: Meta.Context := {} +@[export pantograph_elab_state] +def elabState (levelNames: Array Name): Elab.Term.State := { + levelNames := levelNames.toList, + } + end Pantograph.Condensed diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index eb34614..3bc3cc1 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -78,11 +78,6 @@ def createCoreState (imports: Array String): IO Core.State := do (trustLevel := 1) return { env := env } -@[export pantograph_meta_context] -def metaContext: Lean.Meta.Context := {} -@[export pantograph_meta_state] -def metaState: Lean.Meta.State := {} - @[export pantograph_env_catalog_m] def envCatalog: CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) @@ -99,6 +94,7 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } +@[export pantograph_parse_elab_type_m] def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do let env ← MonadEnv.getEnv let syn ← match parseTerm env type with @@ -109,6 +105,7 @@ def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do | .ok expr => return .ok (← instantiateMVars expr) /-- This must be a TermElabM since the parsed expr contains extra information -/ +@[export pantograph_parse_elab_expr_m] def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do let env ← MonadEnv.getEnv let expectedType? ← match ← expectedType?.mapM parseElabType with -- 2.44.1 From 431ca4e481fb1856d36ed17f322419ab59ed8e25 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Jul 2024 17:57:01 -0700 Subject: [PATCH 06/26] fix: Move elab context to condensed --- Pantograph/Condensed.lean | 5 +++-- Pantograph/Library.lean | 6 ++---- Test/Common.lean | 2 +- Test/Metavar.lean | 2 +- Test/Proofs.lean | 2 +- Test/Serial.lean | 4 ++-- 6 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index a1688f1..ac41133 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -50,12 +50,13 @@ def metaContext: Meta.Context := {} @[export pantograph_meta_state] def metaState: Meta.State := {} @[export pantograph_elab_context] -def elabContext: Meta.Context := {} +def elabContext: Elab.Term.Context := { + errToSorry := false + } @[export pantograph_elab_state] def elabState (levelNames: Array Name): Elab.Term.State := { levelNames := levelNames.toList, } - end Pantograph.Condensed diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 3bc3cc1..2f37cfa 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,3 +1,4 @@ +import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol @@ -38,13 +39,10 @@ open Lean namespace Pantograph -def defaultTermElabMContext: Elab.Term.Context := { - errToSorry := false - } def runMetaM { α } (metaM: MetaM α): CoreM α := metaM.run' def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α := - termElabM.run' (ctx := defaultTermElabMContext) |>.run' + termElabM.run' (ctx := Condensed.elabContext) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } diff --git a/Test/Common.lean b/Test/Common.lean index e4e1d4c..4b17736 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -73,7 +73,7 @@ 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 := Pantograph.defaultTermElabMContext) + termElabM.run' (ctx := Pantograph.Condensed.elabContext) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 0818881..4ac8454 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -67,7 +67,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 := defaultTermElabMContext) + let metaM := termElabM.run' (ctx := Condensed.elabContext) 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 9c45138..51e869d 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -76,7 +76,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 := defaultTermElabMContext) + let metaM := termElabM.run' (ctx := Condensed.elabContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => diff --git a/Test/Serial.lean b/Test/Serial.lean index 2d2b9d1..1c00501 100644 --- a/Test/Serial.lean +++ b/Test/Serial.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 := defaultTermElabMContext) + let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext) 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 := defaultTermElabMContext) + runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext) -- Instance parsing def test_instance (env: Environment): IO LSpec.TestSeq := -- 2.44.1 From 3b415e8dc12485f7b2b9fa6f54329f6ad598d48f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 23 Jul 2024 05:16:46 -0700 Subject: [PATCH 07/26] chore: Rename exports --- Pantograph/Expr.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 63331af..8ef0aa6 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -98,7 +98,7 @@ Convert an expression to an equiavlent form with 2. No aux lemmas 3. No assigned mvars -/ -@[export pantograph_instantiate_all_meta_m] +@[export pantograph_instantiate_all_m] def instantiateAll (e: Expr): MetaM Expr := do let e ← instantiateDelayedMVars e let e ← unfoldAuxLemmas e @@ -111,7 +111,7 @@ structure DelayedMVarInvocation where tail: Array Expr -- The pending mvar of any delayed assigned mvar must not be assigned in any way. -@[export pantograph_to_delayed_mvar_invocation_meta_m] +@[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 -- 2.44.1 From 2682ce5b7b5a7e494d166b20b17852e88bea448a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 23 Jul 2024 11:57:12 -0700 Subject: [PATCH 08/26] refactor: Move condensed functions to condensed --- Pantograph/Condensed.lean | 58 +++++++++++++++++++++++++++++++++++++-- Pantograph/Serial.lean | 48 -------------------------------- 2 files changed, 56 insertions(+), 50 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index ac41133..90fc050 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -1,9 +1,13 @@ /- structures for FFI based interface -/ import Lean +import Pantograph.Goal +import Pantograph.Expr +import Pantograph.Protocol open Lean -namespace Pantograph.Condensed +namespace Pantograph +namespace Condensed /- These two functions are for user defiend names. For internal names such as @@ -58,5 +62,55 @@ def elabState (levelNames: Array Name): Elab.Term.State := { levelNames := levelNames.toList, } +end Condensed -end Pantograph.Condensed +@[export pantograph_to_condensed_goal_m] +def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do + let options : Protocol.Options := {} + let ppAuxDecls := options.printAuxDecls + let ppImplDetailHyps := options.printImplementationDetailHyps + 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/Serial.lean b/Pantograph/Serial.lean index 2cdf3d6..87353e2 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -201,54 +201,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol. dependentMVars?, } -@[export pantograph_to_condensed_goal] -def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do - let options: Protocol.Options := {} - let ppAuxDecls := options.printAuxDecls - let ppImplDetailHyps := options.printImplementationDetailHyps - 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] -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) /-- Adapted from ppGoal -/ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) -- 2.44.1 From bf941cd6862b2658146dbdde9db8079e7e08973e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 27 Jul 2024 17:39:51 -0700 Subject: [PATCH 09/26] feat: Expose parent and root expr functions --- Pantograph/Goal.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index c441ad9..398386e 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -136,6 +136,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except else target.resume (goals := branch.goals) +@[export pantograph_goal_state_root_expr] protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) @@ -146,12 +147,14 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do else assert! goalState.goals.isEmpty return expr +@[export pantograph_goal_state_parent_expr] protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let parent ← goalState.parentMVar? let expr := goalState.mctx.eAssignment.find! parent let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr -protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do +@[export pantograph_goal_state_get_mvar_e_assignment] +protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do let expr ← goalState.mctx.eAssignment.find? mvar let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr -- 2.44.1 From 9db546349925730b445b6cf66fff29cc9dfcc52c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 27 Jul 2024 18:20:34 -0700 Subject: [PATCH 10/26] feat: Export `GoalState.resume` --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 398386e..b44e8d3 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -108,6 +108,7 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState /-- Brings into scope a list of goals -/ +@[export pantograph_goal_state_resume] protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := if ¬ (goals.all (λ goal => state.mvars.contains goal)) then let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString) -- 2.44.1 From 4c81f226d1953aa93c131d5161b397a037f920a2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 28 Jul 2024 13:46:14 -0700 Subject: [PATCH 11/26] feat: Expose environment functions --- Pantograph/Condensed.lean | 4 +++- Pantograph/Environment.lean | 22 +++++++++++++++++++--- Pantograph/Expr.lean | 1 + 3 files changed, 23 insertions(+), 4 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 90fc050..8b5c313 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -19,13 +19,15 @@ def strToName (s: String) : Name := s.toName @[export pantograph_name_to_str] def nameToStr (s: Name) : String := s.toString @[export pantograph_name_is_inaccessible] -def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName +def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes @[export pantograph_mk_app_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs @[export pantograph_pp_expr_m] def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e +@[export pantograph_get_used_constants] +def getUsedConstants (e: Expr) := e.getUsedConstants -- Mirrors Lean's LocalDecl diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 6d91abb..a9b2934 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -7,15 +7,31 @@ open Pantograph namespace Pantograph.Environment -def isNameInternal (n: Lean.Name): Bool := +@[export pantograph_is_name_internal] +def isNameInternal (n: Name): Bool := -- Returns true if the name is an implementation detail which should not be shown to the user. isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes where - isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with + isLeanSymbol (name: Name): Bool := match name.getRoot with | .str _ name => name == "Lean" | _ => true -def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String := +/-- Catalog all the non-internal names -/ +@[export pantograph_environment_catalog] +def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ => + match isNameInternal name with + | true => acc.push name + | false => acc) + +@[export pantograph_environment_module_of_name] +def module_of_name (env: Environment) (name: Name): Option Name := do + let moduleId ← env.getModuleIdxFor? name + return env.allImportedModuleNames.get! moduleId.toNat + +@[export pantograph_constant_info_is_unsafe_or_partial] +def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial + +def toCompactSymbolName (n: Name) (info: ConstantInfo): String := let pref := match info with | .axiomInfo _ => "a" | .defnInfo _ => "d" diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 8ef0aa6..9d8f70c 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -7,6 +7,7 @@ namespace Pantograph 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 -- 2.44.1 From 29f437f859e3c7fad5a48fdce1fddc106991e586 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 28 Jul 2024 13:58:20 -0700 Subject: [PATCH 12/26] feat: Export GoalState.create --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b44e8d3..6dbe525 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -33,6 +33,7 @@ structure GoalState where -- WARNING: If using `state with` outside of `calc`, this must be set to `.none` calcPrevRhs?: Option Expr := .none +@[export pantograph_goal_state_create_m] protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 -- 2.44.1 From 7b5567d784397c9d2a33b9464b5a1dd75fceb34a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 28 Jul 2024 14:19:47 -0700 Subject: [PATCH 13/26] fix: Name internal order --- Pantograph/Environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index a9b2934..d89486c 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -20,8 +20,8 @@ def isNameInternal (n: Name): Bool := @[export pantograph_environment_catalog] def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ => match isNameInternal name with - | true => acc.push name - | false => acc) + | false => acc.push name + | true => acc) @[export pantograph_environment_module_of_name] def module_of_name (env: Environment) (name: Name): Option Name := do -- 2.44.1 From 1c9a411d4d89db0bfc38cee2e2d0ff5f61a8c61b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 29 Jul 2024 18:39:22 -0700 Subject: [PATCH 14/26] feat: Export constant info type/value --- Pantograph/Environment.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index d89486c..37faf72 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -16,10 +16,10 @@ def isNameInternal (n: Name): Bool := | .str _ name => name == "Lean" | _ => true -/-- Catalog all the non-internal names -/ +/-- Catalog all the non-internal and safe names -/ @[export pantograph_environment_catalog] -def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ => - match isNameInternal name with +def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info => + match isNameInternal name || info.isUnsafe with | false => acc.push name | true => acc) @@ -31,6 +31,11 @@ def module_of_name (env: Environment) (name: Name): Option Name := do @[export pantograph_constant_info_is_unsafe_or_partial] def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial +@[export pantograph_constant_info_type] +def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type +@[export pantograph_constant_info_value] +def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas + def toCompactSymbolName (n: Name) (info: ConstantInfo): String := let pref := match info with | .axiomInfo _ => "a" -- 2.44.1 From 3ca52517abe07ecd1c2036eeba4e2ba762299f9f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 30 Jul 2024 13:30:41 -0700 Subject: [PATCH 15/26] feat: Refactor out projToApp --- Pantograph/Expr.lean | 20 ++++++++++++++++++++ Pantograph/Serial.lean | 13 +++++-------- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 9d8f70c..cbee9a5 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -4,6 +4,26 @@ 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. -/ diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 87353e2..21bffce 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -168,15 +168,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- It may become necessary to incorporate the metadata. self inner - | .proj typeName idx inner => do + | .proj _ _ _ => do let env ← getEnv - let ctor := getStructureCtor env typeName - let fieldName := getStructureFields env typeName |>.get! idx - let projectorName := getProjFnForField? env typeName fieldName |>.get! - - let autos := String.intercalate " " (List.replicate ctor.numParams "_") - let inner ← self inner - pure s!"((:c {projectorName}) {autos} {inner})" + let projApp := exprProjToApp env e + let autos := String.intercalate " " (List.replicate projApp.numParams "_") + let inner ← self projApp.inner + pure s!"((:c {projApp.projector}) {autos} {inner})" -- Elides all unhygenic names binderInfoSexp : Lean.BinderInfo → String | .default => "" -- 2.44.1 From caa463f41010326d1f7c213ae2614b9fabacb73d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 30 Jul 2024 17:02:41 -0700 Subject: [PATCH 16/26] feat: Export GoalState.goalsArray --- Pantograph/Expr.lean | 1 - Pantograph/Goal.lean | 2 ++ Pantograph/Library.lean | 11 ----------- 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index cbee9a5..f989575 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -23,7 +23,6 @@ def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication := 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. -/ diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 6dbe525..26a8da1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -54,6 +54,8 @@ protected def GoalState.isConv (state: GoalState): Bool := state.convMVar?.isSome protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals +@[export pantograph_goal_state_goals] +protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx protected def GoalState.env (state: GoalState): Environment := diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 2f37cfa..5aa8f35 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -76,17 +76,6 @@ def createCoreState (imports: Array String): IO Core.State := do (trustLevel := 1) return { env := env } -@[export pantograph_env_catalog_m] -def envCatalog: CoreM Protocol.EnvCatalogResult := - Environment.catalog ({}: Protocol.EnvCatalog) - -@[export pantograph_env_inspect_m] -def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): - CoreM (Protocol.CR Protocol.EnvInspectResult) := - Environment.inspect ({ - name, value? := .some value, dependency?:= .some dependency - }: Protocol.EnvInspect) options - @[export pantograph_env_add_m] def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): CoreM (Protocol.CR Protocol.EnvAddResult) := -- 2.44.1 From abef7a6f0d55de552c3c7297d25ece8121ee931d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 31 Jul 2024 00:00:21 -0700 Subject: [PATCH 17/26] feat: Export fvar names function --- Pantograph/Goal.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 26a8da1..0e87a12 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -69,6 +69,11 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta +@[export pantograph_goal_state_fvar_names_of_goal] +protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do + let mvarDecl ← state.mctx.findDecl? mvarId + return mvarDecl.lctx.getFVarIds + protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState -- 2.44.1 From 651afa75f4cb8cbd10c77247e055177c5adeed56 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 19:49:11 -0700 Subject: [PATCH 18/26] feat: Filter in `visibleFVarsOfMVar` --- Pantograph/Condensed.lean | 14 +++++++++++--- Pantograph/Goal.lean | 10 +++++++--- 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 8b5c313..1db3c62 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -66,11 +66,19 @@ def elabState (levelNames: Array Name): Elab.Term.State := { 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 options : Protocol.Options := {} - let ppAuxDecls := options.printAuxDecls - let ppImplDetailHyps := options.printImplementationDetailHyps + 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) } diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0e87a12..ccb7a3d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -69,10 +69,14 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta -@[export pantograph_goal_state_fvar_names_of_goal] -protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do +-- Get the list of visible free variables from a goal +@[export pantograph_goal_state_visible_fvars] +protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do let mvarDecl ← state.mctx.findDecl? mvarId - return mvarDecl.lctx.getFVarIds + 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 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState -- 2.44.1 From 2c08ef1e23a3429cefb5aacad19819a92768a847 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 19:53:19 -0700 Subject: [PATCH 19/26] refactor: Remove old `visibleFVars` interface --- Pantograph/Goal.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ccb7a3d..26a8da1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -69,15 +69,6 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta --- Get the list of visible free variables from a goal -@[export pantograph_goal_state_visible_fvars] -protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do - let mvarDecl ← state.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 - protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState -- 2.44.1 From c0e2a592ea819389bd5a39d289aabdd3d7a26a75 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 21:44:46 -0700 Subject: [PATCH 20/26] feat: Expose `mkAppM'` --- Pantograph/Condensed.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 1db3c62..fcd70a0 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -23,6 +23,8 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco @[export pantograph_mk_app_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs +@[export pantograph_mk_app_m_expr] +def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs @[export pantograph_pp_expr_m] def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e -- 2.44.1 From 394fb731375785d268184c640cd387f44d76dac4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 22:00:27 -0700 Subject: [PATCH 21/26] feat: Add direct expression to string --- Pantograph/Condensed.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index fcd70a0..9c20f32 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -23,9 +23,11 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco @[export pantograph_mk_app_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs -@[export pantograph_mk_app_m_expr] +@[export pantograph_mk_app_expr_m] def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs +@[export pantograph_expr_to_string] +def exprToString (e: Expr): String := toString e @[export pantograph_pp_expr_m] def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e @[export pantograph_get_used_constants] -- 2.44.1 From c9ee31bbfdd215e5ceba960218c8344afd46954e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 22:33:03 -0700 Subject: [PATCH 22/26] feat: Export `mkFun` --- Pantograph/Condensed.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 9c20f32..8696523 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -25,6 +25,14 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs @[export pantograph_mk_app_expr_m] def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs +-- Copies same function in `Meta/AppBuilder.lean` +@[export pantograph_mk_fun_m] +def mkFun (constName : Name) : MetaM (Expr × Expr) := do + let cinfo ← getConstInfo constName + let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar + let f := mkConst constName us + let fType ← Meta.instantiateTypeLevelParams cinfo us + return (f, fType) @[export pantograph_expr_to_string] def exprToString (e: Expr): String := toString e -- 2.44.1 From 64269868d518b1211b724a46dc080d6f2f5a4a44 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 4 Aug 2024 17:32:20 -0700 Subject: [PATCH 23/26] feat: Expose project and leanPkgs in flake --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index b96d5e2..54a139f 100644 --- a/flake.nix +++ b/flake.nix @@ -63,6 +63,7 @@ packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; + inherit project leanPkgs; default = project.executable; }; checks = { -- 2.44.1 From caac70f0cfedca3964f65d2dbd04a8370c5dd97f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 4 Aug 2024 17:52:36 -0700 Subject: [PATCH 24/26] feat: Move non package outputs to dependencies --- flake.nix | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 54a139f..2b68c0c 100644 --- a/flake.nix +++ b/flake.nix @@ -63,9 +63,11 @@ packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; - inherit project leanPkgs; default = project.executable; }; + dependencies = { + inherit project leanPkgs; + }; checks = { test = pkgs.runCommand "test" { buildInputs = [ test.executable leanPkgs.lean-all ]; -- 2.44.1 From 0bc7bc58565cceb839c41a11d207e4eeb64a845e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 14 Aug 2024 01:20:56 -0700 Subject: [PATCH 25/26] refactor: Remove export of Lean functions If the user wishes to use Lean functions, they should add the bindings manually. --- Pantograph/Condensed.lean | 42 --------------------------------------- flake.nix | 4 +--- 2 files changed, 1 insertion(+), 45 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 8696523..c47f882 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -9,39 +9,6 @@ open Lean namespace Pantograph namespace Condensed -/- -These two functions are for user defiend names. For internal names such as -`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to -construct hash maps for Lean names. --/ -@[export pantograph_str_to_name] -def strToName (s: String) : Name := s.toName -@[export pantograph_name_to_str] -def nameToStr (s: Name) : String := s.toString -@[export pantograph_name_is_inaccessible] -def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes - -@[export pantograph_mk_app_m] -def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs -@[export pantograph_mk_app_expr_m] -def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs --- Copies same function in `Meta/AppBuilder.lean` -@[export pantograph_mk_fun_m] -def mkFun (constName : Name) : MetaM (Expr × Expr) := do - let cinfo ← getConstInfo constName - let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar - let f := mkConst constName us - let fType ← Meta.instantiateTypeLevelParams cinfo us - return (f, fType) - -@[export pantograph_expr_to_string] -def exprToString (e: Expr): String := toString e -@[export pantograph_pp_expr_m] -def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e -@[export pantograph_get_used_constants] -def getUsedConstants (e: Expr) := e.getUsedConstants - - -- Mirrors Lean's LocalDecl structure LocalDecl where -- Default value is for testing @@ -61,20 +28,11 @@ 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_meta_context] -def metaContext: Meta.Context := {} -@[export pantograph_meta_state] -def metaState: Meta.State := {} @[export pantograph_elab_context] def elabContext: Elab.Term.Context := { errToSorry := false } -@[export pantograph_elab_state] -def elabState (levelNames: Array Name): Elab.Term.State := { - levelNames := levelNames.toList, - } end Condensed diff --git a/flake.nix b/flake.nix index 2b68c0c..54a139f 100644 --- a/flake.nix +++ b/flake.nix @@ -63,10 +63,8 @@ packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; - default = project.executable; - }; - dependencies = { inherit project leanPkgs; + default = project.executable; }; checks = { test = pkgs.runCommand "test" { -- 2.44.1 From e943a4b065cc78c268fcd3ca31ff57d7d3e4b697 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 22:39:40 -0700 Subject: [PATCH 26/26] refactor: Assign into its own tactic --- Pantograph/Goal.lean | 68 ++++++----------------------------- Pantograph/Library.lean | 19 ---------- Pantograph/Serial.lean | 6 ++-- Pantograph/Tactic.lean | 1 + Pantograph/Tactic/Assign.lean | 35 ++++++++++++++++++ Test/Metavar.lean | 4 +-- 6 files changed, 52 insertions(+), 81 deletions(-) create mode 100644 Pantograph/Tactic/Assign.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 26a8da1..136379a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -178,13 +178,14 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message: String) -protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): - Elab.TermElabM TacticResult := do +/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ +protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): + Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.execute + goal.checkNotAssigned `GoalState.executeTactic try let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } if (← getThe Core.State).messages.hasErrors then @@ -204,7 +205,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab. catch exception => return .failure #[← exception.toMessageData.toString] -/-- Execute tactic on given state -/ +/-- Execute a string tactic on given state -/ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): Elab.TermElabM TacticResult := do let tactic ← match Parser.runParserCategory @@ -214,68 +215,19 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri (fileName := filename) with | .ok stx => pure $ stx | .error error => return .parseError error - state.execute goalId $ Elab.Tactic.evalTactic tactic - -/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ -protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): - Elab.TermElabM TacticResult := do - let goalType ← goal.getType - try - -- For some reason this is needed. One of the unit tests will fail if this isn't here - let error?: Option String ← goal.withContext do - let exprType ← Meta.inferType expr - if ← Meta.isDefEq goalType exprType then - pure .none - else do - return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}" - if let .some error := error? then - return .parseError error - goal.checkNotAssigned `GoalState.assign - goal.assign expr - if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.toArray - let errors ← (messages.map (·.data)).mapM fun md => md.toString - return .failure errors - let prevMCtx := state.savedState.term.meta.meta.mctx - let nextMCtx ← getMCtx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - let newMVars := newMVarSet prevMCtx nextMCtx - let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned) - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - newMVars, - parentMVar? := .some goal, - calcPrevRhs? := .none - } - catch exception => - return .failure #[← exception.toMessageData.toString] + state.executeTactic goalId $ Elab.Tactic.evalTactic tactic protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): Elab.TermElabM TacticResult := do state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryAssign let expr ← match Parser.runParserCategory - (env := state.env) + (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - let goalType ← goal.getType - try - let expr ← goal.withContext $ - Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType) - state.assign goal expr - catch exception => - return .failure #[← exception.toMessageData.toString] + state.executeTactic goalId $ Tactic.evalAssign expr -- Specialized Tactics @@ -535,7 +487,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.motivatedApply recursor) + state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor) protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM @@ -546,6 +498,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.noConfuse recursor) + state.executeTactic goalId (tacticM := Tactic.noConfuse recursor) end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 5aa8f35..59197f6 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -154,9 +154,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G state.withParentContext do serializeExpression options (← instantiateAll expr)), } -@[export pantograph_goal_diag_m] -def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String := - runMetaM $ state.diag diagOptions @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult := @@ -189,20 +186,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq -inductive SyntheticTactic where - | congruenceArg - | congruenceFun - | congruence -/-- Executes a synthetic tactic which has no arguments -/ -@[export pantograph_goal_synthetic_tactic_m] -def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult := - runTermElabM do - state.restoreElabM - state.execute goalId $ match case with - | .congruenceArg => Tactic.congruenceArg - | .congruenceFun => Tactic.congruenceFun - | .congruence => Tactic.congruence - - - end Pantograph diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 21bffce..6a10309 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -286,7 +286,8 @@ protected def GoalState.serializeGoals | .none => throwError s!"Metavariable does not exist in context {goal.name}" /-- Print the metavariables in a readable format -/ -protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do +@[export pantograph_goal_state_diag_m] +protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do goalState.restoreMetaM let savedState := goalState.savedState let goals := savedState.tactic.goals @@ -305,7 +306,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) => !(goals.contains mvarId || mvarId == root) && options.printAll) |>.mapM (fun (mvarId, decl) => do - let pref := if goalState.newMVars.contains mvarId then "~" else " " + let pref := if parentHasMVar mvarId then " " else "~" printMVar pref mvarId decl ) pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) @@ -345,5 +346,6 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag userNameToString : Name → String | .anonymous => "" | other => s!"[{other}]" + parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true end Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 225ad31..8efebc8 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -1,4 +1,5 @@ +import Pantograph.Tactic.Assign import Pantograph.Tactic.Congruence import Pantograph.Tactic.MotivatedApply import Pantograph.Tactic.NoConfuse diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean new file mode 100644 index 0000000..cd9281f --- /dev/null +++ b/Pantograph/Tactic/Assign.lean @@ -0,0 +1,35 @@ +import Lean + +open Lean + +namespace Pantograph.Tactic + +private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId := + mctxNew.decls.foldl (fun acc mvarId mvarDecl => + if let .some prevMVarDecl := mctxOld.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + acc + else + acc.insert mvarId + ) SSet.empty +def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do + goal.checkNotAssigned `Pantograph.Tactic.assign + + -- This run of the unifier is critical in resolving mvars in passing + let exprType ← Meta.inferType expr + let goalType ← goal.getType + unless ← Meta.isDefEq goalType exprType do + throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}" + + let nextGoals ← Meta.getMVars expr + goal.assign expr + nextGoals.toList.filterM (not <$> ·.isAssigned) + +def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do + let goalType ← Elab.Tactic.getMainTarget + let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType) + let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr + Elab.Tactic.setGoals nextGoals + + +end Pantograph.Tactic diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 4ac8454..3849b44 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -198,10 +198,10 @@ def test_proposition_generation: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) + #[.some "∀ (x : Nat), ?m.29 x"]) addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString -- 2.44.1