Sets.hs

{-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
             UndecidableInstances, ScopedTypeVariables,
             Rank2Types #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-name-shadowing #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.TypeLevel.Num.Sets
-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
--                    and KTH's SAM group 
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  alfonso.acosta@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable (non-standard instances)
--
-- Type-level numerical sets. Currently there is only support for Naturals and 
-- Positives.
-- 
----------------------------------------------------------------------------
module Data.TypeLevel.Num.Sets (Pos, Nat, toNum, toInt, reifyIntegral) where 

import Data.TypeLevel.Num.Reps

-----------
-- Naturals
-----------


-- The well-formedness condition, the kind predicate.
-- These classes are internal, denoted by the ending "I", which is removed in 
-- the exported proxies (read below)

-- | Naturals (Positives and zero), internal version
class NatI n where 
 -- | Reflecting function
 toNum :: Num a => n -> a


-- | Less generic reflecting function (Int)
toInt :: Nat n => n -> Int
toInt =  toNum



-- | Positives (Naturals without zero), internal version
class NatI n => PosI n

-- To prevent the user from adding new instances to NatI and especially
-- to PosI (e.g., to prevent the user from adding the instance |Pos D0|)
-- we do NOT export NatI and PosI. Rather, we export the following proxies.
-- The proxies entail PosI and NatI and so can be used to add PosI and NatI
-- constraints in the signatures. However, all the constraints below
-- are expressed in terms of NatI and PosI rather than proxies. Thus,
-- even if the user adds new instances to proxies, it would not matter.
-- Besides, because the following proxy instances are most general,
-- one may not add further instances without overlapping instance extension.

-- | Naturals (Positives and zero)
class    NatI n => Nat n
instance NatI n => Nat n

-- | Positives (Naturals without zero)
class    PosI n => Pos n
instance PosI n => Pos n

--------------------
-- Natural Instances
--------------------

-- Note: TH would be helpful to sistematically define instances 
--       (our type level operations)
--       However, type-splicing is not yet implemented in GHC :S

-- monodigit naturals
instance NatI D0 where toNum _ = fromInteger 0
instance NatI D1 where toNum _ = fromInteger 1
instance NatI D2 where toNum _ = fromInteger 2
instance NatI D3 where toNum _ = fromInteger 3
instance NatI D4 where toNum _ = fromInteger 4
instance NatI D5 where toNum _ = fromInteger 5
instance NatI D6 where toNum _ = fromInteger 6
instance NatI D7 where toNum _ = fromInteger 7
instance NatI D8 where toNum _ = fromInteger 8
instance NatI D9 where toNum _ = fromInteger 9

-- multidigit naturals
-- Note: The PosI constraint guarantees that all valid representations are 
-- normalized (i.e. D0 :* D1 will lead to a compiler error)
-- Note as well that ill-formed representations such as
-- (D1 :* D2) :* (D3 :* D4) are not recognized as instances of
-- naturals nor positives.
instance PosI x => NatI (x :* D0) where toNum n = subLastDec n
instance PosI x => NatI (x :* D1) where toNum n = subLastDec n + fromInteger 1
instance PosI x => NatI (x :* D2) where toNum n = subLastDec n + fromInteger 2
instance PosI x => NatI (x :* D3) where toNum n = subLastDec n + fromInteger 3
instance PosI x => NatI (x :* D4) where toNum n = subLastDec n + fromInteger 4
instance PosI x => NatI (x :* D5) where toNum n = subLastDec n + fromInteger 5
instance PosI x => NatI (x :* D6) where toNum n = subLastDec n + fromInteger 6
instance PosI x => NatI (x :* D7) where toNum n = subLastDec n + fromInteger 7
instance PosI x => NatI (x :* D8) where toNum n = subLastDec n + fromInteger 8
instance PosI x => NatI (x :* D9) where toNum n = subLastDec n + fromInteger 9

-- monodigit positives
instance PosI D1
instance PosI D2
instance PosI D3
instance PosI D4
instance PosI D5
instance PosI D6
instance PosI D7
instance PosI D8
instance PosI D9

-- multidigit positives
-- Note: The PosI constraint guarantees that all valid representations are 
-- normalized (i.e. D0 :* D1 will lead to a compiler error)
instance PosI x => PosI (x :* D0)
instance PosI x => PosI (x :* D1)
instance PosI x => PosI (x :* D2)
instance PosI x => PosI (x :* D3)
instance PosI x => PosI (x :* D4)
instance PosI x => PosI (x :* D5)
instance PosI x => PosI (x :* D6)
instance PosI x => PosI (x :* D7)
instance PosI x => PosI (x :* D8)
instance PosI x => PosI (x :* D9)


-- | Reification function. In CPS style (best possible solution)
reifyIntegral :: Integral i => i -> (forall n . Nat n => n -> r) -> r
reifyIntegral i f 
 | i < 0     = error "reifyIntegral: integral < 0"
 | i == 0    = f (undefined :: D0)
 | otherwise = reifyIntegralp i f 
       -- reifyIntegral for positives
 where reifyIntegralp :: Integral i => i -> (forall n . Pos n => n -> r) -> r
       reifyIntegralp i f 
         | i < 10 = case i of
                     1 -> f (undefined :: D1)
                     2 -> f (undefined :: D2); 3 -> f (undefined :: D3)
                     4 -> f (undefined :: D4); 5 -> f (undefined :: D5)
                     6 -> f (undefined :: D6); 7 -> f (undefined :: D7)
                     8 -> f (undefined :: D8); 9 -> f (undefined :: D9)
         | otherwise =  
            case m of
              0 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D0)) 
              1 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D1))
              2 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D2))
              3 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D3))
              4 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D4))
              5 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D5))
              6 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D6))
              7 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D7))
              8 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D8))
              9 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D9))      
           where (d,m) = divMod i 10


---------------------
-- Internal functions
---------------------

-- substract the last digit of a decimal type-level numeral and obtain 
-- the result's reflected value 
{-# INLINE subLastDec #-}
subLastDec :: (Num a, NatI (x :* d), NatI x) => x :* d -> a
subLastDec = (10*).toNum.div10Dec

-- Divide a decimal type-level numeral by 10 
{-# INLINE div10Dec #-} 
div10Dec :: NatI (x :* d) => x :* d -> x
div10Dec _ = undefined