string-typelits-0.1.0.0: src/Data/Type/String.hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}
module Data.Type.String
( TChar
, TString
, Chr
, Str
, qChr
, qStr
) where
import Type.Class.Higher
import Type.Class.Witness
import Type.Family.Bool
import Type.Family.List
import Type.Family.Nat
import Data.Type.Boolean
import Data.Type.Product
import Data.Type.Quote
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import qualified Data.Char as Char
data Chr = Char Bool Bool Bool Bool Bool Bool Bool Bool
type instance ('Char a0 a1 a2 a3 a4 a5 a6 a7)
== ('Char b0 b1 b2 b3 b4 b5 b6 b7)
= a0 == b0 && a1 == b1 && a2 == b2 && a3 == b3
&& a4 == b4 && a5 == b5 && a6 == b6 && a7 == b7
data TChar :: Chr -> * where
TChar :: !(Prod Boolean '[b0,b1,b2,b3,b4,b5,b6,b7])
-> TChar ('Char b0 b1 b2 b3 b4 b5 b6 b7)
toChar :: TChar c -> Char
toChar (TChar ds) = Char.chr $ fromBin $ toList toBool ds
instance Show (TChar c) where
showsPrec d c = showParen (d > 10)
$ showString "TChar "
. shows (toChar c)
instance Show1 TChar
instance TestEquality TChar where
testEquality (TChar as) (TChar bs) = as =?= bs //? qed
instance BoolEquality TChar where
boolEquality (TChar as) (TChar bs) = as .== bs
-- Chr QQ {{{
qChr :: QuasiQuoter
qChr = QuasiQuoter
{ quoteExp = quoteTCharE qq
, quotePat = quoteTCharP qq
, quoteType = quoteCharT qq
, quoteDec = stub qq "Dec"
}
where
qq = "qChr"
quoteTCharE :: String -> String -> Q Exp
quoteTCharE qq = \case
[c] -> case toBin $ Char.ord c of
Just bs | length bs == 8 ->
[| TChar $(foldr (\b as -> [| $(booleanE b) :< $as |]) [|Ø|] bs) |]
r -> fail $ qq ++ ": bad binary conversion: " ++ show r
_ -> fail $ qq ++ ": expected Char"
quoteTCharP :: String -> String -> Q Pat
quoteTCharP qq = \case
[c] -> case toBin $ Char.ord c of
Just bs | length bs == 8 ->
[p| TChar $(foldr (\b as -> [p| $(booleanP b) :< $as |]) [p|Ø|] bs) |]
r -> fail $ qq ++ ": bad binary conversion: " ++ show r
_ -> fail $ qq ++ ": expected Char"
quoteCharT :: String -> String -> Q Type
quoteCharT qq = \case
[c] -> case toBin $ Char.ord c of
Just bs | length bs == 8 ->
[t| 'Char $(ds !! 0) $(ds !! 1) $(ds !! 2) $(ds !! 3)
$(ds !! 4) $(ds !! 5) $(ds !! 6) $(ds !! 7)
|]
where
ds = map booleanT bs
r -> fail $ qq ++ ": bad binary conversion: " ++ show r
_ -> fail $ qq ++ ": expected Char"
toBin :: Int -> Maybe [Bool]
toBin n
| n < 0 || n >= 256 = Nothing
| otherwise = Just $ pad 8 False $ go n []
where
go x ds
| x == 0 = ds
| otherwise = go y $ toBinDigit d : ds
where
(y,d) = x `divMod` 2
fromBin :: [Bool] -> Int
fromBin = foldl (\acc d -> 2 * acc + fromBinDigit d) 0
pad :: Int -> a -> [a] -> [a]
pad n a as = replicate (n - length as) a ++ as
toBinDigit :: Int -> Bool
toBinDigit = (>= 1)
fromBinDigit :: Bool -> Int
fromBinDigit b = if b then 1 else 0
booleanE :: Bool -> Q Exp
booleanE b = if b then [|True_|] else [|False_|]
booleanP :: Bool -> Q Pat
booleanP b = if b then [p|True_|] else [p|False_|]
booleanT :: Bool -> Q Type
booleanT b = if b then [t|True|] else [t|False|]
-- }}}
newtype Str = String [Chr]
type instance ('String as) == ('String bs) = as == bs
data TString :: Str -> * where
TString :: !(Prod TChar cs)
-> TString ('String cs)
instance Show (TString s) where
showsPrec = showsPrec1
instance Show1 TString where
showsPrec1 d s = showParen (d > 10)
$ showString "TString "
. shows (toString s)
instance TestEquality TString where
testEquality (TString a) (TString b) = a =?= b //? qed
instance BoolEquality TString where
boolEquality (TString a) (TString b) = a .== b
toString :: TString s -> String
toString (TString s) = toList toChar s
-- Str QQ {{{
qStr :: QuasiQuoter
qStr = QuasiQuoter
{ quoteExp = quoteTStringE qq
, quotePat = quoteTStringP qq
, quoteType = quoteStringT qq
, quoteDec = stub qq "Dec"
}
where
qq = "qStr"
quoteTStringE :: String -> String -> Q Exp
quoteTStringE qq s = [| TString $t |]
where
t = foldr (\a b -> [| $(quoteTCharE qq [a]) :< $b |]) [|Ø|] s
quoteTStringP :: String -> String -> Q Pat
quoteTStringP qq s = [p| TString $t |]
where
t = foldr (\a b -> [p| $(quoteTCharP qq [a]) :< $b |]) [p|Ø|] s
quoteStringT :: String -> String -> Q Type
quoteStringT qq s = [t| 'String $t |]
where
t = foldr (\a b -> [t| $(quoteCharT qq [a]) :< $b |]) [t|Ø|] s
-- }}}
displayQ :: Show a => Q a -> IO ()
displayQ m = do
a <- runQ m
print a