From 159b45c74fcb16f6f3ef49d7b76ce86efdf4db79 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 13 Dec 2017 14:27:12 +0100
Subject: [PATCH] refactor(init/category/state): introduce `monad_state`

* rename `read/write` to `get/put`, as in Haskell
* define `state` as `state_t id`
---
 doc/changes.md                                |   1 +
 leanpkg/leanpkg/resolve.lean                  |   8 +-
 library/init/category/state.lean              | 164 ++++++++----------
 library/init/category/transformers.lean       |  13 +-
 library/init/meta/smt/smt_tactic.lean         |   9 +-
 tests/lean/interactive/my_tac_class.lean      |   9 +-
 .../my_tac_class.lean.expected.out            |   4 +-
 tests/lean/interactive/rb_map_ts.lean         |   9 +-
 .../interactive/rb_map_ts.lean.expected.out   |  14 +-
 tests/lean/run/io_state.lean                  |   6 +-
 tests/lean/run/my_tac_class.lean              |   9 +-
 tests/lean/run/stateT1.lean                   |  32 ----
 12 files changed, 118 insertions(+), 160 deletions(-)
 delete mode 100644 tests/lean/run/stateT1.lean

diff --git a/doc/changes.md b/doc/changes.md
index 93c346da03..89ecbe2169 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -240,6 +240,7 @@ master branch (aka work in progress branch)
 
 * `monad.{monad_transformer,has_monad_lift(_t)}` ~> `{monad_transformer,has_monad_lift(_t)}`
 * `monad.map_comp` ~> `comp_map`
+* `state(_t).{read,write}` ~> `{get,put}` (general operations defined on any `monad_state`)
 
 v3.3.0 (14 September 2017)
 -------------
diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean
index a8d28f66f4..c1dc7a328d 100644
--- a/leanpkg/leanpkg/resolve.lean
+++ b/leanpkg/leanpkg/resolve.lean
@@ -32,11 +32,11 @@ end assignment
 instance {α : Type} : has_coe (io α) (solver α) := ⟨state_t.lift⟩
 
 def not_yet_assigned (d : string) : solver bool := do
-assg ← state_t.read,
+assg ← get,
 return $ ¬ assg.contains d
 
 def resolved_path (d : string) : solver string := do
-assg ← state_t.read,
+assg ← get,
 some path ← return (assg.find d) | io.fail "",
 return path
 
@@ -58,7 +58,7 @@ match dep.src with
 | (source.path dir) := do
   let depdir := resolve_dir dir relpath,
   io.put_str_ln $ dep.name ++ ": using local path " ++ depdir,
-  state_t.modify $ λ assg, assg.insert dep.name depdir
+  modify $ λ assg, assg.insert dep.name depdir
 | (source.git url rev) := do
   let depdir := "_target/deps/" ++ dep.name,
   already_there ← dir_exists depdir,
@@ -75,7 +75,7 @@ match dep.src with
   },
   hash ← git_parse_origin_revision depdir rev,
   exec_cmd {cmd := "git", args := ["checkout", "--detach", hash], cwd := depdir},
-  state_t.modify $ λ assg, assg.insert dep.name depdir
+  modify $ λ assg, assg.insert dep.name depdir
 end
 
 def solve_deps_core : ∀ (rel_path : string) (d : manifest) (max_depth : ℕ), solver unit
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index a1d582fab5..4b35eb6d93 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -1,128 +1,114 @@
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import init.meta.interactive
+import init.category.id
 import init.category.lawful
+import init.category.transformers
 universes u v
 
-def state (σ α : Type u) : Type u :=
-σ → α × σ
+class monad_state (σ : out_param (Type u)) (m : Type u → Type v) [monad m] :=
+(state : Π {α : Type u}, (σ → (α × σ)) → m α)
+(get : m σ := state (λ s, (s, s)))
+(put : σ → m punit := λ s, state (λ _, (punit.star, s)))
+-- TODO: `match` in structures
+--(state := λ α f, do (a,s) ← f <$> get, put s, pure a)
+(state := λ α f, do p ← f <$> get, put p.2, pure p.1)
 
 section
