Primitives.idr

module Control.Isomorphism.Primitives

import Control.Isomorphism
import Data.ZZ

%default total
%access public

-- This module contains isomorphisms between convenient inductive types and
-- Idris primitives.  Because primitives lack a convenient structure, these
-- arguments typically end with "really_believe_me". This is why they are in a
-- separate module.

integerIsoZZ : Iso Integer ZZ
integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ
  where toZZ : Integer -> ZZ
        toZZ n = cast n

        fromZZ : ZZ -> Integer
        fromZZ n = cast n

        toFromZZ : (n : Integer) -> fromZZ (toZZ n) = n
        toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} Refl

        fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n
        fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} Refl


packUnpackIso : Iso (List Char) String
packUnpackIso = MkIso pack
                      unpack
                      (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} Refl)
                      (\cs  => really_believe_me {a = cs=cs}   {b = unpack (pack cs) = cs}   Refl)