1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
module Inky.Decidable.Either
import Data.So
import Data.These
public export
Union : Type -> Type -> Bool -> Type
Union a b False = b
Union a b True = a
public export
record LazyEither (0 a, b : Type) where
constructor Because
does : Bool
reason : Lazy (Union a b does)
%name LazyEither p, q
namespace Union
public export
map : {tag : Bool} -> (a -> c) -> (b -> d) -> Union a b tag -> Union c d tag
map {tag = False} f g x = g x
map {tag = True} f g x = f x
public export
not : {tag : Bool} -> Union a b tag -> Union b a (not tag)
not {tag = False} x = x
not {tag = True} x = x
public export
both :
{tag1 : Bool} -> {tag2 : Lazy Bool} ->
Union a b tag1 -> Lazy (Union c d tag2) ->
Union (a, c) (Either b d) (tag1 && tag2)
both {tag1 = True, tag2 = True} x y = (x, y)
both {tag1 = True, tag2 = False} x y = Right y
both {tag1 = False} x y = Left x
public export
first :
{tag1 : Bool} -> {tag2 : Lazy Bool} ->
Union a b tag1 -> Lazy (Union c d tag2) ->
Union (Either a c) (b, d) (tag1 || tag2)
first {tag1 = True} x y = Left x
first {tag1 = False, tag2 = True} x y = Right y
first {tag1 = False, tag2 = False} x y = (x, y)
public export
all :
{tag1, tag2 : Bool} ->
Union a b tag1 -> Union c d tag2 ->
Union (a, c) (These b d) (tag1 && tag2)
all {tag1 = True, tag2 = True} x y = (x, y)
all {tag1 = True, tag2 = False} x y = That y
all {tag1 = False, tag2 = True} x y = This x
all {tag1 = False, tag2 = False} x y = Both x y
public export
any :
{tag1, tag2 : Bool} ->
Union a b tag1 -> Union c d tag2 ->
Union (These a c) (b, d) (tag1 || tag2)
any {tag1 = True, tag2 = True} x y = Both x y
any {tag1 = True, tag2 = False} x y = This x
any {tag1 = False, tag2 = True} x y = That y
any {tag1 = False, tag2 = False} x y = (x, y)
public export
map : (a -> c) -> (b -> d) -> LazyEither a b -> LazyEither c d
map f g p = p.does `Because` Union.map f g p.reason
public export
not : LazyEither a b -> LazyEither b a
not p = not p.does `Because` Union.not p.reason
public export
both : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (Either b d)
both p q = p.does && q.does `Because` Union.both p.reason q.reason
public export
first : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (Either a c) (b, d)
first p q = p.does || q.does `Because` Union.first p.reason q.reason
public export
all : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (These b d)
all p q = p.does && q.does `Because` Union.all p.reason q.reason
public export
any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d)
any p q = p.does || q.does `Because` Union.any p.reason q.reason
public export
so : (b : Bool) -> LazyEither (So b) (So $ not b)
so b = b `Because` if b then Oh else Oh
export autobind infixr 0 >=>
public export
andThen :
{0 p, q : a -> Type} ->
LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) ->
LazyEither (x ** p x) (Either b (x ** q x))
andThen (True `Because` x) f = map (\px => (x ** px)) (\qx => Right (x ** qx)) (f x)
andThen (False `Because` y) f = False `Because` (Left y)
public export
(>=>) :
{0 p, q : a -> Type} ->
LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) ->
LazyEither (x ** p x) (Either b (x ** q x))
(>=>) = andThen
|