-variables {σ α β : Type u}
-
-@[inline] def state_return (a : α) : state σ α :=
-λ s, (a, s)
-
-@[inline] def state_bind (a : state σ α) (b : α → state σ β) : state σ β :=
-λ s, match (a s) with (a', s') := b a' s' end
-
-instance (σ : Type u) : lawful_monad (state σ) :=
-{pure := @state_return σ, bind := @state_bind σ,
- id_map := begin
-   intros, funext,
-   simp [state_bind], cases x s,
-   apply rfl
- end,
- pure_bind := by intros; apply rfl,
- bind_assoc := begin
-   intros, funext,
-   simp [state_bind], cases x s,
-   apply rfl
- end}
+variables {σ : Type u} {m : Type u → Type v} [monad m] [monad_state σ m]
+@[inline] def get : m σ := monad_state.get _ _
+@[inline] def put' : σ → m punit := monad_state.put _
+@[inline] def modify' (f : σ → σ) : m punit := monad_state.state _ (λ s, (punit.star, f s))
 end
 
-namespace state
-@[inline] def read {σ : Type u} : state σ σ :=
-λ s, (s, s)
+section
+variables {σ : Type} {m : Type → Type v} [monad m] [monad_state σ m]
+@[inline] def put : σ → m unit := λ s, put' s $> ()
+@[inline] def modify (f : σ → σ) : m unit := modify' f $> ()
+end
 
-@[inline] def write {σ : Type} : σ → state σ unit :=
-λ s' s, ((), s')
+instance monad_state_lift (s m m') [has_monad_lift m m'] [monad m] [monad_state s m] [monad m'] : monad_state s m' :=
+{ get := monad_lift (monad_state.get _ m),
+  put := monad_lift ∘ monad_state.put m,
+  state := λ α, monad_lift ∘ monad_state.state m }
 
-@[inline] def write' {σ : Type u} : σ → state σ punit :=
-λ s' s, (punit.star, s')
-end state
 
 def state_t (σ : Type u) (m : Type u → Type v) [monad m] (α : Type u) : Type (max u v) :=
 σ → m (α × σ)
 
+namespace state_t
 section
   variable  {σ : Type u}
   variable  {m : Type u → Type v}
   variable  [monad m]
   variables {α β : Type u}
 
-  def state_t_return (a : α) : state_t σ m α :=
+  protected def return (a : α) : state_t σ m α :=
   λ s, show m (α × σ), from
     return (a, s)
 
-  def state_t_bind (act₁ : state_t σ m α) (act₂ : α → state_t σ m β) : state_t σ m β :=
+  protected def bind (act₁ : state_t σ m α) (act₂ : α → state_t σ m β) : state_t σ m β :=
   λ s, show m (β × σ), from
      do (a, new_s) ← act₁ s,
         act₂ a new_s
-end
 
-instance (σ : Type u) (m : Type u → Type v) [monad m] : monad (state_t σ m) :=
-{pure := @state_t_return σ m _, bind := @state_t_bind σ m _}
+  instance : monad (state_t σ m) :=
+  { pure := @state_t.return σ m _, bind := @state_t.bind σ m _ }
 
