diff --git a/stage0/src/Init/Control/Option.lean b/stage0/src/Init/Control/Option.lean index f0733d061f..3aeda41ce1 100644 --- a/stage0/src/Init/Control/Option.lean +++ b/stage0/src/Init/Control/Option.lean @@ -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 α)) diff --git a/stage0/src/Init/Control/Reader.lean b/stage0/src/Init/Control/Reader.lean index 2ad3ea08fd..887c71ee13 100644 --- a/stage0/src/Init/Control/Reader.lean +++ b/stage0/src/Init/Control/Reader.lean @@ -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, diff --git a/stage0/src/Init/Control/State.lean b/stage0/src/Init/Control/State.lean index 47bd5c8c64..16154f491a 100644 --- a/stage0/src/Init/Control/State.lean +++ b/stage0/src/Init/Control/State.lean @@ -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) diff --git a/stage0/src/Init/Data/BinomialHeap/Basic.lean b/stage0/src/Init/Data/BinomialHeap/Basic.lean index cb24558ce3..a658741e23 100644 --- a/stage0/src/Init/Data/BinomialHeap/Basic.lean +++ b/stage0/src/Init/Data/BinomialHeap/Basic.lean @@ -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 diff --git a/stage0/src/Init/Data/List/Instances.lean b/stage0/src/Init/Data/List/Instances.lean index 7a92dd1b9f..6b190d5c08 100644 --- a/stage0/src/Init/Data/List/Instances.lean +++ b/stage0/src/Init/Data/List/Instances.lean @@ -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 } diff --git a/stage0/src/Init/Data/Option/Basic.lean b/stage0/src/Init/Data/Option/Basic.lean index 5a9c67694b..1209ab2765 100644 --- a/stage0/src/Init/Data/Option/Basic.lean +++ b/stage0/src/Init/Data/Option/Basic.lean @@ -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 diff --git a/stage0/src/Init/Data/PersistentArray/Basic.lean b/stage0/src/Init/Data/PersistentArray/Basic.lean index 0b42406758..435e05f079 100644 --- a/stage0/src/Init/Data/PersistentArray/Basic.lean +++ b/stage0/src/Init/Data/PersistentArray/Basic.lean @@ -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 diff --git a/stage0/src/Init/Data/PersistentHashMap/Basic.lean b/stage0/src/Init/Data/PersistentHashMap/Basic.lean index d14fb72312..69ba4d189d 100644 --- a/stage0/src/Init/Data/PersistentHashMap/Basic.lean +++ b/stage0/src/Init/Data/PersistentHashMap/Basic.lean @@ -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 diff --git a/stage0/src/Init/Data/Queue/Basic.lean b/stage0/src/Init/Data/Queue/Basic.lean index 3d829ec5a7..5faa6573f6 100644 --- a/stage0/src/Init/Data/Queue/Basic.lean +++ b/stage0/src/Init/Data/Queue/Basic.lean @@ -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 diff --git a/stage0/src/Init/Data/Stack/Basic.lean b/stage0/src/Init/Data/Stack/Basic.lean index 9fd29a238c..2e217d5870 100644 --- a/stage0/src/Init/Data/Stack/Basic.lean +++ b/stage0/src/Init/Data/Stack/Basic.lean @@ -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 diff --git a/stage0/src/Init/Lean/Attributes.lean b/stage0/src/Init/Lean/Attributes.lean index 0df48e33b6..06b99ea8e3 100644 --- a/stage0/src/Init/Lean/Attributes.lean +++ b/stage0/src/Init/Lean/Attributes.lean @@ -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 { diff --git a/stage0/src/Init/Lean/Class.lean b/stage0/src/Init/Lean/Class.lean index a7e5d0aa7c..f5d8e9f7c6 100644 --- a/stage0/src/Init/Lean/Class.lean +++ b/stage0/src/Init/Lean/Class.lean @@ -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⟩ diff --git a/stage0/src/Init/Lean/Compiler/IR/Borrow.lean b/stage0/src/Init/Lean/Compiler/IR/Borrow.lean index c2e5ed5b14..baa8c9e602 100644 --- a/stage0/src/Init/Lean/Compiler/IR/Borrow.lean +++ b/stage0/src/Init/Lean/Compiler/IR/Borrow.lean @@ -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; diff --git a/stage0/src/Init/Lean/Compiler/IR/Boxing.lean b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean index 0ff72c058a..6365424f76 100644 --- a/stage0/src/Init/Lean/Compiler/IR/Boxing.lean +++ b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean @@ -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; diff --git a/stage0/src/Init/Lean/Compiler/IR/Checker.lean b/stage0/src/Init/Lean/Compiler/IR/Checker.lean index ac0f2d6f94..9a763aa92d 100644 --- a/stage0/src/Init/Lean/Compiler/IR/Checker.lean +++ b/stage0/src/Init/Lean/Compiler/IR/Checker.lean @@ -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 diff --git a/stage0/src/Init/Lean/Compiler/IR/CompilerM.lean b/stage0/src/Init/Lean/Compiler/IR/CompilerM.lean index a9437865b0..1ff594753c 100644 --- a/stage0/src/Init/Lean/Compiler/IR/CompilerM.lean +++ b/stage0/src/Init/Lean/Compiler/IR/CompilerM.lean @@ -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 diff --git a/stage0/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean b/stage0/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean index 1e73e0d09a..357d3005ff 100644 --- a/stage0/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/stage0/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean @@ -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 diff --git a/stage0/src/Init/Lean/Compiler/IR/EmitC.lean b/stage0/src/Init/Lean/Compiler/IR/EmitC.lean index df805a34f8..8011138e6a 100644 --- a/stage0/src/Init/Lean/Compiler/IR/EmitC.lean +++ b/stage0/src/Init/Lean/Compiler/IR/EmitC.lean @@ -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 () diff --git a/stage0/src/Init/Lean/Compiler/IR/NormIds.lean b/stage0/src/Init/Lean/Compiler/IR/NormIds.lean index 8ca07824ef..f2d2cfb435 100644 --- a/stage0/src/Init/Lean/Compiler/IR/NormIds.lean +++ b/stage0/src/Init/Lean/Compiler/IR/NormIds.lean @@ -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 α) := diff --git a/stage0/src/Init/Lean/Compiler/IR/RC.lean b/stage0/src/Init/Lean/Compiler/IR/RC.lean index 51ae1cb0ac..c0160eb030 100644 --- a/stage0/src/Init/Lean/Compiler/IR/RC.lean +++ b/stage0/src/Init/Lean/Compiler/IR/RC.lean @@ -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 => diff --git a/stage0/src/Init/Lean/Compiler/Specialize.lean b/stage0/src/Init/Lean/Compiler/Specialize.lean index b026c9eb67..0a12403349 100644 --- a/stage0/src/Init/Lean/Compiler/Specialize.lean +++ b/stage0/src/Init/Lean/Compiler/Specialize.lean @@ -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⟩ diff --git a/stage0/src/Init/Lean/Data/SMap.lean b/stage0/src/Init/Lean/Data/SMap.lean index 0d9f3b4aa8..8bfc7b7393 100644 --- a/stage0/src/Init/Lean/Data/SMap.lean +++ b/stage0/src/Init/Lean/Data/SMap.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/App.lean b/stage0/src/Init/Lean/Elab/App.lean index c224837449..e8598022d4 100644 --- a/stage0/src/Init/Lean/Elab/App.lean +++ b/stage0/src/Init/Lean/Elab/App.lean @@ -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 () | _ => diff --git a/stage0/src/Init/Lean/Elab/Binders.lean b/stage0/src/Init/Lean/Elab/Binders.lean index 5f44fc0451..b2f28050f3 100644 --- a/stage0/src/Init/Lean/Elab/Binders.lean +++ b/stage0/src/Init/Lean/Elab/Binders.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Command.lean b/stage0/src/Init/Lean/Elab/Command.lean index 2f784b319e..f817013cd6 100644 --- a/stage0/src/Init/Lean/Elab/Command.lean +++ b/stage0/src/Init/Lean/Elab/Command.lean @@ -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" /-- diff --git a/stage0/src/Init/Lean/Elab/DeclModifiers.lean b/stage0/src/Init/Lean/Elab/DeclModifiers.lean index 6f2c8a021c..cb5b01666d 100644 --- a/stage0/src/Init/Lean/Elab/DeclModifiers.lean +++ b/stage0/src/Init/Lean/Elab/DeclModifiers.lean @@ -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 => diff --git a/stage0/src/Init/Lean/Elab/Frontend.lean b/stage0/src/Init/Lean/Elab/Frontend.lean index a3ecc36393..52f54ea512 100644 --- a/stage0/src/Init/Lean/Elab/Frontend.lean +++ b/stage0/src/Init/Lean/Elab/Frontend.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Level.lean b/stage0/src/Init/Lean/Elab/Level.lean index 611da2e1c8..23cba79426 100644 --- a/stage0/src/Init/Lean/Elab/Level.lean +++ b/stage0/src/Init/Lean/Elab/Level.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Quotation.lean b/stage0/src/Init/Lean/Elab/Quotation.lean index fbd0bbddb5..9116ff1583 100644 --- a/stage0/src/Init/Lean/Elab/Quotation.lean +++ b/stage0/src/Init/Lean/Elab/Quotation.lean @@ -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 ""); 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 => diff --git a/stage0/src/Init/Lean/Elab/ResolveName.lean b/stage0/src/Init/Lean/Elab/ResolveName.lean index 9408588fe8..bf6208a7b6 100644 --- a/stage0/src/Init/Lean/Elab/ResolveName.lean +++ b/stage0/src/Init/Lean/Elab/ResolveName.lean @@ -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) | [] => diff --git a/stage0/src/Init/Lean/Elab/StructInst.lean b/stage0/src/Init/Lean/Elab/StructInst.lean index 8541dc7c28..0bb50105c5 100644 --- a/stage0/src/Init/Lean/Elab/StructInst.lean +++ b/stage0/src/Init/Lean/Elab/StructInst.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Syntax.lean b/stage0/src/Init/Lean/Elab/Syntax.lean index 28d04bb589..a539d08bf6 100644 --- a/stage0/src/Init/Lean/Elab/Syntax.lean +++ b/stage0/src/Init/Lean/Elab/Syntax.lean @@ -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; diff --git a/stage0/src/Init/Lean/Elab/SyntheticMVars.lean b/stage0/src/Init/Lean/Elab/SyntheticMVars.lean index b6892360e9..bb1fccdc49 100644 --- a/stage0/src/Init/Lean/Elab/SyntheticMVars.lean +++ b/stage0/src/Init/Lean/Elab/SyntheticMVars.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Tactic/Basic.lean b/stage0/src/Init/Lean/Elab/Tactic/Basic.lean index 5682cc0aea..0df895aefb 100644 --- a/stage0/src/Init/Lean/Elab/Tactic/Basic.lean +++ b/stage0/src/Init/Lean/Elab/Tactic/Basic.lean @@ -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; diff --git a/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean b/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean index d6bf27ac27..38ed5d4e80 100644 --- a/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean +++ b/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean @@ -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 diff --git a/stage0/src/Init/Lean/Elab/Term.lean b/stage0/src/Init/Lean/Elab/Term.lean index e39fe0994a..ac9390c65d 100644 --- a/stage0/src/Init/Lean/Elab/Term.lean +++ b/stage0/src/Init/Lean/Elab/Term.lean @@ -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 `(` `:` `)` -/ 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 diff --git a/stage0/src/Init/Lean/Environment.lean b/stage0/src/Init/Lean/Environment.lean index 8e08a933bc..dcc141231e 100644 --- a/stage0/src/Init/Lean/Environment.lean +++ b/stage0/src/Init/Lean/Environment.lean @@ -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 diff --git a/stage0/src/Init/Lean/Message.lean b/stage0/src/Init/Lean/Message.lean index fbf056bb6a..a5fa641943 100644 --- a/stage0/src/Init/Lean/Message.lean +++ b/stage0/src/Init/Lean/Message.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/AbstractMVars.lean b/stage0/src/Init/Lean/Meta/AbstractMVars.lean index cab8dd8a2a..a726fd5ca3 100644 --- a/stage0/src/Init/Lean/Meta/AbstractMVars.lean +++ b/stage0/src/Init/Lean/Meta/AbstractMVars.lean @@ -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 } diff --git a/stage0/src/Init/Lean/Meta/Basic.lean b/stage0/src/Init/Lean/Meta/Basic.lean index 61883e19f1..5024cf1b28 100644 --- a/stage0/src/Init/Lean/Meta/Basic.lean +++ b/stage0/src/Init/Lean/Meta/Basic.lean @@ -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. diff --git a/stage0/src/Init/Lean/Meta/ExprDefEq.lean b/stage0/src/Init/Lean/Meta/ExprDefEq.lean index 3b150ea26c..bf9c3663d7 100644 --- a/stage0/src/Init/Lean/Meta/ExprDefEq.lean +++ b/stage0/src/Init/Lean/Meta/ExprDefEq.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/FunInfo.lean b/stage0/src/Init/Lean/Meta/FunInfo.lean index 4797ce0872..4dfb02e78d 100644 --- a/stage0/src/Init/Lean/Meta/FunInfo.lean +++ b/stage0/src/Init/Lean/Meta/FunInfo.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean index b3c5bccde1..86fbfcf7f8 100644 --- a/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean +++ b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean @@ -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) diff --git a/stage0/src/Init/Lean/Meta/InferType.lean b/stage0/src/Init/Lean/Meta/InferType.lean index 00d1147c4a..f166cb0b19 100644 --- a/stage0/src/Init/Lean/Meta/InferType.lean +++ b/stage0/src/Init/Lean/Meta/InferType.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/LevelDefEq.lean b/stage0/src/Init/Lean/Meta/LevelDefEq.lean index 7f17b569f5..cc0037bbfe 100644 --- a/stage0/src/Init/Lean/Meta/LevelDefEq.lean +++ b/stage0/src/Init/Lean/Meta/LevelDefEq.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/SynthInstance.lean b/stage0/src/Init/Lean/Meta/SynthInstance.lean index 8b94f281c3..7d965394cb 100644 --- a/stage0/src/Init/Lean/Meta/SynthInstance.lean +++ b/stage0/src/Init/Lean/Meta/SynthInstance.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/Tactic/Cases.lean b/stage0/src/Init/Lean/Meta/Tactic/Cases.lean index 42508752d7..fb37d6eb2f 100644 --- a/stage0/src/Init/Lean/Meta/Tactic/Cases.lean +++ b/stage0/src/Init/Lean/Meta/Tactic/Cases.lean @@ -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; diff --git a/stage0/src/Init/Lean/Meta/Tactic/Intro.lean b/stage0/src/Init/Lean/Meta/Tactic/Intro.lean index e0397c3385..973dba8368 100644 --- a/stage0/src/Init/Lean/Meta/Tactic/Intro.lean +++ b/stage0/src/Init/Lean/Meta/Tactic/Intro.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/Tactic/Util.lean b/stage0/src/Init/Lean/Meta/Tactic/Util.lean index 404f93afe4..3ae2b1faff 100644 --- a/stage0/src/Init/Lean/Meta/Tactic/Util.lean +++ b/stage0/src/Init/Lean/Meta/Tactic/Util.lean @@ -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 diff --git a/stage0/src/Init/Lean/Meta/WHNF.lean b/stage0/src/Init/Lean/Meta/WHNF.lean index 8d79fc56e6..fb590464f5 100644 --- a/stage0/src/Init/Lean/Meta/WHNF.lean +++ b/stage0/src/Init/Lean/Meta/WHNF.lean @@ -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 diff --git a/stage0/src/Init/Lean/MetavarContext.lean b/stage0/src/Init/Lean/MetavarContext.lean index e4005dbcb4..5137709b81 100644 --- a/stage0/src/Init/Lean/MetavarContext.lean +++ b/stage0/src/Init/Lean/MetavarContext.lean @@ -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 := diff --git a/stage0/src/Init/Lean/Parser/Module.lean b/stage0/src/Init/Lean/Parser/Module.lean index d8924f4180..9fd0b1ac9f 100644 --- a/stage0/src/Init/Lean/Parser/Module.lean +++ b/stage0/src/Init/Lean/Parser/Module.lean @@ -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 diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean index c28371f5f3..fd9d2252e7 100644 --- a/stage0/src/Init/Lean/Parser/Parser.lean +++ b/stage0/src/Init/Lean/Parser/Parser.lean @@ -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) diff --git a/stage0/src/Init/Lean/Parser/Transform.lean b/stage0/src/Init/Lean/Parser/Transform.lean index 275ed1aaa2..126d39cc8d 100644 --- a/stage0/src/Init/Lean/Parser/Transform.lean +++ b/stage0/src/Init/Lean/Parser/Transform.lean @@ -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) diff --git a/stage0/src/Init/Lean/Scopes.lean b/stage0/src/Init/Lean/Scopes.lean index ca2cda91a4..1dcb04f3b6 100644 --- a/stage0/src/Init/Lean/Scopes.lean +++ b/stage0/src/Init/Lean/Scopes.lean @@ -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 diff --git a/stage0/src/Init/Lean/Syntax.lean b/stage0/src/Init/Lean/Syntax.lean index 1ff8e957b5..e9e6b688e6 100644 --- a/stage0/src/Init/Lean/Syntax.lean +++ b/stage0/src/Init/Lean/Syntax.lean @@ -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 diff --git a/stage0/src/Init/Lean/Util/Closure.lean b/stage0/src/Init/Lean/Util/Closure.lean index 830a5712d6..0e51a8183f 100644 --- a/stage0/src/Init/Lean/Util/Closure.lean +++ b/stage0/src/Init/Lean/Util/Closure.lean @@ -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; diff --git a/stage0/src/Init/Lean/Util/CollectFVars.lean b/stage0/src/Init/Lean/Util/CollectFVars.lean index 4bb2b88e9f..040bf9a2c9 100644 --- a/stage0/src/Init/Lean/Util/CollectFVars.lean +++ b/stage0/src/Init/Lean/Util/CollectFVars.lean @@ -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 diff --git a/stage0/src/Init/Lean/Util/CollectLevelParams.lean b/stage0/src/Init/Lean/Util/CollectLevelParams.lean index 737d89453a..a3e641bbc3 100644 --- a/stage0/src/Init/Lean/Util/CollectLevelParams.lean +++ b/stage0/src/Init/Lean/Util/CollectLevelParams.lean @@ -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 diff --git a/stage0/src/Init/Lean/Util/CollectMVars.lean b/stage0/src/Init/Lean/Util/CollectMVars.lean index 9a41a8af1a..b9c6211a69 100644 --- a/stage0/src/Init/Lean/Util/CollectMVars.lean +++ b/stage0/src/Init/Lean/Util/CollectMVars.lean @@ -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 diff --git a/stage0/src/Init/Lean/Util/FoldConsts.lean b/stage0/src/Init/Lean/Util/FoldConsts.lean index d45a9fbf3a..a9d0c21961 100644 --- a/stage0/src/Init/Lean/Util/FoldConsts.lean +++ b/stage0/src/Init/Lean/Util/FoldConsts.lean @@ -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 diff --git a/stage0/src/Init/Lean/Util/MonadCache.lean b/stage0/src/Init/Lean/Util/MonadCache.lean index 0b5df73ae3..9db30b4765 100644 --- a/stage0/src/Init/Lean/Util/MonadCache.lean +++ b/stage0/src/Init/Lean/Util/MonadCache.lean @@ -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, diff --git a/stage0/src/Init/Lean/Util/Trace.lean b/stage0/src/Init/Lean/Util/Trace.lean index b865252997..bd6cef8e01 100644 --- a/stage0/src/Init/Lean/Util/Trace.lean +++ b/stage0/src/Init/Lean/Util/Trace.lean @@ -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 diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean index e28600c9b3..e9766bf9f7 100644 --- a/stage0/src/Init/LeanInit.lean +++ b/stage0/src/Init/LeanInit.lean @@ -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, diff --git a/stage0/stdlib/Init/Lean/Meta/SynthInstance.c b/stage0/stdlib/Init/Lean/Meta/SynthInstance.c index 5fbd31bb5f..b0a6f2898a 100644 --- a/stage0/stdlib/Init/Lean/Meta/SynthInstance.c +++ b/stage0/stdlib/Init/Lean/Meta/SynthInstance.c @@ -18788,36 +18788,36 @@ return x_2; lean_object* l_Lean_Meta_SynthInstance_main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -uint8_t x_5; lean_object* x_6; lean_object* x_360; uint8_t x_361; -x_360 = lean_ctor_get(x_4, 4); -lean_inc(x_360); -x_361 = lean_ctor_get_uint8(x_360, sizeof(void*)*1); -lean_dec(x_360); -if (x_361 == 0) +uint8_t x_5; lean_object* x_6; lean_object* x_266; uint8_t x_267; +x_266 = lean_ctor_get(x_4, 4); +lean_inc(x_266); +x_267 = lean_ctor_get_uint8(x_266, sizeof(void*)*1); +lean_dec(x_266); +if (x_267 == 0) { -uint8_t x_362; -x_362 = 0; -x_5 = x_362; +uint8_t x_268; +x_268 = 0; +x_5 = x_268; x_6 = x_4; -goto block_359; +goto block_265; } else { -lean_object* x_363; lean_object* x_364; lean_object* x_365; lean_object* x_366; uint8_t x_367; -x_363 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_364 = l___private_Init_Lean_Util_Trace_5__checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___main___spec__2(x_363, x_3, x_4); -x_365 = lean_ctor_get(x_364, 0); -lean_inc(x_365); -x_366 = lean_ctor_get(x_364, 1); -lean_inc(x_366); -lean_dec(x_364); -x_367 = lean_unbox(x_365); -lean_dec(x_365); -x_5 = x_367; -x_6 = x_366; -goto block_359; +lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; uint8_t x_273; +x_269 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; +x_270 = l___private_Init_Lean_Util_Trace_5__checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___main___spec__2(x_269, x_3, x_4); +x_271 = lean_ctor_get(x_270, 0); +lean_inc(x_271); +x_272 = lean_ctor_get(x_270, 1); +lean_inc(x_272); +lean_dec(x_270); +x_273 = lean_unbox(x_271); +lean_dec(x_271); +x_5 = x_273; +x_6 = x_272; +goto block_265; } -block_359: +block_265: { if (x_5 == 0) { @@ -18830,7 +18830,7 @@ x_8 = lean_ctor_get(x_6, 4); x_9 = !lean_is_exclusive(x_8); if (x_9 == 0) { -uint8_t x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38; +uint8_t x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; x_10 = lean_ctor_get_uint8(x_8, sizeof(void*)*1); x_11 = 0; lean_ctor_set_uint8(x_8, sizeof(void*)*1, x_11); @@ -18839,374 +18839,212 @@ x_34 = 0; lean_inc(x_3); lean_inc(x_1); x_35 = l_Lean_Meta_mkFreshExprMVar(x_1, x_33, x_34, x_3, x_6); -x_36 = lean_ctor_get(x_35, 1); +x_36 = lean_ctor_get(x_35, 0); lean_inc(x_36); -x_37 = lean_ctor_get(x_35, 0); +x_37 = lean_ctor_get(x_35, 1); lean_inc(x_37); lean_dec(x_35); -x_38 = !lean_is_exclusive(x_36); -if (x_38 == 0) -{ -lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; -x_39 = lean_ctor_get(x_36, 1); -lean_inc(x_39); -x_40 = l_Lean_Meta_SynthInstance_mkTableKey(x_39, x_1); -lean_inc(x_39); -x_41 = lean_box(0); -x_42 = l_Array_empty___closed__1; -x_43 = l_Lean_Meta_SynthInstance_main___closed__1; -x_44 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_44, 0, x_36); -lean_ctor_set(x_44, 1, x_41); -lean_ctor_set(x_44, 2, x_42); -lean_ctor_set(x_44, 3, x_42); -lean_ctor_set(x_44, 4, x_43); -x_45 = lean_box(1); +x_38 = lean_ctor_get(x_37, 1); +lean_inc(x_38); +lean_inc(x_38); +x_39 = l_Lean_Meta_SynthInstance_mkTableKey(x_38, x_1); +x_40 = lean_box(0); +x_41 = l_Array_empty___closed__1; +x_42 = l_Lean_Meta_SynthInstance_main___closed__1; +x_43 = lean_alloc_ctor(0, 5, 0); +lean_ctor_set(x_43, 0, x_37); +lean_ctor_set(x_43, 1, x_40); +lean_ctor_set(x_43, 2, x_41); +lean_ctor_set(x_43, 3, x_41); +lean_ctor_set(x_43, 4, x_42); +x_44 = lean_box(1); lean_inc(x_3); -x_46 = l_Lean_Meta_SynthInstance_newSubgoal(x_39, x_40, x_37, x_45, x_3, x_44); -if (lean_obj_tag(x_46) == 0) +x_45 = l_Lean_Meta_SynthInstance_newSubgoal(x_38, x_39, x_36, x_44, x_3, x_43); +if (lean_obj_tag(x_45) == 0) { -lean_object* x_47; lean_object* x_48; -x_47 = lean_ctor_get(x_46, 1); -lean_inc(x_47); -lean_dec(x_46); -x_48 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_47); -if (lean_obj_tag(x_48) == 0) +lean_object* x_46; lean_object* x_47; +x_46 = lean_ctor_get(x_45, 1); +lean_inc(x_46); +lean_dec(x_45); +x_47 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_46); +if (lean_obj_tag(x_47) == 0) { -lean_object* x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52; -x_49 = lean_ctor_get(x_48, 1); +lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51; +x_48 = lean_ctor_get(x_47, 1); +lean_inc(x_48); +x_49 = lean_ctor_get(x_48, 0); lean_inc(x_49); -x_50 = lean_ctor_get(x_49, 0); +lean_dec(x_48); +x_50 = lean_ctor_get(x_49, 4); lean_inc(x_50); -lean_dec(x_49); -x_51 = lean_ctor_get(x_50, 4); -lean_inc(x_51); -x_52 = !lean_is_exclusive(x_48); -if (x_52 == 0) +x_51 = !lean_is_exclusive(x_47); +if (x_51 == 0) { -lean_object* x_53; uint8_t x_54; -x_53 = lean_ctor_get(x_48, 1); -lean_dec(x_53); -x_54 = !lean_is_exclusive(x_50); -if (x_54 == 0) +lean_object* x_52; uint8_t x_53; +x_52 = lean_ctor_get(x_47, 1); +lean_dec(x_52); +x_53 = !lean_is_exclusive(x_49); +if (x_53 == 0) { -lean_object* x_55; uint8_t x_56; -x_55 = lean_ctor_get(x_50, 4); -lean_dec(x_55); -x_56 = !lean_is_exclusive(x_51); -if (x_56 == 0) +lean_object* x_54; uint8_t x_55; +x_54 = lean_ctor_get(x_49, 4); +lean_dec(x_54); +x_55 = !lean_is_exclusive(x_50); +if (x_55 == 0) { -lean_ctor_set_uint8(x_51, sizeof(void*)*1, x_10); -lean_ctor_set(x_48, 1, x_50); -return x_48; +lean_ctor_set_uint8(x_50, sizeof(void*)*1, x_10); +lean_ctor_set(x_47, 1, x_49); +return x_47; } else { -lean_object* x_57; lean_object* x_58; -x_57 = lean_ctor_get(x_51, 0); -lean_inc(x_57); -lean_dec(x_51); -x_58 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_58, 0, x_57); -lean_ctor_set_uint8(x_58, sizeof(void*)*1, x_10); -lean_ctor_set(x_50, 4, x_58); -lean_ctor_set(x_48, 1, x_50); -return x_48; +lean_object* x_56; lean_object* x_57; +x_56 = lean_ctor_get(x_50, 0); +lean_inc(x_56); +lean_dec(x_50); +x_57 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_57, 0, x_56); +lean_ctor_set_uint8(x_57, sizeof(void*)*1, x_10); +lean_ctor_set(x_49, 4, x_57); +lean_ctor_set(x_47, 1, x_49); +return x_47; } } else { -lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; -x_59 = lean_ctor_get(x_50, 0); -x_60 = lean_ctor_get(x_50, 1); -x_61 = lean_ctor_get(x_50, 2); -x_62 = lean_ctor_get(x_50, 3); -x_63 = lean_ctor_get(x_50, 5); -lean_inc(x_63); +lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; +x_58 = lean_ctor_get(x_49, 0); +x_59 = lean_ctor_get(x_49, 1); +x_60 = lean_ctor_get(x_49, 2); +x_61 = lean_ctor_get(x_49, 3); +x_62 = lean_ctor_get(x_49, 5); lean_inc(x_62); lean_inc(x_61); lean_inc(x_60); lean_inc(x_59); -lean_dec(x_50); -x_64 = lean_ctor_get(x_51, 0); -lean_inc(x_64); -if (lean_is_exclusive(x_51)) { - lean_ctor_release(x_51, 0); - x_65 = x_51; -} else { - lean_dec_ref(x_51); - x_65 = lean_box(0); -} -if (lean_is_scalar(x_65)) { - x_66 = lean_alloc_ctor(0, 1, 1); -} else { - x_66 = x_65; -} -lean_ctor_set(x_66, 0, x_64); -lean_ctor_set_uint8(x_66, sizeof(void*)*1, x_10); -x_67 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_67, 0, x_59); -lean_ctor_set(x_67, 1, x_60); -lean_ctor_set(x_67, 2, x_61); -lean_ctor_set(x_67, 3, x_62); -lean_ctor_set(x_67, 4, x_66); -lean_ctor_set(x_67, 5, x_63); -lean_ctor_set(x_48, 1, x_67); -return x_48; -} -} -else -{ -lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; -x_68 = lean_ctor_get(x_48, 0); -lean_inc(x_68); -lean_dec(x_48); -x_69 = lean_ctor_get(x_50, 0); -lean_inc(x_69); -x_70 = lean_ctor_get(x_50, 1); -lean_inc(x_70); -x_71 = lean_ctor_get(x_50, 2); -lean_inc(x_71); -x_72 = lean_ctor_get(x_50, 3); -lean_inc(x_72); -x_73 = lean_ctor_get(x_50, 5); -lean_inc(x_73); +lean_inc(x_58); +lean_dec(x_49); +x_63 = lean_ctor_get(x_50, 0); +lean_inc(x_63); if (lean_is_exclusive(x_50)) { lean_ctor_release(x_50, 0); - lean_ctor_release(x_50, 1); - lean_ctor_release(x_50, 2); - lean_ctor_release(x_50, 3); - lean_ctor_release(x_50, 4); - lean_ctor_release(x_50, 5); - x_74 = x_50; + x_64 = x_50; } else { lean_dec_ref(x_50); - x_74 = lean_box(0); + x_64 = lean_box(0); } -x_75 = lean_ctor_get(x_51, 0); -lean_inc(x_75); -if (lean_is_exclusive(x_51)) { - lean_ctor_release(x_51, 0); - x_76 = x_51; +if (lean_is_scalar(x_64)) { + x_65 = lean_alloc_ctor(0, 1, 1); } else { - lean_dec_ref(x_51); - x_76 = lean_box(0); + x_65 = x_64; } -if (lean_is_scalar(x_76)) { - x_77 = lean_alloc_ctor(0, 1, 1); -} else { - x_77 = x_76; -} -lean_ctor_set(x_77, 0, x_75); -lean_ctor_set_uint8(x_77, sizeof(void*)*1, x_10); -if (lean_is_scalar(x_74)) { - x_78 = lean_alloc_ctor(0, 6, 0); -} else { - x_78 = x_74; -} -lean_ctor_set(x_78, 0, x_69); -lean_ctor_set(x_78, 1, x_70); -lean_ctor_set(x_78, 2, x_71); -lean_ctor_set(x_78, 3, x_72); -lean_ctor_set(x_78, 4, x_77); -lean_ctor_set(x_78, 5, x_73); -x_79 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_79, 0, x_68); -lean_ctor_set(x_79, 1, x_78); -return x_79; +lean_ctor_set(x_65, 0, x_63); +lean_ctor_set_uint8(x_65, sizeof(void*)*1, x_10); +x_66 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_66, 0, x_58); +lean_ctor_set(x_66, 1, x_59); +lean_ctor_set(x_66, 2, x_60); +lean_ctor_set(x_66, 3, x_61); +lean_ctor_set(x_66, 4, x_65); +lean_ctor_set(x_66, 5, x_62); +lean_ctor_set(x_47, 1, x_66); +return x_47; } } else { -lean_object* x_80; lean_object* x_81; lean_object* x_82; -x_80 = lean_ctor_get(x_48, 0); +lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; +x_67 = lean_ctor_get(x_47, 0); +lean_inc(x_67); +lean_dec(x_47); +x_68 = lean_ctor_get(x_49, 0); +lean_inc(x_68); +x_69 = lean_ctor_get(x_49, 1); +lean_inc(x_69); +x_70 = lean_ctor_get(x_49, 2); +lean_inc(x_70); +x_71 = lean_ctor_get(x_49, 3); +lean_inc(x_71); +x_72 = lean_ctor_get(x_49, 5); +lean_inc(x_72); +if (lean_is_exclusive(x_49)) { + lean_ctor_release(x_49, 0); + lean_ctor_release(x_49, 1); + lean_ctor_release(x_49, 2); + lean_ctor_release(x_49, 3); + lean_ctor_release(x_49, 4); + lean_ctor_release(x_49, 5); + x_73 = x_49; +} else { + lean_dec_ref(x_49); + x_73 = lean_box(0); +} +x_74 = lean_ctor_get(x_50, 0); +lean_inc(x_74); +if (lean_is_exclusive(x_50)) { + lean_ctor_release(x_50, 0); + x_75 = x_50; +} else { + lean_dec_ref(x_50); + x_75 = lean_box(0); +} +if (lean_is_scalar(x_75)) { + x_76 = lean_alloc_ctor(0, 1, 1); +} else { + x_76 = x_75; +} +lean_ctor_set(x_76, 0, x_74); +lean_ctor_set_uint8(x_76, sizeof(void*)*1, x_10); +if (lean_is_scalar(x_73)) { + x_77 = lean_alloc_ctor(0, 6, 0); +} else { + x_77 = x_73; +} +lean_ctor_set(x_77, 0, x_68); +lean_ctor_set(x_77, 1, x_69); +lean_ctor_set(x_77, 2, x_70); +lean_ctor_set(x_77, 3, x_71); +lean_ctor_set(x_77, 4, x_76); +lean_ctor_set(x_77, 5, x_72); +x_78 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_78, 0, x_67); +lean_ctor_set(x_78, 1, x_77); +return x_78; +} +} +else +{ +lean_object* x_79; lean_object* x_80; lean_object* x_81; +x_79 = lean_ctor_get(x_47, 0); +lean_inc(x_79); +x_80 = lean_ctor_get(x_47, 1); lean_inc(x_80); -x_81 = lean_ctor_get(x_48, 1); +lean_dec(x_47); +x_81 = lean_ctor_get(x_80, 0); lean_inc(x_81); -lean_dec(x_48); -x_82 = lean_ctor_get(x_81, 0); +lean_dec(x_80); +x_12 = x_79; +x_13 = x_81; +goto block_32; +} +} +else +{ +lean_object* x_82; lean_object* x_83; lean_object* x_84; +lean_dec(x_3); +lean_dec(x_2); +x_82 = lean_ctor_get(x_45, 0); lean_inc(x_82); -lean_dec(x_81); -x_12 = x_80; -x_13 = x_82; -goto block_32; -} -} -else -{ -lean_object* x_83; lean_object* x_84; lean_object* x_85; -lean_dec(x_3); -lean_dec(x_2); -x_83 = lean_ctor_get(x_46, 0); +x_83 = lean_ctor_get(x_45, 1); lean_inc(x_83); -x_84 = lean_ctor_get(x_46, 1); +lean_dec(x_45); +x_84 = lean_ctor_get(x_83, 0); lean_inc(x_84); -lean_dec(x_46); -x_85 = lean_ctor_get(x_84, 0); -lean_inc(x_85); -lean_dec(x_84); -x_12 = x_83; -x_13 = x_85; +lean_dec(x_83); +x_12 = x_82; +x_13 = x_84; goto block_32; } -} -else -{ -lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; -x_86 = lean_ctor_get(x_36, 0); -x_87 = lean_ctor_get(x_36, 1); -x_88 = lean_ctor_get(x_36, 2); -x_89 = lean_ctor_get(x_36, 3); -x_90 = lean_ctor_get(x_36, 4); -x_91 = lean_ctor_get(x_36, 5); -lean_inc(x_91); -lean_inc(x_90); -lean_inc(x_89); -lean_inc(x_88); -lean_inc(x_87); -lean_inc(x_86); -lean_dec(x_36); -lean_inc(x_87); -x_92 = l_Lean_Meta_SynthInstance_mkTableKey(x_87, x_1); -lean_inc(x_87); -x_93 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_93, 0, x_86); -lean_ctor_set(x_93, 1, x_87); -lean_ctor_set(x_93, 2, x_88); -lean_ctor_set(x_93, 3, x_89); -lean_ctor_set(x_93, 4, x_90); -lean_ctor_set(x_93, 5, x_91); -x_94 = lean_box(0); -x_95 = l_Array_empty___closed__1; -x_96 = l_Lean_Meta_SynthInstance_main___closed__1; -x_97 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_97, 0, x_93); -lean_ctor_set(x_97, 1, x_94); -lean_ctor_set(x_97, 2, x_95); -lean_ctor_set(x_97, 3, x_95); -lean_ctor_set(x_97, 4, x_96); -x_98 = lean_box(1); -lean_inc(x_3); -x_99 = l_Lean_Meta_SynthInstance_newSubgoal(x_87, x_92, x_37, x_98, x_3, x_97); -if (lean_obj_tag(x_99) == 0) -{ -lean_object* x_100; lean_object* x_101; -x_100 = lean_ctor_get(x_99, 1); -lean_inc(x_100); -lean_dec(x_99); -x_101 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_100); -if (lean_obj_tag(x_101) == 0) -{ -lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; -x_102 = lean_ctor_get(x_101, 1); -lean_inc(x_102); -x_103 = lean_ctor_get(x_102, 0); -lean_inc(x_103); -lean_dec(x_102); -x_104 = lean_ctor_get(x_103, 4); -lean_inc(x_104); -x_105 = lean_ctor_get(x_101, 0); -lean_inc(x_105); -if (lean_is_exclusive(x_101)) { - lean_ctor_release(x_101, 0); - lean_ctor_release(x_101, 1); - x_106 = x_101; -} else { - lean_dec_ref(x_101); - x_106 = lean_box(0); -} -x_107 = lean_ctor_get(x_103, 0); -lean_inc(x_107); -x_108 = lean_ctor_get(x_103, 1); -lean_inc(x_108); -x_109 = lean_ctor_get(x_103, 2); -lean_inc(x_109); -x_110 = lean_ctor_get(x_103, 3); -lean_inc(x_110); -x_111 = lean_ctor_get(x_103, 5); -lean_inc(x_111); -if (lean_is_exclusive(x_103)) { - lean_ctor_release(x_103, 0); - lean_ctor_release(x_103, 1); - lean_ctor_release(x_103, 2); - lean_ctor_release(x_103, 3); - lean_ctor_release(x_103, 4); - lean_ctor_release(x_103, 5); - x_112 = x_103; -} else { - lean_dec_ref(x_103); - x_112 = lean_box(0); -} -x_113 = lean_ctor_get(x_104, 0); -lean_inc(x_113); -if (lean_is_exclusive(x_104)) { - lean_ctor_release(x_104, 0); - x_114 = x_104; -} else { - lean_dec_ref(x_104); - x_114 = lean_box(0); -} -if (lean_is_scalar(x_114)) { - x_115 = lean_alloc_ctor(0, 1, 1); -} else { - x_115 = x_114; -} -lean_ctor_set(x_115, 0, x_113); -lean_ctor_set_uint8(x_115, sizeof(void*)*1, x_10); -if (lean_is_scalar(x_112)) { - x_116 = lean_alloc_ctor(0, 6, 0); -} else { - x_116 = x_112; -} -lean_ctor_set(x_116, 0, x_107); -lean_ctor_set(x_116, 1, x_108); -lean_ctor_set(x_116, 2, x_109); -lean_ctor_set(x_116, 3, x_110); -lean_ctor_set(x_116, 4, x_115); -lean_ctor_set(x_116, 5, x_111); -if (lean_is_scalar(x_106)) { - x_117 = lean_alloc_ctor(0, 2, 0); -} else { - x_117 = x_106; -} -lean_ctor_set(x_117, 0, x_105); -lean_ctor_set(x_117, 1, x_116); -return x_117; -} -else -{ -lean_object* x_118; lean_object* x_119; lean_object* x_120; -x_118 = lean_ctor_get(x_101, 0); -lean_inc(x_118); -x_119 = lean_ctor_get(x_101, 1); -lean_inc(x_119); -lean_dec(x_101); -x_120 = lean_ctor_get(x_119, 0); -lean_inc(x_120); -lean_dec(x_119); -x_12 = x_118; -x_13 = x_120; -goto block_32; -} -} -else -{ -lean_object* x_121; lean_object* x_122; lean_object* x_123; -lean_dec(x_3); -lean_dec(x_2); -x_121 = lean_ctor_get(x_99, 0); -lean_inc(x_121); -x_122 = lean_ctor_get(x_99, 1); -lean_inc(x_122); -lean_dec(x_99); -x_123 = lean_ctor_get(x_122, 0); -lean_inc(x_123); -lean_dec(x_122); -x_12 = x_121; -x_13 = x_123; -goto block_32; -} -} block_32: { uint8_t x_14; @@ -19289,891 +19127,668 @@ return x_31; } else { -uint8_t x_124; lean_object* x_125; uint8_t x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_143; uint8_t x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; -x_124 = lean_ctor_get_uint8(x_8, sizeof(void*)*1); -x_125 = lean_ctor_get(x_8, 0); -lean_inc(x_125); +uint8_t x_85; lean_object* x_86; uint8_t x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_104; uint8_t x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; +x_85 = lean_ctor_get_uint8(x_8, sizeof(void*)*1); +x_86 = lean_ctor_get(x_8, 0); +lean_inc(x_86); lean_dec(x_8); -x_126 = 0; -x_127 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_127, 0, x_125); -lean_ctor_set_uint8(x_127, sizeof(void*)*1, x_126); -lean_ctor_set(x_6, 4, x_127); -x_143 = lean_box(0); -x_144 = 0; +x_87 = 0; +x_88 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_88, 0, x_86); +lean_ctor_set_uint8(x_88, sizeof(void*)*1, x_87); +lean_ctor_set(x_6, 4, x_88); +x_104 = lean_box(0); +x_105 = 0; lean_inc(x_3); lean_inc(x_1); -x_145 = l_Lean_Meta_mkFreshExprMVar(x_1, x_143, x_144, x_3, x_6); -x_146 = lean_ctor_get(x_145, 1); -lean_inc(x_146); -x_147 = lean_ctor_get(x_145, 0); -lean_inc(x_147); -lean_dec(x_145); -x_148 = lean_ctor_get(x_146, 0); -lean_inc(x_148); -x_149 = lean_ctor_get(x_146, 1); -lean_inc(x_149); -x_150 = lean_ctor_get(x_146, 2); -lean_inc(x_150); -x_151 = lean_ctor_get(x_146, 3); -lean_inc(x_151); -x_152 = lean_ctor_get(x_146, 4); -lean_inc(x_152); -x_153 = lean_ctor_get(x_146, 5); -lean_inc(x_153); -if (lean_is_exclusive(x_146)) { - lean_ctor_release(x_146, 0); - lean_ctor_release(x_146, 1); - lean_ctor_release(x_146, 2); - lean_ctor_release(x_146, 3); - lean_ctor_release(x_146, 4); - lean_ctor_release(x_146, 5); - x_154 = x_146; -} else { - lean_dec_ref(x_146); - x_154 = lean_box(0); -} -lean_inc(x_149); -x_155 = l_Lean_Meta_SynthInstance_mkTableKey(x_149, x_1); -lean_inc(x_149); -if (lean_is_scalar(x_154)) { - x_156 = lean_alloc_ctor(0, 6, 0); -} else { - x_156 = x_154; -} -lean_ctor_set(x_156, 0, x_148); -lean_ctor_set(x_156, 1, x_149); -lean_ctor_set(x_156, 2, x_150); -lean_ctor_set(x_156, 3, x_151); -lean_ctor_set(x_156, 4, x_152); -lean_ctor_set(x_156, 5, x_153); -x_157 = lean_box(0); -x_158 = l_Array_empty___closed__1; -x_159 = l_Lean_Meta_SynthInstance_main___closed__1; -x_160 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_160, 0, x_156); -lean_ctor_set(x_160, 1, x_157); -lean_ctor_set(x_160, 2, x_158); -lean_ctor_set(x_160, 3, x_158); -lean_ctor_set(x_160, 4, x_159); -x_161 = lean_box(1); +x_106 = l_Lean_Meta_mkFreshExprMVar(x_1, x_104, x_105, x_3, x_6); +x_107 = lean_ctor_get(x_106, 0); +lean_inc(x_107); +x_108 = lean_ctor_get(x_106, 1); +lean_inc(x_108); +lean_dec(x_106); +x_109 = lean_ctor_get(x_108, 1); +lean_inc(x_109); +lean_inc(x_109); +x_110 = l_Lean_Meta_SynthInstance_mkTableKey(x_109, x_1); +x_111 = lean_box(0); +x_112 = l_Array_empty___closed__1; +x_113 = l_Lean_Meta_SynthInstance_main___closed__1; +x_114 = lean_alloc_ctor(0, 5, 0); +lean_ctor_set(x_114, 0, x_108); +lean_ctor_set(x_114, 1, x_111); +lean_ctor_set(x_114, 2, x_112); +lean_ctor_set(x_114, 3, x_112); +lean_ctor_set(x_114, 4, x_113); +x_115 = lean_box(1); lean_inc(x_3); -x_162 = l_Lean_Meta_SynthInstance_newSubgoal(x_149, x_155, x_147, x_161, x_3, x_160); -if (lean_obj_tag(x_162) == 0) +x_116 = l_Lean_Meta_SynthInstance_newSubgoal(x_109, x_110, x_107, x_115, x_3, x_114); +if (lean_obj_tag(x_116) == 0) { -lean_object* x_163; lean_object* x_164; -x_163 = lean_ctor_get(x_162, 1); -lean_inc(x_163); -lean_dec(x_162); -x_164 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_163); -if (lean_obj_tag(x_164) == 0) +lean_object* x_117; lean_object* x_118; +x_117 = lean_ctor_get(x_116, 1); +lean_inc(x_117); +lean_dec(x_116); +x_118 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_117); +if (lean_obj_tag(x_118) == 0) { -lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; -x_165 = lean_ctor_get(x_164, 1); -lean_inc(x_165); -x_166 = lean_ctor_get(x_165, 0); -lean_inc(x_166); -lean_dec(x_165); -x_167 = lean_ctor_get(x_166, 4); -lean_inc(x_167); -x_168 = lean_ctor_get(x_164, 0); -lean_inc(x_168); -if (lean_is_exclusive(x_164)) { - lean_ctor_release(x_164, 0); - lean_ctor_release(x_164, 1); - x_169 = x_164; +lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; +x_119 = lean_ctor_get(x_118, 1); +lean_inc(x_119); +x_120 = lean_ctor_get(x_119, 0); +lean_inc(x_120); +lean_dec(x_119); +x_121 = lean_ctor_get(x_120, 4); +lean_inc(x_121); +x_122 = lean_ctor_get(x_118, 0); +lean_inc(x_122); +if (lean_is_exclusive(x_118)) { + lean_ctor_release(x_118, 0); + lean_ctor_release(x_118, 1); + x_123 = x_118; } else { - lean_dec_ref(x_164); - x_169 = lean_box(0); + lean_dec_ref(x_118); + x_123 = lean_box(0); } -x_170 = lean_ctor_get(x_166, 0); -lean_inc(x_170); -x_171 = lean_ctor_get(x_166, 1); -lean_inc(x_171); -x_172 = lean_ctor_get(x_166, 2); -lean_inc(x_172); -x_173 = lean_ctor_get(x_166, 3); -lean_inc(x_173); -x_174 = lean_ctor_get(x_166, 5); -lean_inc(x_174); -if (lean_is_exclusive(x_166)) { - lean_ctor_release(x_166, 0); - lean_ctor_release(x_166, 1); - lean_ctor_release(x_166, 2); - lean_ctor_release(x_166, 3); - lean_ctor_release(x_166, 4); - lean_ctor_release(x_166, 5); - x_175 = x_166; +x_124 = lean_ctor_get(x_120, 0); +lean_inc(x_124); +x_125 = lean_ctor_get(x_120, 1); +lean_inc(x_125); +x_126 = lean_ctor_get(x_120, 2); +lean_inc(x_126); +x_127 = lean_ctor_get(x_120, 3); +lean_inc(x_127); +x_128 = lean_ctor_get(x_120, 5); +lean_inc(x_128); +if (lean_is_exclusive(x_120)) { + lean_ctor_release(x_120, 0); + lean_ctor_release(x_120, 1); + lean_ctor_release(x_120, 2); + lean_ctor_release(x_120, 3); + lean_ctor_release(x_120, 4); + lean_ctor_release(x_120, 5); + x_129 = x_120; } else { - lean_dec_ref(x_166); - x_175 = lean_box(0); + lean_dec_ref(x_120); + x_129 = lean_box(0); } -x_176 = lean_ctor_get(x_167, 0); -lean_inc(x_176); -if (lean_is_exclusive(x_167)) { - lean_ctor_release(x_167, 0); - x_177 = x_167; +x_130 = lean_ctor_get(x_121, 0); +lean_inc(x_130); +if (lean_is_exclusive(x_121)) { + lean_ctor_release(x_121, 0); + x_131 = x_121; } else { - lean_dec_ref(x_167); - x_177 = lean_box(0); + lean_dec_ref(x_121); + x_131 = lean_box(0); } -if (lean_is_scalar(x_177)) { - x_178 = lean_alloc_ctor(0, 1, 1); +if (lean_is_scalar(x_131)) { + x_132 = lean_alloc_ctor(0, 1, 1); } else { - x_178 = x_177; + x_132 = x_131; } -lean_ctor_set(x_178, 0, x_176); -lean_ctor_set_uint8(x_178, sizeof(void*)*1, x_124); -if (lean_is_scalar(x_175)) { - x_179 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_132, 0, x_130); +lean_ctor_set_uint8(x_132, sizeof(void*)*1, x_85); +if (lean_is_scalar(x_129)) { + x_133 = lean_alloc_ctor(0, 6, 0); } else { - x_179 = x_175; + x_133 = x_129; } -lean_ctor_set(x_179, 0, x_170); -lean_ctor_set(x_179, 1, x_171); -lean_ctor_set(x_179, 2, x_172); -lean_ctor_set(x_179, 3, x_173); -lean_ctor_set(x_179, 4, x_178); -lean_ctor_set(x_179, 5, x_174); -if (lean_is_scalar(x_169)) { - x_180 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_133, 0, x_124); +lean_ctor_set(x_133, 1, x_125); +lean_ctor_set(x_133, 2, x_126); +lean_ctor_set(x_133, 3, x_127); +lean_ctor_set(x_133, 4, x_132); +lean_ctor_set(x_133, 5, x_128); +if (lean_is_scalar(x_123)) { + x_134 = lean_alloc_ctor(0, 2, 0); } else { - x_180 = x_169; + x_134 = x_123; } -lean_ctor_set(x_180, 0, x_168); -lean_ctor_set(x_180, 1, x_179); -return x_180; +lean_ctor_set(x_134, 0, x_122); +lean_ctor_set(x_134, 1, x_133); +return x_134; } else { -lean_object* x_181; lean_object* x_182; lean_object* x_183; -x_181 = lean_ctor_get(x_164, 0); -lean_inc(x_181); -x_182 = lean_ctor_get(x_164, 1); -lean_inc(x_182); -lean_dec(x_164); -x_183 = lean_ctor_get(x_182, 0); -lean_inc(x_183); -lean_dec(x_182); -x_128 = x_181; -x_129 = x_183; -goto block_142; +lean_object* x_135; lean_object* x_136; lean_object* x_137; +x_135 = lean_ctor_get(x_118, 0); +lean_inc(x_135); +x_136 = lean_ctor_get(x_118, 1); +lean_inc(x_136); +lean_dec(x_118); +x_137 = lean_ctor_get(x_136, 0); +lean_inc(x_137); +lean_dec(x_136); +x_89 = x_135; +x_90 = x_137; +goto block_103; } } else { -lean_object* x_184; lean_object* x_185; lean_object* x_186; +lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_dec(x_3); lean_dec(x_2); -x_184 = lean_ctor_get(x_162, 0); -lean_inc(x_184); -x_185 = lean_ctor_get(x_162, 1); -lean_inc(x_185); -lean_dec(x_162); -x_186 = lean_ctor_get(x_185, 0); -lean_inc(x_186); -lean_dec(x_185); -x_128 = x_184; -x_129 = x_186; -goto block_142; +x_138 = lean_ctor_get(x_116, 0); +lean_inc(x_138); +x_139 = lean_ctor_get(x_116, 1); +lean_inc(x_139); +lean_dec(x_116); +x_140 = lean_ctor_get(x_139, 0); +lean_inc(x_140); +lean_dec(x_139); +x_89 = x_138; +x_90 = x_140; +goto block_103; } -block_142: +block_103: { -lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; -x_130 = lean_ctor_get(x_129, 4); -lean_inc(x_130); -x_131 = lean_ctor_get(x_129, 0); -lean_inc(x_131); -x_132 = lean_ctor_get(x_129, 1); -lean_inc(x_132); -x_133 = lean_ctor_get(x_129, 2); -lean_inc(x_133); -x_134 = lean_ctor_get(x_129, 3); -lean_inc(x_134); -x_135 = lean_ctor_get(x_129, 5); -lean_inc(x_135); -if (lean_is_exclusive(x_129)) { - lean_ctor_release(x_129, 0); - lean_ctor_release(x_129, 1); - lean_ctor_release(x_129, 2); - lean_ctor_release(x_129, 3); - lean_ctor_release(x_129, 4); - lean_ctor_release(x_129, 5); - x_136 = x_129; +lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; +x_91 = lean_ctor_get(x_90, 4); +lean_inc(x_91); +x_92 = lean_ctor_get(x_90, 0); +lean_inc(x_92); +x_93 = lean_ctor_get(x_90, 1); +lean_inc(x_93); +x_94 = lean_ctor_get(x_90, 2); +lean_inc(x_94); +x_95 = lean_ctor_get(x_90, 3); +lean_inc(x_95); +x_96 = lean_ctor_get(x_90, 5); +lean_inc(x_96); +if (lean_is_exclusive(x_90)) { + lean_ctor_release(x_90, 0); + lean_ctor_release(x_90, 1); + lean_ctor_release(x_90, 2); + lean_ctor_release(x_90, 3); + lean_ctor_release(x_90, 4); + lean_ctor_release(x_90, 5); + x_97 = x_90; } else { - lean_dec_ref(x_129); - x_136 = lean_box(0); + lean_dec_ref(x_90); + x_97 = lean_box(0); } -x_137 = lean_ctor_get(x_130, 0); -lean_inc(x_137); -if (lean_is_exclusive(x_130)) { - lean_ctor_release(x_130, 0); - x_138 = x_130; +x_98 = lean_ctor_get(x_91, 0); +lean_inc(x_98); +if (lean_is_exclusive(x_91)) { + lean_ctor_release(x_91, 0); + x_99 = x_91; } else { - lean_dec_ref(x_130); - x_138 = lean_box(0); + lean_dec_ref(x_91); + x_99 = lean_box(0); } -if (lean_is_scalar(x_138)) { - x_139 = lean_alloc_ctor(0, 1, 1); +if (lean_is_scalar(x_99)) { + x_100 = lean_alloc_ctor(0, 1, 1); } else { - x_139 = x_138; + x_100 = x_99; } -lean_ctor_set(x_139, 0, x_137); -lean_ctor_set_uint8(x_139, sizeof(void*)*1, x_124); -if (lean_is_scalar(x_136)) { - x_140 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_100, 0, x_98); +lean_ctor_set_uint8(x_100, sizeof(void*)*1, x_85); +if (lean_is_scalar(x_97)) { + x_101 = lean_alloc_ctor(0, 6, 0); } else { - x_140 = x_136; + x_101 = x_97; } -lean_ctor_set(x_140, 0, x_131); -lean_ctor_set(x_140, 1, x_132); -lean_ctor_set(x_140, 2, x_133); -lean_ctor_set(x_140, 3, x_134); -lean_ctor_set(x_140, 4, x_139); -lean_ctor_set(x_140, 5, x_135); -x_141 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_141, 0, x_128); -lean_ctor_set(x_141, 1, x_140); -return x_141; +lean_ctor_set(x_101, 0, x_92); +lean_ctor_set(x_101, 1, x_93); +lean_ctor_set(x_101, 2, x_94); +lean_ctor_set(x_101, 3, x_95); +lean_ctor_set(x_101, 4, x_100); +lean_ctor_set(x_101, 5, x_96); +x_102 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_102, 0, x_89); +lean_ctor_set(x_102, 1, x_101); +return x_102; } } } else { -lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; uint8_t x_193; lean_object* x_194; lean_object* x_195; uint8_t x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_214; uint8_t x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; -x_187 = lean_ctor_get(x_6, 4); -x_188 = lean_ctor_get(x_6, 0); -x_189 = lean_ctor_get(x_6, 1); -x_190 = lean_ctor_get(x_6, 2); -x_191 = lean_ctor_get(x_6, 3); -x_192 = lean_ctor_get(x_6, 5); -lean_inc(x_192); -lean_inc(x_187); -lean_inc(x_191); -lean_inc(x_190); -lean_inc(x_189); -lean_inc(x_188); +lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; uint8_t x_147; lean_object* x_148; lean_object* x_149; uint8_t x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_168; uint8_t x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; +x_141 = lean_ctor_get(x_6, 4); +x_142 = lean_ctor_get(x_6, 0); +x_143 = lean_ctor_get(x_6, 1); +x_144 = lean_ctor_get(x_6, 2); +x_145 = lean_ctor_get(x_6, 3); +x_146 = lean_ctor_get(x_6, 5); +lean_inc(x_146); +lean_inc(x_141); +lean_inc(x_145); +lean_inc(x_144); +lean_inc(x_143); +lean_inc(x_142); lean_dec(x_6); -x_193 = lean_ctor_get_uint8(x_187, sizeof(void*)*1); -x_194 = lean_ctor_get(x_187, 0); -lean_inc(x_194); -if (lean_is_exclusive(x_187)) { - lean_ctor_release(x_187, 0); - x_195 = x_187; +x_147 = lean_ctor_get_uint8(x_141, sizeof(void*)*1); +x_148 = lean_ctor_get(x_141, 0); +lean_inc(x_148); +if (lean_is_exclusive(x_141)) { + lean_ctor_release(x_141, 0); + x_149 = x_141; } else { - lean_dec_ref(x_187); + lean_dec_ref(x_141); + x_149 = lean_box(0); +} +x_150 = 0; +if (lean_is_scalar(x_149)) { + x_151 = lean_alloc_ctor(0, 1, 1); +} else { + x_151 = x_149; +} +lean_ctor_set(x_151, 0, x_148); +lean_ctor_set_uint8(x_151, sizeof(void*)*1, x_150); +x_152 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_152, 0, x_142); +lean_ctor_set(x_152, 1, x_143); +lean_ctor_set(x_152, 2, x_144); +lean_ctor_set(x_152, 3, x_145); +lean_ctor_set(x_152, 4, x_151); +lean_ctor_set(x_152, 5, x_146); +x_168 = lean_box(0); +x_169 = 0; +lean_inc(x_3); +lean_inc(x_1); +x_170 = l_Lean_Meta_mkFreshExprMVar(x_1, x_168, x_169, x_3, x_152); +x_171 = lean_ctor_get(x_170, 0); +lean_inc(x_171); +x_172 = lean_ctor_get(x_170, 1); +lean_inc(x_172); +lean_dec(x_170); +x_173 = lean_ctor_get(x_172, 1); +lean_inc(x_173); +lean_inc(x_173); +x_174 = l_Lean_Meta_SynthInstance_mkTableKey(x_173, x_1); +x_175 = lean_box(0); +x_176 = l_Array_empty___closed__1; +x_177 = l_Lean_Meta_SynthInstance_main___closed__1; +x_178 = lean_alloc_ctor(0, 5, 0); +lean_ctor_set(x_178, 0, x_172); +lean_ctor_set(x_178, 1, x_175); +lean_ctor_set(x_178, 2, x_176); +lean_ctor_set(x_178, 3, x_176); +lean_ctor_set(x_178, 4, x_177); +x_179 = lean_box(1); +lean_inc(x_3); +x_180 = l_Lean_Meta_SynthInstance_newSubgoal(x_173, x_174, x_171, x_179, x_3, x_178); +if (lean_obj_tag(x_180) == 0) +{ +lean_object* x_181; lean_object* x_182; +x_181 = lean_ctor_get(x_180, 1); +lean_inc(x_181); +lean_dec(x_180); +x_182 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_181); +if (lean_obj_tag(x_182) == 0) +{ +lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; +x_183 = lean_ctor_get(x_182, 1); +lean_inc(x_183); +x_184 = lean_ctor_get(x_183, 0); +lean_inc(x_184); +lean_dec(x_183); +x_185 = lean_ctor_get(x_184, 4); +lean_inc(x_185); +x_186 = lean_ctor_get(x_182, 0); +lean_inc(x_186); +if (lean_is_exclusive(x_182)) { + lean_ctor_release(x_182, 0); + lean_ctor_release(x_182, 1); + x_187 = x_182; +} else { + lean_dec_ref(x_182); + x_187 = lean_box(0); +} +x_188 = lean_ctor_get(x_184, 0); +lean_inc(x_188); +x_189 = lean_ctor_get(x_184, 1); +lean_inc(x_189); +x_190 = lean_ctor_get(x_184, 2); +lean_inc(x_190); +x_191 = lean_ctor_get(x_184, 3); +lean_inc(x_191); +x_192 = lean_ctor_get(x_184, 5); +lean_inc(x_192); +if (lean_is_exclusive(x_184)) { + lean_ctor_release(x_184, 0); + lean_ctor_release(x_184, 1); + lean_ctor_release(x_184, 2); + lean_ctor_release(x_184, 3); + lean_ctor_release(x_184, 4); + lean_ctor_release(x_184, 5); + x_193 = x_184; +} else { + lean_dec_ref(x_184); + x_193 = lean_box(0); +} +x_194 = lean_ctor_get(x_185, 0); +lean_inc(x_194); +if (lean_is_exclusive(x_185)) { + lean_ctor_release(x_185, 0); + x_195 = x_185; +} else { + lean_dec_ref(x_185); x_195 = lean_box(0); } -x_196 = 0; if (lean_is_scalar(x_195)) { - x_197 = lean_alloc_ctor(0, 1, 1); + x_196 = lean_alloc_ctor(0, 1, 1); } else { - x_197 = x_195; + x_196 = x_195; } -lean_ctor_set(x_197, 0, x_194); -lean_ctor_set_uint8(x_197, sizeof(void*)*1, x_196); -x_198 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_198, 0, x_188); -lean_ctor_set(x_198, 1, x_189); -lean_ctor_set(x_198, 2, x_190); -lean_ctor_set(x_198, 3, x_191); -lean_ctor_set(x_198, 4, x_197); -lean_ctor_set(x_198, 5, x_192); -x_214 = lean_box(0); -x_215 = 0; -lean_inc(x_3); -lean_inc(x_1); -x_216 = l_Lean_Meta_mkFreshExprMVar(x_1, x_214, x_215, x_3, x_198); -x_217 = lean_ctor_get(x_216, 1); -lean_inc(x_217); -x_218 = lean_ctor_get(x_216, 0); -lean_inc(x_218); -lean_dec(x_216); -x_219 = lean_ctor_get(x_217, 0); -lean_inc(x_219); -x_220 = lean_ctor_get(x_217, 1); -lean_inc(x_220); -x_221 = lean_ctor_get(x_217, 2); -lean_inc(x_221); -x_222 = lean_ctor_get(x_217, 3); -lean_inc(x_222); -x_223 = lean_ctor_get(x_217, 4); -lean_inc(x_223); -x_224 = lean_ctor_get(x_217, 5); -lean_inc(x_224); -if (lean_is_exclusive(x_217)) { - lean_ctor_release(x_217, 0); - lean_ctor_release(x_217, 1); - lean_ctor_release(x_217, 2); - lean_ctor_release(x_217, 3); - lean_ctor_release(x_217, 4); - lean_ctor_release(x_217, 5); - x_225 = x_217; +lean_ctor_set(x_196, 0, x_194); +lean_ctor_set_uint8(x_196, sizeof(void*)*1, x_147); +if (lean_is_scalar(x_193)) { + x_197 = lean_alloc_ctor(0, 6, 0); } else { - lean_dec_ref(x_217); - x_225 = lean_box(0); + x_197 = x_193; } -lean_inc(x_220); -x_226 = l_Lean_Meta_SynthInstance_mkTableKey(x_220, x_1); -lean_inc(x_220); -if (lean_is_scalar(x_225)) { - x_227 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_197, 0, x_188); +lean_ctor_set(x_197, 1, x_189); +lean_ctor_set(x_197, 2, x_190); +lean_ctor_set(x_197, 3, x_191); +lean_ctor_set(x_197, 4, x_196); +lean_ctor_set(x_197, 5, x_192); +if (lean_is_scalar(x_187)) { + x_198 = lean_alloc_ctor(0, 2, 0); } else { - x_227 = x_225; + x_198 = x_187; } -lean_ctor_set(x_227, 0, x_219); -lean_ctor_set(x_227, 1, x_220); -lean_ctor_set(x_227, 2, x_221); -lean_ctor_set(x_227, 3, x_222); -lean_ctor_set(x_227, 4, x_223); -lean_ctor_set(x_227, 5, x_224); -x_228 = lean_box(0); -x_229 = l_Array_empty___closed__1; -x_230 = l_Lean_Meta_SynthInstance_main___closed__1; -x_231 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_231, 0, x_227); -lean_ctor_set(x_231, 1, x_228); -lean_ctor_set(x_231, 2, x_229); -lean_ctor_set(x_231, 3, x_229); -lean_ctor_set(x_231, 4, x_230); -x_232 = lean_box(1); -lean_inc(x_3); -x_233 = l_Lean_Meta_SynthInstance_newSubgoal(x_220, x_226, x_218, x_232, x_3, x_231); -if (lean_obj_tag(x_233) == 0) -{ -lean_object* x_234; lean_object* x_235; -x_234 = lean_ctor_get(x_233, 1); -lean_inc(x_234); -lean_dec(x_233); -x_235 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_234); -if (lean_obj_tag(x_235) == 0) -{ -lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; -x_236 = lean_ctor_get(x_235, 1); -lean_inc(x_236); -x_237 = lean_ctor_get(x_236, 0); -lean_inc(x_237); -lean_dec(x_236); -x_238 = lean_ctor_get(x_237, 4); -lean_inc(x_238); -x_239 = lean_ctor_get(x_235, 0); -lean_inc(x_239); -if (lean_is_exclusive(x_235)) { - lean_ctor_release(x_235, 0); - lean_ctor_release(x_235, 1); - x_240 = x_235; -} else { - lean_dec_ref(x_235); - x_240 = lean_box(0); -} -x_241 = lean_ctor_get(x_237, 0); -lean_inc(x_241); -x_242 = lean_ctor_get(x_237, 1); -lean_inc(x_242); -x_243 = lean_ctor_get(x_237, 2); -lean_inc(x_243); -x_244 = lean_ctor_get(x_237, 3); -lean_inc(x_244); -x_245 = lean_ctor_get(x_237, 5); -lean_inc(x_245); -if (lean_is_exclusive(x_237)) { - lean_ctor_release(x_237, 0); - lean_ctor_release(x_237, 1); - lean_ctor_release(x_237, 2); - lean_ctor_release(x_237, 3); - lean_ctor_release(x_237, 4); - lean_ctor_release(x_237, 5); - x_246 = x_237; -} else { - lean_dec_ref(x_237); - x_246 = lean_box(0); -} -x_247 = lean_ctor_get(x_238, 0); -lean_inc(x_247); -if (lean_is_exclusive(x_238)) { - lean_ctor_release(x_238, 0); - x_248 = x_238; -} else { - lean_dec_ref(x_238); - x_248 = lean_box(0); -} -if (lean_is_scalar(x_248)) { - x_249 = lean_alloc_ctor(0, 1, 1); -} else { - x_249 = x_248; -} -lean_ctor_set(x_249, 0, x_247); -lean_ctor_set_uint8(x_249, sizeof(void*)*1, x_193); -if (lean_is_scalar(x_246)) { - x_250 = lean_alloc_ctor(0, 6, 0); -} else { - x_250 = x_246; -} -lean_ctor_set(x_250, 0, x_241); -lean_ctor_set(x_250, 1, x_242); -lean_ctor_set(x_250, 2, x_243); -lean_ctor_set(x_250, 3, x_244); -lean_ctor_set(x_250, 4, x_249); -lean_ctor_set(x_250, 5, x_245); -if (lean_is_scalar(x_240)) { - x_251 = lean_alloc_ctor(0, 2, 0); -} else { - x_251 = x_240; -} -lean_ctor_set(x_251, 0, x_239); -lean_ctor_set(x_251, 1, x_250); -return x_251; +lean_ctor_set(x_198, 0, x_186); +lean_ctor_set(x_198, 1, x_197); +return x_198; } else { -lean_object* x_252; lean_object* x_253; lean_object* x_254; -x_252 = lean_ctor_get(x_235, 0); -lean_inc(x_252); -x_253 = lean_ctor_get(x_235, 1); -lean_inc(x_253); -lean_dec(x_235); -x_254 = lean_ctor_get(x_253, 0); -lean_inc(x_254); -lean_dec(x_253); -x_199 = x_252; -x_200 = x_254; -goto block_213; -} -} -else -{ -lean_object* x_255; lean_object* x_256; lean_object* x_257; -lean_dec(x_3); -lean_dec(x_2); -x_255 = lean_ctor_get(x_233, 0); -lean_inc(x_255); -x_256 = lean_ctor_get(x_233, 1); -lean_inc(x_256); -lean_dec(x_233); -x_257 = lean_ctor_get(x_256, 0); -lean_inc(x_257); -lean_dec(x_256); -x_199 = x_255; -x_200 = x_257; -goto block_213; -} -block_213: -{ -lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; -x_201 = lean_ctor_get(x_200, 4); +lean_object* x_199; lean_object* x_200; lean_object* x_201; +x_199 = lean_ctor_get(x_182, 0); +lean_inc(x_199); +x_200 = lean_ctor_get(x_182, 1); +lean_inc(x_200); +lean_dec(x_182); +x_201 = lean_ctor_get(x_200, 0); lean_inc(x_201); -x_202 = lean_ctor_get(x_200, 0); +lean_dec(x_200); +x_153 = x_199; +x_154 = x_201; +goto block_167; +} +} +else +{ +lean_object* x_202; lean_object* x_203; lean_object* x_204; +lean_dec(x_3); +lean_dec(x_2); +x_202 = lean_ctor_get(x_180, 0); lean_inc(x_202); -x_203 = lean_ctor_get(x_200, 1); +x_203 = lean_ctor_get(x_180, 1); lean_inc(x_203); -x_204 = lean_ctor_get(x_200, 2); +lean_dec(x_180); +x_204 = lean_ctor_get(x_203, 0); lean_inc(x_204); -x_205 = lean_ctor_get(x_200, 3); -lean_inc(x_205); -x_206 = lean_ctor_get(x_200, 5); +lean_dec(x_203); +x_153 = x_202; +x_154 = x_204; +goto block_167; +} +block_167: +{ +lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; +x_155 = lean_ctor_get(x_154, 4); +lean_inc(x_155); +x_156 = lean_ctor_get(x_154, 0); +lean_inc(x_156); +x_157 = lean_ctor_get(x_154, 1); +lean_inc(x_157); +x_158 = lean_ctor_get(x_154, 2); +lean_inc(x_158); +x_159 = lean_ctor_get(x_154, 3); +lean_inc(x_159); +x_160 = lean_ctor_get(x_154, 5); +lean_inc(x_160); +if (lean_is_exclusive(x_154)) { + lean_ctor_release(x_154, 0); + lean_ctor_release(x_154, 1); + lean_ctor_release(x_154, 2); + lean_ctor_release(x_154, 3); + lean_ctor_release(x_154, 4); + lean_ctor_release(x_154, 5); + x_161 = x_154; +} else { + lean_dec_ref(x_154); + x_161 = lean_box(0); +} +x_162 = lean_ctor_get(x_155, 0); +lean_inc(x_162); +if (lean_is_exclusive(x_155)) { + lean_ctor_release(x_155, 0); + x_163 = x_155; +} else { + lean_dec_ref(x_155); + x_163 = lean_box(0); +} +if (lean_is_scalar(x_163)) { + x_164 = lean_alloc_ctor(0, 1, 1); +} else { + x_164 = x_163; +} +lean_ctor_set(x_164, 0, x_162); +lean_ctor_set_uint8(x_164, sizeof(void*)*1, x_147); +if (lean_is_scalar(x_161)) { + x_165 = lean_alloc_ctor(0, 6, 0); +} else { + x_165 = x_161; +} +lean_ctor_set(x_165, 0, x_156); +lean_ctor_set(x_165, 1, x_157); +lean_ctor_set(x_165, 2, x_158); +lean_ctor_set(x_165, 3, x_159); +lean_ctor_set(x_165, 4, x_164); +lean_ctor_set(x_165, 5, x_160); +x_166 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_166, 0, x_153); +lean_ctor_set(x_166, 1, x_165); +return x_166; +} +} +} +else +{ +lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_252; uint8_t x_253; +x_205 = l___private_Init_Lean_Util_Trace_3__getResetTraces___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__6___rarg(x_6); +x_206 = lean_ctor_get(x_205, 0); lean_inc(x_206); -if (lean_is_exclusive(x_200)) { - lean_ctor_release(x_200, 0); - lean_ctor_release(x_200, 1); - lean_ctor_release(x_200, 2); - lean_ctor_release(x_200, 3); - lean_ctor_release(x_200, 4); - lean_ctor_release(x_200, 5); - x_207 = x_200; -} else { - lean_dec_ref(x_200); - x_207 = lean_box(0); -} -x_208 = lean_ctor_get(x_201, 0); -lean_inc(x_208); -if (lean_is_exclusive(x_201)) { - lean_ctor_release(x_201, 0); - x_209 = x_201; -} else { - lean_dec_ref(x_201); - x_209 = lean_box(0); -} -if (lean_is_scalar(x_209)) { - x_210 = lean_alloc_ctor(0, 1, 1); -} else { - x_210 = x_209; -} -lean_ctor_set(x_210, 0, x_208); -lean_ctor_set_uint8(x_210, sizeof(void*)*1, x_193); -if (lean_is_scalar(x_207)) { - x_211 = lean_alloc_ctor(0, 6, 0); -} else { - x_211 = x_207; -} -lean_ctor_set(x_211, 0, x_202); -lean_ctor_set(x_211, 1, x_203); -lean_ctor_set(x_211, 2, x_204); -lean_ctor_set(x_211, 3, x_205); -lean_ctor_set(x_211, 4, x_210); -lean_ctor_set(x_211, 5, x_206); -x_212 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_212, 0, x_199); -lean_ctor_set(x_212, 1, x_211); -return x_212; -} -} +x_207 = lean_ctor_get(x_205, 1); +lean_inc(x_207); +lean_dec(x_205); +x_252 = lean_ctor_get(x_207, 4); +lean_inc(x_252); +x_253 = lean_ctor_get_uint8(x_252, sizeof(void*)*1); +lean_dec(x_252); +if (x_253 == 0) +{ +x_208 = x_207; +goto block_251; } else { -lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_346; uint8_t x_347; -x_258 = l___private_Init_Lean_Util_Trace_3__getResetTraces___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__6___rarg(x_6); -x_259 = lean_ctor_get(x_258, 0); +lean_object* x_254; lean_object* x_255; lean_object* x_256; uint8_t x_257; +x_254 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; +x_255 = l___private_Init_Lean_Util_Trace_5__checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___main___spec__2(x_254, x_3, x_207); +x_256 = lean_ctor_get(x_255, 0); +lean_inc(x_256); +x_257 = lean_unbox(x_256); +lean_dec(x_256); +if (x_257 == 0) +{ +lean_object* x_258; +x_258 = lean_ctor_get(x_255, 1); +lean_inc(x_258); +lean_dec(x_255); +x_208 = x_258; +goto block_251; +} +else +{ +lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264; +x_259 = lean_ctor_get(x_255, 1); lean_inc(x_259); -x_260 = lean_ctor_get(x_258, 1); -lean_inc(x_260); -lean_dec(x_258); -x_346 = lean_ctor_get(x_260, 4); -lean_inc(x_346); -x_347 = lean_ctor_get_uint8(x_346, sizeof(void*)*1); -lean_dec(x_346); -if (x_347 == 0) -{ -x_261 = x_260; -goto block_345; -} -else -{ -lean_object* x_348; lean_object* x_349; lean_object* x_350; uint8_t x_351; -x_348 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_349 = l___private_Init_Lean_Util_Trace_5__checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___main___spec__2(x_348, x_3, x_260); -x_350 = lean_ctor_get(x_349, 0); -lean_inc(x_350); -x_351 = lean_unbox(x_350); -lean_dec(x_350); -if (x_351 == 0) -{ -lean_object* x_352; -x_352 = lean_ctor_get(x_349, 1); -lean_inc(x_352); -lean_dec(x_349); -x_261 = x_352; -goto block_345; -} -else -{ -lean_object* x_353; lean_object* x_354; lean_object* x_355; lean_object* x_356; lean_object* x_357; lean_object* x_358; -x_353 = lean_ctor_get(x_349, 1); -lean_inc(x_353); -lean_dec(x_349); +lean_dec(x_255); lean_inc(x_1); -x_354 = lean_alloc_ctor(2, 1, 0); -lean_ctor_set(x_354, 0, x_1); -x_355 = l_Lean_Meta_SynthInstance_main___closed__4; -x_356 = lean_alloc_ctor(9, 2, 0); -lean_ctor_set(x_356, 0, x_355); -lean_ctor_set(x_356, 1, x_354); -x_357 = l_Lean_MonadTracerAdapter_addTrace___at_Lean_Meta_isLevelDefEqAux___main___spec__1(x_348, x_356, x_3, x_353); -x_358 = lean_ctor_get(x_357, 1); -lean_inc(x_358); -lean_dec(x_357); -x_261 = x_358; -goto block_345; +x_260 = lean_alloc_ctor(2, 1, 0); +lean_ctor_set(x_260, 0, x_1); +x_261 = l_Lean_Meta_SynthInstance_main___closed__4; +x_262 = lean_alloc_ctor(9, 2, 0); +lean_ctor_set(x_262, 0, x_261); +lean_ctor_set(x_262, 1, x_260); +x_263 = l_Lean_MonadTracerAdapter_addTrace___at_Lean_Meta_isLevelDefEqAux___main___spec__1(x_254, x_262, x_3, x_259); +x_264 = lean_ctor_get(x_263, 1); +lean_inc(x_264); +lean_dec(x_263); +x_208 = x_264; +goto block_251; } } -block_345: +block_251: { -lean_object* x_262; uint8_t x_263; lean_object* x_264; lean_object* x_265; lean_object* x_266; uint8_t x_267; -x_262 = lean_box(0); -x_263 = 0; +lean_object* x_209; uint8_t x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; +x_209 = lean_box(0); +x_210 = 0; lean_inc(x_3); lean_inc(x_1); -x_264 = l_Lean_Meta_mkFreshExprMVar(x_1, x_262, x_263, x_3, x_261); -x_265 = lean_ctor_get(x_264, 1); -lean_inc(x_265); -x_266 = lean_ctor_get(x_264, 0); -lean_inc(x_266); -lean_dec(x_264); -x_267 = !lean_is_exclusive(x_265); -if (x_267 == 0) -{ -lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; -x_268 = lean_ctor_get(x_265, 1); -lean_inc(x_268); -x_269 = l_Lean_Meta_SynthInstance_mkTableKey(x_268, x_1); -lean_inc(x_268); -x_270 = lean_box(0); -x_271 = l_Array_empty___closed__1; -x_272 = l_Lean_Meta_SynthInstance_main___closed__1; -x_273 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_273, 0, x_265); -lean_ctor_set(x_273, 1, x_270); -lean_ctor_set(x_273, 2, x_271); -lean_ctor_set(x_273, 3, x_271); -lean_ctor_set(x_273, 4, x_272); -x_274 = lean_box(1); +x_211 = l_Lean_Meta_mkFreshExprMVar(x_1, x_209, x_210, x_3, x_208); +x_212 = lean_ctor_get(x_211, 0); +lean_inc(x_212); +x_213 = lean_ctor_get(x_211, 1); +lean_inc(x_213); +lean_dec(x_211); +x_214 = lean_ctor_get(x_213, 1); +lean_inc(x_214); +lean_inc(x_214); +x_215 = l_Lean_Meta_SynthInstance_mkTableKey(x_214, x_1); +x_216 = lean_box(0); +x_217 = l_Array_empty___closed__1; +x_218 = l_Lean_Meta_SynthInstance_main___closed__1; +x_219 = lean_alloc_ctor(0, 5, 0); +lean_ctor_set(x_219, 0, x_213); +lean_ctor_set(x_219, 1, x_216); +lean_ctor_set(x_219, 2, x_217); +lean_ctor_set(x_219, 3, x_217); +lean_ctor_set(x_219, 4, x_218); +x_220 = lean_box(1); lean_inc(x_3); -x_275 = l_Lean_Meta_SynthInstance_newSubgoal(x_268, x_269, x_266, x_274, x_3, x_273); -if (lean_obj_tag(x_275) == 0) +x_221 = l_Lean_Meta_SynthInstance_newSubgoal(x_214, x_215, x_212, x_220, x_3, x_219); +if (lean_obj_tag(x_221) == 0) { -lean_object* x_276; lean_object* x_277; -x_276 = lean_ctor_get(x_275, 1); -lean_inc(x_276); -lean_dec(x_275); +lean_object* x_222; lean_object* x_223; +x_222 = lean_ctor_get(x_221, 1); +lean_inc(x_222); +lean_dec(x_221); lean_inc(x_3); -x_277 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_276); -if (lean_obj_tag(x_277) == 0) +x_223 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_222); +if (lean_obj_tag(x_223) == 0) { -lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; uint8_t x_283; -x_278 = lean_ctor_get(x_277, 0); -lean_inc(x_278); -x_279 = lean_ctor_get(x_277, 1); -lean_inc(x_279); -lean_dec(x_277); -x_280 = lean_ctor_get(x_279, 0); -lean_inc(x_280); -lean_dec(x_279); -x_281 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_282 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_281, x_3, x_280); +lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; uint8_t x_229; +x_224 = lean_ctor_get(x_223, 0); +lean_inc(x_224); +x_225 = lean_ctor_get(x_223, 1); +lean_inc(x_225); +lean_dec(x_223); +x_226 = lean_ctor_get(x_225, 0); +lean_inc(x_226); +lean_dec(x_225); +x_227 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; +x_228 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_206, x_227, x_3, x_226); lean_dec(x_3); -x_283 = !lean_is_exclusive(x_282); -if (x_283 == 0) +x_229 = !lean_is_exclusive(x_228); +if (x_229 == 0) { -lean_object* x_284; -x_284 = lean_ctor_get(x_282, 0); -lean_dec(x_284); -lean_ctor_set(x_282, 0, x_278); -return x_282; +lean_object* x_230; +x_230 = lean_ctor_get(x_228, 0); +lean_dec(x_230); +lean_ctor_set(x_228, 0, x_224); +return x_228; } else { -lean_object* x_285; lean_object* x_286; -x_285 = lean_ctor_get(x_282, 1); -lean_inc(x_285); -lean_dec(x_282); -x_286 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_286, 0, x_278); -lean_ctor_set(x_286, 1, x_285); -return x_286; +lean_object* x_231; lean_object* x_232; +x_231 = lean_ctor_get(x_228, 1); +lean_inc(x_231); +lean_dec(x_228); +x_232 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_232, 0, x_224); +lean_ctor_set(x_232, 1, x_231); +return x_232; } } else { -lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; uint8_t x_292; -x_287 = lean_ctor_get(x_277, 0); -lean_inc(x_287); -x_288 = lean_ctor_get(x_277, 1); -lean_inc(x_288); -lean_dec(x_277); -x_289 = lean_ctor_get(x_288, 0); -lean_inc(x_289); -lean_dec(x_288); -x_290 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_291 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_290, x_3, x_289); +lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; uint8_t x_238; +x_233 = lean_ctor_get(x_223, 0); +lean_inc(x_233); +x_234 = lean_ctor_get(x_223, 1); +lean_inc(x_234); +lean_dec(x_223); +x_235 = lean_ctor_get(x_234, 0); +lean_inc(x_235); +lean_dec(x_234); +x_236 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; +x_237 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_206, x_236, x_3, x_235); lean_dec(x_3); -x_292 = !lean_is_exclusive(x_291); -if (x_292 == 0) +x_238 = !lean_is_exclusive(x_237); +if (x_238 == 0) { -lean_object* x_293; -x_293 = lean_ctor_get(x_291, 0); -lean_dec(x_293); -lean_ctor_set_tag(x_291, 1); -lean_ctor_set(x_291, 0, x_287); -return x_291; +lean_object* x_239; +x_239 = lean_ctor_get(x_237, 0); +lean_dec(x_239); +lean_ctor_set_tag(x_237, 1); +lean_ctor_set(x_237, 0, x_233); +return x_237; } else { -lean_object* x_294; lean_object* x_295; -x_294 = lean_ctor_get(x_291, 1); -lean_inc(x_294); -lean_dec(x_291); -x_295 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_295, 0, x_287); -lean_ctor_set(x_295, 1, x_294); -return x_295; +lean_object* x_240; lean_object* x_241; +x_240 = lean_ctor_get(x_237, 1); +lean_inc(x_240); +lean_dec(x_237); +x_241 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_241, 0, x_233); +lean_ctor_set(x_241, 1, x_240); +return x_241; } } } else { -lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; uint8_t x_301; +lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; uint8_t x_247; lean_dec(x_2); -x_296 = lean_ctor_get(x_275, 0); -lean_inc(x_296); -x_297 = lean_ctor_get(x_275, 1); -lean_inc(x_297); -lean_dec(x_275); -x_298 = lean_ctor_get(x_297, 0); -lean_inc(x_298); -lean_dec(x_297); -x_299 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_300 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_299, x_3, x_298); +x_242 = lean_ctor_get(x_221, 0); +lean_inc(x_242); +x_243 = lean_ctor_get(x_221, 1); +lean_inc(x_243); +lean_dec(x_221); +x_244 = lean_ctor_get(x_243, 0); +lean_inc(x_244); +lean_dec(x_243); +x_245 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; +x_246 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_206, x_245, x_3, x_244); lean_dec(x_3); -x_301 = !lean_is_exclusive(x_300); -if (x_301 == 0) +x_247 = !lean_is_exclusive(x_246); +if (x_247 == 0) { -lean_object* x_302; -x_302 = lean_ctor_get(x_300, 0); -lean_dec(x_302); -lean_ctor_set_tag(x_300, 1); -lean_ctor_set(x_300, 0, x_296); -return x_300; +lean_object* x_248; +x_248 = lean_ctor_get(x_246, 0); +lean_dec(x_248); +lean_ctor_set_tag(x_246, 1); +lean_ctor_set(x_246, 0, x_242); +return x_246; } else { -lean_object* x_303; lean_object* x_304; -x_303 = lean_ctor_get(x_300, 1); -lean_inc(x_303); -lean_dec(x_300); -x_304 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_304, 0, x_296); -lean_ctor_set(x_304, 1, x_303); -return x_304; -} -} -} -else -{ -lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; lean_object* x_318; -x_305 = lean_ctor_get(x_265, 0); -x_306 = lean_ctor_get(x_265, 1); -x_307 = lean_ctor_get(x_265, 2); -x_308 = lean_ctor_get(x_265, 3); -x_309 = lean_ctor_get(x_265, 4); -x_310 = lean_ctor_get(x_265, 5); -lean_inc(x_310); -lean_inc(x_309); -lean_inc(x_308); -lean_inc(x_307); -lean_inc(x_306); -lean_inc(x_305); -lean_dec(x_265); -lean_inc(x_306); -x_311 = l_Lean_Meta_SynthInstance_mkTableKey(x_306, x_1); -lean_inc(x_306); -x_312 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_312, 0, x_305); -lean_ctor_set(x_312, 1, x_306); -lean_ctor_set(x_312, 2, x_307); -lean_ctor_set(x_312, 3, x_308); -lean_ctor_set(x_312, 4, x_309); -lean_ctor_set(x_312, 5, x_310); -x_313 = lean_box(0); -x_314 = l_Array_empty___closed__1; -x_315 = l_Lean_Meta_SynthInstance_main___closed__1; -x_316 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_316, 0, x_312); -lean_ctor_set(x_316, 1, x_313); -lean_ctor_set(x_316, 2, x_314); -lean_ctor_set(x_316, 3, x_314); -lean_ctor_set(x_316, 4, x_315); -x_317 = lean_box(1); -lean_inc(x_3); -x_318 = l_Lean_Meta_SynthInstance_newSubgoal(x_306, x_311, x_266, x_317, x_3, x_316); -if (lean_obj_tag(x_318) == 0) -{ -lean_object* x_319; lean_object* x_320; -x_319 = lean_ctor_get(x_318, 1); -lean_inc(x_319); -lean_dec(x_318); -lean_inc(x_3); -x_320 = l_Lean_Meta_SynthInstance_synth___main(x_2, x_3, x_319); -if (lean_obj_tag(x_320) == 0) -{ -lean_object* x_321; lean_object* x_322; lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; lean_object* x_327; lean_object* x_328; -x_321 = lean_ctor_get(x_320, 0); -lean_inc(x_321); -x_322 = lean_ctor_get(x_320, 1); -lean_inc(x_322); -lean_dec(x_320); -x_323 = lean_ctor_get(x_322, 0); -lean_inc(x_323); -lean_dec(x_322); -x_324 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_325 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_324, x_3, x_323); -lean_dec(x_3); -x_326 = lean_ctor_get(x_325, 1); -lean_inc(x_326); -if (lean_is_exclusive(x_325)) { - lean_ctor_release(x_325, 0); - lean_ctor_release(x_325, 1); - x_327 = x_325; -} else { - lean_dec_ref(x_325); - x_327 = lean_box(0); -} -if (lean_is_scalar(x_327)) { - x_328 = lean_alloc_ctor(0, 2, 0); -} else { - x_328 = x_327; -} -lean_ctor_set(x_328, 0, x_321); -lean_ctor_set(x_328, 1, x_326); -return x_328; -} -else -{ -lean_object* x_329; lean_object* x_330; lean_object* x_331; lean_object* x_332; lean_object* x_333; lean_object* x_334; lean_object* x_335; lean_object* x_336; -x_329 = lean_ctor_get(x_320, 0); -lean_inc(x_329); -x_330 = lean_ctor_get(x_320, 1); -lean_inc(x_330); -lean_dec(x_320); -x_331 = lean_ctor_get(x_330, 0); -lean_inc(x_331); -lean_dec(x_330); -x_332 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_333 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_332, x_3, x_331); -lean_dec(x_3); -x_334 = lean_ctor_get(x_333, 1); -lean_inc(x_334); -if (lean_is_exclusive(x_333)) { - lean_ctor_release(x_333, 0); - lean_ctor_release(x_333, 1); - x_335 = x_333; -} else { - lean_dec_ref(x_333); - x_335 = lean_box(0); -} -if (lean_is_scalar(x_335)) { - x_336 = lean_alloc_ctor(1, 2, 0); -} else { - x_336 = x_335; - lean_ctor_set_tag(x_336, 1); -} -lean_ctor_set(x_336, 0, x_329); -lean_ctor_set(x_336, 1, x_334); -return x_336; -} -} -else -{ -lean_object* x_337; lean_object* x_338; lean_object* x_339; lean_object* x_340; lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; -lean_dec(x_2); -x_337 = lean_ctor_get(x_318, 0); -lean_inc(x_337); -x_338 = lean_ctor_get(x_318, 1); -lean_inc(x_338); -lean_dec(x_318); -x_339 = lean_ctor_get(x_338, 0); -lean_inc(x_339); -lean_dec(x_338); -x_340 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__1; -x_341 = l___private_Init_Lean_Util_Trace_2__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(x_259, x_340, x_3, x_339); -lean_dec(x_3); -x_342 = lean_ctor_get(x_341, 1); -lean_inc(x_342); -if (lean_is_exclusive(x_341)) { - lean_ctor_release(x_341, 0); - lean_ctor_release(x_341, 1); - x_343 = x_341; -} else { - lean_dec_ref(x_341); - x_343 = lean_box(0); -} -if (lean_is_scalar(x_343)) { - x_344 = lean_alloc_ctor(1, 2, 0); -} else { - x_344 = x_343; - lean_ctor_set_tag(x_344, 1); -} -lean_ctor_set(x_344, 0, x_337); -lean_ctor_set(x_344, 1, x_342); -return x_344; +lean_object* x_249; lean_object* x_250; +x_249 = lean_ctor_get(x_246, 1); +lean_inc(x_249); +lean_dec(x_246); +x_250 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_250, 0, x_242); +lean_ctor_set(x_250, 1, x_249); +return x_250; } } } diff --git a/stage0/stdlib/Init/Lean/MetavarContext.c b/stage0/stdlib/Init/Lean/MetavarContext.c index 1c18959e4d..421607262c 100644 --- a/stage0/stdlib/Init/Lean/MetavarContext.c +++ b/stage0/stdlib/Init/Lean/MetavarContext.c @@ -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);