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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-20 15:09:12 -07:00
parent bd58048449
commit 8d9543d9c2
66 changed files with 1173 additions and 1558 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/Init/Control/Option.lean
View file

@ -43,9 +43,9 @@ namespace OptionT
(pure none : m (Option α))
instance : Alternative (OptionT m) :=
{ failure := @OptionT.fail m _,
orelse := @OptionT.orelse m _,
..OptionT.Monad }
{ OptionT.Monad with
failure := @OptionT.fail m _,
orelse := @OptionT.orelse m _ }
@[inline] protected def lift (ma : m α) : OptionT m α :=
(some <$> ma : m (Option α))

7
stage0/src/Init/Control/Reader.lean
View file

@ -60,9 +60,10 @@ fun s => x₁ s <|> x₂ s
fun s => failure
instance [Alternative m] : Alternative (ReaderT ρ m) :=
{ failure := @ReaderT.failure _ _ _ _,
orelse := @ReaderT.orelse _ _ _ _,
..ReaderT.Monad }
{ ReaderT.Monad with
failure := @ReaderT.failure _ _ _ _,
orelse := @ReaderT.orelse _ _ _ _ }
instance (ε) [Monad m] [MonadExcept ε m] : MonadExcept ε (ReaderT ρ m) :=
{ throw := fun α => ReaderT.lift ∘ throw,

6
stage0/src/Init/Control/State.lean
View file

@ -51,9 +51,9 @@ fun s => x₁ s <|> x₂ s
fun s => failure
instance [Alternative m] : Alternative (StateT σ m) :=
{ failure := @StateT.failure _ _ _ _,
orelse := @StateT.orelse _ _ _ _,
.. StateT.Monad }
{ StateT.Monad with
failure := @StateT.failure _ _ _ _,
orelse := @StateT.orelse _ _ _ _ }
@[inline] protected def get : StateT σ m σ :=
fun s => pure (s, s)

4
stage0/src/Init/Data/BinomialHeap/Basic.lean
View file

@ -35,9 +35,9 @@ Heap.heap [{ val := a, rank := 1, children := [] }]
@[specialize] def combine (lt : α → α → Bool) (n₁ n₂ : HeapNode α) : HeapNode α :=
if lt n₂.val n₁.val then
{ rank := n₂.rank + 1, children := n₂.children ++ [Heap.heap [n₁]], .. n₂ }
{ n₂ with rank := n₂.rank + 1, children := n₂.children ++ [Heap.heap [n₁]] }
else
{ rank := n₁.rank + 1, children := n₁.children ++ [Heap.heap [n₂]], .. n₁ }
{ n₁ with rank := n₁.rank + 1, children := n₁.children ++ [Heap.heap [n₂]] }
@[specialize] partial def mergeNodes (lt : α → α → Bool) : List (HeapNode α) → List (HeapNode α) → List (HeapNode α)
| [], h => h

6
stage0/src/Init/Data/List/Instances.lean
View file

@ -15,6 +15,6 @@ instance : Monad List :=
{ pure := @List.pure, map := @List.map, bind := @List.bind }
instance : Alternative List :=
{ failure := @List.nil,
orelse := @List.append,
..List.Monad }
{ List.Monad with
failure := @List.nil,
orelse := @List.append }

6
stage0/src/Init/Data/Option/Basic.lean
View file

@ -66,9 +66,9 @@ instance : Monad Option :=
/- Remark: when using the polymorphic notation `a <|> b` is not a `[macroInline]`.
Thus, `a <|> b` will make `Option.orelse` to behave like it was marked as `[inline]`. -/
instance : Alternative Option :=
{ failure := @none,
orelse := @Option.orelse,
..Option.Monad }
{ Option.Monad with
failure := @none,
orelse := @Option.orelse }
@[inline] protected def lt {α : Type u} (r : α → α → Prop) : Option α → Option α → Prop
| none, some x => True

38
stage0/src/Init/Data/PersistentArray/Basic.lean
View file

@ -81,9 +81,9 @@ partial def setAux : PersistentArrayNode α → USize → USize → α → Persi
def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α :=
if i >= t.tailOff then
{ tail := t.tail.set! (i - t.tailOff) a, .. t }
{ t with tail := t.tail.set! (i - t.tailOff) a }
else
{ root := setAux t.root (USize.ofNat i) t.shift a, .. t }
{ t with root := setAux t.root (USize.ofNat i) t.shift a }
@[specialize] partial def modifyAux [Inhabited α] (f : α → α) : PersistentArrayNode α → USize → USize → PersistentArrayNode α
| node cs, i, shift =>
@ -95,9 +95,9 @@ else
@[specialize] def modify [Inhabited α] (t : PersistentArray α) (i : Nat) (f : α → α) : PersistentArray α :=
if i >= t.tailOff then
{ tail := t.tail.modify (i - t.tailOff) f, .. t }
{ t with tail := t.tail.modify (i - t.tailOff) f }
else
{ root := modifyAux f t.root (USize.ofNat i) t.shift, .. t }
{ t with root := modifyAux f t.root (USize.ofNat i) t.shift }
partial def mkNewPath : USize → Array α → PersistentArrayNode α
| shift, a =>
@ -122,21 +122,21 @@ partial def insertNewLeaf : PersistentArrayNode α → USize → USize → Array
def mkNewTail (t : PersistentArray α) : PersistentArray α :=
if t.size <= (mul2Shift 1 (t.shift + initShift)).toNat then
{ tail := mkEmptyArray, root := insertNewLeaf t.root (USize.ofNat (t.size - 1)) t.shift t.tail,
tailOff := t.size,
.. t }
{ t with
tail := mkEmptyArray, root := insertNewLeaf t.root (USize.ofNat (t.size - 1)) t.shift t.tail,
tailOff := t.size }
else
{ tail := #[],
{ t with
tail := #[],
root := let n := mkEmptyArray.push t.root;
node (n.push (mkNewPath t.shift t.tail)),
shift := t.shift + initShift,
tailOff := t.size,
.. t }
tailOff := t.size }
def tooBig : Nat := usizeSz / 8
def push (t : PersistentArray α) (a : α) : PersistentArray α :=
let r := { tail := t.tail.push a, size := t.size + 1, .. t };
let r := { t with tail := t.tail.push a, size := t.size + 1 };
if r.tail.size < branching.toNat || t.size >= tooBig then
r
else
@ -165,7 +165,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
def pop (t : PersistentArray α) : PersistentArray α :=
if t.tail.size > 0 then
{ tail := t.tail.pop, size := t.size - 1, .. t }
{ t with tail := t.tail.pop, size := t.size - 1 }
else
match popLeaf t.root with
| (none, _) => t
@ -180,11 +180,11 @@ else
tail := last,
tailOff := newTailOff }
else
{ root := node newRoots,
{ t with
root := node newRoots,
size := newSize,
tail := last,
tailOff := newTailOff,
.. t }
tailOff := newTailOff }
section
variables {m : Type v → Type w} [Monad m]
@ -295,7 +295,7 @@ variable {β : Type u}
@[specialize] def mapM (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) := do
root ← mapMAux f t.root;
tail ← t.tail.mapM f;
pure { tail := tail, root := root, .. t }
pure { t with tail := tail, root := root }
end
@ -308,9 +308,9 @@ structure Stats :=
partial def collectStats : PersistentArrayNode α → Stats → Nat → Stats
| node cs, s, d =>
cs.foldl (fun s c => collectStats c s (d+1))
{ numNodes := s.numNodes + 1,
depth := Nat.max d s.depth, .. s }
| leaf vs, s, d => { numNodes := s.numNodes + 1, depth := Nat.max d s.depth, .. s }
{ s with numNodes := s.numNodes + 1,
depth := Nat.max d s.depth }
| leaf vs, s, d => { s with numNodes := s.numNodes + 1, depth := Nat.max d s.depth }
def stats (r : PersistentArray α) : Stats :=
collectStats r.root { numNodes := 0, depth := 0, tailSize := r.tail.size } 0

14
stage0/src/Init/Data/PersistentHashMap/Basic.lean
View file

@ -291,18 +291,18 @@ structure Stats :=
partial def collectStats : Node α β → Stats → Nat → Stats
| Node.collision keys _ _, stats, depth =>
{ numNodes := stats.numNodes + 1,
{ stats with
numNodes := stats.numNodes + 1,
numCollisions := stats.numCollisions + keys.size - 1,
maxDepth := Nat.max stats.maxDepth depth,
.. stats }
maxDepth := Nat.max stats.maxDepth depth }
| Node.entries entries, stats, depth =>
let stats :=
{ numNodes := stats.numNodes + 1,
maxDepth := Nat.max stats.maxDepth depth,
.. stats };
{ stats with
numNodes := stats.numNodes + 1,
maxDepth := Nat.max stats.maxDepth depth };
entries.foldl (fun stats entry =>
match entry with
| Entry.null => { numNull := stats.numNull + 1, .. stats }
| Entry.null => { stats with numNull := stats.numNull + 1 }
| Entry.ref node => collectStats node stats (depth + 1)
| Entry.entry _ _ => stats)
stats

6
stage0/src/Init/Data/Queue/Basic.lean
View file

@ -25,14 +25,14 @@ def isEmpty (q : Queue α) : Bool :=
q.dList.isEmpty && q.eList.isEmpty
def enqueue (v : α) (q : Queue α) : Queue α :=
{ eList := v::q.eList, .. q }
{ q with eList := v::q.eList }
def enqueueAll (vs : List α) (q : Queue α) : Queue α :=
{ eList := vs ++ q.eList, .. q }
{ q with eList := vs ++ q.eList }
def dequeue? (q : Queue α) : Option (α × Queue α) :=
match q.dList with
| d::ds => some (d, { dList := ds, .. q })
| d::ds => some (d, { q with dList := ds })
| [] =>
match q.eList.reverse with
| [] => none

6
stage0/src/Init/Data/Stack/Basic.lean
View file

@ -24,7 +24,7 @@ def isEmpty (s : Stack α) : Bool :=
s.vals.isEmpty
def push (v : α) (s : Stack α) : Stack α :=
{ vals := s.vals.push v, .. s }
{ s with vals := s.vals.push v }
def peek? (s : Stack α) : Option α :=
if s.vals.isEmpty then none else s.vals.get? (s.vals.size-1)
@ -33,9 +33,9 @@ def peek! [Inhabited α] (s : Stack α) : α :=
s.vals.back
def pop [Inhabited α] (s : Stack α) : Stack α :=
{ vals := s.vals.pop, .. s }
{ s with vals := s.vals.pop }
def modify [Inhabited α] (s : Stack α) (f : α → α) : Stack α :=
{ vals := s.vals.modify (s.vals.size-1) f, .. s }
{ s with vals := s.vals.modify (s.vals.size-1) f }
end Stack

2
stage0/src/Init/Lean/Attributes.lean
View file

