diff options
author | Son Ho | 2023-07-18 12:22:59 +0200 |
---|---|---|
committer | Son Ho | 2023-07-18 12:22:59 +0200 |
commit | e07177ee2de3fd1346ab6b1fc09aefbcb0e24459 (patch) | |
tree | 439fb9c21b48d26f6fdc5b6e70eda1ddeac2efd0 /backends/lean/Base/Progress | |
parent | aaa2fdfd104f7010ebaf2977a22280716ac15d13 (diff) |
Improve progress
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Progress/Base.lean | 11 | ||||
-rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 11 |
2 files changed, 17 insertions, 5 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 00b0a478..7eace667 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -58,10 +58,10 @@ section Methods def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a) (sanityChecks : Bool := false) : m a := do - trace[Progress] "Theorem: {th}" + trace[Progress] "Proposition: {th}" -- Dive into the quantified variables and the assumptions forallTelescope th fun fvars th => do - trace[Progress] "All arguments: {fvars}" + trace[Progress] "Universally quantified arguments and assumptions: {fvars}" /- -- Filter the argumens which are not propositions let rec getFirstPropIdx (i : Nat) : MetaM Nat := do if i ≥ fargs.size then pure i @@ -83,12 +83,16 @@ section Methods -- Dive into the existentials existsTelescope th fun evars th => do trace[Progress] "Existentials: {evars}" + trace[Progress] "Proposition after stripping the quantifiers: {th}" -- Take the first conjunct let (th, post) ← optSplitConj th + trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}" -- Destruct the equality let (th, ret) ← destEq th + trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}" -- Destruct the application to get the name - th.withApp fun f args => do + th.consumeMData.withApp fun f args => do + trace[Progress] "After stripping the arguments:\n- f: {f}\n- args: {args}" if ¬ f.isConst then throwError "Not a constant: {f}" -- Compute the set of universally quantified variables which appear in the function arguments let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty @@ -114,6 +118,7 @@ section Methods post := post } k thDesc + end Methods diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 001967e5..ace92f4f 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -55,14 +55,20 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) let thDecl := env.constants.find! thName pure thDecl.type | .Local asmDecl => pure asmDecl.type + trace[Progress] "theorem/assumption type: {thTy}" -- TODO: the tactic fails if we uncomment withNewMCtxDepth -- withNewMCtxDepth do let (mvars, binders, thExBody) ← forallMetaTelescope thTy + trace[Progress] "After stripping foralls: {thExBody}" -- Introduce the existentially quantified variables and the post-condition -- in the context let thBody ← existsTelescope thExBody fun _evars thBody => do + trace[Progress] "After stripping existentials: {thBody}" + let (thBody, _) ← optSplitConj thBody + trace[Progress] "After splitting the conjunction: {thBody}" let (thBody, _) ← destEq thBody + trace[Progress] "After splitting equality: {thBody}" -- There shouldn't be any existential variables in thBody pure thBody -- Match the body with the target @@ -152,6 +158,7 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac -- Retrieve the goal let mgoal ← Tactic.getMainGoal let goalTy ← mgoal.getType + trace[Progress] "goal: {goalTy}" -- Dive into the goal to lookup the theorem let (fName, fLevels, args) ← do withPSpec goalTy fun desc => @@ -188,7 +195,7 @@ syntax progressArgs := ("as" " ⟨ " (ident)+ " ⟩")? def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := args.raw -- Process the arguments to retrieve the identifiers to use - trace[Progress] "Progressing arguments: {args}" + trace[Progress] "Progress arguments: {args}" let args := args.getArgs let ids := if args.size > 0 then @@ -196,7 +203,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := (args.get! 2).getArgs args.map Syntax.getId else #[] - trace[Progress] "Ids: {ids}" + trace[Progress] "User-provided ids: {ids}" progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac]) elab "progress" args:progressArgs : tactic => |