string-typelits (empty) → 0.1.0.0

raw patch · 4 files changed

+262/−0 lines, 4 filesdep +basedep +template-haskelldep +type-combinatorssetup-changed

Dependencies added: base, template-haskell, type-combinators, type-combinators-quote

Files

LICENSE +30/−0
Setup.hs +2/−0
src/Data/Type/String.hs +199/−0
string-typelits.cabal +31/−0

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ src/Data/Type/String.hs view

@@ -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+

+ string-typelits.cabal view

@@ -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+