diff options
Diffstat (limited to 'src/Soat/Data')
| -rw-r--r-- | src/Soat/Data/Product.idr | 227 | ||||
| -rw-r--r-- | src/Soat/Data/Sublist.idr | 76 |
2 files changed, 0 insertions, 303 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr deleted file mode 100644 index 1532d4b..0000000 --- a/src/Soat/Data/Product.idr +++ /dev/null @@ -1,227 +0,0 @@ -module Soat.Data.Product - -import Data.List.Elem -import Data.Setoid.Indexed - -%default total - -infix 10 ^ -infix 5 ++ - --- Definitions - -public export -data (^) : (0 _ : a -> Type) -> List a -> Type where - Nil : x ^ [] - (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is) - -public export -ary : List Type -> Type -> Type -ary [] y = y -ary (x :: xs) y = x -> ary xs y - --- Conversions - -public export -uncurry : map x is `ary` a -> x ^ is -> a -uncurry f [] = f -uncurry f (x :: xs) = uncurry (f x) xs - --- Destructors - -public export -head : x ^ (i :: is) -> x i -head (x :: xs) = x - -public export -tail : x ^ (i :: is) -> x ^ is -tail (x :: xs) = xs - -public export -consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs -consHeadTail (x :: xs) = Refl - -public export -index : x ^ is -> Elem i is -> x i -index xs Here = head xs -index xs (There elem) = index (tail xs) elem - --- Constructors - -public export -tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is -tabulate {is = []} f = [] -tabulate {is = (i :: is)} f = f Here :: tabulate (f . There) - -public export -indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is) - -> index (tabulate f) elem = f elem -indexTabulate f Here = Refl -indexTabulate f (There elem) = indexTabulate (f . There) elem - --- Operations - -public export -map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is -map f [] = [] -map f (x :: xs) = f _ x :: map f xs - -public export -indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is) - -> index (map f xs) elem = f i (index xs elem) -indexMap (x :: xs) Here = Refl -indexMap (x :: xs) (There elem) = indexMap xs elem - -public export -mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs -mapId [] = Refl -mapId (x :: xs) = cong ((::) x) $ mapId xs - -public export -mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i} - -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs) -mapComp [] = Refl -mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs - -public export -(++) : x ^ is -> x ^ js -> x ^ (is ++ js) -(++) [] ys = ys -(++) (x :: xs) ys = x :: (xs ++ ys) - -public export -wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is -wrap f [] = [] -wrap f (x :: xs) = x :: wrap f xs - -public export -mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is) - -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs) -mapWrap g [] = Refl -mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs - -public export -unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is -unwrap f {is = []} [] = [] -unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs - -public export -mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) - -> {is : _} -> (xs : x ^ map g is) - -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs) -mapUnwrap g {is = []} [] = Refl -mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs - -public export -unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs -unwrapWrap u [] = Refl -unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs - -public export -wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs -wrapUnwrap {is = []} [] = Refl -wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs - --- Relations - -namespace Pointwise - public export - data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where - Nil : Pointwise rel [] [] - (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)} - -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys) - - -- Destructors - - public export - index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem) - index (r :: rs) Here = r - index (r :: rs) (There elem) = index rs elem - - -- Operators - - public export - map : forall b . {0 r, s : (i : a) -> Rel (b i)} - -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y) - -> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys - map f [] = [] - map f (r :: rs) = f _ r :: map f rs - - -- Relational Properties - - pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys - pwEqImpliesEqual [] = Refl - pwEqImpliesEqual (r :: rs) = trans - (sym $ consHeadTail _) - (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _)) - - equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys - equalImpliesPwEq {xs = []} {ys = []} eq = [] - equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq = - cong head eq :: equalImpliesPwEq (cong tail eq) - - pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> (u : x i) -> rel i u u) - -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs - pwRefl refl [] = [] - pwRefl refl (x :: xs) = refl _ x :: pwRefl refl xs - - pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> (u, v : x i) -> rel i u v -> rel i v u) - -> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs - pwSym sym [] = [] - pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs - - pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> (u, v, w : x i) -> rel i u v -> rel i v w -> rel i u w) - -> {is : List a} -> {xs, ys, zs : x ^ is} - -> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs - pwTrans trans [] [] = [] - pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss - - public export - pwEquivalence : IndexedEquivalence a x -> IndexedEquivalence (List a) ((^) x) - pwEquivalence eq = MkIndexedEquivalence - { relation = \_ => Pointwise eq.relation - , reflexive = \_ => pwRefl eq.reflexive - , symmetric = \_, _, _ => pwSym eq.symmetric - , transitive = \_, _, _, _ => pwTrans eq.transitive - } - - public export - pwSetoid : IndexedSetoid a -> IndexedSetoid (List a) - pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence) - - -- Introductors and Eliminators - - public export - mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} - -> {0 f, g : (i : a) -> x i -> y i} - -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v)) - -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys) - mapIntro'' cong [] = [] - mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs - - public export - mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} - -> {0 f, g : (i : a) -> x i -> y i} - -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v)) - -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys) - mapIntro' cong = mapIntro'' (\t, _, _ => cong t) - - public export - mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is} - -> Pointwise x.equivalence.relation xs ys - -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys) - mapIntro f = mapIntro' f.homomorphic - - public export - wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is} - -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys) - wrapIntro [] = [] - wrapIntro (r :: rs) = r :: wrapIntro rs - - public export - unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {0 xs, ys : x ^ map f is} - -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys) - unwrapIntro {is = []} [] = [] - unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr deleted file mode 100644 index ec73723..0000000 --- a/src/Soat/Data/Sublist.idr +++ /dev/null @@ -1,76 +0,0 @@ -module Soat.Data.Sublist - -import public Control.Relation -import Data.List.Elem -import Soat.Data.Product - -%default total - -infix 5 ++ - -public export -data Sublist : Rel (List a) where - Nil : Sublist [] ys - (::) : (mem : Elem x ys) -> (mems : Sublist xs ys) -> Sublist (x :: xs) ys - -public export -curry : xs `Sublist` ys -> forall x . Elem x xs -> Elem x ys -curry (mem :: mems) Here = mem -curry (mem :: mems) (There y) = curry mems y - -public export -uncurry : {xs : List a} -> (forall x . Elem x xs -> Elem x ys) -> xs `Sublist` ys -uncurry {xs = []} f = [] -uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There) - -public export -uncurryCurry : (f : xs `Sublist` ys) -> uncurry (curry f) = f -uncurryCurry [] = Refl -uncurryCurry (mem :: mems) = cong ((::) mem) (uncurryCurry mems) - -public export -curryUncurry : (0 f : forall x . Elem x xs -> Elem x ys) -> (i : Elem x xs) - -> curry (uncurry f) i = f i -curryUncurry f Here = Refl -curryUncurry f (There elem) = curryUncurry (f . There) elem - -public export -Reflexive (List a) Sublist where - reflexive = uncurry id - -public export -Transitive (List a) Sublist where - transitive f g = uncurry (curry g . curry f) - -public export -elemJoinL : Elem x xs -> Elem x (xs ++ ys) -elemJoinL Here = Here -elemJoinL (There elem) = There (elemJoinL elem) - -public export -elemJoinR : (xs : List a) -> Elem x ys -> Elem x (xs ++ ys) -elemJoinR [] elem = elem -elemJoinR (x :: xs) elem = There (elemJoinR xs elem) - -public export -elemSplit : (xs : List a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys) -elemSplit [] elem = Right elem -elemSplit (x :: xs) Here = Left Here -elemSplit (x :: xs) (There elem) = bimap There id (elemSplit xs elem) - -public export -(++) : {xs, ys, us : List a} - -> xs `Sublist` ys -> us `Sublist` vs -> (xs ++ us) `Sublist` (ys ++ vs) -(++) mems mems' = uncurry - (either (elemJoinL . curry mems) (elemJoinR ys . curry mems') . elemSplit xs) - -public export -shuffle : is `Sublist` js -> x ^ js -> x ^ is -shuffle [] xs = [] -shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs - -public export -indexShuffle : (f : is `Sublist` js) -> {0 xs : x ^ js} -> (elem : Elem i is) - -> index (shuffle f xs) elem = index xs (curry f elem) -indexShuffle (mem :: mems) Here = Refl -indexShuffle (mem :: mems) (There elem) = indexShuffle mems elem |