-instance (σ : Type u) (m : Type u → Type v) [lawful_monad m] : lawful_monad (state_t σ m) :=
-{pure := @state_t_return σ m _, bind := @state_t_bind σ m _,
- id_map := begin
-   intros, funext,
-   simp [state_t_bind, state_t_return, function.comp, return],
-   have h : state_t_bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
-   { funext s, cases s, apply rfl },
-   { simp [h, bind_pure] },
- end,
- pure_bind := begin
-   intros, funext,
-   simp [state_t_bind, state_t_return, pure_bind]
- end,
- bind_assoc := begin
-   intros, funext,
-   simp [state_t_bind, state_t_return, bind_assoc],
-   apply congr_arg, funext r,
-   cases r, refl
- end}
+  instance (m : Type u → Type v) [lawful_monad m] : lawful_monad (state_t σ m) :=
+  {id_map := begin
+    intros, funext,
+    simp [(<$>), state_t.bind, state_t.return, function.comp, return],
+    have h : state_t.bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
+    { funext s, cases s; refl },
+    { simp [h, bind_pure] },
+  end,
+  pure_bind := begin
+    intros, funext,
+    simp [bind, has_pure.pure, state_t.bind, state_t.return, pure_bind]
+  end,
+  bind_assoc := begin
+    intros, funext,
+    simp [bind, state_t.bind, state_t.return, bind_assoc],
+    apply congr_arg, funext r,
+    cases r, refl
+  end, ..state_t.monad}
 
-section
-  variable  {σ : Type u}
-  variable  {m : Type u → Type v}
-  variable  [monad m]
-  variable  [alternative m]
-  variable  {α : Type u}
-
-  def state_t_orelse (act₁ act₂ : state_t σ m α) : state_t σ m α :=
+  protected def orelse [alternative m] (α : Type u) (act₁ act₂ : state_t σ m α) : state_t σ m α :=
   λ s, act₁ s <|> act₂ s
 
-  def state_t_failure : state_t σ m α :=
+  protected def failure [alternative m] (α : Type u) : state_t σ m α :=
   λ s, failure
+
+  instance [alternative m] : alternative (state_t σ m) :=
+  { failure := @state_t.failure σ m _ _,
+    orelse  := @state_t.orelse σ m _ _,
+    ..state_t.monad }
+
+  protected def get : state_t σ m σ :=
+  λ s, return (s, s)
+
+  protected def put : σ → state_t σ m punit :=
+  λ s' s, return (punit.star, s')
+
+  protected def state {α : Type u} (f : σ → (α × σ)) : state_t σ m α :=
+  pure ∘ f
+
+  protected def lift {α : Type u} (t : m α) : state_t σ m α :=
+  λ s, do a ← t, return (a, s)
+
+  instance : monad_state σ (state_t σ m) :=
+  { get := state_t.get, put := state_t.put,
+    state := @state_t.state _ _ _ }
+
+  instance : monad_transformer (state_t σ) :=
+  { is_monad := @state_t.monad σ,
+    monad_lift := @state_t.lift σ }
 end
-
-instance (σ : Type u) (m : Type u → Type v) [alternative m] [monad m] : alternative (state_t σ m) :=
-{ failure := @state_t_failure σ m _ _,
-  orelse  := @state_t_orelse σ m _ _,
-  ..state_t.monad σ m }
-
-namespace state_t
-def read {σ : Type u} {m : Type u → Type v} [monad m] : state_t σ m σ :=
-λ s, return (s, s)
-
-def write {σ : Type} {m : Type → Type v} [monad m] : σ → state_t σ m unit :=
-λ s' s, return ((), s')
-
-def write' {σ : Type u} {m : Type u → Type v} [monad m] : σ → state_t σ m punit :=
-λ s' s, return (punit.star, s')
-
-def modify {σ : Type} {m : Type → Type v} [monad m] (f : σ → σ) : state_t σ m unit :=
-do s ← read, write (f s)
-
-def modify' {σ : Type u} {m : Type u → Type v} [monad m] (f : σ → σ) : state_t σ m punit :=
-do s ← read, write' (f s)
-
-def lift {α σ : Type u} {m : Type u → Type v} [monad m] (t : m α) : state_t σ m α :=
-λ s, do a ← t, return (a, s)
 end state_t
+
+@[reducible] def state (σ α : Type u) : Type u := state_t σ id α
diff --git a/library/init/category/transformers.lean b/library/init/category/transformers.lean
index 51ecac7840..5c1241f6d2 100644
--- a/library/init/category/transformers.lean
+++ b/library/init/category/transformers.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import init.category.state init.function init.coe
+import init.function init.coe
+import init.category.monad
 
 universes u v w
 
@@ -35,13 +36,3 @@ instance has_monad_lift_t_trans (m n o) [has_monad_lift n o] [has_monad_lift_t m
 
 instance has_monad_lift_t_refl (m) [monad m] : has_monad_lift_t m m :=
 ⟨λ α, id⟩
-
-namespace state_t
-
-def state_t_monad_lift (S) (m) [monad m] (α) (f : m α) : state_t S m α :=
-assume state, do res ← f, return (res, state)
-
-instance (S) : monad_transformer (state_t S) :=
-⟨state_t.monad S, state_t_monad_lift S⟩
-
-end state_t
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index ffb719504d..bf2f6cf237 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -60,7 +60,10 @@ meta instance : has_append smt_state :=
 list.has_append
 
 meta instance : monad smt_tactic :=
-state_t.monad _ _
+state_t.monad
+
+meta instance : monad_state smt_state smt_tactic :=
+state_t.monad_state
 
 /- We don't use the default state_t lift operation because only
    tactics that do not change hypotheses can be automatically lifted to smt_tactic. -/
@@ -174,7 +177,7 @@ iterate (ematch >> try close)
 open tactic
 
 protected meta def read : smt_tactic (smt_state × tactic_state) :=
-do s₁ ← state_t.read,
+do s₁ ← get,
    s₂ ← tactic.read,
    return (s₁, s₂)
 
@@ -218,7 +221,7 @@ meta def to_expr (q : pexpr) (allow_mvars := tt) : smt_tactic expr :=
 tactic.to_expr q allow_mvars
 
 meta def classical : smt_tactic bool :=
-do s ← state_t.read,
+do s ← get,
    return s.classical
 
 meta def num_goals : smt_tactic nat :=
diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean
index 3a6cae926f..f24564621f 100644
--- a/tests/lean/interactive/my_tac_class.lean
+++ b/tests/lean/interactive/my_tac_class.lean
@@ -2,7 +2,10 @@ meta def mytac :=
 state_t nat tactic
 
 meta instance : monad mytac :=
-state_t.monad _ _
+state_t.monad
+
+meta instance : monad_state nat mytac :=
+state_t.monad_state
 
 meta instance : has_monad_lift tactic mytac :=
 monad_transformer_lift (state_t nat) tactic
@@ -29,7 +32,7 @@ meta def execute (tac : mytac unit) : tactic unit :=
 tac 0 >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
-do v ← state_t.read,
+do v ← get,
    s ← tactic.read,
    tactic.save_info_thunk p
       (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++
@@ -49,7 +52,7 @@ meta def assumption : mytac unit :=
 tactic.assumption
 
 meta def inc : mytac unit :=
-do v ← state_t.read, state_t.write (v+1)
+modify (+1)
 
 end interactive
 end mytac
diff --git a/tests/lean/interactive/my_tac_class.lean.expected.out b/tests/lean/interactive/my_tac_class.lean.expected.out
index 0e28d1954d..70b2b4d5d4 100644
--- a/tests/lean/interactive/my_tac_class.lean.expected.out
+++ b/tests/lean/interactive/my_tac_class.lean.expected.out
@@ -1,3 +1,3 @@
-{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":61,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":64,"severity":"information","text":"test\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"Custom state: 2\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":65}
+{"record":{"source":,"state":"Custom state: 2\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":68}
diff --git a/tests/lean/interactive/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean
index 0d6a8ade1d..7712118a0a 100644
--- a/tests/lean/interactive/rb_map_ts.lean
+++ b/tests/lean/interactive/rb_map_ts.lean
@@ -2,7 +2,10 @@ meta def mytac :=
 state_t (name_map nat) tactic
 
 meta instance : monad mytac :=
-state_t.monad _ _
+state_t.monad
+
+meta instance : monad_state (name_map nat) mytac :=
+state_t.monad_state
 
 meta instance : has_monad_lift tactic mytac :=
 monad_transformer_lift (state_t (name_map nat)) tactic
@@ -30,7 +33,7 @@ meta def execute (tac : mytac unit) : tactic unit :=
 tac (name_map.mk nat) >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
-do v ← state_t.read,
+do v ← get,
    s ← tactic.read,
    tactic.save_info_thunk p
       (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++
@@ -54,7 +57,7 @@ open interactive
 open interactive.types
 
 meta def add (n : parse ident) (v : nat) : mytac unit :=
-do m ← state_t.read, state_t.write (m^.insert n v)
+modify (λ m, m.insert n v)
 
 end interactive
 end mytac
diff --git a/tests/lean/interactive/rb_map_ts.lean.expected.out b/tests/lean/interactive/rb_map_ts.lean.expected.out
index 430b846f95..214887f481 100644
--- a/tests/lean/interactive/rb_map_ts.lean.expected.out
+++ b/tests/lean/interactive/rb_map_ts.lean.expected.out
@@ -1,8 +1,8 @@
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":89,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":84,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":84,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":92,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":92,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":67}
-{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":71}
-{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":85}
+{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":70}
+{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":74}
+{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":88}
diff --git a/tests/lean/run/io_state.lean b/tests/lean/run/io_state.lean
index 5f27496286..a243dba5a1 100644
--- a/tests/lean/run/io_state.lean
+++ b/tests/lean/run/io_state.lean
@@ -7,10 +7,10 @@ instance lift_io {α} : has_coe (io α) (my_io α) :=
 ⟨state_t.lift⟩
 
 def tst : my_io unit :=
-do x ← read,
+do x ← get,
    print_ln x,
-   write (x+10),
-   y ← read,
+   put (x+10),
+   y ← get,
    print_ln y,
    put_str "end of program"
 
diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean
index a99e5d8136..911b053a17 100644
--- a/tests/lean/run/my_tac_class.lean
+++ b/tests/lean/run/my_tac_class.lean
@@ -2,7 +2,10 @@ meta def mytac :=
 state_t nat tactic
 
 meta instance : monad mytac :=
-state_t.monad _ _
+state_t.monad
+
+meta instance : monad_state nat mytac :=
+state_t.monad_state
 
 meta instance : has_monad_lift tactic mytac :=
 monad_transformer_lift (state_t nat) tactic
@@ -30,7 +33,7 @@ meta def execute (tac : mytac unit) : tactic unit :=
 tac 0 >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
-do v ← state_t.read,
+do v ← get,
    s ← tactic.read,
    tactic.save_info_thunk p
       (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++
@@ -50,7 +53,7 @@ meta def assumption : mytac unit :=
 tactic.assumption
 
 meta def inc : mytac unit :=
-do v ← state_t.read, state_t.write (v+1)
+modify (+1)
 
 end interactive
 end mytac
diff --git a/tests/lean/run/stateT1.lean b/tests/lean/run/stateT1.lean
deleted file mode 100644
index 6653ede88b..0000000000
--- a/tests/lean/run/stateT1.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-meta definition mytactic (A : Type) := state_t (list nat) tactic A
-
-attribute [instance]
-meta definition mytactic_is_monad : monad mytactic :=
-@state_t.monad _ _ _
-
-meta definition read_lst : mytactic (list nat) :=
-state_t.read
-
-meta definition write_lst : list nat → mytactic unit :=
-state_t.write
-
-meta definition foo : mytactic unit :=
-write_lst [10, 20]
-
-meta definition ins (a : nat) : mytactic unit :=
-do l : list nat ← read_lst,
-   write_lst (a :: l)
-
-meta definition invoke (s : list nat) (m : mytactic unit) : tactic (list nat) :=
-do (u, s') ← m s, return s'
-
-meta definition tactic_to_mytactic {A : Type} (t : tactic A) : mytactic A :=
-λ s, do a : A ← t, return (a, s)
-
-open tactic
-
-example : list nat :=
-by do
-   l : list nat ← invoke [] (foo >> ins 30 >> tactic_to_mytactic (trace "foo") >> ins 40),
-   trace l,
-   mk_const `list.nil >>= apply