From dbf5366704d153b57107f64b317889254cd926ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Apr 2022 08:30:21 -0700 Subject: [PATCH] feat: ignore `{}` annotation at constructors --- src/Lean/Elab/Inductive.lean | 33 ++++++++------------- tests/lean/ctorUnivTooBig.lean.expected.out | 12 ++++---- tests/lean/match2.lean | 8 ++--- tests/lean/run/633.lean | 6 ++-- tests/lean/run/inductive1.lean | 4 +-- tests/lean/run/inductive2.lean | 9 ++---- tests/lean/run/matchGenBug.lean | 4 +-- 7 files changed, 32 insertions(+), 44 deletions(-) diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index ae7a7a4990..a4b9252dd2 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -269,6 +269,16 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C)) return replaceArrowBinderNames r binderNames[:bsPrefix.size] +/-- + Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit. +-/ +private def withExplicitToImplicit (xs : Array Expr) (k : TermElabM α) : TermElabM α := do + let mut toImplicit := #[] + for x in xs do + if (← getFVarLocalDecl x).binderInfo.isExplicit then + toImplicit := toImplicit.push (x.fvarId!, BinderInfo.implicit) + withNewBinderInfos toImplicit k + /- Elaborate constructor types. @@ -522,7 +532,7 @@ private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : T indTypes.mapM fun indType => do let type ← mkForallFVars vars indType.type let ctors ← indType.ctors.mapM fun ctor => do - let ctorType ← mkForallFVars vars ctor.type + let ctorType ← withExplicitToImplicit vars (mkForallFVars vars ctor.type) return { ctor with type := ctorType } return { indType with type := type, ctors := ctors } @@ -561,24 +571,6 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : return { ctor with type := type } return { indType with ctors := ctors } -abbrev Ctor2InferMod := Std.HashMap Name Bool - -private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod := Id.run do - let mut m := {} - for view in views do - for ctorView in view.ctors do - m := m.insert ctorView.declName ctorView.inferMod - return m - -private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : List InductiveType := - let ctor2InferMod := mkCtor2InferMod views - indTypes.map fun indType => - let ctors := indType.ctors.map fun ctor => - let inferMod := ctor2InferMod.find! ctor.name -- true if `{}` was used - let ctorType := ctor.type.inferImplicit numParams !inferMod - { ctor with type := ctorType } - { indType with ctors := ctors } - private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do let env ← getEnv let hasEq := env.contains ``Eq @@ -700,7 +692,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : Term.addLocalVarInfo views[i].declId indFVar let r := rs[i] let type ← mkForallFVars params r.type - let ctors ← elabCtors indFVars indFVar params r + let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r) indTypesArray := indTypesArray.push { name := r.view.declName, type := type, ctors := ctors : InductiveType } Term.synthesizeSyntheticMVarsNoPostponing let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars @@ -723,7 +715,6 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : | Except.error msg => throwError msg | Except.ok levelParams => do let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes - let indTypes := applyInferMod views numParams indTypes let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe Term.ensureNoUnassignedMVars decl addDecl decl diff --git a/tests/lean/ctorUnivTooBig.lean.expected.out b/tests/lean/ctorUnivTooBig.lean.expected.out index b66caa4ca7..0281650c96 100644 --- a/tests/lean/ctorUnivTooBig.lean.expected.out +++ b/tests/lean/ctorUnivTooBig.lean.expected.out @@ -17,20 +17,20 @@ at universe level it must be smaller than or equal to the inductive datatype universe level u+1 @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as) -ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'a' has type - α +ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'as' has type + List α at universe level ?u+1 it must be smaller than or equal to the inductive datatype universe level max (u+1) (v+1) -ctorUnivTooBig.lean:41:2-41:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'a' has type - α +ctorUnivTooBig.lean:41:2-41:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'as' has type + List α at universe level ?u+1 it must be smaller than or equal to the inductive datatype universe level u+2 -ctorUnivTooBig.lean:47:2-47:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'a' has type - α +ctorUnivTooBig.lean:47:2-47:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'as' has type + List α at universe level ?u+1 it must be smaller than or equal to the inductive datatype universe level diff --git a/tests/lean/match2.lean b/tests/lean/match2.lean index 1448134446..7493865ad7 100644 --- a/tests/lean/match2.lean +++ b/tests/lean/match2.lean @@ -10,10 +10,10 @@ structure Node : Type where def h1 (x : List Node) : Bool := match x with - | _ :: Node.mk 0 _ Op.mk :: _ => true - | _ => false + | _ :: Node.mk 0 _ (Op.mk _) :: _ => true + | _ => false -def mkNode (n : Nat) : Node := { id₁ := n, id₂ := n, o := Op.mk } +def mkNode (n : Nat) : Node := { id₁ := n, id₂ := n, o := Op.mk _ } #eval h1 [mkNode 1, mkNode 0, mkNode 3] #eval h1 [mkNode 1, mkNode 1, mkNode 3] @@ -53,7 +53,7 @@ def h3 {b : Bool} (x : Foo b) : Bool := def h4 (x : List Node) : Bool := match x with - | _ :: ⟨1, 1, Op.mk⟩ :: _ => true + | _ :: ⟨1, 1, Op.mk _⟩ :: _ => true | _ => false #eval h4 [mkNode 1, mkNode 0, mkNode 3] diff --git a/tests/lean/run/633.lean b/tests/lean/run/633.lean index 3772a0fec7..0b357195dd 100644 --- a/tests/lean/run/633.lean +++ b/tests/lean/run/633.lean @@ -3,8 +3,8 @@ abbrev semantics (α:Type) := StateM (List Nat) α inductive expression : Nat → Type | const : (n : Nat) → expression n -def uext {w:Nat} (x: expression w) (o:Nat) : expression w := expression.const -def eval {n : Nat} (v:expression n) : semantics (expression n) := pure expression.const +def uext {w:Nat} (x: expression w) (o:Nat) : expression w := expression.const _ +def eval {n : Nat} (v:expression n) : semantics (expression n) := pure (expression.const _) def set_overflow {w : Nat} (e : expression w) : semantics Unit := pure () structure instruction := @@ -13,7 +13,7 @@ structure instruction := def definst (mnem:String) (body: expression 8 -> semantics Unit) : instruction := { mnemonic := mnem -, patterns := ((body expression.const).run []).snd.reverse +, patterns := ((body (expression.const _)).run []).snd.reverse } def mul : instruction := Id.run <| do -- this is a "pure" do block (as in it is the Id monad) diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean index ba1d750507..e86facc334 100644 --- a/tests/lean/run/inductive1.lean +++ b/tests/lean/run/inductive1.lean @@ -15,11 +15,11 @@ universe u v variable (α : Type u) inductive A (β : Type v) -| nil {} +| nil | protected cons : α → β → A β → A β #check @A.cons -#check A.nil Nat Bool +#check A.nil (α := Nat) (β := Bool) mutual inductive isEven : Nat → Prop diff --git a/tests/lean/run/inductive2.lean b/tests/lean/run/inductive2.lean index e4d7563ec0..0e06279d29 100644 --- a/tests/lean/run/inductive2.lean +++ b/tests/lean/run/inductive2.lean @@ -1,17 +1,14 @@ - - mutual -universe u -variable (α : Type u) inductive isEvenList : List α → Prop -| nil {} : isEvenList [] +| nil (α) : isEvenList (α := α) [] | cons (h : α) {t : List α} : isOddList t → isEvenList (h::t) inductive isOddList : List α → Prop | cons (h : α) {t : List α} : isEvenList t → isOddList (h::t) end - +set_option pp.explicit true +#print isEvenList #check @isEvenList.nil #check @isEvenList.cons #check @isOddList.cons diff --git a/tests/lean/run/matchGenBug.lean b/tests/lean/run/matchGenBug.lean index 3ea995480c..5ad7b174c6 100644 --- a/tests/lean/run/matchGenBug.lean +++ b/tests/lean/run/matchGenBug.lean @@ -12,8 +12,8 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a induction as with | nil => cases h | cons b bs ih => cases h with - | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩ - | tail a b bs h => + | head bs => exact ⟨[], ⟨bs, rfl⟩⟩ + | tail b bs h => match bs, ih h with | _, ⟨s, t, rfl⟩ => exists b::s; exists t