From 988bb09aaf330a73aec0216531848179dcdf5daa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Sep 2020 09:39:11 -0700 Subject: [PATCH] feat: new `inductive` command syntax cc @Kha --- src/Lean/Elab/Inductive.lean | 37 +++++++++++++----------- tests/lean/inductive1.lean | 2 +- tests/lean/inductive1.lean.expected.out | 2 +- tests/lean/match1.lean | 2 +- tests/lean/mutualWithNamespaceMacro.lean | 14 ++++----- tests/lean/run/inductive1.lean | 16 ++++++---- 6 files changed, 41 insertions(+), 32 deletions(-) diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 7506cf31dc..ffca5a5210 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -171,7 +171,6 @@ private partial def withInductiveLocalDeclsAux {α} (namesAndTypes : Array (Name | i, indFVars => if h : i < namesAndTypes.size then do let (id, type) := namesAndTypes.get ⟨i, h⟩; - type ← instantiateForall type params; withLocalDeclD id type fun indFVar => withInductiveLocalDeclsAux (i+1) (indFVars.push indFVar) else x params indFVars @@ -191,10 +190,10 @@ let params := r0.params; withLCtx r0.lctx r0.localInsts $ withRef r0.view.ref $ withInductiveLocalDeclsAux namesAndTypes params x 0 #[] -private def isInductiveFamily (indFVar : Expr) : TermElabM Bool := do +private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do indFVarType ← inferType indFVar; -indFVarType ← whnf indFVarType; -pure !indFVarType.isSort +forallTelescopeReducing indFVarType fun xs _ => + pure $ xs.size > numParams /- Elaborate constructor types. @@ -205,14 +204,14 @@ pure !indFVarType.isSort - Universe constraints (the kernel checks for it). -/ private def elabCtors (indFVar : Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) := withRef r.view.ref do -indFamily ← isInductiveFamily indFVar; +indFamily ← isInductiveFamily params.size indFVar; r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getArgs fun ctorParams => withRef ctorView.ref $ do type ← match ctorView.type? with | none => do when indFamily $ throwError "constructor resulting type must be specified in inductive family declaration"; - pure indFVar + pure (mkAppN indFVar params) | some ctorType => do { type ← Term.elabTerm ctorType none; resultingType ← getResultingType type; @@ -328,7 +327,7 @@ pure $ indTypes.map fun indType => private def traceIndTypes (indTypes : List InductiveType) : TermElabM Unit := indTypes.forM fun indType => - indType.ctors.forM fun ctor => _root_.dbgTrace (" >> " ++ toString ctor.name ++ " : " ++ toString ctor.type) fun _ => pure () + indType.ctors.forM fun ctor => IO.println (" >> " ++ toString ctor.name ++ " : " ++ toString ctor.type) private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do used ← indTypes.foldlM @@ -370,17 +369,20 @@ views.size.fold m.insert indFVar (mkConst view.declName levelParams)) {} -private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) (numParams : Nat) (indTypes : List InductiveType) - : TermElabM (List InductiveType) := -withRef (views.get! 0).ref $ +/- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration, + and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/ +private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) + (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := let indFVar2Const := mkIndFVar2Const views indFVars levelNames; indTypes.mapM fun indType => do ctors ← indType.ctors.mapM fun ctor => do { - type ← forallBoundedTelescope ctor.type numParams fun params type => do { - let type := type.replace fun e => if !e.isFVar then none else - match indFVar2Const.find? e with - | some c => some $ mkAppN c params - | none => none; + type ← forallBoundedTelescope ctor.type numParams fun params type => do { + let type := type.replace fun e => + if !e.isFVar then + none + else match indFVar2Const.find? e with + | none => none + | some c => mkAppN c (params.extract 0 numVars); mkForallFVars params type }; pure { ctor with type := type } @@ -451,7 +453,8 @@ withRef view0.ref $ Term.withLevelNames allUserLevelNames do u ← getResultingUniverse indTypes; inferLevel ← shouldInferResultUniverse u; withUsed vars indTypes $ fun vars => do - let numParams := vars.size + numExplicitParams; + let numVars := vars.size; + let numParams := numVars + numExplicitParams; indTypes ← updateParams vars indTypes; indTypes ← levelMVarToParam indTypes; indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else pure indTypes; @@ -459,7 +462,7 @@ withRef view0.ref $ Term.withLevelNames allUserLevelNames do match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with | Except.error msg => throwError msg | Except.ok levelParams => do - indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numParams indTypes; + 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; diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean index fd88603a1b..c368c6d88c 100644 --- a/tests/lean/inductive1.lean +++ b/tests/lean/inductive1.lean @@ -112,7 +112,7 @@ inductive T1 : Nat → Type inductive A (α : Type u) (β : Type v) | nil {} -| protected cons : α → β → A → A +| protected cons : α → β → A α β → A α β open A #check cons -- unknown `cons`, it is protected diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index e0f01f5b87..6ae05409a9 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -27,4 +27,4 @@ inductive1.lean:105:0: error: unexpected constructor resulting type, type expect inductive1.lean:108:0: error: unexpected constructor resulting type Nat inductive1.lean:118:7: error: unknown identifier 'cons' -(sorryAx ?m.134) : ?m.134 +(sorryAx ?m.139) : ?m.139 diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean index b17676186d..ab33a9ba05 100644 --- a/tests/lean/match1.lean +++ b/tests/lean/match1.lean @@ -36,7 +36,7 @@ match x with #print "---- inv" inductive Image {α β : Type} (f : α → β) : β → Type -| mk (a : α) : Image (f a) +| mk (a : α) : Image f (f a) def mkImage {α β : Type} (f : α → β) (a : α) : Image f (f a) := Image.mk a diff --git a/tests/lean/mutualWithNamespaceMacro.lean b/tests/lean/mutualWithNamespaceMacro.lean index 8086780eeb..3d87549a7f 100644 --- a/tests/lean/mutualWithNamespaceMacro.lean +++ b/tests/lean/mutualWithNamespaceMacro.lean @@ -4,22 +4,22 @@ mutual inductive Foo.Lst (α : Type) | nil : Lst -| cons : Tree → Lst → Lst +| cons : Tree α → Lst α → Lst α inductive Boo.Tree (α : Type) -- conflicting namespace -| leaf : Tree -| node : Lst → Tree +| leaf : Tree α +| node : Lst α → Tree α end mutual inductive Foo.Lst (α : Type) -| nil : Lst -| cons : Tree → Lst → Lst +| nil : Lst α +| cons : Tree α → Lst α → Lst α inductive Foo.Tree (α : Type) -| leaf : Tree -| node : Lst → Tree +| leaf : Tree α +| node : Lst α → Tree α end diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean index 28bfd9be19..7cdf2252a1 100644 --- a/tests/lean/run/inductive1.lean +++ b/tests/lean/run/inductive1.lean @@ -2,14 +2,14 @@ new_frontend inductive L1.{u} (α : Type u) | nil -| cons : α → L1 → L1 +| cons : α → L1 α → L1 α #check L1 #check @L1.cons inductive L2.{u} (α : Type u) | nil -| cons (head : α) (tail : L2) +| cons (head : α) (tail : L2 α) #check @L2.cons @@ -18,7 +18,7 @@ variable (α : Type u) inductive A (β : Type v) | nil {} -| protected cons : α → β → A → A +| protected cons : α → β → A β → A β #check @A.cons #check A.nil Nat Bool @@ -37,8 +37,8 @@ end #check @isEven.rec inductive V (α : Type _) : Nat → Type _ -| nil : V 0 -| cons {n : Nat} : α → V n → V (n+1) +| nil : V α 0 +| cons {n : Nat} : α → V α n → V α (n+1) #check @V.nil #check @V.cons @@ -65,3 +65,9 @@ inductive T1 | mk : β → β → T1 #check @T1.mk + + +inductive MyEq {α : Type} (a : α) : α → Prop +| refl : MyEq a a + +#check @MyEq.refl