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

refactor: add MonadMetaM class

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-24 11:49:49 -07:00
parent 57a6998426
commit ac565de96c
34 changed files with 442 additions and 449 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Delaborator.lean
View file

@ -227,7 +227,7 @@ delabFor k <|> (liftM $ show MetaM Syntax from throwError $ "don't know how to d
@[builtinDelab fvar]
def delabFVar : Delab := do
Expr.fvar id _ ← getExpr | unreachable!;
l ← liftM $ getLocalDecl id;
l ← getLocalDecl id;
pure $ mkIdent l.userName
@[builtinDelab mvar]

18
src/Lean/Elab/Binders.lean
View file

@ -164,7 +164,7 @@ def elabBinders {α} (binders : Array Syntax) (x : Array Expr → TermElabM α)
if binders.isEmpty then x #[]
else do
lctx ← getLCtx;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
(fvars, lctx, newLocalInsts) ← elabBindersAux binders 0 #[] lctx localInsts;
resettingSynthInstanceCacheWhen (newLocalInsts.size > localInsts.size) $ withLCtx lctx newLocalInsts $
x fvars
@ -177,7 +177,7 @@ fun stx _ => match_syntax stx with
| `(forall $binders*, $term) =>
elabBinders binders $ fun xs => do
e ← elabType term;
mkForall xs e
mkForallFVars xs e
| _ => throwUnsupportedSyntax
@[builtinTermElab arrow] def elabArrow : TermElab :=
@ -192,7 +192,7 @@ fun stx _ =>
let term := stx.getArg 2;
elabBinders #[binder] $ fun xs => do
e ← elabType term;
mkForall xs e
mkForallFVars xs e
/-- Main loop `getFunBinderIds?` -/
private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → TermElabM (Option (Array Syntax))
@ -352,7 +352,7 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
if binders.isEmpty then x #[] expectedType?
else do
lctx ← getLCtx;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
s ← FunBinders.elabFunBindersAux binders 0 { lctx := lctx, localInsts := localInsts, expectedType? := expectedType? };
resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $
x s.fvars s.expectedType?
@ -369,7 +369,7 @@ if expandedPattern then do
else
elabFunBinders binders expectedType? $ fun xs expectedType? => do
e ← elabTerm body expectedType?;
mkLambda xs e
mkLambdaFVars xs e
/-
Recall that
@ -390,8 +390,8 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
(type, val) ← elabBinders binders $ fun xs => do {
type ← elabType typeStx;
val ← elabTermEnsuringType valStx type;
type ← mkForall xs type;
val ← mkLambda xs val;
type ← mkForallFVars xs type;
val ← mkLambdaFVars xs val;
pure (type, val)
};
trace `Elab.let.decl $ fun _ => n ++ " : " ++ type ++ " := " ++ val;
@ -399,12 +399,12 @@ if useLetExpr then
withLetDecl n type val $ fun x => do
body ← elabTerm body expectedType?;
body ← instantiateMVars body;
mkLet x body
mkLetFVars #[x] body
else do
f ← withLocalDecl n BinderInfo.default type $ fun x => do {
body ← elabTerm body expectedType?;
body ← instantiateMVars body;
mkLambda #[x] body
mkLambdaFVars #[x] body
};
pure $ mkApp f val

10
src/Lean/Elab/CollectFVars.lean
View file

@ -11,24 +11,24 @@ namespace Elab
namespace Term
def collectUsedFVars (used : CollectFVars.State) (e : Expr) : TermElabM CollectFVars.State := do
e ← Term.instantiateMVars e;
e ← instantiateMVars e;
pure $ collectFVars used e
def collectUsedFVarsAtFVars (used : CollectFVars.State) (fvars : Array Expr) : TermElabM CollectFVars.State :=
fvars.foldlM
(fun used fvar => do
fvarType ← Term.inferType fvar;
fvarType ← inferType fvar;
collectUsedFVars used fvarType)
used
def removeUnused (vars : Array Expr) (used : CollectFVars.State) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
localInsts ← Term.getLocalInsts;
lctx ← Term.getLCtx;
localInsts ← getLocalInstances;
lctx ← getLCtx;
(lctx, localInsts, newVars, _) ← vars.foldrM
(fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) =>
let (lctx, localInsts, newVars, used) := result;
if used.fvarSet.contains var.fvarId! then do
varType ← Term.inferType var;
varType ← inferType var;
used ← Term.collectUsedFVars used varType;
pure (lctx, localInsts, newVars.push var, used)
else

14
src/Lean/Elab/Command.lean
View file

@ -510,7 +510,7 @@ fun stx => do
withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
e ← Term.elabTerm term none;
Term.synthesizeSyntheticMVars false;
type ← Term.inferType e;
type ← inferType e;
logInfo (e ++ " : " ++ type);
pure ()
@ -541,9 +541,6 @@ when succeeded $
@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab :=
fun stx => failIfSucceeds $ elabCheck stx
def addDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl decl
def compileDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl decl
def addInstance (declName : Name) : CommandElabM Unit := do
env ← getEnv;
env ← liftIO $ Meta.addGlobalInstance env declName;
@ -557,11 +554,10 @@ fun stx => withoutModifyingEnv do
ctx ← read;
env ← getEnv;
let addAndCompile (value : Expr) : TermElabM Unit := do {
type ← Term.inferType value;
type ← inferType value;
let decl := Declaration.defnDecl { name := n, lparams := [], type := type,
value := value, hints := ReducibilityHints.opaque, isUnsafe := true };
Term.addDecl decl;
Term.compileDecl decl
addAndCompile decl
};
let elabMetaEval : CommandElabM Unit := do {
act : IO Environment ← runTermElabM (some n) fun _ => do {
@ -570,7 +566,7 @@ fun stx => withoutModifyingEnv do
e ← Term.withLocalDecl `env BinderInfo.default (mkConst `Lean.Environment) fun env =>
Term.withLocalDecl `opts BinderInfo.default (mkConst `Lean.Options) fun opts => do {
e ← Term.mkAppM `Lean.MetaHasEval.eval #[env, opts, e, toExpr false];
Term.mkLambda #[env, opts] e
mkLambdaFVars #[env, opts] e
};
addAndCompile e;
env ← getEnv;
@ -618,7 +614,7 @@ fun stx => do
withoutModifyingEnv $ runTermElabM `_synth_cmd $ fun _ => do
inst ← Term.elabTerm term none;
Term.synthesizeSyntheticMVars false;
inst ← Term.instantiateMVars inst;
inst ← instantiateMVars inst;
val ← Term.liftMetaM $ Meta.synthInstance inst;
logInfo val;
pure ()

6
src/Lean/Elab/Declaration.lean
View file

@ -87,9 +87,9 @@ withDeclId declId $ fun name => do
decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
type ← Term.elabType typeStx;
Term.synthesizeSyntheticMVars false;
type ← Term.instantiateMVars type;
type ← Term.mkForall xs type;
(type, _) ← Term.mkForallUsedOnly vars type;
type ← instantiateMVars type;
type ← mkForallFVars xs type;
(type, _) ← mkForallUsedOnly vars type;
(type, _) ← Term.levelMVarToParam type;
let usedParams := (collectLevelParams {} type).params;
match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with

18
src/Lean/Elab/Definition.lean
View file

@ -65,18 +65,18 @@ withRef view.ref do
Term.synthesizeSyntheticMVars;
val ← withRef view.val $ Term.ensureHasType type val;
Term.synthesizeSyntheticMVars false;
type ← Term.instantiateMVars type;
val ← Term.instantiateMVars val;
type ← instantiateMVars type;
val ← instantiateMVars val;
if view.kind.isExample then pure none
else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars => do
type ← Term.mkForall xs type;
type ← Term.mkForall vars type;
val ← Term.mkLambda xs val;
val ← Term.mkLambda vars val;
type ← mkForallFVars xs type;
type ← mkForallFVars vars type;
val ← mkLambdaFVars xs val;
val ← mkLambdaFVars vars val;
(type, nextParamIdx) ← Term.levelMVarToParam type;
(val, _) ← Term.levelMVarToParam val nextParamIdx;
type ← Term.instantiateMVars type;
val ← Term.instantiateMVars val;
type ← instantiateMVars type;
val ← instantiateMVars val;
let shareCommonTypeVal : Std.ShareCommonM (Expr × Expr) := do {
type ← Std.withShareCommon type;
val ← Std.withShareCommon val;
@ -131,7 +131,7 @@ withDeclId view.declId $ fun name => do
| some typeStx => do
type ← Term.elabType typeStx;
Term.synthesizeSyntheticMVars false;
type ← Term.instantiateMVars type;
type ← instantiateMVars type;
withUsedWhen' vars xs type view.kind.isTheorem $ fun vars => do
val ← elabDefVal view.val type;
mkDef view declName scopeLevelNames allUserLevelNames vars xs type val

2
src/Lean/Elab/DoNotation.lean
View file

@ -174,7 +174,7 @@ else do
α ← inferType var;
mβ ← inferType body;
β ← extractTypeFormerAppArg mβ;
f ← mkLambda #[var] body;
f ← mkLambdaFVars #[var] body;
-- dbgTrace (">>> f: " ++ toString f);
let body := mkAppN bindAndInst #[α, β, action, f];
pure body)

42
src/Lean/Elab/Inductive.lean
View file

@ -77,16 +77,16 @@ private partial def elabHeaderAux (views : Array InductiveView)
if h : i < views.size then
let view := views.get ⟨i, h⟩;
Term.elabBinders view.binders.getArgs fun params => do
lctx ← Term.getLCtx;
localInsts ← Term.getLocalInsts;
lctx ← getLCtx;
localInsts ← getLocalInstances;
match view.type? with
| none => do
u ← Term.mkFreshLevelMVar;
u ← mkFreshLevelMVar;
let type := mkSort (mkLevelSucc u);
elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
| some typeStx => do
type ← Term.elabTerm typeStx none;
unlessM (Term.isTypeFormerType type) $
unlessM (isTypeFormerType type) $
throwErrorAt typeStx "invalid inductive type, resultant type is not a sort";
elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
else
@ -111,7 +111,7 @@ when (views.size > 1) do
private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
Term.withLocalContext r.lctx r.localInsts do
Term.mkForall r.params r.type
mkForallFVars r.params r.type
private def throwUnexpectedInductiveType {α} : TermElabM α :=
throwError "unexpected inductive resulting type"
@ -121,14 +121,14 @@ private def getResultingType (e : Expr) : TermElabM Expr :=
Term.liftMetaM $ Meta.forallTelescopeReducing e fun _ r => pure r
private def eqvFirstTypeResult (firstType type : Expr) : MetaM Bool :=
Meta.forallTelescopeReducing firstType fun _ firstTypeResult => Meta.isDefEq firstTypeResult type
Meta.forallTelescopeReducing firstType fun _ firstTypeResult => isDefEq firstTypeResult type
-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
private partial def checkParamsAndResultType (numParams : Nat) : Nat → Expr → Expr → TermElabM Unit
| i, type, firstType => do
type ← Term.whnf type;
type ← whnf type;
if i < numParams then do
firstType ← Term.whnf firstType;
firstType ← whnf firstType;
match type, firstType with
| Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ => do
unless (n₁ == n₂) $
@ -190,7 +190,7 @@ private partial def withInductiveLocalDeclsAux {α} (namesAndTypes : Array (Name
| i, indFVars =>
if h : i < namesAndTypes.size then do
let (id, type) := namesAndTypes.get ⟨i, h⟩;
type ← Term.liftMetaM (Meta.instantiateForall type params);
type ← instantiateForall type params;
Term.withLocalDecl id BinderInfo.default type fun indFVar => withInductiveLocalDeclsAux (i+1) (indFVars.push indFVar)
else
x params indFVars
@ -211,8 +211,8 @@ Term.withLocalContext r0.lctx r0.localInsts $ withRef r0.view.ref $
withInductiveLocalDeclsAux namesAndTypes params x 0 #[]
private def isInductiveFamily (indFVar : Expr) : TermElabM Bool := do
indFVarType ← Term.inferType indFVar;
indFVarType ← Term.whnf indFVarType;
indFVarType ← inferType indFVar;
indFVarType ← whnf indFVarType;
pure !indFVarType.isSort
/-
@ -237,18 +237,18 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
resultingType ← getResultingType type;
unless (resultingType.getAppFn == indFVar) $
throwError ("unexpected constructor resulting type" ++ indentExpr resultingType);
unlessM (Term.isType resultingType) $
unlessM (isType resultingType) $
throwError ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
pure type
};
type ← Term.mkForall ctorParams type;
type ← Term.mkForall params type;
type ← mkForallFVars ctorParams type;
type ← mkForallFVars params type;
pure { name := ctorView.declName, type := type }
/- Convert universe metavariables occurring in the `indTypes` into new parameters.
Remark: if the resulting inductive datatype has universe metavariables, we will fix it later using
`inferResultingUniverse`. -/
private def levelMVarToParamAux (indTypes : List InductiveType) : StateT Nat TermElabM (List InductiveType) :=
private def levelMVarToParamAux (indTypes : List InductiveType) : StateRefT Nat TermElabM (List InductiveType) :=
indTypes.mapM fun indType => do
type ← Term.levelMVarToParam' indType.type;
ctors ← indType.ctors.mapM fun ctor => do {
@ -275,7 +275,7 @@ def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
Return false if `u` does not contain universe metavariables.
Throw exception otherwise. -/
def shouldInferResultUniverse (u : Level) : TermElabM Bool := do
u ← Term.instantiateLevelMVars u;
u ← instantiateLevelMVars u;
if u.hasMVar then
match u.getLevelOffset with
| Level.mvar mvarId _ => do
@ -308,7 +308,7 @@ def accLevelAtCtor : Level → Level → Nat → Array Level → Except String (
private partial def collectUniversesFromCtorTypeAux (r : Level) (rOffset : Nat) : Nat → Expr → Array Level → TermElabM (Array Level)
| 0, Expr.forallE n d b c, us => do
u ← Term.getLevel d;
u ← Term.instantiateLevelMVars u;
u ← instantiateLevelMVars u;
match accLevelAtCtor u r rOffset us with
| Except.error msg => throwError msg
| Except.ok us => Term.withLocalDecl n c.binderInfo d $ fun x =>
@ -363,9 +363,9 @@ Term.withLCtx lctx localInsts $ k vars
private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
indTypes.mapM fun indType => do
type ← Term.mkForall vars indType.type;
type ← mkForallFVars vars indType.type;
ctors ← indType.ctors.mapM fun ctor => do {
ctorType ← Term.mkForall vars ctor.type;
ctorType ← mkForallFVars vars ctor.type;
pure { ctor with type := ctorType }
};
pure { indType with type := type, ctors := ctors }
@ -400,7 +400,7 @@ indTypes.mapM fun indType => do
match indFVar2Const.find? e with
| some c => some $ mkAppN c params
| none => none;
Meta.mkForall params type
mkForallFVars params type
};
pure { ctor with type := type }
};
@ -439,7 +439,7 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
(fun i (indTypes : List InductiveType) => do
let indFVar := indFVars.get! i;
let r := rs.get! i;
type ← Term.mkForall params r.type;
type ← mkForallFVars params r.type;
ctors ← elabCtors indFVar params r;
let indType := { name := r.view.declName, type := type, ctors := ctors : InductiveType };
pure (indType :: indTypes))

22
src/Lean/Elab/Match.lean
View file

@ -174,7 +174,7 @@ private def getNumExplicitCtorParams (ctorVal : ConstructorVal) : TermElabM Nat
liftMetaM $ Meta.forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ =>
ps.foldlM
(fun acc p => do
localDecl ← Meta.getLocalDecl p.fvarId!;
localDecl ← getLocalDecl p.fvarId!;
if localDecl.binderInfo.isExplicit then pure $ acc+1 else pure acc)
0
@ -377,7 +377,7 @@ patternVarDecls.foldlM
match pdecl with
| PatternVarDecl.localVar fvarId => do
decl ← getLocalDecl fvarId;
decl ← liftMetaM $ Meta.instantiateLocalDeclMVars decl;
decl ← instantiateLocalDeclMVars decl;
pure $ decls.push decl
| PatternVarDecl.anonymousVar mvarId fvarId => do
e ← instantiateMVars (mkMVar mvarId);
@ -389,7 +389,7 @@ patternVarDecls.foldlM
assignExprMVar newMVarId (mkFVar fvarId);
trace `Elab.match fun _ => "finalizePatternDecls: " ++ mkMVar newMVarId ++ " := " ++ mkFVar fvarId;
decl ← getLocalDecl fvarId;
decl ← liftMetaM $ Meta.instantiateLocalDeclMVars decl;
decl ← instantiateLocalDeclMVars decl;
pure $ decls.push decl
| _ => pure decls)
#[]
@ -427,15 +427,15 @@ private def getFieldsBinderInfoAux (ctorVal : ConstructorVal) : Nat → Expr →
private def mkLocalDeclFor (mvar : Expr) : M Pattern := do
let mvarId := mvar.mvarId!;
s ← get;
val? ← liftM $ liftMetaM $ Meta.getExprMVarAssignment? mvarId;
val? ← getExprMVarAssignment? mvarId;
match val? with
| some val => pure $ Pattern.inaccessible val
| none => do
fvarId ← mkFreshId;
type ← liftM $ inferType mvar;
type ← inferType mvar;
/- HACK: `fvarId` is not in the scope of `mvarId`
If this generates problems in the future, we should update the metavariable declarations. -/
liftM $ assignExprMVar mvarId (mkFVar fvarId);
assignExprMVar mvarId (mkFVar fvarId);
let userName := (`_x).appendIndexAfter (s.localDecls.size+1);
let newDecl := LocalDecl.cdecl (arbitrary _) fvarId userName type BinderInfo.default;
modify $ fun s =>
@ -492,7 +492,7 @@ partial def main : Expr → M Pattern
else if e.isMVar then do
mkLocalDeclFor e
else do
newE ← liftM $ whnf e;
newE ← whnf e;
if newE != e then
main newE
else match e.getAppFn with
@ -520,7 +520,7 @@ end ToDepElimPattern
def withDepElimPatterns {α} (localDecls : Array LocalDecl) (ps : Array Expr) (k : Array LocalDecl → Array Pattern → TermElabM α) : TermElabM α := do
(patterns, s) ← (ps.mapM ToDepElimPattern.main).run { localDecls := localDecls };
localDecls ← s.localDecls.mapM fun d => liftMetaM $ Meta.instantiateLocalDeclMVars d;
localDecls ← s.localDecls.mapM fun d => instantiateLocalDeclMVars d;
/- toDepElimPatterns may have added new localDecls. Thus, we must update the local context before we execute `k` -/
lctx ← getLCtx;
let lctx := localDecls.foldl (fun (lctx : LocalContext) d => lctx.erase d.fvarId) lctx;
@ -543,7 +543,7 @@ withPatternVars patternVars fun patternVarDecls => do
withElaboratedLHS patternVarDecls alt.patterns matchType fun altLHS matchType => do
rhs ← elabTermEnsuringType alt.rhs matchType;
let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr;
rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambda xs rhs;
rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambdaFVars xs rhs;
trace `Elab.match fun _ => "rhs: " ++ rhs;
-- TODO: check whether altLHS still has metavariables
pure (altLHS, rhs)
@ -551,7 +551,7 @@ withPatternVars patternVars fun patternVarDecls => do
def mkMotiveType (matchType : Expr) (expectedType : Expr) : TermElabM Expr := do
liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => do
u ← Meta.getLevel matchType;
Meta.mkForall xs (mkSort u)
mkForallFVars xs (mkSort u)
def mkElim (elimName : Name) (motiveType : Expr) (lhss : List AltLHS) : TermElabM ElimResult :=
liftMetaM $ Meta.Match.mkElim elimName motiveType lhss
@ -573,7 +573,7 @@ alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType;
let rhss := alts.map Prod.snd;
let altLHSS := alts.map Prod.fst;
motiveType ← mkMotiveType matchType expectedType;
motive ← liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => Meta.mkLambda xs matchType;
motive ← liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => mkLambdaFVars xs matchType;
elimName ← mkAuxName `elim;
elimResult ← mkElim elimName motiveType altLHSS.toList;
reportElimResultErrors elimResult;

10
src/Lean/Elab/StructInst.lean
View file

@ -646,9 +646,9 @@ else match e.getAppFn with
/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
partial def reduce (structNames : Array Name) : Expr → MetaM Expr
| e@(Expr.lam _ _ _ _) => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; Meta.mkLambda xs b
| e@(Expr.forallE _ _ _ _) => Meta.forallTelescope e $ fun xs b => do b ← reduce b; Meta.mkForall xs b
| e@(Expr.letE _ _ _ _ _) => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; Meta.mkLambda xs b
| e@(Expr.lam _ _ _ _) => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; mkLambdaFVars xs b
| e@(Expr.forallE _ _ _ _) => Meta.forallTelescope e $ fun xs b => do b ← reduce b; mkForallFVars xs b
| e@(Expr.letE _ _ _ _ _) => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; mkLetFVars xs b
| e@(Expr.proj _ i b _) => do
r? ← Meta.reduceProj? b i;
match r? with
@ -674,7 +674,7 @@ partial def reduce (structNames : Array Name) : Expr → MetaM Expr
else
pure $ e.updateMData! b
| e@(Expr.mvar mvarId _) => do
val? ← Meta.getExprMVarAssignment? mvarId;
val? ← getExprMVarAssignment? mvarId;
match val? with
| some val => if val.isMVar then reduce val else pure val
| none => pure e
@ -728,7 +728,7 @@ partial def step : Struct → M Unit
partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
| d, struct => do
mctx ← liftM $ getMCtx;
mctx ← getMCtx;
match findDefaultMissing? mctx struct with
| none => pure () -- Done
| some field =>

60
src/Lean/Elab/Structure.lean
View file

@ -217,7 +217,7 @@ private partial def processSubfields {α} (structDeclName : Name) (parentFVar :
when (containsFieldName infos subfieldName) $
throwError ("field '" ++ subfieldName ++ "' from '" ++ parentStructName ++ "' has already been declared");
val ← Term.liftMetaM $ Meta.mkProjection parentFVar subfieldName;
type ← Term.inferType val;
type ← inferType val;
Term.withLetDecl subfieldName type val fun subfieldFVar =>
/- The following `declName` is only used for creating the `_default` auxiliary declaration name when
its default value is overwritten in the structure. -/
@ -253,7 +253,7 @@ match view.type? with
| none => pure (none, none)
| some valStx => do
value ← Term.elabTerm valStx none;
value ← Term.mkLambda params value;
value ← mkLambdaFVars params value;
pure (none, value)
| some typeStx => do
type ← Term.elabType typeStx;
@ -261,8 +261,8 @@ match view.type? with
| none => pure (type, none)
| some valStx => do
value ← Term.elabTermEnsuringType valStx type;
type ← Term.mkForall params type;
value ← Term.mkLambda params value;
type ← mkForallFVars params type;
value ← mkLambdaFVars params value;
pure (type, value)
private partial def withFields {α} (views : Array StructFieldView) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
@ -281,7 +281,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
kind := StructFieldKind.newField, inferMod := view.inferMod };
withFields (i+1) infos k
| none, some value => do
type ← Term.inferType value;
type ← inferType value;
Term.withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod };
withFields (i+1) infos k
@ -294,7 +294,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
| some valStx => do
when (!view.binders.getArgs.isEmpty || view.type?.isSome) $
throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
fvarType ← Term.inferType info.fvar;
fvarType ← inferType info.fvar;
value ← Term.elabTermEnsuringType valStx fvarType;
let infos := infos.push { info with value? := value };
withFields (i+1) infos k
@ -303,7 +303,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
k infos
private def getResultUniverse (type : Expr) : TermElabM Level := do
type ← Term.whnf type;
type ← whnf type;
match type with
| Expr.sort u _ => pure u
| _ => throwError "unexpected structure resulting type"
@ -312,12 +312,12 @@ private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldIn
: TermElabM (LocalContext × LocalInstances × Array Expr) := do
used ← params.foldlM
(fun (used : CollectFVars.State) p => do
type ← Term.inferType p;
type ← inferType p;
Term.collectUsedFVars used type)
{};
used ← fieldInfos.foldlM
(fun (used : CollectFVars.State) info => do
fvarType ← Term.inferType info.fvar;
fvarType ← inferType info.fvar;
used ← Term.collectUsedFVars used fvarType;
match info.value? with
| none => pure used
@ -330,16 +330,16 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI
(lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos;
Term.withLCtx lctx localInsts $ k vars
private def levelMVarToParamFVar (fvar : Expr) : StateT Nat TermElabM Unit := do
type ← liftM $ Term.inferType fvar;
private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
type ← inferType fvar;
_ ← Term.levelMVarToParam' type;
pure ()
private def levelMVarToParamFVars (fvars : Array Expr) : StateT Nat TermElabM Unit :=
private def levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
fvars.forM levelMVarToParamFVar
private def levelMVarToParamAux (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
: StateT Nat TermElabM (Array StructFieldInfo) := do
: StateRefT Nat TermElabM (Array StructFieldInfo) := do
levelMVarToParamFVars scopeVars;
levelMVarToParamFVars params;
fieldInfos.mapM fun info => do
@ -356,9 +356,9 @@ private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fie
private partial def collectUniversesFromFields (r : Level) (rOffset : Nat) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Level) := do
fieldInfos.foldlM
(fun (us : Array Level) (info : StructFieldInfo) => do
type ← Term.inferType info.fvar;
type ← inferType info.fvar;
u ← Term.getLevel type;
u ← Term.instantiateLevelMVars u;
u ← instantiateLevelMVars u;
match accLevelAtCtor u r rOffset us with
| Except.error msg => throwError msg
| Except.ok us => pure us)
@ -372,13 +372,13 @@ match r with
| Level.mvar mvarId _ => do
us ← collectUniversesFromFields r rOffset fieldInfos;
let rNew := Level.mkNaryMax us.toList;
Term.assignLevelMVar mvarId rNew;
Term.instantiateMVars type
assignLevelMVar mvarId rNew;
instantiateMVars type
| _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
type ← Term.inferType fvar;
type ← Term.instantiateMVars type;
type ← inferType fvar;
type ← instantiateMVars type;
pure $ collectLevelParams s type
private def collectLevelParamsInFVars (fvars : Array Expr) (s : CollectLevelParams.State) : TermElabM CollectLevelParams.State :=
@ -395,7 +395,7 @@ private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr
| i+1, type => do
let info := fieldInfos.get! i;
decl ← Term.getFVarLocalDecl! info.fvar;
type ← Term.instantiateMVars type;
type ← instantiateMVars type;
let type := type.abstract #[info.fvar];
match info.kind with
| StructFieldKind.fromParent =>
@ -411,8 +411,8 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
withRef view.ref do
let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params;
type ← addCtorFields fieldInfos fieldInfos.size type;
type ← Term.mkForall params type;
type ← Term.instantiateMVars type;
type ← mkForallFVars params type;
type ← instantiateMVars type;
let type := type.inferImplicit params.size !view.ctor.inferMod;
pure { name := view.ctor.declName, type := type }
@ -436,8 +436,8 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
| Except.ok levelParams => do
let params := scopeVars ++ view.params;
ctor ← mkCtor view levelParams params fieldInfos;
type ← Term.mkForall params type;
type ← Term.instantiateMVars type;
type ← mkForallFVars params type;
type ← instantiateMVars type;
let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType };
let decl := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe;
let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
@ -447,12 +447,12 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
pure (info.isSubobject && decl.binderInfo.isInstImplicit)
};
let projInstances := instParents.toList.map fun info => info.declName;
mctx ← Term.getMCtx;
lctx ← Term.getLCtx;
localInsts ← Term.getLocalInsts;
mctx ← getMCtx;
lctx ← getLCtx;
localInsts ← getLocalInstances;
let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome;
defaultAuxDecls ← fieldsWithDefault.mapM fun info => do {
type ← Term.inferType info.fvar;
type ← inferType info.fvar;
pure (info.declName ++ `_default, type, info.value?.get!)
};
/- The `mctx`, `lctx`, `localInsts` and `defaultAuxDecls` are used to create the auxiliary `_default` declarations *after* the structure has been declarated.
@ -490,12 +490,12 @@ when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declN
private def addDefaults (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
(defaultAuxDecls : Array (Name × Expr × Expr)) : CommandElabM Unit :=
liftTermElabM none $ Term.withLocalContext lctx localInsts do
Term.setMCtx mctx;
setMCtx mctx;
defaultAuxDecls.forM fun ⟨declName, type, value⟩ => do
/- The identity function is used as "marker". -/
value ← Term.liftMetaM $ Meta.mkId value;
let zeta := true; -- expand `let-declarations`
_ ← Term.mkAuxDefinition declName type value zeta;
_ ← mkAuxDefinition declName type value zeta;
modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
pure ()

20
src/Lean/Elab/Tactic/Basic.lean
View file

@ -41,15 +41,6 @@ structure BacktrackableState :=
abbrev TacticM := ReaderT Context $ StateRefT State $ TermElabM
abbrev Tactic := Syntax → TacticM Unit
def getMCtx : TacticM MetavarContext := do s ← getThe Meta.State; pure s.mctx
def getLCtx : TacticM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
def getLocalInsts : TacticM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
def getMVarDecl (mvarId : MVarId) : TacticM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
def setMCtx (mctx : MetavarContext) : TacticM Unit := modifyThe Meta.State fun s => { s with mctx := mctx }
@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modifyThe Meta.State $ fun s => { s with mctx := f s.mctx }
def saveBacktrackableState : TacticM BacktrackableState := do
env ← getEnv;
mctx ← getMCtx;
@ -98,15 +89,8 @@ liftM x
@[inline] def liftMetaM {α} (x : MetaM α) : TacticM α :=
liftTermElabM $ Term.liftMetaM x
def instantiateMVars (e : Expr) : TacticM Expr := liftTermElabM $ Term.instantiateMVars e
def isExprMVarAssigned (mvarId : MVarId) : TacticM Bool := liftTermElabM $ Term.isExprMVarAssigned mvarId
def assignExprMVar (mvarId : MVarId) (val : Expr) : TacticM Unit := liftTermElabM $ Term.assignExprMVar mvarId val
def ensureHasType (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType expectedType? e
def reportUnsolvedGoals (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals goals
def inferType (e : Expr) : TacticM Expr := liftTermElabM $ Term.inferType e
def whnf (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnf e
def whnfCore (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnfCore e
def unfoldDefinition? (e : Expr) : TacticM (Option Expr) := liftTermElabM $ Term.unfoldDefinition? e
def resolveGlobalName (n : Name) : TacticM (List (Name × List String)) := liftTermElabM $ Term.resolveGlobalName n
/-- Collect unassigned metavariables -/
@ -233,7 +217,7 @@ if b then resettingSynthInstanceCache x else x
def withMVarContext {α} (mvarId : MVarId) (x : TacticM α) : TacticM α := do
mvarDecl ← getMVarDecl mvarId;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
let needReset := localInsts == mvarDecl.localInstances;
withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
@ -353,7 +337,7 @@ private def getIntrosSize : Expr → Nat
fun stx => match_syntax stx with
| `(tactic| intros) => liftMetaTactic $ fun mvarId => do
type ← Meta.getMVarType mvarId;
type ← Meta.instantiateMVars type;
type ← instantiateMVars type;
let n := getIntrosSize type;
(_, mvarId) ← Meta.introN mvarId n;
pure [mvarId]

2
src/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -18,7 +18,7 @@ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false)
withRef stx $ liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { ctx with errToSorry := false }) $ do
e ← Term.elabTerm stx expectedType?;
Term.synthesizeSyntheticMVars mayPostpone;
Term.instantiateMVars e
instantiateMVars e
@[builtinTactic «exact»] def evalExact : Tactic :=
fun stx => match_syntax stx with

10
src/Lean/Elab/Tactic/Generalize.lean
View file

@ -21,12 +21,12 @@ stx.getIdAt 4
private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
tag ← Meta.getMVarTag mvarId;
eType ← Meta.inferType e;
eType ← inferType e;
u ← Meta.getLevel eType;
mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
let rfl := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
let val := mkApp2 mvar' e rfl;
Meta.assignExprMVar mvarId val;
assignExprMVar mvarId val;
let mvarId' := mvar'.mvarId!;
(_, mvarId') ← Meta.introN mvarId' 2 [] false;
pure [mvarId']
@ -34,11 +34,11 @@ pure [mvarId']
private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
liftMetaTactic $ fun mvarId => do
mvarId ← Meta.generalize mvarId e x;
mvarDecl ← Meta.getMVarDecl mvarId;
mvarDecl ← getMVarDecl mvarId;
match mvarDecl.type with
| Expr.forallE _ _ b _ => do
(_, mvarId) ← Meta.intro1 mvarId false;
eType ← Meta.inferType e;
eType ← inferType e;
u ← Meta.getLevel eType;
let eq := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1);
@ -48,7 +48,7 @@ liftMetaTactic $ fun mvarId => do
-- If generalizing fails, fall back to not replacing anything
private def evalGeneralizeFallback (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
liftMetaTactic $ fun mvarId => do
eType ← Meta.inferType e;
eType ← inferType e;
u ← Meta.getLevel eType;
mvarType ← Meta.getMVarType mvarId;
let eq := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);

4
src/Lean/Elab/Tactic/Induction.lean
View file

@ -104,8 +104,8 @@ structure RecInfo :=
def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
liftMetaMAtMain $ fun mvarId => do
majorType ← Meta.inferType major;
majorType ← Meta.whnf majorType;
majorType ← inferType major;
majorType ← whnf majorType;
match majorType.getAppFn with
| Expr.const n _ _ => do
env ← getEnv;

82
src/Lean/Elab/Term.lean
View file

@ -145,17 +145,17 @@ newTraceState ← getTraceState;
saveTraceAsMessages newTraceState;
setTraceState oldTraceState
@[inline] def liftMetaM {α} (x : MetaM α) : TermElabM α := do
@[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α := do
oldTraceState ← getTraceState;
setTraceState {};
finally (liftMetaMCore x) (liftMetaMFinalizer oldTraceState)
@[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α :=
liftMetaM $ liftM x
Term.liftMetaM $ liftM x
instance : MonadMetaM TermElabM :=
{ liftMetaM := fun α => Term.liftMetaM }
def getMCtx : TermElabM MetavarContext := do s ← getThe Meta.State; pure s.mctx
def getLCtx : TermElabM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
def getLocalInsts : TermElabM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
def getLevelNames : TermElabM (List Name) := do ctx ← read; pure ctx.levelNames
def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
lctx ← getLCtx;
@ -164,8 +164,6 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
| none => unreachable!
def getMessageLog : TermElabM MessageLog := do s ← get; pure s.messages
def setMCtx (mctx : MetavarContext) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := mctx }
private def addContext' (msg : MessageData) : TermElabM MessageData := do
env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
@ -222,7 +220,6 @@ def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace
def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId
def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := s.mctx.assignLevel mvarId val }
def logTrace (cls : Name) (msg : MessageData) : TermElabM Unit := do
@ -254,38 +251,22 @@ def dbgTrace {α} [HasToString α] (a : α) : TermElabM Unit :=
_root_.dbgTrace (toString a) $ fun _ => pure ()
def ppGoal (mvarId : MVarId) : TermElabM Format := liftMetaM $ Meta.ppGoal mvarId
def isType (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isType e
def isTypeFormer (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isTypeFormer e
def isTypeFormerType (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isTypeFormerType e
def isDefEqNoConstantApprox (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.approxDefEq $ Meta.isDefEq t s
def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.fullApproxDefEq $ Meta.isDefEq t s
def isLevelDefEq (u v : Level) : TermElabM Bool := liftMetaM $ Meta.isLevelDefEq u v
def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e
def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e
def whnfForall (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfForall e
def whnfCore (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfCore e
def unfoldDefinition? (e : Expr) : TermElabM (Option Expr) := liftMetaM $ Meta.unfoldDefinition? e
def instantiateMVars (e : Expr) : TermElabM Expr := liftMetaM $ Meta.instantiateMVars e
def instantiateLevelMVars (u : Level) : TermElabM Level := liftMetaM $ Meta.instantiateLevelMVars u
def isDefEqNoConstantApprox (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.approxDefEq $ Lean.isDefEq t s
def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.fullApproxDefEq $ Lean.isDefEq t s
def isClass? (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass? t
def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
def mkFreshExprMVar (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
match type? with
| some type => liftMetaM $ Meta.mkFreshExprMVar type userName? kind
| none => liftMetaM $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
| some type => liftMetaM $ Lean.mkFreshExprMVar type userName? kind
| none => liftMetaM $ do u ← mkFreshLevelMVar; type ← Lean.mkFreshExprMVar (mkSort u); Lean.mkFreshExprMVar type userName? kind
def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous)
: TermElabM Expr :=
match type? with
| some type => liftMetaM $ Meta.mkFreshExprMVarWithId mvarId type userName? kind
| none => liftMetaM $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVarWithId mvarId type userName? kind
| some type => liftMetaM $ Lean.mkFreshExprMVarWithId mvarId type userName? kind
| none => liftMetaM $ do u ← Lean.mkFreshLevelMVar; type ← Lean.mkFreshExprMVar (mkSort u); Lean.mkFreshExprMVarWithId mvarId type userName? kind
def mkFreshTypeMVar (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
liftMetaM $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
liftMetaM $ do u ← Lean.mkFreshLevelMVar; Lean.mkFreshExprMVar (mkSort u) userName? kind
def getLevel (type : Expr) : TermElabM Level := liftMetaM $ Meta.getLevel type
def getLocalDecl (fvarId : FVarId) : TermElabM LocalDecl := liftMetaM $ Meta.getLocalDecl fvarId
def mkForall (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkForall xs e
def mkForallUsedOnly (xs : Array Expr) (e : Expr) : TermElabM (Expr × Nat) := liftMetaM $ Meta.mkForallUsedOnly xs e
def mkLambda (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkLambda xs e
def mkLet (x : Expr) (e : Expr) : TermElabM Expr := mkLambda #[x] e
def trySynthInstance (type : Expr) : TermElabM (LOption Expr) := liftMetaM $ Meta.trySynthInstance type
def mkAppM (constName : Name) (args : Array Expr) : TermElabM Expr := liftMetaM $ Meta.mkAppM constName args
def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : TermElabM Expr := liftMetaM $ Meta.mkExpectedTypeHint e expectedType
@ -368,7 +349,7 @@ setMCtx r.mctx;
pure (r.expr, r.nextParamIdx)
/-- Variant of `levelMVarToParam` where `nextParamIdx` is stored in a state monad. -/
def levelMVarToParam' (e : Expr) : StateT Nat TermElabM Expr := do
def levelMVarToParam' (e : Expr) : StateRefT Nat TermElabM Expr := do
nextParamIdx ← get;
(e, nextParamIdx) ← liftM $ levelMVarToParam e nextParamIdx;
set nextParamIdx;
@ -440,7 +421,7 @@ else
def withLocalDecl {α} (n : Name) (binderInfo : BinderInfo) (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
fvarId ← mkFreshFVarId;
lctx ← getLCtx;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
let lctx := lctx.mkLocalDecl fvarId n type binderInfo;
let fvar := mkFVar fvarId;
c? ← isClass? type;
@ -453,7 +434,7 @@ match c? with
def withLetDecl {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → TermElabM α) : TermElabM α := do
fvarId ← mkFreshFVarId;
lctx ← getLCtx;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
let lctx := lctx.mkLetDecl fvarId n type val;
let fvar := mkFVar fvarId;
c? ← isClass? type;
@ -865,7 +846,7 @@ else match expectedType? with
def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
body ← elabUsingElabFns stx expectedType catchExPostpone;
-- body ← ensureHasType stx expectedType body;
r ← mkLambda fvars body;
r ← mkLambdaFVars fvars body;
trace `Elab.implicitForall $ fun _ => r;
pure r
@ -947,7 +928,7 @@ finally x (restoreSynthInstanceCache savedSythInstance)
if b then resettingSynthInstanceCache x else x
def withLocalContext {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α := do
localInstsCurr ← getLocalInsts;
localInstsCurr ← getLocalInstances;
adaptTheReader Meta.Context (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) $
if localInsts == localInstsCurr then
x
@ -960,7 +941,7 @@ adaptTheReader Meta.Context (fun ctx => { ctx with lctx := lctx, localInstances
different from the current ones. -/
def withMVarContext {α} (mvarId : MVarId) (x : TermElabM α) : TermElabM α := do
mvarDecl ← getMVarDecl mvarId;
localInsts ← getLocalInsts;
localInsts ← getLocalInstances;
let needReset := localInsts == mvarDecl.localInstances;
withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
@ -1012,31 +993,6 @@ u ← mkFreshLevelMVar;
type ← elabTerm stx (mkSort u);
withRef stx $ ensureType type
def addDecl (decl : Declaration) : TermElabM Unit := do
env ← getEnv;
match env.addDecl decl with
| Except.ok env => setEnv env
| Except.error kex => do opts ← getOptions; throwError (kex.toMessageData opts)
def compileDecl (decl : Declaration) : TermElabM Unit := do
env ← getEnv;
opts ← getOptions;
match env.compileDecl opts decl with
| Except.ok env => setEnv env
| Except.error kex => throwError (kex.toMessageData opts)
def mkAuxDefinition (declName : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : TermElabM Expr := do
env ← getEnv;
opts ← getOptions;
mctx ← getMCtx;
lctx ← getLCtx;
match Lean.mkAuxDefinition env opts mctx lctx declName type value zeta with
| Except.error ex => throwError (ex.toMessageData opts)
| Except.ok (r, env, mctx) => do
setEnv env;
setMCtx mctx;
pure r
private partial def mkAuxNameAux (env : Environment) (base : Name) : Nat → Name
| i =>
let candidate := base.appendIndexAfter i;

313
src/Lean/Meta/Basic.lean
View file

@ -144,20 +144,41 @@ instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
protected def throwIsDefEqStuck {α} : MetaM α :=
throw $ Exception.internal isDefEqStuckExceptionId
@[inline] def getLCtx : MetaM LocalContext := do
ctx ← read; pure ctx.lctx
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta;
registerTraceClass `Meta.debug
@[inline] def getLocalInstances : MetaM LocalInstances := do
ctx ← read; pure ctx.localInstances
end Meta
@[inline] def getConfig : MetaM Config := do
ctx ← read; pure ctx.config
export Meta (MetaM)
@[inline] def getMCtx : MetaM MetavarContext := do
s ← get; pure s.mctx
class MonadMetaM (m : Type → Type) :=
(liftMetaM {α} : MetaM α → m α)
def setMCtx (mctx : MetavarContext) : MetaM Unit :=
modify $ fun s => { s with mctx := mctx }
export MonadMetaM (liftMetaM)
instance monadMetaSelf : MonadMetaM MetaM :=
{ liftMetaM := fun α x => x }
-- TODO: uncomment after we switch to new frontend
-- instance monadTrans (m n) [MonadMetaM m] [HasMonadLift m n] : MonadMetaM n :=
-- { liftMetaM := fun α x => liftM (liftMetaM x : m _) }
instance monadMetaReader (m ρ) [MonadMetaM m] : MonadMetaM (ReaderT ρ m) :=
{ liftMetaM := fun α x _ => liftMetaM x }
instance monadMetaStateRef (m ω σ) [MonadMetaM m] : MonadMetaM (StateRefT' ω σ m) :=
{ liftMetaM := fun α x _ => liftMetaM x }
instance monadMetaOption(m) [MonadMetaM m] [Monad m] : MonadMetaM (OptionT m) :=
{ liftMetaM := fun α x => liftM (liftMetaM x : m _) }
section Methods
variables {m : Type → Type} [MonadMetaM m]
def getLCtx : m LocalContext := liftMetaM do ctx ← read; pure ctx.lctx
def getLocalInstances : m LocalInstances := liftMetaM do ctx ← read; pure ctx.localInstances
def getConfig : m Meta.Config := liftMetaM do ctx ← read; pure ctx.config
def getMCtx : m MetavarContext := liftMetaM do s ← get; pure s.mctx
def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
@[inline] def modifyMCtx {m} [MonadMetaM m] (f : MetavarContext → MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := f s.mctx }
def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
IO.mkRef $ fun _ => throwError "whnf implementation was not set"
@ -179,105 +200,86 @@ IO.mkRef $ fun _ => pure false
@[init mkSynthPendingRef] def synthPendingRef : IO.Ref (MVarId → MetaM Bool) := arbitrary _
def whnf (e : Expr) : MetaM Expr :=
withIncRecDepth do
def whnf (e : Expr) : m Expr :=
liftMetaM $ withIncRecDepth do
fn ← liftIO whnfRef.get;
fn e
def whnfForall (e : Expr) : MetaM Expr := do
def whnfForall [Monad m] (e : Expr) : m Expr := do
e' ← whnf e;
if e'.isForall then pure e' else pure e
def inferType (e : Expr) : MetaM Expr :=
withIncRecDepth do
def inferType (e : Expr) : m Expr :=
liftMetaM $ withIncRecDepth do
fn ← liftIO inferTypeRef.get;
fn e
def isExprDefEqAux (t s : Expr) : MetaM Bool :=
protected def Meta.isExprDefEqAux (t s : Expr) : MetaM Bool :=
withIncRecDepth do
fn ← liftIO isExprDefEqAuxRef.get;
fn t s
def synthPending (mvarId : MVarId) : MetaM Bool :=
protected def Meta.synthPending (mvarId : MVarId) : MetaM Bool :=
withIncRecDepth do
fn ← liftIO synthPendingRef.get;
fn mvarId
private def mkFreshExprMVarAtCore
(mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : MetaM Expr := do
modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId userName lctx localInsts type kind;
pure $ mkMVar mvarId
def mkFreshExprMVarAt
(lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
: MetaM Expr := do
: m Expr := liftMetaM do
mvarId ← mkFreshId;
mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : m Expr := liftMetaM do
lctx ← getLCtx;
localInsts ← getLocalInstances;
mkFreshExprMVarAt lctx localInsts type userName kind
/- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
the metavar using this method. -/
def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
: m Expr := liftMetaM do
lctx ← getLCtx;
localInsts ← getLocalInstances;
mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
def mkFreshLevelMVar : MetaM Level := do
def mkFreshLevelMVar : m Level := liftMetaM do
mvarId ← mkFreshId;
modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId;
pure $ mkLevelMVar mvarId
@[inline] def shouldReduceAll : MetaM Bool := do
ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
@[inline] def shouldReduceReducibleOnly : MetaM Bool := do
ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
@[inline] def getTransparency : MetaM TransparencyMode := do
def shouldReduceAll : MetaM Bool := liftMetaM do
ctx ← read; pure $ ctx.config.transparency == Meta.TransparencyMode.all
def shouldReduceReducibleOnly : m Bool := liftMetaM do
ctx ← read; pure $ ctx.config.transparency == Meta.TransparencyMode.reducible
def getTransparency : m Meta.TransparencyMode := liftMetaM do
ctx ← read; pure $ ctx.config.transparency
-- Remark: wanted to use `private`, but in C++ parser, `private` declarations do not shadow outer public ones.
-- Remark: wanted to use `private`, but in the C++ parser, `private` declarations do not shadow outer public ones.
-- TODO: fix this bug
@[inline] def isReducible (constName : Name) : MetaM Bool := do
protected def Meta.isReducible (constName : Name) : MetaM Bool := do
env ← getEnv; pure $ isReducible env constName
@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
/-- While executing `x`, ensure the given transparency mode is used. -/
@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig (fun config => { config with transparency := mode }) x
@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
withTransparency TransparencyMode.reducible x
@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig
(fun config =>
let oldMode := config.transparency;
let mode := if oldMode.lt mode then mode else oldMode;
{ config with transparency := mode })
x
def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
def getMVarDecl (mvarId : MVarId) : m MetavarDecl := liftMetaM do
mctx ← getMCtx;
match mctx.findDecl? mvarId with
| some d => pure d
| none => throwError ("unknown metavariable '" ++ mkMVar mvarId ++ "'")
def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
modify $ fun s => { s with mctx := s.mctx.setMVarKind mvarId kind }
def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit :=
modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
def isReadOnlyExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
mvarDecl ← getMVarDecl mvarId;
mctx ← getMCtx;
pure $ mvarDecl.depth != mctx.depth
def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
mvarDecl ← getMVarDecl mvarId;
match mvarDecl.kind with
| MetavarKind.syntheticOpaque => pure true
@ -285,73 +287,46 @@ match mvarDecl.kind with
mctx ← getMCtx;
pure $ mvarDecl.depth != mctx.depth
def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do
def isReadOnlyLevelMVar (mvarId : MVarId) : m Bool := liftMetaM do
mctx ← getMCtx;
match mctx.findLevelDepth? mvarId with
| some depth => pure $ depth != mctx.depth
| _ => throwError ("unknown universe metavariable '" ++ mkLevelMVar mvarId ++ "'")
def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
modify $ fun s => { s with mctx := s.mctx.renameMVar mvarId newUserName }
def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit :=
modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName
@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool := do
def isExprMVarAssigned (mvarId : MVarId) : m Bool := liftMetaM do
mctx ← getMCtx;
pure $ mctx.isExprAssigned mvarId
@[inline] def getExprMVarAssignment? (mvarId : MVarId) : MetaM (Option Expr) := do
def getExprMVarAssignment? (mvarId : MVarId) : m (Option Expr) := liftMetaM do
mctx ← getMCtx; pure (mctx.getExprAssignment? mvarId)
def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit := do
modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
def assignExprMVar (mvarId : MVarId) (val : Expr) : m Unit := liftMetaM do
modifyMCtx fun mctx => mctx.assignExpr mvarId val
def isDelayedAssigned (mvarId : MVarId) : MetaM Bool := do
def isDelayedAssigned (mvarId : MVarId) : m Bool := liftMetaM do
mctx ← getMCtx;
pure $ mctx.isDelayedAssigned mvarId
def hasAssignableMVar (e : Expr) : MetaM Bool := do
def hasAssignableMVar (e : Expr) : m Bool := liftMetaM do
mctx ← getMCtx;
pure $ mctx.hasAssignableMVar e
def throwUnknownConstant {α} (constName : Name) : MetaM α :=
throwError ("unknown constant '" ++ constName ++ "'")
def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
env ← getEnv;
match env.find? constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM shouldReduceAll (pure (some info)) (pure none)
| some (info@(ConstantInfo.defnInfo _)) =>
condM shouldReduceReducibleOnly
(condM (isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)
| none => throwUnknownConstant constName
def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
env ← getEnv;
match env.find? constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM shouldReduceAll (pure (some info)) (pure none)
| some (info@(ConstantInfo.defnInfo _)) =>
condM shouldReduceReducibleOnly
(condM (isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)
| none => pure none
def throwUnknownFVar {α} (fvarId : FVarId) : MetaM α :=
throwError ("unknown free variable '" ++ mkFVar fvarId ++ "'")
def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl := do
def getLocalDecl (fvarId : FVarId) : m LocalDecl := liftMetaM do
lctx ← getLCtx;
match lctx.find? fvarId with
| some d => pure d
| none => throwUnknownFVar fvarId
def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
def getFVarLocalDecl (fvar : Expr) : m LocalDecl := liftMetaM do
getLocalDecl fvar.fvarId!
def instantiateMVars (e : Expr) : MetaM Expr :=
def instantiateMVars (e : Expr) : m Expr := liftMetaM do
if e.hasMVar then
modifyGet $ fun s =>
let (e, mctx) := s.mctx.instantiateMVars e;
@ -359,7 +334,7 @@ if e.hasMVar then
else
pure e
def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
def instantiateLocalDeclMVars (localDecl : LocalDecl) : m LocalDecl := liftMetaM do
match localDecl with
| LocalDecl.cdecl idx id n type bi => do
type ← instantiateMVars type;
@ -383,18 +358,70 @@ match x lctx { mctx := mctx, ngen := ngen } with
setNGen newS.ngen;
throwError "failed to create binder due to failure when reverting variable dependencies"
def mkForall (xs : Array Expr) (e : Expr) : MetaM Expr :=
def mkForallFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkForall xs e
def mkLambda (xs : Array Expr) (e : Expr) : MetaM Expr :=
def mkLambdaFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkLambda xs e
def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) :=
def mkLetFVars (xs : Array Expr) (e : Expr) : m Expr :=
mkLambdaFVars xs e
def mkForallUsedOnly (xs : Array Expr) (e : Expr) : m (Expr × Nat) := liftMetaM do
if xs.isEmpty then pure (e, 0) else liftMkBindingM $ MetavarContext.mkForallUsedOnly xs e
def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr :=
def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : m Expr := liftMetaM do
if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e preserveOrder
end Methods
namespace Meta
@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
/-- While executing `x`, ensure the given transparency mode is used. -/
@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig (fun config => { config with transparency := mode }) x
@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
withTransparency TransparencyMode.reducible x
@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig
(fun config =>
let oldMode := config.transparency;
let mode := if oldMode.lt mode then mode else oldMode;
{ config with transparency := mode })
x
def throwUnknownConstant {α} (constName : Name) : MetaM α :=
throwError ("unknown constant '" ++ constName ++ "'")
def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
env ← getEnv;
match env.find? constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM shouldReduceAll (pure (some info)) (pure none)
| some (info@(ConstantInfo.defnInfo _)) =>
condM shouldReduceReducibleOnly
(condM (Meta.isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)
| none => throwUnknownConstant constName
def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
env ← getEnv;
match env.find? constName with
| some (info@(ConstantInfo.thmInfo _)) =>
condM shouldReduceAll (pure (some info)) (pure none)
| some (info@(ConstantInfo.defnInfo _)) =>
condM shouldReduceReducibleOnly
(condM (Meta.isReducible constName) (pure (some info)) (pure none))
(pure (some info))
| some info => pure (some info)
| none => pure none
/-- Save cache, execute `x`, restore cache -/
@[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
s ← get;
@ -700,37 +727,6 @@ private partial def lambdaMetaTelescopeAux (maxMVars? : Option Nat)
def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
lambdaMetaTelescopeAux maxMVars? #[] #[] 0 e
@[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
mctx ← getMCtx;
let (a, mctx) := x.run mctx;
modify fun s => { s with mctx := mctx };
pure a
def instantiateLevelMVars (lvl : Level) : MetaM Level :=
liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
def assignLevelMVar (mvarId : MVarId) (lvl : Level) : MetaM Unit :=
modify $ fun s => { s with mctx := MetavarContext.assignLevel s.mctx mvarId lvl }
def whnfD : Expr → MetaM Expr :=
fun e => withTransparency TransparencyMode.default $ whnf e
/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`. -/
@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true} })
x
/--
Similar to `approxDefEq`, but uses all available approximations.
We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`.
Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
solve `[HasPure (fun _ => IO Bool)]` -/
@[inline] def fullApproxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true } })
x
@[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
c? ← isClass? fvarType;
match c? with
@ -803,28 +799,64 @@ mctx' ← getMCtx;
modify $ fun s => { s with mctx := mctx };
finally x (modify $ fun s => { s with mctx := mctx' })
@[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
mctx ← getMCtx;
let (a, mctx) := x.run mctx;
modify fun s => { s with mctx := mctx };
pure a
/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`. -/
@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true} })
x
/--
Similar to `approxDefEq`, but uses all available approximations.
We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`.
Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
solve `[HasPure (fun _ => IO Bool)]` -/
@[inline] def fullApproxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true } })
x
end Meta
section Methods
variables {m : Type → Type} [MonadMetaM m]
def instantiateLevelMVars (lvl : Level) : m Level :=
liftMetaM $ Meta.liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
def assignLevelMVar (mvarId : MVarId) (lvl : Level) : m Unit :=
modifyMCtx fun mctx => mctx.assignLevel mvarId lvl
def whnfD (e : Expr) : m Expr :=
liftMetaM $ Meta.withTransparency Meta.TransparencyMode.default $ whnf e
/--
Create an auxiliary definition with the given name, type and value.
The parameters `type` and `value` may contain free and meta variables.
A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
and `t_j`s are free and meta variables `type` and `value` depend on. -/
def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM Expr := do
def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : m Expr := liftMetaM do
env ← getEnv;
opts ← getOptions;
mctx ← getMCtx;
lctx ← getLCtx;
match Lean.mkAuxDefinition env opts mctx lctx name type value with
match mkAuxDefinitionCore env opts mctx lctx name type value zeta with
| Except.error ex => throwKernelException ex
| Except.ok (e, env, mctx) => do setEnv env; setMCtx mctx; pure e
/-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
def mkAuxDefinitionFor (name : Name) (value : Expr) : MetaM Expr := do
def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do
type ← inferType value;
let type := type.headBeta;
mkAuxDefinition name type value
def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): MetaM Unit := do
def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): m Unit := liftMetaM do
env ← getEnv;
match Compiler.setInlineAttribute env declName kind with
| Except.ok env => setEnv env
@ -842,15 +874,8 @@ private partial def instantiateForallAux (ps : Array Expr) : Nat → Expr → Me
pure e
/- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`. -/
def instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr :=
instantiateForallAux ps 0 e
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta;
registerTraceClass `Meta.debug
end Meta
export Meta (MetaM)
def instantiateForall (e : Expr) (ps : Array Expr) : m Expr :=
liftMetaM $ instantiateForallAux ps 0 e
end Methods
end Lean

4
src/Lean/Meta/Check.lean
View file

@ -41,7 +41,7 @@ lambdaTelescope e $ fun xs b => do
ensureType t;
check t;
vType ← inferType v;
unlessM (isExprDefEqAux t vType) $ throwLetTypeMismatchMessage x.fvarId!;
unlessM (Meta.isExprDefEqAux t vType) $ throwLetTypeMismatchMessage x.fvarId!;
check v
};
check b
@ -92,7 +92,7 @@ fType ← whnf fType;
match fType with
| Expr.forallE _ d _ _ => do
aType ← inferType a;
unlessM (isExprDefEqAux d aType) $ throwAppTypeMismatch f a
unlessM (Meta.isExprDefEqAux d aType) $ throwAppTypeMismatch f a
| _ => throwFunctionExpected (mkApp f a)
private partial def checkAux : Expr → MetaM Unit

2
src/Lean/Meta/EqnCompiler/CaseArraySizes.lean
View file

@ -45,7 +45,7 @@ private partial def introArrayLitAux (mvarId : MVarId) (α : Expr) (a : Expr) (n
aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkNatLit n, aSizeEqN];
withLocalDecl `hEqALit aEqXsLit BinderInfo.default fun heq => do
target ← getMVarType mvarId;
newTarget ← mkForall (xs.push heq) target;
newTarget ← mkForallFVars (xs.push heq) target;
pure (newTarget, args.push aEqLitPrf)
private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do

10
src/Lean/Meta/EqnCompiler/Match.lean
View file

@ -202,7 +202,7 @@ private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt
minorType ← withExistingLocalDecls lhs.fvarDecls do {
args ← lhs.patterns.toArray.mapM Pattern.toExpr;
let minorType := mkAppN motive args;
mkForall xs minorType
mkForallFVars xs minorType
};
let minorType := if minorType.isForall then minorType else mkThunkType minorType;
let idx := alts.length;
@ -387,7 +387,7 @@ else do
partial def unify : Expr → Expr → M Bool
| a, b => do
trace! `Meta.EqnCompiler.matchUnify (a ++ " =?= " ++ b);
condM (liftM $ isDefEq a b) (pure true) do
condM (isDefEq a b) (pure true) do
a' ← expandIfVar a;
b' ← expandIfVar b;
if a != a' || b != b' then unify a' b'
@ -678,8 +678,8 @@ withAlts motive lhss fun alts minors => do
let examples := majors.toList.map fun major => Example.var major.fvarId!;
(_, s) ← (process { mvarId := mvar.mvarId!, vars := majors.toList, alts := alts, examples := examples }).run {};
let args := #[motive] ++ majors ++ minors;
type ← mkForall args mvarType;
val ← mkLambda args mvar;
type ← mkForallFVars args mvarType;
val ← mkLambdaFVars args mvar;
trace! `Meta.EqnCompiler.matchDebug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
elim ← mkAuxDefinition elimName type val;
setInlineAttribute elimName;
@ -715,7 +715,7 @@ else do
def mkElimTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp : Bool := false) : MetaM ElimResult := do
sortv ← mkElimSort majors lhss inProp;
generalizeTelescope majors.toArray `_d fun majors => do
motiveType ← mkForall majors sortv;
motiveType ← mkForallFVars majors sortv;
mkElim elimName motiveType lhss
@[init] private def regTraceClasses : IO Unit := do

73
src/Lean/Meta/ExprDefEq.lean
View file

@ -29,15 +29,15 @@ if a.isLambda && !b.isLambda then do
bType ← whnfD bType;
match bType with
| Expr.forallE n d _ c =>
let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
commitWhen $ isExprDefEqAux a b'
let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
commitWhen $ Meta.isExprDefEqAux a b'
| _ => pure false
else
pure false
/-- Support for `Lean.reduceBool` and `Lean.reduceNat` -/
def isDefEqNative (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
s? ← reduceNative? s;
t? ← reduceNative? t;
match s?, t? with
@ -48,7 +48,7 @@ match s?, t? with
/-- Support for reducing Nat basic operations. -/
def isDefEqNat (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
if s.hasFVar || s.hasMVar || t.hasFVar || t.hasMVar then
pure LBool.undef
else do
@ -62,7 +62,7 @@ else do
/-- Support for constraints of the form `("..." =?= String.mk cs)` -/
def isDefEqStringLit (s t : Expr) : MetaM LBool := do
let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
if s.isStringLit && t.isAppOf `String.mk then
isDefEq (WHNF.toCtorIfLit s) t
else if s.isAppOf `String.mk && t.isStringLit then
@ -122,12 +122,12 @@ private partial def isDefEqArgsFirstPass
let a₂ := args₂.get! i;
if info.implicit || info.instImplicit then
condM (isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂)
(condM (isExprDefEqAux a₁ a₂)
(condM (Meta.isExprDefEqAux a₁ a₂)
(isDefEqArgsFirstPass (i+1) postponed)
(pure none))
(isDefEqArgsFirstPass (i+1) (postponed.push i))
else
condM (isExprDefEqAux a₁ a₂)
condM (Meta.isExprDefEqAux a₁ a₂)
(isDefEqArgsFirstPass (i+1) postponed)
(pure none)
else
@ -138,7 +138,7 @@ private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.s
if h₁ : i < args₁.size then
let a₁ := args₁.get ⟨i, h₁⟩;
let a₂ := args₂.get ⟨i, h ▸ h₁⟩;
condM (isExprDefEqAux a₁ a₂)
condM (Meta.isExprDefEqAux a₁ a₂)
(isDefEqArgsAux (i+1))
(pure false)
else
@ -147,7 +147,7 @@ private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.s
@[specialize] private def trySynthPending (e : Expr) : MetaM Bool := do
mvarId? ← getStuckMVar? e;
match mvarId? with
| some mvarId => synthPending mvarId
| some mvarId => Meta.synthPending mvarId
| none => pure false
private def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : MetaM Bool :=
@ -168,7 +168,7 @@ if h : args₁.size = args₂.size then do
_ ← trySynthPending a₂;
pure ()
};
withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂)
else
pure false
@ -190,7 +190,7 @@ else
fvarDecl ← getFVarLocalDecl fvar;
let fvarType := fvarDecl.type;
let d₂ := ds₂.get! i;
condM (isExprDefEqAux fvarType d₂)
condM (Meta.isExprDefEqAux fvarType d₂)
(do c? ← isClass? fvarType;
match c? with
| some className => withNewLocalInstance className fvar $ isDefEqBindingDomain (i+1) k
@ -219,7 +219,7 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr →
| _, _ =>
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
isDefEqBindingDomain fvars ds₂ 0 $
isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
@[inline] private def isDefEqBinding (a b : Expr) : MetaM Bool := do
lctx ← getLCtx;
@ -230,7 +230,7 @@ traceCtx `Meta.isDefEq.assign.checkTypes $ do
-- must check whether types are definitionally equal or not, before assigning and returning true
mvarType ← inferType mvar;
vType ← inferType v;
condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
condM (withTransparency TransparencyMode.default $ Meta.isExprDefEqAux mvarType vType)
(do trace! `Meta.isDefEq.assign.final (mvar ++ " := " ++ v);
assignExprMVar mvar.mvarId! v; pure true)
(do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
@ -407,11 +407,8 @@ else do
traceM `Meta.isDefEq.assign.outOfScopeFVar $ addAssignmentInfo fvar;
throwOutOfScopeFVar
@[inline] def getMCtx : CheckAssignmentM MetavarContext := do
liftM Meta.getMCtx
def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) : CheckAssignmentM Expr := do
liftM $ mkFreshExprMVarAt lctx localInsts type
mkFreshExprMVarAt lctx localInsts type
@[specialize] def checkMVar (check : Expr → CheckAssignmentM Expr) (mvar : Expr) : CheckAssignmentM Expr := do
let mvarId := mvar.mvarId!;
@ -458,7 +455,7 @@ mvarType ← inferType mvar;
forallBoundedTelescope mvarType numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
else do
v ← mkLambda xs newMVar;
v ← mkLambdaFVars xs newMVar;
checkTypesAndAssign mvar v
partial def check : Expr → CheckAssignmentM Expr
@ -483,8 +480,8 @@ partial def check : Expr → CheckAssignmentM Expr
args ← args.mapM (visit check);
pure $ mkAppN f args)
(fun ex =>
condM (liftM $ isDelayedAssigned f.mvarId!) (throw ex) do
eType ← liftM $ inferType e;
condM (isDelayedAssigned f.mvarId!) (throw ex) do
eType ← inferType e;
mvarType ← check eType;
/- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
Note that `mvarType` may be different from `eType`. -/
@ -580,7 +577,7 @@ else do
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
match v with
| Expr.app f a _ => isExprDefEqAux args.back a <&&> isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
| Expr.app f a _ => Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
| _ => pure false
/-
@ -640,7 +637,7 @@ if cfg.constApprox then do
forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
else do
v ← mkLambda xs v;
v ← mkLambdaFVars xs v;
checkTypesAndAssign mvar v
else
pure false
@ -676,9 +673,9 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
| none => useFOApprox args
| some v => do
trace `Meta.isDefEq.assign.beforeMkLambda $ fun _ => mvar ++ " " ++ args ++ " := " ++ v;
v ← mkLambda args v;
v ← mkLambdaFVars args v;
if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
/- We need to type check `v` because abstraction using `mkLambda` may have produced
/- We need to type check `v` because abstraction using `mkLambdaFVars` may have produced
a type incorrect term. See discussion at A2 -/
condM (isTypeCorrect v)
(checkTypesAndAssign mvar v)
@ -708,17 +705,17 @@ toLBoolM $ isListLevelDefEqAux us vs
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do
trace! `Meta.isDefEq.delta.unfoldLeft fn;
toLBoolM $ isExprDefEqAux t s
toLBoolM $ Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do
trace! `Meta.isDefEq.delta.unfoldRight fn;
toLBoolM $ isExprDefEqAux t s
toLBoolM $ Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
trace! `Meta.isDefEq.delta.unfoldLeftRight fn;
toLBoolM $ isExprDefEqAux t s
toLBoolM $ Meta.isExprDefEqAux t s
/-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
@ -810,8 +807,8 @@ else
private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
condM shouldReduceReducibleOnly
(unfoldDefEq tInfo sInfo t s)
(do tReducible ← isReducible tInfo.name;
sReducible ← isReducible sInfo.name;
(do tReducible ← Meta.isReducible tInfo.name;
sReducible ← Meta.isReducible sInfo.name;
if tReducible && !sReducible then
unfold t (unfoldDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s
else if !tReducible && sReducible then
@ -914,11 +911,11 @@ match status with
| LBool.true => do
tType ← inferType t;
sType ← inferType s;
toLBoolM $ isExprDefEqAux tType sType
toLBoolM $ Meta.isExprDefEqAux tType sType
| LBool.undef => do
tType ← inferType t;
condM (isProp tType)
(do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
(do sType ← inferType s; toLBoolM $ Meta.isExprDefEqAux tType sType)
(pure LBool.undef)
private partial def isDefEqQuick : Expr → Expr → MetaM LBool
@ -995,14 +992,14 @@ else
mvarId? ← getStuckMVar? e;
match mvarId? with
| some mvarId =>
condM (synthPending mvarId)
condM (Meta.synthPending mvarId)
(do e ← instantiateMVars e; successK e)
failK
| none => failK
private def isDefEqOnFailure (t s : Expr) : MetaM Bool :=
unstuckMVar t (fun t => isExprDefEqAux t s) $
unstuckMVar s (fun s => isExprDefEqAux t s) $
unstuckMVar t (fun t => Meta.isExprDefEqAux t s) $
unstuckMVar s (fun s => Meta.isExprDefEqAux t s) $
pure false
/- Remove unnecessary let-decls -/
@ -1019,15 +1016,15 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
whenUndefDo (isDefEqProofIrrel t s) $
isDefEqWHNF t s $ fun t s => do
condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
whenUndefDo (isDefEqNative t s) $ do
whenUndefDo (isDefEqNat t s) $ do
whenUndefDo (isDefEqOffset t s) $ do
whenUndefDo (isDefEqNative t s) do
whenUndefDo (isDefEqNat t s) do
whenUndefDo (isDefEqOffset t s) do
whenUndefDo (isDefEqDelta t s) $
match t, s with
| Expr.const c us _, Expr.const d vs _ => if c == d then isListLevelDefEqAux us vs else pure false
| Expr.app _ _ _, Expr.app _ _ _ =>
let tFn := t.getAppFn;
condM (commitWhen (isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs))
condM (commitWhen (Meta.isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs))
(pure true)
(isDefEqOnFailure t s)
| _, _ =>

29
src/Lean/Meta/InferType.lean
View file

@ -103,7 +103,7 @@ forallTelescope e $ fun xs e => do
private def inferLambdaType (e : Expr) : MetaM Expr :=
lambdaTelescope e $ fun xs e => do
type ← inferType e;
mkForall xs type
mkForallFVars xs type
@[inline] private def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
savingCache $ do
@ -217,7 +217,7 @@ partial def isPropQuick : Expr → MetaM LBool
to decide whether is a proposition or not. We return `false` in this
case. We considered using `LBool` and retuning `LBool.undef`, but
we have no applications for it. -/
def isProp (e : Expr) : MetaM Bool := do
protected def isProp (e : Expr) : MetaM Bool := do
r ← isPropQuick e;
match r with
| LBool.true => pure true
@ -273,14 +273,14 @@ partial def isProofQuick : Expr → MetaM LBool
| Expr.app f _ _ => isProofQuickApp isProofQuick f 1
| Expr.localE _ _ _ _ => unreachable!
def isProof (e : Expr) : MetaM Bool := do
protected def isProof (e : Expr) : MetaM Bool := do
r ← isProofQuick e;
match r with
| LBool.true => pure true
| LBool.false => pure false
| LBool.undef => do
type ← inferType e;
isProp type
Meta.isProp type
/--
`isArrowType type n` is an "approximate" predicate which returns `LBool.true`
@ -326,7 +326,7 @@ partial def isTypeQuick : Expr → MetaM LBool
| Expr.app f _ _ => isTypeQuickApp f 1
| Expr.localE _ _ _ _ => unreachable!
def isType (e : Expr) : MetaM Bool := do
protected def isType {m} [MonadMetaM m] (e : Expr) : m Bool := liftMetaM do
r ← isTypeQuick e;
match r with
| LBool.true => pure true
@ -338,7 +338,7 @@ match r with
| Expr.sort _ _ => pure true
| _ => pure false
partial def isTypeFormerType : Expr → MetaM Bool
protected partial def isTypeFormerType : Expr → MetaM Bool
| type => do
type ← whnfD type;
match type with
@ -348,12 +348,25 @@ partial def isTypeFormerType : Expr → MetaM Bool
isTypeFormerType (b.instantiate1 fvar)
| _ => pure false
end Meta
def isProp {m} [MonadMetaM m] (e : Expr) : m Bool :=
liftMetaM $ Meta.isProp e
def isProof {m} [MonadMetaM m] (e : Expr) : m Bool :=
liftMetaM $ Meta.isProof e
def isType {m} [MonadMetaM m] (e : Expr) : m Bool :=
liftMetaM $ Meta.isType e
def isTypeFormerType {m} [MonadMetaM m] (e : Expr) : m Bool :=
liftMetaM $ Meta.isTypeFormerType e
/--
Return true iff `e : Sort _` or `e : (forall As, Sort _)`.
Remark: it subsumes `isType` -/
def isTypeFormer (e : Expr) : MetaM Bool := do
def isTypeFormer {m} [MonadMetaM m] (e : Expr) : m Bool := liftMetaM do
type ← inferType e;
isTypeFormerType type
end Meta
end Lean

8
src/Lean/Meta/KAbstract.lean
View file

@ -10,9 +10,9 @@ import Lean.Meta.ExprDefEq
namespace Lean
namespace Meta
private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : HeadIndex) (pNumArgs : Nat) : Expr → Nat → StateT Nat MetaM Expr
private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : HeadIndex) (pNumArgs : Nat) : Expr → Nat → StateRefT Nat MetaM Expr
| e, offset =>
let visitChildren : Unit → StateT Nat MetaM Expr := fun _ =>
let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ =>
match e with
| Expr.app f a _ => do f ← kabstractAux f offset; a ← kabstractAux a offset; pure $ e.updateApp! f a
| Expr.mdata _ b _ => do b ← kabstractAux b offset; pure $ e.updateMData! b
@ -23,7 +23,7 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
| e => pure e;
if e.hasLooseBVars then visitChildren ()
else if e.toHeadIndex == pHeadIdx && e.headNumArgs == pNumArgs then
condM (liftM $ isDefEq e p)
condM (isDefEq e p)
(do i ← get;
set (i+1);
if occs.contains i then
@ -34,7 +34,7 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
else
visitChildren ()
def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : MetaM Expr :=
def kabstract {m} [MonadMetaM m] (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : m Expr := liftMetaM do
(kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
end Meta

40
src/Lean/Meta/LevelDefEq.lean
View file

@ -224,26 +224,34 @@ match r? with
| some _ => pure true
| none => pure false
/- Public interface -/
def isLevelDefEq (u v : Level) : MetaM Bool :=
traceCtx `Meta.isLevelDefEq $ do
b ← commitWhen $ isLevelDefEqAux u v;
trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure");
pure b
def isExprDefEq (t s : Expr) : MetaM Bool :=
traceCtx `Meta.isDefEq $ do
b ← commitWhen $ isExprDefEqAux t s;
trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure");
pure b
abbrev isDefEq := @isExprDefEq
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta.isLevelDefEq;
registerTraceClass `Meta.isLevelDefEq.step;
registerTraceClass `Meta.isLevelDefEq.postponed
end Meta
/- Public interface -/
section Methods
variables {m : Type → Type} [MonadMetaM m]
def isLevelDefEq (u v : Level) : m Bool := liftMetaM do
traceCtx `Meta.isLevelDefEq $ do
b ← Meta.commitWhen $ Meta.isLevelDefEqAux u v;
trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure");
pure b
def isExprDefEq (t s : Expr) : m Bool := liftMetaM do
traceCtx `Meta.isDefEq $ do
b ← Meta.commitWhen $ Meta.isExprDefEqAux t s;
trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure");
pure b
abbrev isDefEq (t s : Expr) : m Bool :=
isExprDefEq t s
def isDefEqNoConstantApprox (t s : Expr) : m Bool := liftMetaM do
Meta.approxDefEq $ isDefEq t s
end Methods
end Lean

2
src/Lean/Meta/Offset.lean
View file

@ -99,7 +99,7 @@ else if isNatZero e then mkNatLit offset
else mkAppB (mkConst `Nat.add) e (mkNatLit offset)
def isDefEqOffset (s t : Expr) : MetaM LBool :=
let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
match isOffset s with
| some (s, k₁) => match isOffset t with
| some (t, k₂) => -- s+k₁ =?= t+k₂

4
src/Lean/Meta/Reduce.lean
View file

@ -32,8 +32,8 @@ partial def reduceAux (explicitOnly : Bool) (skipTypes : Bool) (skipProofs : Boo
args.modifyM i reduceAux)
args;
pure $ mkAppN f args
| Expr.lam _ _ _ _ => lambdaTelescope e $ fun xs b => do b ← reduceAux b; mkLambda xs b
| Expr.forallE _ _ _ _ => forallTelescope e $ fun xs b => do b ← reduceAux b; mkForall xs b
| Expr.lam _ _ _ _ => lambdaTelescope e $ fun xs b => do b ← reduceAux b; mkLambdaFVars xs b
| Expr.forallE _ _ _ _ => forallTelescope e $ fun xs b => do b ← reduceAux b; mkForallFVars xs b
| _ => pure e
def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=

12
src/Lean/Meta/SynthInstance.lean
View file

@ -229,8 +229,8 @@ match entry? with
We must instantiate assigned metavariables before we invoke `mkTableKey`. -/
def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr :=
withMCtx mctx $ do
mvarType ← liftM $ inferType mvar;
mvarType ← liftM $ instantiateMVars mvarType;
mvarType ← inferType mvar;
mvarType ← instantiateMVars mvarType;
pure $ mkTableKey mctx mvarType
/- See `getSubgoals` and `getSubgoalsAux`
@ -248,7 +248,7 @@ private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInst
: Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult
| args, j, subgoals, instVal, Expr.forallE n d b c => do
let d := d.instantiateRevRange j args.size args;
mvarType ← mkForall xs d;
mvarType ← mkForallFVars xs d;
mvar ← mkFreshExprMVarAt lctx localInsts mvarType;
let arg := mkAppN mvar xs;
let instVal := mkApp instVal arg;
@ -298,7 +298,7 @@ forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do
⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst;
trace! `Meta.synthInstance.tryResolve (mvarTypeBody ++ " =?= " ++ instTypeBody);
condM (isDefEq mvarTypeBody instTypeBody)
(do instVal ← mkLambda xs instVal;
(do instVal ← mkLambdaFVars xs instVal;
condM (isDefEq mvar instVal)
(do trace! `Meta.synthInstance.tryResolve "success";
mctx ← getMCtx;
@ -482,7 +482,7 @@ the original type `C a_1 ... a_n` witht the normalized one.
private def preprocess (type : Expr) : MetaM Expr :=
forallTelescopeReducing type $ fun xs type => do
type ← whnf type;
mkForall xs type
mkForallFVars xs type
private def preprocessLevels (us : List Level) : MetaM (List Level) := do
us ← us.foldlM
@ -523,7 +523,7 @@ forallTelescope type $ fun xs typeBody =>
let c := mkConst constName us;
cType ← inferType c;
args ← preprocessArgs cType 0 args;
mkForall xs (mkAppN c args)
mkForallFVars xs (mkAppN c args)
| _ => pure type
@[init] def maxStepsOption : IO Unit :=

6
src/Lean/Meta/Tactic/Cases.lean
View file

@ -99,9 +99,9 @@ withMVarContext mvarId $ do
/- auxType `forall (j' : J) (h' : I A j'), j == j' -> h == h' -> target -/
target ← getMVarType mvarId;
tag ← getMVarTag mvarId;
auxType ← mkForall newEqs target;
auxType ← mkForall #[h'] auxType;
auxType ← mkForall newIndices auxType;
auxType ← mkForallFVars newEqs target;
auxType ← mkForallFVars #[h'] auxType;
auxType ← mkForallFVars newIndices auxType;
newMVar ← mkFreshExprMVarAt lctx localInsts auxType tag MetavarKind.syntheticOpaque;
/- assign mvarId := newMVar indices h refls -/
assignExprMVar mvarId (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls);

4
src/Lean/Meta/Tactic/Induction.lean
View file

@ -204,8 +204,8 @@ withMVarContext mvarId $ do
rec ← addRecParams mvarId majorTypeArgs recInfo.paramsPos rec;
-- Compute motive
let motive := target;
motive ← if recInfo.depElim then mkLambda #[major] motive else pure motive;
motive ← mkLambda indices motive;
motive ← if recInfo.depElim then mkLambdaFVars #[major] motive else pure motive;
motive ← mkLambdaFVars indices motive;
let rec := mkApp rec motive;
finalize mvarId givenNames recInfo reverted major indices baseSubst rec
| _ =>

2
src/Lean/Meta/Tactic/Intro.lean
View file

@ -19,7 +19,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
let type := type.headBeta;
newMVar ← mkFreshExprSyntheticOpaqueMVar type tag;
lctx ← getLCtx;
newVal ← mkLambda fvars newMVar;
newVal ← mkLambdaFVars fvars newMVar;
assignExprMVar mvarId newVal;
pure $ (fvars, newMVar.mvarId!)
| (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do

6
src/Lean/Meta/Tactic/Subst.lean
View file

@ -79,7 +79,7 @@ withMVarContext mvarId $ do
reflB ← mkEqRefl b;
let newType := newType.replaceFVar h reflB;
if symm then do
motive ← mkLambda #[a, h] type;
motive ← mkLambdaFVars #[a, h] type;
continue motive newType
else do
/- `type` depends on (h : a = b). So, we use the following trick to avoid a type incorrect motive.
@ -92,11 +92,11 @@ withMVarContext mvarId $ do
hAuxSymm ← mkEqSymm hAux;
/- replace h in type with hAuxSymm -/
let newType := type.replaceFVar h hAuxSymm;
mkLambda #[a, hAux] newType
mkLambdaFVars #[a, hAux] newType
};
continue motive newType
else do
motive ← mkLambda #[a] type;
motive ← mkLambdaFVars #[a] type;
let newType := type.replaceFVar a b;
continue motive newType
| _ =>

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

@ -11,14 +11,14 @@ import Lean.Meta.LevelDefEq
namespace Lean
namespace Meta
def isAuxDef? (constName : Name) : MetaM Bool := do
protected def isAuxDef? (constName : Name) : MetaM Bool := do
env ← getEnv; pure (isAuxRecursor env constName || isNoConfusion env constName)
def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
Lean.WHNF.unfoldDefinitionAux getConstNoEx? isAuxDef? whnf inferType isExprDefEq synthPending getLocalDecl getExprMVarAssignment? e
protected def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
Lean.WHNF.unfoldDefinitionAux getConstNoEx? Meta.isAuxDef? whnf inferType isExprDefEq Meta.synthPending getLocalDecl getExprMVarAssignment? e
def whnfCore (e : Expr) : MetaM Expr :=
Lean.WHNF.whnfCore getConstNoEx? isAuxDef? whnf inferType isExprDefEqAux getLocalDecl getExprMVarAssignment? e
protected def whnfCore (e : Expr) : MetaM Expr :=
Lean.WHNF.whnfCore getConstNoEx? Meta.isAuxDef? whnf inferType Meta.isExprDefEqAux getLocalDecl getExprMVarAssignment? e
unsafe def reduceNativeConst (α : Type) (typeName : Name) (constName : Name) : MetaM α := do
env ← getEnv;
@ -119,7 +119,7 @@ partial def whnfImpl : Expr → MetaM Expr
match e? with
| some e' => pure e'
| none => do
e' ← whnfCore e;
e' ← Meta.whnfCore e;
v? ← reduceNat? e';
match v? with
| some v => cache useCache e v
@ -128,7 +128,7 @@ partial def whnfImpl : Expr → MetaM Expr
match v? with
| some v => cache useCache e v
| none => do
e? ← unfoldDefinition? e';
e? ← Meta.unfoldDefinition? e';
match e? with
| some e => whnfImpl e
| none => cache useCache e e'
@ -153,27 +153,41 @@ match e.getAppFn with
| _ => pure none
| _ => pure none
@[specialize] private partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr
@[specialize] partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr
| e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment? e $ fun e => do
e ← whnfCore e;
e ← Meta.whnfCore e;
condM (pred e)
(do
e? ← unfoldDefinition? e;
e? ← Meta.unfoldDefinition? e;
match e? with
| some e => whnfHeadPredAux e
| none => pure e)
(pure e)
def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
whnfHeadPredAux pred e
end Meta
def whnfUntil (e : Expr) (declName : Name) : MetaM (Option Expr) := do
e ← whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e;
section Methods
variables {m : Type → Type} [MonadMetaM m]
@[inline] def isAuxDef? (constName : Name) : m Bool :=
liftMetaM $ Meta.isAuxDef? constName
@[inline] def unfoldDefinition? (e : Expr) : m (Option Expr) :=
liftMetaM $ Meta.unfoldDefinition? e
@[inline] def whnfCore (e : Expr) : m Expr :=
liftMetaM $ Meta.whnfCore e
@[inline] def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : m Expr :=
liftMetaM $ Meta.whnfHeadPredAux pred e
def whnfUntil {m} [MonadMetaM m] (e : Expr) (declName : Name) : m (Option Expr) := liftMetaM do
e ← Meta.whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e;
if e.isAppOf declName then pure e
else pure none
def getStuckMVar? (e : Expr) : MetaM (Option MVarId) :=
WHNF.getStuckMVar? getConst? whnf e
def getStuckMVar? {m} [MonadMetaM m] (e : Expr) : m (Option MVarId) := liftMetaM do
WHNF.getStuckMVar? Meta.getConst? whnf e
end Meta
end Methods
end Lean

4
src/Lean/ParserCompiler.lean
View file

@ -36,7 +36,7 @@ open Meta
partial def compileParserBody {α} (ctx : Context α) : Expr → MetaM Expr | e => do
e ← whnfCore e;
match e with
| e@(Expr.lam _ _ _ _) => Meta.lambdaTelescope e fun xs b => compileParserBody b >>= Meta.mkLambda xs
| e@(Expr.lam _ _ _ _) => Meta.lambdaTelescope e fun xs b => compileParserBody b >>= mkLambdaFVars xs
| e@(Expr.fvar _ _) => pure e
| _ => do
let fn := e.getAppFn;
@ -88,7 +88,7 @@ match e with
else do
-- if this is a generic function, e.g. `HasAndthen.andthen`, it's easier to just unfold it until we are
-- back to parser combinators
some e' ← liftM $ unfoldDefinition? e
some e' ← unfoldDefinition? e
| throwError $ "don't know how to generate " ++ ctx.varName ++ " for non-parser combinator '" ++ toString e ++ "'";
compileParserBody e'
end

2
src/Lean/Util/Closure.lean
View file

@ -194,7 +194,7 @@ match (mkTypeValue { lctxInput := lctx, zeta := zeta }).run { mctx := mctx } wit
end Closure
def mkAuxDefinition (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
def mkAuxDefinitionCore (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
(zeta : Bool := false) : Except KernelException (Expr × Environment × MetavarContext) :=
match Closure.mkClosure mctx lctx type value zeta with
| Except.error ex => throw $ KernelException.other ex