Merge pull request 'feat(delate): Unfold matchers' (#176) from delate/instantiate into dev
Reviewed-on: #176
This commit is contained in:
commit
bc37482212
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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] }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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": <fileName>,] ["file": <str>], invocations:
|
||||
* `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
|
||||
<bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
|
||||
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
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue