From 02fb2c9c8acfd46257ddd41b445762c4387b22a3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Jul 2016 00:51:32 -0700
Subject: [PATCH] feat(library/init): add 'guard' and helper typeclasses

---
 library/init/alternative.lean             | 22 ++++++++++++
 library/init/applicative.lean             | 19 ++++++++++
 library/init/default.lean                 |  2 +-
 library/init/list.lean                    |  4 +++
 library/init/list_classes.lean            | 23 +++++++++++++
 library/init/meta/base_tactic.lean        | 42 +++++++++++------------
 library/init/monad.lean                   |  8 +++--
 library/init/option.lean                  | 33 ++++++++++--------
 tests/lean/list_monad1.lean               |  7 ++++
 tests/lean/list_monad1.lean.expected.out  |  1 +
 tests/lean/struct_class.lean.expected.out |  4 +++
 11 files changed, 125 insertions(+), 40 deletions(-)
 create mode 100644 library/init/alternative.lean
 create mode 100644 library/init/applicative.lean
 create mode 100644 library/init/list_classes.lean
 create mode 100644 tests/lean/list_monad1.lean
 create mode 100644 tests/lean/list_monad1.lean.expected.out

diff --git a/library/init/alternative.lean b/library/init/alternative.lean
new file mode 100644
index 0000000000..a4e81cbee0
--- /dev/null
+++ b/library/init/alternative.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.logic init.applicative
+
+structure alternative [class] (f : Type → Type) extends applicative f :=
+(failure : Π {A : Type}, f A)
+(orelse  : Π {A : Type}, f A → f A → f A)
+
+inline definition failure {f : Type → Type} [alternative f] {A : Type} : f A :=
+alternative.failure f
+
+inline definition orelse {f : Type → Type} [alternative f] {A : Type} : f A → f A → f A :=
+alternative.orelse
+
+infixr ` <|> `:2 := orelse
+
+inline definition guard {f : Type₁ → Type} [alternative f] (p : Prop) [decidable p] : f unit :=
+if p then pure () else failure
diff --git a/library/init/applicative.lean b/library/init/applicative.lean
new file mode 100644
index 0000000000..58c9e6d1bd
--- /dev/null
+++ b/library/init/applicative.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.functor
+
+structure applicative [class] (f : Type → Type) extends functor f :=
+(pure : Π {A : Type}, A → f A)
+(seq  : Π {A B : Type}, f (A → B) → f A → f B)
+
+inline definition pure {f : Type → Type} [applicative f] {A : Type} (a : A) : f A :=
+applicative.pure f a
+
+inline definition seq_app {A B : Type} {f : Type → Type} [applicative f] (g : f (A → B)) (a : f A) : f B :=
+applicative.seq g a
+
+infixr ` <*> `:2 := seq_app
diff --git a/library/init/default.lean b/library/init/default.lean
index 0f13ebbe36..42608587bb 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -9,6 +9,6 @@ import init.relation init.nat init.prod init.combinator
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.option init.fin init.list init.char init.string init.to_string
-import init.timeit init.trace init.unsigned init.ordering
+import init.timeit init.trace init.unsigned init.ordering init.list_classes
 import init.meta
 import init.wf init.wf_k init.sigma_lex
diff --git a/library/init/list.lean b/library/init/list.lean
index a890a570b6..4e00d9be69 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -61,6 +61,10 @@ definition reverse : list A → list A
 definition map {B : Type} (f : A → B) : list A → list B
 | []       := []
 | (a :: l) := f a :: map l
+
+definition join : list (list A) → list A
+| []        := []
+| (l :: ls) := append l (join ls)
 end list
 
 definition list_has_append [instance] {A : Type} : has_append (list A) :=
diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean
new file mode 100644
index 0000000000..b24d0d1db9
--- /dev/null
+++ b/library/init/list_classes.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.monad init.alternative
+open list
+
+inline definition list_fmap {A B : Type} (f : A → B) (l : list A) : list B :=
+map f l
+
+inline definition list_bind {A B : Type} (a : list A) (b : A → list B) : list B :=
+join (map b a)
+
+inline definition list_return {A : Type} (a : A) : list A :=
+[a]
+
+definition list_is_monad [instance] : monad list :=
+monad.mk @list_fmap @list_return @list_bind
+
+definition list_is_alternative [instance] : alternative list :=
+alternative.mk @list_fmap @list_return (@fapp _ _) @nil @list.append
diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean
index 14a3bec236..b5e0b0a325 100644
--- a/library/init/meta/base_tactic.lean
+++ b/library/init/meta/base_tactic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.monad init.meta.exceptional init.meta.format
+import init.monad init.alternative init.meta.exceptional init.meta.format
 /-
 Remark: we use a function that produces a format object as the exception information.
 Motivation: the formatting object may be big, and we may create it on demand.
@@ -47,35 +47,35 @@ inline protected meta_definition bind (t₁ : base_tactic S A) (t₂ : A → bas
 
 inline protected meta_definition return (a : A) : base_tactic S A :=
 λ s, success a s
-
 end base_tactic
 
-meta_definition base_tactic.is_monad [instance] (S : Type) : monad (base_tactic S) :=
-monad.mk (@base_tactic.fmap S) (@base_tactic.return S) (@base_tactic.bind S)
-
-namespace tactic
-variables {S A : Type}
 open base_tactic_result
-
-meta_definition fail {A B : Type} [has_to_format B] (msg : B) : base_tactic S A :=
-λ s, exception A (λ u, to_fmt msg) s
-
-meta_definition failed : base_tactic S A :=
-fail "failed"
-
-meta_definition try (t : base_tactic S A) : base_tactic S unit :=
-λ s, base_tactic_result.cases_on (t s)
- (λ a, success ())
- (λ e s', success () s)
-
-meta_definition or_else (t₁ t₂ : base_tactic S A) : base_tactic S A :=
+meta_definition tactic_orelse {S A : Type} (t₁ t₂ : base_tactic S A) : base_tactic S A :=
 λ s, base_tactic_result.cases_on (t₁ s)
   success
   (λ e₁ s', base_tactic_result.cases_on (t₂ s)
      success
      (exception A))
 
-infix `<|>`:1 := or_else
+meta_definition base_tactic_is_monad [instance] (S : Type) : monad (base_tactic S) :=
+monad.mk (@base_tactic.fmap S) (@base_tactic.return S) (@base_tactic.bind S)
+
+meta_definition tactic.fail {S A B : Type} [has_to_format B] (msg : B) : base_tactic S A :=
+λ s, exception A (λ u, to_fmt msg) s
+
+meta_definition tactic.failed {S A : Type} : base_tactic S A :=
+tactic.fail "failed"
+
+meta_definition base_tactic_is_alternative [instance] (S : Type) : alternative (base_tactic S) :=
+alternative.mk (@base_tactic.fmap S) (λ A a s, success a s) (@fapp _ _) (@tactic.failed S) (@tactic_orelse S)
+
+namespace tactic
+variables {S A : Type}
+
+meta_definition try (t : base_tactic S A) : base_tactic S unit :=
+λ s, base_tactic_result.cases_on (t s)
+ (λ a, success ())
+ (λ e s', success () s)
 
 meta_definition skip : base_tactic S unit :=
 success ()
diff --git a/library/init/monad.lean b/library/init/monad.lean
index f139313720..20bba6f0a2 100644
--- a/library/init/monad.lean
+++ b/library/init/monad.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson and Jared Roesch
 -/
 prelude
-import init.functor init.string init.trace
+import init.applicative init.string init.trace
 
 structure monad [class] (m : Type → Type) extends functor m : Type :=
 (ret  : Π {a:Type}, a → m a)
@@ -13,14 +13,16 @@ structure monad [class] (m : Type → Type) extends functor m : Type :=
 inline definition return {m : Type → Type} [monad m] {A : Type} (a : A) : m A :=
 monad.ret m a
 
-inline definition fapp {A B : Type} {m : Type → Type} [monad m] (f : m (A → B)) (a : m A) : m B :=
+definition fapp {m : Type → Type} [monad m] {A B : Type} (f : m (A → B)) (a : m A) : m B :=
 do g ← f,
    b ← a,
    return (g b)
 
+inline definition monad_is_applicative [instance] (m : Type → Type) [monad m] : applicative m :=
+applicative.mk (@monad.map _ _) (@monad.ret _ _) (@fapp _ _)
+
 inline definition monad.and_then {A B : Type} {m : Type → Type} [monad m] (a : m A) (b : m B) : m B :=
 do a, b
 
-infixr ` <*> `:2 := fapp
 infixl ` >>= `:2 := monad.bind
 infixl ` >> `:2  := monad.and_then
diff --git a/library/init/option.lean b/library/init/option.lean
index 45f6381656..352f7ee052 100644
--- a/library/init/option.lean
+++ b/library/init/option.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Basic datatypes
 -/
 prelude
-import init.logic init.monad
+import init.logic init.monad init.alternative
 
 open decidable
 
@@ -23,20 +23,23 @@ definition option_has_decidable_eq [instance] {A : Type} [H : decidable_eq A] :
   | ff n := ff (λ H, option.no_confusion H (λ e, absurd e n))
   end
 
-namespace option
-  inline protected definition fmap {A B : Type} (f : A → B) (e : option A) : option B :=
-  option.cases_on e
-    none
-    (λ a, some (f a))
+inline definition option_fmap {A B : Type} (f : A → B) (e : option A) : option B :=
+option.cases_on e
+  none
+  (λ a, some (f a))
 
-  inline protected definition bind {A B : Type} (a : option A) (b : A → option B) : option B :=
-  option.cases_on a
-    none
-    (λ a, b a)
+inline definition option_bind {A B : Type} (a : option A) (b : A → option B) : option B :=
+option.cases_on a
+  none
+  (λ a, b a)
 
-  inline protected definition return {A : Type} (a : A) : option A :=
-  some a
-end option
+definition option_is_monad [instance] : monad option :=
+monad.mk @option_fmap @some @option_bind
 
-definition option.is_monad [instance] : monad option :=
-monad.mk @option.fmap @option.return @option.bind
+definition option_orelse {A : Type} : option A → option A → option A
+| (some a) _         := some a
+| none     (some a)  := some a
+| none     none      := none
+
+definition option_is_alternative [instance] {A : Type} : alternative option :=
+alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse
diff --git a/tests/lean/list_monad1.lean b/tests/lean/list_monad1.lean
new file mode 100644
index 0000000000..47b708eb9b
--- /dev/null
+++ b/tests/lean/list_monad1.lean
@@ -0,0 +1,7 @@
+vm_eval
+(do {
+ a : nat ← [1, 2, 3, 4],
+ b : nat ← [4, 5, 6],
+ (guard $ 2 * a ≥ b : list unit),
+ (guard $ b < 6 : list unit),
+ return (a, b) } : list (nat × nat) )
diff --git a/tests/lean/list_monad1.lean.expected.out b/tests/lean/list_monad1.lean.expected.out
new file mode 100644
index 0000000000..627b028035
--- /dev/null
+++ b/tests/lean/list_monad1.lean.expected.out
@@ -0,0 +1 @@
+[(2, 4), (3, 4), (3, 5), (4, 4), (4, 5)]
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 72183f7757..866442cad1 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,3 +1,5 @@
+alternative : (Type → Type) → Type
+applicative : (Type → Type) → Type
 decidable : Prop → Type₁
 functor : (Type → Type) → Type
 has_add : Type → Type
@@ -26,6 +28,8 @@ point : Type → Type → Type
 setoid : Type → Type
 subsingleton : Type → Prop
 well_founded : Π {A}, (A → A → Prop) → Prop
+alternative : (Type → Type) → Type
+applicative : (Type → Type) → Type
 decidable : Prop → Type₁
 functor : (Type → Type) → Type
 has_add : Type → Type