diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2016, Kyle Carter + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Kyle Carter nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Data/Type/String.hs b/src/Data/Type/String.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/String.hs @@ -0,0 +1,199 @@ +{-# 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 + diff --git a/string-typelits.cabal b/string-typelits.cabal new file mode 100644 --- /dev/null +++ b/string-typelits.cabal @@ -0,0 +1,31 @@ +-- Initial string-typelits.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: string-typelits +version: 0.1.0.0 +category: Data +synopsis: Type-level Chars and Strings, with decidable equality. +license: BSD3 +license-file: LICENSE +author: Kyle Carter +maintainer: kylcarte@indiana.edu +copyright: (c) 2016 Kyle Carter, all rights reserved +build-type: Simple +homepage: https://github.com/kylcarte/string-typelits +cabal-version: >=1.10 + +Source-Repository head + type: git + location: git://github.com/kylcarte/string-typelits.git + +library + exposed-modules: + Data.Type.String + build-depends: + base >=4.8 && <4.9, + template-haskell, + type-combinators >=0.2.2.1, + type-combinators-quote + hs-source-dirs: src + default-language: Haskell2010 +