content: {-# LANGUAGE DataKinds, GADTs, TypeFamilies, TypeOperators,
               ConstraintKinds, ScopedTypeVariables, RankNTypes #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE DeriveDataTypeable#-}
  {-# LANGUAGE CPP #-}
  
  module Numerical.Nat(Nat(..),N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10
      ,SNat(..), type (+),plus_id_r,plus_succ_r,gcastWith,Proxy(..),LitNat,U)  where
  import Data.Typeable
  import Data.Data
  import qualified GHC.TypeLits as TL
  
  
  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
  import Data.Type.Equality(gcastWith)
  #else
  import Data.Proxy
  #endif
  
  
  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904
  import Data.Kind (Type)
  #endif 
  
  
  type LitNat = TL.Nat
  
  data Nat = S !Nat  | Z
      deriving (Eq,Show,Read,Typeable,Data)
  
  #if defined(__GLASGOW_HASKELL__) && ( __GLASGOW_HASKELL__ >= 707) && ( __GLASGOW_HASKELL__ < 709)
  deriving instance Typeable 'Z
  deriving instance Typeable 'S
  #endif
  
  {-
  use closed type families when available,
  need to test that the
  -}
  
  
  type family U (n:: TL.Nat) :: Nat  where
    U 0 = 'Z
    U n = 'S (U (((TL.-)) n  1))
  
  
  type family n1 + n2 where
    'Z + n2 = n2
    ('S n1') + n2 = 'S (n1' + n2)
  
  
  --  ghc 7.6 instances
  
  --type family U (n:: (TL.Nat)) :: Nat
  
  ---- can't induct, hence crippled
  --type instance U n = Z
  
  --type family (n1::Nat) + (n2::Nat) :: Nat
  --type instance Z + n2 = n2
  --type instance  (S n1) + n2 = S (n1 + n2)
  --gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
  --gcastWith Refl x = x
  --data a :~: b where
  --  Refl :: a :~: a
  
  
  
  
  
  -- singleton for Nat
  #if __GLASGOW_HASKELL__ < 904
  
  data SNat :: Nat -> * where
    SZero :: SNat 'Z
    SSucc :: SNat n -> SNat ('S n)
  #else   
  
  data SNat :: Nat -> Type where
    SZero :: SNat 'Z
    SSucc :: SNat n -> SNat ('S n)
  #endif 
  
  
  -- inductive proof of right-identity of +
  plus_id_r :: SNat n -> ((n + 'Z) :~: n)
  plus_id_r SZero = Refl
  plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
  
  -- inductive proof of simplification on the rhs of +
  plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + ('S n2)) :~: ('S (n1 + n2)))
  plus_succ_r SZero _ = Refl
  plus_succ_r (SSucc n1) proxy_n2 = gcastWith (plus_succ_r n1 proxy_n2) Refl
  
  
  
  type N0 = 'Z
  
  type N1 = 'S N0
  
  type N2 = 'S N1
  
  type N3 = 'S N2
  
  type N4 = 'S N3
  
  type N5 = 'S N4
  
  type N6 = 'S N5
  
  type N7 = 'S N6
  
  type N8 = 'S N7
  
  type N9 = 'S N8
  
  type N10 = 'S N9
  