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