From 3b6d65c3c32c12b603681a650169799d209a759a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2020 09:59:24 -0800 Subject: [PATCH] chore: use `deriving Inhabited` --- src/Init/Core.lean | 15 +------ src/Init/Meta.lean | 3 +- src/Init/System/IOError.lean | 2 +- src/Lean/Class.lean | 3 +- src/Lean/Compiler/IR/Basic.lean | 8 ++-- src/Lean/Compiler/IR/ElimDeadBranches.lean | 3 +- src/Lean/Compiler/IR/LiveVars.lean | 3 +- src/Lean/Compiler/IR/RC.lean | 4 +- src/Lean/Compiler/InlineAttrs.lean | 3 +- src/Lean/Data/Position.lean | 7 +--- src/Lean/Declaration.lean | 17 +++----- src/Lean/Elab/App.lean | 6 +-- src/Lean/Elab/Command.lean | 9 ++--- src/Lean/Elab/DeclModifiers.lean | 2 + src/Lean/Elab/DefView.lean | 2 + src/Lean/Elab/Do.lean | 8 +--- src/Lean/Elab/Inductive.lean | 13 ++---- src/Lean/Elab/Match.lean | 3 +- src/Lean/Elab/MutualDef.lean | 4 +- src/Lean/Elab/PreDefinition/Basic.lean | 1 + src/Lean/Environment.lean | 47 +++++++++++----------- src/Lean/KeyedDeclsAttribute.lean | 11 ++--- src/Lean/LocalContext.lean | 4 +- src/Lean/Message.lean | 5 ++- src/Lean/Meta/Basic.lean | 27 +++++-------- src/Lean/Meta/Closure.lean | 4 +- src/Lean/Meta/SynthInstance.lean | 7 +--- src/Lean/MetavarContext.lean | 5 ++- src/Lean/Parser/Basic.lean | 16 ++++---- src/Lean/Parser/Extension.lean | 11 ++--- src/Lean/Parser/Module.lean | 3 +- src/Lean/ParserCompiler/Attribute.lean | 4 +- src/Lean/Util/CollectFVars.lean | 3 +- src/Std/Data/BinomialHeap.lean | 3 +- src/Std/Data/HashMap.lean | 3 +- src/Std/Data/HashSet.lean | 3 +- src/Std/Data/PersistentArray.lean | 6 +-- 37 files changed, 108 insertions(+), 170 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 8d74398938..7c00722efb 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -440,20 +440,7 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : instance : Inhabited Prop where default := True -instance : Inhabited Bool where - default := false - -instance : Inhabited True where - default := trivial - -instance : Inhabited NonScalar where - default := ⟨arbitrary⟩ - -instance : Inhabited PNonScalar.{u} where - default := ⟨arbitrary⟩ - -instance {α} [Inhabited α] : Inhabited (ForInStep α) where - default := ForInStep.done (arbitrary) +deriving instance Inhabited for Bool, NonScalar, PNonScalar, True, ForInStep class inductive Nonempty (α : Sort u) : Prop where | intro (val : α) : Nonempty α diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 71274b859e..540412f169 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -73,11 +73,10 @@ end Name structure NameGenerator where namePrefix : Name := `_uniq idx : Nat := 1 + deriving Inhabited namespace NameGenerator -instance : Inhabited NameGenerator := ⟨{}⟩ - @[inline] def curr (g : NameGenerator) : Name := Name.mkNum g.namePrefix g.idx diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 019b0bda56..c51cae9547 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -51,6 +51,7 @@ inductive IO.Error where | unexpectedEof | userError (msg : String) + deriving Inhabited @[export mk_io_user_error] def IO.userError (s : String) : IO.Error := @@ -190,6 +191,5 @@ def toString : IO.Error → String | userError msg => msg instance : ToString IO.Error := ⟨ IO.Error.toString ⟩ -instance : Inhabited IO.Error := ⟨ userError "" ⟩ end IO.Error diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index 1b98878065..d003e78663 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -20,11 +20,10 @@ end ClassEntry structure ClassState where hasOutParam : SMap Name Bool := SMap.empty + deriving Inhabited namespace ClassState -instance : Inhabited ClassState := ⟨{}⟩ - def addEntry (s : ClassState) (entry : ClassEntry) : ClassState := { s with hasOutParam := s.hasOutParam.insert entry.name entry.hasOutParam } diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 910e092baf..8b258f49b9 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -23,10 +23,12 @@ abbrev Index := Nat /- Variable identifier -/ structure VarId where idx : Index + deriving Inhabited /- Join point identifier -/ structure JoinPointId where idx : Index + deriving Inhabited abbrev Index.lt (a b : Index) : Bool := a < b @@ -80,6 +82,7 @@ inductive IRType where | irrelevant | object | tobject | struct (leanTypeName : Option Name) (types : Array IRType) : IRType | union (leanTypeName : Name) (types : Array IRType) : IRType + deriving Inhabited namespace IRType @@ -134,6 +137,7 @@ end IRType inductive Arg where | var (id : VarId) | irrelevant + deriving Inhabited protected def Arg.beq : Arg → Arg → Bool | var x, var y => x == y @@ -141,7 +145,6 @@ protected def Arg.beq : Arg → Arg → Bool | _, _ => false instance : BEq Arg := ⟨Arg.beq⟩ -instance : Inhabited Arg := ⟨Arg.irrelevant⟩ @[export lean_ir_mk_var_arg] def mkVarArg (id : VarId) : Arg := Arg.var id @@ -233,8 +236,7 @@ structure Param where x : VarId borrow : Bool ty : IRType - -instance : Inhabited Param := ⟨{ x := { idx := 0 }, borrow := false, ty := IRType.object }⟩ + deriving Inhabited @[export lean_ir_mk_param] def mkParam (x : VarId) (borrow : Bool) (ty : IRType) : Param := ⟨x, borrow, ty⟩ diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index 2d19a7646e..84749f19a7 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -15,11 +15,10 @@ inductive Value where | top -- any value | ctor (i : CtorInfo) (vs : Array Value) | choice (vs : List Value) + deriving Inhabited namespace Value -instance : Inhabited Value := ⟨top⟩ - protected partial def beq : Value → Value → Bool | bot, bot => true | top, top => true diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index c6cdfdb807..f93de87be4 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -81,7 +81,8 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool := abbrev LiveVarSet := VarIdSet abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx) -instance : Inhabited LiveVarSet := ⟨{}⟩ +instance : Inhabited LiveVarSet where + default := {} def mkLiveVarSet (x : VarId) : LiveVarSet := Std.RBTree.empty.insert x diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 46d5c8a43d..0b50b9aa27 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -17,12 +17,10 @@ structure VarInfo where ref : Bool := true -- true if the variable may be a reference (aka pointer) at runtime persistent : Bool := false -- true if the variable is statically known to be marked a Persistent at runtime consume : Bool := false -- true if the variable RC must be "consumed" + deriving Inhabited abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => x.idx < y.idx) -instance : Inhabited VarInfo where - default := {} - structure Context where env : Environment decls : Array Decl diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index bb3f6c5138..5b67ed0d61 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -10,11 +10,10 @@ namespace Lean.Compiler inductive InlineAttributeKind where | inline | noinline | macroInline | inlineIfReduce + deriving Inhabited namespace InlineAttributeKind -instance : Inhabited InlineAttributeKind := ⟨InlineAttributeKind.inline⟩ - protected def beq : InlineAttributeKind → InlineAttributeKind → Bool | inline, inline => true | noinline, noinline => true diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index 0836be5179..b1032256da 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -10,6 +10,7 @@ namespace Lean structure Position where line : Nat column : Nat + deriving Inhabited namespace Position instance : DecidableEq Position := @@ -30,20 +31,16 @@ instance : ToFormat Position := instance : ToString Position := ⟨fun ⟨l, c⟩ => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩"⟩ - -instance : Inhabited Position := ⟨⟨1, 0⟩⟩ end Position structure FileMap where source : String positions : Array String.Pos lines : Array Nat + deriving Inhabited namespace FileMap -instance : Inhabited FileMap := - ⟨{ source := "", positions := #[], lines := #[] }⟩ - partial def ofString (s : String) : FileMap := let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap := if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line } diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 306fc82ffe..63d56a1704 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -34,6 +34,7 @@ inductive ReducibilityHints where | opaque : ReducibilityHints | «abbrev» : ReducibilityHints | regular : UInt32 → ReducibilityHints + deriving Inhabited @[export lean_mk_reducibility_hints_regular] def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints := @@ -47,8 +48,6 @@ def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 := namespace ReducibilityHints -instance : Inhabited ReducibilityHints := ⟨opaque⟩ - def lt : ReducibilityHints → ReducibilityHints → Bool | «abbrev», «abbrev» => false | «abbrev», _ => true @@ -63,8 +62,7 @@ structure ConstantVal where name : Name lparams : List Name type : Expr - -instance : Inhabited ConstantVal := ⟨{ name := arbitrary, lparams := arbitrary, type := arbitrary }⟩ + deriving Inhabited structure AxiomVal extends ConstantVal where isUnsafe : Bool @@ -136,8 +134,7 @@ inductive Declaration where | quotDecl | mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` | inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) - -instance : Inhabited Declaration := ⟨Declaration.quotDecl⟩ + deriving Inhabited @[export lean_mk_inductive_decl] def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration := @@ -185,9 +182,7 @@ structure InductiveVal extends ConstantVal where isUnsafe : Bool isReflexive : Bool isNested : Bool - -instance : Inhabited InductiveVal where - default := ⟨arbitrary, 0, 0, [], [], false, false, false, false⟩ + deriving Inhabited @[export lean_mk_inductive_val] def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat) @@ -218,6 +213,7 @@ structure ConstructorVal extends ConstantVal where nparams : Nat -- Number of parameters in inductive datatype `induct` nfields : 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 := { @@ -233,9 +229,6 @@ def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct @[export lean_constructor_val_is_unsafe] def ConstructorVal.isUnsafeEx (v : ConstructorVal) : Bool := v.isUnsafe -instance : Inhabited ConstructorVal := - ⟨{ toConstantVal := arbitrary, induct := arbitrary, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩ - /-- Information for reducing a recursor -/ structure RecursorRule where ctor : Name -- Reduction rule for this Constructor diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 364d21cc47..02724a99f6 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -23,8 +23,7 @@ def hasElabWithoutExpectedType (env : Environment) (declName : Name) : Bool := inductive Arg where | stx (val : Syntax) | expr (val : Expr) - -instance : Inhabited Arg := ⟨Arg.stx arbitrary⟩ + deriving Inhabited instance : ToString Arg := ⟨fun | Arg.stx val => toString val @@ -35,12 +34,11 @@ structure NamedArg where ref : Syntax := Syntax.missing name : Name val : Arg + deriving Inhabited instance : ToString NamedArg where toString s := "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")" -instance : Inhabited NamedArg := ⟨{ name := arbitrary, val := arbitrary }⟩ - def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermElabM α := withRef namedArg.ref $ match fn? with | some fn => throwError! "invalid argument name '{namedArg.name}' for function '{fn}'" diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 924ae8c565..e75cc2dc1e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -21,8 +21,7 @@ structure Scope where openDecls : List OpenDecl := [] levelNames : List Name := [] varDecls : Array Syntax := #[] - -instance : Inhabited Scope := ⟨{ header := "" }⟩ + deriving Inhabited structure State where env : Environment @@ -32,8 +31,7 @@ structure State where maxRecDepth : Nat nextInstIdx : Nat := 1 -- for generating anonymous instance names ngen : NameGenerator := {} - -instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩ + deriving Inhabited def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := { env := env @@ -241,7 +239,8 @@ def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun st private def getVarDecls (s : State) : Array Syntax := s.scopes.head!.varDecls -instance {α} : Inhabited (CommandElabM α) := ⟨throw arbitrary⟩ +instance {α} : Inhabited (CommandElabM α) where + default := throw arbitrary private def mkMetaContext : Meta.Context := { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true } diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 385aba1088..5309e7b410 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -26,6 +26,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception inductive Visibility where | regular | «protected» | «private» + deriving Inhabited instance : ToString Visibility := ⟨fun | Visibility.regular => "regular" @@ -39,6 +40,7 @@ structure Modifiers where isPartial : Bool := false isUnsafe : Bool := false attrs : Array Attribute := #[] + deriving Inhabited def Modifiers.isPrivate : Modifiers → Bool | { visibility := Visibility.private, .. } => true diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 20a86b2744..c49c2b7e02 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -16,6 +16,7 @@ namespace Lean.Elab inductive DefKind where | «def» | «theorem» | «example» | «opaque» | «abbrev» + deriving Inhabited def DefKind.isTheorem : DefKind → Bool | «theorem» => true @@ -39,6 +40,7 @@ structure DefView where binders : Syntax type? : Option Syntax value : Syntax + deriving Inhabited namespace Command diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index bbb392ebb8..1d1ebc5be8 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -80,6 +80,7 @@ structure Alt (σ : Type) where vars : Array Name patterns : Syntax rhs : σ + deriving Inhabited /- Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`). @@ -143,12 +144,7 @@ inductive Code where | ite (ref : Syntax) (h? : Option Name) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) | «match» (ref : Syntax) (discrs : Syntax) (optType : Syntax) (alts : Array (Alt Code)) | jmp (ref : Syntax) (jpName : Name) (args : Array Syntax) - -instance : Inhabited Code := - ⟨Code.«break» arbitrary⟩ - -instance : Inhabited (Alt Code) := - ⟨{ ref := arbitrary, vars := #[], patterns := arbitrary, rhs := arbitrary }⟩ + deriving Inhabited /- A code block, and the collection of variables updated by it. -/ structure CodeBlock where diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index ebb7ad971d..95cbb7ef0b 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -49,9 +49,7 @@ structure CtorView where declName : Name binders : Syntax type? : Option Syntax - -instance : Inhabited CtorView := - ⟨{ ref := arbitrary, modifiers := {}, inferMod := false, declName := arbitrary, binders := arbitrary, type? := none }⟩ + deriving Inhabited structure InductiveView where ref : Syntax @@ -63,10 +61,7 @@ structure InductiveView where type? : Option Syntax ctors : Array CtorView derivingClasses : Array DerivingClassView - -instance : Inhabited InductiveView := - ⟨{ ref := arbitrary, modifiers := {}, shortDeclName := arbitrary, declName := arbitrary, - levelNames := [], binders := arbitrary, type? := none, ctors := #[], derivingClasses := #[] }⟩ + deriving Inhabited structure ElabHeaderResult where view : InductiveView @@ -74,9 +69,7 @@ structure ElabHeaderResult where localInsts : LocalInstances params : Array Expr type : Expr - -instance : Inhabited ElabHeaderResult := - ⟨{ view := arbitrary, lctx := arbitrary, localInsts := arbitrary, params := #[], type := arbitrary }⟩ + deriving Inhabited private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) := do if h : i < views.size then diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 1ced7e6efb..234007ea32 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -268,8 +268,7 @@ structure Context where namedArgs : Array NamedArg args : List Arg newArgs : Array Syntax := #[] - -instance : Inhabited Context := ⟨⟨arbitrary, none, false, false, #[], 0, #[], [], #[]⟩⟩ + deriving Inhabited private def isDone (ctx : Context) : Bool := ctx.paramDeclIdx ≥ ctx.paramDecls.size diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 1ad4a77a85..15c8ba2eac 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -22,9 +22,7 @@ structure DefViewElabHeader where numParams : Nat type : Expr -- including the parameters valueStx : Syntax - -instance : Inhabited DefViewElabHeader := - ⟨⟨arbitrary, {}, DefKind.«def», arbitrary, arbitrary, [], 0, arbitrary, arbitrary ⟩⟩ + deriving Inhabited namespace Term diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 1c0a085849..78b4aa494f 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -24,6 +24,7 @@ structure PreDefinition where declName : Name type : Expr value : Expr + deriving Inhabited instance : Inhabited PreDefinition := ⟨⟨DefKind.«def», [], {}, arbitrary, arbitrary, arbitrary⟩⟩ diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 1921fa7809..a5b0c4e099 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -15,7 +15,8 @@ namespace Lean /- Opaque environment extension state. -/ constant EnvExtensionStateSpec : PointedType.{0} def EnvExtensionState : Type := EnvExtensionStateSpec.type -instance : Inhabited EnvExtensionState := ⟨EnvExtensionStateSpec.val⟩ +instance : Inhabited EnvExtensionState where + default := EnvExtensionStateSpec.val def ModuleIdx := Nat @@ -47,6 +48,7 @@ structure EnvironmentHeader where imports : Array Import := #[] -- direct imports regions : Array CompactedRegion := #[] -- compacted regions of all imported modules moduleNames : NameSet := {} -- names of all imported modules + deriving Inhabited open Std (HashMap) @@ -55,12 +57,10 @@ structure Environment where constants : ConstMap extensions : Array EnvExtensionState header : EnvironmentHeader := {} + deriving Inhabited namespace Environment -instance : Inhabited Environment := - ⟨{ const2ModIdx := {}, constants := {}, extensions := #[] }⟩ - def addAux (env : Environment) (cinfo : ConstantInfo) : Environment := { env with constants := env.constants.insert cinfo.name cinfo } @@ -148,15 +148,16 @@ structure EnvExtensionInterface where getState {σ} (e : ext σ) (env : Environment) : σ mkInitialExtStates : IO (Array EnvExtensionState) -instance : Inhabited EnvExtensionInterface := ⟨{ - ext := id, - inhabitedExt := id, - registerExt := fun mk => mk, - setState := fun _ env _ => env, - modifyState := fun _ env _ => env, - getState := fun ext _ => ext, - mkInitialExtStates := pure #[] -}⟩ +instance : Inhabited EnvExtensionInterface where + default := { + ext := id, + inhabitedExt := id, + registerExt := fun mk => mk, + setState := fun _ env _ => env, + modifyState := fun _ env _ => env, + getState := fun ext _ => ext, + mkInitialExtStates := pure #[] + } /- Unsafe implementation of `EnvExtensionInterface` -/ namespace EnvExtensionInterfaceUnsafe @@ -164,8 +165,7 @@ namespace EnvExtensionInterfaceUnsafe structure Ext (σ : Type) where idx : Nat mkInitial : IO σ - -instance {σ} : Inhabited (Ext σ) := ⟨{idx := 0, mkInitial := arbitrary }⟩ + deriving Inhabited private def mkEnvExtensionsRef : IO (IO.Ref (Array (Ext EnvExtensionState))) := IO.mkRef #[] @[builtinInit mkEnvExtensionsRef] private constant envExtensionsRef : IO.Ref (Array (Ext EnvExtensionState)) @@ -285,14 +285,15 @@ instance : Inhabited EnvExtensionEntry := ⟨EnvExtensionEntrySpec.val⟩ instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) := ⟨{importedEntries := #[], state := arbitrary }⟩ -instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) := ⟨{ - toEnvExtension := arbitrary, - name := arbitrary, - addImportedFn := fun _ => arbitrary, - addEntryFn := fun s _ => s, - exportEntriesFn := fun _ => #[], - statsFn := fun _ => Format.nil -}⟩ +instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) where + default := { + toEnvExtension := arbitrary, + name := arbitrary, + addImportedFn := fun _ => arbitrary, + addEntryFn := fun s _ => s, + exportEntriesFn := fun _ => #[], + statsFn := fun _ => Format.nil + } namespace PersistentEnvExtension diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 436ca2f19c..2306587f52 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -36,9 +36,7 @@ structure Def (γ : Type) where fun builtin arg => match attrParamSyntaxToIdentifier arg with | some id => pure id | none => throwError "invalid attribute argument, expected identifier" - -instance {γ} : Inhabited (Def γ) := - ⟨{ builtinName := arbitrary, name := arbitrary, descr := arbitrary, valueTypeName := arbitrary }⟩ + deriving Inhabited structure OLeanEntry where key : Key @@ -54,6 +52,7 @@ abbrev Table (γ : Type) := SMap Key (List γ) structure ExtensionState (γ : Type) where newEntries : List OLeanEntry := [] table : Table γ := {} + deriving Inhabited abbrev Extension (γ : Type) := PersistentEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ) @@ -65,6 +64,7 @@ structure KeyedDeclsAttribute (γ : Type) where tableRef : IO.Ref (KeyedDeclsAttribute.Table γ) -- instances from current module ext : KeyedDeclsAttribute.Extension γ + deriving Inhabited namespace KeyedDeclsAttribute @@ -73,11 +73,6 @@ def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ := | some vs => SMap.insert table k (v::vs) | none => SMap.insert table k [v] -instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩ - -instance {γ} : Inhabited (KeyedDeclsAttribute γ) := - ⟨{ defn := arbitrary, tableRef := arbitrary, ext := arbitrary }⟩ - private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do let table ← tableRef.get pure { table := table } diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 061d733940..5f8b43f8df 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -12,6 +12,7 @@ namespace Lean inductive LocalDecl where | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) + deriving Inhabited @[export lean_mk_local_decl] def mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalDecl := @@ -25,7 +26,6 @@ def LocalDecl.binderInfoEx : LocalDecl → BinderInfo | _ => BinderInfo.default namespace LocalDecl -instance : Inhabited LocalDecl := ⟨ldecl arbitrary arbitrary arbitrary arbitrary arbitrary false⟩ def isLet : LocalDecl → Bool | cdecl .. => false @@ -96,9 +96,9 @@ open Std (PersistentHashMap PersistentArray PArray) structure LocalContext where fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {} decls : PersistentArray (Option LocalDecl) := {} + deriving Inhabited namespace LocalContext -instance : Inhabited LocalContext := ⟨{}⟩ @[export lean_mk_empty_local_ctx] def mkEmpty : Unit → LocalContext := fun _ => {} diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 7f14f32446..98f2854b27 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -19,6 +19,7 @@ def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : S inductive MessageSeverity where | information | warning | error + deriving Inhabited structure MessageDataContext where env : Environment @@ -51,6 +52,7 @@ inductive MessageData where Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/ | tagged : Name → MessageData → MessageData | node : Array MessageData → MessageData + deriving Inhabited namespace MessageData @@ -65,8 +67,6 @@ def isNest : MessageData → Bool | nest _ _ => true | _ => false -instance : Inhabited MessageData := ⟨MessageData.ofFormat arbitrary⟩ - def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls @@ -142,6 +142,7 @@ structure Message where severity : MessageSeverity := MessageSeverity.error caption : String := "" data : MessageData + deriving Inhabited @[export lean_mk_message] def mkMessageEx (fileName : String) (pos : Position) (endPos : Option Position) (severity : MessageSeverity) (caption : String) (text : String) : Message := diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index af6031cad9..237ea6e97c 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -60,8 +60,7 @@ structure ParamInfo where instImplicit : Bool := false hasFwdDeps : Bool := false backDeps : Array Nat := #[] - -instance : Inhabited ParamInfo := ⟨{}⟩ + deriving Inhabited def ParamInfo.isExplicit (p : ParamInfo) : Bool := !p.implicit && p.instImplicit @@ -74,9 +73,9 @@ structure InfoCacheKey where transparency : TransparencyMode expr : Expr nargs? : Option Nat + deriving Inhabited namespace InfoCacheKey -instance : Inhabited InfoCacheKey := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩ instance : Hashable InfoCacheKey := ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩ instance : BEq InfoCacheKey := @@ -93,6 +92,7 @@ structure Cache where synthInstance : SynthInstanceCache := {} whnfDefault : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.default` whnfAll : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.all` + deriving Inhabited structure PostponedEntry where lhs : Level @@ -104,8 +104,7 @@ structure State where /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/ zetaFVarIds : NameSet := {} postponed : PersistentArray PostponedEntry := {} - -instance : Inhabited State := ⟨{}⟩ + deriving Inhabited structure Context where config : Config := {} @@ -114,22 +113,18 @@ structure Context where abbrev MetaM := ReaderT Context $ StateRefT State CoreM -instance : Inhabited (MetaM α) := { +instance : Inhabited (MetaM α) where default := fun _ _ => arbitrary -} -instance : MonadLCtx MetaM := { - getLCtx := do pure (← read).lctx -} +instance : MonadLCtx MetaM where + getLCtx := return (← read).lctx -instance : MonadMCtx MetaM := { - getMCtx := do pure (← get).mctx, - modifyMCtx := fun f => modify fun s => { s with mctx := f s.mctx } -} +instance : MonadMCtx MetaM where + getMCtx := return (← get).mctx + modifyMCtx f := modify fun s => { s with mctx := f s.mctx } -instance : AddMessageContext MetaM := { +instance : AddMessageContext MetaM where addMessageContext := addMessageContextFull -} @[inline] def MetaM.run (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) := x ctx |>.run s diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 9f8c1d84e9..d76f23d68d 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -100,9 +100,7 @@ namespace Closure structure ToProcessElement where fvarId : FVarId newFVarId : FVarId - -instance : Inhabited ToProcessElement := - ⟨⟨arbitrary, arbitrary⟩⟩ + deriving Inhabited structure Context where zeta : Bool diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index baf60d78f9..5c1e94cb10 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -29,8 +29,7 @@ structure GeneratorNode where mctx : MetavarContext instances : Array Expr currInstanceIdx : Nat - -instance : Inhabited GeneratorNode := ⟨⟨arbitrary, arbitrary, arbitrary, arbitrary, 0⟩⟩ + deriving Inhabited structure ConsumerNode where mvar : Expr @@ -38,9 +37,7 @@ structure ConsumerNode where mctx : MetavarContext subgoals : List Expr size : Nat -- instance size so far - -instance : Inhabited ConsumerNode where - default := { mvar := arbitrary, key := arbitrary, mctx := arbitrary, subgoals := [], size := 0 } + deriving Inhabited inductive Waiter where | consumerNode : ConsumerNode → Waiter diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 9172ce897e..3fd0f39813 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -221,6 +221,7 @@ we may solve the issue by implementing `isDefEqCheap` that never invokes TC and structure LocalInstance where className : Name fvar : Expr + deriving Inhabited abbrev LocalInstances := Array LocalInstance @@ -237,6 +238,7 @@ inductive MetavarKind where | natural | synthetic | syntheticOpaque + deriving Inhabited def MetavarKind.isSyntheticOpaque : MetavarKind → Bool | MetavarKind.syntheticOpaque => true @@ -254,13 +256,12 @@ structure MetavarDecl where localInstances : LocalInstances kind : MetavarKind numScopeArgs : Nat := 0 -- See comment at `CheckAssignment` `Meta/ExprDefEq.lean` + deriving Inhabited @[export lean_mk_metavar_decl] def mkMetavarDeclEx (userName : Name) (lctx : LocalContext) (type : Expr) (depth : Nat) (localInstances : LocalInstances) (kind : MetavarKind) : MetavarDecl := { userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances, kind := kind } -instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary, type := arbitrary, depth := 0, localInstances := #[], kind := MetavarKind.natural }⟩ - /-- A delayed assignment for a metavariable `?m`. It represents an assignment of the form `?m := (fun fvars => val)`. The local context `lctx` provides the declarations for `fvars`. diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 2f56ae3e8c..4579705c2b 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -116,10 +116,7 @@ structure InputContext where input : String fileName : String fileMap : FileMap - -instance : Inhabited InputContext := ⟨{ - input := "", fileName := "", fileMap := arbitrary -}⟩ + deriving Inhabited /-- Input context derived from elaboration of previous commands. -/ structure ParserModuleContext where @@ -142,9 +139,9 @@ def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × structure Error where unexpected : String := "" expected : List String := [] + deriving Inhabited namespace Error -instance : Inhabited Error := ⟨{}⟩ private def expectedToString : List String → String | [] => "" @@ -262,13 +259,15 @@ end ParserState def ParserFn := ParserContext → ParserState → ParserState -instance : Inhabited ParserFn := ⟨fun _ => id⟩ +instance : Inhabited ParserFn where + default := fun ctx s => s inductive FirstTokens where | epsilon : FirstTokens | unknown : FirstTokens | tokens : List Token → FirstTokens | optTokens : List Token → FirstTokens + deriving Inhabited namespace FirstTokens @@ -305,13 +304,12 @@ structure ParserInfo where collectTokens : List Token → List Token := id collectKinds : SyntaxNodeKindSet → SyntaxNodeKindSet := id firstTokens : FirstTokens := FirstTokens.unknown + deriving Inhabited structure Parser where info : ParserInfo := {} fn : ParserFn - -instance : Inhabited Parser := - ⟨{ fn := fun _ s => s }⟩ + deriving Inhabited abbrev TrailingParser := Parser diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index df7e35fcbe..a9b2fe63f7 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -54,18 +54,14 @@ inductive OLeanEntry where | kind (val : SyntaxNodeKind) : OLeanEntry | category (catName : Name) (leadingIdentAsSymbol : Bool) | parser (catName : Name) (declName : Name) (prio : Nat) : OLeanEntry + deriving Inhabited inductive Entry where | token (val : Token) : Entry | kind (val : SyntaxNodeKind) : Entry | category (catName : Name) (leadingIdentAsSymbol : Bool) | parser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Entry - -instance : Inhabited OLeanEntry where - default := OLeanEntry.token arbitrary - -instance : Inhabited Entry where - default := Entry.token arbitrary + deriving Inhabited def Entry.toOLeanEntry : Entry → OLeanEntry | token v => OLeanEntry.token v @@ -77,8 +73,7 @@ structure State where tokens : TokenTable := {} kinds : SyntaxNodeKindSet := {} categories : ParserCategories := {} - -instance : Inhabited State := ⟨{}⟩ + deriving Inhabited end ParserExtension diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index d76de41040..32f651d031 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -31,8 +31,7 @@ end Module structure ModuleParserState where pos : String.Pos := 0 recovering : Bool := false - -instance : Inhabited ModuleParserState := ⟨{}⟩ + deriving Inhabited private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message := let pos := c.fileMap.toPosition pos diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean index 56386d8eb2..43ce4d0a96 100644 --- a/src/Lean/ParserCompiler/Attribute.lean +++ b/src/Lean/ParserCompiler/Attribute.lean @@ -14,7 +14,7 @@ namespace ParserCompiler structure CombinatorAttribute where impl : AttributeImpl ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) - + deriving Inhabited -- TODO(Sebastian): We'll probably want priority support here at some point def registerCombinatorAttribute (name : Name) (descr : String) @@ -40,8 +40,6 @@ def registerCombinatorAttribute (name : Name) (descr : String) namespace CombinatorAttribute -instance : Inhabited CombinatorAttribute := ⟨{ impl := arbitrary, ext := arbitrary }⟩ - def getDeclFor? (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name := (attr.ext.getState env).find? parserDecl diff --git a/src/Lean/Util/CollectFVars.lean b/src/Lean/Util/CollectFVars.lean index 7885785975..ab0f438df6 100644 --- a/src/Lean/Util/CollectFVars.lean +++ b/src/Lean/Util/CollectFVars.lean @@ -10,8 +10,7 @@ namespace Lean.CollectFVars structure State where visitedExpr : ExprSet := {} fvarSet : NameSet := {} - -instance : Inhabited State := ⟨{}⟩ + deriving Inhabited abbrev Visitor := State → State diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean index 7dcbd80107..6aa7321530 100644 --- a/src/Std/Data/BinomialHeap.lean +++ b/src/Std/Data/BinomialHeap.lean @@ -15,13 +15,12 @@ structure HeapNodeAux (α : Type u) (h : Type u) where inductive Heap (α : Type u) : Type u where | empty : Heap α | heap (ns : List (HeapNodeAux α (Heap α))) : Heap α + deriving Inhabited abbrev HeapNode (α) := HeapNodeAux α (Heap α) variables {α : Type u} -instance : Inhabited (Heap α) := ⟨Heap.empty⟩ - def hRank : List (HeapNode α) → Nat | [] => 0 | h::_ => h.rank diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index fc28a737c6..1a588a9813 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -124,7 +124,8 @@ def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) namespace HashMap variables {α : Type u} {β : Type v} [BEq α] [Hashable α] -instance : Inhabited (HashMap α β) := ⟨mkHashMap⟩ +instance : Inhabited (HashMap α β) where + default := mkHashMap instance : EmptyCollection (HashMap α β) := ⟨mkHashMap⟩ diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index 427b245b28..f33497d893 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -116,7 +116,8 @@ def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α namespace HashSet variables {α : Type u} [BEq α] [Hashable α] -instance : Inhabited (HashSet α) := ⟨mkHashSet⟩ +instance : Inhabited (HashSet α) where + default := mkHashSet instance : EmptyCollection (HashSet α) := ⟨mkHashSet⟩ diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index e48671a720..2e3f40de76 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -10,11 +10,10 @@ namespace Std inductive PersistentArrayNode (α : Type u) where | node (cs : Array (PersistentArrayNode α)) : PersistentArrayNode α | leaf (vs : Array α) : PersistentArrayNode α + deriving Inhabited namespace PersistentArrayNode -instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf #[]⟩ - def isNode {α} : PersistentArrayNode α → Bool | node _ => true | leaf _ => false @@ -34,6 +33,7 @@ structure PersistentArray (α : Type u) where size : Nat := 0 shift : USize := PersistentArray.initShift tailOff : Nat := 0 + deriving Inhabited abbrev PArray (α : Type u) := PersistentArray α @@ -47,8 +47,6 @@ def empty : PersistentArray α := {} def isEmpty (a : PersistentArray α) : Bool := a.size == 0 -instance : Inhabited (PersistentArray α) := ⟨{}⟩ - def mkEmptyArray : Array α := Array.mkEmpty branching.toNat abbrev mul2Shift (i : USize) (shift : USize) : USize := i.shiftLeft shift