From b57508785905573084f438f76553cadd44f13c04 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Jan 2021 12:30:26 -0800 Subject: [PATCH] fix: unfold class projections when using `TransparencyMode.instances` --- src/Lean/Meta/Basic.lean | 12 ++++++------ src/Lean/Meta/WHNF.lean | 25 +++++++++++++++++++++++- src/Lean/ReducibilityAttrs.lean | 2 +- src/library/constructions/projection.cpp | 2 +- tests/lean/whnfProj.lean | 22 +++++++++++++++++++++ tests/lean/whnfProj.lean.expected.out | 8 ++++++++ 6 files changed, 62 insertions(+), 9 deletions(-) create mode 100644 tests/lean/whnfProj.lean create mode 100644 tests/lean/whnfProj.lean.expected.out diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index eaeceab52a..ac7401fc12 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -262,14 +262,14 @@ def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind let type ← mkFreshExprMVar (mkSort u) mkFreshExprMVarWithIdCore mvarId type kind userName +def getTransparency : MetaM TransparencyMode := + return (← getConfig).transparency + def shouldReduceAll : MetaM Bool := - return (← read).config.transparency == TransparencyMode.all + return (← getTransparency) == TransparencyMode.all def shouldReduceReducibleOnly : MetaM Bool := - return (← read).config.transparency == TransparencyMode.reducible - -def getTransparency : MetaM TransparencyMode := - return (← read).config.transparency + return (← getTransparency) == TransparencyMode.reducible def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do let mctx ← getMCtx @@ -432,7 +432,7 @@ def getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do return none private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) := do - match (← read).config.transparency with + match (← getTransparency) with | TransparencyMode.all => return some info | TransparencyMode.default => return some info | _ => diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 8aa9fc590b..03390e1786 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.ToExpr import Lean.AuxRecursor +import Lean.ProjFns import Lean.Meta.Basic import Lean.Meta.LevelDefEq import Lean.Meta.GetConst @@ -364,11 +365,33 @@ mutual | some e => whnfUntilIdRhs e | none => pure e -- failed because of symbolic argument + /-- + Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`. + Recall that that class instance projections are not marked with `[reducible]` because we want them to be + in "reducible canonical form". + -/ + private partial def unfoldProjInst (e : Expr) : MetaM (Option Expr) := do + if (← getTransparency) != TransparencyMode.instances then + return none + else + match e.getAppFn with + | Expr.const declName .. => + match (← getProjectionFnInfo? declName) with + | some { fromClass := true, .. } => + match (← withDefault <| unfoldDefinition? e) with + | none => return none + | some e => + match (← reduceProj? e.getAppFn) with + | none => return none + | some r => return mkAppN r e.getAppArgs + | _ => return none + | _ => return none + /-- Unfold definition using "smart unfolding" if possible. -/ partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) := match e with | Expr.app f _ _ => - matchConstAux f.getAppFn (fun _ => pure none) fun fInfo fLvls => do + matchConstAux f.getAppFn (fun _ => unfoldProjInst e) fun fInfo fLvls => do if fInfo.lparams.length != fLvls.length then return none else diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 88fc0956c7..6545f7c83e 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -9,7 +9,7 @@ namespace Lean inductive ReducibilityStatus where | reducible | semireducible | irreducible - deriving Inhabited + deriving Inhabited, Repr builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ← registerEnumAttributes `reducibility diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 850ba28f9b..c04e5ef422 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -98,7 +98,7 @@ environment mk_projections(environment const & env, name const & n, buffer expr proj_val = mk_proj(n, i, c); proj_val = lctx.mk_lambda(proj_args, proj_val); declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val, - reducibility_hints::mk_abbreviation()); + reducibility_hints::mk_abbreviation()); new_env = new_env.add(new_d); if (!inst_implicit) new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); diff --git a/tests/lean/whnfProj.lean b/tests/lean/whnfProj.lean new file mode 100644 index 0000000000..24699be17a --- /dev/null +++ b/tests/lean/whnfProj.lean @@ -0,0 +1,22 @@ +import Lean + +def h (x : Nat) := x +def f (x : Nat) := x + 1 +def g (x : Nat) := (x, x+1).fst + + +open Lean +open Lean.Meta + +def tst (declName : Name) : MetaM Unit := do + let c ← getConstInfo declName + lambdaTelescope c.value! fun _ b => do + trace[Meta.debug]! "1. {b}" + trace[Meta.debug]! "2. {← withReducible <| whnf b}" + trace[Meta.debug]! "3. {← withReducibleAndInstances <| whnf b}" + trace[Meta.debug]! "4. {← withDefault <| whnf b}" + pure () + +set_option trace.Meta.debug true +#eval tst `f +#eval tst `g diff --git a/tests/lean/whnfProj.lean.expected.out b/tests/lean/whnfProj.lean.expected.out new file mode 100644 index 0000000000..501a9f3742 --- /dev/null +++ b/tests/lean/whnfProj.lean.expected.out @@ -0,0 +1,8 @@ +[Meta.debug] 1. x + 1 +[Meta.debug] 2. x + 1 +[Meta.debug] 3. Nat.add x 1 +[Meta.debug] 4. Nat.succ (Nat.add x 0) +[Meta.debug] 1. (x, x + 1).fst +[Meta.debug] 2. x +[Meta.debug] 3. x +[Meta.debug] 4. x