git.iko.soy/Idris-dev
on master help sign in
Replace vectLiftIso with mapIso
9aa0517howtonotwin
libs/contrib/Control/Isomorphism/Extra.idr+6
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1module Control.Isomorphism.Extra
1module Control.Isomorphism.Extra
2
2
3import Control.Isomorphism
3import Control.Isomorphism
4+import Interfaces.Verified
4
5
5%default total
6%default total
6%access public export
7%access public export
@@ -34,3 +35,8 @@ swapped {a} l r = MkIso swap swap prf prf
34 | (No lnx') with (decEq r x)
35 | (No lnx') with (decEq r x)
35 | (Yes rex) = absurd $ rnx rex
36 | (Yes rex) = absurd $ rnx rex
36 | (No rnx') = Refl
37 | (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 @@
1module Control.Isomorphism.Vect
1module Control.Isomorphism.Vect
2
2
3−import Interfaces.Verified
4import Control.Isomorphism
3import Control.Isomorphism
5import Data.Vect
4import Data.Vect
5+import Interfaces.Verified
6
6
7%default total
7%default total
8%access public export
8%access public export
@@ -31,15 +31,6 @@ splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo
31 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
31 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
32 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
32 fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
33
33
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−
43zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
34zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
44zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
35zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
45 where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs
36 where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs