diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index ad923aa..efb1008 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -37,7 +37,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection := def anonymousLevel : Level := .mvar ⟨.anonymous⟩ @[export pantograph_expr_proj_to_app] -def exprProjToApp (env: Environment) (e: Expr): Expr := +def exprProjToApp (env : Environment) (e : Expr) : Expr := let anon : Expr := .mvar ⟨.anonymous⟩ match analyzeProjection env e with | .field projector numParams => @@ -66,9 +66,18 @@ def exprProjToApp (env: Environment) (e: Expr): Expr := 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 +@[export pantograph_unfold_aux_lemmas_m] +def unfoldAuxLemmas : Expr → CoreM Expr := + (Meta.deltaExpand · Lean.Name.isAuxLemma) +/-- Unfold all matcher applications -/ +@[export pantograph_unfold_matchers_m] +def unfoldMatchers (expr : Expr) : CoreM Expr := + Core.transform expr λ e => do + let .some mapp ← Meta.matchMatcherApp? e | return .continue e + let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist" + let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList + let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName) + return .visit $ .mdata mdata (f.betaRev e.getAppRevArgs (useZeta := true)) /-- Force the instantiation of delayed metavariables even if they cannot be fully @@ -85,91 +94,92 @@ 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 +partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr := + withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do + let mut result ← Meta.transform (← instantiateMVars expr) + λ e => e.withApp fun f args => do + let .mvar mvarId := f | return .continue + trace[Pantograph.Delate] "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 + -- 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}" + 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 let .some assign ← getExprMVarAssignment? mvarId then + trace[Pantograph.Delate] "A ?{mvarId.name}" + assert! !(← mvarId.isDelayedAssigned) + return .visit (mkAppN assign args) + else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + if ← isTracingEnabledFor `Pantograph.Delate then + let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList + trace[Pantograph.Delate]"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}" + 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 expr}" + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments Begin" + let args ← args.mapM self + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments End" + if !(← mvarIdPending.isAssignedOrDelayedAssigned) then + trace[Pantograph.Delate] "T1" + let result := mkAppN f args 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}" + let pending ← mvarIdPending.withContext do + let inner ← instantiateDelayedMVars (.mvar mvarIdPending) + trace[Pantograph.Delate] "Pre: {inner}" + pure <| (← inner.abstractM fvars).instantiateRev args + + -- Tail arguments + let result := mkAppRange pending fvars.size args.size args + trace[Pantograph.Delate] "MD {result}" + return .done result + else + assert! !(← mvarId.isAssigned) + assert! !(← mvarId.isDelayedAssigned) + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments Begin" + let args ← args.mapM self + if !args.isEmpty then + trace[Pantograph.Delate] "─ Arguments End" + + trace[Pantograph.Delate] "M ?{mvarId.name}" + return .done (mkAppN f args) + trace[Pantoraph.Delate] "Result {result}" return result where - self e := instantiateDelayedMVars e --(level := level + 1) + self e := instantiateDelayedMVars e /-- Convert an expression to an equiavlent form with 1. No nested delayed assigned mvars -2. No aux lemmas +2. No aux lemmas or matchers 3. No assigned mvars -/ @[export pantograph_instantiate_all_m] -def instantiateAll (e: Expr): MetaM Expr := do +def instantiateAll (e : Expr) : MetaM Expr := do let e ← instantiateDelayedMVars e let e ← unfoldAuxLemmas e + let e ← unfoldMatchers e return e structure DelayedMVarInvocation where - mvarIdPending: MVarId - args: Array (FVarId × (Option Expr)) + mvarIdPending : MVarId + args : Array (FVarId × (Option Expr)) -- Extra arguments applied to the result of this substitution - tail: Array Expr + 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] @@ -594,4 +604,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState : | other => s!"[{other}]" parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true +initialize + registerTraceClass `Pantograph.Delate + end Pantograph diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index c6592d2..8067d17 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -62,7 +62,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do let sourceMCtx ← getSourceMCtx -- We want to create as few mvars as possible let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr - --IO.println s!"Transform src: {srcExpr}" + trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}" let result ← Core.transform srcExpr λ e => do let state ← get match e with @@ -100,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD addTranslatedFVar srcLocalDecl.fvarId fvarId match srcLocalDecl with | .cdecl index _ userName type bi kind => do - --IO.println s!"[CD] {userName} {toString type}" + trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}" return .cdecl index fvarId userName (← translateExpr type) bi kind | .ldecl index _ userName type value nonDep kind => do - --IO.println s!"[LD] {toString type} := {toString value}" + trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}" return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind partial def translateLCtx : MetaTranslateM LocalContext := do @@ -162,4 +162,7 @@ end MetaTranslate export MetaTranslate (MetaTranslateM) +initialize + registerTraceClass `Pantograph.Frontend.MetaTranslate + end Pantograph.Frontend diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 164b72a..7924db7 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -346,10 +346,9 @@ structure FrontendProcess where -- One of these two must be supplied: Either supply the file name or the content. fileName?: Option String := .none file?: Option String := .none - -- If set to true, read the header (otherwise discards the header) + -- Whether to read the header readHeader : Bool := false - -- If set to true, Pantograph's environment will be altered to whatever is - -- after the compilation units. + -- Alter the REPL environment after the compilation units. inheritEnv : Bool := false -- collect tactic invocations invocations: Bool := false diff --git a/Test/Common.lean b/Test/Common.lean index 5274bad..c32d62d 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -108,7 +108,7 @@ def strToTermSyntax (s: String): CoreM Syntax := do (input := s) (fileName := ← getFileName) | panic! s!"Failed to parse {s}" return stx -def parseSentence (s: String): Elab.TermElabM Expr := do +def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do let stx ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) @@ -116,7 +116,7 @@ def parseSentence (s: String): Elab.TermElabM Expr := do (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" - Elab.Term.elabTerm (stx := stx) .none + Elab.Term.elabTerm (stx := stx) expectedType? def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } diff --git a/Test/Delate.lean b/Test/Delate.lean index 517a394..7c5eec3 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -3,10 +3,9 @@ import Pantograph.Delate import Test.Common import Lean -open Lean -namespace Pantograph.Test.Delate +open Lean Pantograph -open Pantograph +namespace Pantograph.Test.Delate deriving instance Repr, DecidableEq for Protocol.BoundExpression @@ -113,6 +112,13 @@ def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do checkEq "numParams" numParams 2 checkEq "numFields" numFields 2 +def test_matcher : TestT Elab.TermElabM Unit := do + let t ← parseSentence "Nat → Nat" + let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t) + let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app" + let e' ← instantiateAll e + checkTrue "ok" <| ← Meta.isTypeCorrect e' + def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("serializeName", do pure test_serializeName), @@ -123,6 +129,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Instance", test_instance env), ("Projection Prod", test_projection_prod env), ("Projection Exists", test_projection_exists env), + ("Matcher", runTestTermElabM env test_matcher), ] end Pantograph.Test.Delate diff --git a/doc/repl.md b/doc/repl.md index a86c01b..93eb6ab 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -46,14 +46,15 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va Save/Load a goal state to/from a file. The environment is not carried with the state. The user is responsible to ensure the sender/receiver instances share the same environment. -* `frontend.process { ["fileName": ,] ["file": ], invocations: +* `frontend.process { ["fileName": ,] ["file": ], readHeader: , inheritEnv: , invocations: , sorrys: , typeErrorsAsGoals: , newConstants: }`: Executes the Lean frontend on a file, collecting the tactic invocations (`"invocations": true`), the sorrys and type errors into goal states (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of `sorrys`, this command additionally outputs the position of each captured - `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the - draft tactic if possible. + `sorry`. Conditionally inherit the environment from executing the file. + Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft + tactic if possible. ## Errors