-- TODO: see also {-# OPTIONS_GHC -Wall -fwarn-tabs #-} {-# LANGUAGE EmptyDataDecls , DeriveDataTypeable , MultiParamTypeClasses , FlexibleContexts , FlexibleInstances , UndecidableInstances , FunctionalDependencies , TypeOperators #-} {- -- for reifyNat... {-# LANGUAGE RankNTypes #-} -} {-# LANGUAGE CPP #-} #if __GLASGOW_HASKELL__ >= 701 -- N.B., Data.Proxy isn't "safe". {-# LANGUAGE Trustworthy #-} #endif ---------------------------------------------------------------- -- 2013.05.29 -- | -- Module : Data.Number.Fin.TyDecimal -- Copyright : 2012--2013 wren ng thornton, -- 2004--2007 Oleg Kiselyov and Chung-chieh Shan -- License : BSD3 -- Maintainer : wren@community.haskell.org -- Stability : experimental -- Portability : non-portable -- -- Type-level decimal natural numbers. This is based on [1], and is -- intended to work with [2] (though we use the @reflection@ package -- for the actual reification part). -- -- Recent versions of GHC have type-level natural number literals. -- Ideally, this module would be completely obviated by that work. -- Unfortunately, the type-level literals aren't quite ready for -- prime time yet, because they do not have a solver. Thus, we're -- implementing here stuff that should be handled natively by GHC -- in the future. A lot of this also duplicates the functionality -- in @HList:Data.HList.FakePrelude@[3], which is (or should be) -- obviated by the new data kinds extension. -- -- [1] Oleg Kiselyov and Chung-chieh Shan. (2007) /Lightweight/ -- /static resources: Sexy types for embedded and systems/ -- /programming/. Proc. Trends in Functional Programming. -- New York, 2--4 April 2007. -- -- -- [2] Oleg Kiselyov and Chung-chieh Shan. (2004) /Implicit/ -- /configurations: or, type classes reflect the values of/ -- /types/. Proc. ACM SIGPLAN 2004 workshop on Haskell. -- Snowbird, Utah, USA, 22 September 2004. pp.33--44. -- -- -- [3] ---------------------------------------------------------------- module Data.Number.Fin.TyDecimal ( -- * Representation -- ** Type-level decimal natural numbers D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, (:.) -- ** Type-level 'Ordering' , LT_, EQ_, GT_ -- * Kind predicates , Nat, NatNE0 -- * Proxies for some small numbers , nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 -- * Aliases for some large numbers , MaxBoundInt8 , MaxBoundInt16 , MaxBoundInt32 , MaxBoundInt64 , MaxBoundWord8 , MaxBoundWord16 , MaxBoundWord32 , MaxBoundWord64 -- * Arithmetic -- ** successor\/predecessor , Succ, succ, pred -- ** addition\/subtraction , Add, add, minus, subtract -- ** comparison , Compare, compare, NatLE, NatLT, assert_NatLE, min, max {- -- ** multiplication\/division , Mul, mul, div, div10 -- mul10 ? -- ** exponentiation\/logarithm , Exp10, exp10, log10 -- ** GCD , GCD, gcd -} ) where import Prelude hiding (succ, pred, subtract, compare, div, gcd, max, min) import Data.Typeable (Typeable) import Data.Proxy (Proxy(Proxy)) import Data.Reflection (Reifies(reflect)) import Data.Number.Fin.TyOrdering ---------------------------------------------------------------- -- | The digit 0. data D0 deriving Typeable -- | The digit 1. data D1 deriving Typeable -- | The digit 2. data D2 deriving Typeable -- | The digit 3. data D3 deriving Typeable -- | The digit 4. data D4 deriving Typeable -- | The digit 5. data D5 deriving Typeable -- | The digit 6. data D6 deriving Typeable -- | The digit 7. data D7 deriving Typeable -- | The digit 8. data D8 deriving Typeable -- | The digit 9. data D9 deriving Typeable -- | The connective. This should only be used left associatively -- (it associates to the left naturally). Decimal digits are -- lexicographically big-endian, so they're written as usual; -- however, they're structurally little-endian due to the left -- associativity. data x :. y deriving Typeable infixl 5 :. -- | Is @n@ a well-formed type of kind @Nat@? The only well-formed -- types of kind @Nat@ are type-level natural numbers in structurally -- little-endian decimal. -- -- The hidden type class @(Nat_ n)@ entails @(Reifies n Integer)@. class Nat_ n => Nat n instance Nat_ n => Nat n -- this instance is "undecidable" -- | Is @n@ a well-formed type of kind @NatNE0@? The only well-formed -- types of kind @NatNE0@ are the non-zero well-formed types of -- kind @Nat@;, i.e., the type-level whole numbers in structurally -- little-endian decimal. -- -- The hidden type class @(NatNE0_ n)@ entails @(Nat_ n)@ and -- @(Reifies n Integer)@. class NatNE0_ n => NatNE0 n instance NatNE0_ n => NatNE0 n -- this instance is "undecidable" -- for internal use only. class Digit_ d instance Digit_ D0 instance Digit_ D1 instance Digit_ D2 instance Digit_ D3 instance Digit_ D4 instance Digit_ D5 instance Digit_ D6 instance Digit_ D7 instance Digit_ D8 instance Digit_ D9 -- for internal use only. class (Reifies n Integer, Nat_ n) => NatNE0_ n instance NatNE0_ D1 instance NatNE0_ D2 instance NatNE0_ D3 instance NatNE0_ D4 instance NatNE0_ D5 instance NatNE0_ D6 instance NatNE0_ D7 instance NatNE0_ D8 instance NatNE0_ D9 instance NatNE0_ n => NatNE0_ (n:.D0) instance NatNE0_ n => NatNE0_ (n:.D1) instance NatNE0_ n => NatNE0_ (n:.D2) instance NatNE0_ n => NatNE0_ (n:.D3) instance NatNE0_ n => NatNE0_ (n:.D4) instance NatNE0_ n => NatNE0_ (n:.D5) instance NatNE0_ n => NatNE0_ (n:.D6) instance NatNE0_ n => NatNE0_ (n:.D7) instance NatNE0_ n => NatNE0_ (n:.D8) instance NatNE0_ n => NatNE0_ (n:.D9) -- for internal use only. class (Reifies n Integer) => Nat_ n instance Nat_ D0 instance Nat_ D1 instance Nat_ D2 instance Nat_ D3 instance Nat_ D4 instance Nat_ D5 instance Nat_ D6 instance Nat_ D7 instance Nat_ D8 instance Nat_ D9 instance NatNE0_ x => Nat_ (x:.D0) instance NatNE0_ x => Nat_ (x:.D1) instance NatNE0_ x => Nat_ (x:.D2) instance NatNE0_ x => Nat_ (x:.D3) instance NatNE0_ x => Nat_ (x:.D4) instance NatNE0_ x => Nat_ (x:.D5) instance NatNE0_ x => Nat_ (x:.D6) instance NatNE0_ x => Nat_ (x:.D7) instance NatNE0_ x => Nat_ (x:.D8) instance NatNE0_ x => Nat_ (x:.D9) -- BUG: stack overflow issues, unlike the big-endian notation? instance Reifies D0 Integer where reflect _ = 0 instance Reifies D1 Integer where reflect _ = 1 instance Reifies D2 Integer where reflect _ = 2 instance Reifies D3 Integer where reflect _ = 3 instance Reifies D4 Integer where reflect _ = 4 instance Reifies D5 Integer where reflect _ = 5 instance Reifies D6 Integer where reflect _ = 6 instance Reifies D7 Integer where reflect _ = 7 instance Reifies D8 Integer where reflect _ = 8 instance Reifies D9 Integer where reflect _ = 9 instance NatNE0_ x => Reifies (x:.D0) Integer where reflect p = 10 * reflect (div10 p) instance NatNE0_ x => Reifies (x:.D1) Integer where reflect p = 10 * reflect (div10 p) + 1 instance NatNE0_ x => Reifies (x:.D2) Integer where reflect p = 10 * reflect (div10 p) + 2 instance NatNE0_ x => Reifies (x:.D3) Integer where reflect p = 10 * reflect (div10 p) + 3 instance NatNE0_ x => Reifies (x:.D4) Integer where reflect p = 10 * reflect (div10 p) + 4 instance NatNE0_ x => Reifies (x:.D5) Integer where reflect p = 10 * reflect (div10 p) + 5 instance NatNE0_ x => Reifies (x:.D6) Integer where reflect p = 10 * reflect (div10 p) + 6 instance NatNE0_ x => Reifies (x:.D7) Integer where reflect p = 10 * reflect (div10 p) + 7 instance NatNE0_ x => Reifies (x:.D8) Integer where reflect p = 10 * reflect (div10 p) + 8 instance NatNE0_ x => Reifies (x:.D9) Integer where reflect p = 10 * reflect (div10 p) + 9 -- HACK: we can't actually monomorphize the input, given our use case. -- | Return a 'Proxy' for the floor of the input divided by 10. Using -- @div10 n@ differs from using @n \`div\` nat10@ in that we take the -- floor of the result rather than being ill-typed; also in that -- @div10@ isn't defined on single-digit numbers. div10 :: proxy (h:.t) -> Proxy h div10 _ = Proxy {-# INLINE div10 #-} {- -- BUG: how can we do this CPS version which properly constrains @x@ to Nat_? It wasn't so hard with the big-endian notation... reifyNat :: Integer -> (forall x. Nat_ x => Proxy x -> r) -> r reifyNat i k | i <= 0 = k (Proxy :: Proxy D0) | otherwise = let (d,m) = divMod i 10 in case m of 0 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D0))) 1 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D1))) 2 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D2))) 3 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D3))) 4 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D4))) 5 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D5))) 6 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D6))) 7 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D7))) 8 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D8))) 9 -> reifyNat d (\p -> k (snoc p (Proxy :: Proxy D9))) _ -> error "Data.Number.Fin.TyDecimal.reifyNat: the impossible happened" where -- BUG: Could not deduce (Snoc x10 D0 x) from the context (Nat_ x10) [etc] snoc :: Snoc x d y => Proxy x -> Proxy d -> Proxy y snoc _ _ = Proxy -} nat0 :: Proxy D0; nat0 = Proxy nat1 :: Proxy D1; nat1 = Proxy nat2 :: Proxy D2; nat2 = Proxy nat3 :: Proxy D3; nat3 = Proxy nat4 :: Proxy D4; nat4 = Proxy nat5 :: Proxy D5; nat5 = Proxy nat6 :: Proxy D6; nat6 = Proxy nat7 :: Proxy D7; nat7 = Proxy nat8 :: Proxy D8; nat8 = Proxy nat9 :: Proxy D9; nat9 = Proxy -- type MinBoundInt8 = Negative (D1:.D2:.D8) -- type MinBoundInt16 = Negative (D3:.D2:. D7:.D6:.D8) -- type MinBoundInt32 = Negative (D2:. D1:.D4:.D7:. D4:.D8:.D3:. D6:.D4:.D8) -- type MinBoundInt64 = -- Negative (D9:. D2:.D2:.D3:. D3:.D7:.D2:. D0:.D3:.D6:. D8:.D5:.D4:. D7:.D7:.D5:. D8:.D0:.D8) -- TODO: MinBoundInt type MaxBoundInt8 = D1:.D2:.D7 type MaxBoundInt16 = D3:.D2:.D7:.D6:.D7 type MaxBoundInt32 = D2:.D1:.D4:.D7:.D4:.D8:.D3:.D6:.D4:.D7 type MaxBoundInt64 = D9:.D2:.D2:.D3:.D3:.D7:.D2:.D0:.D3:.D6:.D8:.D5:.D4:.D7:.D7:.D5:.D8:.D0:.D7 -- TODO: MaxBoundInt type MaxBoundWord8 = D2:.D5:.D5 type MaxBoundWord16 = D6:.D5:.D5:.D3:.D5 type MaxBoundWord32 = D4:.D2:.D9:.D4:.D9:.D6:.D7:.D2:.D9:.D5 type MaxBoundWord64 = D1:.D8:.D4:.D4:.D6:.D7:.D4:.D4:.D0:.D7:.D3:.D7:.D0:.D9:.D5:.D5:.D1:.D6:.D1:.D5 -- TODO: MaxBoundWord ---------------------------------------------------------------- -- BUG: We can't automatically deduce (NatLE x y) nor (NatLT x y) from (Succ x y). We can add them as additional constraints on the instances; and that works to get everything in this package to typecheck, but it causes infinite loops whenever we actually try to use Succ as a type-function in real code... -- | The successor\/predecessor relation; by structural induction -- on the first argument. Modes: -- -- > Succ x (succ x) -- i.e., given x, return the successor of x -- > Succ (pred y) y -- i.e., given y, return the predecessor of y -- class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> x instance Succ D0 D1 instance Succ D1 D2 instance Succ D2 D3 instance Succ D3 D4 instance Succ D4 D5 instance Succ D5 D6 instance Succ D6 D7 instance Succ D7 D8 instance Succ D8 D9 instance Succ D9 (D1:.D0) instance (NatNE0_ x) => Succ (x:.D0) (x :.D1) instance (NatNE0_ x) => Succ (x:.D1) (x :.D2) instance (NatNE0_ x) => Succ (x:.D2) (x :.D3) instance (NatNE0_ x) => Succ (x:.D3) (x :.D4) instance (NatNE0_ x) => Succ (x:.D4) (x :.D5) instance (NatNE0_ x) => Succ (x:.D5) (x :.D6) instance (NatNE0_ x) => Succ (x:.D6) (x :.D7) instance (NatNE0_ x) => Succ (x:.D7) (x :.D8) instance (NatNE0_ x) => Succ (x:.D8) (x :.D9) instance (NatNE0_ x, Succ x (y:.d)) => Succ (x:.D9) (y :.d :.D0) -- this last case triggers the need for undecidable instances succ :: Succ x y => Proxy x -> Proxy y succ _ = Proxy {-# INLINE succ #-} pred :: Succ x y => Proxy y -> Proxy x pred _ = Proxy {-# INLINE pred #-} -- | Assert @10*x + d == y@ where @d@ is a decimal digit and both @x@ -- and @y@ are decimal numbers. @x@ may be zero. Essentially, this -- is the general, non-structural, constructor\/deconstructor of a -- decimal number. This is like the assertion @x:.d ~ y@ except that -- we trim leading zeros of @y@ in order to ensure that it is -- well-formed. class (Digit_ d, Nat_ x, Nat_ y) => Snoc x d y | x d -> y, y -> x d instance Snoc D0 D0 D0 instance Snoc D0 D1 D1 instance Snoc D0 D2 D2 instance Snoc D0 D3 D3 instance Snoc D0 D4 D4 instance Snoc D0 D5 D5 instance Snoc D0 D6 D6 instance Snoc D0 D7 D7 instance Snoc D0 D8 D8 instance Snoc D0 D9 D9 instance (Digit_ d, Nat_ (D1:.d)) => Snoc D1 d (D1:.d) instance (Digit_ d, Nat_ (D2:.d)) => Snoc D2 d (D2:.d) instance (Digit_ d, Nat_ (D3:.d)) => Snoc D3 d (D3:.d) instance (Digit_ d, Nat_ (D4:.d)) => Snoc D4 d (D4:.d) instance (Digit_ d, Nat_ (D5:.d)) => Snoc D5 d (D5:.d) instance (Digit_ d, Nat_ (D6:.d)) => Snoc D6 d (D6:.d) instance (Digit_ d, Nat_ (D7:.d)) => Snoc D7 d (D7:.d) instance (Digit_ d, Nat_ (D8:.d)) => Snoc D8 d (D8:.d) instance (Digit_ d, Nat_ (D9:.d)) => Snoc D9 d (D9:.d) instance (Digit_ d', Nat_ (x:.d), Nat_ (x:.d:.d')) => Snoc (x:.d) d' (x:.d:.d') -- | The primitive addition relation; by structural induction on -- the first argument. Modes: -- -- > Add_ x y (x+y) -- > Add_ x (z-x) z -- when it's defined. -- class (Nat_ x, Nat_ y, Nat_ z) => Add_ x y z | x y -> z, z x -> y instance (Nat_ y) => Add_ D0 y y instance (Succ y y1) => Add_ D1 y y1 instance (Succ y y1, Succ y1 y2) => Add_ D2 y y2 instance (Succ y y1, Succ y1 y2, Succ y2 y3) => Add_ D3 y y3 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4 ) => Add_ D4 y y4 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4, Succ y4 y5 ) => Add_ D5 y y5 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4, Succ y4 y5, Succ y5 y6 ) => Add_ D6 y y6 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4, Succ y4 y5, Succ y5 y6 , Succ y6 y7 ) => Add_ D7 y y7 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4, Succ y4 y5, Succ y5 y6 , Succ y6 y7, Succ y7 y8 ) => Add_ D8 y y8 instance ( Succ y y1, Succ y1 y2, Succ y2 y3 , Succ y3 y4, Succ y4 y5, Succ y5 y6 , Succ y6 y7, Succ y7 y8, Succ y8 y9 ) => Add_ D9 y y9 instance (NatNE0_ x, NatNE0_ (z:.dz), Add_ x y' z, Snoc y' dz y) => Add_ (x:.D0) y (z:.dz) instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D1 (zh:.dy) z) => Add_ (x:.D1) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D2 (zh:.dy) z) => Add_ (x:.D2) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D3 (zh:.dy) z) => Add_ (x:.D3) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D4 (zh:.dy) z) => Add_ (x:.D4) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D5 (zh:.dy) z) => Add_ (x:.D5) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D6 (zh:.dy) z) => Add_ (x:.D6) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D7 (zh:.dy) z) => Add_ (x:.D7) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D8 (zh:.dy) z) => Add_ (x:.D8) y z instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D9 (zh:.dy) z) => Add_ (x:.D9) y z -- | The addition relation with full dependencies. Modes: -- -- > Add x y (x+y) -- > Add x (z-x) z -- when it's defined. -- > Add (z-y) y z -- when it's defined. -- class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x instance (Add_ x y z, Add_ y x z) => Add x y z add :: Add x y z => Proxy x -> Proxy y -> Proxy z add _ _ = Proxy {-# INLINE add #-} -- | N.B., this will be ill-typed if @x@ is greater than @z@. minus :: Add x y z => Proxy z -> Proxy x -> Proxy y minus _ _ = Proxy {-# INLINE minus #-} -- | N.B., this will be ill-typed if @x@ is greater than @z@. subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y subtract _ _ = Proxy {-# INLINE subtract #-} ---------------------------------------------------------------- -- Equality and order: the comparison relation -- | Assert that the comparison relation @r@ (@LT_@, @EQ_@, or -- @GT_@) holds between @x@ and @y@; by structural induction on the -- first, and then the second argument. class (Nat_ x, Nat_ y) => Compare x y r | x y -> r instance Compare D0 D0 EQ_ instance Compare D0 D1 LT_ instance Compare D0 D2 LT_ instance Compare D0 D3 LT_ instance Compare D0 D4 LT_ instance Compare D0 D5 LT_ instance Compare D0 D6 LT_ instance Compare D0 D7 LT_ instance Compare D0 D8 LT_ instance Compare D0 D9 LT_ instance NatNE0_ (y:.dy) => Compare D0 (y:.dy) LT_ instance Compare D1 D0 GT_ instance Compare D1 D1 EQ_ instance Compare D1 D2 LT_ instance Compare D1 D3 LT_ instance Compare D1 D4 LT_ instance Compare D1 D5 LT_ instance Compare D1 D6 LT_ instance Compare D1 D7 LT_ instance Compare D1 D8 LT_ instance Compare D1 D9 LT_ instance NatNE0_ (y:.dy) => Compare D1 (y:.dy) LT_ instance Compare D2 D0 GT_ instance Compare D2 D1 GT_ instance Compare D2 D2 EQ_ instance Compare D2 D3 LT_ instance Compare D2 D4 LT_ instance Compare D2 D5 LT_ instance Compare D2 D6 LT_ instance Compare D2 D7 LT_ instance Compare D2 D8 LT_ instance Compare D2 D9 LT_ instance NatNE0_ (y:.dy) => Compare D2 (y:.dy) LT_ instance Compare D3 D0 GT_ instance Compare D3 D1 GT_ instance Compare D3 D2 GT_ instance Compare D3 D3 EQ_ instance Compare D3 D4 LT_ instance Compare D3 D5 LT_ instance Compare D3 D6 LT_ instance Compare D3 D7 LT_ instance Compare D3 D8 LT_ instance Compare D3 D9 LT_ instance NatNE0_ (y:.dy) => Compare D3 (y:.dy) LT_ instance Compare D4 D0 GT_ instance Compare D4 D1 GT_ instance Compare D4 D2 GT_ instance Compare D4 D3 GT_ instance Compare D4 D4 EQ_ instance Compare D4 D5 LT_ instance Compare D4 D6 LT_ instance Compare D4 D7 LT_ instance Compare D4 D8 LT_ instance Compare D4 D9 LT_ instance NatNE0_ (y:.dy) => Compare D4 (y:.dy) LT_ instance Compare D5 D0 GT_ instance Compare D5 D1 GT_ instance Compare D5 D2 GT_ instance Compare D5 D3 GT_ instance Compare D5 D4 GT_ instance Compare D5 D5 EQ_ instance Compare D5 D6 LT_ instance Compare D5 D7 LT_ instance Compare D5 D8 LT_ instance Compare D5 D9 LT_ instance NatNE0_ (y:.dy) => Compare D5 (y:.dy) LT_ instance Compare D6 D0 GT_ instance Compare D6 D1 GT_ instance Compare D6 D2 GT_ instance Compare D6 D3 GT_ instance Compare D6 D4 GT_ instance Compare D6 D5 GT_ instance Compare D6 D6 EQ_ instance Compare D6 D7 LT_ instance Compare D6 D8 LT_ instance Compare D6 D9 LT_ instance NatNE0_ (y:.dy) => Compare D6 (y:.dy) LT_ instance Compare D7 D0 GT_ instance Compare D7 D1 GT_ instance Compare D7 D2 GT_ instance Compare D7 D3 GT_ instance Compare D7 D4 GT_ instance Compare D7 D5 GT_ instance Compare D7 D6 GT_ instance Compare D7 D7 EQ_ instance Compare D7 D8 LT_ instance Compare D7 D9 LT_ instance NatNE0_ (y:.dy) => Compare D7 (y:.dy) LT_ instance Compare D8 D0 GT_ instance Compare D8 D1 GT_ instance Compare D8 D2 GT_ instance Compare D8 D3 GT_ instance Compare D8 D4 GT_ instance Compare D8 D5 GT_ instance Compare D8 D6 GT_ instance Compare D8 D7 GT_ instance Compare D8 D8 EQ_ instance Compare D8 D9 LT_ instance NatNE0_ (y:.dy) => Compare D8 (y:.dy) LT_ instance Compare D9 D0 GT_ instance Compare D9 D1 GT_ instance Compare D9 D2 GT_ instance Compare D9 D3 GT_ instance Compare D9 D4 GT_ instance Compare D9 D5 GT_ instance Compare D9 D6 GT_ instance Compare D9 D7 GT_ instance Compare D9 D8 GT_ instance Compare D9 D9 EQ_ instance NatNE0_ (y:.dy) => Compare D9 (y:.dy) LT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D0 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D1 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D2 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D3 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D4 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D5 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D6 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D7 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D8 GT_ instance NatNE0_ (x:.dx) => Compare (x:.dx) D9 GT_ instance ( NatNE0_ (x:.dx), NatNE0_ (y:.dy) , Compare dx dy dr, Compare x y r', NCS r' dr r ) => Compare (x:.dx) (y:.dy) r compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r compare _ _ = Proxy {-# INLINE compare #-} -- BUG: is this still an optimization now that there's a combinatorial explosion? -- | Assert that @x <= y@. This is a popular constraint, so we -- implement it specially. We could have said that @Add n x y => -- NatLE x y@, but the following inductive definition is a bit -- more optimal. class (Nat_ x, Nat_ y) => NatLE x y instance NatLE D0 D0 instance NatLE D0 D1 instance NatLE D0 D2 instance NatLE D0 D3 instance NatLE D0 D4 instance NatLE D0 D5 instance NatLE D0 D6 instance NatLE D0 D7 instance NatLE D0 D8 instance NatLE D0 D9 instance NatNE0_ (y:.dy) => NatLE D0 (y:.dy) instance NatLE D1 D1 instance NatLE D1 D2 instance NatLE D1 D3 instance NatLE D1 D4 instance NatLE D1 D5 instance NatLE D1 D6 instance NatLE D1 D7 instance NatLE D1 D8 instance NatLE D1 D9 instance NatNE0_ (y:.dy) => NatLE D1 (y:.dy) instance NatLE D2 D2 instance NatLE D2 D3 instance NatLE D2 D4 instance NatLE D2 D5 instance NatLE D2 D6 instance NatLE D2 D7 instance NatLE D2 D8 instance NatLE D2 D9 instance NatNE0_ (y:.dy) => NatLE D2 (y:.dy) instance NatLE D3 D3 instance NatLE D3 D4 instance NatLE D3 D5 instance NatLE D3 D6 instance NatLE D3 D7 instance NatLE D3 D8 instance NatLE D3 D9 instance NatNE0_ (y:.dy) => NatLE D3 (y:.dy) instance NatLE D4 D4 instance NatLE D4 D5 instance NatLE D4 D6 instance NatLE D4 D7 instance NatLE D4 D8 instance NatLE D4 D9 instance NatNE0_ (y:.dy) => NatLE D4 (y:.dy) instance NatLE D5 D5 instance NatLE D5 D6 instance NatLE D5 D7 instance NatLE D5 D8 instance NatLE D5 D9 instance NatNE0_ (y:.dy) => NatLE D5 (y:.dy) instance NatLE D6 D6 instance NatLE D6 D7 instance NatLE D6 D8 instance NatLE D6 D9 instance NatNE0_ (y:.dy) => NatLE D6 (y:.dy) instance NatLE D7 D7 instance NatLE D7 D8 instance NatLE D7 D9 instance NatNE0_ (y:.dy) => NatLE D7 (y:.dy) instance NatLE D8 D8 instance NatLE D8 D9 instance NatNE0_ (y:.dy) => NatLE D8 (y:.dy) instance NatLE D9 D9 instance NatNE0_ (y:.dy) => NatLE D9 (y:.dy) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D0) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D1) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D2) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D3) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D1) (y:.D0) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D1) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D2) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D3) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D1) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D2) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D3) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D2) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D3) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D3) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D3) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D4) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D3) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D4) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D5) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D3) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D4) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D5) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D6) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D3) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D4) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D5) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D6) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D7) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D9) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D0) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D1) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D2) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D3) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D4) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D5) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D6) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D7) instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D8) instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D9) (y:.D9) -- | N.B., this will be ill-typed if @x@ is greater than @y@. assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> () assert_NatLE Proxy Proxy = () -- | Assert that @x < y@. This is just a shorthand for @x <= pred y@. class (Nat_ x, NatNE0_ y) => NatLT x y instance (Succ y' y, NatLE x y') => NatLT x y -- | Choose the larger of @x@ and @y@ according to the order @r@. class Max_ x y r z | x y r -> z instance Max_ x y LT_ y instance Max_ x y EQ_ y -- doesn't matter which we pick instance Max_ x y GT_ x -- | Choose the larger of @x@ and @y@. max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z max _ _ = Proxy {-# INLINE max #-} -- | Choose the smaller of @x@ and @y@ according to the order @r@. class Min_ x y r z | x y r -> z instance Min_ x y LT_ x instance Min_ x y EQ_ x -- doesn't matter which we pick instance Min_ x y GT_ y -- | Choose the smaller of @x@ and @y@. min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z min _ _ = Proxy {-# INLINE min #-} {- ---------------------------------------------------------------- -- TODO: should we offer @((floor.). div)@, @((ceiling.). div)@, @divMod@ ? -- | Assert that @x * y == z@ where @x > 0@; by structural induction -- on the first argument. class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_ x y z | x y -> z, x z -> y instance Nat_ y => Mul_ B1 y y instance (Mul_ x y zh, Snoc zh B0 z) => Mul_ (x:.B0) y z instance (Mul_F x y z, Mul_B x y z) => Mul_ (x:.B1) y z -- | Assert that @(2x+1) * y == z@ where @x > 0@. class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_F x y z | x y -> z instance NatNE0_ x => Mul_F x B0 B0 instance NatNE0_ x => Mul_F x B1 (x:.B1) -- (2x+1) * 2y instance (Mul_F x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z) => Mul_F x (y:.B0) (z:.B0) -- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y > 0 instance (Mul_F x y z', Add x z' z, NatNE0_ x, NatNE0_ y, NatNE0_ z) => Mul_F x (y:.B1) (z:.B1) -- | Assert that @(2x+1) * y == z@ where @x > 0@. The functional -- dependencies go the other way though. class (NatNE0_ x, Nat_ y, Nat_ z) => Mul_B x y z | z x -> y instance NatNE0_ x => Mul_B x B0 B0 -- instance NatNE0_ x => Mul_B x y B1 -- cannot happen -- (2x+1) * 2y instance (Mul_B x y z, NatNE0_ x, NatNE0_ y, NatNE0_ z) => Mul_B x (y:.B0) (z:.B0) -- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y >= 0 instance (Snoc y B1 yt, Mul_B x y z', Add x z' z, NatNE0_ x, NatNE0_ z) => Mul_B x yt (z:.B1) -- | The multiplication relation with full dependencies. Modes: -- -- > Mul x y (x*y) -- > Mul x (z/x) z -- when it's defined. -- > Mul (z/y) y z -- when it's defined. -- class (Mul_ x y z, Mul_ y x z) => Mul x y z | x y -> z, x z -> y, y z -> x instance (Mul_ x y z, Mul_ y x z) => Mul x y z mul :: Mul x y z => Proxy x -> Proxy y -> Proxy z mul _ _ = Proxy {-# INLINE mul #-} -- | N.B., this will be ill-typed if @z@ is not a multiple of @x@. div :: Mul x y z => Proxy z -> Proxy x -> Proxy y div _ _ = Proxy {-# INLINE div #-} -- tm1 = mul nat2 nat8 -- tm2 = reflect $ mul nat8 nat2 -- tm3 = reflect $ mul (succ nat2) nat2 -- tm4 = reflect $ mul nat2 (succ nat2) -- tm5 = reflect $ mul (succ nat4) (succ nat2) -- tm6 = reflect $ mul (succ nat2) (succ nat4) -- tm7 = reflect $ div (mul (succ nat8) nat2) (succ nat2) -- 18/3 ---------------------------------------------------------------- -- TODO: should we offer @(floor . logBase 2)@ and @(ceiling . logBase 2)@ ? -- TODO: general exponentiation/logarithm -- | Power-of-two exponentiation\/logarithm relation. Modes: -- -- > Exp2 x (2^x) -- > Exp2 (logBase 2 y) y -- when it's defined. -- class (Nat_ x, NatNE0_ y) => Exp2 x y | x -> y, y -> x instance Exp2 B0 B1 instance Exp2 B1 (B1:.B0) instance (Succ x1 (x:.d), Exp2 x1 (y:.B0)) => Exp2 (x:.d) (y:.B0:.B0) exp2 :: Exp2 x y => Proxy x -> Proxy y exp2 _ = Proxy {-# INLINE exp2 #-} -- | N.B., this will be ill-typed if @y@ is not a power of 2. log2 :: Exp2 x y => Proxy y -> Proxy x log2 _ = Proxy {-# INLINE log2 #-} -- te1 = exp2 (succ (succ nat8)) -- te1' = reflect $ exp2 (succ (succ nat8)) -- te2 = reflect $ log2 nat8 ---------------------------------------------------------------- -- Do we need the full dependency? If we know x and we know z, -- we can't tell what y exactly (except being the multiple of z) -- | Get the gcd by Euclid's algorithm. Modes: -- -- > GCD x y (gcd x y) -- class (Nat_ x, Nat_ y, Nat_ z) => GCD x y z | x y -> z instance Nat_ y => GCD B0 y y instance Nat_ y => GCD B1 y B1 instance (Compare (x:.dx) y r, GCD_ r (x:.dx) y z) => GCD (x:.dx) y z class (NatNE0_ x, Nat_ y, Nat_ z) => GCD_ r x y z | r x y -> z instance NatNE0_ x => GCD_ EQ_ x x x instance (GCD y x z, NatNE0_ x) => GCD_ GT_ x y z instance (Add x y1 y, GCD y1 x z, NatNE0_ x) => GCD_ LT_ x y z gcd :: GCD x y z => Proxy x -> Proxy y -> Proxy z gcd _ _ = Proxy {-# INLINE gcd #-} -- tg1 = reflect $ gcd nat8 nat8 -- tg2 = reflect $ gcd nat8 (pred nat8) -- tg3 = reflect $ gcd nat8 (pred (pred nat8)) -- tg4 = reflect $ gcd (pred (pred nat8)) nat8 -- tg5 = reflect $ gcd nat4 nat8 -- tg6 = reflect $ gcd (pred nat4) (succ nat8) -- tg7 = reflect $ gcd (succ nat8) (pred nat4) -} ---------------------------------------------------------------- ----------------------------------------------------------- fin.