From 633578cfafacd4fd192827d52bc3596633d7f8fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 12:28:05 -0700 Subject: [PATCH] chore: use `StateRefT` macro --- src/Init/Control/StateRef.lean | 4 ++-- src/Lean/CoreM.lean | 2 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Meta/AbstractNestedProofs.lean | 2 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 2 +- src/Lean/MetavarContext.lean | 2 +- src/Lean/PrettyPrinter/Formatter.lean | 2 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 2 +- src/Lean/Util/MonadCache.lean | 16 ++++++++-------- tests/lean/run/finally.lean | 4 +--- tests/lean/run/stateRef.lean | 6 ++---- tests/lean/typeMismatch.lean.expected.out | 2 +- 15 files changed, 24 insertions(+), 28 deletions(-) diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 257070da00..38fd9d2115 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -10,8 +10,8 @@ import Init.System.IO import Init.Control.State def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α --- TODO: remove `[STWorld ω m]`. We should use a tactic for synthesizing ω, and the tactic infers the instance `[STWorld ω m]` -abbrev StateRefT {ω : Type} (σ : Type) (m : Type → Type) [STWorld ω m] (α : Type) := StateRefT' ω σ m α + +/- Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/ @[inline] def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do let ref ← ST.mkRef s diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 6d71248f0b..eeb5895eb1 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -28,7 +28,7 @@ structure Context := (maxRecDepth : Nat := 1000) (ref : Syntax := Syntax.missing) -abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception +abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception) instance {α} : Inhabited (CoreM α) := ⟨fun _ _ => throw $ arbitrary _⟩ diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 59b4488fe1..12a3c046be 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -50,7 +50,7 @@ structure Context := (currMacroScope : MacroScope := firstFrontendMacroScope) (ref : Syntax := Syntax.missing) -abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε +abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State (EIO ε) abbrev CommandElabM := CommandElabCoreM Exception abbrev CommandElab := Syntax → CommandElabM Unit abbrev Linter := Syntax → CommandElabM Unit diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 5d3fbcda6c..a8641ee851 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -36,7 +36,7 @@ structure BacktrackableState := (mctx : MetavarContext) (goals : List MVarId) -abbrev TacticM := ReaderT Context $ StateRefT State $ TermElabM +abbrev TacticM := ReaderT Context $ StateRefT State TermElabM abbrev Tactic := Syntax → TacticM Unit def saveBacktrackableState : TacticM BacktrackableState := do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f305356f5d..b5afeb0120 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -137,7 +137,7 @@ structure State := instance : Inhabited State := ⟨{}⟩ -abbrev TermElabM := ReaderT Context $ StateRefT State $ MetaM +abbrev TermElabM := ReaderT Context $ StateRefT State MetaM abbrev TermElab := Syntax → Option Expr → TermElabM Expr open Meta diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index a25f753e36..f82ff5c89e 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -21,7 +21,7 @@ structure Context := structure State := (nextIdx : Nat := 1) -abbrev M := ReaderT Context $ MonadCacheT Expr Expr $ StateRefT State $ MetaM +abbrev M := ReaderT Context $ MonadCacheT Expr Expr $ StateRefT State MetaM private def mkAuxLemma (e : Expr) : M Expr := do let ctx ← read diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 7fb1a80c67..606d8c5df0 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -111,7 +111,7 @@ structure Context := (lctx : LocalContext := {}) (localInstances : LocalInstances := #[]) -abbrev MetaM := ReaderT Context $ StateRefT State $ CoreM +abbrev MetaM := ReaderT Context $ StateRefT State CoreM instance : MonadIO MetaM := { liftIO := fun x => liftM (liftIO x : CoreM _) } diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index f47be183c4..aa6d2f284a 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -414,7 +414,7 @@ structure Context := (hasCtxLocals : Bool) (rhs : Expr) -abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ MetaM +abbrev CheckAssignmentM := ReaderT Context $ StateRefT State MetaM def throwCheckAssignmentFailure {α} : CheckAssignmentM α := throw $ Exception.internal checkAssignmentExceptionId diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index e3ac69ac60..fdf9e4cd17 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -594,7 +594,7 @@ def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext if !e.hasMVar then (e, mctx) else - let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext $ ST ω) Expr := + let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext (ST ω)) Expr := instantiateExprMVars e runST fun _ => instantiate e $.run $.run mctx diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index f41510aef8..84cf8f9db9 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -38,7 +38,7 @@ structure State := end Formatter -abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State $ CoreM +abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State CoreM @[inline] def FormatterM.orelse {α} (p₁ p₂ : FormatterM α) : FormatterM α := do let s ← get diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 528ba5a5e0..14f1729ab5 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -100,7 +100,7 @@ structure Context := end Parenthesizer -abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateRefT Parenthesizer.State $ CoreM +abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateRefT Parenthesizer.State CoreM abbrev Parenthesizer := ParenthesizerM Unit @[inline] def ParenthesizerM.orelse {α} (p₁ p₂ : ParenthesizerM α) : ParenthesizerM α := do diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index b88d48bf9f..319de8d267 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/src/Lean/Util/MonadCache.lean @@ -59,18 +59,18 @@ namespace MonadCacheT variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [HasBeq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := -{ getCache := (get : StateRefT _ _ _), - modifyCache := fun f => (modify f : StateRefT _ _ _) } +{ getCache := (get : StateRefT' ..), + modifyCache := fun f => (modify f : StateRefT' ..) } @[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ := x.run' Std.mkHashMap -instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT _ _)) -instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT _ _)) -instance [MonadIO m] : MonadIO (MonadCacheT α β m) := inferInstanceAs (MonadIO (StateRefT _ _)) -instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateRefT _ _)) -instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT _ _)) -instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT _ _)) +instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _)) +instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _)) +instance [MonadIO m] : MonadIO (MonadCacheT α β m) := inferInstanceAs (MonadIO (StateRefT' _ _ _)) +instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateRefT' _ _ _)) +instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT' _ _ _)) +instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT' _ _ _)) end MonadCacheT end Lean diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean index 3a2e1e7850..3d4ab08949 100644 --- a/tests/lean/run/finally.lean +++ b/tests/lean/run/finally.lean @@ -1,9 +1,7 @@ - - def checkM (b : IO Bool) : IO Unit := unlessM b (throw $ IO.userError "failed") -abbrev M := ExceptT String $ StateRefT Nat $ IO +abbrev M := ExceptT String $ StateRefT Nat IO def f1 : M Nat := throw "error 1" diff --git a/tests/lean/run/stateRef.lean b/tests/lean/run/stateRef.lean index 1893c34850..fdaae76ea0 100644 --- a/tests/lean/run/stateRef.lean +++ b/tests/lean/run/stateRef.lean @@ -1,5 +1,3 @@ - - def f (v : Nat) : StateRefT Nat IO Nat := do IO.println "hello" modify fun s => s - v @@ -41,7 +39,7 @@ instance monadState.hasGetAt (β : Type) (v : β) (α : Type) (m : Type → Type export HasGetAt (getAt) -abbrev M := StateRefT (Label 0 Nat) $ StateRefT (Label 1 Nat) $ StateRefT (Label 2 Nat) IO +abbrev M := StateRefT (Label 0 Nat) (StateRefT (Label 1 Nat) (StateRefT (Label 2 Nat) IO)) def f4 : M Nat := do let a0 : Nat ← getAt 0 @@ -54,7 +52,7 @@ pure (a0 + a1 + a2) #eval f4.run' ⟨10⟩ $.run' ⟨20⟩ $.run' ⟨30⟩ -abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω +abbrev S (ω : Type) := StateRefT Nat (StateRefT String (ST ω)) def f5 {ω} : S ω Unit := do let s ← getThe String diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out index a73d8f455b..fa2d061a67 100644 --- a/tests/lean/typeMismatch.lean.expected.out +++ b/tests/lean/typeMismatch.lean.expected.out @@ -7,6 +7,6 @@ but is expected to have type typeMismatch.lean:12:0: error: type mismatch Meta.isDefEq x x has type - ReaderT Meta.Context (StateRefT Meta.State CoreM) Bool + ReaderT Meta.Context (StateRefT' IO.RealWorld Meta.State CoreM) Bool but is expected to have type MetaM Unit