From ee8063e1f524894e196a5d13cb138568bb7e039a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 14:41:24 -0800 Subject: [PATCH] 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 =>