From 2ebcf29cde83fd29aa3ad5bf360fc6e2428cc1a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Jul 2022 15:12:05 -0700 Subject: [PATCH] chore: use `a[i]!` for array accesses that may panic --- src/Init/Meta.lean | 2 +- src/Init/Notation.lean | 2 +- src/Init/NotationExtra.lean | 6 +- src/Lean/Compiler/IR/Basic.lean | 2 +- src/Lean/Compiler/IR/Borrow.lean | 8 +- src/Lean/Compiler/IR/Boxing.lean | 6 +- src/Lean/Compiler/IR/ElimDeadBranches.lean | 14 ++-- src/Lean/Compiler/IR/EmitC.lean | 40 +++++----- src/Lean/Compiler/IR/ExpandResetReuse.lean | 2 +- src/Lean/Compiler/IR/RC.lean | 16 ++-- src/Lean/Compiler/IR/SimpCase.lean | 6 +- src/Lean/Data/Position.lean | 6 +- src/Lean/Elab/App.lean | 14 ++-- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 4 +- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/Deriving/BEq.lean | 14 ++-- src/Lean/Elab/Deriving/Basic.lean | 2 +- src/Lean/Elab/Deriving/DecEq.lean | 18 ++--- src/Lean/Elab/Deriving/FromToJson.lean | 56 ++++++------- src/Lean/Elab/Deriving/Hashable.lean | 10 +-- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Deriving/Ord.lean | 8 +- src/Lean/Elab/Deriving/Repr.lean | 14 ++-- src/Lean/Elab/Deriving/SizeOf.lean | 2 +- src/Lean/Elab/Deriving/Util.lean | 12 +-- src/Lean/Elab/Do.lean | 14 ++-- src/Lean/Elab/ElabRules.lean | 2 +- src/Lean/Elab/Extra.lean | 12 +-- src/Lean/Elab/Inductive.lean | 40 +++++----- src/Lean/Elab/LetRec.lean | 6 +- src/Lean/Elab/MacroRules.lean | 2 +- src/Lean/Elab/Match.lean | 22 ++--- src/Lean/Elab/MutualDef.lean | 22 ++--- src/Lean/Elab/Open.lean | 4 +- src/Lean/Elab/PatternVar.lean | 6 +- src/Lean/Elab/PreDefinition/Basic.lean | 2 +- src/Lean/Elab/PreDefinition/Eqns.lean | 4 +- src/Lean/Elab/PreDefinition/Main.lean | 6 +- src/Lean/Elab/PreDefinition/MkInhabitant.lean | 2 +- .../Elab/PreDefinition/Structural/BRecOn.lean | 18 ++--- .../Elab/PreDefinition/Structural/Eqns.lean | 4 +- .../PreDefinition/Structural/IndPred.lean | 6 +- .../Elab/PreDefinition/Structural/Main.lean | 4 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 10 +-- src/Lean/Elab/PreDefinition/WF/Fix.lean | 40 +++++----- src/Lean/Elab/PreDefinition/WF/Ite.lean | 6 +- src/Lean/Elab/PreDefinition/WF/Main.lean | 14 ++-- .../Elab/PreDefinition/WF/PackDomain.lean | 24 +++--- .../Elab/PreDefinition/WF/PackMutual.lean | 46 +++++------ src/Lean/Elab/PreDefinition/WF/Rel.lean | 12 +-- .../PreDefinition/WF/TerminationHint.lean | 4 +- src/Lean/Elab/Quotation.lean | 6 +- src/Lean/Elab/StructInst.lean | 10 +-- src/Lean/Elab/Structure.lean | 2 +- src/Lean/Elab/Syntax.lean | 8 +- src/Lean/Elab/SyntheticMVars.lean | 8 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 8 +- src/Lean/Elab/Tactic/Conv/Congr.lean | 4 +- src/Lean/Elab/Tactic/Induction.lean | 26 +++--- src/Lean/Elab/Tactic/Match.lean | 1 - src/Lean/Elab/Tactic/Rewrite.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Elab/Tactic/Split.lean | 2 +- src/Lean/Environment.lean | 4 +- src/Lean/Level.lean | 2 +- src/Lean/LocalContext.lean | 2 +- src/Lean/Meta/ACLt.lean | 16 ++-- src/Lean/Meta/AppBuilder.lean | 2 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/CasesOn.lean | 6 +- src/Lean/Meta/Check.lean | 10 +-- src/Lean/Meta/Closure.lean | 2 +- src/Lean/Meta/CongrTheorems.lean | 46 +++++------ src/Lean/Meta/DiscrTree.lean | 6 +- src/Lean/Meta/ExprDefEq.lean | 24 +++--- src/Lean/Meta/ForEachExpr.lean | 4 +- src/Lean/Meta/FunInfo.lean | 2 +- src/Lean/Meta/IndPredBelow.lean | 58 +++++++------- src/Lean/Meta/InferType.lean | 2 +- src/Lean/Meta/Match/CaseArraySizes.lean | 2 +- src/Lean/Meta/Match/Match.lean | 14 ++-- src/Lean/Meta/Match/MatchEqs.lean | 34 ++++---- src/Lean/Meta/Match/MatcherInfo.lean | 2 +- src/Lean/Meta/RecursorInfo.lean | 6 +- src/Lean/Meta/Reduce.lean | 6 +- src/Lean/Meta/SizeOf.lean | 14 ++-- src/Lean/Meta/Tactic/AC/Main.lean | 8 +- src/Lean/Meta/Tactic/Apply.lean | 10 +-- src/Lean/Meta/Tactic/Assert.lean | 2 +- src/Lean/Meta/Tactic/Cases.lean | 6 +- src/Lean/Meta/Tactic/ElimInfo.lean | 10 +-- src/Lean/Meta/Tactic/Generalize.lean | 10 +-- src/Lean/Meta/Tactic/Induction.lean | 8 +- src/Lean/Meta/Tactic/Injection.lean | 2 +- src/Lean/Meta/Tactic/Intro.lean | 4 +- .../Meta/Tactic/LinearArith/Nat/Basic.lean | 2 +- src/Lean/Meta/Tactic/LinearArith/Solver.lean | 4 +- src/Lean/Meta/Tactic/Simp/Main.lean | 10 +-- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 2 +- src/Lean/Meta/Tactic/Split.lean | 18 ++--- src/Lean/Meta/Tactic/Subst.lean | 8 +- src/Lean/Meta/WHNF.lean | 6 +- src/Lean/MetavarContext.lean | 12 +-- src/Lean/MonadEnv.lean | 2 +- src/Lean/ParserCompiler.lean | 4 +- .../PrettyPrinter/Delaborator/Builtins.lean | 16 ++-- .../PrettyPrinter/Delaborator/SubExpr.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 80 +++++++++---------- src/Lean/Server/FileWorker.lean | 2 +- src/Lean/Server/Rpc/Deriving.lean | 4 +- src/Lean/Syntax.lean | 6 +- 112 files changed, 592 insertions(+), 593 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index d2c3cc9339..b90b2cc7d8 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -348,7 +348,7 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) : none else let i := i - 1 - let v := a[i] + let v := a[i]! match f v with | some v => some <| a.set! i v | none => updateLast a f i diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 9ada407268..d3b4d503c7 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -219,7 +219,7 @@ macro_rules match i, skip with | 0, _ => pure result | i+1, true => expandListLit i false result - | i+1, false => expandListLit i true (← ``(List.cons $(⟨elems.elemsAndSeps[i]⟩) $result)) + | i+1, false => expandListLit i true (← ``(List.cons $(⟨elems.elemsAndSeps[i]!⟩) $result)) if elems.elemsAndSeps.size < 64 then expandListLit elems.elemsAndSeps.size false (← ``(List.nil)) else diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 1dd7027cca..979cee0050 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -26,7 +26,7 @@ def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type match i with | 0 => pure acc | i+1 => - let ident := idents[i][0] + let ident := idents[i]![0] let acc ← match ident.isIdent, type? with | true, none => `($combinator fun $ident => $acc) | true, some type => `($combinator fun $ident:ident : $type => $acc) @@ -40,8 +40,8 @@ def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body match i with | 0 => pure acc | i+1 => - let idents := binders[i][1].getArgs - let type := binders[i][3] + let idents := binders[i]![1].getArgs + let type := binders[i]![3] loop i (← expandExplicitBindersAux combinator idents (some type) acc) loop binders.size body diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index a56b4abde6..16199b9730 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -572,7 +572,7 @@ def addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option In else let mut ρ := ρ for i in [:ps₁.size] do - ρ ← addParamRename ρ ps₁[i] ps₂[i] + ρ ← addParamRename ρ ps₁[i]! ps₂[i]! pure ρ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index 5c4834f56d..56988b9d79 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -205,8 +205,8 @@ def getParamInfo (k : ParamMap.Key) : M (Array Param) := do /- 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 := xs.size.forM fun i => do - let x := xs[i] - let p := ps[i] + let x := xs[i]! + let p := ps[i]! unless p.borrow do ownArg x /- For each xs[i], if xs[i] is owned, then mark ps[i] as owned. @@ -216,8 +216,8 @@ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit := "break" the tail call. -/ def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit := xs.size.forM fun i => do - let x := xs[i] - let p := ps[i] + let x := xs[i]! + let p := ps[i]! match x with | Arg.var x => if (← isOwned x) then ownVar p.x | _ => pure () diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean index c4b50dac39..3a944a9b32 100644 --- a/src/Lean/Compiler/IR/Boxing.lean +++ b/src/Lean/Compiler/IR/Boxing.lean @@ -50,8 +50,8 @@ def mkBoxedVersionAux (decl : Decl) : N Decl := do let ps := decl.params let qs ← ps.mapM fun _ => do let x ← N.mkFresh; pure { x := x, ty := IRType.object, borrow := false : Param } let (newVDecls, xs) ← qs.size.foldM (init := (#[], #[])) fun i (newVDecls, xs) => do - let p := ps[i] - let q := qs[i] + let p := ps[i]! + let q := qs[i]! if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x)) else @@ -244,7 +244,7 @@ def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Arr return (xs', bs) @[inline] def castArgsIfNeeded (xs : Array Arg) (ps : Array Param) (k : Array Arg → M FnBody) : M FnBody := do - let (ys, bs) ← castArgsIfNeededAux xs fun i => ps[i].ty + let (ys, bs) ← castArgsIfNeededAux xs fun i => ps[i]!.ty let b ← k ys pure (reshape bs b) diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index dc6d02c127..30660a3b17 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -62,7 +62,7 @@ partial def merge (v₁ v₂ : Value) : Value := | top, _ => top | _, top => top | v₁@(ctor i₁ vs₁), v₂@(ctor i₂ vs₂) => - if i₁ == i₂ then ctor i₁ <| vs₁.size.fold (init := #[]) fun i r => r.push (merge vs₁[i] vs₂[i]) + if i₁ == i₂ then ctor i₁ <| vs₁.size.fold (init := #[]) fun i r => r.push (merge vs₁[i]! vs₂[i]!) else choice [v₁, v₂] | choice vs₁, choice vs₂ => choice <| vs₁.foldl (addChoice merge) vs₂ | choice vs, v => choice <| addChoice merge vs v @@ -158,7 +158,7 @@ open Value def findVarValue (x : VarId) : M Value := do let ctx ← read let s ← get - let assignment := s.assignments[ctx.currFnIdx] + let assignment := s.assignments[ctx.currFnIdx]! return assignment.findD x bot def findArgValue (arg : Arg) : M Value := @@ -213,8 +213,8 @@ def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do let ctx ← read let currFnIdx := ctx.currFnIdx ys.size.foldM (init := false) fun i r => do - let y := ys[i] - let x := xs[i] + let y := ys[i]! + let x := xs[i]! let yVal ← findVarValue y.x let xVal ← findArgValue x let newVal := merge yVal xVal @@ -270,7 +270,7 @@ def inferStep : M Bool := do let ctx ← read modify fun s => { s with assignments := ctx.decls.map fun _ => {} } ctx.decls.size.foldM (init := false) fun idx modified => do - match ctx.decls[idx] with + match ctx.decls[idx]! with | Decl.fdecl (xs := ys) (body := b) .. => do let s ← get let currVals := s.funVals[idx] @@ -324,8 +324,8 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do let assignments := s.assignments modify fun s => let env := decls.size.fold (init := s.env) fun i env => - addFunctionSummary env decls[i].name funVals[i] + addFunctionSummary env decls[i]!.name funVals[i] { s with env := env } - return decls.mapIdx fun i decl => elimDead assignments[i] decl + return decls.mapIdx fun i decl => elimDead assignments[i]! decl end Lean.IR diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 3536eed947..267951229c 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -109,7 +109,7 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U else ps.size.forM fun i => do if i > 0 then emit ", " - emit (toCType ps[i].ty) + emit (toCType ps[i]!.ty) emit ")" emitLn ";" @@ -271,8 +271,8 @@ def emitTag (x : VarId) (xType : IRType) : M Unit := do def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) := if alts.size != 2 then none - else match alts[0] with - | Alt.ctor c b => some (c.cidx, b, alts[1].body) + else match alts[0]! with + | Alt.ctor c b => some (c.cidx, b, alts[1]!.body) | _ => none def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do @@ -322,8 +322,8 @@ def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit := do let ps ← getJPParams j unless xs.size == ps.size do throw "invalid goto" xs.size.forM fun i => do - let p := ps[i] - let x := xs[i] + let p := ps[i]! + let x := xs[i]! emit p.x; emit " = "; emitArg x; emitLn ";" emit "goto "; emit j; emitLn ";" @@ -333,7 +333,7 @@ def emitLhs (z : VarId) : M Unit := do def emitArgs (ys : Array Arg) : M Unit := ys.size.forM fun i => do if i > 0 then emit ", " - emitArg ys[i] + emitArg ys[i]! def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit := do if usize == 0 then emit ssize @@ -346,7 +346,7 @@ def emitAllocCtor (c : CtorInfo) : M Unit := do def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit := ys.size.forM fun i => do - emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg ys[i]; emitLn ");" + emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg ys[i]!; emitLn ");" def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit := do emitLhs z; @@ -399,11 +399,11 @@ def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M -- We must remove irrelevant arguments to extern calls. discard <| ys.size.foldM (fun i (first : Bool) => - if ps[i].ty.isIrrelevant then + if ps[i]!.ty.isIrrelevant then pure first else do unless first do emit ", " - emitArg ys[i] + emitArg ys[i]! pure false) true emitLn ");" @@ -431,7 +431,7 @@ def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do let arity := decl.params.size; emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");"; ys.size.forM fun i => do - let y := ys[i] + let y := ys[i]! emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");" def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit := @@ -548,8 +548,8 @@ That is, we have def overwriteParam (ps : Array Param) (ys : Array Arg) : Bool := let n := ps.size; n.any fun i => - let p := ps[i] - (i+1, n).anyI fun j => paramEqArg p ys[j] + let p := ps[i]! + (i+1, n).anyI fun j => paramEqArg p ys[j]! def emitTailCall (v : Expr) : M Unit := match v with @@ -560,19 +560,19 @@ def emitTailCall (v : Expr) : M Unit := if overwriteParam ps ys then emitLn "{" ps.size.forM fun i => do - let p := ps[i] - let y := ys[i] + let p := ps[i]! + let y := ys[i]! unless paramEqArg p y do emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";" ps.size.forM fun i => do - let p := ps[i] - let y := ys[i] + let p := ps[i]! + let y := ys[i]! unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";" emitLn "}" else ys.size.forM fun i => do - let p := ps[i] - let y := ys[i] + let p := ps[i]! + let y := ys[i]! unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";" emitLn "goto _start;" | _ => throw "bug at emitTailCall" @@ -659,7 +659,7 @@ def emitDeclAux (d : Decl) : M Unit := do else xs.size.forM fun i => do if i > 0 then emit ", " - let x := xs[i] + let x := xs[i]! emit (toCType x.ty); emit " "; emit x.x emit ")" else @@ -667,7 +667,7 @@ def emitDeclAux (d : Decl) : M Unit := do emitLn " {"; if xs.size > closureMaxArgs && isBoxedName d.name then xs.size.forM fun i => do - let x := xs[i] + let x := xs[i]! emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];" emitLn "_start:"; withReader (fun ctx => { ctx with mainFn := f, mainParams := xs }) (emitFnBody b); diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index 9b0b04c155..feb2201b11 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean @@ -61,7 +61,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke | (FnBody.vdecl _ _ (Expr.uproj _ _) _) => keepInstr b | (FnBody.inc z n c p _) => if n == 0 then done () else - let b' := bs[bs.size - 2] + let b' := bs[bs.size - 2]! match b' with | (FnBody.vdecl w _ (Expr.proj i x) _) => if w == z && y == x then diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 09d56f4079..7b4a7b0515 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -76,20 +76,20 @@ private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) /- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/ private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool := - let x := xs[i] - i.all fun j => xs[j] != x + let x := xs[i]! + i.all fun j => xs[j]! != x /- Return true if `x` also occurs in `ys` in a position that is not consumed. That is, it is also passed as a borrow reference. -/ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool := ys.size.any fun i => - let y := ys[i] + let y := ys[i]! match y with | Arg.irrelevant => false | Arg.var y => x == y && !consumeParamPred i private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool := - isBorrowParamAux x ys fun i => not ps[i].borrow + isBorrowParamAux x ys fun i => not ps[i]!.borrow /- Return `n`, the number of times `x` is consumed. @@ -98,14 +98,14 @@ Return `n`, the number of times `x` is consumed. -/ private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat := ys.size.fold (init := 0) fun i n => - let y := ys[i] + let y := ys[i]! match y with | Arg.irrelevant => n | Arg.var y => if x == y && consumeParamPred i then n+1 else n private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody := xs.size.fold (init := b) fun i b => - let x := xs[i] + let x := xs[i]! match x with | Arg.irrelevant => b | Arg.var x => @@ -122,12 +122,12 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : addInc ctx x b numIncs private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody := - addIncBeforeAux ctx xs (fun i => not ps[i].borrow) b liveVarsAfter + addIncBeforeAux ctx xs (fun i => not ps[i]!.borrow) b liveVarsAfter /- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application. -/ private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody := xs.size.fold (init := b) fun i b => - match xs[i] with + match xs[i]! with | Arg.irrelevant => b | Arg.var x => /- We must add a `dec` if `x` must be consumed, it is alive after the application, diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean index c869f121ee..11053f2dde 100644 --- a/src/Lean/Compiler/IR/SimpCase.lean +++ b/src/Lean/Compiler/IR/SimpCase.lean @@ -20,17 +20,17 @@ private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do let aBody := (alts.get! i).body let mut n := 1 for j in [i+1:alts.size] do - if alts[j].body == aBody then + if alts[j]!.body == aBody then n := n+1 return n private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do - let mut maxAlt := alts[0] + let mut maxAlt := alts[0]! let mut max := getOccsOf alts 0 for i in [1:alts.size] do let curr := getOccsOf alts i if curr > max then - maxAlt := alts[i] + maxAlt := alts[i]! max := curr return (maxAlt, max) diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index 98cf617b2a..86a3331658 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -46,8 +46,8 @@ 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 } else - let c := s.get i; - let i := s.next i; + let c := s.get i + let i := s.next i if c == '\n' then loop i (line+1) (ps.push i) (lines.push (line+1)) else loop i line ps lines loop 0 1 (#[0]) (#[1]) @@ -60,7 +60,7 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position := if i == pos || str.atEnd i then c else toColumn (str.next i) (c+1) let rec loop (b e : Nat) := - let posB := ps[b] + let posB := ps[b]! if e == b + 1 then { line := lines.get! b, column := toColumn posB 0 } else let m := (b + e) / 2; diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 3f16e5abbc..6a0b3071ce 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -339,9 +339,9 @@ private def anyNamedArgDependsOnCurrent : M Bool := do return false else forallTelescopeReducing s.fType fun xs _ => do - let curr := xs[0] + let curr := xs[0]! for i in [1:xs.size] do - let xDecl ← getLocalDecl xs[i].fvarId! + let xDecl ← getLocalDecl xs[i]!.fvarId! if s.namedArgs.any fun arg => arg.name == xDecl.userName then if (← getMCtx).localDeclDependsOn xDecl curr.fvarId! then return true @@ -583,7 +583,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L if idx - 1 < numFields then if isStructure env structName then let fieldNames := getStructureFields env structName - return LValResolution.projFn structName structName fieldNames[idx - 1] + return LValResolution.projFn structName structName fieldNames[idx - 1]! else /- `structName` was declared using `inductive` command. So, we don't projection functions for it. Thus, we use `Expr.proj` -/ @@ -708,7 +708,7 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar let mut argIdx := 0 -- position of the next explicit argument let mut remainingNamedArgs := namedArgs for i in [:xs.size] do - let x := xs[i] + let x := xs[i]! let xDecl ← getLocalDecl x.fvarId! /- If there is named argument with name `xDecl.userName`, then we skip it. -/ match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with @@ -726,7 +726,7 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar /- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible if there isn't an argument with the same name occurring before it. -/ for j in [:i] do - let prev := xs[j] + let prev := xs[j]! let prevDecl ← getLocalDecl prev.fvarId! if prevDecl.userName == xDecl.userName then throwError "invalid field notation, function '{fullName}' has argument with the expected type{indentExpr type}\nbut it cannot be used" @@ -977,11 +977,11 @@ private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do let candidates ← elabAppFn f [] namedArgs args expectedType? (explicit := false) (ellipsis := ellipsis) (overloaded := false) #[] if candidates.size == 1 then - applyResult candidates[0] + applyResult candidates[0]! else let successes ← getSuccesses candidates if successes.size == 1 then - applyResult successes[0] + applyResult successes[0]! else if successes.size > 1 then let msgs : Array MessageData ← successes.mapM fun success => do match success with diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 98a009eaab..c9d6d6b29a 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -204,7 +204,7 @@ def elabBinders (binders : Array Syntax) (k : Array Expr → TermElabM α) : Ter /-- Same as `elabBinder` with a single binder.-/ def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α := - elabBinders #[binder] fun fvars => x fvars[0] + elabBinders #[binder] fun fvars => x fvars[0]! @[builtinTermElab «forall»] def elabForall : TermElab := fun stx _ => match stx with diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 96717f897a..e61b5ab24c 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -48,7 +48,7 @@ are turned into a new anonymous constructor application. For example, let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do let mut n := 0 for i in [cinfo.numParams:xs.size] do - if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then + if (← getFVarLocalDecl xs[i]!).binderInfo.isExplicit then n := n + 1 return n let args := args.getElems @@ -172,7 +172,7 @@ partial def mkPairs (elems : Array Term) : MacroM Term := let rec loop (i : Nat) (acc : Term) := do if i > 0 then let i := i - 1 - let elem := elems[i] + let elem := elems[i]! let acc ← `(Prod.mk $elem $acc) loop i acc else diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 13ff5c20b6..fc5be538dd 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -160,7 +160,7 @@ def getTerminationHints (stx : Syntax) : TerminationHints := let k := decl.getKind if k == ``Parser.Command.def || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then let args := decl.getArgs - { terminationBy? := args[args.size - 2].getOptional?, decreasingBy? := args[args.size - 1].getOptional? } + { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? } else {} diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 91d896570f..3c1a1898cd 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -47,7 +47,7 @@ where ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + 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 (← `(_)) @@ -69,8 +69,8 @@ where return alts def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do - let auxFunName := ctx.auxFunNames[i] - let indVal := ctx.typeInfos[i] + let auxFunName := ctx.auxFunNames[i]! + let indVal := ctx.typeInfos[i]! let header ← mkBEqHeader indVal let mut body ← mkMatch header indVal auxFunName if ctx.usePartial then @@ -92,13 +92,13 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "beq" declNames[0] + let ctx ← mkContext "beq" declNames[0]! let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames) trace[Elab.Deriving.beq] "\n{cmds}" return cmds private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do - let auxFunName := ctx.auxFunNames[0] + let auxFunName := ctx.auxFunNames[0]! `(private def $(mkIdent auxFunName):ident (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx) private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do @@ -110,8 +110,8 @@ private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do open Command def mkBEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do - if declNames.size == 1 && (← isEnumType declNames[0]) then - let cmds ← liftTermElabM none <| mkBEqEnumCmd declNames[0] + if declNames.size == 1 && (← isEnumType declNames[0]!) then + let cmds ← liftTermElabM none <| mkBEqEnumCmd declNames[0]! cmds.forM elabCommand return true else if (← declNames.allM isInductive) && declNames.size > 0 then diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 4a72b66b28..157cb03a19 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -52,7 +52,7 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla let className ← resolveGlobalConstNoOverloadWithInfo cls withRef cls do if declNames.size == 1 && args?.isNone then - if (← tryApplyDefHandler className declNames[0]) then + if (← tryApplyDefHandler className declNames[0]!) then return () applyDerivingHandlers className declNames args? catch ex => diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 4820dc89d4..5884fc972d 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -57,7 +57,7 @@ where ctorArgs2 := ctorArgs2.push (← `(_)) let mut todo := #[] for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + 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 (← `(_)) @@ -82,12 +82,12 @@ where return alts def mkAuxFunction (ctx : Context) : TermElabM Syntax := do - let auxFunName := ctx.auxFunNames[0] - let indVal :=ctx.typeInfos[0] + let auxFunName := ctx.auxFunNames[0]! + let indVal :=ctx.typeInfos[0]! let header ← mkDecEqHeader indVal let mut body ← mkMatch header indVal auxFunName let binders := header.binders - let type ← `(Decidable ($(mkIdent header.targetNames[0]) = $(mkIdent header.targetNames[1]))) + let type ← `(Decidable ($(mkIdent header.targetNames[0]!) = $(mkIdent header.targetNames[1]!))) `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term) def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do @@ -115,9 +115,9 @@ partial def mkEnumOfNat (declName : Name) : MetaM Unit := do let cond := mkConst ``cond [levelZero] let rec mkDecTree (low high : Nat) : Expr := if low + 1 == high then - mkConst ctors[low] + mkConst ctors[low]! else if low + 2 == high then - mkApp4 cond enumType (mkApp2 (mkConst ``Nat.beq) n (mkRawNatLit low)) (mkConst ctors[low]) (mkConst ctors[low+1]) + mkApp4 cond enumType (mkApp2 (mkConst ``Nat.beq) n (mkRawNatLit low)) (mkConst ctors[low]!) (mkConst ctors[low+1]!) else let mid := (low + high)/2 let lowBranch := mkDecTree low mid @@ -176,11 +176,11 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do def mkDecEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size != 1 then return false -- mutually inductive types are not supported yet - else if (← isEnumType declNames[0]) then - mkDecEqEnum declNames[0] + else if (← isEnumType declNames[0]!) then + mkDecEqEnum declNames[0]! return true else - mkDecEq declNames[0] + mkDecEq declNames[0]! builtin_initialize registerBuiltinDerivingHandler `DecidableEq mkDecEqInstanceHandler diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index b4f63dcbdd..32872a1207 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -21,31 +21,31 @@ def mkJsonField (n : Name) : Bool × Term := def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size == 1 then - if isStructure (← getEnv) declNames[0] then + if isStructure (← getEnv) declNames[0]! then let cmds ← liftTermElabM none <| do - let ctx ← mkContext "toJson" declNames[0] - let header ← mkHeader ``ToJson 1 ctx.typeInfos[0] - let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false) + let ctx ← mkContext "toJson" declNames[0]! + let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]! + let fields := getStructureFieldsFlattened (← getEnv) declNames[0]! (includeSubobjectFields := false) let fields ← fields.mapM fun field => do let (isOptField, nm) := mkJsonField field - if isOptField then ``(opt $nm $(mkIdent <| header.targetNames[0] ++ field)) - else ``([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))]) - let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:bracketedBinder* := + if isOptField then ``(opt $nm $(mkIdent <| header.targetNames[0]! ++ field)) + else ``([($nm, toJson $(mkIdent <| header.targetNames[0]! ++ field))]) + let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* := mkObj <| List.join [$fields,*]) return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson declNames) cmds.forM elabCommand return true else - let indVal ← getConstInfoInduct declNames[0] + let indVal ← getConstInfoInduct declNames[0]! let cmds ← liftTermElabM none <| do - let ctx ← mkContext "toJson" declNames[0] - let toJsonFuncId := mkIdent ctx.auxFunNames[0] + let ctx ← mkContext "toJson" declNames[0]! + let toJsonFuncId := mkIdent ctx.auxFunNames[0]! -- Return syntax to JSONify `id`, either via `ToJson` or recursively -- if `id`'s type is the type we're deriving for. let mkToJson (id : Ident) (type : Expr) : TermElabM Term := do if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident) else ``(toJson $id:ident) - let header ← mkHeader ``ToJson 1 ctx.typeInfos[0] + let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]! let discrs ← mkDiscrs header indVal let alts ← mkAlts indVal fun ctor args userNames => do match args, userNames with @@ -56,7 +56,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do ``(mkObj [($(quote ctor.name.getString!), Json.arr #[$[$xs:term],*])]) | xs, some userNames => let xs ← xs.mapIdxM fun idx (x, t) => do - `(($(quote userNames[idx].getString!), $(← mkToJson x t))) + `(($(quote userNames[idx]!.getString!), $(← mkToJson x t))) ``(mkObj [($(quote ctor.name.getString!), mkObj [$[$xs:term],*])]) let auxTerm ← `(match $[$discrs],* with $alts:matchAlt*) let auxCmd ← @@ -90,7 +90,7 @@ where let mut binders := #[] let mut userNames := #[] for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + let x := xs[indVal.numParams + i]! let localDecl ← getLocalDecl x.fvarId! if !localDecl.userName.hasMacroScopes then userNames := userNames.push localDecl.userName @@ -103,26 +103,26 @@ where def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size == 1 then - if isStructure (← getEnv) declNames[0] then + if isStructure (← getEnv) declNames[0]! then let cmds ← liftTermElabM none <| do - let ctx ← mkContext "fromJson" declNames[0] - let header ← mkHeader ``FromJson 0 ctx.typeInfos[0] - let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false) + let ctx ← mkContext "fromJson" declNames[0]! + let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]! + let fields := getStructureFieldsFlattened (← getEnv) declNames[0]! (includeSubobjectFields := false) let jsonFields := fields.map (Prod.snd ∘ mkJsonField) let fields := fields.map mkIdent - let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:bracketedBinder* (j : Json) - : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := do + let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* (j : Json) + : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) := do $[let $fields:ident ← getObjValAs? j _ $jsonFields]* return { $[$fields:ident := $(id fields)],* }) return #[cmd] ++ (← mkInstanceCmds ctx ``FromJson declNames) cmds.forM elabCommand return true else - let indVal ← getConstInfoInduct declNames[0] + let indVal ← getConstInfoInduct declNames[0]! let cmds ← liftTermElabM none <| do - let ctx ← mkContext "fromJson" declNames[0] - let header ← mkHeader ``FromJson 0 ctx.typeInfos[0] - let fromJsonFuncId := mkIdent ctx.auxFunNames[0] + let ctx ← mkContext "fromJson" declNames[0]! + let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]! + let fromJsonFuncId := mkIdent ctx.auxFunNames[0]! let alts ← mkAlts indVal fromJsonFuncId let mut auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched")) if ctx.usePartial then @@ -133,11 +133,11 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do let auxCmd ← if ctx.usePartial || indVal.isRec then `(private partial def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json) - : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := + : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) := $auxTerm) else `(private def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json) - : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := + : Except String $(← mkInductiveApp ctx.typeInfos[0]! header.argNames) := $auxTerm) return #[auxCmd] ++ (← mkInstanceCmds ctx ``FromJson declNames) cmds.forM elabCommand @@ -153,7 +153,7 @@ where let mut binders := #[] let mut userNames := #[] for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + let x := xs[indVal.numParams + i]! let localDecl ← getLocalDecl x.fvarId! if !localDecl.userName.hasMacroScopes then userNames := userNames.push localDecl.userName @@ -163,8 +163,8 @@ where -- Return syntax to parse `id`, either via `FromJson` or recursively -- if `id`'s type is the type we're deriving for. let mkFromJson (idx : Nat) (type : Expr) : TermElabM (TSyntax ``doExpr) := - if type.isAppOf indVal.name then `(Lean.Parser.Term.doExpr| $fromJsonFuncId:ident jsons[$(quote idx)]) - else `(Lean.Parser.Term.doExpr| fromJson? jsons[$(quote idx)]) + if type.isAppOf indVal.name then `(Lean.Parser.Term.doExpr| $fromJsonFuncId:ident jsons[$(quote idx)]!) + else `(Lean.Parser.Term.doExpr| fromJson? jsons[$(quote idx)]!) let identNames := binders.map Prod.fst let fromJsons ← binders.mapIdxM fun idx (_, type) => mkFromJson idx type let userNamesOpt ← if binders.size == userNames.size then diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index 94fbe62fc3..c2c0eaaf07 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -38,14 +38,14 @@ where for _ in [:indVal.numParams] do ctorArgs := ctorArgs.push (← `(_)) for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + let x := xs[indVal.numParams + i]! let a := mkIdent (← mkFreshUserName `a) ctorArgs := ctorArgs.push a let xTy ← whnf (← inferType x) match xTy.getAppFn with | .const declName .. => match allIndVals.findIdx? (· == declName) with - | some x => rhs ← `(mixHash $rhs ($(mkIdent ctx.auxFunNames[x]) $a:ident)) + | some x => rhs ← `(mixHash $rhs ($(mkIdent ctx.auxFunNames[x]!) $a:ident)) | none => rhs ← `(mixHash $rhs (hash $a:ident)) | _ => rhs ← `(mixHash $rhs (hash $a:ident)) patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*)) @@ -55,8 +55,8 @@ where return alts def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do - let auxFunName := ctx.auxFunNames[i] - let indVal := ctx.typeInfos[i] + let auxFunName := ctx.auxFunNames[i]! + let indVal := ctx.typeInfos[i]! let header ← mkHashableHeader indVal let body ← mkMatch ctx header indVal let binders := header.binders @@ -73,7 +73,7 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do `(mutual $auxDefs:command* end) private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "hash" declNames[0] + let ctx ← mkContext "hash" declNames[0]! let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable declNames) trace[Elab.Deriving.hashable] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 48d80e6993..a77bca5fc6 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -87,7 +87,7 @@ where let mut usedInstIdxs := {} let mut ok := true for i in [ctorVal.numParams:xs.size] do - let x := xs[i] + let x := xs[i]! let instType ← mkAppM `Inhabited #[(← inferType x)] trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'" match (← trySynthInstance instType) with diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean index 5e092ea82a..063816311c 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -38,7 +38,7 @@ where ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + let x := xs[indVal.numParams + i]! if type.containsFVar x.fvarId! || (←isProp (←inferType x)) then -- If resulting type depends on this field or is a proof, we don't need to compare ctorArgs1 := ctorArgs1.push (← `(_)) @@ -65,8 +65,8 @@ where return alts.pop.pop def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do - let auxFunName := ctx.auxFunNames[i] - let indVal := ctx.typeInfos[i] + let auxFunName := ctx.auxFunNames[i]! + let indVal := ctx.typeInfos[i]! let header ← mkOrdHeader indVal let mut body ← mkMatch header indVal if ctx.usePartial || indVal.isRec then @@ -87,7 +87,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkOrdInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "ord" declNames[0] + let ctx ← mkContext "ord" declNames[0]! let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord declNames) trace[Elab.Deriving.ord] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 105f4a82a2..8d17e636a3 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -23,16 +23,16 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term : let ctorVal ← getConstInfoCtor indVal.ctors.head! let fieldNames := getStructureFields (← getEnv) indVal.name let numParams := indVal.numParams - let target := mkIdent header.targetNames[0] + let target := mkIdent header.targetNames[0]! forallTelescopeReducing ctorVal.type fun xs _ => do let mut fields ← `(Format.nil) let mut first := true if xs.size != numParams + fieldNames.size then throwError "'deriving Repr' failed, unexpected number of fields in structure" for i in [:fieldNames.size] do - let fieldName := fieldNames[i] + let fieldName := fieldNames[i]! let fieldNameLit := Syntax.mkStrLit (toString fieldName) - let x := xs[numParams + i] + let x := xs[numParams + i]! if first then first := false else @@ -64,7 +64,7 @@ where for _ in [:indVal.numParams] do ctorArgs := ctorArgs.push (← `(_)) for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i] + let x := xs[indVal.numParams + i]! let a := mkIdent (← mkFreshUserName `a) ctorArgs := ctorArgs.push a let localDecl ← getLocalDecl x.fvarId! @@ -85,8 +85,8 @@ def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermE mkBodyForInduct header indVal auxFunName def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do - let auxFunName := ctx.auxFunNames[i] - let indVal := ctx.typeInfos[i] + let auxFunName := ctx.auxFunNames[i]! + let indVal := ctx.typeInfos[i]! let header ← mkReprHeader indVal let mut body ← mkBody header indVal auxFunName if ctx.usePartial then @@ -107,7 +107,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "repr" declNames[0] + let ctx ← mkContext "repr" declNames[0]! let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames) trace[Elab.Deriving.repr] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/SizeOf.lean b/src/Lean/Elab/Deriving/SizeOf.lean index c60f7c43fc..c681a3da81 100644 --- a/src/Lean/Elab/Deriving/SizeOf.lean +++ b/src/Lean/Elab/Deriving/SizeOf.lean @@ -17,7 +17,7 @@ open Command def mkSizeOfHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) && declNames.size > 0 then - liftTermElabM none <| Meta.mkSizeOfInstances declNames[0] + liftTermElabM none <| Meta.mkSizeOfInstances declNames[0]! return true else return false diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 745d5acaf5..d75026b909 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -50,10 +50,10 @@ def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : let mut binders := #[] for i in [:xs.size] do try - let x := xs[i] + let x := xs[i]! let c ← mkAppM className #[x] if (← isTypeCorrect c) then - let argName := argNames[i] + let argName := argNames[i]! let binder : Syntax ← `(instBinderF| [ $(mkIdent className):ident $(mkIdent argName):ident ]) binders := binders.push binder catch _ => @@ -86,8 +86,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do let mut letDecls := #[] for i in [:ctx.typeInfos.size] do - let indVal := ctx.typeInfos[i] - let auxFunName := ctx.auxFunNames[i] + let indVal := ctx.typeInfos[i]! + let auxFunName := ctx.auxFunNames[i]! let currArgNames ← mkInductArgNames indVal let numParams := indVal.numParams let currIndices := currArgNames[numParams:] @@ -109,9 +109,9 @@ open TSyntax.Compat in def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor := true) : TermElabM (Array Command) := do let mut instances := #[] for i in [:ctx.typeInfos.size] do - let indVal := ctx.typeInfos[i] + let indVal := ctx.typeInfos[i]! if typeNames.contains indVal.name then - let auxFunName := ctx.auxFunNames[i] + let auxFunName := ctx.auxFunNames[i]! let argNames ← mkInductArgNames indVal let binders ← mkImplicitBinders argNames let binders := binders ++ (← mkInstImplicitBinders className indVal argNames) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 7222a3ff10..7fc4a4a06b 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -717,7 +717,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do if elems.size == 0 then mkUnit else if elems.size == 1 then - return elems[0] + return elems[0]! else elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple => ``(MProd.mk $elem $tuple) @@ -752,7 +752,7 @@ private def destructTuple (uvars : Array Var) (x : Syntax) (body : Syntax) : Mac if uvars.size == 0 then return body else if uvars.size == 1 then - `(let $(uvars[0]):ident := $x; $body) + `(let $(uvars[0]!):ident := $x; $body) else destruct uvars.toList x body where @@ -1173,7 +1173,7 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt else if k == ``Lean.Parser.Term.liftMethod && !inQuot then withFreshMacroScope do if inBinder then throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`" - let term := args[1] + let term := args[1]! let term ← expandLiftMethodAux inQuot inBinder term let auxDoElem : Syntax ← `(doElem| let a ← $term:term) modify fun s => s ++ [auxDoElem] @@ -1377,7 +1377,7 @@ mutual ``` -/ -- Extract second element - let doForDecl := doForDecls[1] + let doForDecl := doForDecls[1]! unless doForDecl[0].isNone do throwErrorAt doForDecl[0] "the proof annotation here has not been implemented yet" let y := doForDecl[1] @@ -1396,10 +1396,10 @@ mutual do $body) doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems) else withRef doFor do - let h? := if doForDecls[0][0].isNone then none else some doForDecls[0][0][0] - let x := doForDecls[0][1] + let h? := if doForDecls[0]![0].isNone then none else some doForDecls[0]![0][0] + let x := doForDecls[0]![1] withRef x <| checkNotShadowingMutable (← getPatternVarsEx x) - let xs := doForDecls[0][3] + let xs := doForDecls[0]![3] let forElems := getDoSeqElems doFor[3] let forInBodyCodeBlock ← withFor (doSeqToCode forElems) let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 2661a52960..de492fd87e 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -20,7 +20,7 @@ def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) : CommandElabM Syntax := do let alts ← alts.mapM fun (alt : TSyntax ``matchAlt) => match alt with | `(matchAltExpr| | $pats,* => $rhs) => do - let pat := pats.elemsAndSeps[0] + let pat := pats.elemsAndSeps[0]! if !pat.isQuot then throwUnsupportedSyntax let quoted := getQuotContent pat diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index eb2b687f63..6d5e8812d6 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -387,22 +387,22 @@ def elabBinCalc : TermElab := fun stx expectedType? => do let proof ← elabTermEnsuringType stepStx[2] type synthesizeSyntheticMVars proofs := proofs.push proof - let mut result := proofs[0] - let mut resultType := types[0] + let mut result := proofs[0]! + let mut resultType := types[0]! for i in [1:proofs.size] do let some (r, a, b) ← relation? resultType | unreachable! - let some (s, _, c) ← relation? (← instantiateMVars types[i]) | unreachable! + let some (s, _, c) ← relation? (← instantiateMVars types[i]!) | unreachable! let (α, β, γ) := (← inferType a, ← inferType b, ← inferType c) let (u_1, u_2, u_3) := (← getLevel α, ← getLevel β, ← getLevel γ) let t ← mkFreshExprMVar (← mkArrow α (← mkArrow γ (mkSort levelZero))) let selfType := mkAppN (Lean.mkConst ``Trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t] match (← trySynthInstance selfType) with | LOption.some self => - result := mkAppN (Lean.mkConst ``Trans.trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, proofs[i]] + result := mkAppN (Lean.mkConst ``Trans.trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, proofs[i]!] resultType := (← instantiateMVars (← inferType result)).headBeta unless (← relation? resultType).isSome do - throwErrorAt stepStxs[i] "invalid 'calc' step, step result is not a relation{indentExpr resultType}" - | _ => throwErrorAt stepStxs[i] "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}" + throwErrorAt stepStxs[i]! "invalid 'calc' step, step result is not a relation{indentExpr resultType}" + | _ => throwErrorAt stepStxs[i]! "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}" pure () ensureHasType expectedType? result diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 3e3e385c75..3b316ef78a 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -95,21 +95,21 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : return acc private def checkNumParams (rs : Array ElabHeaderResult) : TermElabM Nat := do - let numParams := rs[0].params.size + let numParams := rs[0]!.params.size for r in rs do unless r.params.size == numParams do throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes" return numParams private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do - let isUnsafe := rs[0].view.modifiers.isUnsafe + let isUnsafe := rs[0]!.view.modifiers.isUnsafe for r in rs do unless r.view.modifiers.isUnsafe == isUnsafe do throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes" private def checkLevelNames (views : Array InductiveView) : TermElabM Unit := do if views.size > 1 then - let levelNames := views[0].levelNames + let levelNames := views[0]!.levelNames for view in views do unless view.levelNames == levelNames do throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes" @@ -153,7 +153,7 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible. private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do if i < rs.size then - let type ← checkHeader rs[i] numParams firstType? + let type ← checkHeader rs[i]! numParams firstType? checkHeaders rs numParams (i+1) type private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do @@ -173,7 +173,7 @@ private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : A let namesAndTypes ← rs.mapM fun r => do let type ← mkTypeFor r pure (r.view.shortDeclName, type) - let r0 := rs[0] + let r0 := rs[0]! let params := r0.params withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do let rec loop (i : Nat) (indFVars : Array Expr) := do @@ -210,7 +210,7 @@ where match type with | .forallE n d b data => if n.hasMacroScopes then - mkForall newNames[i] data.binderInfo d (go b (i+1)) + mkForall newNames[i]! data.binderInfo d (go b (i+1)) else mkForall n data.binderInfo d (go b (i+1)) | _ => type @@ -362,8 +362,8 @@ where unless args.size ≥ params.size do throwError "unexpected inductive type occurrence{indentExpr e}" for i in [:params.size] do - let param := params[i] - let arg := args[i] + let param := params[i]! + let arg := args[i]! unless (← isDefEq param arg) do throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}" args := args.set! i param @@ -601,8 +601,8 @@ private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr let levelParams := levelNames.map mkLevelParam; let mut m : ExprMap Expr := {} for i in [:views.size] do - let view := views[i] - let indFVar := indFVars[i] + let view := views[i]! + let indFVar := indFVars[i]! m := m.insert indFVar (mkConst view.declName levelParams) return m @@ -669,7 +669,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) forallTelescopeReducing ctor.type fun xs type => do let typeArgs := type.getAppArgs for i in [numParams:arity] do - unless i < xs.size && xs[i] == typeArgs[i] do -- Remark: if we want to allow arguments to be rearranged, this test should be xs.contains typeArgs[i] + unless i < xs.size && xs[i]! == typeArgs[i]! do -- Remark: if we want to allow arguments to be rearranged, this test should be xs.contains typeArgs[i] maskRef.modify fun mask => mask.set! i false for x in xs[numParams:] do let xType ← inferType x @@ -680,7 +680,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) if i >= typeArgs.size then maskRef.modify (resetMaskAt · i) else - unless eArgs[i] == typeArgs[i] do + unless eArgs[i]! == typeArgs[i]! do maskRef.modify (resetMaskAt · i) go ctors go indType.ctors @@ -713,14 +713,14 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind -- We process just a non-fixed prefix of the indices for now. Reason: we don't want to change the order. -- TODO: extend it in the future. For example, it should be reasonable to change -- the order of indices generated by the auto implicit feature. - let mask := masks[0] - forallBoundedTelescope indTypes[0].type numParams fun params type => do + let mask := masks[0]! + forallBoundedTelescope indTypes[0]!.type numParams fun params type => do let otherTypes ← indTypes[1:].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params) let ctorTypes ← indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD (← instantiateForall ctor.type params) let typesToCheck := otherTypes.toList ++ ctorTypes.join let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do if i < mask.size then - if !masks.all fun mask => i < mask.size && mask[i] then + if !masks.all fun mask => i < mask.size && mask[i]! then return i if !type.isForall then return i @@ -736,7 +736,7 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind go numParams type typesToCheck private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do - let view0 := views[0] + let view0 := views[0]! let scopeLevelNames ← Term.getLevelNames checkLevelNames views let allUserLevelNames := view0.levelNames @@ -747,9 +747,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : trace[Elab.inductive] "indFVars: {indFVars}" let mut indTypesArray := #[] for i in [:views.size] do - let indFVar := indFVars[i] - Term.addLocalVarInfo views[i].declId indFVar - let r := rs[i] + let indFVar := indFVars[i]! + Term.addLocalVarInfo views[i]!.declId indFVar + let r := rs[i]! let type ← mkForallFVars params r.type let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r) indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors } @@ -799,7 +799,7 @@ private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM U classView.applyHandlers declNames def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do - let view0 := views[0] + let view0 := views[0]! let ref := view0.ref runTermElabM view0.declName fun vars => withRef ref do mkInductiveDecl vars views diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index bf9206a558..86d7d1cb51 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -76,7 +76,7 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) := forallBoundedTelescope view.type view.binderIds.size fun xs type => do -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location. for i in [0:view.binderIds.size] do - addLocalVarInfo view.binderIds[i] xs[i] + addLocalVarInfo view.binderIds[i]! xs[i]! withDeclName view.declName do let value ← elabTermEnsuringType view.valStx type mkLambdaFVars xs value @@ -91,14 +91,14 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array let localInstances ← getLocalInstances let toLift := views.mapIdx fun i view => { ref := view.ref - fvarId := fvars[i].fvarId! + fvarId := fvars[i]!.fvarId! attrs := view.attrs shortDeclName := view.shortDeclName declName := view.declName lctx localInstances type := view.type - val := values[i] + val := values[i]! mvarId := view.mvar.mvarId! : LetRecToLift } modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift } diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean index 406cb308f7..f3e964809c 100644 --- a/src/Lean/Elab/MacroRules.lean +++ b/src/Lean/Elab/MacroRules.lean @@ -18,7 +18,7 @@ open Lean.Parser.Command def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (tk : Syntax) (k : SyntaxNodeKind) (alts : Array (TSyntax ``matchAlt)) : CommandElabM Syntax := do let alts ← alts.mapM fun (alt : TSyntax ``matchAlt) => match alt with | `(matchAltExpr| | $pats,* => $rhs) => do - let pat := pats.elemsAndSeps[0] + let pat := pats.elemsAndSeps[0]! if !pat.isQuot then throwUnsupportedSyntax let quoted := getQuotContent pat diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 5e3fb8c211..06d71e02f5 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -290,13 +290,13 @@ where let tArgs := t.getAppArgs let dArgs := d.getAppArgs for i in [:info.numParams] do - let tArg := tArgs[i] - let dArg := dArgs[i] + let tArg := tArgs[i]! + let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do return i :: (← goType tArg dArg) for i in [info.numParams : tArgs.size] do - let tArg := tArgs[i] - let dArg := dArgs[i] + let tArg := tArgs[i]! + let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do return i :: (← goIndex tArg dArg) failure @@ -313,13 +313,13 @@ where let tArgs := t.getAppArgs let dArgs := d.getAppArgs for i in [:info.numParams] do - let tArg := tArgs[i] - let dArg := dArgs[i] + let tArg := tArgs[i]! + let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do failure for i in [info.numParams : tArgs.size] do - let tArg := tArgs[i] - let dArg := dArgs[i] + let tArg := tArgs[i]! + let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do return i :: (← goIndex tArg dArg) failure @@ -342,7 +342,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep let mut patterns := #[] let mut matchType := matchType for idx in [:patternStxs.size] do - let patternStx := patternStxs[idx] + let patternStx := patternStxs[idx]! matchType ← whnf matchType match matchType with | Expr.forallE _ d b _ => @@ -906,7 +906,7 @@ where match (← altViews'.mapM (fun altView => elabMatchAltView discrs' altView matchType' (toClear ++ toClear')) |>.run) with | Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined) | Except.error { patternIdx := patternIdx, pathToIndex := pathToIndex, ex := ex } => - let discr := discrs[patternIdx] + let discr := discrs[patternIdx]! let some index ← getIndexToInclude? discr.expr pathToIndex | throwEx (← updateFirst first? ex) trace[Elab.match] "index to include: {index}" @@ -1027,7 +1027,7 @@ private def isMatchUnit? (altLHSS : List Match.AltLHS) (rhss : Array Expr) : Met match altLHSS with | [ { fvarDecls := [], patterns := [ Pattern.ctor `PUnit.unit .. ], .. } ] => /- Recall that for alternatives of the form `| PUnit.unit => rhs`, `rhss[0]` is of the form `fun _ : Unit => b`. -/ - match rhss[0] with + match rhss[0]! with | Expr.lam _ _ b _ => return if b.hasLooseBVars then none else b | _ => return none | _ => return none diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 49dba0ddb2..eee16a5841 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -83,10 +83,10 @@ private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) : Term ``` -/ private def isMultiConstant? (views : Array DefView) : Option (List Name) := if views.size == 1 && - views[0].kind == DefKind.opaque && - views[0].binders.getArgs.size > 0 && - views[0].binders.getArgs.all (·.getKind == ``Parser.Term.simpleBinder) then - some <| (views[0].binders.getArgs.toList.map (fun stx => stx[0].getArgs.toList.map (·.getId))).join + views[0]!.kind == DefKind.opaque && + views[0]!.binders.getArgs.size > 0 && + views[0]!.binders.getArgs.all (·.getKind == ``Parser.Term.simpleBinder) then + some <| (views[0]!.binders.getArgs.toList.map (fun stx => stx[0].getArgs.toList.map (·.getId))).join else none @@ -209,7 +209,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location. for i in [0:header.binderIds.size] do -- skip auto-bound prefix in `xs` - addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i] + addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]! let val ← elabTermEnsuringType valStx type mkLambdaFVars xs val @@ -539,15 +539,15 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa let mut freeVarMap := mkFreeVarMap (← getMCtx) sectionVars mainFVarIds recFVarIds letRecsToLift let mut result := #[] for i in [:letRecsToLift.size] do - if letRecsToLift[i].val.hasExprMVar then + if letRecsToLift[i]!.val.hasExprMVar then -- This can happen when this particular let-rec has nested let-rec that have been resolved in previous iterations. -- This code relies on the fact that nested let-recs occur before the outer most let-recs at `letRecsToLift`. -- Unresolved nested let-recs appear as metavariables before they are resolved. See `assignExprMVar` at `mkLetRecClosureFor` - let valNew ← instantiateMVars letRecsToLift[i].val + let valNew ← instantiateMVars letRecsToLift[i]!.val letRecsToLift := letRecsToLift.modify i fun t => { t with val := valNew } -- We have to recompute the `freeVarMap` in this case. This overhead should not be an issue in practice. freeVarMap := mkFreeVarMap (← getMCtx) sectionVars mainFVarIds recFVarIds letRecsToLift - let toLift := letRecsToLift[i] + let toLift := letRecsToLift[i]! result := result.push (← mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!) return result.toList @@ -556,7 +556,7 @@ abbrev Replacement := FVarIdMap Expr def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement := mainFVars.size.fold (init := r) fun i r => - r.insert mainFVars[i].fvarId! (mkAppN (Lean.mkConst mainHeaders[i].declName) sectionVars) + r.insert mainFVars[i]!.fvarId! (mkAppN (Lean.mkConst mainHeaders[i]!.declName) sectionVars) def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecClosure) : Replacement := @@ -573,8 +573,8 @@ def Replacement.apply (r : Replacement) (e : Expr) : Expr := def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr) : TermElabM (Array PreDefinition) := mainHeaders.size.foldM (init := preDefs) fun i preDefs => do - let header := mainHeaders[i] - let val ← mkLambdaFVars sectionVars mainVals[i] + let header := mainHeaders[i]! + let val ← mkLambdaFVars sectionVars mainVals[i]! let type ← mkForallFVars sectionVars header.type return preDefs.push { ref := getDeclarationSelectionRef header.ref diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean index f77c61edab..9d0576079c 100644 --- a/src/Lean/Elab/Open.lean +++ b/src/Lean/Elab/Open.lean @@ -58,11 +58,11 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) : if exs.size == nss.length then withRef idStx do if exs.size == 1 then - throw exs[0] + throw exs[0]! else throwErrorWithNestedErrors "failed to open" exs if result.size == 1 then - return result[0] + return result[0]! else withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}" diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 08daafdb4a..f2238c02e5 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -95,7 +95,7 @@ private def isNextArgAccessible (ctx : Context) : Bool := private def getNextParam (ctx : Context) : (Name × BinderInfo) × Context := let i := ctx.paramDeclIdx - let d := ctx.paramDecls[i] + let d := ctx.paramDecls[i]! (d, { ctx with paramDeclIdx := ctx.paramDeclIdx + 1 }) private def processVar (idStx : Syntax) : M Syntax := do @@ -211,7 +211,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc else args let stateSaved ← get - let arg0 ← collect args[0] + let arg0 ← collect args[0]! let stateNew ← get let mut argsNew := #[arg0] for arg in args[1:] do @@ -297,7 +297,7 @@ where let (d, ctx) := getNextParam ctx match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with | some idx => - let arg := ctx.namedArgs[idx] + let arg := ctx.namedArgs[idx]! let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx } let ctx ← pushNewArg accessible ctx arg.val processCtorAppContext ctx diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index e1d490f5ec..0a3a63dd45 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -147,7 +147,7 @@ def eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition := def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := do let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d - withRef preDefs[0].ref do + withRef preDefs[0]!.ref do let all := preDefs.toList.map (·.declName) let decl := Declaration.mutualDefnDecl <| ← preDefs.toList.mapM fun preDef => return { name := preDef.declName diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 57474f573a..d394f37809 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -55,7 +55,7 @@ private def findMatchToSplit? (env : Environment) (e : Expr) (declNames : Array -- If none of the discriminants is a free variable, then it is not worth splitting the match let mut hasFVarDiscr := false for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do - let discr := args[i] + let discr := args[i]! if discr.isFVar then hasFVarDiscr := true break @@ -63,7 +63,7 @@ private def findMatchToSplit? (env : Environment) (e : Expr) (declNames : Array return Expr.FindStep.visit -- At least one alternative must contain a `declNames` application with loose bound variables. for i in [info.getFirstAltPos : info.getFirstAltPos + info.numAlts] do - let alt := args[i] + let alt := args[i]! if Option.isSome <| alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars then return Expr.FindStep.found return Expr.FindStep.visit diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index c4da4a4e5f..6a9617b434 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -103,8 +103,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) let mut hasErrors := false for preDefs in cliques do trace[Elab.definition.scc] "{preDefs.map (·.declName)}" - if preDefs.size == 1 && isNonRecursive preDefs[0] then - let preDef := preDefs[0] + if preDefs.size == 1 && isNonRecursive preDefs[0]! then + let preDef := preDefs[0]! if preDef.modifiers.isNoncomputable then addNonRec preDef else @@ -129,7 +129,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) if wf?.isSome || decrTactic?.isSome then wfRecursion preDefs wf? decrTactic? else - withRef (preDefs[0].ref) <| mapError + withRef (preDefs[0]!.ref) <| mapError (orelseMergeErrors (structuralRecursion preDefs) (wfRecursion preDefs none none)) diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean index fa99a471fc..5050baa096 100644 --- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean +++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean @@ -23,7 +23,7 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Boo let rec loop | 0, type => mkInhabitant? type useOfNonempty | i+1, type => do - let x := xs[i] + let x := xs[i]! let type ← mkForallFVars #[x] type; match (← mkInhabitant? type useOfNonempty) with | none => loop i type diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 3cd6335f1d..8e6d282288 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -53,7 +53,7 @@ private def withBelowDict (below : Expr) (numIndParams : Nat) (k : Expr → Expr let pre := mkAppN f (args.extract 0 numIndParams) let preType ← inferType pre forallBoundedTelescope preType (some 1) fun x _ => do - let motiveType ← inferType x[0] + let motiveType ← inferType x[0]! withLocalDeclD (← mkFreshUserName `C) motiveType fun C => let belowDict := mkApp pre C let belowDict := mkAppN belowDict (args.extract (numIndParams + 1) args.size) @@ -92,7 +92,7 @@ def refinedArgType (matcherApp : MatcherApp) (arg : Expr) : MetaM Bool := do (Array.zip matcherApp.alts matcherApp.altNumParams).anyM fun (alt, numParams) => lambdaTelescope alt fun xs _ => do if xs.size >= numParams then - let refinedArg := xs[numParams - 1] + let refinedArg := xs[numParams - 1]! return !(← isDefEq (← inferType refinedArg) argType) else return false @@ -127,7 +127,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos if recArgPos >= args.size then throwError "insufficient number of parameters at recursive application {indentExpr e}" - let recArg := args[recArgPos] + let recArg := args[recArgPos]! -- For reflexive type, we may have nested recursive applications in recArg let recArg ← loop below recArg let f ← try toBelow below recArgInfo.indParams.size recArg catch _ => throwError "failed to eliminate recursive application{indentExpr e}" @@ -137,7 +137,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) let mut fArgs := #[] for i in [:argsNonFixed.size] do if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then - let arg := argsNonFixed[i] + let arg := argsNonFixed[i]! let arg ← replaceRecApps recFnName recArgInfo below arg fArgs := fArgs.push arg return mkAppN f fArgs @@ -174,7 +174,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}" unless xs.size >= numParams do throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}" - let belowForAlt := xs[numParams - 1] + let belowForAlt := xs[numParams - 1]! mkLambdaFVars xs (← loop belowForAlt altBody) pure { matcherApp with alts := altsNew }.toExpr | none => @@ -187,7 +187,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) lambdaTelescope alt fun xs altBody => do unless xs.size >= numParams do throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" - let belowForAlt := xs[numParams] + let belowForAlt := xs[numParams]! mkLambdaFVars xs (← loop belowForAlt altBody) return { casesOnApp with alts := altsNew }.toExpr else @@ -199,7 +199,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do trace[Elab.definition.structural] "mkBRecOn: {value}" let type := (← inferType value).headBeta - let major := recArgInfo.ys[recArgInfo.pos] + let major := recArgInfo.ys[recArgInfo.pos]! let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}" let motive ← mkForallFVars otherArgs type @@ -224,7 +224,7 @@ def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Exp trace[Elab.definition.structural] "brecOn {brecOn}" trace[Elab.definition.structural] "brecOnType {brecOnType}" forallBoundedTelescope brecOnType (some 1) fun F _ => do - let F := F[0] + let F := F[0]! let FType ← inferType F trace[Elab.definition.structural] "FType: {FType}" let FType ← instantiateForall FType recArgInfo.indIndices @@ -232,7 +232,7 @@ def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Exp forallBoundedTelescope FType (some 1) fun below _ => do -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages. -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used. - let below := below[0] + let below := below[0]! let valueNew ← replaceRecApps recFnName recArgInfo below value let Farg ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew let brecOn := mkApp brecOn Farg diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index f9308b8a2d..a6b8f9af72 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -65,8 +65,8 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := let baseName := mkPrivateName (← getEnv) info.declName let mut thmNames := #[] for i in [: eqnTypes.size] do - let type := eqnTypes[i] - trace[Elab.definition.structural.eqns] "{eqnTypes[i]}" + let type := eqnTypes[i]! + trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}" let name := baseName ++ (`_eq).appendIndexAfter (i+1) thmNames := thmNames.push name let value ← mkProof info.declName type diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean index 7c1db7ba23..2f70bee15c 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean @@ -63,7 +63,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr def mkIndPredBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do let type := (← inferType value).headBeta - let major := recArgInfo.ys[recArgInfo.pos] + let major := recArgInfo.ys[recArgInfo.pos]! let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}" let motive ← mkForallFVars otherArgs type @@ -84,13 +84,13 @@ def mkIndPredBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) -- call, it uses this ih. But that ih doesn't exist in the actual brecOn call. -- That's why it must go. let FType ← forallBoundedTelescope brecOnType (some 1) fun F _ => do - let F := F[0] + let F := F[0]! let FType ← inferType F trace[Elab.definition.structural] "FType: {FType}" let FType ← instantiateForall FType recArgInfo.indIndices instantiateForall FType #[major] forallBoundedTelescope FType (some 1) fun below _ => do - let below := below[0] + let below := below[0]! let valueNew ← replaceIndPredRecApps recFnName recArgInfo motive value let Farg ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew let brecOn := mkApp brecOn Farg diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean index dc891f390a..7a778c44e1 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Main.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean @@ -81,9 +81,9 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit := if preDefs.size != 1 then throwError "structural recursion does not handle mutually recursive functions" else do - let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0] + let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0]! let preDefNonRec ← eraseRecAppSyntax preDefNonRec - let preDef ← eraseRecAppSyntax preDefs[0] + let preDef ← eraseRecAppSyntax preDefs[0]! state.addMatchers.forM liftM registerEqnsInfo preDef recArgPos mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg => diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 209a948946..edbf54104f 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -46,7 +46,7 @@ private def hasWellFoundedFix (e : Expr) : Bool := private partial def decodePackedArg? (info : EqnInfo) (e : Expr) : Option (Name × Array Expr) := do if info.declNames.size == 1 then let args := decodePSigma e #[] - return (info.declNames[0], args) + return (info.declNames[0]!, args) else decodePSum? e 0 where @@ -57,7 +57,7 @@ where decodePSum? e.appArg! (i+1) else guard (i < info.declNames.size) - return (info.declNames[i], decodePSigma e #[]) + return (info.declNames[i]!, decodePSigma e #[]) decodePSigma (e : Expr) (acc : Array Expr) : Array Expr := /- TODO: check arity of the given function. If it takes a PSigma as the last argument, @@ -88,7 +88,7 @@ where let e' := e.headBeta if e'.isAppOf ``WellFounded.fix && e'.getAppNumArgs >= 6 then let args := e'.getAppArgs - let packedArg := args[5] + let packedArg := args[5]! let extraArgs := args[6:] if let some (declName, args) := decodePackedArg? info packedArg then let candidate := mkAppN (mkAppN (mkAppN (mkConst declName us) fixedPrefix) args) extraArgs @@ -194,8 +194,8 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := mkEqnTypes info.declNames goal.mvarId! let mut thmNames := #[] for i in [: eqnTypes.size] do - let type := eqnTypes[i] - trace[Elab.definition.wf.eqns] "{eqnTypes[i]}" + let type := eqnTypes[i]! + trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}" let name := baseName ++ (`_eq).appendIndexAfter (i+1) thmNames := thmNames.push name let value ← mkProof declName info type diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 7cb5702ca6..a686f977e5 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -44,7 +44,7 @@ where loop F (← etaExpand e) else let args := e.getAppArgs - let r := mkApp F (← loop F args[fixedPrefixSize]) + let r := mkApp F (← loop F args[fixedPrefixSize]!) let decreasingProp := (← whnf (← inferType r)).bindingDomain! let r := mkApp r (← mkDecreasingProof decreasingProp decrTactic?) return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F)) @@ -91,7 +91,7 @@ where lambdaTelescope alt fun xs altBody => do unless xs.size >= numParams do throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}" - let FAlt := xs[numParams - 1] + let FAlt := xs[numParams - 1]! mkLambdaFVars xs (← loop FAlt altBody) return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr else @@ -106,7 +106,7 @@ where lambdaTelescope alt fun xs altBody => do unless xs.size >= numParams do throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" - let FAlt := xs[numParams] + let FAlt := xs[numParams]! mkLambdaFVars xs (← loop FAlt altBody) return { casesOnApp with alts := altsNew @@ -120,21 +120,21 @@ where private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F : Expr) → (val : Expr) → TermElabM Expr) : TermElabM Expr := do if x.isFVar && val.isAppOfArity ``PSum.casesOn 6 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 5).isLambda then let args := val.getAppArgs - let α := args[0] - let β := args[1] + let α := args[0]! + let β := args[1]! let FDecl ← getLocalDecl F.fvarId! - let (motiveNew, u) ← lambdaTelescope args[2] fun xs type => do - let type ← mkArrow (FDecl.type.replaceFVar x xs[0]) type + let (motiveNew, u) ← lambdaTelescope args[2]! fun xs type => do + let type ← mkArrow (FDecl.type.replaceFVar x xs[0]!) type return (← mkLambdaFVars xs type, ← getLevel type) let mkMinorNew (ctorName : Name) (minor : Expr) : TermElabM Expr := lambdaTelescope minor fun xs body => do - let xNew := xs[0] + let xNew := xs[0]! let valNew ← mkLambdaFVars xs[1:] body let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM ctorName #[α, β, xNew]) withLocalDeclD FDecl.userName FTypeNew fun FNew => do mkLambdaFVars #[xNew, FNew] (← processSumCasesOn xNew FNew valNew k) - let minorLeft ← mkMinorNew ``PSum.inl args[4] - let minorRight ← mkMinorNew ``PSum.inr args[5] + let minorLeft ← mkMinorNew ``PSum.inl args[4]! + let minorRight ← mkMinorNew ``PSum.inr args[5]! let result := mkAppN (mkConst ``PSum.casesOn [u, (← getLevel α), (← getLevel β)]) #[α, β, motiveNew, x, minorLeft, minorRight, F] return result else @@ -145,15 +145,15 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v if x.isFVar && val.isAppOfArity ``PSigma.casesOn 5 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 4).bindingBody!.isLambda then let args := val.getAppArgs let [_, u, v] := val.getAppFn.constLevels! | unreachable! - let α := args[0] - let β := args[1] + let α := args[0]! + let β := args[1]! let FDecl ← getLocalDecl F.fvarId! - let (motiveNew, w) ← lambdaTelescope args[2] fun xs type => do - let type ← mkArrow (FDecl.type.replaceFVar x xs[0]) type + let (motiveNew, w) ← lambdaTelescope args[2]! fun xs type => do + let type ← mkArrow (FDecl.type.replaceFVar x xs[0]!) type return (← mkLambdaFVars xs type, ← getLevel type) - let minor ← lambdaTelescope args[4] fun xs body => do - let a := xs[0] - let xNew := xs[1] + let minor ← lambdaTelescope args[4]! fun xs body => do + let a := xs[0]! + let xNew := xs[1]! let valNew ← mkLambdaFVars xs[2:] body let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM `PSigma.mk #[α, β, a, xNew]) withLocalDeclD FDecl.userName FTypeNew fun FNew => do @@ -166,7 +166,7 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do let type ← instantiateForall preDef.type prefixArgs let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do - let x := x[0] + let x := x[0]! let α ← inferType x let u ← getLevel α let v ← getLevel type @@ -176,13 +176,13 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (dec let varName := (← getLocalDecl x.fvarId!).userName -- See comment below. return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName) forallBoundedTelescope (← whnf (← inferType wfFix)).bindingDomain! (some 2) fun xs _ => do - let x := xs[0] + let x := xs[0]! -- Remark: we rename `x` here to make sure we preserve the variable name in the -- decreasing goals when the function has only one non fixed argument. -- This renaming is irrelevant if the function has multiple non fixed arguments. See `process*` functions above. let lctx := (← getLCtx).setUserName x.fvarId! varName withTheReader Meta.Context (fun ctx => { ctx with lctx }) do - let F := xs[1] + let F := xs[1]! let val := preDef.value.beta (prefixArgs.push x) let val ← processSumCasesOn x F val fun x F val => do processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size decrTactic?) diff --git a/src/Lean/Elab/PreDefinition/WF/Ite.lean b/src/Lean/Elab/PreDefinition/WF/Ite.lean index d83357d7a4..c628ee583b 100644 --- a/src/Lean/Elab/PreDefinition/WF/Ite.lean +++ b/src/Lean/Elab/PreDefinition/WF/Ite.lean @@ -17,10 +17,10 @@ def iteToDIte (e : Expr) : MetaM Expr := do if e.isAppOfArity ``ite 5 then let f := e.getAppFn let args := e.getAppArgs - let c := args[1] + let c := args[1]! let h ← mkFreshUserName `h - let args := args.set! 3 (Lean.mkLambda h BinderInfo.default c args[3]) - let args := args.set! 4 (Lean.mkLambda h BinderInfo.default (mkNot c) args[4]) + let args := args.set! 3 (Lean.mkLambda h BinderInfo.default c args[3]!) + let args := args.set! 4 (Lean.mkLambda h BinderInfo.default (mkNot c) args[4]!) return .done <| mkAppN (mkConst ``dite f.constLevels!) args else return .done e diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index 0db395002f..36de5cca13 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -18,7 +18,7 @@ open Meta private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) : MetaM Bool := do if preDefs.size == 1 then - lambdaTelescope preDefs[0].value fun xs _ => return xs.size == fixedPrefixSize + 1 + lambdaTelescope preDefs[0]!.value fun xs _ => return xs.size == fixedPrefixSize + 1 else return false @@ -28,7 +28,7 @@ private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonR let us := preDefNonRec.levelParams.map mkLevelParam let all := preDefs.toList.map (·.declName) for fidx in [:preDefs.size] do - let preDef := preDefs[fidx] + let preDef := preDefs[fidx]! let value ← lambdaTelescope preDef.value fun xs _ => do let packedArgs : Array Expr := xs[fixedPrefixSize:] let mkProd (type : Expr) : MetaM Expr := do @@ -40,10 +40,10 @@ private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonR (← whnfD type).withApp fun f args => do assert! args.size == 2 if i == fidx then - return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0] args[1] (← mkProd args[0]) + return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! (← mkProd args[0]!) else - let r ← mkSum (i+1) args[1] - return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0] args[1] r + let r ← mkSum (i+1) args[1]! + return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r let Expr.forallE _ domain _ _ := (← instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable! let arg ← mkSum 0 domain mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg) @@ -56,10 +56,10 @@ where go (fvars : Array Expr) (vals : Array Expr) : TermElabM α := do if !(vals.all fun val => val.isLambda) then k fvars vals - else if !(← vals.allM fun val => return val.bindingName! == vals[0].bindingName! && val.binderInfo == vals[0].binderInfo && (← isDefEq val.bindingDomain! vals[0].bindingDomain!)) then + else if !(← vals.allM fun val => return val.bindingName! == vals[0]!.bindingName! && val.binderInfo == vals[0]!.binderInfo && (← isDefEq val.bindingDomain! vals[0]!.bindingDomain!)) then k fvars vals else - withLocalDecl vals[0].bindingName! vals[0].binderInfo vals[0].bindingDomain! fun x => + withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) def getFixedPrefix (preDefs : Array PreDefinition) : TermElabM Nat := diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index b36ff360c8..1e7e77fc5c 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean @@ -27,7 +27,7 @@ partial def mkUnaryArg (type : Expr) (args : Array Expr) : MetaM Expr := do where go (i : Nat) (type : Expr) : MetaM Expr := do if i < args.size - 1 then - let arg := args[i] + let arg := args[i]! assert! type.isAppOfArity ``PSigma 2 let us := type.getAppFn.constLevels! let α := type.appFn!.appArg! @@ -37,16 +37,16 @@ where let rest ← go (i+1) type return mkApp4 (mkConst ``PSigma.mk us) α β arg rest else - return args[i] + return args[i]! private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Expr) (value : Expr) : MetaM Expr := do let mvar ← mkFreshExprSyntheticOpaqueMVar codomain let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do if ys.size < xs.size - 1 then - let xDecl ← getLocalDecl xs[ys.size].fvarId! - let xDecl' ← getLocalDecl xs[ys.size + 1].fvarId! + let xDecl ← getLocalDecl xs[ys.size]!.fvarId! + let xDecl' ← getLocalDecl xs[ys.size + 1]!.fvarId! let #[s] ← cases mvarId y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable! - go s.mvarId s.fields[1].fvarId! (ys.push s.fields[0]) + go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!) else let ys := ys.push (mkFVar y) assignExprMVar mvarId (value.replaceFVars xs ys) @@ -91,23 +91,23 @@ partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : Met return preDefs -- Update values for i in [:preDefs.size] do - let preDef := preDefs[i] - let preDefNew := preDefsNew[i] + let preDef := preDefs[i]! + let preDefNew := preDefsNew[i]! let valueNew ← lambdaTelescope preDef.value fun xs body => do let ys : Array Expr := xs[:fixedPrefix] let xs : Array Expr := xs[fixedPrefix:] let type ← instantiateForall preDefNew.type ys forallBoundedTelescope type (some 1) fun z codomain => do - let z := z[0] + let z := z[0]! let newBody ← mkPSigmaCasesOn z codomain xs body mkLambdaFVars (ys.push z) (← packApplications newBody arities preDefsNew) let isBad (e : Expr) : Bool := match isAppOfPreDef? e with | none => false - | some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i].declName != preDefs[i].declName + | some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i]!.declName != preDefs[i]!.declName if let some bad := valueNew.find? isBad then if let some i := isAppOfPreDef? bad then - throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i].declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]}" + throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i]!.declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]!}" preDefsNew := preDefsNew.set! i { preDefNew with value := valueNew } return preDefsNew where @@ -121,7 +121,7 @@ where let pack (e : Expr) (funIdx : Nat) : MetaM Expr := do let f := e.getAppFn let args := e.getAppArgs - let fNew := mkConst preDefsNew[funIdx].declName f.constLevels! + let fNew := mkConst preDefsNew[funIdx]!.declName f.constLevels! let fNew := mkAppN fNew args[:fixedPrefix] let Expr.forallE _ d .. ← inferType fNew | unreachable! let argNew ← mkUnaryArg d args[fixedPrefix:] @@ -148,7 +148,7 @@ where let args ← args.mapM visit if let some funIdx := isAppOfPreDef? f then let numArgs := args.size - let arity := arities[funIdx] + let arity := arities[funIdx]! if numArgs < arity then -- Partial application let extra := arity - numArgs diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index 4845dda4bf..d66ccb8e9e 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean @@ -23,16 +23,16 @@ private def getCodomainLevel (preDefType : Expr) : MetaM Level := This method produces an error if the codomains are in different universe levels. -/ private def getCodomainsLevel (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) : MetaM Level := do - let r ← getCodomainLevel preDefTypes[0] + let r ← getCodomainLevel preDefTypes[0]! for i in [1:preDefTypes.size] do - let preDef := preDefTypes[i] + let preDef := preDefTypes[i]! unless (← isLevelDefEq r (← getCodomainLevel preDef)) do - let arity₀ ← lambdaTelescope preDefsOriginal[0].value fun xs _ => return xs.size - let arityᵢ ← lambdaTelescope preDefsOriginal[i].value fun xs _ => return xs.size - forallBoundedTelescope preDefsOriginal[0].type arity₀ fun _ type₀ => - forallBoundedTelescope preDefsOriginal[i].type arityᵢ fun _ typeᵢ => + let arity₀ ← lambdaTelescope preDefsOriginal[0]!.value fun xs _ => return xs.size + let arityᵢ ← lambdaTelescope preDefsOriginal[i]!.value fun xs _ => return xs.size + forallBoundedTelescope preDefsOriginal[0]!.type arity₀ fun _ type₀ => + forallBoundedTelescope preDefsOriginal[i]!.type arityᵢ fun _ typeᵢ => withOptions (fun o => pp.sanitizeNames.set o false) do - throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0].declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i].declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}" + throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}" return r /-- @@ -50,13 +50,13 @@ private partial def mkNewCoDomain (preDefsOriginal : Array PreDefinition) (preDe let casesOn := mkAppN casesOn xTypeArgs -- parameters let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive let casesOn := mkApp casesOn x -- major - let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0] fun x => - mkLambdaFVars #[x] (preDefTypes[i].bindingBody!.instantiate1 x) - let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1] fun x => do + let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x => + mkLambdaFVars #[x] (preDefTypes[i]!.bindingBody!.instantiate1 x) + let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1]! fun x => do mkLambdaFVars #[x] (← go x (i+1)) return mkApp2 casesOn minor1 minor2 else - return preDefTypes[i].bindingBody!.instantiate1 x + return preDefTypes[i]!.bindingBody!.instantiate1 x go x 0 /-- @@ -78,14 +78,14 @@ private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Arra -/ let givenNames : Array AltVarNames := if i == preDefValues.size - 2 then - #[{ varNames := [varNames[i]] }, { varNames := [varNames[i+1]] }] + #[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }] else - #[{ varNames := [varNames[i]] }] + #[{ varNames := [varNames[i]!] }] let #[s₁, s₂] ← cases mvarId x (givenNames := givenNames) | unreachable! - assignExprMVar s₁.mvarId (mkApp preDefValues[i] s₁.fields[0]).headBeta - go s₂.mvarId s₂.fields[0].fvarId! (i+1) + assignExprMVar s₁.mvarId (mkApp preDefValues[i]! s₁.fields[0]!).headBeta + go s₂.mvarId s₂.fields[0]!.fvarId! (i+1) else - assignExprMVar mvarId (mkApp preDefValues[i] (mkFVar x)).headBeta + assignExprMVar mvarId (mkApp preDefValues[i]! (mkFVar x)).headBeta go mvar.mvarId! x.fvarId! 0 instantiateMVars mvar @@ -112,10 +112,10 @@ private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (do (← whnfD type).withApp fun f args => do assert! args.size == 2 if i == fidx then - return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0] args[1] arg + return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg else - let r ← mkNewArg (i+1) args[1] - return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0] args[1] r + let r ← mkNewArg (i+1) args[1]! + return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r return TransformStep.done <| mkApp (mkAppN (mkConst newFn us) fixedArgs) (← mkNewArg 0 domain) return TransformStep.done e @@ -126,7 +126,7 @@ where match i with | 0 => k fvars (← preDefs.mapM fun preDef => instantiateForall preDef.type fvars) vals | i+1 => - withLocalDecl vals[0].bindingName! vals[0].binderInfo vals[0].bindingDomain! fun x => + withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => go i (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) /-- @@ -171,7 +171,7 @@ where Remark: `preDefsOriginal` is used for error reporting, it contains the definitions before applying `packDomain`. -/ def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preDefs : Array PreDefinition) : MetaM PreDefinition := do - if preDefs.size == 1 then return preDefs[0] + if preDefs.size == 1 then return preDefs[0]! withFixedPrefix fixedPrefix preDefs fun ys types vals => do let domains := types.map fun type => type.bindingDomain! let domain ← mkNewDomain domains @@ -179,8 +179,8 @@ def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preD let codomain ← mkNewCoDomain preDefsOriginal types x let type ← mkForallFVars (ys.push x) codomain let value ← packValues x codomain vals - let newFn := preDefs[0].declName ++ `_mutual - let preDefNew := { preDefs[0] with declName := newFn, type, value } + let newFn := preDefs[0]!.declName ++ `_mutual + let preDefNew := { preDefs[0]! with declName := newFn, type, value } addAsAxiom preDefNew let value ← transform value (post := post fixedPrefix preDefs domain newFn) let value ← mkLambdaFVars (ys.push x) value diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index 468117cd19..fcde49b8f3 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -18,13 +18,13 @@ private def getRefFromElems (elems : Array TerminationByElement) : Syntax := Id. for elem in elems do if !elem.implicit then return elem.ref - return elems[0].ref + return elems[0]!.ref private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do if i < preDefs.size - 1 then let #[s₁, s₂] ← cases mvarId fvarId | unreachable! - go (i + 1) s₂.mvarId s₂.fields[0].fvarId! (result.push (s₁.fields[0].fvarId!, s₁.mvarId)) + go (i + 1) s₂.mvarId s₂.fields[0]!.fvarId! (result.push (s₁.fields[0]!.fvarId!, s₁.mvarId)) else return result.push (fvarId, mvarId) go 0 mvarId fvarId #[] @@ -33,9 +33,9 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva let varNames ← lambdaTelescope preDef.value fun xs _ => do let mut varNames ← xs.mapM fun x => return (← getLocalDecl x.fvarId!).userName if element.vars.size > varNames.size then - throwErrorAt element.vars[varNames.size] "too many variable names" + throwErrorAt element.vars[varNames.size]! "too many variable names" for i in [:element.vars.size] do - let varStx := element.vars[i] + let varStx := element.vars[i]! if varStx.isIdent then varNames := varNames.set! (varNames.size - element.vars.size + i) varStx.getId return varNames @@ -47,8 +47,8 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}" if i < numPackedArgs - 1 then - let #[s] ← cases mvarId fvarId #[{ varNames := [varNames[prefixSize + i]] }] | unreachable! - go (i+1) s.mvarId s.fields[1].fvarId! + let #[s] ← cases mvarId fvarId #[{ varNames := [varNames[prefixSize + i]!] }] | unreachable! + go (i+1) s.mvarId s.fields[1]!.fvarId! else rename mvarId fvarId varNames.back go 0 mvarId fvarId diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean index f3d4a12771..9b17b636e6 100644 --- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean @@ -136,7 +136,7 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N usedElse := true unless elements.isEmpty do if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then - withRef elements[0].ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'" + withRef elements[0]!.ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'" result := result.push { elements } if !usedElse && elseElemStx?.isSome then withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case" @@ -191,6 +191,6 @@ def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := else if !hasUsedAllImplicit then unless reportedAllImplicit do reportedAllImplicit := true - Macro.throwErrorAt clique.elements[0].ref "unused termination hint element" + Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element" end Lean.Elab.WF diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 55a2849d8f..400a976b26 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -54,7 +54,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax | #[e] => return e | es => do let stx ← mkTuple (es.eraseIdx 0) - `(Prod.mk $(es[0]) $stx) + `(Prod.mk $(es[0]!) $stx) def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) := -- decode macro scopes from name before recursion @@ -152,7 +152,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term | $[_%$ids],* => Array.empty) | _ => let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back - `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr) + `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr) let arr ← if k == `sepBy then `(mkSepArray $arr $(getSepStxFromSplice arg)) else @@ -383,7 +383,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := yes ← `(let $id := tuples.map (fun $tuple => $id); $yes) `(tuples) let contents := if contents.size == 1 - then contents[0] + then contents[0]! else mkNullNode contents `(match ($(discrs).sequenceMap fun | `($contents) => some $tuple diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 6bc7837bc1..98d95e96af 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -98,7 +98,7 @@ def Source.isNone : Source → Bool /-- `optional (atomic (sepBy1 termParser ", " >> " with ")` -/ private def mkSourcesWithSyntax (sources : Array Syntax) : Syntax := - let ref := sources[0] + let ref := sources[0]! let stx := Syntax.mkSep sources (mkAtomFrom ref ", ") mkNullNode #[stx, mkAtomFrom ref "with "] @@ -167,7 +167,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource let cont (val : Syntax) : TermElabM Expr := do let lval := modifyOp[0][0] let idx := lval[1] - let self := sources[0].stx + let self := sources[0]!.stx let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val)) trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}" withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? @@ -199,8 +199,8 @@ private def getStructName (expectedType? : Option Expr) (sourceView : Source) : match sourceView, expectedType? with | Source.explicit sources, _ => if sources.size > 1 then - throwErrorAt sources[1].stx "invalid \{...} notation, expected type is not known, using the type of the first source, extra sources are not needed" - return sources[0].structName + throwErrorAt sources[1]!.stx "invalid \{...} notation, expected type is not known, using the type of the first source, extra sources are not needed" + return sources[0]!.structName | _, some expectedType => throwUnexpectedExpectedType expectedType | _, none => throwUnknownExpectedType match expectedType? with @@ -389,7 +389,7 @@ private def expandNumLitFields (s : Struct) : TermElabM Struct := | { lhs := FieldLHS.fieldIndex ref idx :: rest, .. } => if idx == 0 then throwErrorAt ref "invalid field index, index must be greater than 0" else if idx > fieldNames.size then throwErrorAt ref "invalid field index, structure has only #{fieldNames.size} fields" - else pure { field with lhs := FieldLHS.fieldName ref fieldNames[idx - 1] :: rest } + else pure { field with lhs := FieldLHS.fieldName ref fieldNames[idx - 1]! :: rest } | _ => pure field /- For example, consider the following structures: diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 6f14bce042..535e20c685 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -668,7 +668,7 @@ private def collectLevelParamsInStructure (structType : Expr) (scopeVars : Array private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr | 0, type => pure type | i+1, type => do - let info := fieldInfos[i] + let info := fieldInfos[i]! let decl ← Term.getFVarLocalDecl! info.fvar let type ← instantiateMVars type let type := type.abstract #[info.fvar] diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 6b0150e5c5..97cf646f7d 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -21,9 +21,9 @@ private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) := if ds.size == 0 then throwUnsupportedSyntax else if ds.size == 1 then - pure ds[0] + pure ds[0]! else - let mut (r, stackSum) := ds[0] + let mut (r, stackSum) := ds[0]! for (d, stackSz) in ds[1:ds.size] do r ← `(ParserDescr.binary `andthen $r $d) stackSum := stackSum + stackSz @@ -376,11 +376,11 @@ def inferMacroRulesAltKind : TSyntax ``matchAlt → CommandElabM SyntaxNodeKind Infer syntax kind `k` from first pattern, put alternatives of same kind into new `macro/elab_rules (kind := k)` via `mkCmd (some k)`, leave remaining alternatives (via `mkCmd none`) to be recursively expanded. -/ def expandNoKindMacroRulesAux (alts : Array (TSyntax ``matchAlt)) (cmdName : String) (mkCmd : Option Name → Array (TSyntax ``matchAlt) → CommandElabM Command) : CommandElabM Command := do - let mut k ← inferMacroRulesAltKind alts[0] + let mut k ← inferMacroRulesAltKind alts[0]! if k.isStr && k.getString! == "antiquot" then k := k.getPrefix if k == choiceKind then - throwErrorAt alts[0] + throwErrorAt alts[0]! "invalid {cmdName} alternative, multiple interpretations for pattern (solution: specify node kind using `{cmdName} (kind := ...) ...`)" else let altsK ← alts.filterM fun alt => return checkRuleKind (← inferMacroRulesAltKind alt) k diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 5e45c5a177..7526345b11 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -172,8 +172,8 @@ where -- Succeeded. Collect new TC problems let mut pending := [] for i in [:bis.size] do - if bis[i] == BinderInfo.instImplicit then - pending := mvars[i].mvarId! :: pending + if bis[i]! == BinderInfo.instImplicit then + pending := mvars[i]!.mvarId! :: pending synthesizePending pending else return false @@ -274,8 +274,8 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do found := found.insert (lhs, rhs) uniqueEntries := uniqueEntries.push entry for i in [1:uniqueEntries.size] do - logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]) - throwErrorAt uniqueEntries[0].ref (← mkLevelStuckErrorMessage uniqueEntries[0]) + logErrorAt uniqueEntries[i]!.ref (← mkLevelStuckErrorMessage uniqueEntries[i]!) + throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!) /-- Try to solve postponed universe constraints, and throws an exception if there are stuck constraints. diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 44053fc85c..297768b22c 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -23,9 +23,9 @@ open Parser.Tactic let args := stx[0].getArgs for i in [:args.size] do if i % 2 == 0 then - evalTactic args[i] + evalTactic args[i]! else - saveTacticInfoForToken args[i] -- add `TacticInfo` node for `;` + saveTacticInfoForToken args[i]! -- add `TacticInfo` node for `;` @[builtinTactic paren] def evalParen : Tactic := fun stx => evalTactic stx[1] @@ -348,9 +348,9 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List where loop (tacs : Array Syntax) (i : Nat) := if i == tacs.size - 1 then - evalTactic tacs[i][1] + evalTactic tacs[i]![1] else - evalTactic tacs[i][1] <|> loop tacs (i+1) + evalTactic tacs[i]![1] <|> loop tacs (i+1) @[builtinTactic «fail»] def evalFail : Tactic := fun stx => do let goals ← getGoals diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 4c920dec19..78e6b4d12b 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -22,10 +22,10 @@ private def congrApp (mvarId : MVarId) (lhs rhs : Expr) (addImplicitArgs := fals for arg in args do let addGoal ← if i < infos.size then - pure (addImplicitArgs || infos[i].binderInfo.isExplicit) + pure (addImplicitArgs || infos[i]!.binderInfo.isExplicit) else pure (← whnfD (← inferType r.expr)).isArrow - let hasFwdDep := i < infos.size && infos[i].hasFwdDeps + let hasFwdDep := i < infos.size && infos[i]!.hasFwdDeps if addGoal then if hasFwdDep then newGoals := newGoals.push none diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 133581d166..b8a46f7076 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -125,7 +125,7 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) let ctx ← read unless s.targetPos < ctx.targets.size do throwError "insufficient number of targets for '{elimInfo.name}'" - let target := ctx.targets[s.targetPos] + let target := ctx.targets[s.targetPos]! let expectedType ← getArgExpectedType let target ← withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do Term.ensureHasType expectedType target modify fun s => { s with targetPos := s.targetPos + 1 } @@ -183,7 +183,7 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N private def checkAltNames (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax) : TacticM Unit := for i in [:altsSyntax.size] do - let altStx := altsSyntax[i] + let altStx := altsSyntax[i]! if getAltName altStx == `_ && i != altsSyntax.size - 1 then withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative" let altName := getAltName altStx @@ -208,7 +208,7 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar for fvarId in fvarIds do if !useNamesForExplicitOnly || (← getLocalDecl fvarId).binderInfo.isExplicit then if i < altVars.size then - Term.addLocalVarInfo altVars[i] (mkFVar fvarId) + Term.addLocalVarInfo altVars[i]! (mkFVar fvarId) i := i + 1 /-- @@ -240,7 +240,7 @@ def reorderAlts (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax) : Ar for altStx in altsSyntax do let altName := getAltName altStx let some i := alts.findIdx? (·.1 == altName) | return result ++ alts - result := result.push alts[i] + result := result.push alts[i]! alts := alts.eraseIdx i return result ++ alts @@ -266,13 +266,13 @@ where let altStx? ← match altsSyntax.findIdx? (fun alt => getAltName alt == altName) with | some idx => - let altStx := altsSyntax[idx] + let altStx := altsSyntax[idx]! altsSyntax := altsSyntax.eraseIdx idx pure (some altStx) | none => match altsSyntax.findIdx? (fun alt => getAltName alt == `_) with | some idx => isWildcard := true - pure (some altsSyntax[idx]) + pure (some altsSyntax[idx]!) | none => pure none match altStx? with @@ -323,7 +323,7 @@ where if usedWildcard then altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_ unless altsSyntax.isEmpty do - logErrorAt altsSyntax[0] "unused alternative" + logErrorAt altsSyntax[0]! "unused alternative" setGoals subgoals.toList applyPreTac (mvarId : MVarId) : TacticM (List MVarId) := if optPreTac.isNone then @@ -471,7 +471,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti return elimInfo unless targets.size == 1 do throwError "eliminator must be provided when multiple targets are used (use 'using '), and no default eliminator has been registered using attribute `[eliminator]`" - let indVal ← getInductiveValFromMajor targets[0] + let indVal ← getInductiveValFromMajor targets[0]! if induction && indVal.all.length != 1 then throwError "'induction' tactic does not support mutually inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives" if induction && indVal.isNested then @@ -520,7 +520,7 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do ElimApp.mkElimApp elimInfo targets tag trace[Elab.induction] "elimApp: {result.elimApp}" let elimArgs := result.elimApp.getAppArgs - ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds + ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts assignExprMVar mvarId result.elimApp ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds) @@ -548,7 +548,7 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) := let mut j := 0 for arg in args do if (← shouldGeneralizeTarget arg.expr) || arg.hName?.isSome then - result := result.push (mkFVar fvarIdsNew[j]) + result := result.push (mkFVar fvarIdsNew[j]!) j := j+1 else result := result.push arg.expr @@ -575,12 +575,12 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) := let targets ← addImplicitTargets elimInfo targets let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag let elimArgs := result.elimApp.getAppArgs - let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i] - let motiveType ← inferType elimArgs[elimInfo.motivePos] + let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]! + let motiveType ← inferType elimArgs[elimInfo.motivePos]! let mvarId ← generalizeTargetsEq mvarId motiveType targets let (targetsNew, mvarId) ← introN mvarId targets.size withMVarContext mvarId do - ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetsNew + ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew assignExprMVar mvarId result.elimApp ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew) diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean index 30ca7a03da..e415a973e9 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/src/Lean/Elab/Tactic/Match.lean @@ -28,7 +28,6 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM if holeOrTacticSeq.isOfKind ``Parser.Term.syntheticHole then pure () else if holeOrTacticSeq.isOfKind ``Parser.Term.hole then - let s ← get let tag := if alts.size > 1 then parentTag ++ (`match).appendIndexAfter nextIdx else parentTag let holeName := mkIdentFrom holeOrTacticSeq tag let newHole ← `(?$holeName:ident) diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index feda6e7650..d8339fc9d5 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -34,7 +34,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ()) let numRules := (rules.size + 1) / 2 for i in [:numRules] do - let rule := rules[i * 2] + let rule := rules[i * 2]! let sep := rules.getD (i * 2 + 1) Syntax.missing -- show rule state up to (incl.) next `,` withTacticInfoContext (mkNullNode #[rule, sep]) do diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 830071a0f2..c8e1f56ad9 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -143,7 +143,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) -/ withMainContext do let mut thmsArray := ctx.simpTheorems - let mut thms := thmsArray[0] + let mut thms := thmsArray[0]! let mut starArg := false for arg in stx[1].getSepArgs do if arg.getKind == ``Lean.Parser.Tactic.simpErase then diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean index 53dd0c97a8..a4a905f393 100644 --- a/src/Lean/Elab/Tactic/Split.lean +++ b/src/Lean/Elab/Tactic/Split.lean @@ -23,7 +23,7 @@ open Meta let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "" return mvarIds else - let fvarId ← getFVarId hyps[0] + let fvarId ← getFVarId hyps[0]! liftMetaTactic fun mvarId => do let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "" return mvarIds diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 951ba5207e..4b52143f5a 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -204,7 +204,7 @@ where loop (i : Nat) (env : Environment) : IO Environment := do let envExtensions ← envExtensionsRef.get if i < envExtensions.size then - let s ← envExtensions[i].mkInitial + let s ← envExtensions[i]!.mkInitial let env := { env with extensions := env.extensions.push s } loop (i + 1) env else @@ -593,7 +593,7 @@ where -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions. let pExtDescrs ← persistentEnvExtensionsRef.get if i < pExtDescrs.size then - let extDescr := pExtDescrs[i] + let extDescr := pExtDescrs[i]! let s := extDescr.toEnvExtension.getState env let prevSize := (← persistentEnvExtensionsRef.get).size let prevAttrSize ← getNumBuiltiAttributes diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index cd39ec318d..07e1c7ed32 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -366,7 +366,7 @@ partial def normalize (l : Level) : Level := let lvls := lvls.qsort normLt let firstNonExplicit := skipExplicit lvls 0 let i := if isExplicitSubsumed lvls firstNonExplicit then firstNonExplicit else firstNonExplicit - 1 - let lvl₁ := lvls[i] + let lvl₁ := lvls[i]! let prev := lvl₁.getLevelOffset let prevK := lvl₁.getOffset mkMaxAux lvls k (i+1) prev prevK levelZero diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index aad39263bb..a80adca01d 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -347,7 +347,7 @@ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr := @[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr := let b := b.abstract xs xs.size.foldRev (init := b) fun i b => - let x := xs[i] + let x := xs[i]! match lctx.findFVar? x with | some (LocalDecl.cdecl _ _ n ty bi) => let ty := ty.abstractRange i xs; diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean index e5808ae23b..d7dd4d3808 100644 --- a/src/Lean/Meta/ACLt.lean +++ b/src/Lean/Meta/ACLt.lean @@ -80,15 +80,15 @@ where let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo for i in [:infos.size] do -- We ignore instance implicit arguments during comparison - if !infos[i].isInstImplicit then - if (← lt aArgs[i] bArgs[i]) then + if !infos[i]!.isInstImplicit then + if (← lt aArgs[i]! bArgs[i]!) then return true - else if (← lt bArgs[i] aArgs[i]) then + else if (← lt bArgs[i]! aArgs[i]!) then return false for i in [infos.size:aArgs.size] do - if (← lt aArgs[i] bArgs[i]) then + if (← lt aArgs[i]! bArgs[i]!) then return true - else if (← lt bArgs[i] aArgs[i]) then + else if (← lt bArgs[i]! aArgs[i]!) then return false return false @@ -118,11 +118,11 @@ where let infos := (← getFunInfoNArgs f args.size).paramInfo for i in [:infos.size] do -- We ignore instance implicit arguments during comparison - if !infos[i].isInstImplicit then - if !(← lt args[i] b) then + if !infos[i]!.isInstImplicit then + if !(← lt args[i]! b) then return false for i in [infos.size:args.size] do - if !(← lt args[i] b) then + if !(← lt args[i]! b) then return false return true | Expr.lam _ d e .. => lt d b <&&> lt e b diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 48ea6723e8..b146a8691d 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -218,7 +218,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met let mvar ← mkFreshExprMVar d MetavarKind.synthetic n loop b i j (args.push mvar) (instMVars.push mvar.mvarId!) | _ => - let x := xs[i] + let x := xs[i]! let xType ← inferType x if (← isDefEq d xType) then loop b (i+1) j (args.push x) instMVars diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index f76f7589ae..63af2aa092 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1061,7 +1061,7 @@ partial def withLocalDecls where loop [Inhabited α] (acc : Array Expr) : n α := do if acc.size < declInfos.size then - let (name, bi, typeCtor) := declInfos[acc.size] + let (name, bi, typeCtor) := declInfos[acc.size]! withLocalDecl name bi (←typeCtor acc) fun x => loop (acc.push x) else k acc diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 172547c910..bc7cb40b4e 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -31,9 +31,9 @@ def toCasesOnApp? (e : Expr) : MetaM (Option CasesOnApp) := do let args := e.getAppArgs unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none let params := args[:info.numParams] - let motive := args[info.numParams] + let motive := args[info.numParams]! let indices := args[info.numParams + 1 : info.numParams + 1 + info.numIndices] - let major := args[info.numParams + 1 + info.numIndices] + let major := args[info.numParams + 1 + info.numIndices]! let alts := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors] let remaining := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :] let propOnly := info.levelParams.length == us.length @@ -94,7 +94,7 @@ where let alt := alt.beta xs let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative if checkIfRefined then - return (← mkLambdaFVars xs alt, !(← isDefEq argType (← inferType x[0]))) + return (← mkLambdaFVars xs alt, !(← isDefEq argType (← inferType x[0]!))) else return (← mkLambdaFVars xs alt, true) if refinedAt then diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index 29caa140c0..5e9d65b909 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -92,8 +92,8 @@ where return (mkAppN a.getAppFn as', mkAppN b.getAppFn bs') else for i in [:as.size] do - unless (← isDefEq as[i] bs[i]) do - let (ai, bi) ← visit as[i] bs[i] + unless (← isDefEq as[i]! bs[i]!) do + let (ai, bi) ← visit as[i]! bs[i]! as := as.set! i ai bs := bs.set! i bi let a := mkAppN a.getAppFn as @@ -104,10 +104,10 @@ where hasExplicitDiff? (xs as bs : Array Expr) : MetaM (Option (Array Expr × Array Expr)) := do for i in [:xs.size] do - let localDecl ← getLocalDecl xs[i].fvarId! + let localDecl ← getLocalDecl xs[i]!.fvarId! if localDecl.binderInfo.isExplicit then - unless (← isDefEq as[i] bs[i]) do - let (ai, bi) ← visit as[i] bs[i] + unless (← isDefEq as[i]! bs[i]!) do + let (ai, bi) ← visit as[i]! bs[i]! return some (as.set! i ai, bs.set! i bi) return none diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 2a9def77bc..ff7667cf9b 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -287,7 +287,7 @@ partial def process : ClosureM Unit := do let xs := decls.map LocalDecl.toExpr let b := b.abstract xs decls.size.foldRev (init := b) fun i b => - let decl := decls[i] + let decl := decls[i]! match decl with | LocalDecl.cdecl _ _ n ty bi => let ty := ty.abstractRange i xs diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 386d2b902e..0d32d4a6e5 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -77,8 +77,8 @@ where withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α := let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do if i < xs.size then - let x := xs[i] - let y := ys[i] + let x := xs[i]! + let y := ys[i]! let xType := (← inferType x).consumeTypeAnnotations let yType := (← inferType y).consumeTypeAnnotations if xType == yType then @@ -98,9 +98,9 @@ where mkHEqRefl lhs else forallBoundedTelescope type (some 1) fun a type => - let a := a[0] + let a := a[0]! forallBoundedTelescope type (some 1) fun b motive => - let b := b[0] + let b := b[0]! let type := type.bindingBody!.instantiate1 a withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do let type := type.bindingBody! @@ -122,8 +122,8 @@ private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind let mut kinds := kinds for i in [:info.paramInfo.size] do for j in [i+1:info.paramInfo.size] do - if info.paramInfo[j].backDeps.contains i then - if kinds[j] matches CongrArgKind.eq || kinds[j] matches CongrArgKind.fixed then + if info.paramInfo[j]!.backDeps.contains i then + if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed. kinds := kinds.set! i CongrArgKind.fixed break @@ -136,7 +136,7 @@ private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do let rec go (i : Nat) (type : Expr) : MetaM Expr := do if i < deps.size then - match eqs[deps[i]] with + match eqs[deps[i]!]! with | none => go (i+1) type | some major => let some (_, lhs, rhs) := (← inferType major).eq? | unreachable! @@ -158,15 +158,15 @@ private def hasCastLike (kinds : Array CongrArgKind) : Bool := kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do - forallBoundedTelescope type (some 1) fun xs type => k xs[0] type + forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type /-- Test whether we should use `subsingletonInst` kind for instances which depend on `eq`. (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/ private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do - if info.paramInfo[i].isDecInst then - for j in info.paramInfo[i].backDeps do - if kinds[j] matches CongrArgKind.eq then + if info.paramInfo[i]!.isDecInst then + for j in info.paramInfo[i]!.backDeps do + if kinds[j]! matches CongrArgKind.eq then return true return false @@ -183,9 +183,9 @@ def getCongrSimpKinds (info : FunInfo) : Array CongrArgKind := Id.run do for i in [:info.paramInfo.size] do if info.resultDeps.contains i then result := result.push CongrArgKind.fixed - else if info.paramInfo[i].isProp then + else if info.paramInfo[i]!.isProp then result := result.push CongrArgKind.cast - else if info.paramInfo[i].isInstImplicit then + else if info.paramInfo[i]!.isInstImplicit then if shouldUseSubsingletonInst info result i then result := result.push CongrArgKind.subsingletonInst else @@ -228,23 +228,23 @@ where let proof ← mkProof type kinds return { type, proof, argKinds := kinds } else - let hyps := hyps.push lhss[i] - match kinds[i] with + let hyps := hyps.push lhss[i]! + match kinds[i]! with | CongrArgKind.heq => unreachable! | CongrArgKind.fixedNoParam => unreachable! | CongrArgKind.eq => - let localDecl ← getLocalDecl lhss[i].fvarId! + let localDecl ← getLocalDecl lhss[i]!.fvarId! withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do - withLocalDeclD ((`e).appendIndexAfter (eqs.size+1)) (← mkEq lhss[i] rhs) fun eq => do + withLocalDeclD ((`e).appendIndexAfter (eqs.size+1)) (← mkEq lhss[i]! rhs) fun eq => do go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq) - | CongrArgKind.fixed => go (i+1) (rhss.push lhss[i]) (eqs.push none) hyps + | CongrArgKind.fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps | CongrArgKind.cast => - let rhsType := (← inferType lhss[i]).replaceFVars (lhss[:rhss.size]) rhss - let rhs ← mkCast lhss[i] rhsType info.paramInfo[i].backDeps eqs + let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss + let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs go (i+1) (rhss.push rhs) (eqs.push none) hyps | CongrArgKind.subsingletonInst => - let rhsType := (← inferType lhss[i]).replaceFVars (lhss[:rhss.size]) rhss - withLocalDecl (← getLocalDecl lhss[i].fvarId!).userName BinderInfo.instImplicit rhsType fun rhs => + let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss + withLocalDecl (← getLocalDecl lhss[i]!.fvarId!).userName BinderInfo.instImplicit rhsType fun rhs => go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs) return some (← go 0 #[] #[] #[]) catch _ => @@ -257,7 +257,7 @@ where mkEqRefl lhs else withNext type fun lhs type => do - match kinds[i] with + match kinds[i]! with | CongrArgKind.heq => unreachable! | CongrArgKind.fixedNoParam => unreachable! | CongrArgKind.fixed => mkLambdaFVars #[lhs] (← go (i+1) type) diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index 52158e5ffc..b7c560a30e 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -352,7 +352,7 @@ private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Tri def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α := if keys.isEmpty then panic! "invalid key sequence" else - let k := keys[0] + let k := keys[0]! match d.root.find? k with | none => let c := createNodes keys v 1 @@ -463,7 +463,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr else let e := todo.back let todo := todo.pop - let first := cs[0] /- Recall that `Key.star` is the minimal key -/ + let first := cs[0]! /- Recall that `Key.star` is the minimal key -/ let (k, args) ← getMatchKeyArgs e (root := false) /- We must always visit `Key.star` edges since they are wildcards. Thus, `todo` is not used linearly when there is `Key.star` edge @@ -565,7 +565,7 @@ where let todo := todo.pop let (k, args) ← getUnifyKeyArgs e (root := false) let visitStar (result : Array α) : MetaM (Array α) := - let first := cs[0] + let first := cs[0]! if first.1 == Key.star then process 0 todo first.2 result else diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index ae3e8f763f..0cdb2d2f8c 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -55,9 +55,9 @@ where for i in [ctorVal.numParams : args.size] do let j := i - ctorVal.numParams let proj ← mkProjFn ctorVal us params j a - trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]}" - unless (← isDefEq proj args[i]) do - trace[Meta.isDefEq.eta.struct] "failed, unexpect arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]}" + trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}" + unless (← isDefEq proj args[i]!) do + trace[Meta.isDefEq.eta.struct] "failed, unexpect arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}" return false return true else @@ -167,8 +167,8 @@ private partial def isDefEqArgsFirstPass let rec loop (i : Nat) (postponed : Array Nat) := do if h : i < paramInfo.size then let info := paramInfo.get ⟨i, h⟩ - let a₁ := args₁[i] - let a₂ := args₂[i] + let a₁ := args₁[i]! + let a₂ := args₂[i]! if !info.isExplicit then if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then if (← Meta.isExprDefEqAux a₁ a₂) then @@ -210,9 +210,9 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta /- Second pass: unify implicit arguments. In the second pass, we make sure we are unfolding at least non reducible definitions (default setting). -/ - let a₁ := args₁[i] - let a₂ := args₂[i] - let info := finfo.paramInfo[i] + let a₁ := args₁[i]! + let a₂ := args₂[i]! + let info := finfo.paramInfo[i]! if info.isInstImplicit then discard <| trySynthPending a₁ discard <| trySynthPending a₂ @@ -239,7 +239,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let fvar := fvars.get ⟨i, h⟩ let fvarDecl ← getFVarLocalDecl fvar let fvarType := fvarDecl.type - let d₂ := ds₂[i] + let d₂ := ds₂[i]! if (← Meta.isExprDefEqAux fvarType d₂) then match (← isClass? fvarType) with | some className => withNewLocalInstance className fvar <| loop (i+1) @@ -333,7 +333,7 @@ where We use it a quick-check to avoid the more expensive collection procedure. -/ hasLetDeclsInBetween : MetaM Bool := do let check (lctx : LocalContext) : Bool := Id.run do - let start := lctx.getFVar! xs[0] |>.index + let start := lctx.getFVar! xs[0]! |>.index let stop := lctx.getFVar! xs.back |>.index for i in [start+1:stop] do match lctx.getAt? i with @@ -391,7 +391,7 @@ where /- Computes the set `ys`. It is a set of `FVarId`s, -/ collectLetDeps : MetaM FVarIdHashSet := do let lctx ← getLCtx - let start := lctx.getFVar! xs[0] |>.index + let start := lctx.getFVar! xs[0]! |>.index let stop := lctx.getFVar! xs.back |>.index let s := xs.foldl (init := {}) fun s x => s.insert x.fvarId! let (_, s) ← collectLetDepsAux stop |>.run start |>.run s @@ -403,7 +403,7 @@ where let lctx ← getLCtx let s ← collectLetDeps /- Convert `s` into the array `ys` -/ - let start := lctx.getFVar! xs[0] |>.index + let start := lctx.getFVar! xs[0]! |>.index let stop := lctx.getFVar! xs.back |>.index let mut ys := #[] for i in [start:stop+1] do diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index 75c744ac89..e3756fc733 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -79,14 +79,14 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId) if e.isApp then let args := e.getAppArgs for i in [:args.size] do - let arg := args[i] + let arg := args[i]! if arg.isMVar && isTarget.contains arg then let mvarId := arg.mvarId! if (← Meta.getMVarDecl mvarId).userName.isAnonymous then forallBoundedTelescope (← inferType e.getAppFn) (some (i+1)) fun xs _ => do if i < xs.size then let mvarId := arg.mvarId! - let userName ← mkFreshUserName (← getFVarLocalDecl xs[i]).userName + let userName ← mkFreshUserName (← getFVarLocalDecl xs[i]!).userName toReset.modify (·.push mvarId) modifyMCtx fun mctx => mctx.setMVarUserNameTemporarily mvarId userName toReset.get diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index 3ba872c87f..7635e440ed 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -57,7 +57,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := forallBoundedTelescope fnType maxArgs? fun fvars type => do let mut pinfo := #[] for i in [:fvars.size] do - let fvar := fvars[i] + let fvar := fvars[i]! let decl ← getFVarLocalDecl fvar let backDeps := collectDeps fvars decl.type pinfo := updateHasFwdDeps pinfo backDeps diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index 2b0331a726..b8306d2c7a 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -108,7 +108,7 @@ partial def mkCtorType where addHeaderVars (vars : Variables) := do let headersWithNames ← ctx.headers.mapIdxM fun idx header => - return (ctx.belowNames[idx], fun _ : Array Expr => pure header) + return (ctx.belowNames[idx]!, fun _ : Array Expr => pure header) withLocalDeclsD headersWithNames fun xs => addMotives { vars with indVal := xs } @@ -122,7 +122,7 @@ where modifyBinders (vars : Variables) (i : Nat) := do if i < vars.args.size then - let binder := vars.args[i] + let binder := vars.args[i]! let binderType ← inferType binder if (← checkCount binderType) then mkBelowBinder vars binder binderType fun indValIdx x => @@ -136,16 +136,16 @@ where vars.innerType.withApp fun _ args => do let hApp := mkAppN - (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam) + (mkConst originalCtor.name $ ctx.typeInfos[0]!.levelParams.map mkLevelParam) (vars.params ++ vars.args) - let innerType := mkAppN vars.indVal[belowIdx] $ + let innerType := mkAppN vars.indVal[belowIdx]! $ vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp] let x ← mkForallFVars vars.target innerType return replaceTempVars vars x replaceTempVars (vars : Variables) (ctor : Expr) := let levelParams := - ctx.typeInfos[0].levelParams.map mkLevelParam + ctx.typeInfos[0]!.levelParams.map mkLevelParam ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal => mkConst indVal levelParams @@ -178,7 +178,7 @@ where fun indVal => indVal.name == name then let hApp := mkAppN binder xs let t := - mkAppN vars.indVal[idx] $ + mkAppN vars.indVal[idx]! $ vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp] let newDomain ← mkForallFVars xs t @@ -195,7 +195,7 @@ where forallTelescopeReducing domain fun xs t => do t.withApp fun _ args => do let hApp := mkAppN binder xs - let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp] + let t := mkAppN vars.motives[indValIdx]! $ args[ctx.numParams:] ++ #[hApp] let newDomain ← mkForallFVars xs t withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k @@ -206,7 +206,7 @@ where def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor := do let ctorInfo ← getConstInfoCtor ctor - let name := ctor.updatePrefix ctx.belowNames[i] + let name := ctor.updatePrefix ctx.belowNames[i]! let type ← mkCtorType ctx i ctorInfo return { name := name @@ -217,18 +217,18 @@ def mkInductiveType (i : Fin ctx.typeInfos.size) (indVal : InductiveVal) : MetaM InductiveType := do return { - name := ctx.belowNames[i] - type := ctx.headers[i] + name := ctx.belowNames[i]! + type := ctx.headers[i]! ctors := (← indVal.ctors.mapM (mkConstructor ctx i)) } def mkBelowDecl (ctx : Context) : MetaM Declaration := do - let lparams := ctx.typeInfos[0].levelParams + let lparams := ctx.typeInfos[0]!.levelParams return Declaration.inductDecl lparams (ctx.numParams + ctx.motives.size) (←ctx.typeInfos.mapIdxM $ mkInductiveType ctx).toList - ctx.typeInfos[0].isUnsafe + ctx.typeInfos[0]!.isUnsafe partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do if depth = 0 then return false @@ -280,7 +280,7 @@ where let motives ← ctx.motives.mapIdxM fun idx (_, motive) => do let motive ← instantiateForall motive params forallTelescopeReducing motive fun xs _ => do - mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs) + mkLambdaFVars xs <| mkAppN (mkConst ctx.belowNames[idx]! levelParams) $ (params ++ motives ++ xs) let recursorInfo ← getConstInfo $ mkRecName indVal.name let recLevels := if recursorInfo.numLevelParams > levelParams.length @@ -315,7 +315,7 @@ where def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do let type ← mkType - let indVal := ctx.typeInfos[idx] + let indVal := ctx.typeInfos[idx]! let name := indVal.name ++ brecOnSuffix return Declaration.thmDecl { name := name @@ -324,13 +324,13 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do value := ←proveBrecOn ctx indVal type } where mkType : MetaM Expr := - forallTelescopeReducing ctx.headers[idx] fun xs _ => do + forallTelescopeReducing ctx.headers[idx]! fun xs _ => do let params := xs[:ctx.numParams] let motives := xs[ctx.numParams:ctx.numParams + ctx.motives.size].toArray let indices := xs[ctx.numParams + ctx.motives.size:] let motiveBinders ← ctx.motives.mapIdxM $ mkIH params motives withLocalDeclsD motiveBinders fun ys => do - mkForallFVars (xs ++ ys) (mkAppN motives[idx] indices) + mkForallFVars (xs ++ ys) (mkAppN motives[idx]! indices) mkIH (params : Array Expr) (motives : Array Expr) @@ -343,13 +343,13 @@ where let ih ← instantiateForall motive.2 params let mkDomain (_ : Array Expr) : MetaM Expr := forallTelescopeReducing ih fun ys _ => do - let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam + let levels := ctx.typeInfos[idx]!.levelParams.map mkLevelParam let args := params ++ motives ++ ys let premise := mkAppN - (mkConst ctx.belowNames[idx.val] levels) args + (mkConst ctx.belowNames[idx.val]! levels) args let conclusion := - mkAppN motives[idx] ys + mkAppN motives[idx]! ys mkForallFVars ys (←mkArrow premise conclusion) return (←name, mkDomain) @@ -367,7 +367,7 @@ where (belowIndices : Array Nat) (xIdx yIdx : Nat) : MetaM $ Array Nat := do if xIdx ≥ xs.size then return belowIndices else - let x := xs[xIdx] + let x := xs[xIdx]! let xTy ← inferType x let yTy := rest.bindingDomain! if (← isDefEq xTy yTy) then @@ -378,10 +378,10 @@ where loop xs rest belowIndices xIdx (yIdx + 1) private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Name × Expr := do - (← inferType xs[idx]).withApp fun type args => do + (← inferType xs[idx]!).withApp fun type args => do let indName := type.constName! let indInfo ← getConstInfoInduct indName - let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]] + let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]!] let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs return (indName, belowType) @@ -414,7 +414,7 @@ partial def mkBelowMatcher let motive ← newMotive belowType xs pure (indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType) - let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName + let lhss ← mkMatcherInput.lhss.mapM <| addBelowPattern indName let alts ← mkMatcherInput.lhss.zip lhss |>.toArray.zip matcherApp.alts |>.mapIdxM fun idx ((oldLhs, lhs), alt) => do withExistingLocalDecls (oldLhs.fvarDecls ++ lhs.fvarDecls) do lambdaTelescope alt fun xs t => do @@ -441,7 +441,7 @@ partial def mkBelowMatcher -- we check here, so that errors can propagate higher up the call stack. check res.matcher let newApp := mkApp res.matcher motive - let newApp := mkAppN newApp $ matcherApp.discrs.push below + let newApp := mkAppN newApp <| matcherApp.discrs.push below let newApp := mkAppN newApp alts return (newApp, res.addMatcher) @@ -449,8 +449,8 @@ where addBelowPattern (indName : Name) (lhs : AltLHS) : MetaM AltLHS := do withExistingLocalDecls lhs.fvarDecls do let patterns := lhs.patterns.toArray - let originalPattern := patterns[idx] - let (fVars, belowPattern) ← convertToBelow indName patterns[idx] + let originalPattern := patterns[idx]! + let (fVars, belowPattern) ← convertToBelow indName patterns[idx]! withExistingLocalDecls fVars.toList do let patterns := patterns.push belowPattern let patterns := patterns.set! idx (←toInaccessible originalPattern) @@ -488,7 +488,7 @@ where let mut belowFieldOpts := mkArray belowCtor.numFields none let fields := fields.toArray for fieldIdx in [:fields.size] do - belowFieldOpts := belowFieldOpts.set! belowIndices[fieldIdx] (some fields[fieldIdx]) + belowFieldOpts := belowFieldOpts.set! belowIndices[fieldIdx]! (some fields[fieldIdx]!) let belowParams := params.toArray.push belowMotive let belowCtorExpr := mkAppN (mkConst belowCtor.name us) belowParams @@ -516,7 +516,7 @@ where (belowFields : Array Pattern) (additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Pattern) := do if belowFields.size ≥ belowFieldOpts.size then pure (additionalFVars, belowFields) else - if let some belowField := belowFieldOpts[belowFields.size] then + if let some belowField := belowFieldOpts[belowFields.size]! then let belowFieldExpr ← belowField.toExpr let belowCtor := mkApp belowCtor belowFieldExpr let patTy ← inferType belowFieldExpr @@ -587,7 +587,7 @@ def mkBelow (declName : Name) : MetaM Unit := do try let decl ← IndPredBelow.mkBrecOnDecl ctx i addDecl decl - catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]}\n{e.toMessageData}" + catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]!}\n{e.toMessageData}" else trace[Meta.IndPredBelow] "Not recursive" else trace[Meta.IndPredBelow] "Not inductive predicate" diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index b8d7dd4a49..3b51f10604 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -54,7 +54,7 @@ where -- So, we must have offset ≤ vidx, since we are in the "else" branch of `if offset >= e.looseBVarRange` let n := stop - start if vidx < offset + n then - return args[stop - (vidx - offset) - 1].liftLooseBVars 0 offset + return args[stop - (vidx - offset) - 1]!.liftLooseBVars 0 offset else return mkBVar (vidx - n) -- The following cases are unreachable because they never contain loose bound variables diff --git a/src/Lean/Meta/Match/CaseArraySizes.lean b/src/Lean/Meta/Match/CaseArraySizes.lean index 527124fb44..6ab1e34720 100644 --- a/src/Lean/Meta/Match/CaseArraySizes.lean +++ b/src/Lean/Meta/Match/CaseArraySizes.lean @@ -71,7 +71,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam let hEqSz := (subst.get hEq).fvarId! if h : i.val < sizes.size then let n := sizes.get ⟨i, h⟩ - let mvarId ← clear mvarId subgoal.newHs[0] + let mvarId ← clear mvarId subgoal.newHs[0]! let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId! withMVarContext mvarId do let hEqSzSymm ← mkEqSymm (mkFVar hEqSz) diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index a0b6099c08..9085e47557 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -32,8 +32,8 @@ private partial def withEqs (lhs rhs : Array Expr) (discrInfos : Array DiscrInfo where go (i : Nat) (hs : Array Expr) : MetaM α := do if i < lhs.size then - if let some hName := discrInfos[i].hName? then - withLocalDeclD hName (← mkEqHEq lhs[i] rhs[i]) fun h => + if let some hName := discrInfos[i]!.hName? then + withLocalDeclD hName (← mkEqHEq lhs[i]! rhs[i]!) fun h => go (i+1) (hs.push h) else go (i+1) hs @@ -880,7 +880,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor let mut isEqMaskIdx := 0 for discr in discrs, info in discrInfos do if info.hName?.isSome then - if isEqMask[isEqMaskIdx] then + if isEqMask[isEqMaskIdx]! then rfls := rfls.push (← mkEqRefl discr) else rfls := rfls.push (← mkHEqRefl discr) @@ -910,7 +910,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput let matchType ← do let u := if let some idx := matcherInfo.uElimPos? - then mkLevelParam matcherConst.levelParams.toArray[idx] + then mkLevelParam matcherConst.levelParams.toArray[idx]! else levelZero forallBoundedTelescope matcherType (some matcherInfo.numDiscrs) fun discrs _ => do mkForallFVars discrs (mkConst ``PUnit [u]) @@ -949,7 +949,7 @@ end Match private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (i : Nat) : MetaM (Array Nat × Array Expr) := do if h : i < alts.size then let alt := alts.get ⟨i, h⟩ - let numParams := altNumParams[i] + let numParams := altNumParams[i]! let typeNew ← whnfD typeNew match typeNew with | Expr.forallE _ d b _ => @@ -980,8 +980,8 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" let eType ← inferType e let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do - let motiveArg := motiveArgs[i] - let discr := matcherApp.discrs[i] + let motiveArg := motiveArgs[i]! + let discr := matcherApp.discrs[i]! let eTypeAbst ← kabstract eTypeAbst discr return eTypeAbst.instantiate1 motiveArg let motiveBody ← mkArrow eTypeAbst motiveBody diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 90190bb42b..adb66fa3ec 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -35,14 +35,14 @@ where match (← getProjectionFnInfo? declName) with | some projInfo => if projInfo.numParams < args.size then - findFVar? args[projInfo.numParams] + findFVar? args[projInfo.numParams]! else return none | none => matchConstRec f (fun _ => return none) fun recVal _ => do if recVal.getMajorIdx >= args.size then return none - let major := args[recVal.getMajorIdx] + let major := args[recVal.getMajorIdx]! if major.isFVar then return some major.fvarId! else @@ -118,7 +118,7 @@ where /- Recall that alternatives that do not have variables have a `Unit` parameter to ensure they are not eagerly evaluated. -/ if ys.size == 1 then - if (← inferType ys[0]).isConstOf ``Unit && !(← dependsOn type ys[0].fvarId!) then + if (← inferType ys[0]!).isConstOf ``Unit && !(← dependsOn type ys[0]!.fvarId!) then return (← k #[] #[] #[mkConst ``Unit.unit] #[false] type) k ys eqs args mask type @@ -459,7 +459,7 @@ where let mut argsNew := args let mut isAlt := #[] for i in [6:args.size] do - let arg := argsNew[i] + let arg := argsNew[i]! if arg.isFVar then match (← read).find? arg.fvarId! with | some (altNew, _, _) => @@ -473,13 +473,13 @@ where argsNew := argsNew.set! i (← convertTemplate arg) isAlt := isAlt.push false assert! isAlt.size == args.size - 6 - let rhs := args[4] - let motive := args[2] + let rhs := args[4]! + let motive := args[2]! -- Construct new motive using the splitter theorem minor premise types. let motiveNew ← lambdaTelescope motive fun motiveArgs body => do unless motiveArgs.size == 1 do throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with 1 binder{indentExpr motive}" - let x := motiveArgs[0] + let x := motiveArgs[0]! forallTelescopeReducing body fun motiveTypeArgs resultType => do unless motiveTypeArgs.size >= isAlt.size do throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected arrow with at least #{isAlt.size} binders{indentExpr body}" @@ -487,15 +487,15 @@ where assert! motiveTypeArgsNew.size == i if h : i < motiveTypeArgs.size then let motiveTypeArg := motiveTypeArgs.get ⟨i, h⟩ - if i < isAlt.size && isAlt[i] then - let altNew := argsNew[6+i] -- Recall that `Eq.ndrec` has 6 arguments + if i < isAlt.size && isAlt[i]! then + let altNew := argsNew[6+i]! -- Recall that `Eq.ndrec` has 6 arguments let altTypeNew ← inferType altNew trace[Meta.Match.matchEqs] "altNew: {altNew} : {altTypeNew}" -- Replace `rhs` with `x` (the lambda binder in the motive) let mut altTypeNewAbst := (← kabstract altTypeNew rhs).instantiate1 x -- Replace args[6:6+i] with `motiveTypeArgsNew` for j in [:i] do - altTypeNewAbst := (← kabstract altTypeNewAbst argsNew[6+j]).instantiate1 motiveTypeArgsNew[j] + altTypeNewAbst := (← kabstract altTypeNewAbst argsNew[6+j]!).instantiate1 motiveTypeArgsNew[j]! let localDecl ← getLocalDecl motiveTypeArg.fvarId! withLocalDecl localDecl.userName localDecl.binderInfo altTypeNewAbst fun motiveTypeArgNew => go (i+1) (motiveTypeArgsNew.push motiveTypeArgNew) @@ -513,18 +513,18 @@ where let eqRecNewPrefix := mkAppN f argsNew[:3] -- `Eq.ndrec` minor premise is the fourth argument. let .forallE _ minorTypeNew .. ← whnf (← inferType eqRecNewPrefix) | unreachable! trace[Meta.Match.matchEqs] "new minor type: {minorTypeNew}" - let minor := args[3] + let minor := args[3]! let minorNew ← forallBoundedTelescope minorTypeNew isAlt.size fun minorArgsNew _ => do let mut minorBodyNew := minor -- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises let mut m ← read for i in [:isAlt.size] do - if isAlt[i] then + if isAlt[i]! then -- `convertTemplate` will correct occurrences of the alternative - let alt := args[6+i] -- Recall that `Eq.ndrec` has 6 arguments + let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable! -- We add a new entry to `m` to make sure `convertTemplate` will correct the occurrences of the alternative - m := m.insert minorArgsNew[i].fvarId! (minorArgsNew[i], numParams, argMask) + m := m.insert minorArgsNew[i]!.fvarId! (minorArgsNew[i]!, numParams, argMask) unless minorBodyNew.isLambda do throwError "unexpected `Eq.ndrec` minor premise while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with at least #{isAlt.size} binders{indentExpr minor}" minorBodyNew := minorBodyNew.bindingBody! @@ -619,7 +619,7 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := forallTelescopeReducing constInfo.type fun xs matchResultType => do let mut eqnNames := #[] let params := xs[:matchInfo.numParams] - let motive := xs[matchInfo.getMotivePos] + let motive := xs[matchInfo.getMotivePos]! let alts := xs[xs.size - matchInfo.numAlts:] let firstDiscrIdx := matchInfo.numParams + 1 let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs] @@ -629,7 +629,7 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := let mut splitterAltNumParams := #[] let mut altArgMasks := #[] -- masks produced by `forallAltTelescope` for i in [:alts.size] do - let altNumParams := matchInfo.altNumParams[i] + let altNumParams := matchInfo.altNumParams[i]! let altNonEqNumParams := altNumParams - numDiscrEqs let thmName := baseName ++ ((`eq).appendIndexAfter idx) eqnNames := eqnNames.push thmName @@ -651,7 +651,7 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant. Thus, we need to create new `alts`. -/ withNewAlts numDiscrEqs discrs patterns alts fun alts => do - let alt := alts[i] + let alt := alts[i]! let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts) let rhs := mkAppN alt rhsArgs let thmType ← mkEq lhs rhs diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index 8d592fabe9..40563bf3dc 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -148,7 +148,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] (e : Expr) : m (Option MatcherApp) : matcherLevels := declLevels.toArray uElimPos? := info.uElimPos? params := args.extract 0 info.numParams - motive := args[info.getMotivePos] + motive := args[info.getMotivePos]! discrs := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs] altNumParams := info.altNumParams alts := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts] diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 053b8ed650..24da9eff8c 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -137,7 +137,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do let mut paramsPos := #[] for i in [:numParams] do - let x := xs[i] + let x := xs[i]! match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with | some j => paramsPos := paramsPos.push (some j) | none => do @@ -152,7 +152,7 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic let mut indicesPos := #[] for i in [:numIndices] do let i := majorPos - numIndices + i - let x := xs[i] + let x := xs[i]! match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with | some j => indicesPos := indicesPos.push j | none => throwError "invalid user defined recursor '{declName}', type of the major premise does not contain the recursor index" @@ -187,7 +187,7 @@ private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices if majorPos - numIndices ≤ i && i ≤ majorPos then continue -- skip indices and major premise -- process minor premise - let x := xs[i] + let x := xs[i]! let xType ← inferType x (produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do let produceMotive := produceMotive.push (res == motive) diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean index 77c0c47770..27765dc655 100644 --- a/src/Lean/Meta/Reduce.lean +++ b/src/Lean/Meta/Reduce.lean @@ -26,13 +26,13 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta let mut args := e.getAppArgs for i in [:args.size] do if i < finfo.paramInfo.size then - let info := finfo.paramInfo[i] + let info := finfo.paramInfo[i]! if !explicitOnly || info.isExplicit then args ← args.modifyM i visit else args ← args.modifyM i visit - if f.isConstOf ``Nat.succ && args.size == 1 && args[0].isNatLit then - return mkRawNatLit (args[0].natLit?.get! + 1) + if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isNatLit then + return mkRawNatLit (args[0]!.natLit?.get! + 1) else return mkAppN f args | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b) diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 72b683e446..a9ae724a9b 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -14,7 +14,7 @@ private partial def mkLocalInstances {α} (params : Array Expr) (k : Array Expr where loop (i : Nat) (insts : Array Expr) : MetaM α := do if i < params.size then - let param := params[i] + let param := params[i]! let paramType ← inferType param let instType? ← forallTelescopeReducing paramType fun xs _ => do let type := mkAppN param xs @@ -65,7 +65,7 @@ private partial def mkSizeOfMotives {α} (motiveFVars : Array Expr) (k : Array E where loop (i : Nat) (motives : Array Expr) : MetaM α := do if i < motiveFVars.size then - let type ← inferType motiveFVars[i] + let type ← inferType motiveFVars[i]! let motive ← forallTelescopeReducing type fun xs _ => do mkLambdaFVars xs <| mkConst ``Nat trace[Meta.sizeOf] "motive: {motive}" @@ -97,14 +97,14 @@ private partial def mkSizeOfMinors {α} (motiveFVars : Array Expr) (minorFVars : where loop (i : Nat) (minors : Array Expr) : MetaM α := do if i < minorFVars.size then - forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ => do - forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do + forallTelescopeReducing (← inferType minorFVars[i]!) fun xs _ => do + forallBoundedTelescope (← inferType minorFVars'[i]!) xs.size fun xs' _ => do let mut minor ← mkNumeral (mkConst ``Nat) 1 for x in xs, x' in xs' do unless (← isInductiveHypothesis motiveFVars x) do unless (← ignoreField x) do -- we suppress higher-order fields match (← isRecField? motiveFVars xs x) with - | some idx => minor ← mkAdd minor (← mkSizeOfRecFieldFormIH xs'[idx]) + | some idx => minor ← mkAdd minor (← mkSizeOfRecFieldFormIH xs'[idx]!) | none => minor ← mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x']) minor ← mkLambdaFVars xs' minor trace[Meta.sizeOf] "minor: {minor}" @@ -124,7 +124,7 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do 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 major := xs[recInfo.getMajorIdx]! let nat := mkConst ``Nat mkLocalInstances params fun localInsts => mkSizeOfMotives motiveFVars fun motives => do @@ -217,7 +217,7 @@ private def recToSizeOf (e : Expr) : M Expr := do | some sizeOfName => let args := e.getAppArgs let indices := args[info.getFirstIndexIdx : info.getFirstIndexIdx + info.numIndices] - let major := args[info.getMajorIdx] + let major := args[info.getMajorIdx]! return mkAppN (mkConst sizeOfName us.tail!) ((← read).params ++ (← read).localInsts ++ indices ++ #[major]) mutual diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index ffd304c312..623e3574c2 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -25,7 +25,7 @@ structure PreContext where instance : ContextInformation (PreContext × Array Bool) where isComm ctx := ctx.1.comm.isSome isIdem ctx := ctx.1.idem.isSome - isNeutral ctx x := ctx.2[x] + isNeutral ctx x := ctx.2[x]! instance : EvalInformation PreContext ACExpr where arbitrary _ := Data.AC.Expr.var 0 @@ -86,7 +86,7 @@ def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr × Lean.Expr) := do let (vars, acExpr) ← toACExpr preContext.op l r - let α ← inferType vars[0] + let α ← inferType vars[0]! let u ← getLevel α let (isNeutrals, context) ← mkContext α u vars let acExprNormed := Data.AC.evalList ACExpr preContext $ Data.AC.norm (preContext, isNeutrals) acExpr @@ -97,7 +97,7 @@ def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr × return (proof, tgt) where mkContext (α : Expr) (u : Level) (vars : Array Expr) : MetaM (Array Bool × Expr) := do - let arbitrary := vars[0] + let arbitrary := vars[0]! let zero := mkLevelZeroEx () let noneE := mkApp (mkConst ``Option.none [zero]) let someE := mkApp2 (mkConst ``Option.some [zero]) @@ -135,7 +135,7 @@ where convertTarget (vars : Array Expr) : ACExpr → Expr | Data.AC.Expr.op l r => mkApp2 preContext.op (convertTarget vars l) (convertTarget vars r) - | Data.AC.Expr.var x => vars[x] + | Data.AC.Expr.var x => vars[x]! def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do let simpCtx := diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index acb4cca4ba..b81c48b0d5 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -27,8 +27,8 @@ private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := newMVars.size.forM fun i => do - if binderInfos[i].isInstImplicit then - let mvar := newMVars[i] + if binderInfos[i]!.isInstImplicit then + let mvar := newMVars[i]! let mvarType ← inferType mvar let mvarVal ← synthInstance mvarType unless (← isDefEq mvar mvarVal) do @@ -38,13 +38,13 @@ def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Arr let parentTag ← getMVarTag mvarId if newMVars.size == 1 then -- if there is only one subgoal, we inherit the parent tag - setMVarTag newMVars[0].mvarId! parentTag + setMVarTag newMVars[0]!.mvarId! parentTag else unless parentTag.isAnonymous do newMVars.size.forM fun i => do - let newMVarId := newMVars[i].mvarId! + let newMVarId := newMVars[i]!.mvarId! unless (← isExprMVarAssigned newMVarId) do - unless binderInfos[i].isInstImplicit do + unless binderInfos[i]!.isInstImplicit do let currTag ← getMVarTag newMVarId setMVarTag newMVarId (appendTag parentTag currTag) diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean index 89d7259e94..9ad05eef4a 100644 --- a/src/Lean/Meta/Tactic/Assert.lean +++ b/src/Lean/Meta/Tactic/Assert.lean @@ -81,7 +81,7 @@ def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Ex assignExprMVar mvarId (mkAppN mvarNew args) let (fvarIdNew, mvarIdNew) ← intro1P mvarNew.mvarId! let (fvarIdsNew, mvarIdNew) ← introNP mvarIdNew fvarIds.size - let subst := fvarIds.size.fold (init := {}) fun i subst => subst.insert fvarIds[i] (mkFVar fvarIdsNew[i]) + let subst := fvarIds.size.fold (init := {}) fun i subst => subst.insert fvarIds[i]! (mkFVar fvarIdsNew[i]!) pure { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst } structure Hypothesis where diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index 8a44be69f9..c70fb8c5ce 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -35,7 +35,7 @@ private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do private partial def withNewEqs (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α := let rec loop (i : Nat) (newEqs : Array Expr) (newRefls : Array Expr) := do if i < targets.size then - let (newEqType, newRefl) ← mkEqAndProof targets[i] targetsNew[i] + let (newEqType, newRefl) ← mkEqAndProof targets[i]! targetsNew[i]! withLocalDeclD `h newEqType fun newEq => do loop (i+1) (newEqs.push newEq) (newRefls.push newRefl) else @@ -167,7 +167,7 @@ private def hasIndepIndices (ctx : Context) : MetaM Bool := do else if ctx.majorTypeIndices.any fun idx => !idx.isFVar then /- One of the indices is not a free variable. -/ pure false - else if ctx.majorTypeIndices.size.any fun i => i.any fun j => ctx.majorTypeIndices[i] == ctx.majorTypeIndices[j] then + else if ctx.majorTypeIndices.size.any fun i => i.any fun j => ctx.majorTypeIndices[i]! == ctx.majorTypeIndices[j]! then /- An index ocurrs more than once -/ pure false else @@ -195,7 +195,7 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name) (majorFVarId : FVarId) (us : List Level) (params : Array Expr) : Array CasesSubgoal := s.mapIdx fun i s => - let ctorName := ctorNames[i] + let ctorName := ctorNames[i]! let ctorApp := mkAppN (mkAppN (mkConst ctorName us) params) s.fields let s := { s with subst := s.subst.insert majorFVarId ctorApp } { ctorName := ctorName, diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 0eada8cd87..e1ece88bfd 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -42,7 +42,7 @@ def getElimInfo (declName : Name) : MetaM ElimInfo := do | some targetPos => pure targetPos.val let mut altsInfo := #[] for i in [:xs.size] do - let x := xs[i] + let x := xs[i]! if x != motive && !targets.contains x then let xDecl ← getLocalDecl x.fvarId! if xDecl.binderInfo.isExplicit then @@ -72,7 +72,7 @@ where if c.binderInfo.isExplicit then unless targetIdx < targets.size do throwError "insufficient number of targets for '{elimInfo.name}'" - let target := targets[targetIdx] + let target := targets[targetIdx]! let targetType ← inferType target unless (← isDefEq d targetType) do throwError "target{indentExpr target}\n{← mkHasTypeButIsExpectedMsg targetType d}" @@ -112,12 +112,12 @@ def mkCustomEliminator (declName : Name) : MetaM CustomEliminator := do forallTelescopeReducing info.type fun xs _ => do let mut typeNames := #[] for i in [:elimInfo.targetsPos.size] do - let targetPos := elimInfo.targetsPos[i] - let x := xs[targetPos] + let targetPos := elimInfo.targetsPos[i]! + let x := xs[targetPos]! /- Return true if there is another target that depends on `x`. -/ let isImplicitTarget : MetaM Bool := do for j in [i+1:elimInfo.targetsPos.size] do - let y := xs[elimInfo.targetsPos[j]] + let y := xs[elimInfo.targetsPos[j]!]! let yType ← inferType y if (← dependsOn yType x.fvarId!) then return true diff --git a/src/Lean/Meta/Tactic/Generalize.lean b/src/Lean/Meta/Tactic/Generalize.lean index 8c560467b6..502cb94e3f 100644 --- a/src/Lean/Meta/Tactic/Generalize.lean +++ b/src/Lean/Meta/Tactic/Generalize.lean @@ -26,7 +26,7 @@ partial def generalize let target ← instantiateMVars (← getMVarType mvarId) let rec go (i : Nat) : MetaM Expr := do if i < args.size then - let arg := args[i] + let arg := args[i]! let e ← instantiateMVars arg.expr let eType ← instantiateMVars (← inferType e) let type ← go (i+1) @@ -46,15 +46,15 @@ partial def generalize let (rfls, targetNew) ← forallBoundedTelescope targetNew args.size fun xs type => do let rec go' (i : Nat) : MetaM (List Expr × Expr) := do if i < xs.size then - let arg := args[i] + let arg := args[i]! if let some hName := arg.hName? then - let xType ← inferType xs[i] + let xType ← inferType xs[i]! let e ← instantiateMVars arg.expr let eType ← instantiateMVars (← inferType e) let (hType, r) ← if (← isDefEq xType eType) then - pure (← mkEq e xs[i], ← mkEqRefl e) + pure (← mkEq e xs[i]!, ← mkEqRefl e) else - pure (← mkHEq e xs[i], ← mkHEqRefl e) + pure (← mkHEq e xs[i]!, ← mkHEqRefl e) let (rs, type) ← go' (i+1) return (r :: rs, mkForall hName BinderInfo.default hType type) else diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean index d6e5e52036..e9421941a3 100644 --- a/src/Lean/Meta/Tactic/Induction.lean +++ b/src/Lean/Meta/Tactic/Induction.lean @@ -107,8 +107,8 @@ private partial def finalize let subst := reverted.size.fold (init := baseSubst) fun i (subst : FVarSubst) => if i < indices.size + 1 then subst else - let revertedFVarId := reverted[i] - let newFVarId := extra[i - indices.size - 1] + let revertedFVarId := reverted[i]! + let newFVarId := extra[i - indices.size - 1]! subst.insert revertedFVarId (mkFVar newFVarId) let fields := fields.map mkFVar loop (pos+1) (minorIdx+1) recursor recursorType consumedMajor (subgoals.push { mvarId := mvarId', fields := fields, subst := subst }) @@ -140,7 +140,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi let idx := majorTypeArgs.get! idxPos unless idx.isFVar do throwTacticEx `induction mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}" majorTypeArgs.size.forM fun i => do - let arg := majorTypeArgs[i] + let arg := majorTypeArgs[i]! if i != idxPos && arg == idx then throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}" if i < idxPos && mctx.exprDependsOn arg idx.fvarId! then @@ -165,7 +165,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi let mut subst : FVarSubst := {} let mut i := 0 for index in indices do - subst := subst.insert index.fvarId! (mkFVar indices'[i]) + subst := subst.insert index.fvarId! (mkFVar indices'[i]!) i := i + 1 pure subst trace[Meta.Tactic.induction] "after revert&intro\n{MessageData.ofGoal mvarId}" diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index 71649e8bfc..2185c1081c 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -16,7 +16,7 @@ def getCtorNumPropFields (ctorInfo : ConstructorVal) : MetaM Nat := do forallTelescopeReducing ctorInfo.type fun xs _ => do let mut numProps := 0 for i in [:ctorInfo.numFields] do - if (← isProp (← inferType xs[ctorInfo.numParams + i])) then + if (← isProp (← inferType xs[ctorInfo.numParams + i]!)) then numProps := numProps + 1 return numProps diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 47f09c9faf..7085dcb617 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -108,11 +108,11 @@ abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) := def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do let (fvarIds, mvarId) ← introN mvarId 1 [name] - return (fvarIds[0], mvarId) + return (fvarIds[0]!, mvarId) def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId) := do let (fvarIds, mvarId) ← introNCore mvarId 1 [] (useNamesForExplicitOnly := false) preserveBinderNames - return (fvarIds[0], mvarId) + return (fvarIds[0]!, mvarId) abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := intro1Core mvarId false diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean index 72032fa2f9..28ff61ff98 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean +++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean @@ -41,7 +41,7 @@ open Nat.Linear.Expr in def LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) : MetaM Expr := do match e with | num v => return mkNatLit v - | var i => return ctx[i] + | var i => return ctx[i]! | add a b => mkAdd (← toArith ctx a) (← toArith ctx b) | mulL k a => mkMul (mkNatLit k) (← toArith ctx a) | mulR a k => mkMul (← toArith ctx a) (mkNatLit k) diff --git a/src/Lean/Meta/Tactic/LinearArith/Solver.lean b/src/Lean/Meta/Tactic/LinearArith/Solver.lean index b4995ef92d..6b02bc1db1 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Solver.lean +++ b/src/Lean/Meta/Tactic/LinearArith/Solver.lean @@ -196,10 +196,10 @@ abbrev State.getNumVars (s : State) : Nat := s.lowers.size abbrev State.currVar (s : State) : Nat := s.assignment.size abbrev State.getBestLowerBound? (s : State) : Option (Rat × Cnstr) := - getBestBound? s.lowers[s.currVar] s.assignment true s.int[s.currVar] + getBestBound? s.lowers[s.currVar]! s.assignment true s.int[s.currVar]! abbrev State.getBestUpperBound? (s : State) : Option (Rat × Cnstr) := - getBestBound? s.uppers[s.currVar] s.assignment false s.int[s.currVar] + getBestBound? s.uppers[s.currVar]! s.assignment false s.int[s.currVar]! abbrev State.assignCurr (s : State) (v : Rat) : State := { s with assignment := s.assignment.push v } diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 3e98d59fac..3ca87a3de0 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -224,7 +224,7 @@ partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do let mut args := e.getAppArgs let mut modified := false for i in [:args.size] do - let arg := args[i] + let arg := args[i]! if isDummyEqRec arg then args := args.set! i (elimDummyEqRec arg) modified := true @@ -339,8 +339,8 @@ where let mut r := r let mut i := 0 for arg in args do - trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}" - if i < infos.size && !infos[i].hasFwdDeps then + trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i]!.hasFwdDeps}" + if i < infos.size && !infos[i]!.hasFwdDeps then r ← mkCongr r (← simp arg) else if (← whnfD (← inferType r.expr)).isArrow then r ← mkCongr r (← simp arg) @@ -455,7 +455,7 @@ where subst := subst.push instNew type := type.bindingBody! | CongrArgKind.eq => - let argResult := argResults[j] + let argResult := argResults[j]! let argProof ← argResult.getProof' arg j := j + 1 proof := mkApp2 proof argResult.expr argProof @@ -526,7 +526,7 @@ where if (← isDefEq lhs e) then let mut modified := false for i in c.hypothesesPos do - let x := xs[i] + let x := xs[i]! try if (← processCongrHypothesis x) then modified := true diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index 09bd05f99a..f6f83caa1c 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -51,7 +51,7 @@ private partial def loop : M Bool := do modify fun s => { s with modified := false } -- simplify entries for i in [:(← get).entries.size] do - let entry := (← get).entries[i] + let entry := (← get).entries[i]! let ctx := (← get).ctx -- We disable the current entry to prevent it to be simplified to `True` let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 466d4783ff..aa74062161 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -63,8 +63,8 @@ private partial def withEqs (lhs rhs : Array Expr) (k : Array Expr → Array Exp where go (i : Nat) (hs : Array Expr) (rfls : Array Expr) : MetaM α := do if i < lhs.size then - withLocalDeclD (← mkFreshUserName `heq) (← mkEqHEq lhs[i] rhs[i]) fun h => do - let rfl ← if (← inferType h).isEq then mkEqRefl lhs[i] else mkHEqRefl lhs[i] + withLocalDeclD (← mkFreshUserName `heq) (← mkEqHEq lhs[i]! rhs[i]!) fun h => do + let rfl ← if (← inferType h).isEq then mkEqRefl lhs[i]! else mkHEqRefl lhs[i]! go (i+1) (hs.push h) (rfls.push rfl) else k hs rfls @@ -121,8 +121,8 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N foundRef.set true let mut altsNew := #[] for i in [:matcherApp.alts.size] do - let alt := matcherApp.alts[i] - let altNumParams := matcherApp.altNumParams[i] + let alt := matcherApp.alts[i]! + let altNumParams := matcherApp.altNumParams[i]! let altNew ← lambdaTelescope alt fun xs body => do if xs.size < altNumParams || xs.size < numDiscrEqs then throwError "'applyMatchSplitter' failed, unexpected `match` alternative" @@ -164,8 +164,8 @@ where -- `eqs'.size == altEqs.size ≤ eqs.size` let rec go (i : Nat) (altEqsNew : Array Expr) (subst : Array Expr) : MetaM Expr := do if i < altEqs.size then - let altEqDecl ← getFVarLocalDecl altEqs[i] - let eq := eqs'[i] + let altEqDecl ← getFVarLocalDecl altEqs[i]! + let eq := eqs'[i]! let eqType ← inferType eq let altEqType := altEqDecl.type match eqType.eq?, altEqType.eq? with @@ -232,7 +232,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le unless mvarIds.length == matchEqns.size do throwError "'applyMatchSplitter' failed, unexpected number of goals created after applying splitter for '{matcherDeclName}'." let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do - let numParams := matchEqns.splitterAltNumParams[i] + let numParams := matchEqns.splitterAltNumParams[i]! let (_, mvarId) ← introN mvarId numParams trace[Meta.Tactic.split] "before unifyEqs\n{mvarId}" match (← Cases.unifyEqs? (numEqs + info.getNumDiscrEqs) mvarId {}) with @@ -249,7 +249,7 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do let matchEqns ← Match.getEquationsFor app.matcherName let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do - let mvarId ← simpMatchTargetCore mvarId app.matcherName matchEqns.eqnNames[i] + let mvarId ← simpMatchTargetCore mvarId app.matcherName matchEqns.eqnNames[i]! return (i+1, mvarId::mvarIds) return mvarIds.reverse catch ex => @@ -278,7 +278,7 @@ where else if let some info := isMatcherAppCore? env e then let args := e.getAppArgs for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do - if args[i].hasLooseBVars then + if args[i]!.hasLooseBVars then return false return true else diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index 71e1fd0ee0..3358c13b82 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -37,9 +37,9 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let (twoVars, mvarId) ← introNP mvarId 2 trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}" trace[Meta.Tactic.subst] "reverted variables {vars.map (·.name)}" - let aFVarId := twoVars[0] + let aFVarId := twoVars[0]! let a := mkFVar aFVarId - let hFVarId := twoVars[1] + let hFVarId := twoVars[1]! let h := mkFVar hFVarId /- Set skip to true if there is no local variable nor the target depend on the equality -/ let skip ← if !tryToSkip || vars.size != 2 then @@ -81,8 +81,8 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let (newFVars, mvarId) ← introNP mvarId (vars.size - 2) trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}" let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) => - let var := vars[i+2] - let newFVar := newFVars[i] + let var := vars[i+2]! + let newFVar := newFVars[i]! pure $ fvarSubst.insert var (mkFVar newFVar) let fvarSubst := fvarSubst.insert aFVarIdOriginal (if clearH then b else mkFVar aFVarId) let fvarSubst := fvarSubst.insert hFVarIdOriginal (mkFVar hFVarId) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 4526d26d3e..2546d86f42 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -208,10 +208,10 @@ private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : match major with | Expr.app (Expr.app (Expr.app (Expr.const majorFn _ _) _ _) _ _) majorArg _ => do let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getConstNoEx? majorFn | failK () - let f := recArgs[argPos] + let f := recArgs[argPos]! let r := mkApp f majorArg let recArity := majorPos + 1 - successK $ mkAppRange r recArity recArgs.size recArgs + successK <| mkAppRange r recArity recArgs.size recArgs | _ => failK () else failK () @@ -418,7 +418,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do let mut i := prefixSz for h in hs do if auxAppFn == h then - let result := mkAppN args[i] auxApp.getAppArgs + let result := mkAppN args[i]! auxApp.getAppArgs let result := mkAppN result args[prefixSz + info.numAlts:args.size] return ReduceMatcherResult.reduced result.headBeta i := i + 1 diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 67e745fb1f..c74303d6a5 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -778,7 +778,7 @@ instance : MonadHashMapCacheAdapter ExprStructEq Expr M where /-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl := Id.run do - let mut d : LocalDecl := lctx.getFVar! xs[0] + let mut d : LocalDecl := lctx.getFVar! xs[0]! for x in xs[1:] do if x.isFVar then let curr := lctx.getFVar! x @@ -826,9 +826,9 @@ def collectForwardDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : if preserveOrder then -- Make sure toRevert[j] does not depend on toRevert[i] for j > i toRevert.size.forM fun i => do - let fvar := toRevert[i] + let fvar := toRevert[i]! i.forM fun j => do - let prevFVar := toRevert[j] + let prevFVar := toRevert[j]! let prevDecl := lctx.getFVar! prevFVar if localDeclDependsOn mctx prevDecl fvar.fvarId! then throw (Exception.revertFailure mctx lctx toRevert prevDecl.userName.toString) @@ -836,7 +836,7 @@ def collectForwardDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : let firstDeclToVisit := getLocalDeclWithSmallestIdx lctx toRevert let initSize := newToRevert.size lctx.foldlM (init := newToRevert) (start := firstDeclToVisit.index) fun (newToRevert : Array Expr) decl => do - if initSize.any fun i => decl.fvarId == newToRevert[i].fvarId! then + if initSize.any fun i => decl.fvarId == newToRevert[i]!.fvarId! then return newToRevert else if toRevert.any fun x => decl.fvarId == x.fvarId! then return newToRevert.push decl.toExpr @@ -903,7 +903,7 @@ mutual private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do let e ← abstractRangeAux xs xs.size e xs.size.foldRevM (init := e) fun i e => do - let x := xs[i] + let x := xs[i]! if x.isFVar then match lctx.getFVar! x with | LocalDecl.cdecl _ _ n type bi => @@ -1042,7 +1042,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr) @[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) : M (Expr × Nat) := do let e ← abstractRange xs xs.size e xs.size.foldRevM (init := (e, 0)) fun i (e, num) => do - let x := xs[i] + let x := xs[i]! if x.isFVar then match lctx.getFVar! x with | LocalDecl.cdecl _ _ n type bi => diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 5cc68818c7..c3241cf046 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -169,7 +169,7 @@ def findModuleOf? [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m (O discard <| getConstInfo declName -- ensure declaration exists match (← getEnv).getModuleIdxFor? declName with | none => return none - | some modIdx => return some ((← getEnv).allImportedModuleNames[modIdx]) + | some modIdx => return some ((← getEnv).allImportedModuleNames[modIdx]!) def isEnumType [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Bool := do if let ConstantInfo.inductInfo info ← getConstInfo declName then diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index a8692e0aba..9935ea0cb5 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -71,8 +71,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do let mut p := mkConst p let args := e.getAppArgs for i in [:Nat.min params.size args.size] do - let param := params[i] - let arg := args[i] + let param := params[i]! + let arg := args[i]! let paramTy ← inferType param let resultTy ← forallTelescope paramTy fun _ b => pure b let arg ← if resultTy.isConstOf ctx.tyName then compileParserExpr arg else pure arg diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index dc7c7e3c58..1e66d7d614 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -228,11 +228,11 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct let args := e.getAppArgs let fieldVals := args.extract s.numParams args.size for idx in [:fieldNames.size] do - let fieldName := fieldNames[idx] + let fieldName := fieldNames[idx]! let fieldId := mkIdent fieldName let fieldPos ← nextExtraPos let fieldId := annotatePos fieldPos fieldId - addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId fieldVals[idx] + addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId fieldVals[idx]! let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]):term) fields := fields.push field let tyStx ← withType do @@ -317,14 +317,14 @@ private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Te -- Currently, we reset `optionsPerPos` at the beginning of `delabPatterns` to avoid -- incorrectly considering annotations. withTheReader SubExpr ({ · with expr := ty }) $ - usingNames st.varNames[idx] do + usingNames st.varNames[idx]! do withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push (← delab)) where usingNames {α} (varNames : Array Name) (x : DelabM α) : DelabM α := usingNamesAux 0 varNames x usingNamesAux {α} (i : Nat) (varNames : Array Name) (x : DelabM α) : DelabM α := if i < varNames.size then - withBindingBody varNames[i] <| usingNamesAux (i+1) varNames x + withBindingBody varNames[i]! <| usingNamesAux (i+1) varNames x else x @@ -351,7 +351,7 @@ where else -- eta expand `e` let e ← forallTelescopeReducing (← inferType e) fun xs _ => do - if xs.size == 1 && (← inferType xs[0]).isConstOf ``Unit then + if xs.size == 1 && (← inferType xs[0]!).isConstOf ``Unit then -- `e` might be a thunk create by the dependent pattern matching compiler, and `xs[0]` may not even be a pattern variable. -- If it is a pattern variable, it doesn't look too bad to use `()` instead of the pattern variable. -- If it becomes a problem in the future, we should modify the dependent pattern matching compiler, and make sure @@ -392,7 +392,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat else if st.discrs.size < st.info.numDiscrs then let idx := st.discrs.size let discr ← delab - if let some hName := st.info.discrInfos[idx].hName? then + if let some hName := st.info.discrInfos[idx]!.hName? then -- TODO: we should check whether the corresponding binder name, matches `hName`. -- If it does not we should pretty print this `match` as a regular application. return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) } @@ -401,7 +401,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat else if st.rhss.size < st.info.altNumParams.size then /- We save the variables names here to be able to implement safe_shadowing. The pattern delaboration must use the names saved here. -/ - let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size] fun varNames => do + let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size]! fun varNames => do let rhs ← delab return (varNames, rhs) return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames } @@ -732,7 +732,7 @@ partial def delabDoElems : DelabM (List Syntax) := do let e ← getExpr if e.isAppOfArity ``Bind.bind 6 then -- Bind.bind.{u, v} : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} → m α → (α → m β) → m β - let α := e.getAppArgs[2] + let α := e.getAppArgs[2]! let ma ← withAppFn $ withAppArg delab withAppArg do match (← getExpr) with diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 02fd7d25d6..30bb845964 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -86,7 +86,7 @@ def withNaryArg (argIdx : Nat) (x : m α) : m α := do let e ← getExpr let args := e.getAppArgs let newPos := (← getPos).pushNaryArg args.size argIdx - withTheReader SubExpr (fun cfg => { cfg with expr := args[argIdx], pos := newPos }) x + withTheReader SubExpr (fun cfg => { cfg with expr := args[argIdx]!, pos := newPos }) x end Descend diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 38423a798b..9157911c30 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -297,8 +297,8 @@ where -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here? -- if so, I'll need to take a callback if fd.isOutParam then - tryUnify (args[i]) (mvars[i]) - inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars + tryUnify (args[i]!) (mvars[i]!) + inspectAux (fb.instantiate1 args[i]!) (mb.instantiate1 mvars[i]!) (i+1) args mvars | _, _ => return () partial def isTrivialBottomUp (e : Expr) : AnalyzeM Bool := do @@ -322,12 +322,12 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := let fType ← replaceLPsWithVars (← inferType e.getAppFn) let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType e.getAppArgs.size for i in [:mvars.size] do - if bInfos[i] == BinderInfo.instImplicit then - inspectOutParams args[i] mvars[i] - else if bInfos[i] == BinderInfo.default then - if ← isTrivialBottomUp args[i] then tryUnify args[i] mvars[i] - else if ← typeUnknown mvars[i] <&&> canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i] - if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1] + if bInfos[i]! == BinderInfo.instImplicit then + inspectOutParams args[i]! mvars[i]! + else if bInfos[i]! == BinderInfo.default then + if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]! + else if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! mvars[i]! fuel then tryUnify args[i]! mvars[i]! + if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0]! <||> valUnknown mvars[1]!)) then tryUnify mvars[0]! mvars[1]! if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!) return !(← valUnknown resultType) @@ -489,44 +489,44 @@ mutual where collectBottomUps := do let { args, mvars, bInfos, ..} ← read - for target in [fun _ => none, fun i => some mvars[i]] do + for target in [fun _ => none, fun i => some mvars[i]!] do for i in [:args.size] do - if bInfos[i] == BinderInfo.default then - if ← typeUnknown mvars[i] <&&> canBottomUp args[i] (target i) then - tryUnify args[i] mvars[i] + if bInfos[i]! == BinderInfo.default then + if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (target i) then + tryUnify args[i]! mvars[i]! modify fun s => { s with bottomUps := s.bottomUps.set! i true } checkOutParams := do let { args, mvars, bInfos, ..} ← read for i in [:args.size] do - if bInfos[i] == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i] + if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i]! mvars[i]! collectHigherOrders := do let { args, mvars, bInfos, ..} ← read for i in [:args.size] do - if not (bInfos[i] == BinderInfo.implicit || bInfos[i] == BinderInfo.strictImplicit) then continue - if not (← isHigherOrder (← inferType args[i])) then continue - if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i] then continue + if not (bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue + if not (← isHigherOrder (← inferType args[i]!)) then continue + if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue - if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && not (← valUnknown mvars[i]) - && (← isType2Type (args[i])) && (← isFOLike (args[i])) then continue + if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && not (← valUnknown mvars[i]!) + && (← isType2Type (args[i]!)) && (← isFOLike (args[i]!)) then continue - tryUnify args[i] mvars[i] + tryUnify args[i]! mvars[i]! modify fun s => { s with higherOrders := s.higherOrders.set! i true } hBinOpHeuristic := do let { mvars, ..} ← read - if ← (pure (isHBinOp (← getExpr)) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then - tryUnify mvars[0] mvars[1] + if ← (pure (isHBinOp (← getExpr)) <&&> (valUnknown mvars[0]! <||> valUnknown mvars[1]!)) then + tryUnify mvars[0]! mvars[1]! collectTrivialBottomUps := do -- motivation: prevent levels from printing in -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β let { args, mvars, bInfos, ..} ← read for i in [:args.size] do - if bInfos[i] == BinderInfo.default then - if ← valUnknown mvars[i] <&&> isTrivialBottomUp args[i] then - tryUnify args[i] mvars[i] + if bInfos[i]! == BinderInfo.default then + if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i]! then + tryUnify args[i]! mvars[i]! modify fun s => { s with bottomUps := s.bottomUps.set! i true } applyFunBinderHeuristic := do @@ -537,9 +537,9 @@ mutual | Expr.lam .., Expr.forallE _ t b .. => let mut annotated := false for i in [:argIdx] do - if ← pure (bInfos[i] == BinderInfo.implicit) <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then + if ← pure (bInfos[i]! == BinderInfo.implicit) <&&> valUnknown mvars[i]! <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]!) then annotateBool `pp.funBinderTypes - tryUnify args[i] mvars[i] + tryUnify args[i]! mvars[i]! -- Note: currently we always analyze the lambda binding domains in `analyzeLam` -- (so we don't need to analyze it again here) annotated := true @@ -550,8 +550,8 @@ mutual | _, _ => return false for i in [:args.size] do - if bInfos[i] == BinderInfo.default then - let b ← withNaryArg i (core i (← inferType mvars[i])) + if bInfos[i]! == BinderInfo.default then + let b ← withNaryArg i (core i (← inferType mvars[i]!)) if b then modify fun s => { s with funBinders := s.funBinders.set! i true } analyzeFn := do @@ -566,22 +566,22 @@ mutual analyzeArg (i : Nat) := do let { f, args, mvars, bInfos, forceRegularApp ..} ← read let { bottomUps, higherOrders, funBinders, ..} ← get - let arg := args[i] + let arg := args[i]! let argType ← inferType arg let processNaturalImplicit : AnalyzeAppM Unit := do - if (← valUnknown mvars[i] <||> pure higherOrders[i]) && !forceRegularApp then - annotateNamedArg (← mvarName mvars[i]) + if (← valUnknown mvars[i]! <||> pure higherOrders[i]!) && !forceRegularApp then + annotateNamedArg (← mvarName mvars[i]!) modify fun s => { s with provideds := s.provideds.set! i true } else annotateBool `pp.analysis.skip withNaryArg (f.getAppNumArgs + i) do - withTheReader Context (fun ctx => { ctx with inBottomUp := ctx.inBottomUp || bottomUps[i] }) do + withTheReader Context (fun ctx => { ctx with inBottomUp := ctx.inBottomUp || bottomUps[i]! }) do - match bInfos[i] with + match bInfos[i]! with | BinderInfo.default => - if ← pure (getPPAnalyzeExplicitHoles (← getOptions)) <&&> pure !(← valUnknown mvars[i]) <&&> pure !(← readThe Context).inBottomUp <&&> pure !(← isFunLike arg) <&&> pure !funBinders[i] <&&> checkpointDefEq mvars[i] arg then + if ← pure (getPPAnalyzeExplicitHoles (← getOptions)) <&&> pure !(← valUnknown mvars[i]!) <&&> pure !(← readThe Context).inBottomUp <&&> pure !(← isFunLike arg) <&&> pure !funBinders[i]! <&&> checkpointDefEq mvars[i]! arg then annotateBool `pp.analysis.hole else modify fun s => { s with provideds := s.provideds.set! i true } @@ -601,22 +601,22 @@ mutual match instResult with | LOption.some inst => if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip; provided := false - else annotateNamedArg (← mvarName mvars[i]) - | _ => annotateNamedArg (← mvarName mvars[i]) + else annotateNamedArg (← mvarName mvars[i]!) + | _ => annotateNamedArg (← mvarName mvars[i]!) else annotateBool `pp.analysis.skip; provided := false modify fun s => { s with provideds := s.provideds.set! i provided } | BinderInfo.auxDecl => pure () - if (← get).provideds[i] then withKnowing (not (← typeUnknown mvars[i])) true analyze - tryUnify mvars[i] args[i] + if (← get).provideds[i]! then withKnowing (not (← typeUnknown mvars[i]!)) true analyze + tryUnify mvars[i]! args[i]! maybeSetExplicit := do let { f, args, bInfos, ..} ← read if (← get).namedArgs.any nameNotRoundtrippable then annotateBool `pp.explicit for i in [:args.size] do - if !(← get).provideds[i] then + if !(← get).provideds[i]! then withNaryArg (f.getAppNumArgs + i) do annotateBool `pp.analysis.hole - if bInfos[i] == BinderInfo.instImplicit && getPPInstanceTypes (← getOptions) then + if bInfos[i]! == BinderInfo.instImplicit && getPPInstanceTypes (← getOptions) then withType (withKnowing true false analyze) end diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 2e122cf973..9ad6ca5337 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -124,7 +124,7 @@ section Elab def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do let ctx ← read - let headerSnap := snaps[0] + let headerSnap := snaps[0]! if headerSnap.msgLog.hasErrors then -- Treat header processing errors as fatal so users aren't swamped with -- followup errors diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index da20786541..ecb25bc016 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -296,9 +296,9 @@ private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? evalExpr' DerivingParams ``DerivingParams args else pure {} if args.withRef then - deriveWithRefInstance declNames[0] + deriveWithRefInstance declNames[0]! else - deriveInstance declNames[0] + deriveInstance declNames[0]! @[implementedBy dispatchDeriveInstanceUnsafe] private opaque dispatchDeriveInstance (declNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Bool diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index caf502ae7f..101cfc4583 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -164,7 +164,7 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax if args.size == 0 then n else let i := args.size - 1 - let last := updateTrailing trailing args[i] + let last := updateTrailing trailing args[i]! let args := args.set! i last; Syntax.node info k args | s => s @@ -238,7 +238,7 @@ partial instance : ForIn m TopDown Syntax where let mut b := b' if let Syntax.node _ k args := stx then if firstChoiceOnly && k == choiceKind then - return ← loop args[0] b + return ← loop args[0]! b else for arg in args do match (← loop arg b) with @@ -260,7 +260,7 @@ partial def reprint (stx : Syntax) : Option String := do if kind == choiceKind then -- this visit the first arg twice, but that should hardly be a problem -- given that choice nodes are quite rare and small - let s0 ← reprint args[0] + let s0 ← reprint args[0]! for arg in args[1:] do let s' ← reprint arg guard (s0 == s')