524f27f · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -77,6 +77,7 @@ Extra-source-files:

77 libs/base/base.ipkg

78 libs/base/*.idr

79 libs/base/Control/*.idr

80+ libs/base/Control/Isomorphism/*.idr

80 libs/base/Control/Monad/*.idr

81 libs/base/Control/Monad/*.idr

81 libs/base/Data/*.idr

82 libs/base/Data/*.idr

82 libs/base/Data/Vect/*.idr

83 libs/base/Data/Vect/*.idr

libs/base/Control/Isomorphism/Primitives.idrnew file+35

@@ -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+

libs/base/base.ipkg+1−1

@@ -26,7 +26,7 @@ modules = System,

26 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

27 Data.Rel, Data.Buffer,

28

29− Control.Isomorphism,

29+ Control.Isomorphism, Control.Isomorphism.Primitives,

30 Control.Monad.Identity,

31 Control.Monad.RWS,

32 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,