From 3af65381bda109ad4e26c865ebc68613c1aaac03 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Nov 2019 20:25:29 -0800 Subject: [PATCH] feat: add `isPropQuick` It is used to speedup `isProp`. --- library/Init/Lean/LBool.lean | 12 +++++ library/Init/Lean/Meta/Default.lean | 2 +- library/Init/Lean/Meta/FunInfo.lean | 2 +- library/Init/Lean/Meta/InferType.lean | 78 ++++++++++++++++++++++++--- tests/lean/run/meta1.lean | 34 ++++++++++++ 5 files changed, 118 insertions(+), 10 deletions(-) diff --git a/library/Init/Lean/LBool.lean b/library/Init/Lean/LBool.lean index ee3068833b..6f7b929581 100644 --- a/library/Init/Lean/LBool.lean +++ b/library/Init/Lean/LBool.lean @@ -22,6 +22,18 @@ def neg : LBool → LBool | false => true | undef => undef +def and : LBool → LBool → LBool +| true, b => b +| a, _ => a + +def beq : LBool → LBool → Bool +| true, true => Bool.true +| false, false => Bool.true +| undef, undef => Bool.true +| _, _ => Bool.false + +instance : HasBeq LBool := ⟨beq⟩ + def toString : LBool → String | true => "true" | false => "false" diff --git a/library/Init/Lean/Meta/Default.lean b/library/Init/Lean/Meta/Default.lean index 4fb581bbf7..a6c17238f5 100644 --- a/library/Init/Lean/Meta/Default.lean +++ b/library/Init/Lean/Meta/Default.lean @@ -53,7 +53,7 @@ exprToBool <$> auxFixpoint isDefEqOp e₁ e₂ /- END OF BIG HACK -/ /- =========================================== -/ -def isProp (e : Expr) : MetaM Bool := +def isProp (e : Expr) : MetaM LBool := isPropAux whnf e def getFunInfo (fn : Expr) : MetaM FunInfo := diff --git a/library/Init/Lean/Meta/FunInfo.lean b/library/Init/Lean/Meta/FunInfo.lean index 7c9123e4f8..7f076082b9 100644 --- a/library/Init/Lean/Meta/FunInfo.lean +++ b/library/Init/Lean/Meta/FunInfo.lean @@ -68,7 +68,7 @@ checkFunInfoCache fn maxArgs? $ do let pinfo := updateHasFwdDeps pinfo backDeps; pure $ pinfo.push { backDeps := backDeps, - prop := prop, + prop := prop == LBool.true, implicit := decl.binderInfo == BinderInfo.implicit, instImplicit := decl.binderInfo == BinderInfo.instImplicit }) #[]; diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean index b8ee84f45a..6a54de6e46 100644 --- a/library/Init/Lean/Meta/InferType.lean +++ b/library/Init/Lean/Meta/InferType.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Lean.LBool import Init.Lean.Meta.Basic namespace Lean @@ -166,14 +167,75 @@ do s ← get; (e : Expr) : MetaM Expr := inferTypeAuxAux (fun e => usingTransparency TransparencyMode.all $ whnf e) e -@[specialize] def isPropAux - (whnf : Expr → MetaM Expr) - (e : Expr) : MetaM Bool := -do type ← inferTypeAux whnf e; - type ← whnf type; - match type with - | Expr.sort Level.zero => pure true - | _ => pure false +/-- + Return `LBool.true` if given level is always equivalent to universe level zero. + If the given level contains a metavariable, the result may be `LBool.undef` since + it depends on metavariable assignment. + + It is used to implement `isProp`. -/ +private def isAlwaysZero : Level → LBool +| Level.zero => LBool.true +| Level.mvar _ => LBool.undef +| Level.param _ => LBool.false +| Level.succ _ => LBool.false +| Level.max u v => (isAlwaysZero u).and (isAlwaysZero v) +| Level.imax _ u => isAlwaysZero u + +/-- + `isArrowProp type n` is an "approximate" predicate which returns `LBool.true` + if `type` is of the form `A_1 -> ... -> A_n -> Prop`. + Remark: `type` can be a dependent arrow. -/ +@[specialize] private partial def isArrowProp : Expr → Nat → MetaM LBool +| Expr.sort u, 0 => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u +| Expr.forallE _ _ _ _, 0 => pure 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 + +/-- + `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true` + if `f` applied to `n` arguments is a proposition. -/ +@[specialize] private partial def isPropQuickApp : Expr → Nat → MetaM LBool +| Expr.const c lvls, arity => do constType ← inferConstType c lvls; isArrowProp constType arity +| Expr.fvar fvarId, arity => do fvarType ← inferFVarType fvarId; isArrowProp fvarType arity +| Expr.mvar mvarId, arity => do mvarType ← inferMVarType mvarId; isArrowProp mvarType arity +| 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 _ _ _ b, arity+1 => isPropQuickApp b arity +| _, _ => pure LBool.undef + +/-- + `isPropQuick e` is an "approximate" predicate which returns `LBool.true` + if `e` is a proposition. -/ +@[specialize] private 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.letE _ _ _ b => isPropQuick b +| Expr.proj _ _ _ => pure LBool.undef +| Expr.forallE _ _ _ b => isPropQuick b +| Expr.mdata _ e => isPropQuick e +| Expr.const c lvls => do constType ← inferConstType c lvls; isArrowProp constType 0 +| Expr.fvar fvarId => do fvarType ← inferFVarType fvarId; isArrowProp fvarType 0 +| Expr.mvar mvarId => do mvarType ← inferMVarType mvarId; isArrowProp mvarType 0 +| Expr.app f _ => isPropQuickApp f 1 + +@[specialize] def isPropAux (whnf : Expr → MetaM Expr) (e : Expr) : MetaM LBool := +do r ← isPropQuick e; + match r with + | LBool.true => pure LBool.true + | LBool.false => pure LBool.false + | LBool.undef => do + -- dbgTrace ("PropQuick failed " ++ toString e); + type ← inferTypeAux whnf e; + type ← (fun e => usingTransparency TransparencyMode.all $ whnf e) type; + match type with + | Expr.sort u => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u + | _ => pure LBool.false end Meta end Lean diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean index 0ead3f654a..772593f633 100644 --- a/tests/lean/run/meta1.lean +++ b/tests/lean/run/meta1.lean @@ -14,6 +14,12 @@ do env ← importModules mods; | EStateM.Result.ok type s => IO.println (toString e ++ " ==> " ++ toString type) | EStateM.Result.error err _ => throw (IO.userError (toString err)) +def tstIsProp (mods : List Name) (e : Expr) : IO Unit := +do env ← importModules mods; + match isProp e {} { env := env } with + | EStateM.Result.ok b s => IO.println (toString e ++ ", isProp: " ++ toString b) + | EStateM.Result.error err _ => throw (IO.userError (toString err)) + def t1 : Expr := let map := Expr.const `List.map [Level.one, Level.one]; let nat := Expr.const `Nat []; @@ -105,3 +111,31 @@ Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr #eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited []))) #eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited [])) #eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited []))) + +def t10 : Expr := +let nat := Expr.const `Nat []; +let refl := Expr.app (Expr.const `Eq.refl [Level.one]) nat; +Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0)) + +#eval tstInferType [`Init.Core] t10 +#eval tstIsProp [`Init.Core] t10 + +#eval tstIsProp [`Init.Core] (mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const `True []]) + +#eval tstIsProp [`Init.Core] (Expr.const `And []) + +-- Example where isPropQuick fails +#eval tstIsProp [`Init.Core] (mkApp (Expr.const `id [Level.zero]) #[Expr.sort Level.zero, mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const + `True []]]) + +#eval tstIsProp [`Init.Core] (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)]) + +#eval tstIsProp [`Init.Core] $ + Expr.forallE `x BinderInfo.default (Expr.const `Nat []) + (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]) + +#eval tstIsProp [`Init.Core] $ + Expr.app + (Expr.lam `x BinderInfo.default (Expr.const `Nat []) + (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])) + (Expr.lit (Literal.natVal 0))