{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE PolyKinds, UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
module Data.Type.Set.Internal (
Set(Nil, (:~)),
Numbered, numbered,
Singleton, Insert, Merge, Map,
(:-), (:+:) ) where
import GHC.TypeLits (Nat, type (<=?))
import Language.Haskell.TH (
TypeQ, DecsQ, runIO,
instanceD, cxt, tySynInstD, tySynEqn, conT, appT, litT, numTyLit )
import Data.Kind (Type)
import System.Random (randomRIO)
infixr 5 :~
data Set a = Nil | a :~ Set a
type Singleton t = t ':~ 'Nil
infixr 5 :-
type t :- ts = t `Insert` ts
type family Insert (t :: Type) (ts :: Set Type) :: Set Type where
Insert t 'Nil = t ':~ 'Nil
Insert t (t ':~ ts) = t ':~ ts
Insert t (t' ':~ ts) = BOOL
(InsertElse t t' ts)
(InsertThen t t' ts)
$ (Number t <=? Number t')
data InsertElse t t' ts :: () >-> k
type instance InsertElse t t' ts $ '() = t' ':~ t :- ts
data InsertThen t t' ts :: () >-> k
type instance InsertThen t t' ts $ '() = t ':~ t' ':~ ts
infixr 5 :+:
type ts :+: ts' = ts `Merge` ts'
type family Merge (ts :: Set Type) (ts' :: Set Type) :: Set Type where
Merge ts 'Nil = ts
Merge 'Nil ts' = ts'
Merge (t ':~ ts) (t ':~ ts') = t ':~ Merge ts ts'
Merge (t ':~ ts) (t' ':~ ts') = BOOL
(MergeElse t ts t' ts')
(MergeThen t ts t' ts')
$ (Number t <=? Number t')
data MergeElse t ts t' ts' :: () >-> k
type instance MergeElse t ts t' ts' $ '() = t' ':~ (t ':~ ts) :+: ts'
data MergeThen t ts t' ts' :: () >-> k
type instance MergeThen t ts t' ts' $ '() = t ':~ ts :+: (t' ':~ ts')
type family Map (f :: Type -> Type) (ts :: Set Type) :: Set Type where
_ `Map` 'Nil = 'Nil
f `Map` (t ':~ ts) = f t ':~ (f `Map` ts)
class Numbered a where type Number (a :: Type) = (r :: Nat) | r -> a
numbered :: TypeQ -> DecsQ
numbered :: TypeQ -> DecsQ
numbered TypeQ
t = ((forall a. a -> [a] -> [a]
: []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
Quote m =>
m Cxt -> m Type -> [m Dec] -> m Dec
instanceD (forall (m :: * -> *). Quote m => [m Type] -> m Cxt
cxt []) (forall (m :: * -> *). Quote m => Name -> m Type
conT ''Numbered forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` TypeQ
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
: [])
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => m TySynEqn -> m Dec
tySynInstD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn forall a. Maybe a
Nothing (forall (m :: * -> *). Quote m => Name -> m Type
conT ''Number forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` TypeQ
t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Quote m => m TyLit -> m Type
litT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Quote m => Integer -> m TyLit
numTyLit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. IO a -> Q a
runIO (forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0, Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
s forall a. Num a => a -> a -> a
- Integer
1))
where s :: Int
s = Int
64 :: Int
type a >-> b = (b -> Type) -> a -> Type
type family ($) (f :: a >-> b) (x :: a) :: b
data BOOL :: (() >-> k) -> (() >-> k) -> (Bool >-> k)
type instance (BOOL f _) $ 'False = f $ '()
type instance (BOOL _ t) $ 'True = t $ '()