chore: style
This commit is contained in:
Leonardo de Moura
parent
e04ad112b2
commit
622995b2c7
1 changed files with 52 additions and 51 deletions
|
|
@ -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 _)`.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue