git.iko.soy/Idris-dev
on master help sign in
Replace vectLiftIso with mapIso

mapIso is generic over all VerifiedFunctors, including Vect.

commit9aa05175ef13dcda8e4fe03152b9c23450ff33fe authorhowtonotwin <rasheeqhere@gmail.com> dateWed 4 Jul 2018, 23:22 (8 years ago) parenta27d753
2 files changed+7−10
compare with master
unifiedsplit
libs/contrib/Control/Isomorphism/Extra.idr+6 libs/contrib/Control/Isomorphism/Vect.idr+1−10
libs/contrib/Control/Isomorphism/Extra.idr+6
@@ -1,6 +1,7 @@
11module Control.Isomorphism.Extra
22
33import Control.Isomorphism
4+import Interfaces.Verified
45
56%default total
67%access public export
@@ -34,3 +35,8 @@ swapped {a} l r = MkIso swap swap prf prf
3435 | (No lnx') with (decEq r x)
3536 | (Yes rex) = absurd $ rnx rex
3637 | (No rnx') = Refl
38+
39+mapIso : VerifiedFunctor f => Iso a b -> Iso (f a) (f b)
40+mapIso {f} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) (prf to from toFrom) (prf from to fromTo)
41+ where prf : {a : Type} -> {b : Type} -> (to : a -> b) -> (from : b -> a) -> (toFrom : (x : b) -> to (from x) = x) -> (x : f b) -> map to (map from x) = x
42+ prf to' from' toFrom' x = rewrite sym $ functorComposition x from' to' in functorIdentity (to' . from') toFrom' x
libs/contrib/Control/Isomorphism/Vect.idr+1−10
@@ -1,8 +1,8 @@
11module Control.Isomorphism.Vect
22
3−import Interfaces.Verified
43import Control.Isomorphism
54import Data.Vect
5+import Interfaces.Verified
66
77%default total
88%access public export
@@ -31,15 +31,6 @@ splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo
3131 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
3232 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
3333
34−vectLiftIso : Iso l r -> Iso (Vect n l) (Vect n r)
35−vectLiftIso (MkIso to from toFrom fromTo) = MkIso (map to) (map from) toFrom' fromTo'
36− where toFrom' : {n : Nat} -> (rs : Vect n r) -> map to (map from rs) = rs
37− toFrom' [] = Refl
38− toFrom' (x :: xs) = rewrite toFrom x in rewrite toFrom' xs in Refl
39− fromTo' : {n : Nat} -> (ls : Vect n l) -> map from (map to ls) = ls
40− fromTo' [] = Refl
41− fromTo' (x :: xs) = rewrite fromTo x in rewrite fromTo' xs in Refl
42−
4334zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
4435zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
4536 where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs