refactor(init/category): make all monad transformers structures, replace monad classes with has_monad_lift_t wrappers
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
8c157eba64
commit
69cfdbd290
17 changed files with 195 additions and 191 deletions
|
|
@ -124,7 +124,7 @@ def fixup_git_version (dir : string) : ∀ (src : source), io source
|
|||
| src := return src
|
||||
|
||||
def add (dep : dependency) : io unit := do
|
||||
(_, assg) ← materialize "." dep assignment.empty,
|
||||
(_, assg) ← (materialize "." dep).run assignment.empty,
|
||||
some downloaded_path ← return (assg.find dep.name),
|
||||
manif ← manifest.from_file (downloaded_path ++ "/" ++ leanpkg_toml_fn),
|
||||
src ← fixup_git_version downloaded_path dep.src,
|
||||
|
|
|
|||
|
|
@ -92,7 +92,7 @@ deps.mmap' $ λ dep, do
|
|||
solve_deps_core p d' max_depth
|
||||
|
||||
def solve_deps (d : manifest) : io assignment := do
|
||||
(_, assg) ← solve_deps_core "." d 1024 $ assignment.empty.insert d.name ".",
|
||||
(_, assg) ← (solve_deps_core "." d 1024).run $ assignment.empty.insert d.name ".",
|
||||
return assg
|
||||
|
||||
def construct_path_core (depname : string) (dirname : string) : io (list string) :=
|
||||
|
|
|
|||
|
|
@ -34,9 +34,6 @@ section
|
|||
| (except.error err) := except.error err
|
||||
| (except.ok v) := f v
|
||||
end
|
||||
|
||||
instance monad : monad (except ε) :=
|
||||
{ map := @map, pure := @return, bind := @bind }
|
||||
end
|
||||
end except
|
||||
|
||||
|
|
@ -52,14 +49,12 @@ section
|
|||
protected def return {α : Type u} (a : α) : except_t ε m α :=
|
||||
⟨pure $ except.ok a⟩
|
||||
|
||||
protected def map {α β : Type u} (f : α → β) (ma : except_t ε m α) : except_t ε m β :=
|
||||
⟨has_map.map f <$> ma.run⟩
|
||||
protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
|
||||
| (except.ok a) := (f a).run
|
||||
| (except.error e) := pure (except.error e)
|
||||
|
||||
protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
|
||||
⟨ma.run >>= λ res, match res with
|
||||
| except.ok a := (f a).run
|
||||
| except.error e := pure (except.error e)
|
||||
end⟩
|
||||
⟨ma.run >>= bind_cont f⟩
|
||||
|
||||
protected def lift {α : Type u} (t : m α) : except_t ε m α :=
|
||||
⟨except.ok <$> t⟩
|
||||
|
|
@ -71,7 +66,7 @@ section
|
|||
end⟩
|
||||
|
||||
instance : monad (except_t ε m) :=
|
||||
{ pure := @return, map := @map, bind := @bind }
|
||||
{ pure := @return, bind := @bind }
|
||||
end
|
||||
|
||||
instance (ε : Type u) : monad_transformer (except_t ε) :=
|
||||
|
|
|
|||
|
|
@ -76,59 +76,91 @@ lemma map_ext_congr {α β} {m : Type u → Type v} [has_map m] {x : m α} {f :
|
|||
|
||||
-- instances of previously defined monads
|
||||
|
||||
namespace state_t
|
||||
section
|
||||
variable {σ : Type u}
|
||||
variable {m : Type u → Type v}
|
||||
variable [monad m]
|
||||
variables {α β : Type u}
|
||||
variables (x : state_t σ m α) (st : σ)
|
||||
|
||||
lemma ext {x x' : state_t σ m α} (h : ∀ st, x.run st = x'.run st) : x = x' :=
|
||||
by cases_type* state_t; simp [show x = x', from funext h]
|
||||
|
||||
@[simp] lemma run_pure (a) : (pure a : state_t σ m α).run st = pure (a, st) := rfl
|
||||
@[simp] lemma run_bind (f : α → state_t σ m β) : (x >>= f).run st = x.run st >>= λ p, (f p.1).run p.2 :=
|
||||
by simp [bind, state_t.bind, state_t.run]; rw bind_ext_congr; intro a; cases a; simp [state_t.bind, state_t.run]
|
||||
@[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run st = (λ p : α × σ, (f (prod.fst p), prod.snd p)) <$> x.run st :=
|
||||
begin
|
||||
rw ←bind_pure_comp_eq_map m,
|
||||
change (x >>= pure ∘ f).run st = _,
|
||||
simp
|
||||
end
|
||||
end
|
||||
end state_t
|
||||
|
||||
instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (σ : Type u) : is_lawful_monad (state_t σ m) :=
|
||||
{ id_map := begin
|
||||
intros, funext,
|
||||
simp [(<$>), state_t.bind, state_t.return, function.comp, return],
|
||||
rw [bind_ext_congr pure], swap,
|
||||
{ intros, cases a, refl },
|
||||
{ simp [bind_pure] }
|
||||
end,
|
||||
pure_bind := begin
|
||||
intros, funext,
|
||||
simp [bind, pure, 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 }
|
||||
{ id_map := by intros; apply state_t.ext; intro; simp; erw id_map,
|
||||
pure_bind := by intros; apply state_t.ext; intro; simp,
|
||||
bind_assoc := by intros; apply state_t.ext; intro; simp [bind_assoc] }
|
||||
|
||||
|
||||
instance (ε : Type u) : is_lawful_monad (except ε) :=
|
||||
{ id_map := begin intros, cases x; refl, end,
|
||||
pure_bind := begin intros; refl end,
|
||||
bind_pure_comp_eq_map := begin intros, cases x; refl end,
|
||||
bind_assoc := begin intros, cases x; reflexivity end }
|
||||
namespace except_t
|
||||
variables {α β ε : Type u} {m : Type u → Type v} [monad m] (x : except_t ε m α)
|
||||
|
||||
local attribute [simp] except_t.map except_t.bind except_t.return except_t.monad
|
||||
lemma ext {x x' : except_t ε m α} (h : x.run = x'.run) : x = x' :=
|
||||
by cases_type* except_t; simp * at *
|
||||
|
||||
@[simp] lemma run_pure (a) : (pure a : except_t ε m α).run = pure (@except.ok ε α a) := rfl
|
||||
@[simp] lemma run_bind (f : α → except_t ε m β) : (x >>= f).run = x.run >>= except_t.bind_cont f := rfl
|
||||
@[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run = except.map f <$> x.run :=
|
||||
begin
|
||||
rw ←bind_pure_comp_eq_map m,
|
||||
change (x >>= pure ∘ f).run = _,
|
||||
simp,
|
||||
rw [bind_ext_congr],
|
||||
intro a; cases a; simp [except_t.bind_cont, except.map]
|
||||
end
|
||||
end except_t
|
||||
|
||||
instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) : is_lawful_monad (except_t ε m) :=
|
||||
{ id_map := begin
|
||||
intros, cases x, dsimp,
|
||||
rw map_ext_congr id; simp
|
||||
intros, apply except_t.ext, simp,
|
||||
rw [map_ext_congr, id_map],
|
||||
intro a, cases a; refl
|
||||
end,
|
||||
bind_pure_comp_eq_map := begin
|
||||
intros, cases x, dsimp,
|
||||
intros, apply except_t.ext, simp,
|
||||
rw [bind_ext_congr, bind_pure_comp_eq_map],
|
||||
intro a, cases a; dsimp [except.monad, except.map]; refl
|
||||
intro a, cases a; refl
|
||||
end,
|
||||
bind_assoc := begin
|
||||
intros, cases x, dsimp, simp [bind_assoc],
|
||||
intros, apply except_t.ext, simp [bind_assoc],
|
||||
rw [bind_ext_congr],
|
||||
{ intro a, cases a; simp }
|
||||
{ intro a, cases a; simp [except_t.bind_cont] }
|
||||
end,
|
||||
pure_bind := begin
|
||||
intros, dsimp, simp,
|
||||
cases f x, refl
|
||||
end,
|
||||
..except_t.monad }
|
||||
pure_bind := by intros; apply except_t.ext; simp [except_t.bind_cont] }
|
||||
|
||||
|
||||
local attribute [simp] reader_t.bind reader_t.pure
|
||||
namespace reader_t
|
||||
section
|
||||
variable {r : Type u}
|
||||
variable {m : Type u → Type v}
|
||||
variable [monad m]
|
||||
variables {α β : Type u}
|
||||
variables (x : reader_t r m α) (cfg : r)
|
||||
|
||||
lemma ext {x x' : reader_t r m α} (h : ∀ cfg, x.run cfg = x'.run cfg) : x = x' :=
|
||||
by cases_type* reader_t; simp [show x = x', from funext h]
|
||||
|
||||
@[simp] lemma run_pure (a) : (pure a : reader_t r m α).run cfg = pure a := rfl
|
||||
@[simp] lemma run_bind (f : α → reader_t r m β) : (x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
|
||||
@[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run cfg = f <$> x.run cfg :=
|
||||
by rw ←bind_pure_comp_eq_map m; refl
|
||||
end
|
||||
end reader_t
|
||||
|
||||
instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t r m) :=
|
||||
{ id_map := by intros; dsimp [reader_t.monad]; simp,
|
||||
pure_bind := by intros; dsimp [reader_t.monad]; simp,
|
||||
bind_assoc := by intros; dsimp [reader_t.monad]; simp [bind_assoc] }
|
||||
{ id_map := by intros; apply reader_t.ext; intro; simp,
|
||||
pure_bind := by intros; apply reader_t.ext; intro; simp,
|
||||
bind_assoc := by intros; apply reader_t.ext; intro; simp [bind_assoc] }
|
||||
|
|
|
|||
|
|
@ -8,16 +8,8 @@ prelude
|
|||
import init.category.transformers init.category.id
|
||||
universes u v w
|
||||
|
||||
class monad_reader (r : out_param (Type u)) (m : Type u → Type v) [monad m] :=
|
||||
(reader {} {α : Type u} : (r → α) → m α)
|
||||
(read {} : m r := reader id)
|
||||
(reader := λ α f, f <$> read)
|
||||
|
||||
|
||||
export monad_reader (read)
|
||||
|
||||
def reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
r → m α
|
||||
structure reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
(run : r → m α)
|
||||
|
||||
@[reducible] def reader (r : Type u) := reader_t r id
|
||||
|
||||
|
|
@ -29,31 +21,41 @@ section
|
|||
variables {α β : Type u}
|
||||
|
||||
protected def read : reader_t r m r :=
|
||||
λ r, pure r
|
||||
|
||||
protected def run : r → reader_t r m α → m α :=
|
||||
λ r x, x r
|
||||
⟨pure⟩
|
||||
|
||||
protected def pure (a : α) : reader_t r m α :=
|
||||
λ r, pure a
|
||||
⟨λ r, pure a⟩
|
||||
|
||||
protected def bind (x : reader_t r m α) (f : α → reader_t r m β) : reader_t r m β :=
|
||||
λ r, do a ← x r,
|
||||
f a r
|
||||
⟨λ r, do a ← x.run r,
|
||||
(f a).run r⟩
|
||||
|
||||
instance : monad (reader_t r m) :=
|
||||
{ pure := @reader_t.pure _ _ _, bind := @reader_t.bind _ _ _ }
|
||||
|
||||
protected def lift (a : m α) : reader_t r m α :=
|
||||
λ r, a
|
||||
⟨λ r, a⟩
|
||||
|
||||
instance (m) [monad m] : has_monad_lift m (reader_t r m) :=
|
||||
⟨@reader_t.lift r m _⟩
|
||||
|
||||
protected def map {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
|
||||
λ x, ⟨λ r, f (x.run r)⟩
|
||||
|
||||
instance (r m m') [monad m] [monad m'] : monad_functor m m' (reader_t r m) (reader_t r m') :=
|
||||
⟨@reader_t.map r m m' _ _⟩
|
||||
end
|
||||
end reader_t
|
||||
|
||||
def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
|
||||
λ x r, x (f r)
|
||||
class monad_reader_lift (r : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
|
||||
[has_lift : has_monad_lift_t (reader_t r m) n]
|
||||
|
||||
attribute [instance] monad_reader_lift.mk
|
||||
local attribute [instance] monad_reader_lift.has_lift
|
||||
|
||||
def monad_reader_lift.read {r : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift r m n] : n r :=
|
||||
@monad_lift _ _ _ _ (reader_t.read : reader_t r m _)
|
||||
export monad_reader_lift (read)
|
||||
|
||||
class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
|
||||
[functor {} : monad_functor_t (reader_t r m) (reader_t r' m) n n']
|
||||
|
|
@ -61,17 +63,8 @@ class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u
|
|||
attribute [instance] monad_reader_functor.mk
|
||||
local attribute [instance] monad_reader_functor.functor
|
||||
|
||||
def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
|
||||
λ x, ⟨λ r, x.run (f r)⟩
|
||||
|
||||
def with_reader {r r'} {m n n'} [monad m] [monad_reader_functor r r' m n n'] {α : Type u} (f : r' → r) : n α → n' α :=
|
||||
monad_map $ λ α, (with_reader_t f : reader_t r m α → reader_t r' m α)
|
||||
|
||||
def map_reader_t {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
|
||||
λ x r, f (x r)
|
||||
|
||||
instance (r m m') [monad m] [monad m'] : monad_functor m m' (reader_t r m) (reader_t r m') :=
|
||||
⟨@map_reader_t r m m' _ _⟩
|
||||
|
||||
instance (r m) [monad m] : monad_reader r (reader_t r m) :=
|
||||
{ reader := λ α f, pure ∘ f }
|
||||
|
||||
instance monad_reader_lift (r m m') [has_monad_lift m m'] [monad m] [monad_reader r m] [monad m'] : monad_reader r m' :=
|
||||
{ reader := λ α, monad_lift ∘ (monad_reader.reader : _ → m α) }
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@ import init.category.id
|
|||
import init.category.transformers
|
||||
universes u v w
|
||||
|
||||
def state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
σ → m (α × σ)
|
||||
structure state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
(run' : σ → m (α × σ))
|
||||
|
||||
@[reducible] def state (σ α : Type u) : Type u := state_t σ id α
|
||||
|
||||
|
|
@ -22,25 +22,23 @@ section
|
|||
variables {α β : Type u}
|
||||
|
||||
protected def run (st : σ) (x : state_t σ m α) : m (α × σ) :=
|
||||
x st
|
||||
state_t.run' x st
|
||||
|
||||
protected def return (a : α) : state_t σ m α :=
|
||||
λ s, show m (α × σ), from
|
||||
return (a, s)
|
||||
protected def pure (a : α) : state_t σ m α :=
|
||||
⟨λ s, pure (a, s)⟩
|
||||
|
||||
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
|
||||
⟨λ s, do (a, new_s) ← act₁.run s,
|
||||
(act₂ a).run new_s⟩
|
||||
|
||||
instance : monad (state_t σ m) :=
|
||||
{ pure := @state_t.return σ m _, bind := @state_t.bind σ m _ }
|
||||
{ pure := @state_t.pure σ m _, bind := @state_t.bind σ m _ }
|
||||
|
||||
protected def orelse [alternative m] (α : Type u) (act₁ act₂ : state_t σ m α) : state_t σ m α :=
|
||||
λ s, act₁ s <|> act₂ s
|
||||
⟨λ s, act₁.run s <|> act₂.run s⟩
|
||||
|
||||
protected def failure [alternative m] (α : Type u) : state_t σ m α :=
|
||||
λ s, failure
|
||||
⟨λ s, failure⟩
|
||||
|
||||
instance [alternative m] : alternative (state_t σ m) :=
|
||||
{ failure := @state_t.failure σ m _ _,
|
||||
|
|
@ -48,46 +46,52 @@ section
|
|||
..state_t.monad }
|
||||
|
||||
protected def get : state_t σ m σ :=
|
||||
λ s, return (s, s)
|
||||
⟨λ s, return (s, s)⟩
|
||||
|
||||
protected def put : σ → state_t σ m punit :=
|
||||
λ s' s, return (punit.star, s')
|
||||
λ s', ⟨λ s, return (punit.star, s')⟩
|
||||
|
||||
protected def modify (f : σ → σ) : state_t σ m punit :=
|
||||
λ s, return (punit.star, f s)
|
||||
|
||||
protected def embed {α : Type u} (x : state σ α) : state_t σ m α :=
|
||||
pure ∘ x
|
||||
⟨λ s, return (punit.star, f s)⟩
|
||||
|
||||
protected def lift {α : Type u} (t : m α) : state_t σ m α :=
|
||||
λ s, do a ← t, return (a, s)
|
||||
⟨λ s, do a ← t, return (a, s)⟩
|
||||
|
||||
instance (m) [monad m] : has_monad_lift m (state_t σ m) :=
|
||||
instance has_monad_lift_lift (m) [monad m] : has_monad_lift m (state_t σ m) :=
|
||||
⟨@state_t.lift σ m _⟩
|
||||
|
||||
protected def map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
|
||||
λ x, ⟨λ st, f (x.run st)⟩
|
||||
|
||||
instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
|
||||
⟨@state_t.map σ m m' _ _⟩
|
||||
|
||||
-- TODO(Sebastian): uses lenses as in https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Zoom ?
|
||||
protected def zoom {σ σ' α : Type u} {m : Type u → Type v} [monad m] (f : σ → σ') (f' : σ' → σ) (x : state_t σ' m α) : state_t σ m α :=
|
||||
λ st, (λ p : α × σ', (p.fst, f' p.snd)) <$> x.run (f st)
|
||||
⟨λ st, (λ p : α × σ', (p.fst, f' p.snd)) <$> x.run (f st)⟩
|
||||
end
|
||||
end state_t
|
||||
|
||||
@[reducible] protected def state.run {σ α : Type u} (st : σ) (x : state σ α) : α × σ :=
|
||||
state_t.run st x
|
||||
|
||||
@[reducible] def monad_state (σ : out_param (Type u)) (m : Type u → Type u) [monad m] :=
|
||||
has_monad_lift_t (state σ) m
|
||||
class monad_state_lift (σ : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
|
||||
[has_lift : has_monad_lift_t (state_t σ m) n]
|
||||
|
||||
attribute [instance] monad_state_lift.mk
|
||||
local attribute [instance] monad_state_lift.has_lift
|
||||
|
||||
section
|
||||
variables {σ : Type u} {m : Type u → Type u} [monad m] [monad_state σ m]
|
||||
variables {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_state_lift σ m n]
|
||||
|
||||
@[inline] def get : m σ :=
|
||||
@monad_lift _ _ _ _ (state_t.get : state σ _)
|
||||
@[inline] def get : n σ :=
|
||||
@monad_lift _ _ _ _ (state_t.get : state_t σ m _)
|
||||
|
||||
@[inline] def put (st : σ) : m punit :=
|
||||
monad_lift (state_t.put st : state σ _)
|
||||
@[inline] def put (st : σ) : n punit :=
|
||||
monad_lift (state_t.put st : state_t σ m _)
|
||||
|
||||
@[inline] def modify (f : σ → σ) : m punit :=
|
||||
monad_lift (state_t.modify f : state σ _)
|
||||
@[inline] def modify (f : σ → σ) : n punit :=
|
||||
monad_lift (state_t.modify f : state_t σ m _)
|
||||
end
|
||||
|
||||
class monad_state_functor (σ σ' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
|
||||
|
|
@ -98,9 +102,3 @@ local attribute [instance] monad_state_functor.functor
|
|||
|
||||
def zoom {σ σ'} {m n n'} [monad m] {α : Type u} (f : σ → σ') (f' : σ' → σ) [monad_state_functor σ' σ m n n'] : n α → n' α :=
|
||||
monad_map $ λ α, (state_t.zoom f f' : state_t σ' m α → state_t σ m α)
|
||||
|
||||
def map_state_t {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
|
||||
λ x st, f (x st)
|
||||
|
||||
instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
|
||||
⟨@map_state_t σ m m' _ _⟩
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ has_monad_lift_t.monad_lift n α
|
|||
instance has_monad_lift_t_trans (m n o) [has_monad_lift n o] [has_monad_lift_t m n] : has_monad_lift_t m o :=
|
||||
⟨λ α (ma : m α), has_monad_lift.monad_lift o α $ has_monad_lift_t.monad_lift n α ma⟩
|
||||
|
||||
instance has_monad_lift_t_refl (m) [monad m] : has_monad_lift_t m m :=
|
||||
instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
|
||||
⟨λ α, id⟩
|
||||
|
||||
/-- A functor in the category of monads. Can be used to lift monad-transforming functions.
|
||||
|
|
@ -49,6 +49,9 @@ class monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type w) :=
|
|||
|
||||
export monad_functor_t (monad_map)
|
||||
|
||||
def monad_map' {α : Type u} (m m' : Type u → Type v) (n n' : Type u → Type w) [monad_functor_t (λ (α : Type u), m α) (λ (α : Type u), m' punit) n (λ {α : Type u}, n' punit)] : (∀ {α}, m α → m' punit) → n α → n' punit :=
|
||||
monad_map
|
||||
|
||||
instance monad_functor_t_trans (m m' n n' o o') [monad_functor n n' o o'] [monad_functor_t m m' n n'] : monad_functor_t m m' o o' :=
|
||||
⟨λ α f, monad_functor.monad_map (λ α, (monad_map @f : n α → n' α))⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
|
|||
tac >> solve_goals
|
||||
|
||||
meta def istep {α : Type} (line0 col0 line col : nat) (tac : smt_tactic α) : smt_tactic unit :=
|
||||
λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals) ss ts)).clamp_pos line0 line col
|
||||
⟨λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals).run ss ts)).clamp_pos line0 line col⟩
|
||||
|
||||
meta def execute (tac : smt_tactic unit) : tactic unit :=
|
||||
using_smt tac
|
||||
|
|
|
|||
|
|
@ -59,11 +59,12 @@ state_t smt_state tactic
|
|||
meta instance : has_append smt_state :=
|
||||
list.has_append
|
||||
|
||||
meta instance : monad smt_tactic :=
|
||||
state_t.monad
|
||||
|
||||
meta instance : monad_state smt_state smt_tactic :=
|
||||
state_t.monad_state
|
||||
section
|
||||
local attribute [reducible] smt_tactic
|
||||
meta instance : monad smt_tactic := by apply_instance
|
||||
meta instance : alternative smt_tactic := by apply_instance
|
||||
meta instance : monad_state_lift smt_state tactic smt_tactic := by apply_instance
|
||||
end
|
||||
|
||||
/- 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. -/
|
||||
|
|
@ -75,21 +76,9 @@ meta instance : has_monad_lift tactic smt_tactic :=
|
|||
meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) :=
|
||||
⟨monad_lift⟩
|
||||
|
||||
meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic α :=
|
||||
λ ss ts, result.cases_on (t₁ ss ts)
|
||||
result.success
|
||||
(λ e₁ ref₁ s', result.cases_on (t₂ ss ts)
|
||||
result.success
|
||||
result.exception)
|
||||
|
||||
meta instance : monad_fail smt_tactic :=
|
||||
{ fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α), ..smt_tactic.monad }
|
||||
|
||||
meta instance : alternative smt_tactic :=
|
||||
{ failure := λ α, @tactic.failed α,
|
||||
orelse := @smt_tactic_orelse,
|
||||
..smt_tactic.monad }
|
||||
|
||||
namespace smt_tactic
|
||||
open tactic (transparency)
|
||||
meta constant intros : smt_tactic unit
|
||||
|
|
@ -154,9 +143,9 @@ meta def fail {α : Type} {β : Type u} [has_to_format β] (msg : β) : smt_tact
|
|||
tactic.fail msg
|
||||
|
||||
meta def try {α : Type} (t : smt_tactic α) : smt_tactic unit :=
|
||||
λ ss ts, result.cases_on (t ss ts)
|
||||
⟨λ ss ts, result.cases_on (t.run ss ts)
|
||||
(λ ⟨a, new_ss⟩, result.success ((), new_ss))
|
||||
(λ e ref s', result.success ((), ss) ts)
|
||||
(λ e ref s', result.success ((), ss) ts)⟩
|
||||
|
||||
/-- `iterate_at_most n t`: repeat the given tactic at most n times or until t fails -/
|
||||
meta def iterate_at_most : nat → smt_tactic unit → smt_tactic unit
|
||||
|
|
@ -182,7 +171,7 @@ do s₁ ← get,
|
|||
return (s₁, s₂)
|
||||
|
||||
protected meta def write : smt_state × tactic_state → smt_tactic unit :=
|
||||
λ ⟨ss, ts⟩ _ _, result.success ((), ss) ts
|
||||
λ ⟨ss, ts⟩, ⟨λ _ _, result.success ((), ss) ts⟩
|
||||
|
||||
private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_goal → list expr
|
||||
→ tactic (list smt_goal × list expr)
|
||||
|
|
@ -195,14 +184,14 @@ private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_go
|
|||
|
||||
/- See slift -/
|
||||
meta def slift_aux {α : Type} (t : tactic α) (cfg : smt_config) : smt_tactic α :=
|
||||
λ ss, do
|
||||
⟨λ ss, do
|
||||
_::sgs ← return ss | tactic.fail "slift tactic failed, there no smt goals to be solved",
|
||||
tg::tgs ← tactic.get_goals | tactic.failed,
|
||||
tactic.set_goals [tg], a ← t,
|
||||
new_tgs ← tactic.get_goals,
|
||||
(new_sgs, new_tgs) ← mk_smt_goals_for cfg new_tgs [] [],
|
||||
tactic.set_goals (new_tgs ++ tgs),
|
||||
return (a, new_sgs ++ sgs)
|
||||
return (a, new_sgs ++ sgs)⟩
|
||||
|
||||
/--
|
||||
This lift operation will restart the SMT state.
|
||||
|
|
@ -225,7 +214,7 @@ do s ← get,
|
|||
return s.classical
|
||||
|
||||
meta def num_goals : smt_tactic nat :=
|
||||
λ ss, return (ss.length, ss)
|
||||
list.length <$> get
|
||||
|
||||
/- Low level primitives for managing set of goals -/
|
||||
meta def get_goals : smt_tactic (list smt_goal × list expr) :=
|
||||
|
|
@ -234,7 +223,7 @@ do (g₁, _) ← smt_tactic.read,
|
|||
return (g₁, g₂)
|
||||
|
||||
meta def set_goals : list smt_goal → list expr → smt_tactic unit :=
|
||||
λ g₁ g₂ ss, tactic.set_goals g₂ >> return ((), g₁)
|
||||
λ g₁ g₂, ⟨λ ss, tactic.set_goals g₂ >> return ((), g₁)⟩
|
||||
|
||||
private meta def all_goals_core (tac : smt_tactic unit) : list smt_goal → list expr → list smt_goal → list expr → smt_tactic unit
|
||||
| [] ts acs act := set_goals acs (ts ++ act)
|
||||
|
|
@ -407,7 +396,7 @@ open smt_tactic
|
|||
|
||||
meta def using_smt {α} (t : smt_tactic α) (cfg : smt_config := {}) : tactic α :=
|
||||
do ss ← smt_state.mk cfg,
|
||||
(a, _) ← (do a ← t, iterate close, return a) ss,
|
||||
(a, _) ← (do a ← t, iterate close, return a).run ss,
|
||||
return a
|
||||
|
||||
meta def using_smt_with {α} (cfg : smt_config) (t : smt_tactic α) : tactic α :=
|
||||
|
|
|
|||
|
|
@ -1,14 +1,12 @@
|
|||
meta def mytac :=
|
||||
state_t nat tactic
|
||||
|
||||
meta instance : monad mytac :=
|
||||
state_t.monad
|
||||
|
||||
meta instance : monad_state nat mytac :=
|
||||
state_t.monad_state
|
||||
|
||||
meta instance : has_monad_lift tactic mytac :=
|
||||
state_t.has_monad_lift _
|
||||
section
|
||||
local attribute [reducible] mytac
|
||||
meta instance : monad mytac := by apply_instance
|
||||
meta instance : monad_state_lift nat tactic mytac := by apply_instance
|
||||
meta instance : has_monad_lift tactic mytac := by apply_instance
|
||||
end
|
||||
|
||||
meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
|
||||
⟨monad_lift⟩
|
||||
|
|
@ -19,17 +17,17 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
|
|||
t >> return ()
|
||||
|
||||
meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
|
||||
λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
|
||||
⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
|
||||
(λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
|
||||
(λ opt_msg_thunk e new_s, match opt_msg_thunk with
|
||||
| some msg_thunk :=
|
||||
let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
|
||||
interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
|
||||
| none := interaction_monad.silent_fail new_s
|
||||
end)
|
||||
end)⟩
|
||||
|
||||
meta def execute (tac : mytac unit) : tactic unit :=
|
||||
tac 0 >> return ()
|
||||
tac.run 0 >> return ()
|
||||
|
||||
meta def save_info (p : pos) : mytac unit :=
|
||||
do v ← get,
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":64,"severity":"information","text":"test\n"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":62,"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":68}
|
||||
{"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":66}
|
||||
|
|
|
|||
|
|
@ -1,14 +1,12 @@
|
|||
meta def mytac :=
|
||||
state_t (name_map nat) tactic
|
||||
|
||||
meta instance : monad mytac :=
|
||||
state_t.monad
|
||||
|
||||
meta instance : monad_state (name_map nat) mytac :=
|
||||
state_t.monad_state
|
||||
|
||||
meta instance : has_monad_lift tactic mytac :=
|
||||
state_t.has_monad_lift _
|
||||
section
|
||||
local attribute [reducible] mytac
|
||||
meta instance : monad mytac := by apply_instance
|
||||
meta instance : monad_state_lift (name_map nat) tactic mytac := by apply_instance
|
||||
meta instance : has_monad_lift tactic mytac := by apply_instance
|
||||
end
|
||||
|
||||
meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
|
||||
⟨monad_lift⟩
|
||||
|
|
@ -19,7 +17,7 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
|
|||
t >> return ()
|
||||
|
||||
meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
|
||||
λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
|
||||
⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
|
||||
(λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
|
||||
(λ opt_msg_thunk e new_s,
|
||||
match opt_msg_thunk with
|
||||
|
|
@ -27,10 +25,10 @@ meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac un
|
|||
let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
|
||||
interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
|
||||
| none := interaction_monad.silent_fail new_s
|
||||
end)
|
||||
end)⟩
|
||||
|
||||
meta def execute (tac : mytac unit) : tactic unit :=
|
||||
tac (name_map.mk nat) >> return ()
|
||||
tac.run (name_map.mk nat) >> return ()
|
||||
|
||||
meta def save_info (p : pos) : mytac unit :=
|
||||
do v ← get,
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
{"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"}
|
||||
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"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":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"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":82,"severity":"information","text":"test\n"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"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":82,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":90,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":90,"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":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}
|
||||
{"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":68}
|
||||
{"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":72}
|
||||
{"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":86}
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ meta constant smt2_state : Type
|
|||
state_t smt2_state tactic α
|
||||
|
||||
meta instance tactic_to_smt2_m (α : Type) : has_coe (tactic α) (smt2_m α) :=
|
||||
⟨ fun tc, fun s, do res ← tc, return (res, s) ⟩
|
||||
⟨ fun tc, ⟨fun s, do res ← tc, return (res, s)⟩ ⟩
|
||||
|
||||
meta def reflect_arith_formula : expr → smt2_m term
|
||||
| `(has_zero.zero) := smt2.builder.int_const <$> tactic.eval_expr int `(has_zero.zero int)
|
||||
|
|
|
|||
|
|
@ -14,4 +14,4 @@ do x ← get,
|
|||
print_ln y,
|
||||
put_str "end of program"
|
||||
|
||||
#eval tst 5
|
||||
#eval tst.run 5
|
||||
|
|
|
|||
|
|
@ -1,14 +1,12 @@
|
|||
meta def mytac :=
|
||||
state_t nat tactic
|
||||
|
||||
meta instance : monad mytac :=
|
||||
state_t.monad
|
||||
|
||||
meta instance : monad_state nat mytac :=
|
||||
state_t.monad_state
|
||||
|
||||
meta instance : has_monad_lift tactic mytac :=
|
||||
state_t.has_monad_lift _
|
||||
section
|
||||
local attribute [reducible] mytac
|
||||
meta instance : monad mytac := by apply_instance
|
||||
meta instance : monad_state_lift nat tactic mytac := by apply_instance
|
||||
meta instance : has_monad_lift tactic mytac := by apply_instance
|
||||
end
|
||||
|
||||
meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
|
||||
⟨monad_lift⟩
|
||||
|
|
@ -19,7 +17,7 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
|
|||
t >> return ()
|
||||
|
||||
meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
|
||||
λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
|
||||
⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
|
||||
(λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
|
||||
(λ opt_msg_thunk e new_s,
|
||||
match opt_msg_thunk with
|
||||
|
|
@ -27,10 +25,10 @@ meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac un
|
|||
let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
|
||||
interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
|
||||
| none := interaction_monad.silent_fail new_s
|
||||
end)
|
||||
end)⟩
|
||||
|
||||
meta def execute (tac : mytac unit) : tactic unit :=
|
||||
tac 0 >> return ()
|
||||
tac.run 0 >> return ()
|
||||
|
||||
meta def save_info (p : pos) : mytac unit :=
|
||||
do v ← get,
|
||||
|
|
|
|||
|
|
@ -6,10 +6,10 @@ by using_smt $ smt_tactic.intros >> get_local `x >>= (fun a, trace a)
|
|||
open tactic_result
|
||||
|
||||
meta def fail_if_success {α : Type} (t : smt_tactic α) : smt_tactic unit :=
|
||||
λ ss ts, match t ss ts with
|
||||
⟨λ ss ts, match t.run ss ts with
|
||||
| success _ _ := failed ts
|
||||
| exception _ _ _ := success ((), ss) ts
|
||||
end
|
||||
end⟩
|
||||
|
||||
def my_smt_config : smt_config :=
|
||||
{ pre_cfg := { zeta := tt } }
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue