Commits

Anonymous committed e35c384

initial commit

Comments (0)

Files changed (8)

+syntax: glob
+*.swp
+*.hi
+html
+MyGen.hs
+QC.hs
+Tramp.hs
+a
+a.hs
+a.o
+t.m
+t.o
+*.o

Data/Fields/BasicTypes.hs

+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Data.Fields.BasicTypes where
+import Data.Word
+import Data.Fields.TLNat
+data BasicType = W8 | W16 | W32 | W64 
+
+type family   ReprType (t :: BasicType) :: *
+type instance ReprType W8   = Word8
+type instance ReprType W16  = Word16
+type instance ReprType W32  = Word32
+type instance ReprType W64  = Word64
+
+type family BitWidth (t :: BasicType) :: Nat
+type instance BitWidth W8   = N8
+type instance BitWidth W16  = N16
+type instance BitWidth W32  = N32
+type instance BitWidth W64  = N64
+

Data/Fields/BitField.hs

+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE TypeFamilies           #-}
+
+module Data.Fields.BitField (
+      Repr
+    , mkRepr
+    , mkRepr'
+    , extractRepr
+    , shiftR
+    , shiftL
+    , expand
+    , contract
+    , shiftLP
+    , bitNegate
+
+) where
+import Data.Fields.TLNat
+import Data.Fields.BasicTypes
+import Data.Word
+import qualified Data.Bits as B
+
+
+
+newtype Repr (base :: BasicType) (width :: Nat) = Repr {getRepr :: ReprType base} 
+
+mkRepr :: ReprType t -> Repr t (BitWidth t)
+mkRepr = Repr
+
+mkRepr' :: (LE k (BitWidth t)) => NatProxy k -> ReprType t -> Repr t k
+mkRepr' _ = Repr
+
+shiftR :: B.Bits (ReprType b) => Repr b (S a) -> Repr b a
+shiftR = Repr . (flip B.shiftR 1) . getRepr
+
+shiftL :: (B.Bits (ReprType b), LE (S a) (BitWidth b)) => Repr b a -> Repr b (S a)
+shiftL = Repr . (flip B.shiftL 1) . getRepr
+
+shiftLP :: (B.Bits (ReprType b), LE (Add k a) (BitWidth b), ToInt k) => NatProxy k -> Repr b a -> Repr b (Add k a)
+shiftLP p = Repr . (flip B.shiftL (toIntL p)) . getRepr
+
+shiftRP :: (B.Bits (ReprType b), Add c k ~ a, ToInt k) => NatProxy k -> Repr b a -> Repr b c
+shiftRP p = Repr . (flip B.shiftR (toIntL p)) . getRepr
+
+expand :: (Integral (ReprType b), Num (ReprType b1), ToInt a, (B.Bits (ReprType b)), LE (BitWidth b) (BitWidth b1)) => Repr b a -> Repr b1 a
+expand = Repr . fromInteger . toInteger . extractRepr
+
+contract :: (LE l2 l1) => Repr b l1 -> Repr b l2
+contract = Repr . getRepr
+
+bitAnd :: B.Bits (ReprType b) => Repr b a -> Repr b a -> Repr b a
+bitAnd (Repr a) (Repr b) = Repr (a B..&. b)
+
+bitNegate :: B.Bits (ReprType b) => Repr b a -> Repr b a
+bitNegate = Repr . B.complement . getRepr
+
+extractRepr :: (ToInt k , Num (ReprType b), B.Bits (ReprType b)) => Repr b k -> ReprType b
+extractRepr  r = createMask (toIntL (widthProxy r)) B..&. ( getRepr r)
+
+widthProxy :: Repr b k -> NatProxy k
+widthProxy = undefined
+
+createMask :: (B.Bits b, Num b) => Int -> b
+createMask = createMask' 0 where
+    createMask' b 0 = b
+    createMask' b n = createMask' (B.shiftL b 1 B..|. 1) (n-1)
+
+

Data/Fields/BitStruct.hs

+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Data.Fields.BitStruct (
+      ReprStruct
+    , mkStruct
+    , flatten
+    , extractField
+    , storeField
+    , reinterpret
+) where
+
+import Data.Fields.BasicTypes
+import Data.Fields.TLNat
+import Data.Fields.BitField
+import qualified Data.Bits as B
+
+newtype ReprStruct (base :: BasicType) (fields :: [Nat]) = ReprStruct {getStruct :: ReprType base}
+
+type family WidthL (t :: [Nat]) :: Nat
+type instance WidthL ('[]) = Z
+type instance WidthL (a ': b) = Add a (WidthL b) 
+
+totalWidth :: a l -> NatProxy (WidthL l)
+totalWidth = undefined
+
+class ListPosition (t :: Nat) (l :: [Nat]) where
+    type OffsetOf t l :: Nat
+    proxyOffset :: NatProxy t -> a l ->  NatProxy (OffsetOf t l)
+    proxyOffset = undefined
+    proxyWidth  :: NatProxy t -> a l ->  NatProxy (FieldWidth t l)
+    proxyWidth = undefined
+
+instance ListPosition Z (x ': xs) where
+    type OffsetOf Z (x ': xs) = WidthL xs
+    
+
+instance ListPosition t xs => ListPosition (S t) (x ': xs) where
+    type OffsetOf (S t) (x ': xs) = OffsetOf t xs
+
+type family FieldWidth (n :: Nat) (l :: [Nat]) :: Nat
+type instance FieldWidth Z (x ': xs) = x
+type instance FieldWidth (S a) (x ': xs) = FieldWidth a xs
+
+mkStruct :: (LE (WidthL l) (BitWidth t)) => ReprType t -> ReprStruct t l
+mkStruct = ReprStruct
+
+
+flatten :: (LE (WidthL fields) (BitWidth b)) => ReprStruct b fields -> Repr b (WidthL fields)
+flatten s = mkRepr' (totalWidth s) . getStruct $ s
+
+extractField :: (LE (WidthL fields) (BitWidth b), LE (FieldWidth k fields) (BitWidth b), B.Bits (ReprType b), ListPosition k fields,  ToInt (WidthL fields), ToInt (OffsetOf k fields)) => NatProxy k -> ReprStruct b fields  -> Repr b (FieldWidth k fields)
+extractField p b =  mkRepr' (proxyWidth p b) .  flip B.shiftR (toIntL  (proxyOffset p b))  .  extractRepr . flatten $ b
+
+storeField :: (B.Bits (ReprType b), ListPosition k fields, ToInt(FieldWidth k fields), ToInt (OffsetOf k fields)) => NatProxy k -> ReprStruct b fields  -> Repr b (FieldWidth k fields) ->
+    ReprStruct b fields
+storeField p b f = ReprStruct (getStruct b B..|. (B.shiftL (extractRepr f) (toIntL (proxyOffset p b))))
+
+reinterpret :: (LE (WidthL f2) (WidthL f1)) => ReprStruct b f1 -> ReprStruct b f2
+reinterpret = ReprStruct . getStruct 

Data/Fields/TH.hs

+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds       #-}
+module Data.Fields.TH where
+import Language.Haskell.TH
+import Data.Fields.TLNat (NatProxy, Nat(..))
+
+nat ::  (Num a, Ord a) => a -> Q Type
+nat n | n < 0 = fail "Invalid natural"
+      | n == 0  = return $ ConT 'Z
+      | otherwise = fmap (AppT (ConT 'S)) (nat (n-1))
+
+natProxy :: (Num a, Ord a) => a -> Q Exp
+natProxy  n = do
+    n <- nat n
+    return $ (SigE (VarE 'undefined)) (AppT (ConT ''NatProxy) n)

Data/Fields/TLNat.hs

+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+
+module Data.Fields.TLNat where
+data Nat = Z | S Nat
+
+type family Add (a :: Nat) (b :: Nat) :: Nat
+type instance Add Z a = a
+type instance Add (S a) b = S (Add a b)
+
+type family Mul (a :: Nat) (b :: Nat) :: Nat
+type instance Mul Z a = Z
+type instance Mul (S a) b = Add b (Mul a b)
+
+type family Pow (a :: Nat) (b :: Nat) :: Nat
+type instance Pow (a :: Nat) Z = S Z
+type instance Pow a (S b) = Mul a (Pow a b)
+
+type N1 = S Z
+type N2 = Add N1 N1
+type N3 = Add N2 N1
+type N4 = Mul N2 N2
+type N5 = Add N4 N1
+type N6 = Add N5 N1
+type N7 = Add N6 N1
+type N8 = Mul N4 N2
+type N9 = Add N8 N1
+type N16 = Pow N4 N2
+type N32 = Pow N2 N5
+type N64 = Pow N2 N6
+
+class Less (a :: Nat) (b :: Nat) where
+
+    
+instance Less Z (S a) where
+instance Less a b => Less (S a) (S b) where
+
+class LE (a :: Nat) (b :: Nat) 
+instance LE Z a
+instance (LE a b) => LE (S a) (S b)
+
+data NatProxy (n :: Nat) where
+
+class ToInt (a :: Nat) where
+    toIntL :: NatProxy a -> Int
+
+instance ToInt Z where
+    toIntL _ = 0
+
+instance (ToInt t) => ToInt (S t) where
+    toIntL _ = 1 + toIntL (undefined :: NatProxy t)
+
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TemplateHaskell        #-}
+
+module Fields  where
+import Data.Word
+import qualified Data.Bits as B
+import Data.Fields.TLNat
+import Data.Fields.BitField
+import Data.Fields.BitStruct
+import Data.Fields.BasicTypes
+import Data.Fields.TH
+
+
+tst :: Repr W8 N8
+tst = mkRepr 3
+
+tst1 ::  Repr 'W8 $(nat 7)
+tst1 = shiftR tst
+
+tst2 ::  Repr 'W8 N8
+tst2 = shiftL tst1
+
+-- fail
+-- tst3 = shiftL tst
+
+tst4 :: Repr W16 N8
+tst4 = expand tst
+
+tst5 ::  Repr 'W16 (S N8)
+tst5 = shiftL tst4
+
+tst6 = shiftLP $(natProxy 2) tst4
+
+mask :: ReprStruct 'W16 '[N8 , N2]
+mask = mkStruct (0xAAAA)
+
+f1 ::  Repr 'W16 $(nat 8)
+f1 = extractField $(natProxy 0) mask
+
+f2 ::  Repr 'W16 (S (S 'Z))
+f2 = extractField $(natProxy 1) mask
+
+f3 = bitNegate f1
+mask1 = storeField $(natProxy 0) mask f3
+{- 
+ - Представления битовых последовательностей произвольной длины (статически заданной)
+ - Статический выбор минимального представления
+ - expand/contract/сдвиги
+ - Представления битовых структур
+ - Операции извлечения и сохранения данных
+ - Разложить по модулям
+ - Экспорты из модулей
+ - Пример набора полей
+ - Пример интерпретации полей
+ - тесты извлечения и вставки полей
+ - Посмотреть констрейнты - очень длинные
+ -
+ - Операции передачи данных
+ - Конверсия в типы
+ - Template Haskell для конструирования типов
+ -}
+
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+module Selection where
+import Control.Monad(mplus, liftM)
+data a :+: b = a :+: b
+infixl 6 :+:
+class Selector sel  where
+    type Interpretation sel  
+    type Raw sel
+    reinterpret :: sel -> Raw sel -> Maybe (Interpretation sel)
+
+
+{- getVal :: (Selector sel) => sel -> Raw sel -> Maybe (Interpretation sel)
+getVal s raw    | check s raw = Just (reinterpret s  raw)
+                | otherwise   = Nothing
+-}
+
+instance (Selector s1, Selector s2, Raw s1 ~ Raw s2) => Selector (s1 :+: s2) where
+    type Interpretation (s1 :+: s2) = Either (Interpretation s1) (Interpretation s2)
+    type Raw (s1 :+: s2) = Raw s1
+    reinterpret (s1 :+: s2) raw = fmap Left (reinterpret s1 raw) `mplus` fmap Right (reinterpret s2 raw)
+
+
+class (Monad m)=>Stream raw m where
+    next :: m raw 
+
+selectNext :: (Stream raw m, Selector sel, Raw sel ~ raw) => sel -> m (Maybe (Interpretation sel) )
+selectNext s = liftM (reinterpret s) next
+