diff options
Diffstat (limited to 'src/Inky/Decidable')
| -rw-r--r-- | src/Inky/Decidable/Either.idr | 106 | ||||
| -rw-r--r-- | src/Inky/Decidable/Maybe.idr | 146 |
2 files changed, 252 insertions, 0 deletions
diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr new file mode 100644 index 0000000..9da2c72 --- /dev/null +++ b/src/Inky/Decidable/Either.idr @@ -0,0 +1,106 @@ +module Inky.Decidable.Either + +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 + +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 diff --git a/src/Inky/Decidable/Maybe.idr b/src/Inky/Decidable/Maybe.idr new file mode 100644 index 0000000..2f1d83c --- /dev/null +++ b/src/Inky/Decidable/Maybe.idr @@ -0,0 +1,146 @@ +module Inky.Decidable.Maybe + +import Data.Maybe +import Data.These +import Inky.Decidable.Either + +public export +WhenJust : (a -> Type) -> Type -> Maybe a -> Type +WhenJust p b (Just x) = p x +WhenJust p b Nothing = b + +public export +record Proof (0 a : Type) (0 p : a -> Type) (0 b : Type) where + constructor Because + does : Maybe a + reason : WhenJust p b does + +%name Proof p, q + +public export +DecWhen : (0 a : Type) -> (0 p : a -> Type) -> Type +DecWhen a p = Proof a p ((x : a) -> Not (p x)) + +-- Operations ------------------------------------------------------------------ + +public export +(.forget) : Proof a p b -> LazyEither (x ** p x) b +(Just x `Because` px).forget = True `Because` (x ** px) +(Nothing `Because` y).forget = False `Because` y + +public export +map : + (f : a -> a') -> + ((x : a) -> p x -> q (f x)) -> + (b -> b') -> + Proof a p b -> Proof a' q b' +map f g h (Just x `Because` px) = Just (f x) `Because` g x px +map f g h (Nothing `Because` y) = Nothing `Because` h y + +export autobind infixr 0 >=> + +public export +andThen : + {0 q : a -> a' -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof a' (q x) (b' x)) -> + Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) +andThen (Just x `Because` px) f = map (x,) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x +andThen (Nothing `Because` y) f = Nothing `Because` Left y + +public export +(>=>) : + {0 q : a -> a' -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof a' (q x) (b' x)) -> + Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) +(>=>) = andThen + +public export +andThen' : + {0 a' : a -> Type} -> + {0 q : (x : a) -> a' x -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof (a' x) (q x) (b' x)) -> + Proof (x ** a' x) (\xy => (p (fst xy), q (fst xy) (snd xy))) (Either b (x ** (p x, b' x))) +andThen' (Just x `Because` px) f = + map (\y => (x ** y)) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x +andThen' (Nothing `Because` y) f = Nothing `Because` Left y + +public export +all : + Proof a p b -> + Proof a' q b' -> + Proof (a, a') (\xy => (p (fst xy), q (snd xy))) (These b b') +all (Just x `Because` px) (Just y `Because` py) = Just (x, y) `Because` (px, py) +all (Just x `Because` px) (Nothing `Because` y) = Nothing `Because` That y +all (Nothing `Because` x) q = + Nothing `Because` + case q of + (Just _ `Because` _) => This x + (Nothing `Because` y) => Both x y + +public export +first : + Proof a p b -> + Lazy (Proof c q d) -> + Proof (Either a c) (either p q) (b, d) +first (Just x `Because` px) q = Just (Left x) `Because` px +first (Nothing `Because` x) (Just y `Because` py) = Just (Right y) `Because` py +first (Nothing `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) + +namespace Either + public export + andThen : + (0 c : a -> Type) -> + (0 p : (x : a) -> c x -> Type) -> + (0 d : a -> Type) -> + LazyEither a b -> ((x : a) -> Proof (c x) (p x) (d x)) -> + Proof (x ** c x) (\xy => p (fst xy) (snd xy)) (Either b (x ** d x)) + andThen _ _ _ (True `Because` x) f = map (\y => (x ** y)) (\_ => id) (\y => Right (x ** y)) (f x) + andThen _ _ _ (False `Because` y) f = Nothing `Because` Left y + + public export + first : + LazyEither a b -> + Lazy (Proof c p d) -> + Proof (Maybe c) (maybe a p) (b, d) + first (True `Because` x) q = Just Nothing `Because` x + first (False `Because` x) (Just y `Because` py) = Just (Just y) `Because` py + first (False `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) + + public export + all : LazyEither a b -> Lazy (Proof c p d) -> Proof c (\x => (a, p x)) (These b d) + all (True `Because` x) (Just y `Because` py) = Just y `Because` (x, py) + all (True `Because` x) (Nothing `Because` y) = Nothing `Because` That y + all (False `Because` x) q = + Nothing `Because` + case q of + (Just y `Because` _) => This x + (Nothing `Because` y) => Both x y + +namespace Elim + export autobind infixr 0 >=> + + public export + andThen : + {0 q, r : a -> Type} -> + Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> + LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) + andThen (Just x `Because` px) f = map (\qx => (x ** (px, qx))) (\rx => Right (x ** (px, rx))) (f x) + andThen (Nothing `Because` y) f = False `Because` Left y + + public export + (>=>) : + {0 q, r : a -> Type} -> + Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> + LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) + (>=>) = andThen + +public export +pure : (x : a) -> LazyEither (b x) c -> Proof a b c +pure x (True `Because` y) = Just x `Because` y +pure x (False `Because` y) = Nothing `Because` y |