diff options
Diffstat (limited to 'src/Inky/Decidable')
| -rw-r--r-- | src/Inky/Decidable/Either.idr | 111 | ||||
| -rw-r--r-- | src/Inky/Decidable/Maybe.idr | 146 |
2 files changed, 0 insertions, 257 deletions
diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr deleted file mode 100644 index bea3364..0000000 --- a/src/Inky/Decidable/Either.idr +++ /dev/null @@ -1,111 +0,0 @@ -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 diff --git a/src/Inky/Decidable/Maybe.idr b/src/Inky/Decidable/Maybe.idr deleted file mode 100644 index 2f1d83c..0000000 --- a/src/Inky/Decidable/Maybe.idr +++ /dev/null @@ -1,146 +0,0 @@ -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 |