From ea0fda39bc32fea7b827544d74595cfe857a09c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jan 2021 15:11:55 -0800 Subject: [PATCH] chore: `Declaration.lean` naming convention `Declaration.lean` was one of the first Lean 4 files, and was still using an old naming convention. cc @Kha --- src/Lean/Declaration.lean | 74 +++++++++---------- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 2 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Declaration.lean | 8 +- src/Lean/Elab/Deriving/BEq.lean | 10 +-- src/Lean/Elab/Deriving/DecEq.lean | 8 +- src/Lean/Elab/Deriving/Inhabited.lean | 10 +-- src/Lean/Elab/Deriving/Repr.lean | 10 +-- src/Lean/Elab/Deriving/Util.lean | 6 +- src/Lean/Elab/Match.lean | 18 ++--- src/Lean/Elab/MutualDef.lean | 28 +++---- src/Lean/Elab/PreDefinition/Basic.lean | 46 ++++++------ src/Lean/Elab/PreDefinition/Structural.lean | 4 +- src/Lean/Elab/Print.lean | 46 ++++++------ src/Lean/Elab/StructInst.lean | 10 +-- src/Lean/Elab/Term.lean | 2 +- src/Lean/KeyedDeclsAttribute.lean | 2 +- src/Lean/Meta/Closure.lean | 12 +-- src/Lean/Meta/InferType.lean | 2 +- src/Lean/Meta/Match/Match.lean | 4 +- src/Lean/Meta/RecursorInfo.lean | 14 ++-- src/Lean/Meta/SizeOf.lean | 30 ++++---- src/Lean/Meta/Tactic/Cases.lean | 16 ++-- src/Lean/Meta/Tactic/Constructor.lean | 6 +- src/Lean/Meta/Tactic/Injection.lean | 2 +- src/Lean/Meta/WHNF.lean | 12 +-- src/Lean/Parser/Extension.lean | 2 +- src/Lean/ParserCompiler.lean | 2 +- .../PrettyPrinter/Delaborator/Builtins.lean | 6 +- src/Lean/Structure.lean | 30 ++++---- src/Lean/Util/Recognizers.lean | 4 +- tests/lean/run/depElim1.lean | 6 +- tests/lean/run/meta2.lean | 3 +- tests/lean/run/toExpr.lean | 12 +-- 35 files changed, 225 insertions(+), 226 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 7e17bcfec3..b42eff71ec 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -60,7 +60,7 @@ end ReducibilityHints /-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `InductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`. -/ structure ConstantVal where name : Name - lparams : List Name + levelParams : List Name type : Expr deriving Inhabited @@ -68,9 +68,9 @@ structure AxiomVal extends ConstantVal where isUnsafe : Bool @[export lean_mk_axiom_val] -def mkAxiomValEx (name : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : AxiomVal := { +def mkAxiomValEx (name : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : AxiomVal := { name := name, - lparams := lparams, + levelParams := levelParams, type := type, isUnsafe := isUnsafe } @@ -89,9 +89,9 @@ structure DefinitionVal extends ConstantVal where deriving Inhabited @[export lean_mk_definition_val] -def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := { +def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := { name := name, - lparams := lparams, + levelParams := levelParams, type := type, value := val, hints := hints, @@ -110,9 +110,9 @@ structure OpaqueVal extends ConstantVal where isUnsafe : Bool @[export lean_mk_opaque_val] -def mkOpaqueValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := { +def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := { name := name, - lparams := lparams, + levelParams := levelParams, type := type, value := val, isUnsafe := isUnsafe @@ -179,8 +179,8 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool A series of checks are performed by the kernel to check whether a `inductiveDecls` is valid or not. -/ structure InductiveVal extends ConstantVal where - nparams : Nat -- Number of parameters - nindices : Nat -- Number of indices + numParams : Nat -- Number of parameters + numIndices : Nat -- Number of indices all : List Name -- List of all (including this one) inductive datatypes in the mutual declaration containing this one ctors : List Name -- List of all constructors for this inductive datatype isRec : Bool -- `true` Iff it is recursive @@ -190,13 +190,13 @@ structure InductiveVal extends ConstantVal where deriving Inhabited @[export lean_mk_inductive_val] -def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat) +def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numParams numIndices : Nat) (all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := { name := name - lparams := lparams + levelParams := levelParams type := type - nparams := nparams - nindices := nindices + numParams := numParams + numIndices := numIndices all := all ctors := ctors isRec := isRec @@ -213,22 +213,22 @@ def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams def InductiveVal.nctors (v : InductiveVal) : Nat := v.ctors.length structure ConstructorVal extends ConstantVal where - induct : Name -- Inductive Type this Constructor is a member of - cidx : Nat -- Constructor index (i.e., Position in the inductive declaration) - nparams : Nat -- Number of parameters in inductive datatype `induct` - nfields : Nat -- Number of fields (i.e., arity - nparams) + induct : Name -- Inductive Type this Constructor is a member of + cidx : Nat -- Constructor index (i.e., Position in the inductive declaration) + numParams : Nat -- Number of parameters in inductive datatype `induct` + numFields : Nat -- Number of fields (i.e., arity - nparams) isUnsafe : Bool deriving Inhabited @[export lean_mk_constructor_val] -def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct : Name) (cidx nparams nfields : Nat) (isUnsafe : Bool) : ConstructorVal := { +def mkConstructorValEx (name : Name) (levelParams : List Name) (type : Expr) (induct : Name) (cidx numParams numFields : Nat) (isUnsafe : Bool) : ConstructorVal := { name := name, - lparams := lparams, + levelParams := levelParams, type := type, induct := induct, cidx := cidx, - nparams := nparams, - nfields := nfields, + numParams := numParams, + numFields := numFields, isUnsafe := isUnsafe } @@ -241,33 +241,33 @@ structure RecursorRule where rhs : Expr -- Right hand side of the reduction rule structure RecursorVal extends ConstantVal where - all : List Name -- List of all inductive datatypes in the mutual declaration that generated this recursor - nparams : Nat -- Number of parameters - nindices : Nat -- Number of indices - nmotives : Nat -- Number of motives - nminors : Nat -- Number of minor premises - rules : List RecursorRule -- A reduction for each Constructor - k : Bool -- It supports K-like reduction + all : List Name -- List of all inductive datatypes in the mutual declaration that generated this recursor + numParams : Nat -- Number of parameters + numIndices : Nat -- Number of indices + numMotives : Nat -- Number of motives + numMinors : Nat -- Number of minor premises + rules : List RecursorRule -- A reduction for each Constructor + k : Bool -- It supports K-like reduction isUnsafe : Bool @[export lean_mk_recursor_val] -def mkRecursorValEx (name : Name) (lparams : List Name) (type : Expr) (all : List Name) (nparams nindices nmotives nminors : Nat) +def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat) (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := { - name := name, lparams := lparams, type := type, all := all, nparams := nparams, nindices := nindices, - nmotives := nmotives, nminors := nminors, rules := rules, k := k, isUnsafe := isUnsafe + name := name, levelParams := levelParams, type := type, all := all, numParams := numParams, numIndices := numIndices, + numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe } @[export lean_recursor_k] def RecursorVal.kEx (v : RecursorVal) : Bool := v.k @[export lean_recursor_is_unsafe] def RecursorVal.isUnsafeEx (v : RecursorVal) : Bool := v.isUnsafe def RecursorVal.getMajorIdx (v : RecursorVal) : Nat := - v.nparams + v.nmotives + v.nminors + v.nindices + v.numParams + v.numMotives + v.numMinors + v.numIndices def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat := - v.nparams + v.nmotives + v.nminors + v.numParams + v.numMotives + v.numMinors def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat := - v.nparams + v.nmotives + v.numParams + v.numMotives def RecursorVal.getInduct (v : RecursorVal) : Name := v.name.getPrefix @@ -282,8 +282,8 @@ structure QuotVal extends ConstantVal where kind : QuotKind @[export lean_mk_quot_val] -def mkQuotValEx (name : Name) (lparams : List Name) (type : Expr) (kind : QuotKind) : QuotVal := { - name := name, lparams := lparams, type := type, kind := kind +def mkQuotValEx (name : Name) (levelParams : List Name) (type : Expr) (kind : QuotKind) : QuotVal := { + name := name, levelParams := levelParams, type := type, kind := kind } @[export lean_quot_val_kind] def QuotVal.kindEx (v : QuotVal) : QuotKind := v.kind @@ -325,7 +325,7 @@ def name (d : ConstantInfo) : Name := d.toConstantVal.name def lparams (d : ConstantInfo) : List Name := - d.toConstantVal.lparams + d.toConstantVal.levelParams def type (d : ConstantInfo) : Expr := d.toConstantVal.type diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 06d6f4e237..4f5c6453a9 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -65,7 +65,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name := let val ← elabTerm tactic type let val ← instantiateMVars val trace[Elab.autoParam]! val - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } addDecl decl compileDecl decl diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 4a2cf0fd7e..6dc8378a4b 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -93,7 +93,7 @@ private def elabTParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax private def mkNativeReflAuxDecl (type val : Expr) : TermElabM Name := do let auxName ← mkAuxName `_nativeRefl let decl := Declaration.defnDecl { - name := auxName, lparams := [], type := type, value := val, + name := auxName, levelParams := [], type := type, value := val, hints := ReducibilityHints.abbrev, safety := DefinitionSafety.safe } diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index fdf7494d2e..2ffd3a1bb2 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -598,7 +598,7 @@ unsafe def elabEvalUnsafe : CommandElab let addAndCompile (value : Expr) : TermElabM Unit := do let type ← inferType value let decl := Declaration.defnDecl { - name := n, lparams := [], type := type, + name := n, levelParams := [], type := type, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.unsafe } diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 1003aaeb84..14a6a54aa6 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -74,10 +74,10 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do | Except.error msg => throwErrorAt stx msg | Except.ok levelParams => let decl := Declaration.axiomDecl { - name := declName, - lparams := levelParams, - type := type, - isUnsafe := modifiers.isUnsafe + name := declName, + levelParams := levelParams, + type := type, + isUnsafe := modifiers.isUnsafe } Term.ensureNoUnassignedMVars decl addDecl decl diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 09abe7097a..58105bb064 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -22,7 +22,7 @@ where mkElseAlt : TermElabM Syntax := do let mut patterns := #[] -- add `_` pattern for indices - for i in [:indVal.nindices] do + for i in [:indVal.numIndices] do patterns := patterns.push (← `(_)) patterns := patterns.push (← `(_)) patterns := patterns.push (← `(_)) @@ -37,17 +37,17 @@ where let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies let mut patterns := #[] -- add `_` pattern for indices - for i in [:indVal.nindices] do + for i in [:indVal.numIndices] do patterns := patterns.push (← `(_)) let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] let mut rhs ← `(true) -- add `_` for inductive parameters, they are inaccessible - for i in [:indVal.nparams] do + for i in [:indVal.numParams] do ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) - for i in [:ctorInfo.nfields] do - let x := xs[indVal.nparams + i] + for i in [:ctorInfo.numFields] do + let x := xs[indVal.numParams + i] if type.containsFVar x.fvarId! then -- If resulting type depends on this field, we don't need to compare ctorArgs1 := ctorArgs1.push (← `(_)) diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index dc2d41402c..1f661652ee 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -41,7 +41,7 @@ where for ctorName₂ in indVal.ctors do let mut patterns := #[] -- add `_` pattern for indices - for i in [:indVal.nindices] do + for i in [:indVal.numIndices] do patterns := patterns.push (← `(_)) if ctorName₁ == ctorName₂ then let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do @@ -50,12 +50,12 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] -- add `_` for inductive parameters, they are inaccessible - for i in [:indVal.nparams] do + for i in [:indVal.numParams] do ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) let mut todo := #[] - for i in [:ctorInfo.nfields] do - let x := xs[indVal.nparams + i] + for i in [:ctorInfo.numFields] do + let x := xs[indVal.numParams + i] if type.containsFVar x.fvarId! then -- If resulting type depends on this field, we don't need to compare ctorArgs1 := ctorArgs1.push (← `(_)) diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index c28b8982ac..80083a91a7 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -63,7 +63,7 @@ where let ctorVal ← getConstInfoCtor ctorName let mut indArgs := #[] let mut binders := #[] - for i in [:indVal.nparams + indVal.nindices] do + for i in [:indVal.numParams + indVal.numIndices] do let arg := mkIdent (← mkFreshUserName `a) indArgs := indArgs.push arg let binder ← `(implicitBinderF| { $arg:ident }) @@ -73,9 +73,9 @@ where binders := binders.push binder let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*)) let mut ctorArgs := #[] - for i in [:ctorVal.nparams] do + for i in [:ctorVal.numParams] do ctorArgs := ctorArgs.push (← `(_)) - for i in [:ctorVal.nfields] do + for i in [:ctorVal.numFields] do ctorArgs := ctorArgs.push (← `(arbitrary)) let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs:ident*⟩) `(instance $binders:explicitBinder* : $type := $val) @@ -83,10 +83,10 @@ where mkInstanceCmd? : TermElabM (Option Syntax) := do let ctorVal ← getConstInfoCtor ctorName forallTelescopeReducing ctorVal.type fun xs _ => - addLocalInstancesForParams xs[:ctorVal.nparams] fun localInst2Index => do + addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do let mut usedInstIdxs := {} let mut ok := true - for i in [ctorVal.nparams:xs.size] do + for i in [ctorVal.numParams:xs.size] do let x := xs[i] let instType ← mkAppM `Inhabited #[(← inferType x)] trace[Elab.Deriving.inhabited]! "checking {instType} for '{ctorName}'" diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index a59f2b942a..e83b60bbb8 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -23,7 +23,7 @@ def mkReprHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := d def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do let ctorVal ← getConstInfoCtor indVal.ctors.head! let fieldNames ← getStructureFields (← getEnv) indVal.name - let numParams := indVal.nparams + let numParams := indVal.numParams let target := mkIdent header.targetNames[0] forallTelescopeReducing ctorVal.type fun xs _ => do let mut fields : Syntax ← `(Format.nil) @@ -56,16 +56,16 @@ where let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do let mut patterns := #[] -- add `_` pattern for indices - for i in [:indVal.nindices] do + for i in [:indVal.numIndices] do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] let mut rhs := Syntax.mkStrLit (toString ctorInfo.name) let mut rhs ← `(Format.text $rhs) -- add `_` for inductive parameters, they are inaccessible - for i in [:indVal.nparams] do + for i in [:indVal.numParams] do ctorArgs := ctorArgs.push (← `(_)) - for i in [:ctorInfo.nfields] do - let x := xs[indVal.nparams + i] + for i in [:ctorInfo.numFields] do + let x := xs[indVal.numParams + i] let a := mkIdent (← mkFreshUserName `a) ctorArgs := ctorArgs.push a if (← inferType x).isAppOf indVal.name then diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 95e71dc551..3c4ef885aa 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -32,7 +32,7 @@ def mkImplicitBinders (argNames : Array Name) : TermElabM (Array Syntax) := `(implicitBinderF| { $(mkIdent argName) }) def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) := - forallBoundedTelescope indVal.type indVal.nparams fun xs _ => do + forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do let mut binders := #[] for i in [:xs.size] do try @@ -75,7 +75,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array let indVal := ctx.typeInfos[i] let auxFunName := ctx.auxFunNames[i] let currArgNames ← mkInductArgNames indVal - let numParams := indVal.nparams + let numParams := indVal.numParams let currIndices := currArgNames[numParams:] let binders ← mkImplicitBinders currIndices let argNamesNew := argNames[:numParams] ++ currIndices @@ -134,7 +134,7 @@ def mkHeader (ctx : Context) (className : Name) (arity : Nat) (indVal : Inductiv def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array Syntax) := do let mut discrs := #[] -- add indices - for argName in header.argNames[indVal.nparams:] do + for argName in header.argNames[indVal.numParams:] do discrs := discrs.push (← mkDiscr argName) return discrs ++ (← header.targetNames.mapM mkDiscr) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index af6673f5cc..78050e0bed 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -202,7 +202,7 @@ private def throwCtorExpected {α} : M α := throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected" private def getNumExplicitCtorParams (ctorVal : ConstructorVal) : TermElabM Nat := - forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ => do + forallBoundedTelescope ctorVal.type ctorVal.numParams fun ps _ => do let mut result := 0 for p in ps do let localDecl ← getLocalDecl p.fvarId! @@ -250,7 +250,7 @@ private def finalize (ctx : Context) : M Syntax := do private def isNextArgAccessible (ctx : Context) : Bool := let i := ctx.paramDeclIdx match ctx.ctorVal? with - | some ctorVal => i ≥ ctorVal.nparams -- For constructor applications only fields are accessible + | some ctorVal => i ≥ ctorVal.numParams -- For constructor applications only fields are accessible | none => if h : i < ctx.paramDecls.size then -- For `[matchPattern]` applications, only explicit parameters are accessible. @@ -649,10 +649,10 @@ partial def main (e : Expr) : M Pattern := do main newE else matchConstCtor e.getAppFn (fun _ => throwInvalidPattern e) fun v us => do let args := e.getAppArgs - unless args.size == v.nparams + v.nfields do + unless args.size == v.numParams + v.numFields do throwInvalidPattern e - let params := args.extract 0 v.nparams - let fields := args.extract v.nparams args.size + let params := args.extract 0 v.numParams + let fields := args.extract v.numParams args.size let fields ← fields.mapM main pure $ Pattern.ctor v.name us params.toList fields.toList @@ -916,8 +916,8 @@ where elabMatchCore stx expectedType? @[builtinInit] private def regTraceClasses : IO Unit := do -registerTraceClass `Elab.match; -pure () + registerTraceClass `Elab.match; + pure () -- parser!:leadPrec "nomatch " >> termParser @[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => @@ -928,6 +928,4 @@ pure () elabMatchAux #[discr] #[] mkNullNode expectedType | _ => throwUnsupportedSyntax -end Term -end Elab -end Lean +end Lean.Elab.Term diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 4d68cccc1e..7c672f8e42 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -527,13 +527,13 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea let val ← mkLambdaFVars sectionVars mainVals[i] let type ← mkForallFVars sectionVars header.type return preDefs.push { - ref := getDeclarationSelectionRef header.ref - kind := header.kind - declName := header.declName - lparams := [], -- we set it later - modifiers := header.modifiers - type := type - value := val + ref := getDeclarationSelectionRef header.ref + kind := header.kind + declName := header.declName + levelParams := [], -- we set it later + modifiers := header.modifiers + type := type + value := val } def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : Array PreDefinition := @@ -541,13 +541,13 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo let type := Closure.mkForall c.localDecls c.toLift.type let val := Closure.mkLambda c.localDecls c.toLift.val preDefs.push { - ref := c.ref - kind := kind - declName := c.toLift.declName - lparams := [] -- we set it later - modifiers := { modifiers with attrs := c.toLift.attrs } - type := type - value := val + ref := c.ref + kind := kind + declName := c.toLift.declName + levelParams := [] -- we set it later + modifiers := { modifiers with attrs := c.toLift.attrs } + type := type + value := val } def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind := diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index fa811895d6..058565b1c1 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -18,13 +18,13 @@ A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies. -/ structure PreDefinition where - ref : Syntax - kind : DefKind - lparams : List Name - modifiers : Modifiers - declName : Name - type : Expr - value : Expr + ref : Syntax + kind : DefKind + levelParams : List Name + modifiers : Modifiers + declName : Name + type : Expr + value : Expr deriving Inhabited def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) := @@ -61,17 +61,17 @@ private def shareCommon (preDefs : Array PreDefinition) : Array PreDefinition := def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do let preDefs := shareCommon preDefs - let lparams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames - let us := lparams.map mkLevelParam + let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames + let us := levelParams.map mkLevelParam let fixExpr (e : Expr) : Expr := e.replace fun c => match c with | Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none | _ => none pure $ preDefs.map fun preDef => { preDef with - type := fixExpr preDef.type, - value := fixExpr preDef.value, - lparams := lparams } + type := fixExpr preDef.type, + value := fixExpr preDef.value, + levelParams := levelParams } def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do for preDef in preDefs do @@ -87,7 +87,7 @@ def abstractNestedProofs (preDef : PreDefinition) : MetaM PreDefinition := /- Auxiliary method for (temporarily) adding pre definition as an axiom -/ def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do withRef preDef.ref do - addDecl <| Declaration.axiomDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe } + addDecl <| Declaration.axiomDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe } private def shouldGenCodeFor (preDef : PreDefinition) : Bool := !preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable @@ -100,16 +100,16 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U match preDef.kind with | DefKind.«example» => unreachable! | DefKind.«theorem» => - Declaration.thmDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value } + Declaration.thmDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value } | DefKind.«opaque» => - Declaration.opaqueDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, + Declaration.opaqueDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, isUnsafe := preDef.modifiers.isUnsafe } | DefKind.«abbrev» => - Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, + Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, hints := ReducibilityHints.«abbrev», safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe } | DefKind.«def» => - Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value, + Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1), safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe } addDecl decl @@ -127,12 +127,12 @@ def addNonRec (preDef : PreDefinition) : TermElabM Unit := do def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := withRef preDefs[0].ref do let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => { - name := preDef.declName, - lparams := preDef.lparams, - type := preDef.type, - value := preDef.value, - safety := safety, - hints := ReducibilityHints.opaque + name := preDef.declName + levelParams := preDef.levelParams + type := preDef.type + value := preDef.value + safety := safety + hints := ReducibilityHints.opaque } addDecl decl applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index 92c197c03c..87897a85f6 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -119,8 +119,8 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA loop (i+1) else let indArgs := xType.getAppArgs - let indParams := indArgs.extract 0 indInfo.nparams - let indIndices := indArgs.extract indInfo.nparams indArgs.size + let indParams := indArgs.extract 0 indInfo.numParams + let indIndices := indArgs.extract indInfo.numParams indArgs.size if !indIndices.all Expr.isFVar then orelse' (throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}") diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 8335e4ff26..254e640886 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -11,8 +11,8 @@ namespace Lean.Elab.Command private def throwUnknownId (id : Name) : CommandElabM Unit := throwError! "unknown identifier '{mkConst id}'" -private def lparamsToMessageData (lparams : List Name) : MessageData := - match lparams with +private def levelParamsToMessageData (levelParams : List Name) : MessageData := + match levelParams with | [] => "" | u::us => do let mut m := m!".\{{u}" @@ -20,7 +20,7 @@ private def lparamsToMessageData (lparams : List Name) : MessageData := m := m ++ ", " ++ u return m ++ "}" -private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do +private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do let m : MessageData := match safety with | DefinitionSafety.unsafe => "unsafe " @@ -30,26 +30,26 @@ private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : E let (m, id) := match privateToUserName? id with | some id => (m ++ "private ", id) | none => (m, id) - let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type + let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type pure m -private def mkHeader' (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := - mkHeader kind id lparams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) +private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := + mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) -private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do - let m ← mkHeader kind id lparams type safety +private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do + let m ← mkHeader kind id levelParams type safety let m := m ++ " :=" ++ Format.line ++ value logInfo m -private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do - logInfo (← mkHeader' kind id lparams type isUnsafe) +private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do + logInfo (← mkHeader' kind id levelParams type isUnsafe) -private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do - printAxiomLike "Quotient primitive" id lparams type +private def printQuot (kind : QuotKind) (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do + printAxiomLike "Quotient primitive" id levelParams type -private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr) +private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (numIndices : Nat) (type : Expr) (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do - let mut m ← mkHeader' "inductive" id lparams type isUnsafe + let mut m ← mkHeader' "inductive" id levelParams type isUnsafe m := m ++ Format.line ++ "constructors:" for ctor in ctors do let cinfo ← getConstInfo ctor @@ -58,15 +58,15 @@ private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindi private def printIdCore (id : Name) : CommandElabM Unit := do match (← getEnv).find? id with - | ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u - | ConstantInfo.defnInfo { lparams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s - | ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v - | ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u - | ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t - | ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u - | ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u - | ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } => - printInduct id us nparams nindices t ctors u + | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u + | ConstantInfo.defnInfo { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s + | ConstantInfo.thmInfo { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v + | ConstantInfo.opaqueInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u + | ConstantInfo.quotInfo { kind := kind, levelParams := us, type := t, .. } => printQuot kind id us t + | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u + | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u + | ConstantInfo.inductInfo { levelParams := us, numParams := numParams, numIndices := numIndices, type := t, ctors := ctors, isUnsafe := u, .. } => + printInduct id us numParams numIndices t ctors u | none => throwUnknownId id private def printId (id : Name) : CommandElabM Unit := do diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 1156d535f5..e2278a1d17 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -514,11 +514,11 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? discard <| isDefEq expectedType typeBody private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do - let lvls ← ctorVal.lparams.mapM fun _ => mkFreshLevelMVar - let val := Lean.mkConst ctorVal.name lvls - let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams lvls - let r ← mkCtorHeaderAux ctorVal.nparams type val #[] - propagateExpectedType r.ctorFnType ctorVal.nfields expectedType? + let us ← ctorVal.levelParams.mapM fun _ => mkFreshLevelMVar + let val := Lean.mkConst ctorVal.name us + let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams us + let r ← mkCtorHeaderAux ctorVal.numParams type val #[] + propagateExpectedType r.ctorFnType ctorVal.numFields expectedType? synthesizeAppInstMVars r.instMVars pure r diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 23d56e03f8..de019a077b 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1436,7 +1436,7 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α := unless type.isConstOf typeName do throwError! "unexpected type at evalExpr{indentExpr type}" let decl := Declaration.defnDecl { - name := name, lparams := [], type := type, + name := name, levelParams := [], type := type, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.unsafe } diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 28060870d6..045333d273 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -102,7 +102,7 @@ def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment) let name := `_regBuiltin ++ declName let type := mkApp (mkConst `IO) (mkConst `Unit) let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName] - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } match env.addAndCompile {} decl with -- TODO: pretty print error diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index b80e5ddfd0..70a54ebf2d 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -351,12 +351,12 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f let result ← Closure.mkValueTypeClosure type value zeta let env ← getEnv let decl := Declaration.defnDecl { - name := name, - lparams := result.levelParams.toList, - type := result.type, - value := result.value, - hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), - safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe + name := name, + levelParams := result.levelParams.toList, + type := result.type, + value := result.value, + hints := ReducibilityHints.regular (getMaxHeight env result.value + 1), + safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe } trace[Meta.debug]! "{name} : {result.type} := {result.value}" addDecl decl diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 60e352346e..261b96fc49 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -99,7 +99,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp let structType ← inferType e let structType ← whnf structType matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal => - let n := structVal.nparams + let n := structVal.numParams let structParams := structType.getAppArgs if n != structParams.size then failed () else do diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index b2395c6aa7..fb5dc48a4e 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -299,7 +299,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) match e.constructorApp? env with | some (ctorVal, ctorArgs) => if ctorVal.name == ctorName then - let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size + let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size let fields := fields.toList.map Pattern.inaccessible pure $ some { alt with patterns := fields ++ ps } else @@ -370,7 +370,7 @@ private def processNonVariable (p : Problem) : MetaM Problem := | Pattern.inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name | p :: _ => throwError! "failed to compile pattern matching, inaccessible pattern or constructor expected{indentD p.toMessageData}" | _ => unreachable! - let xFields := xArgs.extract ctorVal.nparams xArgs.size + let xFields := xArgs.extract ctorVal.numParams xArgs.size pure { p with alts := alts, vars := xFields.toList ++ xs } | none => let alts ← p.alts.filterMapM fun alt => match alt.patterns with diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 9b3ca0cba0..46a973e047 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -68,13 +68,13 @@ end RecursorInfo private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do let ival ← getConstInfoInduct val.getInduct - let numLParams := ival.lparams.length + let numLParams := ival.levelParams.length let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType - let univLevelPos := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos - let produceMotive := List.replicate val.nminors true - let paramsPos := (List.range val.nparams).map some - let indicesPos := (List.range val.nindices).map fun pos => val.nparams + pos - let numArgs := val.nindices + val.nparams + val.nminors + val.nmotives + 1 + let univLevelPos := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos + let produceMotive := List.replicate val.numMinors true + let paramsPos := (List.range val.numParams).map some + let indicesPos := (List.range val.numIndices).map fun pos => val.numParams + pos + let numArgs := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1 pure { recursorName := declName, typeName := val.getInduct, @@ -100,7 +100,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) pure none else do let val ← getConstInfoRec (mkRecName p) - pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives)) + pure $ some (val.numParams + val.numIndices + (if s == casesOnSuffix then 1 else val.numMotives)) | _ => pure none private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 12dc3f6b2d..37659781b9 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -32,7 +32,7 @@ where loop (i+1) (insts.push inst) else k insts -/-- +/-- Let `motiveFVars` be free variables for each motive in a kernel recursor, and `minorFVars` the free variables for a minor premise. Then, return `true` is `fvar` (an element of `minorFVars`) corresponds to a recursive field. That is, there is a free variable `minorFVar` in `minorFVars` with type `... -> motive ... fvar` where `motive` is an element of `motiveFVars`. @@ -41,7 +41,7 @@ private def isRecField (motiveFVars : Array Expr) (minorFVars : Array Expr) (fva for minorFVar in minorFVars do let found ← forallTelescopeReducing (← inferType minorFVar) fun _ type => return motiveFVars.contains type.getAppFn && type.appArg! == fvar - if found then + if found then return true return false @@ -67,7 +67,7 @@ where forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ => forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do let mut minor ← mkNumeral (mkConst ``Nat) 1 - for x in xs, x' in xs' do + for x in xs, x' in xs' do -- If `x` is a recursive field, we skip it since we use the inductive hypothesis occurring later unless (← isRecField motiveFVars xs x) do let xType ← inferType x @@ -77,28 +77,28 @@ where if ys.size > 0 then -- ignore `x` because it is a function return minor - else + else mkAdd minor x' else - try + try mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x']) catch _ => - return minor - minor ← mkLambdaFVars xs' minor - trace[Meta.sizeOf]! "minor: {minor}" + return minor + minor ← mkLambdaFVars xs' minor + trace[Meta.sizeOf]! "minor: {minor}" loop (i+1) (minors.push minor) else - k minors + k minors partial def mkSizeOfFn (recName : Name) : MetaM Unit := do trace[Meta.sizeOf]! "recName: {recName}" let recInfo : RecursorVal ← getConstInfoRec recName forallTelescopeReducing recInfo.type fun xs type => - let levelParams := recInfo.lparams.tail! -- universe parameters for declaration being defined - let params := xs[:recInfo.nparams] - let motiveFVars := xs[recInfo.nparams : recInfo.nparams + recInfo.nmotives] - let minorFVars := xs[recInfo.getFirstMinorIdx : recInfo.getFirstMinorIdx + recInfo.nminors] - let indices := xs[recInfo.getFirstIndexIdx : recInfo.getFirstIndexIdx + recInfo.nindices] + let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined + let params := xs[:recInfo.numParams] + let motiveFVars := xs[recInfo.numParams : recInfo.numParams + recInfo.numMotives] + let minorFVars := xs[recInfo.getFirstMinorIdx : recInfo.getFirstMinorIdx + recInfo.numMinors] + let indices := xs[recInfo.getFirstIndexIdx : recInfo.getFirstIndexIdx + recInfo.numIndices] let major := xs[recInfo.getMajorIdx] let nat := mkConst ``Nat mkLocalInstances params fun localInsts => @@ -106,7 +106,7 @@ partial def mkSizeOfFn (recName : Name) : MetaM Unit := do let us := levelOne :: levelParams.map mkLevelParam -- universe level parameters for `rec`-application let recFn := mkConst recName us let val := mkAppN recFn (params ++ motives) - forallBoundedTelescope (← inferType val) recInfo.nminors fun minorFVars' _ => + forallBoundedTelescope (← inferType val) recInfo.numMinors fun minorFVars' _ => mkSizeOfMinors motiveFVars minorFVars minorFVars' fun minors => do let sizeOfFnType ← mkForallFVars (params ++ localInsts ++ indices ++ #[major]) nat let val := mkAppN val (minors ++ indices ++ #[major]) diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index 3854b02ff2..0044e02f93 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -19,7 +19,7 @@ def getInductiveUniverseAndParams (type : Expr) : MetaM (List Level × Array Exp matchConstInduct type.getAppFn (fun _ => throwInductiveTypeExpected type) fun val us => let I := type.getAppFn let Iargs := type.getAppArgs - let params := Iargs.extract 0 val.nparams + let params := Iargs.extract 0 val.numParams pure (us, params) private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do @@ -89,10 +89,10 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi let fvarDecl ← getLocalDecl fvarId let type ← whnf fvarDecl.type type.withApp fun f args => matchConstInduct f (fun _ => throwTacticEx `generalizeIndices mvarId "inductive type expected") fun val _ => do - unless val.nindices > 0 do throwTacticEx `generalizeIndices mvarId "indexed inductive type expected" - unless args.size == val.nindices + val.nparams do throwTacticEx `generalizeIndices mvarId "ill-formed inductive datatype" - let indices := args.extract (args.size - val.nindices) args.size - let IA := mkAppN f (args.extract 0 val.nparams) -- `I A` + unless val.numIndices > 0 do throwTacticEx `generalizeIndices mvarId "indexed inductive type expected" + unless args.size == val.numIndices + val.numParams do throwTacticEx `generalizeIndices mvarId "ill-formed inductive datatype" + let indices := args.extract (args.size - val.numIndices) args.size + let IA := mkAppN f (args.extract 0 val.numParams) -- `I A` let IAType ← inferType IA forallTelescopeReducing IAType fun newIndices _ => do let newType := mkAppN IA newIndices @@ -132,7 +132,7 @@ structure Context where majorDecl : LocalDecl majorTypeFn : Expr majorTypeArgs : Array Expr - majorTypeIndices : Array Expr := majorTypeArgs.extract (majorTypeArgs.size - inductiveVal.nindices) majorTypeArgs.size + majorTypeIndices : Array Expr := majorTypeArgs.extract (majorTypeArgs.size - inductiveVal.numIndices) majorTypeArgs.size private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := do let env ← getEnv @@ -142,7 +142,7 @@ private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := d let majorDecl ← getLocalDecl majorFVarId let majorType ← whnf majorDecl.type majorType.withApp fun f args => matchConstInduct f (fun _ => pure none) fun ival _ => - if args.size != ival.nindices + ival.nparams then pure none + if args.size != ival.numIndices + ival.numParams then pure none else match env.find? (Name.mkStr ival.name "casesOn") with | ConstantInfo.defnInfo cval => pure $ some { @@ -291,7 +291,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Nam /- Remark: if caller does not need a `FVarSubst` (variable substitution), and `hasIndepIndices ctx` is true, then we can also use the simple case. This is a minor optimization, and we currently do not even allow callers to specify whether they want the `FVarSubst` or not. -/ - if ctx.inductiveVal.nindices == 0 then + if ctx.inductiveVal.numIndices == 0 then -- Simple case inductionCasesOn mvarId majorFVarId givenNames useUnusedNames ctx else diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean index 2e2cb405ee..14fbf51799 100644 --- a/src/Lean/Meta/Tactic/Constructor.lean +++ b/src/Lean/Meta/Tactic/Constructor.lean @@ -16,11 +16,11 @@ def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do matchConstStruct target.getAppFn (fun _ => throwTacticEx `exists mvarId "target is not an inductive datatype with one constructor") fun ival us cval => do - if cval.nfields < 2 then + if cval.numFields < 2 then throwTacticEx `exists mvarId "constructor must have at least two fields" - let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.nparams] + let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.numParams] let ctorType ← inferType ctor - let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.nfields-2)) + let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.numFields-2)) let f := mkAppN ctor mvars checkApp f w let [mvarId] ← apply mvarId <| mkApp f w diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index 5d4cf04e5a..32ae02f435 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -42,7 +42,7 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag assignExprMVar mvarId (mkApp val newMVar) let mvarId ← tryClear newMVar.mvarId! fvarId - pure $ InjectionResultCore.subgoal mvarId aCtor.nfields + pure $ InjectionResultCore.subgoal mvarId aCtor.numFields | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction" | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected" diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 3cf8463faf..0a9616019f 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -75,10 +75,10 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM (Option Ex let majorTypeI := majorType.getAppFn if !majorTypeI.isConstOf recVal.getInduct then pure none - else if majorType.hasExprMVar && majorType.getAppArgs[recVal.nparams:].any Expr.hasExprMVar then + else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then pure none else do - let (some newCtorApp) ← mkNullaryCtor majorType recVal.nparams | pure none + let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure none let newType ← inferType newCtorApp if (← isDefEq majorType newType) then pure newCtorApp @@ -98,12 +98,12 @@ private def reduceRec {α} (recVal : RecursorVal) (recLvls : List Level) (recArg match getRecRuleFor recVal major with | some rule => let majorArgs := major.getAppArgs - if recLvls.length != recVal.lparams.length then + if recLvls.length != recVal.levelParams.length then failK () else - let rhs := rule.rhs.instantiateLevelParams recVal.lparams recLvls + let rhs := rule.rhs.instantiateLevelParams recVal.levelParams recLvls -- Apply parameters, motives and minor premises from recursor application. - let rhs := mkAppRange rhs 0 (recVal.nparams+recVal.nmotives+recVal.nminors) recArgs + let rhs := mkAppRange rhs 0 (recVal.numParams+recVal.numMotives+recVal.numMinors) recArgs /- The number of parameters in the constructor is not necessarily equal to the number of parameters in the recursor when we have nested inductive types. -/ @@ -292,7 +292,7 @@ def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do let e ← whnf e matchConstCtor e.getAppFn (fun _ => pure none) fun ctorVal _ => let numArgs := e.getAppNumArgs - let idx := ctorVal.nparams + i + let idx := ctorVal.numParams + i if idx < numArgs then pure (some (e.getArg! idx)) else diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 87a299462e..83554712ef 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -422,7 +422,7 @@ def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) let name := `_regBuiltinParser ++ declName let type := mkApp (mkConst `IO) (mkConst `Unit) let val := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio] - let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, + let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } match env.addAndCompile {} decl with -- TODO: pretty print error diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 0076f3c4e8..b9c8f51845 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -82,7 +82,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do let paramTy ← replaceParserTy ctx <$> inferType param pure $ mkForall `_ BinderInfo.default paramTy ty let decl := Declaration.defnDecl { - name := c', lparams := [], + name := c', levelParams := [], type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } let env ← getEnv let env ← match env.addAndCompile {} decl with diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index f76528847b..b81d9e30e5 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -454,14 +454,14 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do /- If implicit arguments should be shown, and the structure has parameters, we should not pretty print using { ... }, because we will not be able to see the parameters. -/ let explicit ← getPPOption getPPExplicit - guard !(explicit && s.nparams > 0) + guard !(explicit && s.numParams > 0) let fieldNames := getStructureFields env s.induct let (_, fields) ← withAppFnArgs (pure (0, #[])) fun ⟨idx, fields⟩ => do - if idx < s.nparams then + if idx < s.numParams then pure (idx + 1, fields) else let val ← delab - let field ← `(structInstField|$(mkIdent <| fieldNames.get! (idx - s.nparams)):ident := $val) + let field ← `(structInstField|$(mkIdent <| fieldNames.get! (idx - s.numParams)):ident := $val) pure (idx + 1, fields.push field) let lastField := fields[fields.size - 1] let fields := fields.pop diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 3bae2f87d9..b12ba6bf68 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -37,42 +37,42 @@ def deinternalizeFieldName : Name → Name def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal := match env.find? constName with - | some (ConstantInfo.inductInfo { nparams := nparams, isRec := false, ctors := [ctorName], .. }) => + | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctorName], .. }) => match env.find? ctorName with | some (ConstantInfo.ctorInfo val) => val | _ => panic! "ill-formed environment" | _ => panic! "structure expected" -private def getStructureFieldsAux (nparams : Nat) : Nat → Expr → Array Name → Array Name +private def getStructureFieldsAux (numParams : Nat) : Nat → Expr → Array Name → Array Name | i, Expr.forallE n d b _, fieldNames => - if i < nparams then - getStructureFieldsAux nparams (i+1) b fieldNames + if i < numParams then + getStructureFieldsAux numParams (i+1) b fieldNames else - getStructureFieldsAux nparams (i+1) b <| fieldNames.push <| deinternalizeFieldName n + getStructureFieldsAux numParams (i+1) b <| fieldNames.push <| deinternalizeFieldName n | _, _, fieldNames => fieldNames -- TODO: fix. See comment in the beginning of the file def getStructureFields (env : Environment) (structName : Name) : Array Name := let ctor := getStructureCtor env structName; - getStructureFieldsAux ctor.nparams 0 ctor.type #[] + getStructureFieldsAux ctor.numParams 0 ctor.type #[] -private def isSubobjectFieldAux (nparams : Nat) (target : Name) : Nat → Expr → Option Name +private def isSubobjectFieldAux (numParams : Nat) (target : Name) : Nat → Expr → Option Name | i, Expr.forallE n d b _ => - if i < nparams then - isSubobjectFieldAux nparams target (i+1) b + if i < numParams then + isSubobjectFieldAux numParams target (i+1) b else if n == target then match d.getAppFn with | Expr.const parentStructName _ _ => some parentStructName | _ => panic! "ill-formed structure" else - isSubobjectFieldAux nparams target (i+1) b + isSubobjectFieldAux numParams target (i+1) b | _, _ => none -- TODO: fix. See comment in the beginning of the file /-- If `fieldName` represents the relation to a parent structure `S`, return `S` -/ def isSubobjectField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := let ctor := getStructureCtor env structName; - isSubobjectFieldAux ctor.nparams (mkInternalSubobjectFieldName fieldName) 0 ctor.type + isSubobjectFieldAux ctor.numParams (mkInternalSubobjectFieldName fieldName) 0 ctor.type /-- Return immediate parent structures -/ def getParentStructures (env : Environment) (structName : Name) : Array Name := @@ -100,10 +100,10 @@ def getStructureFieldsFlattened (env : Environment) (structName : Name) : Array getStructureFieldsFlattenedAux env structName #[] -- TODO: fix. See comment in the beginning of the file -private def hasProjFn (env : Environment) (structName : Name) (nparams : Nat) : Nat → Expr → Bool +private def hasProjFn (env : Environment) (structName : Name) (numParams : Nat) : Nat → Expr → Bool | i, Expr.forallE n d b _ => - if i < nparams then - hasProjFn env structName nparams (i+1) b + if i < numParams then + hasProjFn env structName numParams (i+1) b else let fullFieldName := structName ++ deinternalizeFieldName n; env.isProjectionFn fullFieldName @@ -118,7 +118,7 @@ private def hasProjFn (env : Environment) (structName : Name) (nparams : Nat) : def isStructure (env : Environment) (constName : Name) : Bool := if isStructureLike env constName then let ctor := getStructureCtor env constName; - hasProjFn env constName ctor.nparams 0 ctor.type + hasProjFn env constName ctor.numParams 0 ctor.type else false diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean index cc41645bca..a8799282f8 100644 --- a/src/Lean/Util/Recognizers.lean +++ b/src/Lean/Util/Recognizers.lean @@ -84,7 +84,7 @@ def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal := | _ => match e.getAppFn with | Expr.const n _ _ => match getConstructorVal? env n with - | some v => if v.nparams + v.nfields == e.getAppNumArgs then some v else none + | some v => if v.numParams + v.numFields == e.getAppNumArgs then some v else none | none => none | _ => none @@ -104,7 +104,7 @@ def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × A match e.getAppFn with | Expr.const n _ _ => do let v ← getConstructorVal? env n - if v.nparams + v.nfields == e.getAppNumArgs then + if v.numParams + v.numFields == e.getAppNumArgs then pure (v, e.getAppArgs) else none diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean index 6c0c9487da..ce13fc781d 100644 --- a/tests/lean/run/depElim1.lean +++ b/tests/lean/run/depElim1.lean @@ -28,7 +28,7 @@ inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do let env ← getEnv match env.find? ctorName with -| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then return some (v, fn, args) else return none +| some (ConstantInfo.ctorInfo v) => if args.size == v.numParams + v.numFields then return some (v, fn, args) else return none | _ => return none private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do @@ -79,8 +79,8 @@ partial def mkPattern : Expr → MetaM Pattern match r? with | none => throwError "unexpected pattern" | some (cval, fn, args) => - let params := args.extract 0 cval.nparams - let fields := args.extract cval.nparams args.size + let params := args.extract 0 cval.numParams + let fields := args.extract cval.numParams args.size let pats ← fields.toList.mapM mkPattern return Pattern.ctor cval.name fn.constLevels! params.toList pats diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 7c2c6933a5..acdc95ffda 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -242,13 +242,14 @@ do print "----- tst14 -----"; def tst15 : MetaM Unit := do print "----- tst15 -----"; - let inst ← mkAdd nat; + let inst ← _root_.mkAdd nat; let r ← synthInstance inst; print r; pure () #eval tst15 + def tst16 : MetaM Unit := do print "----- tst16 -----"; let prod ← mkProd nat nat; diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean index bc8a66f718..497eda3258 100644 --- a/tests/lean/run/toExpr.lean +++ b/tests/lean/run/toExpr.lean @@ -6,12 +6,12 @@ unsafe def test {α : Type} [ToString α] [ToExpr α] [BEq α] (a : α) : CoreM let env ← getEnv; let auxName := `_toExpr._test; let decl := Declaration.defnDecl { - name := auxName, - lparams := [], - value := toExpr a, - type := toTypeExpr α, - hints := ReducibilityHints.abbrev, - safety := DefinitionSafety.safe + name := auxName, + levelParams := [], + value := toExpr a, + type := toTypeExpr α, + hints := ReducibilityHints.abbrev, + safety := DefinitionSafety.safe }; IO.println (toExpr a); (match env.addAndCompile {} decl with