git.iko.soy/Idris-dev
on master help sign in
Add a template for bijections to/from primitives
626d0eaDavid Raymond Christiansen
idris.cabal+1
compare with master
unifiedsplit
@@ -77,6 +77,7 @@ Extra-source-files:
77 libs/base/base.ipkg
77 libs/base/base.ipkg
78 libs/base/*.idr
78 libs/base/*.idr
79 libs/base/Control/*.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+27
@@ -0,0 +1,27 @@
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+
libs/base/base.ipkg+1−1
@@ -26,7 +26,7 @@ modules = System,
26 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
26 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
27 Data.Rel, Data.Buffer,
27 Data.Rel, Data.Buffer,
28
28
29− Control.Isomorphism,
29+ Control.Isomorphism, Control.Isomorphism.Primitives,
30 Control.Monad.Identity,
30 Control.Monad.Identity,
31 Control.Monad.RWS,
31 Control.Monad.RWS,
32 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
32 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,