max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use #[] instead of Array.empty

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-08 16:23:06 -07:00
parent bfe4f5e7d3
commit d1ca45d83a
19 changed files with 50 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Data/ByteArray/Basic.lean
View file

@ -18,7 +18,7 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
namespace ByteArray
@[extern c inline "lean_mk_empty_byte_array(#1)"]
def mkEmpty (c : @& Nat) : ByteArray :=
{ data := Array.empty }
{ data := #[] }
def empty : ByteArray :=
mkEmpty 0

4
library/Init/Data/PersistentArray/Basic.lean
View file

@ -13,7 +13,7 @@ inductive PersistentArrayNode (α : Type u)
namespace PersistentArrayNode
instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf Array.empty⟩
instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf #[]⟩
def isNode {α} : PersistentArrayNode α → Bool
| node _ => true
@ -122,7 +122,7 @@ if t.size <= (mul2Shift 1 (t.shift + initShift)).toNat then
tailOff := t.size,
.. t }
else
{ tail := Array.empty,
{ tail := #[],
root := let n := mkEmptyArray.push t.root;
node (n.push (mkNewPath t.shift t.tail)),
shift := t.shift + initShift,

2
library/Init/Data/PersistentHashMap/Basic.lean
View file

@ -21,7 +21,7 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v)
| entries (es : Array (Entry α β Node)) : Node
| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node
instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries Array.empty⟩
instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
abbrev shift : USize := 5
abbrev branching : USize := USize.ofNat (2 ^ shift.toNat)

4
library/Init/Data/Stack/Basic.lean
View file

@ -11,14 +11,14 @@ import Init.Data.Int
universes u v w
structure Stack (α : Type u) :=
(vals : Array α := Array.empty)
(vals : Array α := #[])
namespace Stack
variable {α : Type u}
def empty : Stack α :=
{ vals := Array.empty }
{}
def isEmpty (s : Stack α) : Bool :=
s.vals.isEmpty

8
library/Init/Lean/Attributes.lean
View file

@ -35,7 +35,7 @@ IO.mkRef {}
constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := default _
def mkAttributeArrayRef : IO (IO.Ref (Array AttributeImpl)) :=
IO.mkRef Array.empty
IO.mkRef #[]
@[init mkAttributeArrayRef]
constant attributeArrayRef : IO.Ref (Array AttributeImpl) := default _
@ -153,7 +153,7 @@ do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension
addImportedFn := fun _ => pure {},
addEntryFn := fun (s : NameSet) n => s.insert n,
exportEntriesFn := fun es =>
let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
let r : Array Name := es.fold (fun a e => a.push e) #[];
r.qsort Name.quickLt,
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
};
@ -201,7 +201,7 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
addImportedFn := fun _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
};
@ -259,7 +259,7 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
addImportedFn := fun _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
};

2
library/Init/Lean/Compiler/IR/Basic.lean
View file

@ -339,7 +339,7 @@ partial def flattenAux : FnBody → Array FnBody → (Array FnBody) × FnBody
else flattenAux b.body (push r b)
def FnBody.flatten (b : FnBody) : (Array FnBody) × FnBody :=
flattenAux b Array.empty
flattenAux b #[]
partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
| a, i, b =>

4
library/Init/Lean/Compiler/IR/Borrow.lean
View file

@ -182,8 +182,8 @@ do s ← get;
ctx ← read;
match findEnvDecl ctx.env fn with
| some decl => pure decl.params
| none => pure Array.empty -- unreachable if well-formed input
| _ => pure Array.empty -- unreachable if well-formed input
| none => pure #[] -- unreachable if well-formed input
| _ => pure #[] -- unreachable if well-formed input
/- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=

18
library/Init/Lean/Compiler/IR/Boxing.lean
View file

