{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE CPP #-}
-- | Utilities for working with 'KnownSymbol' constraints.
--
-- This module is only available on GHC 8.0 or later.
module Data.Constraint.Symbol
  ( type AppendSymbol
  , type (++)
  , type Take
  , type Drop
  , type Length
  , appendSymbol
  , appendUnit1
  , appendUnit2
  , appendAssociates
  , takeSymbol
  , dropSymbol
  , takeAppendDrop
  , lengthSymbol
  , takeLength
  , take0
  , takeEmpty
  , dropLength
  , drop0
  , dropEmpty
  , lengthTake
  , lengthDrop
  , dropDrop
  , takeTake
  ) where

import Data.Constraint
import Data.Constraint.Nat
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce

#if !(MIN_VERSION_base(4,10,0))
type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol
#endif

-- | An infix synonym for 'AppendSymbol'.
type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n
infixr 5 ++

type family Take :: Nat -> Symbol -> Symbol where
type family Drop :: Nat -> Symbol -> Symbol where
type family Length :: Symbol -> Nat where

-- implementation details

newtype Magic n = Magic (KnownSymbol n => Dict (KnownSymbol n))

magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
magicNSS :: (Int -> String -> String)
-> (KnownNat n, KnownSymbol m) :- KnownSymbol o
magicNSS Int -> String -> String
f = ((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
-> (KnownNat n, KnownSymbol m) :- KnownSymbol o
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
 -> (KnownNat n, KnownSymbol m) :- KnownSymbol o)
-> ((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
-> (KnownNat n, KnownSymbol m) :- KnownSymbol o
forall a b. (a -> b) -> a -> b
$ Magic Any -> String -> Dict (KnownSymbol o)
forall a b. a -> b
unsafeCoerce ((KnownSymbol Any => Dict (KnownSymbol Any)) -> Magic Any
forall (n :: Symbol).
(KnownSymbol n => Dict (KnownSymbol n)) -> Magic n
Magic KnownSymbol Any => Dict (KnownSymbol Any)
forall (a :: Constraint). a => Dict a
Dict) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n)) Int -> String -> String
`f` Proxy m -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))

magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
magicSSS :: (String -> String -> String)
-> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
magicSSS String -> String -> String
f = ((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
-> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
 -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o)
-> ((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
-> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
forall a b. (a -> b) -> a -> b
$ Magic Any -> String -> Dict (KnownSymbol o)
forall a b. a -> b
unsafeCoerce ((KnownSymbol Any => Dict (KnownSymbol Any)) -> Magic Any
forall (n :: Symbol).
(KnownSymbol n => Dict (KnownSymbol n)) -> Magic n
Magic KnownSymbol Any => Dict (KnownSymbol Any)
forall (a :: Constraint). a => Dict a
Dict) (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n) String -> String -> String
`f` Proxy m -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))

magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n
magicSN :: (String -> Int) -> KnownSymbol a :- KnownNat n
magicSN String -> Int
f = (KnownSymbol a => Dict (KnownNat n)) -> KnownSymbol a :- KnownNat n
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownSymbol a => Dict (KnownNat n))
 -> KnownSymbol a :- KnownNat n)
-> (KnownSymbol a => Dict (KnownNat n))
-> KnownSymbol a :- KnownNat n
forall a b. (a -> b) -> a -> b
$ Magic Any -> Integer -> Dict (KnownNat n)
forall a b. a -> b
unsafeCoerce ((KnownSymbol Any => Dict (KnownSymbol Any)) -> Magic Any
forall (n :: Symbol).
(KnownSymbol n => Dict (KnownSymbol n)) -> Magic n
Magic KnownSymbol Any => Dict (KnownSymbol Any)
forall (a :: Constraint). a => Dict a
Dict) (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (String -> Int
f (Proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a))))

axiom :: Dict c
axiom :: Dict c
axiom = Dict (() :: Constraint) -> Dict c
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint)
forall (a :: Constraint). a => Dict a
Dict :: Dict ())

-- axioms and operations

appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
appendSymbol = (String -> String -> String)
-> (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
forall (n :: Symbol) (m :: Symbol) (o :: Symbol).
(String -> String -> String)
-> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
magicSSS String -> String -> String
forall a. [a] -> [a] -> [a]
(++)

appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)
appendUnit1 :: Dict (AppendSymbol "" a ~ a)
appendUnit1 =
#if MIN_VERSION_base(4,10,0)
  Dict (AppendSymbol "" a ~ a)
