@@ -0,0 +1,35 @@
1+module Control.Isomorphism.Primitives
2+
3+import Control.Isomorphism
4+import Data.ZZ
5+
6+%default total
7+%access public
8+
9+-- This module contains isomorphisms between convenient inductive types and
10+-- Idris primitives. Because primitives lack a convenient structure, these
11+-- arguments typically end with "really_believe_me". This is why they are in a
12+-- separate module.
13+
14+integerIsoZZ : Iso Integer ZZ
15+integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ
16+ where toZZ : Integer -> ZZ
17+ toZZ n = cast n
18+
19+ fromZZ : ZZ -> Integer
20+ fromZZ n = cast n
21+
22+ toFromZZ : (n : Integer) -> fromZZ (toZZ n) = n
23+ toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} refl
24+
25+ fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n
26+ fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl
27+
28+
29+packUnpackIso : Iso (List Char) String
30+packUnpackIso = MkIso pack
31+ unpack
32+ (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} refl)
33+ (\cs => really_believe_me {a = cs=cs} {b = unpack (pack cs) = cs} refl)
34+
35+