diff --git a/tests/lean/run/ext_eff.lean b/tests/lean/run/ext_eff.lean deleted file mode 100644 index 0e70312f18..0000000000 --- a/tests/lean/run/ext_eff.lean +++ /dev/null @@ -1,247 +0,0 @@ --- TODO: renable test after we restore tactic framework -#exit -import init.IO - -/- An extensible effects library, inspired by "Freer Monads, More Extensible Effects" (O. Kiselyov, H. Ishii) - and https://github.com/lexi-lambda/freer-simple -/ - -def N := 100 -- Default number of interations for testing - -def effect := Type → Type - -class member {α : Type*} (x : α) (xs : List α) := -(idx : ℕ) -(prf : xs.nth idx = some x) - -instance memberHead {α : Type*} (x : α) (xs) : member x (x::xs) := -⟨0, by simp⟩ - -instance memberTail {α : Type*} (x y : α) (ys) [member x ys] : member x (y::ys) := -⟨member.idx x ys + 1, by simp [member.prf x ys]⟩ - -class lastMember {α : Type*} (x : outParam α) (xs : List α) extends member x xs - -instance lastMemberSingleton {α : Type*} (x : α) : lastMember x [x] := {} -instance lastMemberTail {α : Type*} (x y : α) (ys) [lastMember x ys] : lastMember x (y::ys) := {} - - -structure union (effs : List effect) (α : Type) := -(eff : effect) -[mem : member eff effs] -(val : eff α) - -section -variables {α : Type} {effs : List effect} {eff : effect} - -@[inline] def union.inj (val : eff α) [member eff effs] : union effs α := -{ eff := eff, val := val } - -@[inline] def union.prj (u : union effs α) (eff : effect) [mem : member eff effs] : Option (eff α) := -if h : member.idx eff effs = @member.idx _ u.eff effs u.mem then - have u.eff = eff, - by apply Option.some.inj; rw [←member.prf eff effs, ←@member.prf _ u.eff effs u.mem, h], - some $ cast (congrFun this _) u.val -else none - -@[inline] def union.decomp (u : union (eff::effs) α) : eff α ⊕ union effs α := -by { - have prf := @member.prf _ u.eff (eff::effs) u.mem, - cases h : @member.idx _ u.eff (eff::effs) u.mem, - case Nat.zero { - have : u.eff = eff, - by apply Option.some.inj; rw [←prf, h, List.nth], - rw ←this, - exact Sum.inl u.val - }, - case Nat.succ : idx { - rw [h] at prf, - exact Sum.inr { mem := ⟨idx, prf⟩, ..u } - } -end -end - - -inductive eff (effs : List effect) (α : Type) -| pure {} (a : α) : eff -| impure {β : Type} (u : union effs β) (k : β → eff) : eff - -def eff.bind {α β : Type} {effs : List effect} : eff effs α → (α → eff effs β) → eff effs β -| (eff.pure a) f := f a -| (@eff.impure _ _ β u k) f := eff.impure u (fun b => eff.bind (k b) f) - -instance (effs) : Monad (eff effs) := -{ pure := fun α => eff.pure, - bind := fun α β => eff.bind } - -@[inline] def eff.send {e : effect} {effs α} [member e effs] : e α → eff effs α := -fun x => eff.impure (union.inj x) pure - -@[inline] def eff.sendM {e : effect} {effs α} [Monad e] [lastMember e effs] : e α → eff effs α := -fun x => eff.impure (union.inj x) pure - -@[inline] def eff.handleRelay {e : effect} {effs α β} (ret : β → eff effs α) - (h : ∀ {β}, e β → (β → eff effs α) → eff effs α) : eff (e :: effs) β → eff effs α -| (eff.pure a) := ret a -| (@eff.impure _ _ β u k) := match u.decomp with - | Sum.inl e := h e (fun b => eff.handleRelay (k b)) - | Sum.inr u := eff.impure u (fun b => eff.handleRelay (k b)) - - -@[inline] def eff.handleRelayΣ {e : effect} {effs α β} {σ : Type} (ret : σ → β → eff effs α) - (h : ∀ {β}, σ → e β → (σ → β → eff effs α) → eff effs α) : σ → eff (e :: effs) β → eff effs α -| st (eff.pure a) := ret st a -| st (@eff.impure _ _ β u k) := match u.decomp with - | Sum.inl e := h st e (fun st b => eff.handleRelayΣ st (k b)) - | Sum.inr u := eff.impure u (fun b => eff.handleRelayΣ st (k b)) - - -@[inline] def eff.interpose (e : effect) {effs α β} [member e effs] (ret : β → eff effs α) - (h : ∀ {β}, e β → (β → eff effs α) → eff effs α) : eff effs β → eff effs α -| (eff.pure a) := ret a -| (@eff.impure _ _ β u k) := match u.prj e with - | some e := h e (fun b => eff.interpose (k b)) - | none := eff.impure u (fun b => eff.interpose (k b)) - - -inductive Reader (ρ : Type) : Type → Type -| read {} : Reader ρ - -@[inline] def eff.read {ρ effs} [member (Reader ρ) effs] : eff effs ρ := eff.send Reader.read -instance {ρ effs} [member (Reader ρ) effs] : MonadReader ρ (eff effs) := ⟨eff.read⟩ - -@[inline] def Reader.run {ρ effs α} (env : ρ) : eff (Reader ρ :: effs) α → eff effs α := -eff.handleRelay pure (fun β x k => by cases x; exact k env) - - -inductive State (σ : Type) : Type → Type -| get {} : State σ -| put : σ → State Unit - -@[inline] def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get -@[inline] def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s) -instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) := -⟨fun α x => do st ← eff.get; - let ⟨a, s'⟩ := x.run st; - eff.put s'; - pure a⟩ - -@[inline] def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) := -eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => by { - cases x, - case State.get { exact k st st }, - case State.put : st' { exact k st' () } -}) st - -inductive Exception (ε α : Type) : Type -| throw {} (ex : ε) : Exception - -@[inline] def eff.throw {ε α effs} [member (Exception ε) effs] (ex : ε) : eff effs α := eff.send (Exception.throw ex) -@[inline] def eff.catch {ε α effs} [member (Exception ε) effs] (x : eff effs α) (handle : ε → eff effs α) : eff effs α := -x.interpose (Exception ε) pure (fun β x k => match x with Exception.throw e := handle e) -instance {ε effs} [member (Exception ε) effs] : MonadExcept ε (eff effs) := -⟨fun α => eff.throw, fun α => eff.catch⟩ - -@[inline] def Exception.run {ε effs α} : eff (Exception ε :: effs) α → eff effs (Except ε α) := -eff.handleRelay (pure ∘ Except.ok) (fun β x k => match x with Exception.throw e := pure (Except.error e)) - - -def eff.run {α : Type} : eff [] α → α -| (eff.pure a) := a - -def eff.runM {α : Type} {m} [Monad m] : eff [m] α → m α -| (eff.pure a) := pure a -| (eff.impure u k) := match u.decomp with - | Sum.inl m := m >>= fun a => eff.runM (k a) - -instance (m effs) [member m effs] : HasMonadLift m (eff effs) := -⟨fun α => eff.send⟩ - -section examples - --- from http://okmij.org/ftp/Haskell/extensible/EffDynCatch.hs - -@[inline] def IO.try {α} : IO α → IO (Except IO.error α) := -fun x => IO.catch (Except.ok <$> x) (pure ∘ Except.error) - -instance : HasRepr IO.error := -⟨fun e => match e with - | IO.error.sys n := "IO.error.sys " ++ repr n - | IO.error.other s := "IO.error.other " ++ repr s⟩ - -@[inline] def eff.catchIO {effs α} [member IO effs] (x : eff effs α) (catch : IO.error → eff effs α) : eff effs α := -x.interpose IO pure (fun β x k => do ex ← monadLift x.try; - match ex with - | Except.ok b := k b - | Except.error e := catch e) - --- like `IO.try`, but can be used at any point, not just in the very last layer -@[inline] def eff.tryIO {α effs} [member IO effs] (x : eff effs α) : eff effs (Except IO.error α) := -eff.catchIO (Except.ok <$> x) (pure ∘ Except.error) - -@[inline] def exfn : Bool → IO Bool -| tt := IO.fail "thrown" -| ff := pure tt - --- handle IO exceptions before State -def test1 := - let tf : Bool → eff [IO] _ := fun (x : Bool) => Reader.run x $ State.run ([] : List String) $ eff.tryIo $ - do modify (fun xs => "begin"::xs); - x ← read; - r ← monadLift $ exfn x; - modify (fun xs => "end"::xs); - pure r in - do repr <$> eff.runM (tf tt) >>= IO.println; - repr <$> eff.runM (tf ff) >>= IO.println - -#eval test1 - --- handle IO exceptions after State -def test2 := - let tf : Bool → eff [IO] _ := fun (x : Bool) => Reader.run x $ eff.tryIo $ State.run ([] : List String) $ - do modify (fun xs => "begin"::xs); - x ← read; - r ← monadLift $ exfn x; - modify (fun xs => "end"::xs); - pure r in - do repr <$> eff.runM (tf tt) >>= IO.println; - repr <$> eff.runM (tf ff) >>= IO.println - -#eval test2 - -end examples - -section benchmarks -def State.run {σ α : Type*} : State σ α → σ → α × σ := StateT.run - -def benchStateClassy {m : Type → Type*} [Monad m] [MonadState ℕ m] : ℕ → m ℕ -| 0 := get -| (Nat.succ n) := modify (+n) >> benchStateClassy n - -setOption profiler True -#eval State.run (benchStateClassy N) 0 -#eval eff.run $ State.run 0 (benchStateClassy N) - -#eval State.run (ReaderT.run (ReaderT.run (ReaderT.run (benchStateClassy N) 0) 0) 0) 0 -#eval eff.run $ State.run 0 $ Reader.run 0 $ Reader.run 0 $ Reader.run 0 (benchStateClassy N) - --- left-associated binds lead to quadratic run time (section 2.6) -def benchStateClassy' {m : Type → Type*} [Monad m] [MonadState ℕ m] : ℕ → m ℕ -| 0 := get -| (Nat.succ n) := benchStateClassy' n <* modify (+n) - -#eval eff.run $ State.run 0 (benchStateClassy' (N/100)) -#eval eff.run $ State.run 0 (benchStateClassy' (N/20)) -#eval eff.run $ State.run 0 (benchStateClassy' (N/10)) - -def benchStateT : ℕ → State ℕ ℕ -| 0 := get -| (Nat.succ n) := modify (+n) >> benchStateT n - -#eval State.run (benchStateT N) 0 - -def benchState : ℕ → eff [State ℕ] ℕ -| 0 := get -| (Nat.succ n) := modify (+n) >> benchState n - -#eval eff.run $ State.run 0 (benchState N) -end benchmarks diff --git a/tests/lean/run/ext_eff_linear.lean b/tests/lean/run/ext_eff_linear.lean deleted file mode 100644 index c389a2c31c..0000000000 --- a/tests/lean/run/ext_eff_linear.lean +++ /dev/null @@ -1,201 +0,0 @@ --- TODO: renable test after we restore tactic framework -#exit -/- An extensible effects library, inspired by "Freer Monads, More Extensible Effects" (O. Kiselyov, H. Ishii) - and https://github.com/lexi-lambda/freer-simple -/ - -def N := 100 -- Default number of interations for testing - -def effect := Type → Type - -class member {α : Type*} (x : α) (xs : List α) := -(idx : ℕ) -(prf : xs.nth idx = some x) - -instance memberHead {α : Type*} (x : α) (xs) : member x (x::xs) := -⟨0, by simp⟩ - -instance memberTail {α : Type*} (x y : α) (ys) [member x ys] : member x (y::ys) := -⟨member.idx x ys + 1, by simp [member.prf x ys]⟩ - - -structure union (effs : List effect) (α : Type) := -(eff : effect) -[mem : member eff effs] -(val : eff α) - -section -variables {α : Type} {effs : List effect} {eff : effect} - -@[inline] def union.inj (val : eff α) [member eff effs] : union effs α := -{ eff := eff, val := val } - -@[inline] def union.prj (u : union effs α) (eff : effect) [mem : member eff effs] : Option (eff α) := -if h : member.idx eff effs = @member.idx _ u.eff effs u.mem then - have u.eff = eff, - by apply Option.some.inj; rw [←member.prf eff effs, ←@member.prf _ u.eff effs u.mem, h], - some $ cast (congrFun this _) u.val -else none - -@[inline] def union.decomp (u : union (eff::effs) α) : eff α ⊕ union effs α := -by { - have prf := @member.prf _ u.eff (eff::effs) u.mem, - cases h : @member.idx _ u.eff (eff::effs) u.mem, - case Nat.zero { - have : u.eff = eff, - by apply Option.some.inj; rw [←prf, h, List.nth], - rw ←this, - exact Sum.inl u.val - }, - case Nat.succ : idx { - rw [h] at prf, - exact Sum.inr { mem := ⟨idx, prf⟩, ..u } - } -} -end - -inductive ftcQueue (m : Type → Type 1) : Type → Type → Type 1 -| leaf {α β} (f : α → m β) : ftcQueue α β -| Node {α β γ} : Thunk (ftcQueue α β) → Thunk (ftcQueue β γ) → ftcQueue α γ - -inductive ftcQueue.lView (m : Type → Type 1) : Type → Type → Type 1 -| single {α β} (f : α → m β) : ftcQueue.lView α β -| cons {α β γ} (f : α → m β) : (Unit → ftcQueue m β γ) → ftcQueue.lView α γ - -meta def ftcQueue.viewLAux {m : Type → Type 1} {α} : Π {β γ}, ftcQueue m α β → Thunk (ftcQueue m β γ) → ftcQueue.lView m α γ -| β γ (ftcQueue.leaf f) q := ftcQueue.lView.cons f q -| β γ (ftcQueue.Node n m) q := ftcQueue.viewLAux (n ()) (ftcQueue.Node (m ()) (q ())) - -meta def ftcQueue.viewL {m : Type → Type 1} {α β} : ftcQueue m α β → ftcQueue.lView m α β -| (ftcQueue.leaf f) := ftcQueue.lView.single f -| (ftcQueue.Node n m) := ftcQueue.viewLAux (n ()) (m ()) - -meta inductive eff (effs : List effect) : Type → Type 1 -| pure {} {α : Type} (a : α) : eff α -| impure {α β : Type} (u : union effs β) (k : ftcQueue eff β α) : eff α - -meta abbreviation arrs (effs) := ftcQueue (eff effs) - -meta def arrs.apply {effs} : Π {α β}, arrs effs α β → α → eff effs β -| α β q a := match q.viewL with - | ftcQueue.lView.single f := f a - | ftcQueue.lView.cons f q := match f a with - | eff.pure b := arrs.apply (q ()) b - | eff.impure u k := eff.impure u (ftcQueue.Node k (q ())) - -meta def eff.bind {α β : Type} {effs : List effect} : eff effs α → (α → eff effs β) → eff effs β -| (eff.pure a) f := f a -| (@eff.impure _ _ β u k) f := eff.impure u (ftcQueue.Node k (ftcQueue.leaf f)) - -meta instance (effs) : Monad (eff effs) := -{ pure := fun α => eff.pure, - bind := fun α β => eff.bind } - -@[inline] meta def eff.send {e : effect} {effs α} [member e effs] : e α → eff effs α := -fun x => eff.impure (union.inj x) (ftcQueue.leaf pure) - -@[inline] meta def eff.handleRelay {e : effect} {effs α β} (ret : β → eff effs α) - (h : ∀ {β}, e β → (β → eff effs α) → eff effs α) : eff (e :: effs) β → eff effs α -| (eff.pure a) := ret a -| (@eff.impure _ _ γ u k) := match u.decomp with - | Sum.inl e := h e (fun c => eff.handleRelay (arrs.apply k c)) - | Sum.inr u := eff.impure u (ftcQueue.leaf (fun c => eff.handleRelay (arrs.apply k c))) - - -@[inline] meta def eff.handleRelayΣ {e : effect} {effs α β} {σ : Type} (ret : σ → β → eff effs α) - (h : ∀ {β}, σ → e β → (σ → β → eff effs α) → eff effs α) : σ → eff (e :: effs) β → eff effs α -| st (eff.pure a) := ret st a -| st (@eff.impure _ _ γ u k) := match u.decomp with - | Sum.inl e := h st e (fun st c => eff.handleRelayΣ st (arrs.apply k c)) - | Sum.inr u := eff.impure u (ftcQueue.leaf (fun c => eff.handleRelayΣ st (arrs.apply k c))) - - -@[inline] meta def eff.interpose {e : effect} {effs α β} [member e effs] (ret : β → eff effs α) - (h : ∀ {β}, e β → (β → eff effs α) → eff effs α) : eff effs β → eff effs α -| (eff.pure a) := ret a -| (@eff.impure _ _ γ u k) := match u.prj e with - | some e := h e (fun c => eff.interpose (arrs.apply k c)) - | none := eff.impure u (ftcQueue.leaf (fun c => eff.interpose (arrs.apply k c))) - - -inductive Reader (ρ : Type) : Type → Type -| read {} : Reader ρ - -@[inline] meta def eff.read {ρ effs} [member (Reader ρ) effs] : eff effs ρ := eff.send Reader.read -meta instance {ρ effs} [member (Reader ρ) effs] : MonadReader ρ (eff effs) := ⟨eff.read⟩ - -@[inline] meta def Reader.run {ρ effs α} (env : ρ) : eff (Reader ρ :: effs) α → eff effs α := -eff.handleRelay pure (fun β x k => by cases x; exact k env) - - -inductive State (σ : Type) : Type → Type -| get {} : State σ -| put : σ → State Unit - -@[inline] meta def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get -@[inline] meta def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s) -meta instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) := -⟨fun α x => do st ← eff.get; - let ⟨a, s'⟩ := x.run st; - eff.put s'; - pure a⟩ - -meta def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) := -eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => by { - cases x, - case State.get { exact k st st }, - case State.put : st' { exact k st' () } -}) st - -inductive Exception (ε α : Type) : Type -| throw {} (ex : ε) : Exception - -@[inline] meta def eff.throw {ε α effs} [member (Exception ε) effs] (ex : ε) : eff effs α := eff.send (Exception.throw ex) -@[inline] meta def eff.catch {ε α effs} [member (Exception ε) effs] (x : eff effs α) (handle : ε → eff effs α) : eff effs α := -x.interpose pure (fun β x k => match (x : Exception ε β) with Exception.throw e := handle e) -meta instance {ε effs} [member (Exception ε) effs] : MonadExcept ε (eff effs) := -⟨fun α => eff.throw, fun α => eff.catch⟩ - -@[inline] meta def Exception.run {ε effs α} : eff (Exception ε :: effs) α → eff effs (Except ε α) := -eff.handleRelay (pure ∘ Except.ok) (fun β x k => match x with Exception.throw e := pure (Except.error e)) - - -meta def eff.run {α : Type} : eff [] α → α -| (eff.pure a) := a - - -section benchmarks -def State.run {σ α : Type*} : State σ α → σ → α × σ := StateT.run - -def benchStateClassy {m : Type → Type*} [Monad m] [MonadState ℕ m] : ℕ → m ℕ -| 0 := get -| (Nat.succ n) := benchStateClassy n <* modify (+n) - -setOption profiler True -#eval State.run (benchStateClassy N) 0 -#eval eff.run $ State.run 0 (benchStateClassy N) - -#eval State.run (ReaderT.run (ReaderT.run (ReaderT.run (benchStateClassy N) 0) 0) 0) 0 -#eval eff.run $ State.run 0 $ Reader.run 0 $ Reader.run 0 $ Reader.run 0 (benchStateClassy N) - --- ftcQueue removes the quadratic slowdown -def benchStateClassy' {m : Type → Type*} [Monad m] [MonadState ℕ m] : ℕ → m ℕ -| 0 := get -| (Nat.succ n) := benchStateClassy' n <* modify (+n) - - -#eval eff.run $ State.run 0 (benchStateClassy' (N/100)) -#eval eff.run $ State.run 0 (benchStateClassy' (N/20)) -#eval eff.run $ State.run 0 (benchStateClassy' N) - -def benchStateT : ℕ → State ℕ ℕ -| 0 := get -| (Nat.succ n) := modify (+n) >> benchStateT n - -#eval State.run (benchStateT N) 0 - -meta def benchState : ℕ → eff [State ℕ] ℕ -| 0 := get -| (Nat.succ n) := modify (+n) >> benchState n - -#eval eff.run $ State.run 0 (benchState N) -end benchmarks