forall (a :: Constraint). a => Dict a
Dict
#else
  axiom
#endif

appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)
appendUnit2 :: Dict (AppendSymbol a "" ~ a)
appendUnit2 =
#if MIN_VERSION_base(4,10,0)
  Dict (AppendSymbol a "" ~ a)
forall (a :: Constraint). a => Dict a
Dict
#else
  axiom
#endif

appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
appendAssociates :: Dict
  (AppendSymbol (AppendSymbol a b) c
   ~ AppendSymbol a (AppendSymbol b c))
appendAssociates = Dict
  (AppendSymbol (AppendSymbol a b) c
   ~ AppendSymbol a (AppendSymbol b c))
forall (c :: Constraint). Dict c
axiom

takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
takeSymbol :: (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
takeSymbol = (Int -> String -> String)
-> (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
forall (n :: Nat) (m :: Symbol) (o :: Symbol).
(Int -> String -> String)
-> (KnownNat n, KnownSymbol m) :- KnownSymbol o
magicNSS Int -> String -> String
forall a. Int -> [a] -> [a]
take

dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
dropSymbol :: (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
dropSymbol = (Int -> String -> String)
-> (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
forall (n :: Nat) (m :: Symbol) (o :: Symbol).
(Int -> String -> String)
-> (KnownNat n, KnownSymbol m) :- KnownSymbol o
magicNSS Int -> String -> String
forall a. Int -> [a] -> [a]
drop

takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
takeAppendDrop :: Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
takeAppendDrop = Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
forall (c :: Constraint). Dict c
axiom

lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)
lengthSymbol :: KnownSymbol a :- KnownNat (Length a)
lengthSymbol = (String -> Int) -> KnownSymbol a :- KnownNat (Length a)
forall (a :: Symbol) (n :: Nat).
(String -> Int) -> KnownSymbol a :- KnownNat n
magicSN String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)
takeLength :: (Length a <= n) :- (Take n a ~ a)
takeLength = ((Length a <= n) => Dict (Take n a ~ a))
-> (Length a <= n) :- (Take n a ~ a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Length a <= n) => Dict (Take n a ~ a)
forall (c :: Constraint). Dict c
axiom

take0 :: forall a. Dict (Take 0 a ~ "")
take0 :: Dict (Take 0 a ~ "")
take0 = Dict (Take 0 a ~ "")
forall (c :: Constraint). Dict c
axiom

takeEmpty :: forall n. Dict (Take n "" ~ "")
takeEmpty :: Dict (Take n "" ~ "")
takeEmpty = Dict (Take n "" ~ "")
forall (c :: Constraint). Dict c
axiom

dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")
dropLength :: (Length a <= n) :- (Drop n a ~ "")
dropLength = ((Length a <= n) => Dict (Drop n a ~ ""))
-> (Length a <= n) :- (Drop n a ~ "")
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Length a <= n) => Dict (Drop n a ~ "")
forall (c :: Constraint). Dict c
axiom

drop0 :: forall a. Dict (Drop 0 a ~ a)
drop0 :: Dict (Drop 0 a ~ a)
drop0 = Dict (Drop 0 a ~ a)
forall (c :: Constraint). Dict c
axiom

dropEmpty :: forall n. Dict (Drop n "" ~ "")
dropEmpty :: Dict (Drop n "" ~ "")
dropEmpty = Dict (Drop n "" ~ "")
forall (c :: Constraint). Dict c
axiom

lengthTake :: forall n a. Dict (Length (Take n a) <= n)
lengthTake :: Dict (Length (Take n a) <= n)
lengthTake = Dict (Length (Take n a) <= n)
forall (c :: Constraint). Dict c
axiom

lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))
lengthDrop :: Dict (Length a <= (Length (Drop n a) + n))
lengthDrop = Dict (Length a <= (Length (Drop n a) + n))
forall (c :: Constraint). Dict c
axiom

dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)
dropDrop :: Dict (Drop n (Drop m a) ~ Drop (n + m) a)
dropDrop = Dict (Drop n (Drop m a) ~ Drop (n + m) a)
forall (c :: Constraint). Dict c
axiom

takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)
takeTake :: Dict (Take n (Take m a) ~ Take (Min n m) a)
takeTake = Dict (Take n (Take m a) ~ Take (Min n m) a)
forall (c :: Constraint). Dict c
axiom