@ -117,7 +117,7 @@ map ← es.foldlM
pure { map := map }
private def AttributeExtension.addEntry (s : AttributeExtensionState) (e : AttributeExtensionOLeanEntry × AttributeImpl) : AttributeExtensionState :=
{ map := s.map.insert e.2.name e.2, newEntries := e.1 :: s.newEntries, .. s }
{ s with map := s.map.insert e.2.name e.2, newEntries := e.1 :: s.newEntries }
def mkAttributeExtension : IO AttributeExtension :=
registerPersistentEnvExtension {

8
stage0/src/Init/Lean/Class.lean
View file

@ -35,13 +35,13 @@ instance : Inhabited ClassState := ⟨{}⟩
def addEntry (s : ClassState) (entry : ClassEntry) : ClassState :=
match entry with
| ClassEntry.«class» clsName hasOutParam =>
{ hasOutParam := s.hasOutParam.insert clsName hasOutParam, .. s }
{ s with hasOutParam := s.hasOutParam.insert clsName hasOutParam }
| ClassEntry.«instance» instName clsName =>
{ instances := s.instances.insert instName (),
{ s with
instances := s.instances.insert instName (),
classToInstances := match s.classToInstances.find? clsName with
| some insts => s.classToInstances.insert clsName (instName :: insts)
| none => s.classToInstances.insert clsName [instName],
.. s }
| none => s.classToInstances.insert clsName [instName] }
def switch : ClassState → ClassState
| ⟨m₁, m₂, m₃⟩ => ⟨m₁.switch, m₂.switch, m₃.switch⟩

16
stage0/src/Init/Lean/Compiler/IR/Borrow.lean
View file

@ -70,7 +70,7 @@ instance : HasToString ParamMap := ⟨fun m => Format.pretty (format m)⟩
namespace InitParamMap
/- Mark parameters that take a reference as borrow -/
def initBorrow (ps : Array Param) : Array Param :=
ps.map $ fun p => { borrow := p.ty.isObj, .. p }
ps.map $ fun p => { p with borrow := p.ty.isObj }
/- We do perform borrow inference for constants marked as `export`.
Reason: we current write wrappers in C++ for using exported functions.
@ -158,14 +158,14 @@ ctx ← read;
pure ctx.currFn
def markModified : M Unit :=
modify $ fun s => { modified := true, .. s }
modify $ fun s => { s with modified := true }
def ownVar (x : VarId) : M Unit := do
-- dbgTrace ("ownVar " ++ toString x) $ fun _ =>
currFn ← getCurrFn;
modify $ fun s =>
if s.owned.contains (currFn, x.idx) then s
else { owned := s.owned.insert (currFn, x.idx), modified := true, .. s }
else { s with owned := s.owned.insert (currFn, x.idx), modified := true }
def ownArg (x : Arg) : M Unit :=
match x with
@ -189,9 +189,9 @@ match s.paramMap.find? k with
ps ← ps.mapM $ fun (p : Param) =>
if !p.borrow then pure p
else condM (isOwned p.x)
(do markModified; pure { borrow := false, .. p })
(do markModified; pure { p with borrow := false })
(pure p);
modify $ fun s => { paramMap := s.paramMap.insert k ps, .. s }
modify $ fun s => { s with paramMap := s.paramMap.insert k ps }
| none => pure ()
def getParamInfo (k : ParamMap.Key) : M (Array Param) := do
@ -268,7 +268,7 @@ match v, b with
| _, _ => pure ()
def updateParamSet (ctx : BorrowInfCtx) (ps : Array Param) : BorrowInfCtx :=
{ paramSet := ps.foldl (fun s p => s.insert p.x.idx) ctx.paramSet, .. ctx }
{ ctx with paramSet := ps.foldl (fun s p => s.insert p.x.idx) ctx.paramSet }
partial def collectFnBody : FnBody → M Unit
| FnBody.jdecl j ys v b => do
@ -287,14 +287,14 @@ partial def collectFnBody : FnBody → M Unit
partial def collectDecl : Decl → M Unit
| Decl.fdecl f ys _ b =>
adaptReader (fun ctx => let ctx := updateParamSet ctx ys; { currFn := f, .. ctx }) $ do
adaptReader (fun ctx => let ctx := updateParamSet ctx ys; { ctx with currFn := f }) $ do
collectFnBody b;
updateParamMap (ParamMap.Key.decl f)
| _ => pure ()
@[specialize] partial def whileModifingAux (x : M Unit) : Unit → M Unit
| _ => do
modify $ fun s => { modified := false, .. s };
modify $ fun s => { s with modified := false };
-- s ← get;
-- dbgTrace (toString s.map) $ fun _ => do
x;

14
stage0/src/Init/Lean/Compiler/IR/Boxing.lean
View file

@ -128,7 +128,7 @@ structure BoxingState :=
abbrev M := ReaderT BoxingContext (StateT BoxingState Id)
def mkFresh : M VarId := do
oldS ← getModify (fun s => { nextIdx := s.nextIdx + 1, .. s });
oldS ← getModify (fun s => { s with nextIdx := s.nextIdx + 1 });
pure { idx := oldS.nextIdx }
def getEnv : M Environment := BoxingContext.env <$> read
@ -154,13 +154,13 @@ match findEnvDecl' ctx.env fid ctx.decls with
| none => pure (arbitrary _) -- unreachable if well-formed
@[inline] def withParams {α : Type} (xs : Array Param) (k : M α) : M α :=
adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addParams xs, .. ctx }) k
adaptReader (fun (ctx : BoxingContext) => { ctx with localCtx := ctx.localCtx.addParams xs }) k
@[inline] def withVDecl {α : Type} (x : VarId) (ty : IRType) (v : Expr) (k : M α) : M α :=
adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addLocal x ty v, .. ctx }) k
adaptReader (fun (ctx : BoxingContext) => { ctx with localCtx := ctx.localCtx.addLocal x ty v }) k
@[inline] def withJDecl {α : Type} (j : JoinPointId) (xs : Array Param) (v : FnBody) (k : M α) : M α :=
adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addJP j xs v, .. ctx }) k
adaptReader (fun (ctx : BoxingContext) => { ctx with localCtx := ctx.localCtx.addJP j xs v }) k
/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c #[]`,
and `x`'s type is not cheap to box (e.g., it is `UInt64), then return its value. -/
@ -206,10 +206,10 @@ match opt? with
let auxConst := Expr.fap auxName #[];
let auxDecl := Decl.fdecl auxName #[] expectedType body;
modify $ fun s => {
s with
auxDecls := s.auxDecls.push auxDecl,
auxDeclCache := s.auxDeclCache.cons body auxConst,
nextAuxId := s.nextAuxId + 1,
.. s
nextAuxId := s.nextAuxId + 1
};
pure auxConst
| none => pure $ if xType.isScalar then Expr.box xType x else Expr.unbox x
@ -328,7 +328,7 @@ let decls := decls.foldl (fun (newDecls : Array Decl) (decl : Decl) =>
match decl with
| Decl.fdecl f xs t b =>
let nextIdx := decl.maxIndex + 1;
let (b, s) := (withParams xs (visitFnBody b) { f := f, resultType := t, .. ctx }).run { nextIdx := nextIdx };
let (b, s) := (withParams xs (visitFnBody b) { ctx with f := f, resultType := t }).run { nextIdx := nextIdx };
let newDecls := newDecls ++ s.auxDecls;
let newDecl := Decl.fdecl f xs t b;
let newDecl := newDecl.elimDead;

8
stage0/src/Init/Lean/Compiler/IR/Checker.lean
View file

@ -23,7 +23,7 @@ abbrev M := ReaderT CheckerContext (ExceptT String (StateT CheckerState Id))
def markIndex (i : Index) : M Unit := do
s ← get;
when (s.foundVars.contains i) $ throw ("variable / joinpoint index " ++ toString i ++ " has already been used");
modify $ fun s => { foundVars := s.foundVars.insert i, .. s }
modify $ fun s => { s with foundVars := s.foundVars.insert i }
def markVar (x : VarId) : M Unit :=
markIndex x.idx
@ -120,19 +120,19 @@ ctx ← read;
localCtx ← ps.foldlM (fun (ctx : LocalContext) p => do
markVar p.x;
pure $ ctx.addParam p) ctx.localCtx;
adaptReader (fun _ => { localCtx := localCtx, .. ctx }) k
adaptReader (fun _ => { ctx with localCtx := localCtx }) k
partial def checkFnBody : FnBody → M Unit
| FnBody.vdecl x t v b => do
checkExpr t v;
markVar x;
ctx ← read;
adaptReader (fun (ctx : CheckerContext) => { localCtx := ctx.localCtx.addLocal x t v, .. ctx }) (checkFnBody b)
adaptReader (fun (ctx : CheckerContext) => { ctx with localCtx := ctx.localCtx.addLocal x t v }) (checkFnBody b)
| FnBody.jdecl j ys v b => do
markJP j;
withParams ys (checkFnBody v);
ctx ← read;
adaptReader (fun (ctx : CheckerContext) => { localCtx := ctx.localCtx.addJP j ys v, .. ctx }) (checkFnBody b)
adaptReader (fun (ctx : CheckerContext) => { ctx with localCtx := ctx.localCtx.addJP j ys v }) (checkFnBody b)
| FnBody.set x _ y b => checkVar x *> checkArg y *> checkFnBody b
| FnBody.uset x _ y b => checkVar x *> checkVar y *> checkFnBody b
| FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b

4
stage0/src/Init/Lean/Compiler/IR/CompilerM.lean
View file

@ -39,7 +39,7 @@ structure CompilerState :=
abbrev CompilerM := ReaderT Options (EStateM String CompilerState)
def log (entry : LogEntry) : CompilerM Unit :=
modify $ fun s => { log := s.log.push entry, .. s }
modify $ fun s => { s with log := s.log.push entry }
def tracePrefixOptionName := `trace.compiler.ir
@ -66,7 +66,7 @@ logMessageIfAux (tracePrefixOptionName ++ cls) a
logMessageIfAux tracePrefixOptionName a
@[inline] def modifyEnv (f : Environment → Environment) : CompilerM Unit :=
modify $ fun s => { env := f s.env, .. s }
modify $ fun s => { s with env := f s.env }
abbrev DeclMap := SMap Name Decl

14
stage0/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean
View file

@ -144,7 +144,7 @@ match arg with
def updateVarAssignment (x : VarId) (v : Value) : M Unit := do
v' ← findVarValue x;
ctx ← read;
modify $ fun s => { assignments := s.assignments.modify ctx.currFnIdx $ fun a => a.insert x (merge v v'), .. s }
modify $ fun s => { s with assignments := s.assignments.modify ctx.currFnIdx $ fun a => a.insert x (merge v v') }
partial def projValue : Value → Nat → Value
| ctor _ vs, i => vs.getD i bot
@ -174,7 +174,7 @@ partial def containsCtor : Value → CtorInfo → Bool
def updateCurrFnSummary (v : Value) : M Unit := do
ctx ← read;
let currFnIdx := ctx.currFnIdx;
modify $ fun s => { funVals := s.funVals.modify currFnIdx (fun v' => widening ctx.env v v'), .. s }
modify $ fun s => { s with funVals := s.funVals.modify currFnIdx (fun v' => widening ctx.env v v') }
/-- Return true if the assignment of at least one parameter has been updated. -/
def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
@ -189,7 +189,7 @@ ys.size.foldM
let newVal := merge yVal xVal;
if newVal == yVal then pure r
else do
modify $ fun s => { assignments := s.assignments.modify currFnIdx $ fun a => a.insert y.x newVal, .. s };
modify $ fun s => { s with assignments := s.assignments.modify currFnIdx $ fun a => a.insert y.x newVal };
pure true)
false
@ -199,7 +199,7 @@ partial def interpFnBody : FnBody → M Unit
updateVarAssignment x v;
interpFnBody b
| FnBody.jdecl j ys v b =>
adaptReader (fun (ctx : InterpContext) => { lctx := ctx.lctx.addJP j ys v, .. ctx }) $
adaptReader (fun (ctx : InterpContext) => { ctx with lctx := ctx.lctx.addJP j ys v }) $
interpFnBody b
| FnBody.case _ x _ alts => do
v ← findVarValue x;
@ -221,14 +221,14 @@ partial def interpFnBody : FnBody → M Unit
def inferStep : M Bool := do
ctx ← read;
modify $ fun s => { assignments := ctx.decls.map $ fun _ => {}, .. s };
modify $ fun s => { s with assignments := ctx.decls.map $ fun _ => {} };
ctx.decls.size.foldM (fun idx modified => do
match ctx.decls.get! idx with
| Decl.fdecl fid ys _ b => do
s ← get;
-- dbgTrace (">> " ++ toString fid) $ fun _ =>
let currVals := s.funVals.get! idx;
adaptReader (fun (ctx : InterpContext) => { currFnIdx := idx, .. ctx }) $ do
adaptReader (fun (ctx : InterpContext) => { ctx with currFnIdx := idx }) $ do
ys.forM $ fun y => updateVarAssignment y.x top;
interpFnBody b;
s ← get;
@ -282,7 +282,7 @@ modify $ fun s =>
-- dbgTrace (">> " ++ toString (decls.get! i).name ++ " " ++ toString (funVals.get! i)) $ fun _ =>
addFunctionSummary env (decls.get! i).name (funVals.get! i))
s.env;
{ env := env, .. s };
{ s with env := env };
pure $ decls.mapIdx $ fun i decl => elimDead (assignments.get! i) decl
end IR

4
stage0/src/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -624,7 +624,7 @@ emitLn "}"
def emitDeclAux (d : Decl) : M Unit := do
env ← getEnv;
let (vMap, jpMap) := mkVarJPMaps d;
adaptReader (fun (ctx : Context) => { jpMap := jpMap, .. ctx }) $ do
adaptReader (fun (ctx : Context) => { ctx with jpMap := jpMap }) $ do
unless (hasInitAttr env d.name) $
match d with
| Decl.fdecl f xs t b => do
@ -652,7 +652,7 @@ unless (hasInitAttr env d.name) $
emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
};
emitLn "_start:";
adaptReader (fun (ctx : Context) => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b);
adaptReader (fun (ctx : Context) => { ctx with mainFn := f, mainParams := xs }) (emitFnBody b);
emitLn "}"
| _ => pure ()

2
stage0/src/Init/Lean/Compiler/IR/NormIds.lean
View file

@ -91,7 +91,7 @@ fun m => do
@[inline] def withParams {α : Type} (ps : Array Param) (k : Array Param → N α) : N α :=
fun m => do
m ← ps.foldlM (fun (m : IndexRenaming) p => do n ← getModify (fun n => n + 1); pure $ m.insert p.x.idx n) m;
let ps := ps.map $ fun p => { x := normVar p.x m, .. p };
let ps := ps.map $ fun p => { p with x := normVar p.x m };
k ps m
instance MtoN {α} : HasCoe (M α) (N α) :=

18
stage0/src/Init/Lean/Compiler/IR/RC.lean
View file

@ -65,10 +65,10 @@ FnBody.dec x 1 true info.persistent b
private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : Context :=
if c.isRef then ctx
else let m := ctx.varMap;
{ varMap := match m.find? x with
| some info => m.insert x { ref := false, .. info } -- I really want a Lenses library + notation
| none => m,
.. ctx }
{ ctx with
varMap := match m.find? x with
| some info => m.insert x { info with ref := false } -- I really want a Lenses library + notation
| none => m }
private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody :=
caseLiveVars.fold
@ -181,11 +181,11 @@ match v with
| _ => false
private def updateVarInfo (ctx : Context) (x : VarId) (t : IRType) (v : Expr) : Context :=
{ varMap := ctx.varMap.insert x {
{ ctx with
varMap := ctx.varMap.insert x {
ref := t.isObj && !isScalarBoxedInTaggedPtr v,
persistent := isPersistent v,
consume := consumeExpr ctx.varMap v },
.. ctx }
consume := consumeExpr ctx.varMap v } }
private def addDecIfNeeded (ctx : Context) (x : VarId) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
if mustConsume ctx x && !bLiveVars.contains x then addDec ctx x b else b
@ -219,7 +219,7 @@ let liveVars := liveVars.erase z;
def updateVarInfoWithParams (ctx : Context) (ps : Array Param) : Context :=
let m := ps.foldl (fun (m : VarMap) p => m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }) ctx.varMap;
{ varMap := m, .. ctx }
{ ctx with varMap := m }
partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
| FnBody.vdecl x t v b, ctx =>
@ -229,7 +229,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
| FnBody.jdecl j xs v b, ctx =>
let (v, vLiveVars) := visitFnBody v (updateVarInfoWithParams ctx xs);
let v := addDecForDeadParams ctx xs v vLiveVars;
let ctx := { jpLiveVarMap := updateJPLiveVarMap j xs v ctx.jpLiveVarMap, .. ctx };
let ctx := { ctx with jpLiveVarMap := updateJPLiveVarMap j xs v ctx.jpLiveVarMap };
let (b, bLiveVars) := visitFnBody b ctx;
(FnBody.jdecl j xs v b, bLiveVars)
| FnBody.uset x i y b, ctx =>

4
stage0/src/Init/Lean/Compiler/Specialize.lean
View file

@ -82,8 +82,8 @@ instance : Inhabited SpecState := ⟨{}⟩
def addEntry (s : SpecState) (e : SpecEntry) : SpecState :=
match e with
| SpecEntry.info name info => { specInfo := s.specInfo.insert name info, .. s }
| SpecEntry.cache key fn => { cache := s.cache.insert key fn, .. s }
| SpecEntry.info name info => { s with specInfo := s.specInfo.insert name info }
| SpecEntry.cache key fn => { s with cache := s.cache.insert key fn }
def switch : SpecState → SpecState
| ⟨m₁, m₂⟩ => ⟨m₁.switch, m₂.switch⟩

2
stage0/src/Init/Lean/Data/SMap.lean
View file

@ -67,7 +67,7 @@ match m.find? a with
/- Move from stage 1 into stage 2. -/
def switch (m : SMap α β) : SMap α β :=
if m.stage₁ then { stage₁ := false, .. m } else m
if m.stage₁ then { m with stage₁ := false } else m
@[inline] def foldStage2 {σ : Type w} (f : σ → α → β → σ) (s : σ) (m : SMap α β) : σ :=
m.map₂.foldl f s

12
stage0/src/Init/Lean/Elab/App.lean
View file

@ -216,14 +216,14 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
let namedArgs := ctx.namedArgs.eraseIdx idx;
argElab ← elabArg ctx.ref e arg.val d;
propagateExpectedType ctx eType;
elabAppArgsAux { foundExplicit := true, namedArgs := namedArgs, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
elabAppArgsAux { ctx with foundExplicit := true, namedArgs := namedArgs } (mkApp e argElab) (b.instantiate1 argElab)
| none =>
let processExplictArg : Unit → TermElabM Expr := fun _ => do {
propagateExpectedType ctx eType;
let ctx := { foundExplicit := true, .. ctx };
let ctx := { ctx with foundExplicit := true };
if h : ctx.argIdx < ctx.args.size then do
argElab ← elabArg ctx.ref e (ctx.args.get ⟨ctx.argIdx, h⟩) d;
elabAppArgsAux { argIdx := ctx.argIdx + 1, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
elabAppArgsAux { ctx with argIdx := ctx.argIdx + 1 } (mkApp e argElab) (b.instantiate1 argElab)
else match ctx.explicit, d.getOptParamDefault?, d.getAutoParamTactic? with
| false, some defVal, _ => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
| false, _, some (Expr.const tacticDecl _ _) => do
@ -255,19 +255,19 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
else do
a ← mkFreshExprMVar ctx.ref d;
typeMVars ← condM (isTypeFormer ctx.ref a) (pure $ ctx.typeMVars.push a.mvarId!) (pure ctx.typeMVars);
elabAppArgsAux { typeMVars := typeMVars, .. ctx } (mkApp e a) (b.instantiate1 a)
elabAppArgsAux { ctx with typeMVars := typeMVars } (mkApp e a) (b.instantiate1 a)
| BinderInfo.instImplicit =>
if ctx.explicit && nextArgIsHole ctx then do
/- Recall that if '@' has been used, and the argument is '_', then we still use
type class resolution -/
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
elabAppArgsAux { argIdx := ctx.argIdx + 1, instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
elabAppArgsAux { ctx with argIdx := ctx.argIdx + 1, instMVars := ctx.instMVars.push a.mvarId! } (mkApp e a) (b.instantiate1 a)
else if ctx.explicit then
processExplictArg ()
else do
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
elabAppArgsAux { instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
elabAppArgsAux { ctx with instMVars := ctx.instMVars.push a.mvarId! } (mkApp e a) (b.instantiate1 a)
| _ =>
processExplictArg ()
| _ =>

10
stage0/src/Init/Lean/Elab/Binders.lean
View file

@ -308,8 +308,8 @@ match s.expectedType? with
_ ← isDefEq ref fvarType d;
checkNoOptAutoParam ref fvarType;
let b := b.instantiate1 fvar;
pure { expectedType? := some b, .. s }
| _ => pure { expectedType? := none, .. s }
pure { s with expectedType? := some b }
| _ => pure { s with expectedType? := none }
private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat → State → TermElabM State
| i, s =>
@ -320,7 +320,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
checkNoOptAutoParam binderView.type type;
fvarId ← mkFreshFVarId;
let fvar := mkFVar fvarId;
let s := { fvars := s.fvars.push fvar, .. s };
let s := { s with fvars := s.fvars.push fvar };
-- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
/-
We do **not** want to support default and auto arguments in lambda abstractions.
@ -329,14 +329,14 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
-/
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
s ← propagateExpectedType binderView.id fvar type s;
let s := { lctx := lctx, .. s };
let s := { s with lctx := lctx };
className? ← isClass binderView.type type;
match className? with
| none => elabFunBinderViews (i+1) s
| some className => do
resetSynthInstanceCache;
let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
elabFunBinderViews (i+1) { localInsts := localInsts, .. s }
elabFunBinderViews (i+1) { s with localInsts := localInsts }
else
pure s

59
stage0/src/Init/Lean/Elab/Command.lean
View file

@ -93,7 +93,7 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
getFileMap := do ctx ← read; pure ctx.fileMap,
getFileName := do ctx ← read; pure ctx.fileName,
addContext := addContext,
logMessage := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
logMessage := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
/--
Throws an error with the given `msgData` and extracting position information from `ref`.
@ -136,7 +136,7 @@ mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinComm
@[inline] def withIncRecDepth {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
ctx ← read; s ← get;
when (ctx.currRecDepth == s.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
| [] => do
@ -149,13 +149,13 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → C
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
instance : MonadMacroAdapter CommandElabM :=
{ getEnv := getEnv,
getCurrMacroScope := getCurrMacroScope,
getNextMacroScope := do s ← get; pure s.nextMacroScope,
setNextMacroScope := fun next => modify $ fun s => { nextMacroScope := next, .. s },
setNextMacroScope := fun next => modify $ fun s => { s with nextMacroScope := next },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax}
@ -211,7 +211,7 @@ private def mkTermState (s : State) : Term.State :=
nextMacroScope := s.nextMacroScope }
private def updateState (s : State) (newS : Term.State) : State :=
{ env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
{ s with env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope }
private def getVarDecls (s : State) : Array Syntax :=
s.scopes.head!.varDecls
@ -229,8 +229,8 @@ instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
ctx ← read;
s ← get;
match (x $ mkTermContext ctx s declName?).run (mkTermState s) with
| EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
| EStateM.Result.error (Term.Exception.ex ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
| EStateM.Result.ok a newS => do modify $ fun s => { s with env := newS.env, messages := newS.messages }; pure a
| EStateM.Result.error (Term.Exception.ex ex) newS => do modify $ fun s => { s with env := newS.env, messages := newS.messages }; throw ex
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
@[inline] def runTermElabM {α} (declName? : Option Name) (elab : Array Expr → TermElabM α) : CommandElabM α := do
@ -248,16 +248,17 @@ def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
_root_.dbgTrace (toString a) $ fun _ => pure ()
def setEnv (newEnv : Environment) : CommandElabM Unit :=
modify $ fun s => { env := newEnv, .. s }
modify $ fun s => { s with env := newEnv }
def getCurrNamespace : CommandElabM Name := do
scope ← getScope; pure scope.currNamespace
private def addScope (kind : String) (header : String) (newNamespace : Name) : CommandElabM Unit :=
modify $ fun s => {
s with
env := s.env.registerNamespace newNamespace,
scopes := { kind := kind, header := header, currNamespace := newNamespace, .. s.scopes.head! } :: s.scopes,
.. s }
scopes := { s.scopes.head! with kind := kind, header := header, currNamespace := newNamespace } :: s.scopes
}
private def addScopes (ref : Syntax) (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
| Name.anonymous => pure ()
@ -301,10 +302,10 @@ fun stx => do
| some n => n.getNumParts;
scopes ← getScopes;
if endSize < scopes.length then
modify $ fun s => { scopes := s.scopes.drop endSize, .. s }
modify $ fun s => { s with scopes := s.scopes.drop endSize }
else do {
-- we keep "root" scope
modify $ fun s => { scopes := s.scopes.drop (s.scopes.length - 1), .. s };
modify $ fun s => { s with scopes := s.scopes.drop (s.scopes.length - 1) };
throwError stx "invalid 'end', insufficient scopes"
};
match header? with
@ -314,15 +315,15 @@ fun stx => do
@[inline] def withNamespace {α} (ref : Syntax) (ns : Name) (elab : CommandElabM α) : CommandElabM α := do
addNamespace ref ns;
a ← elab;
modify $ fun s => { scopes := s.scopes.drop ns.getNumParts, .. s };
modify $ fun s => { s with scopes := s.scopes.drop ns.getNumParts };
pure a
@[specialize] def modifyScope (f : Scope → Scope) : CommandElabM Unit :=
modify $ fun s =>
{ scopes := match s.scopes with
{ s with
scopes := match s.scopes with
| h::t => f h :: t
| [] => unreachable!,
.. s }
| [] => unreachable! }
def getLevelNames : CommandElabM (List Name) := do
scope ← getScope; pure scope.levelNames
@ -336,7 +337,7 @@ levelNames ← getLevelNames;
if levelNames.elem id then
throwAlreadyDeclaredUniverseLevel idStx id
else
modifyScope $ fun scope => { levelNames := id :: scope.levelNames, .. scope }
modifyScope $ fun scope => { scope with levelNames := id :: scope.levelNames }
partial def elabChoiceAux (cmds : Array Syntax) : Nat → CommandElabM Unit
| i =>
@ -405,10 +406,10 @@ fun stx => do
pure aliases
})
[];
modify $ fun s => { env := aliases.foldl (fun env p => addAlias env p.1 p.2) s.env, .. s }
modify $ fun s => { s with env := aliases.foldl (fun env p => addAlias env p.1 p.2) s.env }
def addOpenDecl (d : OpenDecl) : CommandElabM Unit :=
modifyScope $ fun scope => { openDecls := d :: scope.openDecls, .. scope }
modifyScope $ fun scope => { scope with openDecls := d :: scope.openDecls }
def elabOpenSimple (n : SyntaxNode) : CommandElabM Unit :=
-- `open` id+
@ -482,7 +483,7 @@ fun n => do
let binder := n.getArg 1;
-- Try to elaborate `binder` for sanity checking
runTermElabM none $ fun _ => Term.elabBinder binder $ fun _ => pure ();
modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope }
modifyScope $ fun scope => { scope with varDecls := scope.varDecls.push binder }
@[builtinCommandElab «variables»] def elabVariables : CommandElab :=
fun n => do
@ -490,7 +491,7 @@ fun n => do
let binders := (n.getArg 1).getArgs;
-- Try to elaborate `binders` for sanity checking
runTermElabM none $ fun _ => Term.elabBinders binders $ fun _ => pure ();
modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope }
modifyScope $ fun scope => { scope with varDecls := scope.varDecls ++ binders }
@[inline] def withoutModifyingEnv {α} (x : CommandElabM α) : CommandElabM α := do
env ← getEnv;
@ -513,18 +514,18 @@ def failIfSucceeds (ref : Syntax) (x : CommandElabM Unit) : CommandElabM Unit :=
let resetMessages : CommandElabM MessageLog := do {
s ← get;
let messages := s.messages;
modify $ fun s => { messages := {}, .. s };
modify $ fun s => { s with messages := {} };
pure messages
};
let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do {
modify $ fun s => { messages := prevMessages ++ s.messages.errorsToWarnings, .. s }
modify $ fun s => { s with messages := prevMessages ++ s.messages.errorsToWarnings }
};
prevMessages ← resetMessages;
succeeded ← finally
(catch
(do x; hasNoErrorMessages)
(fun ex => match ex with
| Exception.error msg => do modify (fun s => { messages := s.messages.add msg, .. s }); pure false
| Exception.error msg => do modify (fun s => { s with messages := s.messages.add msg }); pure false
| Exception.unsupportedSyntax => do logError ref "unsupported syntax"; pure false))
(restoreMessages prevMessages);
when succeeded $
@ -548,9 +549,9 @@ fun stx => do
def setOption (ref : Syntax) (optionName : Name) (val : DataValue) : CommandElabM Unit := do
decl ← liftIO ref $ getOptionDecl optionName;
unless (decl.defValue.sameCtor val) $ throwError ref "type mismatch at set_option";
modifyScope $ fun scope => { opts := scope.opts.insert optionName val, .. scope };
modifyScope $ fun scope => { scope with opts := scope.opts.insert optionName val };
match optionName, val with
| `maxRecDepth, DataValue.ofNat max => modify $ fun s => { maxRecDepth := max, .. s}
| `maxRecDepth, DataValue.ofNat max => modify $ fun s => { s with maxRecDepth := max }
| _, _ => pure ()
@[builtinCommandElab «set_option»] def elabSetOption : CommandElab :=
@ -609,10 +610,10 @@ match scpView.name with
| Name.str pre s _ =>
/- Add back macro scopes. We assume a declaration like `def a.b[1,2] ...` with macro scopes `[1,2]`
is always meant to mean `namespace a def b[1,2] ...`. -/
let id := { name := mkNameSimple s, .. scpView }.review;
let id := { scpView with name := mkNameSimple s }.review;
withNamespace ref pre $ do
modifyScope $ fun scope => { levelNames := levelNames, .. scope };
finally (f id) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
modifyScope $ fun scope => { scope with levelNames := levelNames };
finally (f id) (modifyScope $ fun scope => { scope with levelNames := savedLevelNames })
| _ => throwError ref "invalid declaration name"
/--

2
stage0/src/Init/Lean/Elab/DeclModifiers.lean
View file

@ -34,7 +34,7 @@ structure Modifiers :=
(attrs : Array Attribute := #[])
def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
{ attrs := modifiers.attrs.push attr, .. modifiers }
{ modifiers with attrs := modifiers.attrs.push attr }
instance Modifiers.hasFormat : HasFormat Modifiers :=
⟨fun m =>

2
stage0/src/Init/Lean/Elab/Frontend.lean
View file

@ -46,7 +46,7 @@ def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit :=
fun ctx => liftIOCore! $ ctx.parserStateRef.set ps
def setMessages (msgs : MessageLog) : FrontendM Unit :=
fun ctx => liftIOCore! $ ctx.commandStateRef.modify $ fun s => { messages := msgs, .. s }
fun ctx => liftIOCore! $ ctx.commandStateRef.modify $ fun s => { s with messages := msgs }
def getInputContext : FrontendM Parser.InputContext := do
ctx ← read; pure ctx.inputCtx

4
stage0/src/Init/Lean/Elab/Level.lean
View file

@ -33,12 +33,12 @@ instance LevelElabM.MonadLog : MonadPosInfo LevelElabM :=
def mkFreshId : LevelElabM Name := do
s ← get;
let id := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
modify $ fun s => { s with ngen := s.ngen.next };
pure id
def mkFreshLevelMVar : LevelElabM Level := do
mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s};
modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
pure $ mkLevelMVar mvarId
partial def elabLevel : Syntax → LevelElabM Level

6
stage0/src/Init/Lean/Elab/Quotation.lean
View file

@ -351,7 +351,7 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
let lctx := lctx.mkLocalDecl n n ty;
let params := params.eraseIdx 0;
stx ← `(fun $params* => $body);
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $ do
e ← toPreterm stx;
pure $ lctx.mkLambda #[mkFVar n] e
| `Lean.Parser.Term.let => do
@ -362,7 +362,7 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
val ← toPreterm val;
lctx ← getLCtx;
let lctx := lctx.mkLetDecl n n exprPlaceholder val;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $ do
e ← toPreterm $ body;
pure $ lctx.mkLambda #[mkFVar n] e
| `Lean.Parser.Term.app => do
@ -397,7 +397,7 @@ def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Excep
let c := Parser.mkParserContext env (Parser.mkInputContext input "<foo>");
let s := Parser.mkParserState c.input;
let s := s.setPos pos;
let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn { rbp := Parser.appPrec, .. c } s;
let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn { c with rbp := Parser.appPrec } s;
let stx := s.stxStack.back;
match s.errorMsg with
| some errorMsg =>

2
stage0/src/Init/Lean/Elab/ResolveName.lean
View file

@ -81,7 +81,7 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li
(scpView : MacroScopesView) : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { name := id, .. scpView }.review;
let id := { scpView with name := id }.review;
match resolveUsingNamespace env id ns with
| resolvedIds@(_ :: _) => resolvedIds.eraseDups.map $ fun id => (id, projs)
| [] =>

30
stage0/src/Init/Lean/Elab/StructInst.lean
View file

@ -34,7 +34,7 @@ args ← args.mapM $ fun arg =>
else
let optSource := arg.getArg 1;
if optSource.isNone then do
modify $ fun s => { found := true, .. s };
modify $ fun s => { s with found := true };
pure arg
else do
let source := optSource.getArg 0;
@ -42,11 +42,11 @@ args ← args.mapM $ fun arg =>
match fvar? with
| some _ => do
-- it is already a local variable
modify $ fun s => { found := true, .. s };
modify $ fun s => { s with found := true };
pure arg
| none => do
src ← `(src);
modify $ fun s => { found := true, source? := source, .. s };
modify $ fun s => { s with found := true, source? := source };
let optSource := optSource.setArg 0 src;
let arg := arg.setArg 1 optSource;
pure arg
@ -335,7 +335,7 @@ s.modifyFields $ fun fields => fields.map $ fun field => match field with
| { lhs := FieldLHS.fieldName ref (Name.str Name.anonymous _ _) :: rest, .. } => field
| { lhs := FieldLHS.fieldName ref n@(Name.str _ _ _) :: rest, .. } =>
let newEntries := n.components.map $ FieldLHS.fieldName ref;
{ lhs := newEntries ++ rest, .. field }
{ field with lhs := newEntries ++ rest }
| _ => field
private def expandNumLitFields (s : Struct) : TermElabM Struct :=
@ -346,7 +346,7 @@ s.modifyFieldsM $ fun fields => do
| { lhs := FieldLHS.fieldIndex ref idx :: rest, .. } =>
if idx == 0 then throwError ref "invalid field index, index must be greater than 0"
else if idx > fieldNames.size then throwError ref ("invalid field index, structure has only #" ++ toString fieldNames.size ++ " fields")
else pure { lhs := FieldLHS.fieldName ref (fieldNames.get! $ idx - 1) :: rest, .. field }
else pure { field with lhs := FieldLHS.fieldName ref (fieldNames.get! $ idx - 1) :: rest }
| _ => pure field
/- For example, consider the following structures:
@ -377,7 +377,7 @@ s.modifyFieldsM $ fun fields => fields.mapM $ fun field => match field with
let path := path.map $ fun funName => match funName with
| Name.str _ s _ => FieldLHS.fieldName ref (mkNameSimple s)
| _ => unreachable!;
pure { lhs := path ++ field.lhs, .. field }
pure { field with lhs := path ++ field.lhs }
| _ => throwError ref ("failed to access field '" ++ fieldName ++ "' in parent structure")
| _ => pure field
@ -427,14 +427,14 @@ s.modifyFieldsM $ fun fields => do
match isSimpleField? fields with
| some field => pure field
| none => do
let substructFields := fields.map $ fun field => { lhs := field.lhs.tail!, .. field };
let substructFields := fields.map $ fun field => { field with lhs := field.lhs.tail! };
substructSource ← mkSubstructSource s.ref s.structName fieldNames fieldName s.source;
let field := fields.head!;
match Lean.isSubobjectField? env s.structName fieldName with
| some substructName => do
let substruct := Struct.mk s.ref substructName substructFields substructSource;
substruct ← expandStruct substruct;
pure { lhs := [field.lhs.head!], val := FieldVal.nested substruct, .. field }
pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
| none => do
-- It is not a substructure field. Thus, we wrap fields using `Syntax`, and use `elabTerm` to process them.
let valStx := s.ref; -- construct substructure syntax using s.ref as template
@ -442,7 +442,7 @@ s.modifyFieldsM $ fun fields => do
let args := substructFields.toArray.map $ Field.toSyntax;
let args := substructSource.addSyntax args;
let valStx := valStx.setArg 2 (mkSepStx args (mkAtomFrom s.ref ","));
pure { lhs := [field.lhs.head!], val := FieldVal.term valStx, .. field }
pure { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
fields.find? $ fun field =>
@ -558,12 +558,12 @@ private partial def elabStruct : Struct → Option Expr → TermElabM (Expr × S
let continue (val : Expr) (field : Field Struct) : TermElabM (Expr × Expr × Fields) := do {
let e := mkApp e val;
let type := b.instantiate1 val;
let field := { expr? := some val, .. field };
let field := { field with expr? := some val };
pure (e, type, field::fields)
};
match field.val with
| FieldVal.term stx => do val ← elabTerm stx (some d); val ← ensureHasType stx d val; continue val field
| FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); val ← ensureHasType s.ref d val; continue val { val := FieldVal.nested sNew, .. field }
| FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); val ← ensureHasType s.ref d val; continue val { field with val := FieldVal.nested sNew }
| FieldVal.default => do val ← mkFreshExprMVar field.ref (some d); continue (markDefaultMissing val) field
| _ => throwFailedToElabField field.ref fieldName s.structName ("unexpected constructor type" ++ indentExpr type)
| _ => throwError field.ref "unexpected unexpanded structure field")
@ -766,7 +766,7 @@ def tryToSynthesizeDefault (ref : Syntax) (structs : Array Struct) (allStructNam
tryToSynthesizeDefaultAux ref structs allStructNames maxDistance fieldName mvarId 0 0
partial def step : Struct → M Unit
| struct => unlessM isRoundDone $ adaptReader (fun (ctx : Context) => { structs := ctx.structs.push struct, .. ctx }) $ do
| struct => unlessM isRoundDone $ adaptReader (fun (ctx : Context) => { ctx with structs := ctx.structs.push struct }) $ do
struct.fields.forM $ fun field =>
match field.val with
| FieldVal.nested struct => step struct
@ -777,7 +777,7 @@ partial def step : Struct → M Unit
unlessM (liftM $ isExprMVarAssigned mvarId) $ do
ctx ← read;
whenM (liftM $ tryToSynthesizeDefault field.ref ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) $ do
modify $ fun s => { progress := true, .. s }
modify $ fun s => { s with progress := true }
| _ => pure ()
partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
@ -788,8 +788,8 @@ partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
| some field =>
if d > hierarchyDepth then
liftM $ throwError field.ref ("field '" ++ getFieldName field ++ "' is missing")
else adaptReader (fun (ctx : Context) => { maxDistance := d, .. ctx }) $ do
modify $ fun (s : State) => { progress := false, .. s};
else adaptReader (fun (ctx : Context) => { ctx with maxDistance := d }) $ do
modify $ fun (s : State) => { s with progress := false };
step struct;
s ← get;
if s.progress then do

4
stage0/src/Init/Lean/Elab/Syntax.lean
View file

@ -44,10 +44,10 @@ abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateT Bool TermElabM)
private def markAsTrailingParser : ToParserDescrM Unit := set true
@[inline] private def withNotFirst {α} (x : ToParserDescrM α) : ToParserDescrM α :=
adaptReader (fun (ctx : ToParserDescrContext) => { first := false, .. ctx }) x
adaptReader (fun (ctx : ToParserDescrContext) => { ctx with first := false }) x
@[inline] private def withoutLeftRec {α} (x : ToParserDescrM α) : ToParserDescrM α :=
adaptReader (fun (ctx : ToParserDescrContext) => { leftRec := false, .. ctx }) x
adaptReader (fun (ctx : ToParserDescrContext) => { ctx with leftRec := false }) x
def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
ctx ← read;

22
stage0/src/Init/Lean/Elab/SyntheticMVars.lean
View file

@ -16,16 +16,16 @@ open Tactic (TacticM evalTactic getUnsolvedGoals)
def liftTacticElabM {α} (ref : Syntax) (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
withMVarContext mvarId $ fun ctx s =>
let savedSyntheticMVars := s.syntheticMVars;
match x { ref := ref, main := mvarId, .. ctx } { goals := [mvarId], syntheticMVars := [], .. s } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) { syntheticMVars := savedSyntheticMVars, .. newS.toTermState }
| EStateM.Result.ok a newS => EStateM.Result.ok a { syntheticMVars := savedSyntheticMVars, .. newS.toTermState }
match x { ctx with ref := ref, main := mvarId } { s with goals := [mvarId], syntheticMVars := [] } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) { newS.toTermState with syntheticMVars := savedSyntheticMVars }
| EStateM.Result.ok a newS => EStateM.Result.ok a { newS.toTermState with syntheticMVars := savedSyntheticMVars }
def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
val ← instantiateMVars ref (mkMVar mvarId);
when val.hasExprMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val)
def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };
modify $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
remainingGoals ← liftTacticElabM ref mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
let tailRef := ref.getTailWithPos.getD ref;
unless remainingGoals.isEmpty (reportUnsolvedGoals tailRef remainingGoals);
@ -34,7 +34,7 @@ ensureAssignmentHasNoMVars tailRef mvarId
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
-- Remark: if `ctx.errToSorry` is already false, then we don't enable it. Recall tactics disable `errToSorry`
adaptReader (fun (ctx : Context) => { errToSorry := ctx.errToSorry && errToSorry, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with errToSorry := ctx.errToSorry && errToSorry }) $
elabTerm stx expectedType? false
/--
@ -45,7 +45,7 @@ private def resumePostponed (macroStack : MacroStack) (stx : Syntax) (mvarId : M
withMVarContext mvarId $ do
s ← get;
catch
(adaptReader (fun (ctx : Context) => { macroStack := macroStack, .. ctx }) $ do
(adaptReader (fun (ctx : Context) => { ctx with macroStack := macroStack }) $ do
mvarDecl ← getMVarDecl mvarId;
expectedType ← instantiateMVars stx mvarDecl.type;
result ← resumeElabTerm stx expectedType (!postponeOnError);
@ -115,7 +115,7 @@ s ← get;
let syntheticMVars := s.syntheticMVars;
let numSyntheticMVars := syntheticMVars.length;
-- We reset `syntheticMVars` because new synthetic metavariables may be created by `synthesizeSyntheticMVar`.
modify $ fun s => { syntheticMVars := [], .. s };
modify $ fun s => { s with syntheticMVars := [] };
-- Recall that `syntheticMVars` is a list where head is the most recent pending synthetic metavariable.
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
@ -126,7 +126,7 @@ remainingSyntheticMVars ← syntheticMVars.filterRevM $ fun mvarDecl => do {
pure $ !succeeded
};
-- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized
modify $ fun s => { syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars, .. s };
modify $ fun s => { s with syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars };
pure $ numSyntheticMVars != remainingSyntheticMVars.length
/-- Apply default value to any pending synthetic metavariable of kind `SyntheticMVarKind.withDefault` -/
@ -142,7 +142,7 @@ newSyntheticMVars ← s.syntheticMVars.filterM $ fun mvarDecl =>
throwError mvarDecl.ref "failed to assign default value to metavariable"; -- TODO: better error message
pure false
| _ => pure true;
modify $ fun s => { syntheticMVars := newSyntheticMVars, .. s };
modify $ fun s => { s with syntheticMVars := newSyntheticMVars };
pure $ newSyntheticMVars.length != len
/-- Report an error for each synthetic metavariable that could not be resolved. -/
@ -215,13 +215,13 @@ synthesizeSyntheticMVarsAux mayPostpone ()
def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
s ← get;
let syntheticMVars := s.syntheticMVars;
modify $ fun s => { syntheticMVars := [], .. s };
modify $ fun s => { s with syntheticMVars := [] };
finally
(do
v ← elabTerm stx expectedType?;
synthesizeSyntheticMVars false;
instantiateMVars stx v)
(modify $ fun s => { syntheticMVars := s.syntheticMVars ++ syntheticMVars, .. s })
(modify $ fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVars })
end Term
end Elab

26
stage0/src/Init/Lean/Elab/Tactic/Basic.lean
View file

@ -46,10 +46,10 @@ abbrev TacticM := ReaderT Context (EStateM Exception State)
abbrev Tactic := Syntax → TacticM Unit
protected def save (s : State) : BacktrackableState :=
{ .. s }
{ env := s.env, mctx := s.mctx, goals := s.goals }
protected def restore (s : State) (bs : BacktrackableState) : State :=
{ env := bs.env, mctx := bs.mctx, goals := bs.goals, .. s }
{ s with env := bs.env, mctx := bs.mctx, goals := bs.goals }
instance : EStateM.Backtrackable BacktrackableState State :=
{ save := Tactic.save,
@ -57,15 +57,15 @@ instance : EStateM.Backtrackable BacktrackableState State :=
def liftTermElabM {α} (x : TermElabM α) : TacticM α :=
fun ctx s => match x ctx.toTermCtx s.toTermState with
| EStateM.Result.ok a newS => EStateM.Result.ok a { toTermState := newS, .. s }
| EStateM.Result.error (Term.Exception.ex ex) newS => EStateM.Result.error ex { toTermState := newS, .. s }
| EStateM.Result.ok a newS => EStateM.Result.ok a { s with toTermState := newS }
| EStateM.Result.error (Term.Exception.ex ex) newS => EStateM.Result.error ex { s with toTermState := newS }
| EStateM.Result.error Term.Exception.postpone _ => unreachable!
def liftMetaM {α} (ref : Syntax) (x : MetaM α) : TacticM α := liftTermElabM $ Term.liftMetaM ref x
def getEnv : TacticM Environment := do s ← get; pure s.env
def getMCtx : TacticM MetavarContext := do s ← get; pure s.mctx
@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modify $ fun s => { mctx := f s.mctx, .. s }
@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modify $ fun s => { s with mctx := f s.mctx }
def getLCtx : TacticM LocalContext := do ctx ← read; pure ctx.lctx
def getLocalInsts : TacticM LocalInstances := do ctx ← read; pure ctx.localInstances
def getOptions : TacticM Options := do ctx ← read; pure ctx.config.opts
@ -93,7 +93,7 @@ instance monadLog : MonadLog TacticM :=
getFileMap := do ctx ← read; pure ctx.fileMap,
getFileName := do ctx ← read; pure ctx.fileName,
addContext := addContext,
logMessage := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
logMessage := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
def throwError {α} (ref : Syntax) (msgData : MessageData) : TacticM α := do
ref ← if ref.getPos.isNone then do ctx ← read; pure ctx.ref else pure ref;
@ -104,7 +104,7 @@ def throwUnsupportedSyntax {α} : TacticM α := liftTermElabM $ Term.throwUnsupp
@[inline] def withIncRecDepth {α} (ref : Syntax) (x : TacticM α) : TacticM α := do
ctx ← read;
when (ctx.currRecDepth == ctx.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
protected def getCurrMacroScope : TacticM MacroScope := do ctx ← read; pure ctx.currMacroScope
protected def getMainModule : TacticM Name := do env ← getEnv; pure env.mainModule
@ -142,13 +142,13 @@ private def evalTacticUsing (s : State) (stx : Syntax) : List Tactic → TacticM
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α :=
adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
instance : MonadMacroAdapter TacticM :=
{ getEnv := getEnv,
getCurrMacroScope := getCurrMacroScope,
getNextMacroScope := do s ← get; pure s.nextMacroScope,
setNextMacroScope := fun next => modify $ fun s => { nextMacroScope := next, .. s },
setNextMacroScope := fun next => modify $ fun s => { s with nextMacroScope := next },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax }
@ -193,7 +193,7 @@ fun stx => do
withMacroExpansion stx stx' $ evalTactic stx'
@[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TacticM α) : TacticM α :=
adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx, localInstances := localInsts }) x
def resetSynthInstanceCache : TacticM Unit := liftTermElabM Term.resetSynthInstanceCache
@ -201,7 +201,7 @@ def resetSynthInstanceCache : TacticM Unit := liftTermElabM Term.resetSynthInsta
s ← get;
let savedSythInstance := s.cache.synthInstance;
resetSynthInstanceCache;
finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s })
finally x (modify $ fun s => { s with cache := { s.cache with synthInstance := savedSythInstance } })
@[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : TacticM α) : TacticM α :=
if b then resettingSynthInstanceCache x else x
@ -213,8 +213,8 @@ let needReset := ctx.localInstances == mvarDecl.localInstances;
withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
def getGoals : TacticM (List MVarId) := do s ← get; pure s.goals
def setGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { goals := gs, .. s }
def appendGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { goals := s.goals ++ gs, .. s }
def setGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { s with goals := gs }
def appendGoals (gs : List MVarId) : TacticM Unit := modify $ fun s => { s with goals := s.goals ++ gs }
def pruneSolvedGoals : TacticM Unit := do
gs ← getGoals;
gs ← gs.filterM $ fun g => not <$> isExprMVarAssigned g;

2
stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -16,7 +16,7 @@ namespace Tactic
/- `elabTerm` for Tactics and basic tactics that use it. -/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr :=
liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { errToSorry := false, .. ctx }) $ do
liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { ctx with errToSorry := false }) $ do
e ← Term.elabTerm stx expectedType?;
Term.synthesizeSyntheticMVars mayPostpone;
Term.instantiateMVars stx e

63
stage0/src/Init/Lean/Elab/Term.lean
View file

@ -117,8 +117,8 @@ def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
def setEnv (env : Environment) : TermElabM Unit := modify $ fun s => { env := env, .. s }
def setMCtx (mctx : MetavarContext) : TermElabM Unit := modify $ fun s => { mctx := mctx, .. s }
def setEnv (env : Environment) : TermElabM Unit := modify $ fun s => { s with env := env }
def setMCtx (mctx : MetavarContext) : TermElabM Unit := modify $ fun s => { s with mctx := mctx }
def addContext (msg : MessageData) : TermElabM MessageData := do
env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
@ -129,7 +129,7 @@ instance monadLog : MonadLog TermElabM :=
getFileMap := do ctx ← read; pure ctx.fileMap,
getFileName := do ctx ← read; pure ctx.fileName,
addContext := addContext,
logMessage := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
logMessage := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
/--
Throws an error with the given `msgData` and extracting position information from `ref`.
@ -147,7 +147,7 @@ throw (Exception.ex Elab.Exception.unsupportedSyntax)
@[inline] def withIncRecDepth {α} (ref : Syntax) (x : TermElabM α) : TermElabM α := do
ctx ← read;
when (ctx.currRecDepth == ctx.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
protected def getCurrMacroScope : TermElabM MacroScope := do ctx ← read; pure ctx.currMacroScope
protected def getMainModule : TermElabM Name := do env ← getEnv; pure env.mainModule
@ -184,10 +184,10 @@ def getDeclName? : TermElabM (Option Name) := do ctx ← read; pure ctx.declName
def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace
def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState
def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s }
def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { s with traceState := traceState }
def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId
def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ fun s => { mctx := s.mctx.assignExpr mvarId val, .. s }
def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TermElabM Unit := do
ctx ← read;
@ -227,14 +227,14 @@ Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData Mess
private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=
let traces := newS.traceState.traces;
let messages := traces.foldl (fun (messages : MessageLog) trace => messages.add (mkMessageAux ctx ref trace MessageSeverity.information)) s.messages;
{ toState := { traceState := oldTraceState, .. newS },
messages := messages,
.. s }
{ s with
toState := { newS with traceState := oldTraceState },
messages := messages }
@[inline] def liftMetaM {α} (ref : Syntax) (x : MetaM α) : TermElabM α :=
fun ctx s =>
let oldTraceState := s.traceState;
match x ctx.toContext { traceState := {}, .. s.toState } with
match x ctx.toContext { s.toState with traceState := {} } with
| EStateM.Result.ok a newS => EStateM.Result.ok a (fromMetaState ref ctx s newS oldTraceState)
| EStateM.Result.error ex newS => EStateM.Result.error (fromMetaException ctx ref ex) (fromMetaState ref ctx s newS oldTraceState)
@ -282,41 +282,42 @@ decLevel ref u
@[inline] def savingMCtx {α} (x : TermElabM α) : TermElabM α := do
mctx ← getMCtx;
finally x (modify $ fun s => { mctx := mctx, .. s })
finally x (modify $ fun s => { s with mctx := mctx })
def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
fun ctx s =>
match (x { .. ctx }).run { .. s } with
| EStateM.Result.ok a newS => EStateM.Result.ok a { mctx := newS.mctx, ngen := newS.ngen, .. s }
let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap, cmdPos := ctx.cmdPos, levelNames := ctx.levelNames };
match (x lvlCtx).run { ngen := s.ngen, mctx := s.mctx } with
| EStateM.Result.ok a newS => EStateM.Result.ok a { s with mctx := newS.mctx, ngen := newS.ngen }
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.ex ex) s
def elabLevel (stx : Syntax) : TermElabM Level :=
liftLevelM $ Level.elabLevel stx
@[inline] def withConfig {α} (f : Meta.Config → Meta.Config) (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { config := f ctx.config, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
@[inline] def withTransparency {α} (mode : Meta.TransparencyMode) (x : TermElabM α) : TermElabM α :=
withConfig (fun config => { transparency := mode, .. config }) x
withConfig (fun config => { config with transparency := mode }) x
@[inline] def withReducible {α} (x : TermElabM α) : TermElabM α :=
withTransparency Meta.TransparencyMode.reducible x
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
/-
Add the given metavariable to the list of pending synthetic metavariables.
The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/
def registerSyntheticMVar (ref : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit :=
modify $ fun s => { syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars, .. s }
modify $ fun s => { s with syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars }
/-
Execute `x` without allowing it to postpone elaboration tasks.
That is, `tryPostpone` is a noop. -/
@[inline] def withoutPostponing {α} (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { mayPostpone := false, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with mayPostpone := false }) x
/-- Creates syntax for `(` <ident> `:` <type> `)` -/
def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
@ -327,7 +328,7 @@ def levelMVarToParam (e : Expr) : TermElabM Expr := do
ctx ← read;
mctx ← getMCtx;
let r := mctx.levelMVarToParam (fun n => ctx.levelNames.elem n) e;
modify $ fun s => { mctx := r.mctx, .. s };
modify $ fun s => { s with mctx := r.mctx };
pure r.expr
/--
@ -336,7 +337,7 @@ pure r.expr
def mkFreshAnonymousName : TermElabM Name := do
s ← get;
let anonymousIdx := s.anonymousIdx;
modify $ fun s => { anonymousIdx := s.anonymousIdx + 1, .. s};
modify $ fun s => { s with anonymousIdx := s.anonymousIdx + 1 };
pure $ (`_a).appendIndexAfter anonymousIdx
/--
@ -353,7 +354,7 @@ pure $ mkIdentFrom ref n
def mkFreshInstanceName : TermElabM Name := do
s ← get;
let instIdx := s.instImplicitIdx;
modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
modify $ fun s => { s with instImplicitIdx := s.instImplicitIdx + 1 };
pure $ (`_inst).appendIndexAfter instIdx
private partial def hasCDot : Syntax → Bool
@ -396,7 +397,7 @@ else
def mkFreshFVarId : TermElabM Name := do
s ← get;
let id := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
modify $ fun s => { s with ngen := s.ngen.next };
pure id
def withLocalDecl {α} (ref : Syntax) (n : Name) (binderInfo : BinderInfo) (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
@ -407,8 +408,8 @@ let localInsts := ctx.localInstances;
let fvar := mkFVar fvarId;
c? ← isClass ref type;
match c? with
| some c => adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar }, .. ctx }) $ k fvar
| none => adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ k fvar
| some c => adaptReader (fun (ctx : Context) => { ctx with lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar } }) $ k fvar
| none => adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $ k fvar
def withLetDecl {α} (ref : Syntax) (n : Name) (type : Expr) (val : Expr) (k : Expr → TermElabM α) : TermElabM α := do
fvarId ← mkFreshFVarId;
@ -418,8 +419,8 @@ let localInsts := ctx.localInstances;
let fvar := mkFVar fvarId;
c? ← isClass ref type;
match c? with
| some c => adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar }, .. ctx }) $ k fvar
| none => adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ k fvar
| some c => adaptReader (fun (ctx : Context) => { ctx with lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar } }) $ k fvar
| none => adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $ k fvar
def throwTypeMismatchError {α} (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr)
(f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
@ -439,7 +440,7 @@ match f? with
throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f e { env := env, mctx := mctx, lctx := lctx, opts := opts } ++ extraMsg
@[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { macroStackAtErr := false, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with macroStackAtErr := false }) x
/- Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of `instMVar` coincide
@ -760,7 +761,7 @@ instance : MonadMacroAdapter TermElabM :=
{ getEnv := getEnv,
getCurrMacroScope := getCurrMacroScope,
getNextMacroScope := do s ← get; pure s.nextMacroScope,
setNextMacroScope := fun next => modify $ fun s => { nextMacroScope := next, .. s },
setNextMacroScope := fun next => modify $ fun s => { s with nextMacroScope := next },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax}
@ -866,16 +867,16 @@ fun stx expectedType? => do
withMacroExpansion stx stx' $ elabTerm stx' expectedType?
@[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx, localInstances := localInsts }) x
def resetSynthInstanceCache : TermElabM Unit :=
modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s }
modify $ fun s => { s with cache := { s.cache with synthInstance := {} } }
@[inline] def resettingSynthInstanceCache {α} (x : TermElabM α) : TermElabM α := do
s ← get;
let savedSythInstance := s.cache.synthInstance;
resetSynthInstanceCache;
finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s })
finally x (modify $ fun s => { s with cache := { s.cache with synthInstance := savedSythInstance } })
@[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : TermElabM α) : TermElabM α :=
if b then resettingSynthInstanceCache x else x

25
stage0/src/Init/Lean/Environment.lean
View file

@ -55,7 +55,7 @@ instance : Inhabited Environment :=
⟨{ const2ModIdx := {}, constants := {}, extensions := #[] }⟩
def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
{ constants := env.constants.insert cinfo.name cinfo, .. env }
{ env with constants := env.constants.insert cinfo.name cinfo }
@[export lean_environment_find]
def find? (env : Environment) (n : Name) : Option ConstantInfo :=
@ -73,7 +73,7 @@ env.header.moduleNames
@[export lean_environment_set_main_module]
def setMainModule (env : Environment) (m : Name) : Environment :=
{ header := { mainModule := m, .. env.header }, .. env }
{ env with header := { env.header with mainModule := m } }
@[export lean_environment_main_module]
def mainModule (env : Environment) : Name :=
@ -81,7 +81,7 @@ env.header.mainModule
@[export lean_environment_mark_quot_init]
private def markQuotInit (env : Environment) : Environment :=
{ header := { quotInit := true, .. env.header } , .. env }
{ env with header := { env.header with quotInit := true } }
@[export lean_environment_quot_init]
private def isQuotInit (env : Environment) : Bool :=
@ -140,7 +140,7 @@ structure EnvExtension (σ : Type) :=
namespace EnvExtension
unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
{ extensions := env.extensions.set! ext.idx (unsafeCast s), .. env }
{ env with extensions := env.extensions.set! ext.idx (unsafeCast s) }
@[implementedBy setStateUnsafe]
constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := arbitrary _
@ -153,11 +153,11 @@ unsafeCast s
constant getState {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ := ext.stateInh
@[inline] unsafe def modifyStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment :=
{ extensions := env.extensions.modify ext.idx $ fun s =>
{ env with
extensions := env.extensions.modify ext.idx $ fun s =>
let s : σ := unsafeCast s;
let s : σ := f s;
unsafeCast s,
.. env }
unsafeCast s }
@[implementedBy modifyStateUnsafe]
constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := arbitrary _
@ -260,16 +260,16 @@ def getModuleEntries {α β σ : Type} (ext : PersistentEnvExtension α β σ) (
def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
ext.toEnvExtension.modifyState env $ fun s =>
let state := ext.addEntryFn s.state b;
{ state := state, .. s }
{ s with state := state }
def getState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) : σ :=
(ext.toEnvExtension.getState env).state
def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=
ext.toEnvExtension.modifyState env $ fun ps => { state := s, .. ps }
ext.toEnvExtension.modifyState env $ fun ps => { ps with state := s }
def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) : Environment :=
ext.toEnvExtension.modifyState env $ fun ps => { state := f (ps.state), .. ps }
ext.toEnvExtension.modifyState env $ fun ps => { ps with state := f (ps.state) }
end PersistentEnvExtension
@ -504,15 +504,14 @@ pure $ mods.iterate env $ fun _ mod env =>
pExtDescrs.iterate env $ fun _ extDescr env =>
let entries := getEntriesFor mod extDescr.name 0;
extDescr.toEnvExtension.modifyState env $ fun s =>
{ importedEntries := s.importedEntries.push entries,
.. s }
{ s with importedEntries := s.importedEntries.push entries }
private def finalizePersistentExtensions (env : Environment) : IO Environment := do
pExtDescrs ← persistentEnvExtensionsRef.get;
pExtDescrs.iterateM env $ fun _ extDescr env => do
let s := extDescr.toEnvExtension.getState env;
newState ← extDescr.addImportedFn env s.importedEntries;
pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
pure $ extDescr.toEnvExtension.setState env { s with state := newState }
@[export lean_import_modules]
def importModules (imports : List Import) (trustLevel : UInt32 := 0) : IO Environment := do

2
stage0/src/Init/Lean/Message.lean
View file

@ -169,7 +169,7 @@ log.msgs.any $ fun m => match m.severity with
| _ => false
def errorsToWarnings (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { severity := MessageSeverity.warning, .. m} | _ => m) }
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
log.msgs.forM f

10
stage0/src/Init/Lean/Meta/AbstractMVars.lean
View file

@ -37,7 +37,7 @@ abbrev M := ReaderT MetavarContext (StateM State)
def mkFreshId : M Name := do
s ← get;
let fresh := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
modify $ fun s => { s with ngen := s.ngen.next };
pure fresh
@[inline] private def visitLevel (f : Level → M Level) (u : Level) : M Level :=
@ -65,7 +65,7 @@ private partial def abstractLevelMVars : Level → M Level
| none => do
let paramId := mkNameNum `_abstMVar s.nextParamIdx;
let u := mkLevelParam paramId;
modify $ fun s => { nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId, .. s };
modify $ fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId };
pure u
partial def abstractExprMVars : Expr → M Expr
@ -94,10 +94,10 @@ partial def abstractExprMVars : Expr → M Expr
let fvar := mkFVar fvarId;
let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter s.fvars.size else decl.userName;
modify $ fun s => {
s with
emap := s.emap.insert mvarId fvar,
fvars := s.fvars.push fvar,
lctx := s.lctx.mkLocalDecl fvarId userName type,
.. s };
lctx := s.lctx.mkLocalDecl fvarId userName type };
pure fvar
| Expr.localE _ _ _ _ => unreachable!
@ -126,7 +126,7 @@ e ← instantiateMVars e;
s ← get;
lctx ← getLCtx;
let (e, s) := AbstractMVars.abstractExprMVars e s.mctx { lctx := lctx, ngen := s.ngen };
modify $ fun s => { ngen := s.ngen, .. s };
modify $ fun s => { s with ngen := s.ngen };
let e := s.lctx.mkLambda s.fvars e;
pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }

72
stage0/src/Init/Lean/Meta/Basic.lean
View file

@ -138,7 +138,7 @@ instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
@[inline] def withIncRecDepth {α} (x : MetaM α) : MetaM α := do
ctx ← read;
when (ctx.currRecDepth == ctx.maxRecDepth) $ throw $ Exception.other maxRecDepthErrorMessage;
adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
@[inline] def getLCtx : MetaM LocalContext := do
ctx ← read; pure ctx.lctx
@ -156,7 +156,7 @@ s ← get; pure s.mctx
s ← get; pure s.env
@[inline] def setEnv (env : Environment) : MetaM Unit := do
modify $ fun s => { env := env, .. s }
modify $ fun s => { s with env := env }
def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
IO.mkRef $ fun _ => throw $ Exception.other "whnf implementation was not set"
@ -225,14 +225,14 @@ withIncRecDepth $ do
def mkFreshId : MetaM Name := do
s ← get;
let id := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
modify $ fun s => { s with ngen := s.ngen.next };
pure id
def mkFreshExprMVarAt
(lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
: MetaM Expr := do
mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind, .. s };
modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
pure $ mkMVar mvarId
def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
@ -242,13 +242,13 @@ mkFreshExprMVarAt lctx localInsts type userName kind
def mkFreshLevelMVar : MetaM Level := do
mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s};
modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
pure $ mkLevelMVar mvarId
@[inline] def throwEx {α} (f : ExceptionContext → Exception) : MetaM α := do
ctx ← read;
s ← get;
throw (f {env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts })
throw (f { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts })
def throwBug {α} (b : Bug) : MetaM α :=
throwEx $ Exception.bug b
@ -276,11 +276,11 @@ ctx ← read; pure ctx.config.opts
env ← getEnv; pure $ isReducible env constName
@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := f ctx.config, .. ctx }) x
adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
/-- While executing `x`, ensure the given transparency mode is used. -/
@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig (fun config => { transparency := mode, .. config }) x
withConfig (fun config => { config with transparency := mode }) x
@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
withTransparency TransparencyMode.reducible x
@ -290,7 +290,7 @@ withConfig
(fun config =>
let oldMode := config.transparency;
let mode := if oldMode.lt mode then mode else oldMode;
{ transparency := mode, .. config })
{ config with transparency := mode })
x
def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
@ -300,7 +300,7 @@ match mctx.findDecl? mvarId with
| none => throwEx $ Exception.unknownExprMVar mvarId
def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
modify $ fun s => { mctx := s.mctx.setMVarKind mvarId kind, .. s}
modify $ fun s => { s with mctx := s.mctx.setMVarKind mvarId kind }
def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
mvarDecl ← getMVarDecl mvarId;
@ -322,7 +322,7 @@ match mctx.findLevelDepth? mvarId with
| _ => throwEx $ Exception.unknownLevelMVar mvarId
def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
modify $ fun s => { mctx := s.mctx.renameMVar mvarId newUserName, .. s }
modify $ fun s => { s with mctx := s.mctx.renameMVar mvarId newUserName }
@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool := do
mctx ← getMCtx;
@ -333,7 +333,7 @@ mctx ← getMCtx; pure (mctx.getExprAssignment? mvarId)
def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit := do
whenDebugging $ whenM (isExprMVarAssigned mvarId) $ throwBug $ Bug.overwritingExprMVar mvarId;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId val, .. s }
modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
def isDelayedAssigned (mvarId : MVarId) : MetaM Bool := do
mctx ← getMCtx;
@ -358,7 +358,7 @@ instance tracer : SimpleMonadTracerAdapter MetaM :=
{ getOptions := getOptions,
getTraceState := getTraceState,
addContext := addContext,
modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } }
def getConstAux (constName : Name) (exception? : Bool) : MetaM (Option ConstantInfo) := do
env ← getEnv;
@ -399,7 +399,7 @@ def instantiateMVars (e : Expr) : MetaM Expr :=
if e.hasMVar then
modifyGet $ fun s =>
let (e, mctx) := s.mctx.instantiateMVars e;
(e, { mctx := mctx, .. s })
(e, { s with mctx := mctx })
else
pure e
@ -407,11 +407,11 @@ else
fun ctx s =>
match x ctx.lctx { mctx := s.mctx, ngen := s.ngen } with
| EStateM.Result.ok e newS =>
EStateM.Result.ok e { mctx := newS.mctx, ngen := newS.ngen, .. s}
EStateM.Result.ok e { s with mctx := newS.mctx, ngen := newS.ngen }
| EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) newS =>
EStateM.Result.error
(Exception.revertFailure toRevert decl { lctx := lctx, mctx := mctx, env := s.env, opts := ctx.config.opts })
{ mctx := newS.mctx, ngen := newS.ngen, .. s }
{ s with mctx := newS.mctx, ngen := newS.ngen }
def mkForall (xs : Array Expr) (e : Expr) : MetaM Expr :=
if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkForall xs e
@ -429,7 +429,7 @@ if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e
@[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
s ← get;
let savedCache := s.cache;
finally x (modify $ fun s => { cache := savedCache, .. s })
finally x (modify $ fun s => { s with cache := savedCache })
def isClassQuickConst (constName : Name) : MetaM (LOption Name) := do
env ← getEnv;
@ -468,8 +468,8 @@ partial def isClassQuick : Expr → MetaM (LOption Name)
@[inline] def resettingSynthInstanceCache {α} (x : MetaM α) : MetaM α := do
s ← get;
let savedSythInstance := s.cache.synthInstance;
modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s };
finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s })
modify $ fun s => { s with cache := { s.cache with synthInstance := {} } };
finally x (modify $ fun s => { s with cache := { s.cache with synthInstance := savedSythInstance } })
/-- Add entry `{ className := className, fvar := fvar }` to localInstances,
and then execute continuation `k`.
@ -477,9 +477,7 @@ finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, ..
@[inline] def withNewLocalInstance {α} (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α :=
resettingSynthInstanceCache $
adaptReader
(fun (ctx : Context) => {
localInstances := ctx.localInstances.push { className := className, fvar := fvar },
.. ctx })
(fun (ctx : Context) => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
k
/--
@ -555,12 +553,12 @@ resettingSynthInstanceCache $
process ()
else
let type := type.instantiateRevRange j fvars.size fvars;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewLocalInstances isClassExpensive fvars j $
k fvars type
| lctx, fvars, j, type =>
let type := type.instantiateRevRange j fvars.size fvars;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewLocalInstances isClassExpensive fvars j $
if reducing? then do
newType ← whnf type;
@ -646,7 +644,7 @@ private partial def lambdaTelescopeAux {α}
lambdaTelescopeAux lctx (fvars.push fvar) j b
| lctx, fvars, j, e =>
let e := e.instantiateRevRange j fvars.size fvars;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewLocalInstances isClassExpensive fvars j $ do
k fvars e
@ -728,17 +726,17 @@ lambdaMetaTelescopeAux maxMVars? #[] #[] 0 e
@[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α :=
fun _ s =>
let (a, mctx) := x.run s.mctx;
EStateM.Result.ok a { mctx := mctx, .. s }
EStateM.Result.ok a { s with mctx := mctx }
def instantiateLevelMVars (lvl : Level) : MetaM Level :=
liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
def assignLevelMVar (mvarId : MVarId) (lvl : Level) : MetaM Unit :=
modify $ fun s => { mctx := MetavarContext.assignLevel s.mctx mvarId lvl, .. s }
modify $ fun s => { s with mctx := MetavarContext.assignLevel s.mctx mvarId lvl }
def mkFreshLevelMVarId : MetaM MVarId := do
mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
pure mvarId
def whnfD : Expr → MetaM Expr :=
@ -746,7 +744,7 @@ fun e => withTransparency TransparencyMode.default $ whnf e
/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`. -/
@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, .. ctx.config }, .. ctx })
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true} })
x
/--
@ -757,7 +755,7 @@ adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox :=
as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
solve `[HasPure (fun _ => IO Bool)]` -/
@[inline] def fullApproxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true, .. ctx.config }, .. ctx })
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true } })
x
@[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
@ -771,7 +769,7 @@ fvarId ← mkFreshId;
ctx ← read;
let lctx := ctx.lctx.mkLocalDecl fvarId n type bi;
let fvar := mkFVar fvarId;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewFVar fvar type k
def withLocalDeclD {α} (n : Name) (type : Expr) (k : Expr → MetaM α) : MetaM α :=
@ -782,7 +780,7 @@ fvarId ← mkFreshId;
ctx ← read;
let lctx := ctx.lctx.mkLetDecl fvarId n type val;
let fvar := mkFVar fvarId;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewFVar fvar type k
/--
@ -791,12 +789,12 @@ adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
@[inline] def withNewMCtxDepth {α} (x : MetaM α) : MetaM α := do
s ← get;
let savedMCtx := s.mctx;
modify $ fun s => { mctx := s.mctx.incDepth, .. s };
finally x (modify $ fun s => { mctx := savedMCtx, .. s })
modify $ fun s => { s with mctx := s.mctx.incDepth };
finally x (modify $ fun s => { s with mctx := savedMCtx })
def withLocalContext {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
localInstsCurr ← getLocalInstances;
adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx, localInstances := localInsts }) $
if localInsts == localInstsCurr then
x
else
@ -812,8 +810,8 @@ withLocalContext mvarDecl.lctx mvarDecl.localInstances x
@[inline] def withMCtx {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
mctx' ← getMCtx;
modify $ fun s => { mctx := mctx, .. s };
finally x (modify $ fun s => { mctx := mctx', .. s })
modify $ fun s => { s with mctx := mctx };
finally x (modify $ fun s => { s with mctx := mctx' })
/--
Create an auxiliary definition with the given name, type and value.

12
stage0/src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -218,7 +218,7 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr →
| Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
| Expr.lam n d₁ b₁ _, Expr.lam _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
| _, _ =>
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
isDefEqBindingDomain fvars ds₂ 0 $
isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
@ -372,15 +372,15 @@ private def findCached? (e : Expr) : CheckAssignmentM (Option Expr) := do
s ← get; pure $ s.checkCache.find? e
private def cache (e r : Expr) : CheckAssignmentM Unit :=
modify $ fun s => { checkCache := s.checkCache.insert e r, .. s }
modify $ fun s => { s with checkCache := s.checkCache.insert e r }
instance : MonadCache Expr Expr CheckAssignmentM :=
{ findCached? := findCached?, cache := cache }
def liftMetaM {α} (x : MetaM α) : CheckAssignmentM α :=
fun ctx s => match x ctx.toContext s.toState with
| EStateM.Result.ok a newS => EStateM.Result.ok a { toState := newS, .. s }
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }
| EStateM.Result.ok a newS => EStateM.Result.ok a { s with toState := newS }
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { s with toState := newS }
@[inline] private def visit (f : Expr → CheckAssignmentM Expr) (e : Expr) : CheckAssignmentM Expr :=
if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f
@ -402,7 +402,7 @@ s ← get; pure s.mctx
def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) : CheckAssignmentM Expr := do
s ← get;
let mvarId := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type, .. s };
modify $ fun s => { s with ngen := s.ngen.next, mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type };
pure (mkMVar mvarId)
@[specialize] def checkMVar (check : Expr → CheckAssignmentM Expr) (mvar : Expr) : CheckAssignmentM Expr := do
@ -428,7 +428,7 @@ else match mctx.getExprAssignment? mvarId with
Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
a metavariable that we also need to reduce the context. -/
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId newMVar };
pure newMVar
else
pure mvar

4
stage0/src/Init/Lean/Meta/FunInfo.lean
View file

@ -17,7 +17,7 @@ match s.cache.funInfo.find? ⟨t, fn, maxArgs?⟩ with
| some finfo => pure finfo
| none => do
finfo ← k;
modify $ fun s => { cache := { funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo, .. s.cache }, .. s };
modify $ fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo } };
pure finfo
@[inline] private def whenHasVar {α} (e : Expr) (deps : α) (k : α → α) : α :=
@ -49,7 +49,7 @@ else
pinfo.mapIdx $ fun i info =>
if info.hasFwdDeps then info
else if backDeps.contains i then
{ hasFwdDeps := true, .. info }
{ info with hasFwdDeps := true }
else
info

2
stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean
View file

@ -24,7 +24,7 @@ partial def updateTypes (e newE : Expr) : Array Entry → Nat → MetaM (Array E
typeAbst ← kabstract type e;
if typeAbst.hasLooseBVars then do
let typeNew := typeAbst.instantiate1 newE;
let entries := entries.set ⟨i, h⟩ { type := typeNew, modified := true, .. entry };
let entries := entries.set ⟨i, h⟩ { entry with type := typeNew, modified := true };
updateTypes entries (i+1)
else
updateTypes entries (i+1)

4
stage0/src/Init/Lean/Meta/InferType.lean
View file

@ -100,7 +100,7 @@ lambdaTelescope e $ fun xs e => do
@[inline] private def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
savingCache $ do
fvarId ← mkFreshId;
adaptReader (fun (ctx : Context) => { lctx := ctx.lctx.mkLocalDecl fvarId name type bi, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) $
x (mkFVar fvarId)
private def inferMVarType (mvarId : MVarId) : MetaM Expr := do
@ -121,7 +121,7 @@ match s.cache.inferType.find? e with
| some type => pure type
| none => do
type ← inferType;
modify $ fun s => { cache := { inferType := s.cache.inferType.insert e type, .. s.cache }, .. s };
modify $ fun s => { s with cache := { s.cache with inferType := s.cache.inferType.insert e type } };
pure type
private partial def inferTypeAux : Expr → MetaM Expr

10
stage0/src/Init/Lean/Meta/LevelDefEq.lean
View file

@ -45,7 +45,7 @@ result? ← decAux? u;
match result? with
| some v => pure $ some v
| none => do
modify $ fun s => { mctx := mctx, .. s };
modify $ fun s => { s with mctx := mctx };
pure none
private def strictOccursMaxAux (lvl : Level) : Level → Bool
@ -73,7 +73,7 @@ n ← mkFreshLevelMVar;
assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n
private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit :=
modify $ fun s => { postponed := s.postponed.push { lhs := lhs, rhs := rhs }, .. s }
modify $ fun s => { s with postponed := s.postponed.push { lhs := lhs, rhs := rhs } }
inductive LevelConstraintKind
| mvarEq -- ?m =?= l where ?m does not occur in l
@ -150,7 +150,7 @@ s ← get; pure s.postponed.size
private def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
s ← get;
let ps := s.postponed;
modify $ fun s => { postponed := {}, .. s };
modify $ fun s => { s with postponed := {} };
pure ps
private def processPostponedStep : MetaM Bool :=
@ -190,7 +190,7 @@ if numPostponed == 0 then pure true
else traceCtx `Meta.isLevelDefEq.postponed $ processPostponedAux ()
def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit :=
modify $ fun s => { env := env, mctx := mctx, postponed := postponed, .. s }
modify $ fun s => { s with env := env, mctx := mctx, postponed := postponed }
/--
`commitWhen x` executes `x` and process all postponed universe level constraints produced by `x`.
@ -203,7 +203,7 @@ s ← get;
let env := s.env;
let mctx := s.mctx;
let postponed := s.postponed;
modify $ fun s => { postponed := {}, .. s };
modify $ fun s => { s with postponed := {} };
catch
(condM x
(condM processPostponed

50
stage0/src/Init/Lean/Meta/SynthInstance.lean
View file

@ -94,7 +94,7 @@ partial def normLevel : Level → M Level
| some u' => pure u'
| none => do
let u' := mkLevelParam $ mkNameNum `_tc s.nextIdx;
modify $ fun s => { nextIdx := s.nextIdx + 1, lmap := s.lmap.insert mvarId u', .. s };
modify $ fun s => { s with nextIdx := s.nextIdx + 1, lmap := s.lmap.insert mvarId u' };
pure u'
| u => pure u
@ -118,7 +118,7 @@ partial def normExpr : Expr → M Expr
| some e' => pure e'
| none => do
let e' := mkFVar $ mkNameNum `_tc s.nextIdx;
modify $ fun s => { nextIdx := s.nextIdx + 1, emap := s.emap.insert mvarId e', .. s };
modify $ fun s => { s with nextIdx := s.nextIdx + 1, emap := s.emap.insert mvarId e' };
pure e'
| _ => pure e
@ -166,17 +166,17 @@ instance tracer : SimpleMonadTracerAdapter SynthM :=
{ getOptions := getOptions,
getTraceState := getTraceState,
addContext := addContext,
modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } }
@[inline] def liftMeta {α} (x : MetaM α) : SynthM α :=
adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { toState := s', .. s }) x
adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { s with toState := s' }) x
instance meta2Synth {α} : HasCoe (MetaM α) (SynthM α) := ⟨liftMeta⟩
@[inline] def withMCtx {α} (mctx : MetavarContext) (x : SynthM α) : SynthM α := do
mctx' ← getMCtx;
modify $ fun s => { mctx := mctx, .. s };
finally x (modify $ fun s => { mctx := mctx', .. s })
modify $ fun s => { s with mctx := mctx };
finally x (modify $ fun s => { s with mctx := mctx' })
/-- Return globals and locals instances that may unify with `type` -/
def getInstances (type : Expr) : MetaM (Array Expr) :=
@ -217,9 +217,9 @@ withMCtx mctx $ do
};
let entry : TableEntry := { waiters := #[waiter] };
modify $ fun s =>
{ generatorStack := s.generatorStack.push node,
tableEntries := s.tableEntries.insert key entry,
.. s }
{ s with
generatorStack := s.generatorStack.push node,
tableEntries := s.tableEntries.insert key entry }
def findEntry? (key : Expr) : SynthM (Option TableEntry) := do
s ← get;
@ -294,7 +294,7 @@ match inst.getAppFn with
| Expr.const constName _ _ => do
env ← getEnv;
if hasInferTCGoalsLRAttribute env constName then
pure { subgoals := result.subgoals.reverse, .. result }
pure { result with subgoals := result.subgoals.reverse }
else
pure result
| _ => pure result
@ -339,12 +339,12 @@ withMCtx mctx $ do
def wakeUp (answer : Answer) : Waiter → SynthM Unit
| Waiter.root =>
if answer.result.paramNames.isEmpty && answer.result.numMVars == 0 then do
modify $ fun s => { result := answer.result.expr, .. s }
modify $ fun s => { s with result := answer.result.expr }
else do
(_, _, answerExpr) ← openAbstractMVarsResult answer.result;
trace! `Meta.synthInstance ("skip answer containing metavariables " ++ answerExpr);
pure ()
| Waiter.consumerNode cNode => modify $ fun s => { resumeStack := s.resumeStack.push (cNode, answer), .. s }
| Waiter.consumerNode cNode => modify $ fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
oldAnswers.all $ fun oldAnswer => do
@ -368,8 +368,8 @@ answer ← withMCtx cNode.mctx $ do {
let key := cNode.key;
entry ← getEntry key;
when (isNewAnswer entry.answers answer) $ do
let newEntry := { answers := entry.answers.push answer, .. entry };
modify $ fun s => { tableEntries := s.tableEntries.insert key newEntry, .. s };
let newEntry := { entry with answers := entry.answers.push answer };
modify $ fun s => { s with tableEntries := s.tableEntries.insert key newEntry };
entry.waiters.forM (wakeUp answer)
/-- Process the next subgoal in the given consumer node. -/
@ -383,21 +383,21 @@ match cNode.subgoals with
match entry? with
| none => newSubgoal cNode.mctx key mvar waiter
| some entry => modify $ fun s =>
{ resumeStack := entry.answers.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,
tableEntries := s.tableEntries.insert key { waiters := entry.waiters.push waiter, .. entry },
.. s }
{ s with
resumeStack := entry.answers.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,
tableEntries := s.tableEntries.insert key { entry with waiters := entry.waiters.push waiter } }
def getTop : SynthM GeneratorNode := do
s ← get; pure s.generatorStack.back
@[inline] def modifyTop (f : GeneratorNode → GeneratorNode) : SynthM Unit :=
modify $ fun s => { generatorStack := s.generatorStack.modify (s.generatorStack.size - 1) f, .. s }
modify $ fun s => { s with generatorStack := s.generatorStack.modify (s.generatorStack.size - 1) f }
/-- Try the next instance in the node on the top of the generator stack. -/
def generate : SynthM Unit := do
gNode ← getTop;
if gNode.currInstanceIdx == 0 then
modify $ fun s => { generatorStack := s.generatorStack.pop, .. s }
modify $ fun s => { s with generatorStack := s.generatorStack.pop }
else do
let key := gNode.key;
let idx := gNode.currInstanceIdx - 1;
@ -405,7 +405,7 @@ else do
let mctx := gNode.mctx;
let mvar := gNode.mvar;
trace! `Meta.synthInstance.generate ("instance " ++ inst);
modifyTop $ fun gNode => { currInstanceIdx := idx, .. gNode };
modifyTop $ fun gNode => { gNode with currInstanceIdx := idx };
result? ← tryResolve mctx mvar inst;
match result? with
| none => pure ()
@ -414,7 +414,7 @@ else do
def getNextToResume : SynthM (ConsumerNode × Answer) := do
s ← get;
let r := s.resumeStack.back;
modify $ fun s => { resumeStack := s.resumeStack.pop, .. s };
modify $ fun s => { s with resumeStack := s.resumeStack.pop };
pure r
/--
@ -465,7 +465,7 @@ traceCtx `Meta.synthInstance $ do
mvar ← mkFreshExprMVar type;
mctx ← getMCtx;
let key := mkTableKey mctx type;
adaptState' (fun (s : Meta.State) => { State . .. s }) (fun (s : State) => s.toState) $ do {
adaptState' (fun (s : Meta.State) => { State . toState := s }) (fun (s : State) => s.toState) $ do {
newSubgoal mctx key mvar Waiter.root;
synth fuel
}
@ -542,7 +542,7 @@ def synthInstance? (type : Expr) : MetaM (Option Expr) := do
opts ← getOptions;
let fuel := getMaxSteps opts;
inputConfig ← getConfig;
withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox := true, ctxApprox := true, .. config }) $ do
withConfig (fun config => { config with transparency := TransparencyMode.reducible, foApprox := true, ctxApprox := true }) $ do
type ← instantiateMVars type;
type ← preprocess type;
s ← get;
@ -575,14 +575,14 @@ withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox
if type.hasMVar then
pure result?
else do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result?, .. s.cache }, .. s };
modify $ fun s => { s with cache := { s.cache with synthInstance := s.cache.synthInstance.insert type result? } };
pure result?
/--
Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
instance cannot be synthesized right now because `type` contains metavariables. -/
def trySynthInstance (type : Expr) : MetaM (LOption Expr) :=
adaptReader (fun (ctx : Context) => { config := { isDefEqStuckEx := true, .. ctx.config }, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with isDefEqStuckEx := true } }) $
catch
(toLOptionM $ synthInstance? type)
(fun ex => match ex with

12
stage0/src/Init/Lean/Meta/Tactic/Cases.lean
View file

@ -165,7 +165,7 @@ s₂.mapM $ fun s => do
indicesFVarIds.foldlM
(fun s indexFVarId =>
let indexFVarId' := s.subst.get indexFVarId;
(do mvarId ← clear s.mvarId indexFVarId'; pure { mvarId := mvarId, subst := s.subst.erase indexFVarId, .. s })
(do mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId })
<|>
(pure s))
s
@ -188,27 +188,27 @@ private partial def unifyEqsAux : Nat → CasesSubgoal → MetaM (Option CasesSu
aEqb ← mkEq a b;
mvarId ← assert mvarId eqDecl.userName aEqb prf;
mvarId ← clear mvarId eqFVarId;
unifyEqsAux (n+1) { mvarId := mvarId, .. s }
unifyEqsAux (n+1) { s with mvarId := mvarId }
| none => match eqDecl.type.eq? with
| some (α, a, b) =>
let skip : Unit → MetaM (Option CasesSubgoal) := fun _ => do {
mvarId ← clear mvarId eqFVarId;
unifyEqsAux n { mvarId := mvarId, .. s }
unifyEqsAux n { s with mvarId := mvarId }
};
let substEq (symm : Bool) : MetaM (Option CasesSubgoal) := do {
(newSubst, mvarId) ← substCore mvarId eqFVarId false true;
unifyEqsAux n {
s with
mvarId := mvarId,
subst := newSubst.compose s.subst,
fields := s.fields.map $ fun fvarId => newSubst.get fvarId,
.. s
fields := s.fields.map $ fun fvarId => newSubst.get fvarId
}
};
let inj : Unit → MetaM (Option CasesSubgoal) := fun _ => do {
r ← injectionCore mvarId eqFVarId;
match r with
| InjectionResultCore.solved => pure none -- this alternative has been solved
| InjectionResultCore.subgoal mvarId numEqs => unifyEqsAux (n+numEqs) { mvarId := mvarId, .. s }
| InjectionResultCore.subgoal mvarId numEqs => unifyEqsAux (n+numEqs) { s with mvarId := mvarId }
};
condM (isDefEq a b) (skip ()) $ do
a ← whnf a;

4
stage0/src/Init/Lean/Meta/Tactic/Intro.lean
View file

@ -14,7 +14,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
: Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId)
| 0, lctx, fvars, j, _, type =>
let type := type.instantiateRevRange j fvars.size fvars;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewLocalInstances isClassExpensive fvars j $ do
tag ← getMVarTag mvarId;
let type := type.headBeta;
@ -44,7 +44,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
introNCoreAux i lctx fvars j s body
| (i+1), lctx, fvars, j, s, type =>
let type := type.instantiateRevRange j fvars.size fvars;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
withNewLocalInstances isClassExpensive fvars j $ do
newType ← whnf type;
if newType.isForall then

2
stage0/src/Init/Lean/Meta/Tactic/Util.lean
View file

@ -16,7 +16,7 @@ mvarDecl ← getMVarDecl mvarId;
pure mvarDecl.userName
def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
modify $ fun s => { mctx := s.mctx.setMVarUserName mvarId tag, .. s }
modify $ fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag }
def mkFreshExprSyntheticOpaqueMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr :=
mkFreshExprMVar type userName MetavarKind.syntheticOpaque

2
stage0/src/Init/Lean/Meta/WHNF.lean
View file

@ -102,7 +102,7 @@ else
private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
when useCache $
modify $ fun s => { cache := { whnfDefault := s.cache.whnfDefault.insert e r, .. s.cache }, .. s };
modify $ fun s => { s with cache := { s.cache with whnfDefault := s.cache.whnfDefault.insert e r } };
pure r
partial def whnfImpl : Expr → MetaM Expr

49
stage0/src/Init/Lean/MetavarContext.lean
View file

@ -302,21 +302,20 @@ def addExprMVarDecl (mctx : MetavarContext)
(lctx : LocalContext)
(localInstances : LocalInstances)
(type : Expr) (kind : MetavarKind := MetavarKind.natural) : MetavarContext :=
{ decls := mctx.decls.insert mvarId {
{ mctx with
decls := mctx.decls.insert mvarId {
userName := userName,
lctx := lctx,
localInstances := localInstances,
type := type,
depth := mctx.depth,
kind := kind },
.. mctx }
kind := kind } }
/- Low level API for adding/declaring universe level metavariable declarations.
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
def addLevelMVarDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=
{ lDepth := mctx.lDepth.insert mvarId mctx.depth,
.. mctx }
{ mctx with lDepth := mctx.lDepth.insert mvarId mctx.depth }
@[export lean_metavar_ctx_find_decl]
def findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
@ -329,11 +328,11 @@ match mctx.decls.find? mvarId with
def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) : MetavarContext :=
let decl := mctx.getDecl mvarId;
{ decls := mctx.decls.insert mvarId { kind := kind, .. decl }, .. mctx }
{ mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } }
def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext :=
let decl := mctx.getDecl mvarId;
{ decls := mctx.decls.insert mvarId { userName := userName, .. decl }, .. mctx }
{ mctx with decls := mctx.decls.insert mvarId { decl with userName := userName } }
def findLevelDepth? (mctx : MetavarContext) (mvarId : MVarId) : Option Nat :=
mctx.lDepth.find? mvarId
@ -351,22 +350,22 @@ match mctx.findDecl? mvarId with
def renameMVar (mctx : MetavarContext) (mvarId : MVarId) (newUserName : Name) : MetavarContext :=
match mctx.findDecl? mvarId with
| none => panic! "unknown metavariable"
| some mvarDecl => { decls := mctx.decls.insert mvarId { userName := newUserName, .. mvarDecl }, .. mctx }
| some mvarDecl => { mctx with decls := mctx.decls.insert mvarId { mvarDecl with userName := newUserName } }
@[export lean_metavar_ctx_assign_level]
def assignLevel (m : MetavarContext) (mvarId : MVarId) (val : Level) : MetavarContext :=
{ lAssignment := m.lAssignment.insert mvarId val, .. m }
{ m with lAssignment := m.lAssignment.insert mvarId val }
@[export lean_metavar_ctx_assign_expr]
def assignExprCore (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
{ eAssignment := m.eAssignment.insert mvarId val, .. m }
{ m with eAssignment := m.eAssignment.insert mvarId val }
def assignExpr (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
{ eAssignment := m.eAssignment.insert mvarId val, .. m }
{ m with eAssignment := m.eAssignment.insert mvarId val }
@[export lean_metavar_ctx_assign_delayed]
def assignDelayed (m : MetavarContext) (mvarId : MVarId) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
{ dAssignment := m.dAssignment.insert mvarId { lctx := lctx, fvars := fvars, val := val }, .. m }
{ m with dAssignment := m.dAssignment.insert mvarId { lctx := lctx, fvars := fvars, val := val } }
@[export lean_metavar_ctx_get_level_assignment]
def getLevelAssignment? (m : MetavarContext) (mvarId : MVarId) : Option Level :=
@ -394,7 +393,7 @@ m.dAssignment.contains mvarId
@[export lean_metavar_ctx_erase_delayed]
def eraseDelayed (m : MetavarContext) (mvarId : MVarId) : MetavarContext :=
{ dAssignment := m.dAssignment.erase mvarId, .. m }
{ m with dAssignment := m.dAssignment.erase mvarId }
def isLevelAssignable (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
match mctx.lDepth.find? mvarId with
@ -406,7 +405,7 @@ let decl := mctx.getDecl mvarId;
decl.depth == mctx.depth
def incDepth (mctx : MetavarContext) : MetavarContext :=
{ depth := mctx.depth + 1, .. mctx }
{ mctx with depth := mctx.depth + 1 }
/-- Return true iff the given level contains an assigned metavariable. -/
def hasAssignedLevelMVar (mctx : MetavarContext) : Level → Bool
@ -487,7 +486,7 @@ if !e.hasMVar then pure e else checkCache e f
s ← get; pure s.state
@[inline] private def modifyCtx (f : MetavarContext → MetavarContext) : M Unit :=
modify $ fun s => { state := f s.state, .. s }
modify $ fun s => { s with state := f s.state }
/-- instantiateExprMVars main function -/
partial def main : Expr → M Expr
@ -585,7 +584,7 @@ def instantiateMVarDeclMVars (mctx : MetavarContext) (mvarId : MVarId) : Metavar
let mvarDecl := mctx.getDecl mvarId;
let (lctx, mctx) := mctx.instantiateLCtxMVars mvarDecl.lctx;
let (type, mctx) := mctx.instantiateMVars mvarDecl.type;
{ decls := mctx.decls.insert mvarId { lctx := lctx, type := type, .. mvarDecl }, .. mctx }
{ mctx with decls := mctx.decls.insert mvarId { mvarDecl with lctx := lctx, type := type } }
namespace DependsOn
@ -680,7 +679,7 @@ def preserveOrder : M Bool := read
instance : MonadHashMapCacheAdapter Expr Expr M :=
{ getCache := do s ← get; pure s.cache,
modifyCache := fun f => modify $ fun s => { cache := f s.cache, .. s } }
modifyCache := fun f => modify $ fun s => { s with cache := f s.cache } }
/-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl :=
@ -756,9 +755,9 @@ xs.foldl
/-- Execute `x` with an empty cache, and then restore the original cache. -/
@[inline] private def withFreshCache {α} (x : M α) : M α := do
cache ← modifyGet $ fun s => (s.cache, { cache := {}, .. s });
cache ← modifyGet $ fun s => (s.cache, { s with cache := {} });
a ← x;
modify $ fun s => { cache := cache, .. s };
modify $ fun s => { s with cache := cache };
pure a
@[inline] private def abstractRangeAux (elimMVarDeps : Expr → M Expr) (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do
@ -801,7 +800,7 @@ xs.foldl
private def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind) : M MVarId := do
s ← get;
let mvarId := s.ngen.curr;
modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type kind, ngen := s.ngen.next, .. s };
modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type kind, ngen := s.ngen.next };
pure mvarId
/-- Return true iff some `e` in `es` depends on `fvarId` -/
@ -857,9 +856,9 @@ private partial def elimMVarDepsApp (elimMVarDepsAux : Expr → M Expr) (xs : Ar
let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind;
match newMVarKind with
| MetavarKind.syntheticOpaque =>
modify $ fun s => { mctx := assignDelayed s.mctx newMVarId mvarLCtx (toRevert ++ nestedFVars) (mkAppN f nestedFVars), .. s }
modify $ fun s => { s with mctx := assignDelayed s.mctx newMVarId mvarLCtx (toRevert ++ nestedFVars) (mkAppN f nestedFVars) }
| _ =>
modify $ fun s => { mctx := assignExpr s.mctx mvarId result, .. s };
modify $ fun s => { s with mctx := assignExpr s.mctx mvarId result };
pure (mkAppN result args)
};
if !mvarDecl.kind.isSyntheticOpaque then
@ -991,10 +990,10 @@ partial def mkParamName : Unit → M Name
s ← get;
let newParamName := ctx.paramNamePrefix.appendIndexAfter s.nextParamIdx;
if ctx.alreadyUsedPred newParamName then do
modify $ fun s => { nextParamIdx := s.nextParamIdx + 1, .. s};
modify $ fun s => { s with nextParamIdx := s.nextParamIdx + 1 };
mkParamName ()
else do
modify $ fun s => { nextParamIdx := s.nextParamIdx + 1, paramNames := s.paramNames.push newParamName, .. s};
modify $ fun s => { s with nextParamIdx := s.nextParamIdx + 1, paramNames := s.paramNames.push newParamName };
pure newParamName
partial def visitLevel : Level → M Level
@ -1010,7 +1009,7 @@ partial def visitLevel : Level → M Level
| none => do
p ← mkParamName ();
let p := mkLevelParam p;
modify $ fun s => { mctx := s.mctx.assignLevel mvarId p, .. s };
modify $ fun s => { s with mctx := s.mctx.assignLevel mvarId p };
pure p
@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=

6
stage0/src/Init/Lean/Parser/Module.lean
View file

@ -16,10 +16,10 @@ def «import» := parser! "import " >> optional "runtime" >> ident
def header := parser! optional «prelude» >> many «import»
def updateTokens (c : ParserContext) : ParserContext :=
{ tokens := match addParserTokens c.tokens header.info with
{ c with
tokens := match addParserTokens c.tokens header.info with
| Except.ok tables => tables
| Except.error _ => unreachable!,
.. c }
| Except.error _ => unreachable! }
end Module

53
stage0/src/Init/Lean/Parser/Parser.lean
View file

@ -144,25 +144,25 @@ s.errorMsg != none
s.stxStack.size
def restore (s : ParserState) (iniStackSz : Nat) (iniPos : Nat) : ParserState :=
{ stxStack := s.stxStack.shrink iniStackSz, errorMsg := none, pos := iniPos, .. s}
{ s with stxStack := s.stxStack.shrink iniStackSz, errorMsg := none, pos := iniPos }
def setPos (s : ParserState) (pos : Nat) : ParserState :=
{ pos := pos, .. s }
{ s with pos := pos }
def setCache (s : ParserState) (cache : ParserCache) : ParserState :=
{ cache := cache, .. s }
{ s with cache := cache }
def pushSyntax (s : ParserState) (n : Syntax) : ParserState :=
{ stxStack := s.stxStack.push n, .. s }
{ s with stxStack := s.stxStack.push n }
def popSyntax (s : ParserState) : ParserState :=
{ stxStack := s.stxStack.pop, .. s }
{ s with stxStack := s.stxStack.pop }
def shrinkStack (s : ParserState) (iniStackSz : Nat) : ParserState :=
{ stxStack := s.stxStack.shrink iniStackSz, .. s }
{ s with stxStack := s.stxStack.shrink iniStackSz }
def next (s : ParserState) (input : String) (pos : Nat) : ParserState :=
{ pos := input.next pos, .. s }
{ s with pos := input.next pos }
def toErrorMsg (ctx : ParserContext) (s : ParserState) : String :=
match s.errorMsg with
@ -1383,7 +1383,7 @@ def categoryParserFn (catName : Name) : ParserFn :=
fun ctx s => categoryParserFnExtension.getState ctx.env catName ctx s
def categoryParser (catName : Name) (rbp : Nat) : Parser :=
{ fn := fun c s => categoryParserFn catName { rbp := rbp, .. c } s }
{ fn := fun c s => categoryParserFn catName { c with rbp := rbp } s }
-- Define `termParser` here because we need it for antiquotations
@[inline] def termParser (rbp : Nat := 0) : Parser :=
@ -1497,7 +1497,7 @@ fun ctx s =>
| _ => s.mkUnexpectedError ("failed to determine parser category using syntax stack, the specified element on the stack is not an identifier")
def categoryParserOfStack (offset : Nat) (rbp : Nat := 0) : Parser :=
{ fn := fun c s => categoryParserOfStackFn offset { rbp := rbp, .. c } s }
{ fn := fun c s => categoryParserOfStackFn offset { c with rbp := rbp } s }
private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
if s.stackSize == iniSz + 1 then s
@ -1632,7 +1632,7 @@ else match tokens.find tk.val with
| some oldTk => do
lbp ← mergePrecendences "" tk.val oldTk.lbp tk.lbp;
lbpNoWs ← mergePrecendences "(no whitespace) " tk.val oldTk.lbpNoWs tk.lbpNoWs;
pure $ tokens.insert tk.val { lbp := lbp, lbpNoWs := lbpNoWs, .. tk }
pure $ tokens.insert tk.val { tk with lbp := lbp, lbpNoWs := lbpNoWs }
def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
throw ("unknown parser category '" ++ toString catName ++ "'")
@ -1644,28 +1644,28 @@ match categories.find? catName with
| some cat =>
let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
let tks := tks.map $ fun tk => mkNameSimple tk.val;
let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) cat.tables;
pure $ categories.insert catName { tables := tables, .. cat };
let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with leadingTable := tables.leadingTable.insert tk p }) cat.tables;
pure $ categories.insert catName { cat with tables := tables };
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ =>
let tables := { leadingParsers := p :: cat.tables.leadingParsers, .. cat.tables };
pure $ categories.insert catName { tables := tables, .. cat }
let tables := { cat.tables with leadingParsers := p :: cat.tables.leadingParsers };
pure $ categories.insert catName { cat with tables := tables }
private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) : PrattParsingTables :=
let addTokens (tks : List TokenConfig) : PrattParsingTables :=
let tks := tks.map $ fun tk => mkNameSimple tk.val;
tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with trailingTable := tables.trailingTable.insert tk p }) tables;
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ => { trailingParsers := p :: tables.trailingParsers, .. tables }
| _ => { tables with trailingParsers := p :: tables.trailingParsers }
def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
match categories.find? catName with
| none => throwUnknownParserCategory catName
| some cat => pure $ categories.insert catName { tables := addTrailingParserAux cat.tables p, .. cat }
| some cat => pure $ categories.insert catName { cat with tables := addTrailingParserAux cat.tables p }
def addParser (categories : ParserCategories) (catName : Name) (declName : Name) (leading : Bool) (p : Parser) : Except String ParserCategories :=
match leading, p with
@ -1699,17 +1699,18 @@ private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExten
match e with
| ParserExtensionEntry.token tk =>
match addTokenConfig s.tokens tk with
| Except.ok tokens => { tokens := tokens, newEntries := ParserExtensionOleanEntry.token tk :: s.newEntries, .. s }
| Except.ok tokens => { s with tokens := tokens, newEntries := ParserExtensionOleanEntry.token tk :: s.newEntries }
| _ => unreachable!
| ParserExtensionEntry.kind k =>
{ kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries, .. s }
{ s with kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries }
| ParserExtensionEntry.category catName leadingIdentAsSymbol =>
if s.categories.contains catName then s
else { categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries, .. s }
else { s with
categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries }
| ParserExtensionEntry.parser catName declName leading parser =>
match addParser s.categories catName declName leading parser with
| Except.ok categories => { categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries, .. s }
| Except.ok categories => { s with categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries }
| _ => unreachable!
def compileParserDescr (categories : ParserCategories) : ParserDescr → Except String (Parser)
@ -1770,17 +1771,17 @@ es.foldlM
match entry with
| ParserExtensionOleanEntry.token tk => do
tokens ← IO.ofExcept (addTokenConfig s.tokens tk);
pure { tokens := tokens, .. s }
pure { s with tokens := tokens }
| ParserExtensionOleanEntry.kind k =>
pure { kinds := s.kinds.insert k, .. s }
pure { s with kinds := s.kinds.insert k }
| ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol});
pure { categories := categories, .. s }
pure { s with categories := categories }
| ParserExtensionOleanEntry.parser catName declName =>
match mkParserOfConstant env s.categories declName with
| Except.ok p =>
match addParser s.categories catName declName p.1 p.2 with
| Except.ok categories => pure { categories := categories, .. s }
| Except.ok categories => pure { s with categories := categories }
| Except.error ex => throw (IO.userError ex)
| Except.error ex => throw (IO.userError ex))
s)

2
stage0/src/Init/Lean/Parser/Transform.lean
View file

@ -38,7 +38,7 @@ stx.ifNodeKind `Lean.Parser.Term.paren
| atom { trailing := some outer } ")", some bodyInfo@{ trailing := some inner } =>
let bodyInfoTrail := inner.toString ++ " "; -- add whithespaces for removed parentheses
let bodyInfoTrail := bodyInfoTrail ++ outer.toString; -- add close paren trailing spaces
body.setTailInfo { trailing := bodyInfoTrail.toSubstring, .. bodyInfo }
body.setTailInfo { bodyInfo with trailing := bodyInfoTrail.toSubstring }
| _, _ => stx.val
else stx.val)
(fun _ => stx)

16
stage0/src/Init/Lean/Scopes.lean
View file

@ -27,7 +27,7 @@ namespace ScopeManagerState
instance : Inhabited ScopeManagerState := ⟨{}⟩
def saveNamespace (s : ScopeManagerState) (n : Name) : ScopeManagerState :=
{ allNamespaces := s.allNamespaces.insert n, .. s }
{ s with allNamespaces := s.allNamespaces.insert n }
end ScopeManagerState
@ -35,7 +35,7 @@ def regScopeManagerExtension : IO (SimplePersistentEnvExtension Name ScopeManage
registerSimplePersistentEnvExtension {
name := `scopes,
addImportedFn := fun as => mkStateFromImportedEntries ScopeManagerState.saveNamespace {} as,
addEntryFn := fun s n => { allNamespaces := s.allNamespaces.insert n, .. s },
addEntryFn := fun s n => { s with allNamespaces := s.allNamespaces.insert n },
}
@[init regScopeManagerExtension]
@ -101,19 +101,19 @@ let ns := env.getNamespace;
let newNs := if isNamespace then ns ++ header else ns;
let env := env.registerNamespaceAux newNs;
let env := scopeManagerExt.modifyState env $ fun s =>
{ headers := header :: s.headers,
{ s with
headers := header :: s.headers,
namespaces := newNs :: s.namespaces,
isNamespace := isNamespace :: s.isNamespace,
.. s };
isNamespace := isNamespace :: s.isNamespace };
env
def popScopeCore (env : Environment) : Environment :=
if env.getNamespaces.isEmpty then env
else scopeManagerExt.modifyState env $ fun s =>
{ headers := s.headers.tail!,
{ s with
headers := s.headers.tail!,
namespaces := s.namespaces.tail!,
isNamespace := s.isNamespace.tail!,
.. s }
isNamespace := s.isNamespace.tail! }
end Environment
end Lean

2
stage0/src/Init/Lean/Syntax.lean
View file

@ -12,7 +12,7 @@ namespace Lean
namespace SourceInfo
def updateTrailing (info : SourceInfo) (trailing : Option Substring) : SourceInfo :=
{ trailing := trailing, .. info }
{ info with trailing := trailing }
end SourceInfo

18
stage0/src/Init/Lean/Util/Closure.lean
View file

@ -39,13 +39,13 @@ else do
| some v => pure v
| none => do
v ← f u;
modify $ fun s => { visitedLevel := s.visitedLevel.insert u v, .. s };
modify $ fun s => { s with visitedLevel := s.visitedLevel.insert u v };
pure v
def mkNewLevelParam (u : Level) : ClosureM Level := do
s ← get;
let p := (`u).appendIndexAfter s.nextLevelIdx;
modify $ fun s => { levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelClosure := s.levelClosure.push u, .. s };
modify $ fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelClosure := s.levelClosure.push u };
pure $ mkLevelParam p
partial def collectLevelAux : Level → ClosureM Level
@ -62,7 +62,7 @@ visitLevel collectLevelAux u
def mkFreshFVarId : ClosureM FVarId := do
s ← get;
let id := s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
modify $ fun s => { s with ngen := s.ngen.next };
pure id
/--
@ -72,7 +72,7 @@ pure id
def mkNextUserName : ClosureM Name := do
s ← get;
let n := (`_x).appendIndexAfter s.nextExprIdx;
modify $ fun s => { nextExprIdx := s.nextExprIdx + 1, .. s };
modify $ fun s => { s with nextExprIdx := s.nextExprIdx + 1 };
pure n
def getUserName (userName? : Option Name) : ClosureM Name :=
@ -83,12 +83,12 @@ match userName? with
def mkLocalDecl (userName? : Option Name) (type : Expr) : ClosureM Expr := do
userName ← getUserName userName?;
fvarId ← mkFreshFVarId;
modify $ fun s => { lctxOutput := s.lctxOutput.mkLocalDecl fvarId userName type, .. s };
modify $ fun s => { s with lctxOutput := s.lctxOutput.mkLocalDecl fvarId userName type };
pure $ mkFVar fvarId
def mkLetDecl (userName : Name) (type : Expr) (value : Expr) : ClosureM Expr := do
fvarId ← mkFreshFVarId;
modify $ fun s => { lctxOutput := s.lctxOutput.mkLetDecl fvarId userName type value, .. s };
modify $ fun s => { s with lctxOutput := s.lctxOutput.mkLetDecl fvarId userName type value };
pure $ mkFVar fvarId
@[inline] def visitExpr (f : Expr → ClosureM Expr) (e : Expr) : ClosureM Expr :=
@ -99,7 +99,7 @@ else do
| some r => pure r
| none => do
r ← f e;
modify $ fun s => { visitedExpr := s.visitedExpr.insert e r, .. s };
modify $ fun s => { s with visitedExpr := s.visitedExpr.insert e r };
pure r
partial def collectExprAux : Expr → ClosureM Expr
@ -121,7 +121,7 @@ partial def collectExprAux : Expr → ClosureM Expr
| some mvarDecl => do
type ← collect mvarDecl.type;
x ← mkLocalDecl none type;
modify $ fun s => { exprClosure := s.exprClosure.push e, .. s };
modify $ fun s => { s with exprClosure := s.exprClosure.push e };
pure x
| Expr.fvar fvarId _ => do
ctx ← read;
@ -130,7 +130,7 @@ partial def collectExprAux : Expr → ClosureM Expr
| some (LocalDecl.cdecl _ _ userName type _) => do
type ← collect type;
x ← mkLocalDecl userName type;
modify $ fun s => { exprClosure := s.exprClosure.push e, .. s };
modify $ fun s => { s with exprClosure := s.exprClosure.push e };
pure x
| some (LocalDecl.ldecl _ _ userName type value) => do
type ← collect type;

4
stage0/src/Init/Lean/Util/CollectFVars.lean
View file

@ -21,7 +21,7 @@ abbrev Visitor := State → State
@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor :=
fun s =>
if !e.hasFVar || s.visitedExpr.contains e then s
else f e { visitedExpr := s.visitedExpr.insert e, .. s }
else f e { s with visitedExpr := s.visitedExpr.insert e }
partial def main : Expr → Visitor
| Expr.proj _ _ e _ => visit main e
@ -30,7 +30,7 @@ partial def main : Expr → Visitor
| Expr.letE _ t v b _ => visit main b ∘ visit main v ∘ visit main t
| Expr.app f a _ => visit main a ∘ visit main f
| Expr.mdata _ b _ => visit main b
| Expr.fvar fvarId _ => fun s => { fvarSet := s.fvarSet.insert fvarId, .. s }
| Expr.fvar fvarId _ => fun s => { s with fvarSet := s.fvarSet.insert fvarId }
| _ => id
end CollectFVars

6
stage0/src/Init/Lean/Util/CollectLevelParams.lean
View file

@ -22,20 +22,20 @@ abbrev Visitor := State → State
@[inline] def visitLevel (f : Level → Visitor) (u : Level) : Visitor :=
fun s =>
if !u.hasParam || s.visitedLevel.contains u then s
else f u { visitedLevel := s.visitedLevel.insert u, .. s }
else f u { s with visitedLevel := s.visitedLevel.insert u }
partial def collect : Level → Visitor
| Level.succ v _ => visitLevel collect v
| Level.max u v _ => visitLevel collect v ∘ visitLevel collect u
| Level.imax u v _ => visitLevel collect v ∘ visitLevel collect u
| Level.param n _ => fun s => { params := s.params.push n, .. s }
| Level.param n _ => fun s => { s with params := s.params.push n }
| _ => id
@[inline] def visitExpr (f : Expr → Visitor) (e : Expr) : Visitor :=
fun s =>
if !e.hasLevelParam then s
else if s.visitedExpr.contains e then s
else f e { visitedExpr := s.visitedExpr.insert e, .. s }
else f e { s with visitedExpr := s.visitedExpr.insert e }
partial def main : Expr → Visitor
| Expr.proj _ _ s _ => visitExpr main s

4
stage0/src/Init/Lean/Util/CollectMVars.lean
View file

@ -21,7 +21,7 @@ abbrev Visitor := State → State
@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor :=
fun s =>
if !e.hasMVar || s.visitedExpr.contains e then s
else f e { visitedExpr := s.visitedExpr.insert e, .. s }
else f e { s with visitedExpr := s.visitedExpr.insert e }
partial def main : Expr → Visitor
| Expr.proj _ _ e _ => visit main e
@ -30,7 +30,7 @@ partial def main : Expr → Visitor
| Expr.letE _ t v b _ => visit main b ∘ visit main v ∘ visit main t
| Expr.app f a _ => visit main a ∘ visit main f
| Expr.mdata _ b _ => visit main b
| Expr.mvar mvarId _ => fun s => { result := s.result.push mvarId, .. s }
| Expr.mvar mvarId _ => fun s => { s with result := s.result.push mvarId }
| _ => id
end CollectMVars

4
stage0/src/Init/Lean/Util/FoldConsts.lean
View file

@ -27,7 +27,7 @@ let i := h % size;
let k := s.visitedTerms.uget i lcProof;
if ptrAddrUnsafe k == h then pure true
else do
modify $ fun s => { visitedTerms := s.visitedTerms.uset i e lcProof, .. s };
modify $ fun s => { s with visitedTerms := s.visitedTerms.uset i e lcProof };
pure false
@[specialize] unsafe partial def fold {α : Type} (f : Name → α → α) (size : USize) : Expr → α → FoldM α
@ -43,7 +43,7 @@ else do
s ← get;
if s.visitedConsts.contains c then pure acc
else do
modify $ fun s => { visitedConsts := s.visitedConsts.insert c, .. s };
modify $ fun s => { s with visitedConsts := s.visitedConsts.insert c };
pure $ f c acc
| _ => pure acc

4
stage0/src/Init/Lean/Util/MonadCache.lean
View file

@ -65,7 +65,7 @@ namespace WithHashMapCache
s ← get; pure s.cache
@[inline] def modifyCache {α β σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : StateM (WithHashMapCache α β σ) Unit :=
modify $ fun s => { cache := f s.cache, .. s }
modify $ fun s => { s with cache := f s.cache }
instance stateAdapter (α β σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (StateM (WithHashMapCache α β σ)) :=
{ getCache := WithHashMapCache.getCache,
@ -75,7 +75,7 @@ instance stateAdapter (α β σ : Type) [HasBeq α] [Hashable α] : MonadHashMap
s ← get; pure s.cache
@[inline] def modifyCacheE {α β ε σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : EStateM ε (WithHashMapCache α β σ) Unit :=
modify $ fun s => { cache := f s.cache, .. s }
modify $ fun s => { s with cache := f s.cache }
instance estateAdapter (α β ε σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (EStateM ε (WithHashMapCache α β σ)) :=
{ getCache := WithHashMapCache.getCacheE,

6
stage0/src/Init/Lean/Util/Trace.lean
View file

@ -148,17 +148,17 @@ else checkTraceOptionM cls
@[inline] def enableTracing (b : Bool) : m Bool := do
s ← getTraceState;
let oldEnabled := s.enabled;
modifyTraceState $ fun s => { enabled := b, .. s };
modifyTraceState $ fun s => { s with enabled := b };
pure oldEnabled
@[inline] def getTraces : m (PersistentArray MessageData) := do
s ← getTraceState; pure s.traces
@[inline] def modifyTraces (f : PersistentArray MessageData → PersistentArray MessageData) : m Unit :=
modifyTraceState $ fun s => { traces := f s.traces, .. s }
modifyTraceState $ fun s => { s with traces := f s.traces }
@[inline] def setTrace (f : PersistentArray MessageData → PersistentArray MessageData) : m Unit :=
modifyTraceState $ fun s => { traces := f s.traces, .. s }
modifyTraceState $ fun s => { s with traces := f s.traces }
@[inline] def setTraceState (s : TraceState) : m Unit :=
modifyTraceState $ fun _ => s

8
stage0/src/Init/LeanInit.lean
View file

@ -125,11 +125,11 @@ instance : Inhabited NameGenerator := ⟨{}⟩
mkNameNum g.namePrefix g.idx
@[inline] def next (g : NameGenerator) : NameGenerator :=
{ idx := g.idx + 1, .. g }
{ g with idx := g.idx + 1 }
@[inline] def mkChild (g : NameGenerator) : NameGenerator × NameGenerator :=
({ namePrefix := mkNameNum g.namePrefix g.idx, idx := 1 },
{ idx := g.idx + 1, .. g })
{ g with idx := g.idx + 1 })
end NameGenerator
@ -363,7 +363,7 @@ if n.hasMacroScopes then
if view.mainModule == mainModule then
mkNameNum n scp
else
{ imported := view.scopes.foldl mkNameNum (view.imported ++ view.mainModule), mainModule := mainModule, scopes := [scp], .. view }.review
{ view with imported := view.scopes.foldl mkNameNum (view.imported ++ view.mainModule), mainModule := mainModule, scopes := [scp] }.review
else
mkNameNum (mkNameStr (mkNameStr n "_@" ++ mainModule) "_hyg") scp
@ -398,7 +398,7 @@ throw $ Macro.Exception.error ref msg
@[inline] protected def Macro.withFreshMacroScope {α} (x : MacroM α) : MacroM α := do
fresh ← modifyGet (fun s => (s, s+1));
adaptReader (fun (ctx : Macro.Context) => { currMacroScope := fresh, .. ctx }) x
adaptReader (fun (ctx : Macro.Context) => { ctx with currMacroScope := fresh }) x
instance MacroM.monadQuotation : MonadQuotation MacroM :=
{ getCurrMacroScope := fun ctx => pure ctx.currMacroScope,

1891
stage0/stdlib/Init/Lean/Meta/SynthInstance.c
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Init/Lean/MetavarContext.c
View file

@ -2270,7 +2270,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_MetavarContext_getDecl___closed__1;
x_2 = lean_unsigned_to_nat(328u);
x_2 = lean_unsigned_to_nat(327u);
x_3 = lean_unsigned_to_nat(15u);
x_4 = l_Lean_MetavarContext_getDecl___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -2724,7 +2724,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_MetavarContext_getDecl___closed__1;
x_2 = lean_unsigned_to_nat(344u);
x_2 = lean_unsigned_to_nat(343u);
x_3 = lean_unsigned_to_nat(12u);
x_4 = l_Lean_MetavarContext_getDecl___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -2803,7 +2803,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_MetavarContext_getDecl___closed__1;
x_2 = lean_unsigned_to_nat(353u);
x_2 = lean_unsigned_to_nat(352u);
x_3 = lean_unsigned_to_nat(19u);
x_4 = l_Lean_MetavarContext_getDecl___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6292,7 +6292,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_MetavarContext_getDecl___closed__1;
x_2 = lean_unsigned_to_nat(402u);
x_2 = lean_unsigned_to_nat(401u);
x_3 = lean_unsigned_to_nat(12u);
x_4 = l_Lean_MetavarContext_isLevelAssignable___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);