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

feat: add lazy unfolding to field name resolution

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-13 09:52:44 -08:00
parent 1b701dae2f
commit afc50a801d
3 changed files with 24 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Init/Lean/Elab/Term.lean
View file

@ -169,7 +169,7 @@ def inferType (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta
def whnf (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnf e
def whnfForall (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnfForall e
def whnfCore (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnfCore e
def unfoldDefinition (ref : Syntax) (e : Expr) : TermElabM (Option Expr) := liftMetaM ref $ Meta.unfoldDefinition e
def unfoldDefinition? (ref : Syntax) (e : Expr) : TermElabM (Option Expr) := liftMetaM ref $ Meta.unfoldDefinition? e
def instantiateMVars (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.instantiateMVars e
def isClass (ref : Syntax) (t : Expr) : TermElabM (Option Name) := liftMetaM ref $ Meta.isClass t
def mkFreshLevelMVar (ref : Syntax) : TermElabM Level := liftMetaM ref $ Meta.mkFreshLevelMVar
@ -621,7 +621,7 @@ inductive FieldResolution
private def throwFieldError {α} (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwError ref $ msg ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr eType
private def resolveField (ref : Syntax) (e : Expr) (eType : Expr) (field : Field) : TermElabM FieldResolution :=
private def resolveFieldAux (ref : Syntax) (e : Expr) (eType : Expr) (field : Field) : TermElabM FieldResolution :=
match eType.getAppFn, field with
| Expr.const structName _ _, Field.num idx => do
when (idx == 0) $
@ -669,10 +669,26 @@ match eType.getAppFn, field with
searchLCtx ()
| _, _ => throwFieldError ref e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
private partial def resolveFieldLoop (ref : Syntax) (e : Expr) (field : Field) : Expr → Array Exception → TermElabM FieldResolution
| eType, previousExceptions => do
eType ← whnfCore ref eType;
catch (resolveFieldAux ref e eType field)
(fun ex => do
eType? ← unfoldDefinition? ref eType;
match eType? with
| some eType => resolveFieldLoop eType (previousExceptions.push ex)
| none => do
previousExceptions.forM $ fun ex => logMessage ex;
throw ex)
private def resolveField (ref : Syntax) (e : Expr) (field : Field) : TermElabM FieldResolution := do
eType ← inferType ref e;
resolveFieldLoop ref e field eType #[]
private def elabAppFieldsAux (ref : Syntax) (namedArgs : Array NamedArg) (args : Array Syntax) (expectedType? : Option Expr) (explicit : Bool)
: Expr → List Field → TermElabM Expr
| f, [] => elabAppArgs ref f namedArgs args expectedType? explicit
| f, proj::fields => do
| f, [] => elabAppArgs ref f namedArgs args expectedType? explicit
| f, field::fields => do
fType ← inferType ref f;
-- TODO
elabAppArgs ref f namedArgs args expectedType? explicit

4
src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -607,7 +607,7 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
trace! `Meta.isDefEq.foApprox (mvar ++ " " ++ args ++ " := " ++ v);
condM (try $ processAssignmentFOApproxAux mvar args v)
(pure true)
(do v? ← unfoldDefinition v;
(do v? ← unfoldDefinition? v;
match v? with
| none => pure false
| some v => processAssignmentFOApprox v)
@ -733,7 +733,7 @@ traceCtx `Meta.isDefEq.delta $
/-- Auxiliary method for isDefEqDelta -/
private abbrev unfold {α} (e : Expr) (failK : MetaM α) (successK : Expr → MetaM α) : MetaM α := do
e? ← unfoldDefinition e;
e? ← unfoldDefinition? e;
match e? with
| some e => successK e
| none => failK

4
src/Init/Lean/Meta/WHNF.lean
View file

@ -15,7 +15,7 @@ namespace Meta
def isAuxDef? (constName : Name) : MetaM Bool := do
env ← getEnv; pure (isAuxRecursor env constName || isNoConfusion env constName)
def unfoldDefinition (e : Expr) : MetaM (Option Expr) :=
def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
Lean.WHNF.unfoldDefinitionAux getConstNoEx isAuxDef? whnf inferType isExprDefEq synthPending getLocalDecl getExprMVarAssignment e
def whnfCore (e : Expr) : MetaM Expr :=
@ -24,7 +24,7 @@ Lean.WHNF.whnfCore getConstNoEx isAuxDef? whnf inferType isExprDefEqAux getLocal
partial def whnfImpl : Expr → MetaM Expr
| e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment e $ fun e => do
e ← whnfCore e;
e? ← unfoldDefinition e;
e? ← unfoldDefinition? e;
match e? with
| some e => whnfImpl e
| none => pure e