git.iko.soy/Idris-dev
on master help sign in
Add a template for bijections to/from primitives

RE #833

commit626d0ea92ad44045a53f0e32a46127f2cd30c502 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 4 Feb 2014, 08:53 (13 years ago) parentb7d6d41
3 files changed+29−1
compare with master
unifiedsplit
idris.cabal+1 libs/base/Control/Isomorphism/Primitives.idr+27 libs/base/base.ipkg+1−1
idris.cabal+1
@@ -77,6 +77,7 @@ Extra-source-files:
7777 libs/base/base.ipkg
7878 libs/base/*.idr
7979 libs/base/Control/*.idr
80+ libs/base/Control/Isomorphism/*.idr
8081 libs/base/Control/Monad/*.idr
8182 libs/base/Data/*.idr
8283 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,
2626 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
2727 Data.Rel, Data.Buffer,
2828
29− Control.Isomorphism,
29+ Control.Isomorphism, Control.Isomorphism.Primitives,
3030 Control.Monad.Identity,
3131 Control.Monad.RWS,
3232 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,