max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add flag to control projection reduction at whnfCore

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-30 16:44:42 -07:00
parent 2c152dae7d
commit f3bb0be045
1 changed files with 50 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

88
src/Lean/Meta/WHNF.lean
View file

@ -425,8 +425,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
return ReduceMatcherResult.stuck auxApp
| _ => pure ReduceMatcherResult.notMatcher
def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
let e ← whnf e
private def projectCore? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
let e := toCtorIfLit e
matchConstCtor e.getAppFn (fun _ => pure none) fun ctorVal _ =>
let numArgs := e.getAppNumArgs
@ -436,6 +435,9 @@ def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
else
return none
def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
projectCore? (← whnf e) i
/-- Reduce kernel projection `Expr.proj ..` expression. -/
def reduceProj? (e : Expr) : MetaM (Option Expr) := do
match e with
@ -469,42 +471,52 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
/--
Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
expand let-expressions, expand assigned meta-variables. -/
partial def whnfCore (e : Expr) : MetaM Expr :=
whnfEasyCases e fun e => do
trace[Meta.whnf] e
match e with
| Expr.const .. => pure e
| Expr.letE _ _ v b _ => whnfCore $ b.instantiate1 v
| Expr.app f .. =>
let f := f.getAppFn
let f' ← whnfCore f
if f'.isLambda then
let revArgs := e.getAppRevArgs
whnfCore <| f'.betaRev revArgs
else if let some eNew ← whnfDelayedAssigned? f' e then
whnfCore eNew
else
let e := if f == f' then e else e.updateFn f'
match (← reduceMatcher? e) with
| ReduceMatcherResult.reduced eNew => whnfCore eNew
| ReduceMatcherResult.partialApp => pure e
| ReduceMatcherResult.stuck _ => pure e
| ReduceMatcherResult.notMatcher =>
matchConstAux f' (fun _ => return e) fun cinfo lvls =>
match cinfo with
| ConstantInfo.recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) whnfCore
| ConstantInfo.quotInfo rec => reduceQuotRec rec lvls e.getAppArgs (fun _ => return e) whnfCore
| c@(ConstantInfo.defnInfo _) => do
if (← isAuxDef c.name) then
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) whnfCore
else
return e
| _ => return e
| Expr.proj .. => match (← reduceProj? e) with
| some e => whnfCore e
| none => return e
| _ => unreachable!
expand let-expressions, expand assigned meta-variables.
The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
We only set this flag to `false` when implementing `isDefEq`.
-/
partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) : MetaM Expr :=
go e
where
go (e : Expr) : MetaM Expr :=
whnfEasyCases e fun e => do
trace[Meta.whnf] e
match e with
| Expr.const .. => pure e
| Expr.letE _ _ v b _ => go <| b.instantiate1 v
| Expr.app f .. =>
let f := f.getAppFn
let f' ← go f
if f'.isLambda then
let revArgs := e.getAppRevArgs
go <| f'.betaRev revArgs
else if let some eNew ← whnfDelayedAssigned? f' e then
go eNew
else
let e := if f == f' then e else e.updateFn f'
match (← reduceMatcher? e) with
| ReduceMatcherResult.reduced eNew => go eNew
| ReduceMatcherResult.partialApp => pure e
| ReduceMatcherResult.stuck _ => pure e
| ReduceMatcherResult.notMatcher =>
matchConstAux f' (fun _ => return e) fun cinfo lvls =>
match cinfo with
| ConstantInfo.recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
| ConstantInfo.quotInfo rec => reduceQuotRec rec lvls e.getAppArgs (fun _ => return e) go
| c@(ConstantInfo.defnInfo _) => do
if (← isAuxDef c.name) then
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
else
return e
| _ => return e
| Expr.proj _ i c _ =>
let c ← if deltaAtProj then whnf c else whnfCore c
match (← projectCore? c i) with
| some e => go e
| none => return e
| _ => unreachable!
/--
Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**).