@ -62,7 +62,7 @@ do let ps := decl.params;
else do
x ← mkFresh;
pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
(Array.empty, Array.empty);
(#[], #[]);
r ← mkFresh;
let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
body ←
@ -81,7 +81,7 @@ def mkBoxedVersion (decl : Decl) : Decl :=
def addBoxedVersions (env : Environment) (decls : Array Decl) : Array Decl :=
let boxedDecls := decls.foldl
(fun (newDecls : Array Decl) decl => if requiresBoxedVersion env decl then newDecls.push (mkBoxedVersion decl) else newDecls)
Array.empty;
#[];
decls ++ boxedDecls
/- Infer scrutinee type using `case` alternatives.
@ -120,7 +120,7 @@ structure BoxingState :=
we use auxDeclCache to avoid creating equivalent auxiliary declarations more than once when
processing the same IR declaration.
-/
(auxDecls : Array Decl := Array.empty)
(auxDecls : Array Decl := #[])
(auxDeclCache : AssocList FnBody Expr := AssocList.empty)
(nextAuxId : Nat := 1)
@ -143,7 +143,7 @@ def getJPParams (j : JoinPointId) : M (Array Param) :=
do localCtx ← getLocalContext;
match localCtx.getJPParams j with
| some ys => pure ys
| none => pure Array.empty -- unreachable, we assume the code is well formed
| none => pure #[] -- unreachable, we assume the code is well formed
def getDecl (fid : FunId) : M Decl :=
do ctx ← read;
match findEnvDecl' ctx.env fid ctx.decls with
@ -159,7 +159,7 @@ adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addLocal x
@[inline] def withJDecl {α : Type} (j : JoinPointId) (xs : Array Param) (v : FnBody) (k : M α) : M α :=
adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addJP j xs v, .. ctx }) k
/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c Array.empty`,
/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c #[]`,
and `x`'s type is not cheap to box (e.g., it is `UInt64), then return its value. -/
private def isExpensiveConstantValueBoxing (x : VarId) (xType : IRType) : M (Option Expr) :=
if !xType.isScalar then pure none -- We assume unboxing is always cheap
@ -200,8 +200,8 @@ do optVal ← isExpensiveConstantValueBoxing x xType;
| some v => pure v
| none => do
let auxName := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
let auxConst := Expr.fap auxName Array.empty;
let auxDecl := Decl.fdecl auxName Array.empty expectedType body;
let auxConst := Expr.fap auxName #[];
let auxDecl := Decl.fdecl auxName #[] expectedType body;
modify $ fun s => {
auxDecls := s.auxDecls.push auxDecl,
auxDeclCache := s.auxDeclCache.cons body auxConst,
@ -225,7 +225,7 @@ match x with
| _ => k x
@[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) :=
xs.miterate (Array.empty, Array.empty) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
xs.miterate (#[], #[]) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
let expected := typeFromIdx i.val;
let (xs, bs) := r;
match x with
@ -331,7 +331,7 @@ let decls := decls.foldl (fun (newDecls : Array Decl) (decl : Decl) =>
let newDecl := newDecl.elimDead;
newDecls.push newDecl
| d => newDecls.push d)
Array.empty;
#[];
addBoxedVersions env decls
end ExplicitBoxing

4
library/Init/Lean/Compiler/IR/CompilerM.lean
View file

@ -34,7 +34,7 @@ def Log.toString (log : Log) : String :=
log.format.pretty
structure CompilerState :=
(env : Environment) (log : Log := Array.empty)
(env : Environment) (log : Log := #[])
abbrev CompilerM := ReaderT Options (EState String CompilerState)
@ -76,7 +76,7 @@ private def mkEntryArray (decls : List Decl) : Array Decl :=
/- Remove duplicates by adding decls into a map -/
let map : HashMap Name Decl := {};
let map := decls.foldl (fun (map : HashMap Name Decl) decl => map.insert decl.name decl) map;
map.fold (fun a k v => a.push v) Array.empty
map.fold (fun a k v => a.push v) #[]
def mkDeclMapExtension : IO (SimplePersistentEnvExtension Decl DeclMap) :=
registerSimplePersistentEnvExtension {

2
library/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -27,7 +27,7 @@ structure Context :=
(modName : Name)
(jpMap : JPParamsMap := {})
(mainFn : FunId := default _)
(mainParams : Array Param := Array.empty)
(mainParams : Array Param := #[])
abbrev M := ReaderT Context (EState String String)

10
library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
View file

@ -90,7 +90,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
/- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
eraseProjIncForAux y bs (mkArray n none) Array.empty
eraseProjIncForAux y bs (mkArray n none) #[]
/- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/
partial def reuseToCtor (x : VarId) : FnBody → FnBody
@ -251,7 +251,7 @@ do let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
let bSlow := mkSlowPath x y mask b;
bFast ← mkFastPath x y mask b;
/- We only optimize recursively the fast. -/
bFast ← mainFn bFast Array.empty;
bFast ← mainFn bFast #[];
c ← mkFresh;
let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
pure $ reshape bs b
@ -263,10 +263,10 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
else
searchAndExpand b (push bs d)
| FnBody.jdecl j xs v b, bs => do
v ← searchAndExpand v Array.empty;
v ← searchAndExpand v #[];
searchAndExpand b (push bs (FnBody.jdecl j xs v FnBody.nil))
| FnBody.case tid x xType alts, bs => do
alts ← alts.mmap $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b Array.empty;
alts ← alts.mmap $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b #[];
pure $ reshape bs (FnBody.case tid x xType alts)
| b, bs =>
if b.isTerminal then pure $ reshape bs b
@ -278,7 +278,7 @@ match d with
| (Decl.fdecl f xs t b) =>
let m := mkProjMap d;
let nextIdx := d.maxIndex + 1;
let b := (searchAndExpand b Array.empty { projMap := m }).run' nextIdx;
let b := (searchAndExpand b #[] { projMap := m }).run' nextIdx;
Decl.fdecl f xs t b
| d => d

2
library/Init/Lean/Compiler/IR/PushProj.lean
View file

@ -45,7 +45,7 @@ partial def FnBody.pushProj : FnBody → FnBody
match term with
| FnBody.case tid x xType alts =>
let altsF := alts.map $ fun alt => alt.body.freeIndices;
let (bs, alts) := pushProjs bs alts altsF Array.empty (mkIndexSet x.idx);
let (bs, alts) := pushProjs bs alts altsF #[] (mkIndexSet x.idx);
let alts := alts.map $ fun alt => alt.modifyBody FnBody.pushProj;
let term := FnBody.case tid x xType alts;
reshape bs term

2
library/Init/Lean/Compiler/IR/RC.lean
View file

@ -43,7 +43,7 @@ match ctx.varMap.find x with
def getJPParams (ctx : Context) (j : JoinPointId) : Array Param :=
match ctx.localCtx.getJPParams j with
| some ps => ps
| none => Array.empty -- unreachable in well-formed code
| none => #[] -- unreachable in well-formed code
def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet :=
match ctx.jpLiveVarMap.find j with

2
library/Init/Lean/Compiler/IR/UnreachBranches.lean
View file

@ -50,7 +50,7 @@ partial def merge : Value → Value → Value
| top, _ => top
| _, top => top
| v₁@(ctor i₁ vs₁), v₂@(ctor i₂ vs₂) =>
if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (fun i r => r.push (merge (vs₁.get! i) (vs₂.get! i))) Array.empty
if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (fun i r => r.push (merge (vs₁.get! i) (vs₂.get! i))) #[]
else choice [v₁, v₂]
| choice vs₁, choice vs₂ => choice $ vs₁.foldl (addChoice merge) vs₂
| choice vs, v => choice $ addChoice merge vs v

2
library/Init/Lean/Elaborator/Basic.lean
View file

@ -199,7 +199,7 @@ do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvE
-- TODO: populate table with `es`
pure table,
addEntryFn := fun (s : σ) _ => s, -- TODO
exportEntriesFn := fun _ => Array.empty, -- TODO
exportEntriesFn := fun _ => #[], -- TODO
statsFn := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
};
let attrImpl : AttributeImpl := {

6
library/Init/Lean/Elaborator/PreTerm.lean
View file

@ -167,12 +167,12 @@ match b.getKind with
| _ => throw "unknown binder default value annotation";
decl ← mkLocalDecl id type;
pure (mkLocal decl)
| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure Array.empty
| `Lean.Parser.Term.instBinder => do runIO (IO.println $ ">> inst " ++ (toString b)); pure Array.empty
| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure #[]
| `Lean.Parser.Term.instBinder => do runIO (IO.println $ ">> inst " ++ (toString b)); pure #[]
| _ => throw "unknown binder kind"
private def processBinders (bs : Array (Syntax Expr)) : Elab (Array PreTerm) :=
bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) Array.empty
bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) #[]
@[builtinPreTermElab «forall»] def convertForall : PreTermElab :=
fun n => do

6
library/Init/Lean/Parser/Parser.lean
View file

@ -114,7 +114,7 @@ match e₂ with
end Error
structure ParserState :=
(stxStack : Array Syntax := Array.empty)
(stxStack : Array Syntax := #[])
(pos : String.Pos := 0)
(cache : ParserCache := {})
(errorMsg : Option Error := none)
@ -1350,7 +1350,7 @@ do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnv
name := `_tokens_,
addImportedFn := fun es => mkImportedTokenTable es,
addEntryFn := fun (s : TokenTable) _ => s, -- TODO
exportEntriesFn := fun _ => Array.empty, -- TODO
exportEntriesFn := fun _ => #[], -- TODO
statsFn := fun _ => fmt "token table attribute" -- TODO
};
let attrImpl : AttributeImpl := {
@ -1520,7 +1520,7 @@ do ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerP
-- TODO: populate table with `es`
pure table,
addEntryFn := fun (s : ParsingTables) _ => s, -- TODO
exportEntriesFn := fun _ => Array.empty, -- TODO
exportEntriesFn := fun _ => #[], -- TODO
statsFn := fun _ => fmt "parser attribute" -- TODO
};
let attrImpl : AttributeImpl := {

4
library/Init/Lean/Position.lean
View file

@ -42,7 +42,7 @@ structure FileMap :=
namespace FileMap
instance : Inhabited FileMap :=
⟨{ source := "", positions := Array.empty, lines := Array.empty }⟩
⟨{ source := "", positions := #[], lines := #[] }⟩
private partial def ofStringAux (s : String) : String.Pos → Nat → Array String.Pos → Array Nat → FileMap
| i, line, ps, lines =>
@ -54,7 +54,7 @@ private partial def ofStringAux (s : String) : String.Pos → Nat → Array Stri
else ofStringAux i line ps lines
def ofString (s : String) : FileMap :=
ofStringAux s 0 1 (Array.empty.push 0) (Array.empty.push 1)
ofStringAux s 0 1 (#[0]) (#[1])
private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos : String.Pos) : String.Pos → Nat → Nat
| i, c =>

16
library/Init/Lean/TypeClass/Synth.lean
View file

@ -60,7 +60,7 @@ instance GeneratorNode.Inhabited : Inhabited GeneratorNode :=
structure TableEntry : Type :=
(waiters : Array Waiter)
(answers : Array TypedExpr := Array.empty)
(answers : Array TypedExpr := #[])
structure TCState : Type :=
(env : Environment)
@ -134,8 +134,8 @@ partial def introduceLocals : Nat → LocalContext → Array Expr → Expr → L
def tryResolve (ctx : Context) (futureAnswer : TypedExpr) (instTE : TypedExpr) : TCMethod (Option (Context × List Expr)) :=
do let ⟨mvar, mvarType⟩ := futureAnswer;
let ⟨instVal, instType⟩ := instTE;
let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} Array.empty mvarType;
let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType Array.empty;
let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} #[] mvarType;
let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType #[];
match (Context.eUnify mvarType instType *> Context.eUnify mvar (lctx.mkLambda locals instVal)).run ctx with
| EState.Result.error msg _ => pure none
| EState.Result.ok _ ctx => pure $ some $ (ctx, newMVars.toList) -- TODO(dselsam): rm toList
@ -269,21 +269,21 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr
def preprocessForOutParams (env : Environment) (goalType : Expr) : Context × Expr × Array (Level × Level) × Array (Expr × Expr) :=
if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName
then ({}, goalType, Array.empty, Array.empty)
then ({}, goalType, #[], #[])
else
let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} Array.empty goalType;
let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} #[] goalType;
let f := goalType.getAppFn;
let fArgs := goalType.getAppArgs;
if !(f.isConst && isClass env f.constName)
then ({}, goalType, Array.empty, Array.empty)
then ({}, goalType, #[], #[])
else
let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} Array.empty Array.empty;
let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} #[] #[];
let f := if uReplacements.isEmpty then f else Expr.const f.constName CLevels.toList;
let fType :=
match env.find f.constName with
| none => panic! "found constant not in the environment"
| some cInfo => cInfo.instantiateTypeUnivParams CLevels.toList;
let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs ctx Array.empty Array.empty;
let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs ctx #[] #[];
(ctx, lctx.mkForall locals $ mkApp f fArgs.toList, uReplacements, eReplacements)
def synth (goalType₀ : Expr) (fuel : Nat := 100000) : TCMethod Expr :=