diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 75b98fa751..c45d4c352e 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -101,7 +101,8 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal => let n := structVal.numParams let structParams := structType.getAppArgs - if n != structParams.size then failed () + if n != structParams.size then + failed () else do let mut ctorType ← inferAppType (mkConst ctorVal.name structLvls) structParams for i in [:idx] do @@ -109,13 +110,13 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp match ctorType with | Expr.forallE _ _ body _ => if body.hasLooseBVars then - ctorType := body.instantiate1 $ mkProj structName i e + ctorType := body.instantiate1 <| mkProj structName i e else ctorType := body | _ => failed () ctorType ← whnf ctorType match ctorType with - | Expr.forallE _ d _ _ => pure d + | Expr.forallE _ d _ _ => return d | _ => failed () def throwTypeExcepted {α} (type : Expr) : MetaM α := @@ -125,14 +126,14 @@ def getLevel (type : Expr) : MetaM Level := do let typeType ← inferType type let typeType ← whnfD typeType match typeType with - | Expr.sort lvl _ => pure lvl + | Expr.sort lvl _ => return lvl | Expr.mvar mvarId _ => if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then throwTypeExcepted type else let lvl ← mkFreshLevelMVar assignExprMVar mvarId (mkSort lvl) - pure lvl + return lvl | _ => throwTypeExcepted type private def inferForallType (e : Expr) : MetaM Expr := @@ -141,8 +142,8 @@ private def inferForallType (e : Expr) : MetaM Expr := let lvl ← xs.foldrM (init := lvl) fun x lvl => do let xType ← inferType x let xTypeLvl ← getLevel xType - pure $ mkLevelIMax' xTypeLvl lvl - pure $ mkSort lvl.normalize + return mkLevelIMax' xTypeLvl lvl + return mkSort lvl.normalize /- Infer type of lambda and let expressions -/ private def inferLambdaType (e : Expr) : MetaM Expr := @@ -161,22 +162,22 @@ def throwUnknownMVar {α} (mvarId : MVarId) : MetaM α := private def inferMVarType (mvarId : MVarId) : MetaM Expr := do match (← getMCtx).findDecl? mvarId with - | some d => pure d.type + | some d => return d.type | none => throwUnknownMVar mvarId private def inferFVarType (fvarId : FVarId) : MetaM Expr := do match (← getLCtx).find? fvarId with - | some d => pure d.type + | some d => return d.type | none => throwUnknownFVar fvarId @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do match (← get).cache.inferType.find? e with - | some type => pure type + | some type => return type | none => let type ← inferType unless e.hasMVar || type.hasMVar do modifyInferTypeCache fun c => c.insert e type - pure type + return type @[export lean_infer_type] def inferTypeImp (e : Expr) : MetaM Expr := @@ -189,8 +190,8 @@ def inferTypeImp (e : Expr) : MetaM Expr := | Expr.fvar fvarId _ => inferFVarType fvarId | Expr.bvar bidx _ => throwError "unexpected bound variable {mkBVar bidx}" | Expr.mdata _ e _ => infer e - | Expr.lit v _ => pure v.type - | Expr.sort lvl _ => pure $ mkSort (mkLevelSucc lvl) + | Expr.lit v _ => return v.type + | Expr.sort lvl _ => return mkSort (mkLevelSucc lvl) | e@(Expr.forallE _ _ _ _) => checkInferTypeCache e (inferForallType e) | e@(Expr.lam _ _ _ _) => checkInferTypeCache e (inferLambdaType e) | e@(Expr.letE _ _ _ _ _) => checkInferTypeCache e (inferLambdaType e) @@ -213,11 +214,11 @@ private def isAlwaysZero : Level → Bool Remark: `type` can be a dependent arrow. -/ private partial def isArrowProp : Expr → Nat → MetaM LBool | Expr.sort u _, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool - | Expr.forallE _ _ _ _, 0 => pure LBool.false + | Expr.forallE _ _ _ _, 0 => return LBool.false | Expr.forallE _ _ b _, n+1 => isArrowProp b n | Expr.letE _ _ _ b _, n => isArrowProp b n | Expr.mdata _ e _, n => isArrowProp e n - | _, _ => pure LBool.undef + | _, _ => return LBool.undef /-- `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true` @@ -229,20 +230,20 @@ private partial def isPropQuickApp : Expr → Nat → MetaM LBool | Expr.app f _ _, arity => isPropQuickApp f (arity+1) | Expr.mdata _ e _, arity => isPropQuickApp e arity | Expr.letE _ _ _ b _, arity => isPropQuickApp b arity - | Expr.lam _ _ _ _, 0 => pure LBool.false + | Expr.lam _ _ _ _, 0 => return LBool.false | Expr.lam _ _ b _, arity+1 => isPropQuickApp b arity - | _, _ => pure LBool.undef + | _, _ => return LBool.undef /-- `isPropQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a proposition. -/ partial def isPropQuick : Expr → MetaM LBool - | Expr.bvar _ _ => pure LBool.undef - | Expr.lit _ _ => pure LBool.false - | Expr.sort _ _ => pure LBool.false - | Expr.lam _ _ _ _ => pure LBool.false + | Expr.bvar _ _ => return LBool.undef + | Expr.lit _ _ => return LBool.false + | Expr.sort _ _ => return LBool.false + | Expr.lam _ _ _ _ => return LBool.false | Expr.letE _ _ _ b _ => isPropQuick b - | Expr.proj _ _ _ _ => pure LBool.undef + | Expr.proj _ _ _ _ => return LBool.undef | Expr.forallE _ _ b _ => isPropQuick b | Expr.mdata _ e _ => isPropQuick e | Expr.const c lvls _ => do let constType ← inferConstType c lvls; isArrowProp constType 0 @@ -259,14 +260,14 @@ partial def isPropQuick : Expr → MetaM LBool def isProp (e : Expr) : MetaM Bool := do let r ← isPropQuick e match r with - | LBool.true => pure true - | LBool.false => pure false + | LBool.true => return true + | LBool.false => return false | LBool.undef => let type ← inferType e let type ← whnfD type match type with | Expr.sort u _ => return isAlwaysZero (← instantiateLevelMVars u) - | _ => pure false + | _ => return false /-- `isArrowProposition type n` is an "approximate" predicate which returns `LBool.true` @@ -277,7 +278,7 @@ private partial def isArrowProposition : Expr → Nat → MetaM LBool | Expr.letE _ _ _ b _, n => isArrowProposition b n | Expr.mdata _ e _, n => isArrowProposition e n | type, 0 => isPropQuick type - | _, _ => pure LBool.undef + | _, _ => return LBool.undef mutual /-- @@ -292,19 +293,19 @@ private partial def isProofQuickApp : Expr → Nat → MetaM LBool | Expr.letE _ _ _ b _, arity => isProofQuickApp b arity | Expr.lam _ _ b _, 0 => isProofQuick b | Expr.lam _ _ b _, arity+1 => isProofQuickApp b arity - | _, _ => pure LBool.undef + | _, _ => return LBool.undef /-- `isProofQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a proof. -/ partial def isProofQuick : Expr → MetaM LBool - | Expr.bvar _ _ => pure LBool.undef - | Expr.lit _ _ => pure LBool.false - | Expr.sort _ _ => pure LBool.false + | Expr.bvar _ _ => return LBool.undef + | Expr.lit _ _ => return LBool.false + | Expr.sort _ _ => return LBool.false | Expr.lam _ _ b _ => isProofQuick b | Expr.letE _ _ _ b _ => isProofQuick b - | Expr.proj _ _ _ _ => pure LBool.undef - | Expr.forallE _ _ b _ => pure LBool.false + | Expr.proj _ _ _ _ => return LBool.undef + | Expr.forallE _ _ b _ => return LBool.false | Expr.mdata _ e _ => isProofQuick e | Expr.const c lvls _ => do let constType ← inferConstType c lvls; isArrowProposition constType 0 | Expr.fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType 0 @@ -316,8 +317,8 @@ end def isProof (e : Expr) : MetaM Bool := do let r ← isProofQuick e match r with - | LBool.true => pure true - | LBool.false => pure false + | LBool.true => return true + | LBool.false => return false | LBool.undef => do let type ← inferType e Meta.isProp type @@ -327,12 +328,12 @@ def isProof (e : Expr) : MetaM Bool := do if `type` is of the form `A_1 -> ... -> A_n -> Sort _`. Remark: `type` can be a dependent arrow. -/ private partial def isArrowType : Expr → Nat → MetaM LBool - | Expr.sort u _, 0 => pure LBool.true - | Expr.forallE _ _ _ _, 0 => pure LBool.false + | Expr.sort u _, 0 => return LBool.true + | Expr.forallE _ _ _ _, 0 => return LBool.false | Expr.forallE _ _ b _, n+1 => isArrowType b n | Expr.letE _ _ _ b _, n => isArrowType b n | Expr.mdata _ e _, n => isArrowType e n - | _, _ => pure LBool.undef + | _, _ => return LBool.undef /-- `isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true` @@ -344,21 +345,21 @@ private partial def isTypeQuickApp : Expr → Nat → MetaM LBool | Expr.app f _ _, arity => isTypeQuickApp f (arity+1) | Expr.mdata _ e _, arity => isTypeQuickApp e arity | Expr.letE _ _ _ b _, arity => isTypeQuickApp b arity - | Expr.lam _ _ _ _, 0 => pure LBool.false + | Expr.lam _ _ _ _, 0 => return LBool.false | Expr.lam _ _ b _, arity+1 => isTypeQuickApp b arity - | _, _ => pure LBool.undef + | _, _ => return LBool.undef /-- `isTypeQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a type. -/ partial def isTypeQuick : Expr → MetaM LBool - | Expr.bvar _ _ => pure LBool.undef - | Expr.lit _ _ => pure LBool.false - | Expr.sort _ _ => pure LBool.true - | Expr.lam _ _ _ _ => pure LBool.false + | Expr.bvar _ _ => return LBool.undef + | Expr.lit _ _ => return LBool.false + | Expr.sort _ _ => return LBool.true + | Expr.lam _ _ _ _ => return LBool.false | Expr.letE _ _ _ b _ => isTypeQuick b - | Expr.proj _ _ _ _ => pure LBool.undef - | Expr.forallE _ _ b _ => pure LBool.true + | Expr.proj _ _ _ _ => return LBool.undef + | Expr.forallE _ _ b _ => return LBool.true | Expr.mdata _ e _ => isTypeQuick e | Expr.const c lvls _ => do let constType ← inferConstType c lvls; isArrowType constType 0 | Expr.fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowType fvarType 0 @@ -368,23 +369,23 @@ partial def isTypeQuick : Expr → MetaM LBool def isType (e : Expr) : MetaM Bool := do let r ← isTypeQuick e match r with - | LBool.true => pure true - | LBool.false => pure false + | LBool.true => return true + | LBool.false => return false | LBool.undef => let type ← inferType e let type ← whnfD type match type with - | Expr.sort _ _ => pure true - | _ => pure false + | Expr.sort _ _ => return true + | _ => return false partial def isTypeFormerType (type : Expr) : MetaM Bool := do let type ← whnfD type match type with - | Expr.sort _ _ => pure true + | Expr.sort _ _ => return true | Expr.forallE n d b c => withLocalDecl' n c.binderInfo d fun fvar => isTypeFormerType (b.instantiate1 fvar) - | _ => pure false + | _ => return false /-- Return true iff `e : Sort _` or `e : (forall As, Sort _)`.