1{-# LANGUAGE ScopedTypeVariables #-} 2{-# LANGUAGE AllowAmbiguousTypes #-} 3{-# LANGUAGE TypeApplications #-} 4{-# LANGUAGE ConstraintKinds #-} 5{-# LANGUAGE TypeOperators #-} 6{-# LANGUAGE TypeFamilies #-} 7{-# LANGUAGE RankNTypes #-} 8{-# LANGUAGE DataKinds #-} 9{-# LANGUAGE PolyKinds #-} 10{-# LANGUAGE CPP #-} 11-- | Utilities for working with 'KnownSymbol' constraints. 12-- 13-- This module is only available on GHC 8.0 or later. 14module Data.Constraint.Symbol 15 ( type AppendSymbol 16 , type (++) 17 , type Take 18 , type Drop 19 , type Length 20 , appendSymbol 21 , appendUnit1 22 , appendUnit2 23 , appendAssociates 24 , takeSymbol 25 , dropSymbol 26 , takeAppendDrop 27 , lengthSymbol 28 , takeLength 29 , take0 30 , takeEmpty 31 , dropLength 32 , drop0 33 , dropEmpty 34 , lengthTake 35 , lengthDrop 36 , dropDrop 37 , takeTake 38 ) where 39 40import Data.Constraint 41import Data.Constraint.Nat 42import Data.Proxy 43import GHC.TypeLits 44import Unsafe.Coerce 45 46#if !(MIN_VERSION_base(4,10,0)) 47type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol 48#endif 49 50-- | An infix synonym for 'AppendSymbol'. 51type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n 52infixr 5 ++ 53 54type family Take :: Nat -> Symbol -> Symbol where 55type family Drop :: Nat -> Symbol -> Symbol where 56type family Length :: Symbol -> Nat where 57 58-- implementation details 59 60newtype Magic n = Magic (KnownSymbol n => Dict (KnownSymbol n)) 61 62magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o 63magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m)) 64 65magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o 66magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m)) 67 68magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n 69magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy :: Proxy a)))) 70 71axiom :: forall a b. Dict (a ~ b) 72axiom = unsafeCoerce (Dict :: Dict (a ~ a)) 73 74-- axioms and operations 75 76appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b) 77appendSymbol = magicSSS (++) 78 79appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a) 80appendUnit1 = 81#if MIN_VERSION_base(4,10,0) 82 Dict 83#else 84 axiom 85#endif 86 87appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a) 88appendUnit2 = 89#if MIN_VERSION_base(4,10,0) 90 Dict 91#else 92 axiom 93#endif 94 95appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c)) 96appendAssociates = axiom 97 98takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a) 99takeSymbol = magicNSS take 100 101dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a) 102dropSymbol = magicNSS drop 103 104takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a) 105takeAppendDrop = axiom 106 107lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a) 108lengthSymbol = magicSN length 109 110takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a) 111takeLength = Sub axiom 112 113take0 :: forall a. Dict (Take 0 a ~ "") 114take0 = axiom 115 116takeEmpty :: forall n. Dict (Take n "" ~ "") 117takeEmpty = axiom 118 119dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "") 120dropLength = Sub axiom 121 122drop0 :: forall a. Dict (Drop 0 a ~ a) 123drop0 = axiom 124 125dropEmpty :: forall n. Dict (Drop n "" ~ "") 126dropEmpty = axiom 127 128lengthTake :: forall n a. Dict (Length (Take n a) <= n) 129lengthTake = axiom 130 131lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n)) 132lengthDrop = axiom 133 134dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a) 135dropDrop = axiom 136 137takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a) 138takeTake = axiom 139