type-natural 0.1.0.0 → 0.2.0.0

raw patch · 2 files changed

+28/−10 lines, 2 files

Files

• Data/Type/Ordinal.hs +27/−9
• type-natural.cabal +1/−1

@@ -1,5 +1,5 @@ {-# LANGUAGE DataKinds, EmptyDataDecls, FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-} {-# LANGUAGE GADTs, KindSignatures, PolyKinds, StandaloneDeriving           #-} {-# LANGUAGE TypeFamilies, TypeOperators                                    #-} -- | Set-theoretic ordinal arithmetic@@ -9,12 +9,18 @@          -- * Conversion from cardinals to ordinals.          sNatToOrd', sNatToOrd, ordToInt, ordToSNat,          ordToSNat', CastedOrdinal(..),-         unsafeFromInt,+         unsafeFromInt, inclusion, inclusion',          -- * Ordinal arithmetics-         (@+), enumOrdinal+         (@+), enumOrdinal,+         -- * Quasi Quote+         od        ) where import Data.Type.Monomorphic+import Unsafe.Coerce+import Language.Haskell.TH.Quote+import Language.Haskell.TH import Data.Type.Natural hiding (promote)+import Proof.Equational (coerce) import Data.Constraint  -- | Set-theoretic (finite) ordinals:@@ -116,26 +122,38 @@  -- | Inclusion function for ordinals. inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m+inclusion' _ = unsafeCoerce+{-# INLINE inclusion' #-}+{-+-- The "proof" of the correctness of the above+inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m inclusion' (SS SZ) OZ = OZ inclusion' (SS (SS _)) OZ = OZ inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (sS n) m inclusion' _ _ = bugInGHC+-}  -- | Inclusion function for ordinals with codomain inferred.-inclusion :: ((n :<<= m) ~ True, SingRep m) => Ordinal n -> Ordinal m-inclusion = inclusion' sing+inclusion :: ((n :<<= m) ~ True) => Ordinal n -> Ordinal m+inclusion on = unsafeCoerce on+{-# INLINE inclusion #-}  -- | Ordinal addition. (@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) OZ @+ n =   let sn = sing :: SNat n       sm = sing :: SNat m-  in case singInstance (sn %+ sm) of-       SingInstance ->-         case propToBoolLeq (plusLeqR sn sm) of-           Dict -> inclusion n+  in case propToBoolLeq (plusLeqR sn sm) of+      Dict -> inclusion n OS n @+ m =   case sing :: SNat n of     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m     _ -> bugInGHC +-- | Quasiquoter for ordinals+od :: QuasiQuoter+od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read+                 , quoteType = error "No type quoter for Ordinals"+                 , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read+                 , quoteDec = error "No declaration quoter for Ordinals"+                 }

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.1.0.0+version:             0.2.0.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural