packages feed

bv-sized 0.5.0 → 0.6.0

raw patch · 29 files changed

+2259/−586 lines, 29 filesdep +prettydep −prettyclass

Dependencies added: pretty

Dependencies removed: prettyclass

Files

bv-sized.cabal view
@@ -1,16 +1,16 @@ name:                bv-sized-version:             0.5.0+version:             0.6.0 category:            Bit Vectors synopsis:            a BitVector datatype that is parameterized by the vector width description:   This module defines a width-parameterized 'BitVector' type and various associated   operations that assume a 2's complement representation.-homepage:            https://github.com/benjaminselfridge/bv-sized+homepage:            https://github.com/GaloisInc/bv-sized license:             BSD3 license-file:        LICENSE author:              Ben Selfridge maintainer:          benselfridge@galois.com-copyright:           March 2018+copyright:           Galois Inc., Ben Selfridge March 2018 build-type:          Simple cabal-version:       >=1.10 extra-source-files:  README.md@@ -19,12 +19,13 @@   exposed-modules:     Data.BitVector.Sized                      , Data.BitVector.Sized.App                      , Data.BitVector.Sized.BitLayout+  other-modules:       Data.BitVector.Sized.Internal   build-depends:       base >= 4.7 && < 5                      , containers >= 0.5.10 && < 0.6                      , lens >= 4 && < 5                      , mtl >= 2 && < 3                      , parameterized-utils-                     , prettyclass >= 1.0 && < 2.0+                     , pretty                      , random >= 1.1 && < 1.2                      , QuickCheck >= 2.11 && < 2.12   hs-source-dirs:      src@@ -42,6 +43,6 @@                      , bv-sized                      , lens >= 4 && < 5                      , parameterized-utils-                     , prettyclass >= 1.0 && < 2.0+                     , pretty                      , random >= 1.1 && < 1.2                      , QuickCheck >= 2.11 && < 2.12
+ cabal.project view
@@ -0,0 +1,2 @@+packages: .+          submodules/parameterized-utils
changelog.md view
@@ -1,5 +1,15 @@ # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized) +## 0.6.0 *March 2019*+* changed WithRepr functions to '+* added Num, Bits instances+* bitVector now takes arbitrary Integral argument+* add 'bitLayoutAssignmentList' function (see haddocks for details+* Hid BV constructor, exposed BitVector as pattern++## 0.5.1 *August 2018*+  * fixed github URL+ ## 0.5.0 *August 2018*   * Added a lot of better support for the App module, including a type class for     embedding BVApp expressions along with associated smart constructors
src/Data/BitVector/Sized.hs view
@@ -1,8 +1,8 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-}  {-|@@ -19,12 +19,12 @@  module Data.BitVector.Sized   ( -- * BitVector type-    BitVector(..)-  , bitVector+    BitVector, pattern BitVector+  , bitVector, bitVector'   , bv0     -- * Bitwise operations (width-preserving)-    -- | These are alternative versions of some of the 'Bits' functions where we do-    -- not need to know the width at compile time. They are all width-preserving.+    -- | These are alternative versions of some of the 'Data.Bits' functions where we+    -- do not need to know the width at compile time. They are all width-preserving.   , bvAnd, bvOr, bvXor   , bvComplement   , bvShift, bvShiftL, bvShiftRA, bvShiftRL, bvRotate@@ -41,10 +41,10 @@   , bvLTS, bvLTU     -- * Variable-width operations     -- | These are functions that involve bit vectors of different lengths.-  , bvConcat, (<:>), bvConcatMany, bvConcatManyWithRepr-  , bvExtract, bvExtractWithRepr-  , bvZext, bvZextWithRepr-  , bvSext, bvSextWithRepr+  , bvConcat, (<:>), bvConcatMany, bvConcatMany'+  , bvExtract, bvExtract'+  , bvZext, bvZext'+  , bvSext, bvSext'     -- * Conversions to Integer   , bvIntegerU   , bvIntegerS@@ -52,391 +52,4 @@   , bvGetBytesU   ) where -import Data.Bits-import Data.Ix-import Data.Parameterized-import GHC.TypeLits-import Numeric-import System.Random-import Test.QuickCheck (Arbitrary(..), choose)-import Text.PrettyPrint.HughesPJClass-import Text.Printf-import Unsafe.Coerce (unsafeCoerce)--------------------------------------------- BitVector data type definitions---- | BitVector datatype, parameterized by width.-data BitVector (w :: Nat) :: * where-  BV :: NatRepr w -> Integer -> BitVector w---- | Construct a bit vector with a particular width, where the width is inferrable--- from the type context. The 'Integer' input (an unbounded data type, hence with an--- infinite-width bit representation), whether positive or negative, is silently--- truncated to fit into the number of bits demanded by the return type.------ >>> bitVector 0xA :: BitVector 4--- 0xa--- >>> bitVector 0xA :: BitVector 2--- 0x2-bitVector :: KnownNat w => Integer -> BitVector w-bitVector x = BV wRepr (truncBits width (fromIntegral x))-  where wRepr = knownNat-        width = natValue wRepr---- | The zero bitvector with width 0.-bv0 :: BitVector 0-bv0 = bitVector 0--------------------------------------------- BitVector -> Integer functions---- | Unsigned interpretation of a bit vector as a (positive) Integer.-bvIntegerU :: BitVector w -> Integer-bvIntegerU (BV _ x) = x---- | Signed interpretation of a bit vector as an Integer.-bvIntegerS :: BitVector w -> Integer-bvIntegerS bv = if bvTestBit bv (width - 1)-                then bvIntegerU bv - (1 `shiftL` width)-                else bvIntegerU bv-  where width = bvWidth bv--------------------------------------------- BitVector w operations (fixed width)---- | Bitwise and.-bvAnd :: BitVector w -> BitVector w -> BitVector w-bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)---- | Bitwise or.-bvOr :: BitVector w -> BitVector w -> BitVector w-bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)---- | Bitwise xor.-bvXor :: BitVector w -> BitVector w -> BitVector w-bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)---- | Bitwise complement (flip every bit).-bvComplement :: BitVector w -> BitVector w-bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))-  where width = natValue wRepr---- | Bitwise shift. Uses an arithmetic right shift.-bvShift :: BitVector w -> Int -> BitVector w-bvShift bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))-  where width = natValue wRepr-        x     = bvIntegerS bv -- arithmetic right shift when negative--toPos :: Int -> Int-toPos x | x < 0 = 0-toPos x = x---- | Left shift.-bvShiftL :: BitVector w -> Int -> BitVector w-bvShiftL bv shf = bvShift bv (toPos shf)---- | Right arithmetic shift.-bvShiftRA :: BitVector w -> Int -> BitVector w-bvShiftRA bv shf = bvShift bv (- (toPos shf))---- | Right logical shift.-bvShiftRL :: BitVector w -> Int -> BitVector w-bvShiftRL bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` (- toPos shf)))-  where width = natValue wRepr-        x     = bvIntegerU bv---- | Bitwise rotate.-bvRotate :: BitVector w -> Int -> BitVector w-bvRotate bv rot' = leftChunk `bvOr` rightChunk-  where rot = rot' `mod` bvWidth bv-        leftChunk = bvShift bv rot-        rightChunk = bvShift bv (rot - bvWidth bv)---- | Get the width of a 'BitVector'.-bvWidth :: BitVector w -> Int-bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)---- | Test if a particular bit is set.-bvTestBit :: BitVector w -> Int -> Bool-bvTestBit (BV _ x) b = testBit x b---- | Get the number of 1 bits in a 'BitVector'.-bvPopCount :: BitVector w -> Int-bvPopCount (BV _ x) = popCount x---- | Truncate a bit vector to a particular width given at runtime, while keeping the--- type-level width constant.-bvTruncBits :: BitVector w -> Int -> BitVector w-bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)--------------------------------------------- BitVector w arithmetic operations (fixed width)---- | Bitwise add.-bvAdd :: BitVector w -> BitVector w -> BitVector w-bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))-  where width = natValue wRepr---- | Bitwise multiply.-bvMul :: BitVector w -> BitVector w -> BitVector w-bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))-  where width = natValue wRepr---- | Bitwise division (unsigned). Rounds to zero.-bvQuotU :: BitVector w -> BitVector w -> BitVector w-bvQuotU (BV wRepr x) (BV _ y) = BV wRepr (x `quot` y)---- | Bitwise division (signed). Rounds to zero (not negative infinity).-bvQuotS :: BitVector w -> BitVector w -> BitVector w-bvQuotS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `quot` y))-  where x = bvIntegerS bv1-        y = bvIntegerS bv2-        width = natValue wRepr---- | Bitwise remainder after division (unsigned), when rounded to zero.-bvRemU :: BitVector w -> BitVector w -> BitVector w-bvRemU (BV wRepr x) (BV _ y) = BV wRepr (x `rem` y)---- | Bitwise remainder after  division (signed), when rounded to zero (not negative--- infinity).-bvRemS :: BitVector w -> BitVector w -> BitVector w-bvRemS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `rem` y))-  where x = bvIntegerS bv1-        y = bvIntegerS bv2-        width = natValue wRepr---- | Bitwise absolute value.-bvAbs :: BitVector w -> BitVector w-bvAbs bv@(BV wRepr _) = BV wRepr abs_x-  where width = natValue wRepr-        x     = bvIntegerS bv-        abs_x = truncBits width (abs x) -- this is necessary---- | Bitwise negation.-bvNegate :: BitVector w -> BitVector w-bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))-  where width = fromIntegral (natValue wRepr) :: Integer---- | Get the sign bit as a 'BitVector'.-bvSignum :: BitVector w -> BitVector w-bvSignum bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1-  where width = fromIntegral (natValue wRepr)---- | Signed less than.-bvLTS :: BitVector w -> BitVector w -> Bool-bvLTS bv1 bv2 = bvIntegerS bv1 < bvIntegerS bv2---- | Unsigned less than.-bvLTU :: BitVector w -> BitVector w -> Bool-bvLTU bv1 bv2 = bvIntegerU bv1 < bvIntegerU bv2--------------------------------------------- Width-changing operations---- | Concatenate two bit vectors.------ >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)--- 0xaabcdef0--- >>> :type it--- it :: BitVector 32------ Note that the first argument gets placed in the higher-order bits. The above--- example should be illustrative enough.-bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)-bvConcat (BV hiWRepr hi) (BV loWRepr lo) =-  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)-  where loWidth = fromIntegral (natValue loWRepr)---- | Infix 'bvConcat'.-(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)-(<:>) = bvConcat--bvConcatSome :: Some BitVector -> Some BitVector -> Some BitVector-bvConcatSome (Some bv1) (Some bv2) = Some (bv2 <:> bv1)---- | Concatenate a list of 'BitVector's into a 'BitVector' of arbitrary width. The ordering is little endian:------ >>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16--- 0xbbaa--- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16--- 0xbbaa------ If the sum of the widths of the input 'BitVector's exceeds the output width, we--- ignore the tail end of the list.-bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w'-bvConcatMany = bvConcatManyWithRepr knownNat---- | 'bvConcatMany' with an explicit 'NatRepr'.-bvConcatManyWithRepr :: NatRepr w' -> [BitVector w] -> BitVector w'-bvConcatManyWithRepr wRepr bvs =-  viewSome (bvZextWithRepr wRepr) $ foldl bvConcatSome (Some bv0) (Some <$> bvs)--infixl 6 <:>---- | Slice out a smaller bit vector from a larger one. The lowest significant bit is--- given explicitly as an argument of type 'Int', and the length of the slice is--- inferred from a type-level context.------ >>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8--- 0xcd------ Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and--- extract bits that aren't present in the input, you will get 0's.-bvExtract :: forall w w' . (KnownNat w')-          => Int-          -> BitVector w-          -> BitVector w'-bvExtract pos bv = bitVector xShf-  where (BV _ xShf) = bvShift bv (- pos)---- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.-bvExtractWithRepr :: NatRepr w'-                  -> Int-                  -> BitVector w-                  -> BitVector w'-bvExtractWithRepr repr pos bv = BV repr (truncBits width xShf)-  where (BV _ xShf) = bvShift bv (- pos)-        width = natValue repr---- | Zero-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvZext :: forall w w' . KnownNat w'-       => BitVector w-       -> BitVector w'-bvZext (BV _ x) = bitVector x---- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.-bvZextWithRepr :: NatRepr w'-               -> BitVector w-               -> BitVector w'-bvZextWithRepr repr (BV _ x) = BV repr (truncBits width x)-  where width = natValue repr---- | Sign-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvSext :: forall w w' . KnownNat w'-       => BitVector w-       -> BitVector w'-bvSext bv = bitVector (bvIntegerS bv)---- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.-bvSextWithRepr :: NatRepr w'-               -> BitVector w-               -> BitVector w'-bvSextWithRepr repr bv = BV repr (truncBits width (bvIntegerS bv))-  where width = natValue repr--------------------------------------------- Byte decomposition---- | Given a 'BitVector' of arbitrary length, decompose it into a list of bytes. Uses--- an unsigned interpretation of the input vector, so if you ask for more bytes that--- the 'BitVector' contains, you get zeros. The result is little-endian, so the first--- element of the list will be the least significant byte of the input vector.-bvGetBytesU :: Int -> BitVector w -> [BitVector 8]-bvGetBytesU n _ | n <= 0 = []-bvGetBytesU n bv = bvExtract 0 bv : bvGetBytesU (n-1) (bvShiftRL bv 8)--------------------------------------------- Bits---- | Mask for a specified number of lower bits.-lowMask :: (Integral a, Bits b) => a -> b-lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)---- | Truncate to a specified number of lower bits.-truncBits :: (Integral a, Bits b) => a -> b -> b-truncBits width b = b .&. lowMask width--------------------------------------------- Class instances-$(return [])--instance Show (BitVector w) where-  show (BV _ x) = "0x" ++ showHex x ""--instance KnownNat w => Read (BitVector w) where-  readsPrec s =-    (fmap . fmap) (\(a,s') -> (bitVector a, s')) (readsPrec s :: ReadS Integer)--instance ShowF BitVector--instance Eq (BitVector w) where-  (BV _ x) == (BV _ y) = x == y--instance EqF BitVector where-  (BV _ x) `eqF` (BV _ y) = x == y--instance Ord (BitVector w) where-  (BV _ x) `compare` (BV _ y) = x `compare` y--instance OrdF BitVector where-  (BV xRepr x) `compareF` (BV yRepr y) =-    case xRepr `compareF` yRepr of-      EQF -> fromOrdering (x `compare` y)-      cmp -> cmp--instance TestEquality BitVector where-  testEquality (BV wRepr x) (BV wRepr' y) =-    if natValue wRepr == natValue wRepr' && x == y-    then Just (unsafeCoerce (Refl :: a :~: a))-    else Nothing--instance KnownNat w => Bits (BitVector w) where-  (.&.)        = bvAnd-  (.|.)        = bvOr-  xor          = bvXor-  complement   = bvComplement-  shift        = bvShift-  rotate       = bvRotate-  bitSize      = bvWidth-  bitSizeMaybe = Just . bvWidth-  isSigned     = const False-  testBit      = bvTestBit-  bit          = bitVector . bit-  popCount     = bvPopCount--instance KnownNat w => FiniteBits (BitVector w) where-  finiteBitSize = bvWidth--instance KnownNat w => Num (BitVector w) where-  (+)         = bvAdd-  (*)         = bvMul-  abs         = bvAbs-  signum      = bvSignum-  fromInteger = bitVector-  negate      = bvNegate--instance KnownNat w => Enum (BitVector w) where-  toEnum   = bitVector . fromIntegral-  fromEnum = fromIntegral . bvIntegerU--instance KnownNat w => Ix (BitVector w) where-  range (lo, hi) = bitVector <$> [bvIntegerU lo .. bvIntegerU hi]-  index (lo, hi) bv = index (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)-  inRange (lo, hi) bv = inRange (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)--instance KnownNat w => Bounded (BitVector w) where-  minBound = bitVector 0-  maxBound = bitVector (-1)--instance KnownNat w => Arbitrary (BitVector w) where-  arbitrary = choose (minBound, maxBound)--instance KnownNat w => Random (BitVector w) where-  randomR (bvLo, bvHi) gen =-    let (x, gen') = randomR (bvIntegerU bvLo, bvIntegerU bvHi) gen-    in (bitVector x, gen')-  random gen =-    let (x, gen') = random gen-    in (bitVector x, gen')--prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String-prettyHex width val = printf format val width-  where numDigits = (width+3) `quot` 4-        format = "0x%." ++ show numDigits ++ "x<%d>"--instance Pretty (BitVector w) where-  -- | Pretty print a bit vector (shows its width)-  pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x+import Data.BitVector.Sized.Internal
src/Data/BitVector/Sized/App.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-}@@ -48,6 +49,9 @@   , quotsE   , remuE   , remsE+  , negateE+  , absE+  , signumE   , sllE   , srlE   , sraE@@ -56,9 +60,9 @@   , ltuE   , ltsE   -- ** Width-changing-  , zextE, zextEWithRepr-  , sextE, sextEWithRepr-  , extractE, extractEWithRepr+  , zextE, zextE'+  , sextE, sextE'+  , extractE, extractE'   , concatE   -- ** Control   , iteE@@ -66,6 +70,7 @@  import Control.Monad.Identity import Data.BitVector.Sized+import Data.Bits import Data.Parameterized import Data.Parameterized.TH.GADT import Foreign.Marshal.Utils (fromBool)@@ -96,6 +101,9 @@   QuotSApp :: !(expr w) -> !(expr w) -> BVApp expr w   RemUApp  :: !(expr w) -> !(expr w) -> BVApp expr w   RemSApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  NegateApp :: !(expr w) -> BVApp expr w+  AbsApp   :: !(expr w) -> BVApp expr w+  SignumApp :: !(expr w) -> BVApp expr w    -- Comparisons   EqApp  :: !(expr w) -> !(expr w) -> BVApp expr 1@@ -120,6 +128,9 @@ instance TestEquality expr => Eq (BVApp expr w) where   (==) = \x y -> isJust (testEquality x y) +instance TestEquality expr => EqF (BVApp expr) where+  eqF = (==)+ instance OrdF expr => OrdF (BVApp expr) where   compareF = $(structuralTypeOrd [t|BVApp|]                 [ (AnyType `TypeApp` AnyType, [|compareF|]) ])@@ -160,12 +171,15 @@ evalBVAppM eval (QuotUApp e1 e2) = bvQuotU  <$> eval e1 <*> eval e2 evalBVAppM eval (RemSApp  e1 e2) = bvRemS   <$> eval e1 <*> eval e2 evalBVAppM eval (RemUApp  e1 e2) = bvRemU   <$> eval e1 <*> eval e2+evalBVAppM eval (NegateApp e) = bvNegate <$> eval e+evalBVAppM eval (AbsApp e) = bvAbs <$> eval e+evalBVAppM eval (SignumApp e) = bvSignum <$> eval e evalBVAppM eval (EqApp  e1 e2) = fromBool <$> ((==)  <$> eval e1 <*> eval e2) evalBVAppM eval (LtuApp e1 e2) = fromBool <$> (bvLTU <$> eval e1 <*> eval e2) evalBVAppM eval (LtsApp e1 e2) = fromBool <$> (bvLTS <$> eval e1 <*> eval e2)-evalBVAppM eval (ZExtApp wRepr e) = bvZextWithRepr wRepr <$> eval e-evalBVAppM eval (SExtApp wRepr e) = bvSextWithRepr wRepr <$> eval e-evalBVAppM eval (ExtractApp wRepr base e) = bvExtractWithRepr wRepr base <$> eval e+evalBVAppM eval (ZExtApp wRepr e) = bvZext' wRepr <$> eval e+evalBVAppM eval (SExtApp wRepr e) = bvSext' wRepr <$> eval e+evalBVAppM eval (ExtractApp wRepr base e) = bvExtract' wRepr base <$> eval e evalBVAppM eval (ConcatApp e1 e2) = do   e1Val <- eval e1   e2Val <- eval e2@@ -186,6 +200,31 @@ class BVExpr (expr :: Nat -> *) where   appExpr :: BVApp expr w -> expr w +instance (KnownNat w, BVExpr expr) => Num (BVApp expr w) where+  app1 + app2 = AddApp (appExpr app1) (appExpr app2)+  app1 * app2 = MulApp (appExpr app1) (appExpr app2)+  abs app = AbsApp (appExpr app)+  signum app = SignumApp (appExpr app)+  fromInteger x = LitBVApp (fromInteger x)+  negate app = NegateApp (appExpr app)+  app1 - app2 = SubApp (appExpr app1) (appExpr app2)++-- TODO: finish+instance (KnownNat w, BVExpr expr, TestEquality expr) => Bits (BVApp expr w) where+  app1 .&. app2 = AndApp (appExpr app1) (appExpr app2)+  app1 .|. app2 = OrApp (appExpr app1) (appExpr app2)+  app1 `xor` app2 = XorApp (appExpr app1) (appExpr app2)+  complement app = NotApp (appExpr app)+  shiftL app x = SllApp (appExpr app) (litBV (bitVector x))+  shiftR app x = SraApp (appExpr app) (litBV (bitVector x))+  rotate = undefined+  bitSize = undefined+  bitSizeMaybe = undefined+  isSigned = undefined+  testBit = undefined+  bit = undefined+  popCount = undefined+ -- | Literal bit vector. litBV :: BVExpr expr => BitVector w -> expr w litBV = appExpr . LitBVApp@@ -214,27 +253,36 @@ subE :: BVExpr expr => expr w -> expr w -> expr w subE e1 e2 = appExpr (SubApp e1 e2) --- | Signed multiply two 'BitVectors', doubling the width of the result to hold all+-- | Signed multiply two 'BitVector's, doubling the width of the result to hold all -- arithmetic overflow bits. mulE :: BVExpr expr => expr w -> expr w -> expr w mulE e1 e2 = appExpr (MulApp e1 e2) --- | Signed divide two 'BitVectors', rounding to zero.+-- | Signed divide two 'BitVector's, rounding to zero. quotsE :: BVExpr expr => expr w -> expr w -> expr w quotsE e1 e2 = appExpr (QuotSApp e1 e2) --- | Unsigned divide two 'BitVectors', rounding to zero.+-- | Unsigned divide two 'BitVector's, rounding to zero. quotuE :: BVExpr expr => expr w -> expr w -> expr w quotuE e1 e2 = appExpr (QuotUApp e1 e2) --- | Remainder after signed division of two 'BitVectors', when rounded to zero.+-- | Remainder after signed division of two 'BitVector's, when rounded to zero. remsE :: BVExpr expr => expr w -> expr w -> expr w remsE e1 e2 = appExpr (RemSApp e1 e2) --- | Remainder after unsigned division of two 'BitVectors', when rounded to zero.+-- | Remainder after unsigned division of two 'BitVector's, when rounded to zero. remuE :: BVExpr expr => expr w -> expr w -> expr w remuE e1 e2 = appExpr (RemUApp e1 e2) +negateE :: BVExpr expr => expr w -> expr w+negateE e = appExpr (NegateApp e)++absE :: BVExpr expr => expr w -> expr w+absE e = appExpr (AbsApp e)++signumE :: BVExpr expr => expr w -> expr w+signumE e = appExpr (SignumApp e)+ -- | Left logical shift the first expression by the second. sllE :: BVExpr expr => expr w -> expr w -> expr w sllE e1 e2 = appExpr (SllApp e1 e2)@@ -264,24 +312,24 @@ zextE e = appExpr (ZExtApp knownNat e)  -- | Zero-extension with an explicit width argument-zextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'-zextEWithRepr repr e = appExpr (ZExtApp repr e)+zextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w'+zextE' repr e = appExpr (ZExtApp repr e)  -- | Sign-extension sextE :: (BVExpr expr, KnownNat w') => expr w -> expr w' sextE e = appExpr (SExtApp knownNat e)  -- | Sign-extension with an explicit width argument-sextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'-sextEWithRepr repr e = appExpr (SExtApp repr e)+sextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w'+sextE' repr e = appExpr (SExtApp repr e)  -- | Extract bits extractE :: (BVExpr expr, KnownNat w') => Int -> expr w -> expr w' extractE base e = appExpr (ExtractApp knownNat base e)  -- | Extract bits with an explicit width argument-extractEWithRepr :: BVExpr expr => NatRepr w' -> Int -> expr w -> expr w'-extractEWithRepr wRepr base e = appExpr (ExtractApp wRepr base e)+extractE' :: BVExpr expr => NatRepr w' -> Int -> expr w -> expr w'+extractE' wRepr base e = appExpr (ExtractApp wRepr base e)  -- | Concatenation concatE :: BVExpr expr => expr w -> expr w' -> expr (w+w')
src/Data/BitVector/Sized/BitLayout.hs view
@@ -32,9 +32,11 @@   , extract     -- * Lenses   , layoutLens, layoutsLens+    -- * Utilities+  , bitLayoutAssignmentList   ) where -import Data.BitVector.Sized+import Data.BitVector.Sized.Internal import Data.Foldable import qualified Data.Functor.Product as P import Control.Lens (lens, Simple, Lens)@@ -198,8 +200,8 @@        -> BitVector s        -> BitVector t        -> BitVector t-bvOrAt start sVec tVec@(BV tRepr _) =-  (bvZextWithRepr tRepr sVec `bvShift` start) `bvOr` tVec+bvOrAt start sVec tVec@(BitVector tRepr _) =+  (bvZext' tRepr sVec `bvShift` start) `bvOr` tVec  -- | Given a list of 'Chunk's, inject each chunk from a source 'BitVector' @s@ into a -- target 'BitVector' @t@.@@ -230,7 +232,7 @@              -> BitVector s extractChunk sRepr sStart (Some (Chunk chunkRepr chunkStart)) tVec =   bvShift extractedChunk sStart-  where extractedChunk = bvZextWithRepr sRepr (bvExtractWithRepr chunkRepr chunkStart tVec)+  where extractedChunk = bvZext' sRepr (bvExtract' chunkRepr chunkStart tVec)  extractAll :: NatRepr s       -- ^ determines width of output vector            -> Int             -- ^ current position in output vector@@ -241,7 +243,7 @@ extractAll sRepr outStart (chk@(Some (Chunk chunkRepr _)) : chunks) tVec =   extractChunk sRepr outStart chk tVec `bvOr`   extractAll sRepr (outStart + chunkWidth) chunks tVec-  where chunkWidth = fromInteger (natValue chunkRepr)+  where chunkWidth = fromInteger (intValue chunkRepr)  -- | Use a 'BitLayout' to extract a smaller vector from a larger one. extract :: BitLayout t s -- ^ The layout@@ -260,3 +262,22 @@   (\bv bvFlds -> ifoldr (\_ (P.Pair fld layout) bv' -> inject layout bv' fld)                  bv                  (izipWith (const P.Pair) bvFlds layouts))++-- | From a `BitLayout`, get a list representing the position of each bit from the+-- source to the target. The list+--+-- @+-- [3,4,5,10,11,12,13]+-- @+--+-- means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the+-- source is placed in bit 4 of the target, etc.++bitLayoutAssignmentList :: BitLayout t s -> [Int]+bitLayoutAssignmentList (BitLayout _ _ someChunks) = reverse (bitLayoutAssignmentList' (toList someChunks))++bitLayoutAssignmentList' :: [Some Chunk] -> [Int]+bitLayoutAssignmentList' [] = []+bitLayoutAssignmentList' (Some (Chunk wRepr start):rst) =+  reverse [start..start+w-1] ++ bitLayoutAssignmentList' rst+  where w = fromIntegral (natValue wRepr)
+ src/Data/BitVector/Sized/Internal.hs view
@@ -0,0 +1,419 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}++{-|+Module      : Data.BitVector.Sized+Copyright   : (c) Galois Inc. 2018+License     : BSD-3+Maintainer  : benselfridge@galois.com+Stability   : experimental+Portability : portable++This module defines a width-parameterized 'BitVector' type and various associated+operations that assume a 2's complement representation.+-}++module Data.BitVector.Sized.Internal where++import Data.Bits+import Data.Ix+import Data.Parameterized+import GHC.TypeLits+import Numeric+import System.Random+import Test.QuickCheck (Arbitrary(..), choose)+import Text.PrettyPrint.HughesPJClass+import Text.Printf+import Unsafe.Coerce (unsafeCoerce)++----------------------------------------+-- BitVector data type definitions++-- | BitVector datatype, parameterized by width.+data BitVector (w :: Nat) :: * where+  BV :: NatRepr w -> Integer -> BitVector w++-- | 'BitVector' can be treated as a constructor for pattern matching, but to build+-- one you must use the smart constructor `bitVector`.+pattern BitVector :: NatRepr w -> Integer -> BitVector w+pattern BitVector wRepr x <- BV wRepr x+{-# COMPLETE BitVector #-}++-- | Construct a bit vector with a particular width, where the width is inferrable+-- from the type context. The input (an unbounded data type, hence with an+-- infinite-width bit representation), whether positive or negative, is silently+-- truncated to fit into the number of bits demanded by the return type.+--+-- >>> bitVector 0xA :: BitVector 4+-- 0xa+-- >>> bitVector 0xA :: BitVector 2+-- 0x2+bitVector :: (Integral a, KnownNat w) => a -> BitVector w+bitVector x = bitVector' knownNat x++-- | Like 'bitVector', but with an explict 'NatRepr'.+bitVector' :: Integral a => NatRepr w -> a -> BitVector w+bitVector' wRepr x = BV wRepr (truncBits width (fromIntegral x))+  where width = natValue wRepr++-- | The zero bitvector with width 0.+bv0 :: BitVector 0+bv0 = bitVector (0 :: Integer)++----------------------------------------+-- BitVector -> Integer functions++-- | Unsigned interpretation of a bit vector as a (positive) Integer.+bvIntegerU :: BitVector w -> Integer+bvIntegerU (BV _ x) = x++-- | Signed interpretation of a bit vector as an Integer.+bvIntegerS :: BitVector w -> Integer+bvIntegerS bv = if bvTestBit bv (width - 1)+                then bvIntegerU bv - (1 `shiftL` width)+                else bvIntegerU bv+  where width = bvWidth bv++----------------------------------------+-- BitVector w operations (fixed width)++-- | Bitwise and.+bvAnd :: BitVector w -> BitVector w -> BitVector w+bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)++-- | Bitwise or.+bvOr :: BitVector w -> BitVector w -> BitVector w+bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)++-- | Bitwise xor.+bvXor :: BitVector w -> BitVector w -> BitVector w+bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)++-- | Bitwise complement (flip every bit).+bvComplement :: BitVector w -> BitVector w+bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))+  where width = natValue wRepr++-- | Bitwise shift. Uses an arithmetic right shift.+bvShift :: BitVector w -> Int -> BitVector w+bvShift bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))+  where width = natValue wRepr+        x     = bvIntegerS bv -- arithmetic right shift when negative++toPos :: Int -> Int+toPos x | x < 0 = 0+toPos x = x++-- | Left shift.+bvShiftL :: BitVector w -> Int -> BitVector w+bvShiftL bv shf = bvShift bv (toPos shf)++-- | Right arithmetic shift.+bvShiftRA :: BitVector w -> Int -> BitVector w+bvShiftRA bv shf = bvShift bv (- (toPos shf))++-- | Right logical shift.+bvShiftRL :: BitVector w -> Int -> BitVector w+bvShiftRL bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` (- toPos shf)))+  where width = natValue wRepr+        x     = bvIntegerU bv++-- | Bitwise rotate.+bvRotate :: BitVector w -> Int -> BitVector w+bvRotate bv rot' = leftChunk `bvOr` rightChunk+  where rot = rot' `mod` bvWidth bv+        leftChunk = bvShift bv rot+        rightChunk = bvShift bv (rot - bvWidth bv)++-- | Get the width of a 'BitVector'.+bvWidth :: BitVector w -> Int+bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)++-- | Test if a particular bit is set.+bvTestBit :: BitVector w -> Int -> Bool+bvTestBit (BV _ x) b = testBit x b++-- | Get the number of 1 bits in a 'BitVector'.+bvPopCount :: BitVector w -> Int+bvPopCount (BV _ x) = popCount x++-- | Truncate a bit vector to a particular width given at runtime, while keeping the+-- type-level width constant.+bvTruncBits :: BitVector w -> Int -> BitVector w+bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)++----------------------------------------+-- BitVector w arithmetic operations (fixed width)++-- | Bitwise add.+bvAdd :: BitVector w -> BitVector w -> BitVector w+bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))+  where width = natValue wRepr++-- | Bitwise multiply.+bvMul :: BitVector w -> BitVector w -> BitVector w+bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))+  where width = natValue wRepr++-- | Bitwise division (unsigned). Rounds to zero.+bvQuotU :: BitVector w -> BitVector w -> BitVector w+bvQuotU (BV wRepr x) (BV _ y) = BV wRepr (x `quot` y)++-- | Bitwise division (signed). Rounds to zero (not negative infinity).+bvQuotS :: BitVector w -> BitVector w -> BitVector w+bvQuotS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `quot` y))+  where x = bvIntegerS bv1+        y = bvIntegerS bv2+        width = natValue wRepr++-- | Bitwise remainder after division (unsigned), when rounded to zero.+bvRemU :: BitVector w -> BitVector w -> BitVector w+bvRemU (BV wRepr x) (BV _ y) = BV wRepr (x `rem` y)++-- | Bitwise remainder after  division (signed), when rounded to zero (not negative+-- infinity).+bvRemS :: BitVector w -> BitVector w -> BitVector w+bvRemS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `rem` y))+  where x = bvIntegerS bv1+        y = bvIntegerS bv2+        width = natValue wRepr++-- | Bitwise absolute value.+bvAbs :: BitVector w -> BitVector w+bvAbs bv@(BV wRepr _) = BV wRepr abs_x+  where width = natValue wRepr+        x     = bvIntegerS bv+        abs_x = truncBits width (abs x) -- this is necessary++-- | Bitwise negation.+bvNegate :: BitVector w -> BitVector w+bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))+  where width = fromIntegral (natValue wRepr) :: Integer++-- | Get the sign bit as a 'BitVector'.+bvSignum :: BitVector w -> BitVector w+bvSignum bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1+  where width = fromIntegral (natValue wRepr)++-- | Signed less than.+bvLTS :: BitVector w -> BitVector w -> Bool+bvLTS bv1 bv2 = bvIntegerS bv1 < bvIntegerS bv2++-- | Unsigned less than.+bvLTU :: BitVector w -> BitVector w -> Bool+bvLTU bv1 bv2 = bvIntegerU bv1 < bvIntegerU bv2++----------------------------------------+-- Width-changing operations++-- | Concatenate two bit vectors.+--+-- >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)+-- 0xaabcdef0+-- >>> :type it+-- it :: BitVector 32+--+-- Note that the first argument gets placed in the higher-order bits. The above+-- example should be illustrative enough.+bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)+bvConcat (BV hiWRepr hi) (BV loWRepr lo) =+  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)+  where loWidth = fromIntegral (natValue loWRepr)++-- | Infix 'bvConcat'.+(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)+(<:>) = bvConcat++bvConcatSome :: Some BitVector -> Some BitVector -> Some BitVector+bvConcatSome (Some bv1) (Some bv2) = Some (bv2 <:> bv1)++-- | Concatenate a list of 'BitVector's into a 'BitVector' of arbitrary width. The ordering is little endian:+--+-- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16+-- 0xbbaa+-- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16+-- 0xbbaa+--+-- If the sum of the widths of the input 'BitVector's exceeds the output width, we+-- ignore the tail end of the list.+bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w'+bvConcatMany = bvConcatMany' knownNat++-- | 'bvConcatMany' with an explicit 'NatRepr'.+bvConcatMany' :: NatRepr w' -> [BitVector w] -> BitVector w'+bvConcatMany' wRepr bvs =+  viewSome (bvZext' wRepr) $ foldl bvConcatSome (Some bv0) (Some <$> bvs)++infixl 6 <:>++-- | Slice out a smaller bit vector from a larger one. The lowest significant bit is+-- given explicitly as an argument of type 'Int', and the length of the slice is+-- inferred from a type-level context.+--+-- >>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8+-- 0xcd+--+-- Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and+-- extract bits that aren't present in the input, you will get 0's.+bvExtract :: forall w w' . (KnownNat w')+          => Int+          -> BitVector w+          -> BitVector w'+bvExtract pos bv = bitVector xShf+  where (BV _ xShf) = bvShift bv (- pos)++-- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.+bvExtract' :: NatRepr w'+                  -> Int+                  -> BitVector w+                  -> BitVector w'+bvExtract' repr pos bv = BV repr (truncBits width xShf)+  where (BV _ xShf) = bvShift bv (- pos)+        width = natValue repr++-- | Zero-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvZext :: forall w w' . KnownNat w'+       => BitVector w+       -> BitVector w'+bvZext (BV _ x) = bitVector x++-- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.+bvZext' :: NatRepr w'+               -> BitVector w+               -> BitVector w'+bvZext' repr (BV _ x) = BV repr (truncBits width x)+  where width = natValue repr++-- | Sign-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvSext :: forall w w' . KnownNat w'+       => BitVector w+       -> BitVector w'+bvSext bv = bitVector (bvIntegerS bv)++-- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.+bvSext' :: NatRepr w'+               -> BitVector w+               -> BitVector w'+bvSext' repr bv = BV repr (truncBits width (bvIntegerS bv))+  where width = natValue repr++----------------------------------------+-- Byte decomposition++-- | Given a 'BitVector' of arbitrary length, decompose it into a list of bytes. Uses+-- an unsigned interpretation of the input vector, so if you ask for more bytes that+-- the 'BitVector' contains, you get zeros. The result is little-endian, so the first+-- element of the list will be the least significant byte of the input vector.+bvGetBytesU :: Int -> BitVector w -> [BitVector 8]+bvGetBytesU n _ | n <= 0 = []+bvGetBytesU n bv = bvExtract 0 bv : bvGetBytesU (n-1) (bvShiftRL bv 8)++----------------------------------------+-- Bits++-- | Mask for a specified number of lower bits.+lowMask :: (Integral a, Bits b) => a -> b+lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)++-- | Truncate to a specified number of lower bits.+truncBits :: (Integral a, Bits b) => a -> b -> b+truncBits width b = b .&. lowMask width++----------------------------------------+-- Class instances+$(return [])++instance Show (BitVector w) where+  show (BV _ x) = "0x" ++ showHex x ""++instance KnownNat w => Read (BitVector w) where+  readsPrec s =+    (fmap . fmap) (\(a,s') -> (bitVector a, s')) (readsPrec s :: ReadS Integer)++instance ShowF BitVector++instance Eq (BitVector w) where+  (BV _ x) == (BV _ y) = x == y++instance EqF BitVector where+  (BV _ x) `eqF` (BV _ y) = x == y++instance Ord (BitVector w) where+  (BV _ x) `compare` (BV _ y) = x `compare` y++instance OrdF BitVector where+  (BV xRepr x) `compareF` (BV yRepr y) =+    case xRepr `compareF` yRepr of+      EQF -> fromOrdering (x `compare` y)+      cmp -> cmp++instance TestEquality BitVector where+  testEquality (BV wRepr x) (BV wRepr' y) =+    if natValue wRepr == natValue wRepr' && x == y+    then Just (unsafeCoerce (Refl :: a :~: a))+    else Nothing++instance KnownNat w => Bits (BitVector w) where+  (.&.)        = bvAnd+  (.|.)        = bvOr+  xor          = bvXor+  complement   = bvComplement+  shift        = bvShift+  rotate       = bvRotate+  bitSize      = bvWidth+  bitSizeMaybe = Just . bvWidth+  isSigned     = const False+  testBit      = bvTestBit+  bit          = bitVector . (bit :: Int -> Integer)+  popCount     = bvPopCount++instance KnownNat w => FiniteBits (BitVector w) where+  finiteBitSize = bvWidth++instance KnownNat w => Num (BitVector w) where+  (+)         = bvAdd+  (*)         = bvMul+  abs         = bvAbs+  signum      = bvSignum+  fromInteger = bitVector+  negate      = bvNegate++instance KnownNat w => Enum (BitVector w) where+  toEnum   = bitVector+  fromEnum = fromIntegral . bvIntegerU++instance KnownNat w => Ix (BitVector w) where+  range (lo, hi) = bitVector <$> [bvIntegerU lo .. bvIntegerU hi]+  index (lo, hi) bv = index (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)+  inRange (lo, hi) bv = inRange (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)++instance KnownNat w => Bounded (BitVector w) where+  minBound = bitVector (0 :: Integer)+  maxBound = bitVector ((-1) :: Integer)++instance KnownNat w => Arbitrary (BitVector w) where+  arbitrary = choose (minBound, maxBound)++instance KnownNat w => Random (BitVector w) where+  randomR (bvLo, bvHi) gen =+    let (x, gen') = randomR (bvIntegerU bvLo, bvIntegerU bvHi) gen+    in (bitVector x, gen')+  random gen =+    let (x :: Integer, gen') = random gen+    in (bitVector x, gen')++prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String+prettyHex width val = printf format val width+  where numDigits = (width+3) `quot` 4+        format = "0x%." ++ show numDigits ++ "x<%d>"++instance Pretty (BitVector w) where+  -- | Pretty print a bit vector (shows its width)+  pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x
− stack.yaml 
@@ -1,12 +0,0 @@-resolver: lts-12.5--packages:-- .-- submodules/parameterized-utils--extra-deps:-- containers-0.5.11.0-- lens-4.16-- prettyclass-1.0.0.0-- random-1.1-- QuickCheck-2.11.3
+ submodules/parameterized-utils/.travis.yml view
@@ -0,0 +1,103 @@+# This Travis job script has been generated by a script via+#+#   runghc make_travis_yml_2.hs 'parameterized-utils.cabal'+#+# For more information, see https://github.com/haskell-CI/haskell-ci+#+language: c+sudo: false++git:+  submodules: false  # whether to recursively clone submodules++cache:+  directories:+    - $HOME/.cabal/packages+    - $HOME/.cabal/store++before_cache:+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log+  # remove files that are regenerated by 'cabal update'+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.*+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx++  - rm -rfv $HOME/.cabal/packages/head.hackage++matrix:+  include:+    - compiler: "ghc-8.4.3"+    # env: TEST=--disable-tests BENCH=--disable-benchmarks+      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-2.2,ghc-8.4.3], sources: [hvr-ghc]}}++before_install:+  - HC=${CC}+  - HCPKG=${HC/ghc/ghc-pkg}+  - unset CC+  - ROOTDIR=$(pwd)+  - mkdir -p $HOME/.local/bin+  - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH"+  - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))+  - echo $HCNUMVER++install:+  - cabal --version+  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"+  - BENCH=${BENCH---enable-benchmarks}+  - TEST=${TEST---enable-tests}+  - HADDOCK=${HADDOCK-true}+  - UNCONSTRAINED=${UNCONSTRAINED-true}+  - NOINSTALLEDCONSTRAINTS=${NOINSTALLEDCONSTRAINTS-false}+  - GHCHEAD=${GHCHEAD-false}+  - travis_retry cabal update -v+  - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config"+  - rm -fv cabal.project cabal.project.local+  - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$'+  - "printf 'packages: \".\"\\n' > cabal.project"+  - touch cabal.project.local+  - "if ! $NOINSTALLEDCONSTRAINTS; then for pkg in $($HCPKG list --simple-output); do echo $pkg  | grep -vw -- parameterized-utils | sed 's/^/constraints: /' | sed 's/-[^-]*$/ installed/' >> cabal.project.local; done; fi"+  - cat cabal.project || true+  - cat cabal.project.local || true+  - if [ -f "./configure.ac" ]; then+      (cd "." && autoreconf -i);+    fi+  - rm -f cabal.project.freeze+  - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all+  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks --project-file="cabal.project" --dep -j2 all+  - rm -rf .ghc.environment.* "."/dist+  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)++# Here starts the actual work to be performed for the package under test;+# any command which exits with a non-zero exit code causes the build to fail.+script:+  # test that source-distributions can be generated+  - (cd "." && cabal sdist)+  - mv "."/dist/parameterized-utils-*.tar.gz ${DISTDIR}/+  - cd ${DISTDIR} || false+  - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \;+  - "printf 'packages: parameterized-utils-*/*.cabal\\n' > cabal.project"+  - touch cabal.project.local+  - "if ! $NOINSTALLEDCONSTRAINTS; then for pkg in $($HCPKG list --simple-output); do echo $pkg  | grep -vw -- parameterized-utils | sed 's/^/constraints: /' | sed 's/-[^-]*$/ installed/' >> cabal.project.local; done; fi"+  - cat cabal.project || true+  - cat cabal.project.local || true+  # this builds all libraries and executables (without tests/benchmarks)+  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks all++  # build & run tests, build benchmarks+  - cabal new-build -w ${HC} ${TEST} ${BENCH} all+  - if [ "x$TEST" = "x--enable-tests" ]; then cabal new-test -w ${HC} ${TEST} ${BENCH} all; fi++  # cabal check+  - (cd parameterized-utils-* && cabal check)++  # haddock+  - rm -rf ./dist-newstyle+  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi++  # Build without installed constraints for packages in global-db+  - if $UNCONSTRAINED; then rm -f cabal.project.local; echo cabal new-build -w ${HC} --disable-tests --disable-benchmarks all; else echo "Not building without installed constraints"; fi++# REGENDATA ["parameterized-utils.cabal"]+# EOF
submodules/parameterized-utils/parameterized-utils.cabal view
@@ -1,5 +1,5 @@ Name:          parameterized-utils-Version:       1.0.0+Version:       1.0.8 Author:        Galois Inc. Maintainer:    jhendrix@galois.com Build-type:    Simple@@ -14,6 +14,7 @@   intended for things like expression libraries where one wishes   to leverage the Haskell type-checker to improve type-safety by encoding   the object language type system into data kinds.+tested-with: GHC==8.4.3, GHC==8.6.1  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -30,8 +31,9 @@  library   build-depends:-    base >= 4.7 && < 4.12,+    base >= 4.7 && < 4.13,     th-abstraction >=0.1 && <0.3,+    constraints >= 0.10 && < 0.11,     containers,     deepseq,     ghc-prim,@@ -48,11 +50,14 @@   exposed-modules:     Data.Parameterized     Data.Parameterized.Classes+    Data.Parameterized.ClassesC+    Data.Parameterized.Compose     Data.Parameterized.Context     Data.Parameterized.Context.Safe     Data.Parameterized.Context.Unsafe     Data.Parameterized.Ctx     Data.Parameterized.Ctx.Proofs+    Data.Parameterized.DecidableEq     Data.Parameterized.HashTable     Data.Parameterized.List     Data.Parameterized.Map@@ -60,13 +65,16 @@     Data.Parameterized.Nonce     Data.Parameterized.Nonce.Transformers     Data.Parameterized.Nonce.Unsafe+    Data.Parameterized.Pair+    Data.Parameterized.Peano     Data.Parameterized.Some     Data.Parameterized.SymbolRepr-    Data.Parameterized.Pair     Data.Parameterized.TH.GADT     Data.Parameterized.TraversableF     Data.Parameterized.TraversableFC     Data.Parameterized.Utils.BinTree+    Data.Parameterized.Utils.Endian+    Data.Parameterized.Vector    ghc-options: -Wall @@ -84,6 +92,7 @@   other-modules:     Test.Context     Test.NatRepr+    Test.Vector    build-depends:     base,@@ -94,7 +103,7 @@     mtl,     parameterized-utils,     tasty,-    tasty-ant-xml,+    tasty-ant-xml >= 1.1.0,     tasty-hunit,     tasty-quickcheck >= 0.8.1,     QuickCheck >= 2.7
submodules/parameterized-utils/src/Data/Parameterized/Classes.hs view
@@ -37,6 +37,7 @@   , orderingF_refl   , toOrdering   , fromOrdering+  , ordFCompose     -- * Typeclass generalizations   , ShowF(..)   , showsF@@ -55,11 +56,14 @@   ) where  import Data.Functor.Const+import Data.Functor.Compose (Compose(..)) import Data.Hashable import Data.Maybe (isJust) import Data.Proxy import Data.Type.Equality as Equality +import Data.Parameterized.Compose ()+ -- We define these type alias here to avoid importing Control.Lens -- modules, as this apparently causes problems with the safe Hasekll -- checking.@@ -193,6 +197,23 @@             -> (a ~ b => OrderingF c d)             -> OrderingF c d lexCompareF x y = joinOrderingF (compareF x y)++-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated+-- for the \"inner\" functor. The type-level evidence of equality is deduced+-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.+ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y.+                (forall w z. f w -> f z -> OrderingF w z)+            -> Compose f g x+            -> Compose f g y+            -> OrderingF x y+ordFCompose ordF_ (Compose x) (Compose y) =+  case ordF_ x y of+    LTF -> LTF+    GTF -> GTF+    EQF -> EQF++instance OrdF f => OrdF (Compose f g) where+  compareF x y = ordFCompose compareF x y  ------------------------------------------------------------------------ -- ShowF
+ submodules/parameterized-utils/src/Data/Parameterized/ClassesC.hs view
@@ -0,0 +1,52 @@+{-|+Copyright        : (c) Galois, Inc 2014-2015+Maintainer       : Langston Barrett <langston@galois.com>++This module declares classes for working with types with the kind+@(k -> *) -> *@ for any kind @k@.++These classes generally require type-level evidence for operations+on their subterms, but don't actually provide it themselves (because+their types are not themselves parameterized, unlike those in+"Data.Parameterized.TraverableFC").++Note that there is still some ambiguity around naming conventions, see+<https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.+-}++{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.ClassesC+  ( TestEqualityC(..)+  , OrdC(..)+  ) where++import Data.Type.Equality ((:~:)(..))+import Data.Maybe (isJust)+import Data.Parameterized.Classes (OrderingF, toOrdering)+import Data.Parameterized.Some (Some(..))++class TestEqualityC (t :: (k -> *) -> *) where+  testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))+                -> t f+                -> t f+                -> Bool++class TestEqualityC t => OrdC (t :: (k -> *) -> *) where+  compareC :: (forall x y. f x -> g y -> OrderingF x y)+           -> t f+           -> t g+           -> Ordering++-- | This instance demonstrates where the above class is useful: namely, in+-- types with existential quantification.+instance TestEqualityC Some where+  testEqualityC subterms (Some someone) (Some something) =+    isJust (subterms someone something)++instance OrdC Some where+  compareC subterms (Some someone) (Some something) =+    toOrdering (subterms someone something)
+ submodules/parameterized-utils/src/Data/Parameterized/Compose.hs view
@@ -0,0 +1,45 @@+{-|+Copyright        : (c) Galois, Inc 2014-2018+Maintainer       : Langston Barrett <langston@galois.com++Utilities for working with "Data.Functor.Compose".++NB: This module contains an orphan instance. It will be included in GHC 8.10,+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+-}++{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Safe #-}++module Data.Parameterized.Compose+  ( testEqualityComposeBare+  ) where++import Data.Functor.Compose+import Data.Type.Equality++-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.+--+-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y.+                           (forall w z. f w -> f z -> Maybe (w :~: z))+                        -> Compose f g x+                        -> Compose f g y+                        -> Maybe (x :~: y)+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =+  case (testEquality_ x y :: Maybe (g x :~: g y)) of+    Just Refl -> Just (Refl :: x :~: y)+    Nothing   -> Nothing++testEqualityCompose :: forall (f :: k -> *) (g :: l -> k) x y. (TestEquality f)+                    => Compose f g x+                    -> Compose f g y+                    -> Maybe (x :~: y)+testEqualityCompose = testEqualityComposeBare testEquality++instance (TestEquality f) => TestEquality (Compose f g) where+  testEquality = testEqualityCompose
submodules/parameterized-utils/src/Data/Parameterized/Context.hs view
@@ -33,50 +33,63 @@ module Data.Parameterized.Context  ( #ifdef UNSAFE_OPS-   module Data.Parameterized.Context.Unsafe+    module Data.Parameterized.Context.Unsafe #else-   module Data.Parameterized.Context.Safe+    module Data.Parameterized.Context.Safe #endif- , singleton- , toVector- , pattern (:>)- , pattern Empty- , decompose- , Data.Parameterized.Context.null- , Data.Parameterized.Context.init- , Data.Parameterized.Context.last- , Data.Parameterized.Context.view- , forIndexM- , generateSome- , generateSomeM- , fromList-   -- * Context extension and embedding utilities- , CtxEmbedding(..)- , ExtendContext(..)- , ExtendContext'(..)- , ApplyEmbedding(..)- , ApplyEmbedding'(..)- , identityEmbedding- , extendEmbeddingRightDiff- , extendEmbeddingRight- , extendEmbeddingBoth- , ctxeSize- , ctxeAssignment+  , singleton+  , toVector+  , pattern (:>)+  , pattern Empty+  , decompose+  , Data.Parameterized.Context.null+  , Data.Parameterized.Context.init+  , Data.Parameterized.Context.last+  , Data.Parameterized.Context.view+  , Data.Parameterized.Context.take+  , forIndexM+  , generateSome+  , generateSomeM+  , fromList+  , traverseAndCollect -   -- * Static indexing and lenses for assignments- , Idx- , field- , natIndex- , natIndexProxy-   -- * Currying and uncurrying for assignments- , CurryAssignment- , CurryAssignmentClass(..)- ) where+    -- * Context extension and embedding utilities+  , CtxEmbedding(..)+  , ExtendContext(..)+  , ExtendContext'(..)+  , ApplyEmbedding(..)+  , ApplyEmbedding'(..)+  , identityEmbedding+  , extendEmbeddingRightDiff+  , extendEmbeddingRight+  , extendEmbeddingBoth+  , appendEmbedding+  , ctxeSize+  , ctxeAssignment +    -- * Static indexing and lenses for assignments+  , Idx+  , field+  , natIndex+  , natIndexProxy+    -- * Currying and uncurrying for assignments+  , CurryAssignment+  , CurryAssignmentClass(..)+    -- * Size and Index values+  , size1, size2, size3, size4, size5, size6+  , i1of2, i2of2+  , i1of3, i2of3, i3of3+  , i1of4, i2of4, i3of4, i4of4+  , i1of5, i2of5, i3of5, i4of5, i5of5+  , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6+  ) where++import           Control.Applicative (liftA2) import           Control.Lens hiding (Index, (:>), Empty) import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import           GHC.TypeLits (Nat, type (-))+import           Data.Monoid ((<>))  import           Data.Parameterized.Classes import           Data.Parameterized.Some@@ -152,7 +165,7 @@ #endif  ----------------------------------------------------------------------------------- | Views+-- Views  -- | Return true if assignment is empty. null :: Assignment f ctx -> Bool@@ -181,10 +194,15 @@ view :: forall f ctx . Assignment f ctx -> AssignView f ctx view = viewAssign +take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx+take sz sz' asgn =+  let diff = appendDiff sz' in+  generate sz (\i -> asgn ! extendIndex' diff i)+ ----------------------------------------------------------------------------------- | Context embedding.+-- Context embedding. --- This datastructure contains a proof that the first context is+-- | This datastructure contains a proof that the first context is -- embeddable in the second.  This is useful if we want to add extend -- an existing term under a larger context. @@ -248,6 +266,11 @@ extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) extendEmbeddingRight = extendEmbeddingRightDiff knownDiff +appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')+appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))+  where+  diff = appendDiff sz'+ extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))   where@@ -339,3 +362,102 @@   where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)         go prev [] = Some prev         go prev (Some g:next) = (go $! prev `extend` g) next+++newtype Collector m w a = Collector { runCollector :: m w }+instance Functor (Collector m w) where+  fmap _ (Collector x) = Collector x+instance (Applicative m, Monoid w) => Applicative (Collector m w) where+  pure _ = Collector (pure mempty)+  Collector x <*> Collector y = Collector (liftA2 (<>) x y)++-- | Visit each of the elements in an @Assignment@ in order+--   from left to right and collect the results using the provided @Monoid@.+traverseAndCollect ::+  (Monoid w, Applicative m) =>+  (forall tp. Index ctx tp -> f tp -> m w) ->+  Assignment f ctx ->+  m w+traverseAndCollect f =+  runCollector . traverseWithIndex (\i x -> Collector (f i x))++--------------------------------------------------------------------------------+-- Size and Index values++size1 :: Size (EmptyCtx ::> a)+size1 = incSize zeroSize++size2 :: Size (EmptyCtx ::> a ::> b)+size2 = incSize size1++size3 :: Size (EmptyCtx ::> a ::> b ::> c)+size3 = incSize size2++size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)+size4 = incSize size3++size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)+size5 = incSize size4++size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)+size6 = incSize size5++i1of2 :: Index (EmptyCtx ::> a ::> b) a+i1of2 = skipIndex baseIndex++i2of2 :: Index (EmptyCtx ::> a ::> b) b+i2of2 = nextIndex size1++i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a+i1of3 = skipIndex i1of2++i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b+i2of3 = skipIndex i2of2++i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c+i3of3 = nextIndex size2++i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a+i1of4 = skipIndex i1of3++i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b+i2of4 = skipIndex i2of3++i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c+i3of4 = skipIndex i3of3++i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d+i4of4 = nextIndex size3++i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a+i1of5 = skipIndex i1of4++i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b+i2of5 = skipIndex i2of4++i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c+i3of5 = skipIndex i3of4++i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d+i4of5 = skipIndex i4of4++i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e+i5of5 = nextIndex size4++i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a+i1of6 = skipIndex i1of5++i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b+i2of6 = skipIndex i2of5++i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c+i3of6 = skipIndex i3of5++i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d+i4of6 = skipIndex i4of5++i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e+i5of6 = skipIndex i5of5++i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f+i6of6 = nextIndex size5
submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs view
@@ -60,6 +60,7 @@   , Diff   , noDiff   , extendRight+  , appendDiff   , DiffView(..)   , viewDiff   , KnownDiff(..)@@ -120,7 +121,7 @@ ------------------------------------------------------------------------ -- Size --- | A  indexed singleton type representing the size of a context.+-- | An indexed singleton type representing the size of a context. data Size (ctx :: Ctx k) where   SizeZero :: Size 'EmptyCtx   SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)@@ -185,6 +186,10 @@ -- | Extend the difference to a sub-context of the right side. extendRight :: Diff l r -> Diff l (r '::> tp) extendRight diff = DiffThere diff++appendDiff :: Size r -> Diff l (l <+> r)+appendDiff SizeZero = DiffHere+appendDiff (SizeSucc sz) = DiffThere (appendDiff sz)  composeDiff :: Diff a b -> Diff b c -> Diff a c composeDiff x DiffHere = x
submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs view
@@ -32,6 +32,7 @@   , Diff   , noDiff   , extendRight+  , appendDiff   , DiffView(..)   , viewDiff   , KnownDiff(..)@@ -97,10 +98,14 @@ -- Size  -- | Represents the size of a context.-newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int }+newtype Size (ctx :: Ctx k) = Size Int  type role Size nominal +-- | Convert a context size to an 'Int'.+sizeInt :: Size ctx -> Int+sizeInt (Size n) = n+ -- | The size of an empty context. zeroSize :: Size 'EmptyCtx zeroSize = Size 0@@ -143,6 +148,8 @@ newtype Diff (l :: Ctx k) (r :: Ctx k)       = Diff { _contextExtSize :: Int } +type role Diff nominal nominal+ -- | The identity difference. noDiff :: Diff l l noDiff = Diff 0@@ -150,6 +157,9 @@ -- | Extend the difference to a sub-context of the right side. extendRight :: Diff l r -> Diff l (r '::> tp) extendRight (Diff i) = Diff (i+1)++appendDiff :: Size r -> Diff l (l <+> r)+appendDiff (Size r) = Diff r  instance Cat.Category Diff where   id = Diff 0
+ submodules/parameterized-utils/src/Data/Parameterized/DecidableEq.hs view
@@ -0,0 +1,37 @@+{-|+Copyright        : (c) Galois, Inc 2014-2018+Maintainer       : Langston Barrett <langston@galois.com>++This defines a class @DecidableEq@, which represents decidable equality on a+type family.++This is different from GHC's @TestEquality@ in that it provides evidence+of non-equality. In fact, it is a superclass of @TestEquality@.+-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Safe #-}+module Data.Parameterized.DecidableEq+  ( DecidableEq(..)+  ) where++import Data.Void (Void)+import Data.Type.Equality ((:~:))++-- | Decidable equality.+class DecidableEq f where+  decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)++-- TODO: instances for sums, products of types with decidable equality++-- import Data.Type.Equality ((:~:), TestEquality(..))+-- instance (DecidableEq f) => TestEquality f where+--   testEquality a b =+--     case decEq a b of+--       Left  prf -> Just prf+--       Right _   -> Nothing
submodules/parameterized-utils/src/Data/Parameterized/Map.hs view
@@ -45,13 +45,21 @@   , fromKeys   , fromKeysM    -- * Filter+  , filter+  , filterWithKey   , filterGt   , filterLt     -- * Folds+  , foldlWithKey+  , foldlWithKey'   , foldrWithKey+  , foldrWithKey'+  , foldMapWithKey     -- * Traversal   , map+  , mapWithKey   , mapMaybe+  , mapMaybeWithKey   , traverseWithKey   , traverseWithKey_     -- * Complex interface.@@ -65,18 +73,18 @@   , Pair(..)   ) where -import Control.Applicative hiding (empty)-import Control.Lens (Traversal', Lens')-import Control.Monad.Identity-import Data.List (intercalate, foldl')-import Data.Maybe ()-import Data.Kind(Type)+import           Control.Applicative hiding (empty)+import           Control.Lens (Traversal', Lens')+import           Control.Monad.Identity+import           Data.Kind (Type)+import           Data.List (intercalate, foldl')+import           Data.Monoid -import Data.Parameterized.Classes-import Data.Parameterized.Some-import Data.Parameterized.Pair ( Pair(..) )-import Data.Parameterized.TraversableF-import Data.Parameterized.Utils.BinTree+import           Data.Parameterized.Classes+import           Data.Parameterized.Some+import           Data.Parameterized.Pair ( Pair(..) )+import           Data.Parameterized.TraversableF+import           Data.Parameterized.Utils.BinTree   ( MaybeS(..)   , fromMaybeS   , Updated(..)@@ -91,9 +99,9 @@ import qualified Data.Parameterized.Utils.BinTree as Bin  #if MIN_VERSION_base(4,8,0)-import Prelude hiding (lookup, map, traverse, null)+import           Prelude hiding (filter, lookup, map, traverse, null) #else-import Prelude hiding (lookup, map, null)+import           Prelude hiding (filter, lookup, map, null) #endif  ------------------------------------------------------------------------@@ -106,7 +114,7 @@ ------------------------------------------------------------------------ -- MapF --- | A map from parameterized keys to values with the same paramter type.+-- | A map from parameterized keys to values with the same parameter type. data MapF (k :: v -> Type) (a :: v -> Type) where   Bin :: {-# UNPACK #-}          !Size -- Number of elements in tree.@@ -165,18 +173,30 @@  #-} #endif ++-- | Apply function to all elements in map.+mapWithKey+  :: (forall tp . ktp tp -> f tp -> g tp)+  -> MapF ktp f+  -> MapF ktp g+mapWithKey _ Tip = Tip+mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r)+ -- | Modify elements in a map map :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g-map _ Tip = Tip-map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r)+map f = mapWithKey (\_ x -> f x) --- | Run partial map over elements.+-- | Map keys and elements and collect `Just` results.+mapMaybeWithKey :: (forall tp . k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k g+mapMaybeWithKey _ Tip = Tip+mapMaybeWithKey f (Bin _ k x l r) =+  case f k x of+    Just y -> Bin.link (Pair k y) (mapMaybeWithKey f l) (mapMaybeWithKey f r)+    Nothing -> Bin.merge (mapMaybeWithKey f l) (mapMaybeWithKey f r)++-- | Map elements and collect `Just` results. mapMaybe :: (forall tp . f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g-mapMaybe _ Tip = Tip-mapMaybe f (Bin _ k x l r) =-  case f x of-    Just y -> Bin.link (Pair k y) (mapMaybe f l) (mapMaybe f r)-    Nothing -> Bin.merge (mapMaybe f l) (mapMaybe f r)+mapMaybe f = mapMaybeWithKey (\_ x -> f x)  -- | Traverse elements in a map traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)@@ -270,13 +290,43 @@ elems :: MapF k a -> [Some a] elems = foldrF (\e l -> Some e : l) [] --- | Perform a fold with the key also provided.+-- | Perform a left fold with the key also provided.+foldlWithKey :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b+foldlWithKey _ z Tip = z+foldlWithKey f z (Bin _ kx x l r) =+  let lz = foldlWithKey f z l+      kz = f lz kx x+   in foldlWithKey f kz r++-- | Perform a strict left fold with the key also provided.+foldlWithKey' :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b+foldlWithKey' _ z Tip = z+foldlWithKey' f z (Bin _ kx x l r) =+  let lz = foldlWithKey f z l+      kz = seq lz $ f lz kx x+   in seq kz $ foldlWithKey f kz r++-- | Perform a right fold with the key also provided. foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b-foldrWithKey f z = go z-  where-    go z' Tip = z'-    go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l+foldrWithKey _ z Tip = z+foldrWithKey f z (Bin _ kx x l r) =+  let rz = foldrWithKey f z r+      kz = f kx x rz+   in foldrWithKey f kz l +-- | Perform a strict right fold with the key also provided.+foldrWithKey' :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b+foldrWithKey' _ z Tip = z+foldrWithKey' f z (Bin _ kx x l r) =+  let rz = foldrWithKey f z r+      kz = seq rz $ f kx x rz+   in seq kz $ foldrWithKey f kz l++-- | Fold the keys and values using the given monoid.+foldMapWithKey :: Monoid m => (forall s . k s -> a s -> m) -> MapF k a -> m+foldMapWithKey _ Tip = mempty+foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r+ showMap :: (forall tp . ktp tp -> String)         -> (forall tp . rtp tp -> String)         -> MapF ktp rtp@@ -286,6 +336,17 @@  ------------------------------------------------------------------------ -- filter++-- | Return entries with values that satisfy predicate.+filter :: (forall tp . f tp -> Bool) -> MapF k f -> MapF k f+filter f = filterWithKey (\_ v -> f v)++-- | Return key-value pairs that satisfy predicate.+filterWithKey :: (forall tp . k tp -> f tp -> Bool) -> MapF k f -> MapF k f+filterWithKey _ Tip = Tip+filterWithKey f (Bin _ k x l r)+  | f k x     = Bin.link (Pair k x) (filterWithKey f l) (filterWithKey f r)+  | otherwise = Bin.merge (filterWithKey f l) (filterWithKey f r)  compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x)
submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs view
@@ -1,5 +1,5 @@ {-|-Copyright        : (c) Galois, Inc 2014-2015+Copyright        : (c) Galois, Inc 2014-2018 Maintainer       : Joe Hendrix <jhendrix@galois.com>  This defines a type 'NatRepr' for representing a type-level natural@@ -8,14 +8,17 @@ @n@.  This can be used to help use type-level variables on code with data dependendent types. -The 'TestEquality' instance for 'NatRepr' is implemented using-'unsafeCoerce', as is the `isZeroNat` function. This should be-typesafe because we maintain the invariant that the integer value+The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'+are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This+should be typesafe because we maintain the invariant that the integer value contained in a NatRepr value matches its static type. -} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -24,19 +27,25 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} #if MIN_VERSION_base(4,9,0) {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} #endif+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif module Data.Parameterized.NatRepr   ( NatRepr   , natValue+  , intValue   , knownNat   , withKnownNat   , IsZeroNat(..)   , isZeroNat+  , isZeroOrGT1   , NatComparison(..)   , compareNat   , decNat@@ -49,11 +58,18 @@   , withDivModNat   , natMultiply   , someNat+  , mkNatRepr   , maxNat   , natRec+  , natRecStrong+  , natRecBounded   , natForEach+  , natFromZero   , NatCases(..)   , testNatCases+    -- * Strict order+  , lessThanIrreflexive+  , lessThanAsymmetric     -- * Bitvector utilities   , widthVal   , minUnsigned@@ -66,6 +82,7 @@   , signedClamp     -- * LeqProof   , LeqProof(..)+  , decideLeq   , testLeq   , testStrictLeq   , leqRefl@@ -98,6 +115,7 @@   , withSubMulDistribRight   , mulCancelR   , mul2Plus+  , lemmaMul     -- * Re-exports typelists basics --  , NatK   , type (+)@@ -107,20 +125,25 @@   , Equality.TestEquality(..)   , (Equality.:~:)(..)   , Data.Parameterized.Some.Some+    -- * Backdoor, no touchy+  , activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing   ) where -import Data.Bits ((.&.))+import Data.Bits ((.&.), bit) import Data.Hashable import Data.Proxy as Proxy import Data.Type.Equality as Equality-import GHC.TypeLits as TypeLits+import Data.Void as Void+import Numeric.Natural+import GHC.TypeNats as TypeNats import Unsafe.Coerce  import Data.Parameterized.Classes+import Data.Parameterized.DecidableEq import Data.Parameterized.Some -maxInt :: Integer-maxInt = toInteger (maxBound :: Int)+maxInt :: Natural+maxInt = fromIntegral (maxBound :: Int)  ------------------------------------------------------------------------ -- Nat@@ -129,15 +152,27 @@ -- -- This can be used for performing dynamic checks on a type-level natural -- numbers.-newtype NatRepr (n::Nat) = NatRepr { natValue :: Integer-                                     -- ^ The underlying integer value of the number.+newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural+                                     -- ^ The underlying natural value of the number.                                    }   deriving (Hashable) +type role NatRepr nominal++intValue :: NatRepr n -> Integer+intValue n = toInteger (natValue n)+{-# INLINE intValue #-}++-- | If you are not 110% sure what the consequences of using this are and+--   how to use it, don't.+activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing :: ((Natural -> NatRepr n) -> a) -> a+activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing k = k NatRepr+{-# INLINE activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing #-}+ -- | Return the value of the nat representation. widthVal :: NatRepr n -> Int-widthVal (NatRepr i) | i < maxInt = fromInteger i-                     | otherwise = error "Width is too large."+widthVal (NatRepr i) | i <= maxInt = fromIntegral i+                     | otherwise   = error ("Width is too large: " ++ show i)  instance Eq (NatRepr m) where   _ == _ = True@@ -147,20 +182,26 @@     | m == n = Just (unsafeCoerce Refl)     | otherwise = Nothing +instance DecidableEq NatRepr where+  decEq (NatRepr m) (NatRepr n)+    | m == n    = Left $ unsafeCoerce Refl+    | otherwise = Right $+        \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"+ -- | Result of comparing two numbers. data NatComparison m n where   -- First number is less than second.-  NatLT :: !(NatRepr y) -> NatComparison x (x+(y+1))+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))   NatEQ :: NatComparison x x   -- First number is greater than second.-  NatGT :: !(NatRepr y) -> NatComparison (x+(y+1)) x+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x  compareNat :: NatRepr m -> NatRepr n -> NatComparison m n compareNat m n =   case compare (natValue m) (natValue n) of-    LT -> unsafeCoerce $ NatLT (NatRepr (natValue n - natValue m - 1))-    EQ -> unsafeCoerce $ NatEQ-    GT -> unsafeCoerce $ NatGT (NatRepr (natValue m - natValue n - 1))+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))+    EQ -> unsafeCoerce  NatEQ+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))  instance OrdF NatRepr where   compareF x y =@@ -187,14 +228,12 @@ instance (KnownNat n) => KnownRepr NatRepr n where   knownRepr = knownNat -{-# DEPRECATED withKnownNat "This function is potentially unsafe and is schedueled to be removed." #-} withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r withKnownNat (NatRepr nVal) v =   case someNatVal nVal of-    Just (SomeNat (Proxy :: Proxy n')) ->-      case unsafeCoerce (Refl :: 0 :~: 0) :: n :~: n' of+    SomeNat (Proxy :: Proxy n') ->+      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of         Refl -> v-    Nothing -> error "withKnownNat: inner value in NatRepr is not a natural"  data IsZeroNat n where   ZeroNat    :: IsZeroNat 0@@ -204,11 +243,35 @@ isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat +-- | Every nat is either zero or >= 1.+isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)+isZeroOrGT1 n =+  case isZeroNat n of+    ZeroNat    -> Left Refl+    NonZeroNat -> Right $+      -- We have n = m + 1 for some m.+      let+        -- | x <= x + 1+        leqSucc:: forall x. LeqProof x (x+1)+        leqSucc = leqAdd2 (LeqProof :: LeqProof x x) (LeqProof :: LeqProof 0 1)+        leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y+        leqPlus fx =+          case (plusComm fx (knownNat @1) :: x + 1 :~: 1 + x)    of { Refl ->+          case (plusMinusCancel (knownNat @1) fx :: 1+x-x :~: 1) of { Refl ->+          case (LeqProof :: LeqProof (x+1) y)                    of { LeqProof ->+          case (LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ->+            leqTrans (LeqProof :: LeqProof 1 (y-x))+                     (leqSub (LeqProof :: LeqProof y y)+                             (leqTrans (leqSucc :: LeqProof x (x+1))+                                       (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)+          }}}}+      in leqPlus (predNat n)+ -- | Decrement a @NatRepr@ decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1) decNat (NatRepr i) = NatRepr (i-1) --- | Get the predicessor of a nat+-- | Get the predecessor of a nat predNat :: NatRepr (n+1) -> NatRepr n predNat (NatRepr i) = NatRepr (i-1) @@ -254,15 +317,15 @@  -- | Return maximum unsigned value for bitvector with given width. maxUnsigned :: NatRepr w -> Integer-maxUnsigned w = 2^(natValue w) - 1+maxUnsigned w = bit (widthVal w) - 1  -- | Return minimum value for bitvector in 2s complement with given width. minSigned :: (1 <= w) => NatRepr w -> Integer-minSigned w = negate (2^(natValue w - 1))+minSigned w = negate (bit (widthVal w - 1))  -- | Return maximum value for bitvector in 2s complement with given width. maxSigned :: (1 <= w) => NatRepr w -> Integer-maxSigned w = 2^(natValue w - 1) - 1+maxSigned w = bit (widthVal w - 1) - 1  -- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@. toUnsigned :: NatRepr w -> Integer -> Integer@@ -272,7 +335,7 @@ -- signed number in two's complement notation and returns that value. toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer toSigned w i0-    | i > maxSigned w = i - 2^(natValue w)+    | i > maxSigned w = i - bit (widthVal w)     | otherwise       = i   where i = i0 .&. maxUnsigned w @@ -295,10 +358,16 @@ ------------------------------------------------------------------------ -- Some NatRepr -someNat :: Integer -> Maybe (Some NatRepr)-someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n)))-          | otherwise = Nothing+-- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@+--   if the given value is negative.+someNat :: Integral a => a -> Maybe (Some NatRepr)+someNat x | x >= 0 = Just . Some . NatRepr $! fromIntegral x+someNat _ = Nothing +-- | Turn a @Natural@ into the corresponding @NatRepr@+mkNatRepr :: Natural -> Some NatRepr+mkNatRepr n = Some (NatRepr n)+ -- | Return the maximum of two nat representations. maxNat :: NatRepr m -> NatRepr n -> Some NatRepr maxNat x y@@ -345,8 +414,6 @@   case unsafeCoerce (Refl :: 0 :~: 0) of     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f -- ------------------------------------------------------------------------ -- LeqProof @@ -355,6 +422,13 @@ data LeqProof m n where   LeqProof :: (m <= n) => LeqProof m n +-- | (<=) is a decidable relation on nats.+decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)+decideLeq (NatRepr m) (NatRepr n)+  | m <= n    = Left $ unsafeCoerce (LeqProof :: LeqProof 0 0)+  | otherwise = Right $+      \x -> seq x $ error "Impossible [decidable <= on NatRepr]"+ testStrictLeq :: forall m n                . (m <= n)               => NatRepr m@@ -384,6 +458,31 @@     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0)) {-# NOINLINE testNatCases #-} +-- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.+lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void+lessThanIrreflexive a prf =+  let prf1 :: LeqProof (1 + a - a) (a - a)+      prf1 = leqSub2 prf (LeqProof :: LeqProof a a)+      prf2 :: 1 + a - a :~: 1+      prf2 = plusMinusCancel (knownNat @1) a+      prf3 :: a - a :~: 0+      prf3 = plusMinusCancel (knownNat @0) a+      prf4 :: LeqProof 1 0+      prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }+  in case prf4 of {}++-- | The strict order on the naturals is irreflexive.+lessThanAsymmetric :: forall m f n+                    . LeqProof (n+1) m+                   -> LeqProof (m+1) n+                   -> f n+                   -> Void+lessThanAsymmetric nLTm mLTn n =+  case plusComm n (knownNat @1) :: n + 1 :~: 1 + n of { Refl ->+  case leqAdd (LeqProof :: LeqProof m m) (knownNat @1) :: LeqProof m (m+1) of+    LeqProof -> lessThanIrreflexive n $ leqTrans (leqTrans nLTm LeqProof) mLTn+  }+ -- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@. testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n) testLeq (NatRepr m) (NatRepr n)@@ -395,7 +494,6 @@ leqRefl :: forall f n . f n -> LeqProof n n leqRefl _ = LeqProof - -- | Apply transitivity to LeqProof leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)@@ -509,19 +607,84 @@            -> [a] natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f) +-- | Apply a function to each element in a range starting at zero;+-- return the list of values obtained.+natFromZero :: forall h a+            . NatRepr h+           -> (forall n. (n <= h) => NatRepr n -> a)+           -> [a]+natFromZero = natForEach (knownNat @0)+ -- | Recursor for natural numbeers.-natRec :: forall m f-       .  NatRepr m-       -> f 0+natRec :: forall p f+       .  NatRepr p+       -> f 0 {- ^ base case -}        -> (forall n. NatRepr n -> f n -> f (n + 1))-       -> f m-natRec n f0 ih = go n-  where-    go :: forall n'. NatRepr n' -> f n'-    go n' = case isZeroNat n' of-              ZeroNat    -> f0-              NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')+       -> f p+natRec n base ind =+  case isZeroNat n of+    ZeroNat    -> base+    NonZeroNat -> let n' = predNat n+                  in ind n' (natRec n' base ind) +-- | Strong induction variant of the recursor.+natRecStrong :: forall p f+             .  NatRepr p+             -> f 0 {- ^ base case -}+             -> (forall n.+                  NatRepr n ->+                  (forall m. (m <= n) => NatRepr m -> f m) ->+                  f (n + 1)) {- ^ inductive step -}+             -> f p+natRecStrong p base ind = natRecStrong' base ind p+  where -- We can't use use "flip" or some other basic combinator+        -- because type variables can't be instantiated to contain "forall"s.+        natRecStrong' :: forall p' f'+                      .  f' 0 {- ^ base case -}+                      -> (forall n.+                            NatRepr n ->+                            (forall m. (m <= n) => NatRepr m -> f' m) ->+                            f' (n + 1)) {- ^ inductive step -}+                      -> NatRepr p'+                      -> f' p'+        natRecStrong' base' ind' n =+          case isZeroNat n of+            ZeroNat    -> base'+            NonZeroNat -> ind' (predNat n) (natRecStrong' base' ind')++-- | Bounded recursor for natural numbers.+--+-- If you can prove:+-- - Base case: f 0+-- - Inductive step: if n <= h and (f n) then (f (n + 1))+-- You can conclude: for all n <= h, (f (n + 1)).+natRecBounded :: forall m h f. (m <= h)+              => NatRepr m+              -> NatRepr h+              -> f 0+              -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))+              -> f (m + 1)+natRecBounded m h base indH =+  case isZeroOrGT1 m of+    Left Refl      -> indH (knownNat @0) base+    Right LeqProof ->+      case decideLeq m h of+        Left LeqProof {- :: m <= h -} ->+          let -- Since m is non-zero, it is n + 1 for some n.+              lemma :: LeqProof (m-1) h+              lemma = leqSub (LeqProof :: LeqProof m h) (LeqProof :: LeqProof 1 m)+          in indH m $+            case lemma of { LeqProof ->+            case minusPlusCancel m (knownNat @1) of { Refl ->+              natRecBounded @(m - 1) @h @f (predNat m) h base indH+            }}+        Right f {- :: (m <= h) -> Void -} ->+          absurd $ f (LeqProof :: LeqProof m h)+ mulCancelR ::   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2) mulCancelR _ _ _ = unsafeCoerce Refl++-- | Used in @Vector@+lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)+lemmaMul = unsafeCoerce Refl
submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-}@@ -29,6 +30,7 @@   ( -- * NonceGenerator     NonceGenerator   , freshNonce+  , countNoncesGenerated   , Nonce   , indexValue     -- * Accessing a nonce generator@@ -53,7 +55,7 @@ import Data.Parameterized.Classes import Data.Parameterized.Some -#if MIN_VERSION_base(4,9,0)+#if MIN_VERSION_base(4,9,0) && __GLASGOW_HASKELL__ < 805 import Data.Kind #endif @@ -61,47 +63,53 @@ -- -- The first type parameter @m@ is the monad used for generating names, and -- the second parameter @s@ is used for the counter.-data NonceGenerator (m :: * -> *) (s :: *) = NonceGenerator {+data NonceGenerator (m :: * -> *) (s :: *) where+  STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s+  IONG :: !(IORef Word64) -> NonceGenerator IO s+ #if MIN_VERSION_base(4,9,0) -- We have to make the k explicit in GHC 8.0 to avoid a warning.-    freshNonce :: forall k (tp :: k) . m (Nonce s tp)+freshNonce :: forall m s k (tp :: k) . NonceGenerator m s -> m (Nonce s tp) #else-    freshNonce :: forall (tp :: k) . m (Nonce s tp)+freshNonce :: forall m s (tp :: k) . NonceGenerator m s -> m (Nonce s tp) #endif-  }+freshNonce (IONG r) =+  atomicModifyIORef' r $ \n -> (n+1, Nonce n)+freshNonce (STNG r) = do+  i <- readSTRef r+  writeSTRef r $! i+1+  return $ Nonce i+  -- (Weirdly, there's no atomicModifySTRef'.  Yes, only the IO monad+  -- does concurrency, but the ST monad is part of the IO monad via+  -- stToIO, so there's no guarantee that ST code won't be run in+  -- multiple threads.) +{-# INLINE freshNonce #-}+  -- Inlining is particularly necessary since there's no @Monad m@+  -- constraint on 'freshNonce', so SPECIALIZE doesn't work on it.  In+  -- this case, though, we get specialization for free from inlining.+  -- For instance, a @NonceGenerator IO s@ must be an @IONG@, so the+  -- simplifier eliminates the STNG branch.++-- | The number of nonces generated so far by this generator.  Only+-- really useful for profiling.+countNoncesGenerated :: NonceGenerator m s -> m Integer+countNoncesGenerated (IONG r) = toInteger <$> readIORef r+countNoncesGenerated (STNG r) = toInteger <$> readSTRef r+ -- | Create a new counter. withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r withGlobalSTNonceGenerator f = runST $ do   r <- newSTRef (toEnum 0)-  f $! NonceGenerator {-      freshNonce = do-          i <- readSTRef r-          writeSTRef r $! succ i-          return $! Nonce i-    }+  f $! STNG r  -- | Create a new nonce generator in the ST monad. newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))-newSTNonceGenerator = g <$> newSTRef (toEnum 0)-  where g r = Some $!-          NonceGenerator {-              freshNonce = do-                i <- readSTRef r-                writeSTRef r $! succ i-                return $! Nonce i-            }+newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0)  -- | Create a new nonce generator in the ST monad. newIONonceGenerator :: IO (Some (NonceGenerator IO))-newIONonceGenerator = g <$> newIORef (toEnum 0)-  where g r = Some $!-          NonceGenerator {-              freshNonce = do-                  i <- readIORef r-                  writeIORef r $! succ i-                  return $! Nonce i-            }+newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0)  -- | Run a ST computation with a new nonce generator in the ST monad. withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> (ST t) r) -> ST t r@@ -152,7 +160,4 @@  -- | A nonce generator that uses a globally-defined counter. globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator-globalNonceGenerator =-  NonceGenerator-  { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n))-  }+globalNonceGenerator = IONG globalNonceIORef
+ submodules/parameterized-utils/src/Data/Parameterized/Peano.hs view
@@ -0,0 +1,285 @@+{-|++This defines a type 'Peano' and 'PeanoRepr' for representing a+type-level natural at runtime. These type-level numbers are defined+inductively instead of using GHC.TypeLits.++As a result, type-level computation defined recursively over these+numbers works more smoothly. (For example, see the type-level+function Repeatn below.)++Note: as in NatRepr, the runtime representation of these type-level+natural numbers is an Int.++-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++#if MIN_VERSION_base(4,9,0)+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}+#endif+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif+module Data.Parameterized.Peano+   ( Peano+     , Z , S+     , Plus, Minus, Mul, Le, Lt, Gt, Ge, Max, Min, Repeat+     , plusP, minusP, mulP, maxP, minP, repeatP+     , zeroP, succP, predP++     , KnownPeano+     , withKnownPeano++     , PeanoRepr, peanoValue+     , PeanoView(..), peanoView+     , viewRepr++     , somePeano+     , mkPeanoRepr+     , maxPeano+     , minPeano++     -- * Re-exports+     , TestEquality(..)+     , (:~:)(..)+     , Data.Parameterized.Some.Some++     ) where++import           Data.Parameterized.Classes+import           Data.Parameterized.DecidableEq+import           Data.Parameterized.Some++import           Data.Hashable+import           Data.Constraint+import           Data.Word++import           Unsafe.Coerce(unsafeCoerce)++------------------------------------------------------------------------+-- ** Peano - a unary representation of natural numbers++data Peano = Z | S Peano+-- | Peano zero+type Z = 'Z+-- | Peano successor+type S = 'S++-- Peano numbers are more about *counting* than arithmetic.+-- They are most useful as iteration arguments and list indices+-- However, for completeness, we define a few standard+-- operations.++type family Plus (a :: Peano) (b :: Peano) :: Peano where+  Plus Z     b = b+  Plus (S a) b = S (Plus a b)++type family Minus (a :: Peano) (b :: Peano) :: Peano where+  Minus Z     b     = Z+  Minus (S a) (S b) = Minus a b+  Minus a    Z      = a++type family Mul (a :: Peano) (b :: Peano) :: Peano where+  Mul Z     b = Z+  Mul (S a) b = Plus a (Mul a b)++type family Le  (a :: Peano) (b :: Peano) :: Bool where+  Le  a  a        = 'True+  Le  Z  b        = 'True+  Le  a  Z        = 'False+  Le  (S a) (S b) = Le a b++type family Lt  (a :: Peano) (b :: Peano) :: Bool where+  Lt a b = Le (S a) b++type family Gt  (a :: Peano) (b :: Peano) :: Bool where+  Gt a b = Lt b a++type family Ge  (a :: Peano) (b :: Peano) :: Bool where+  Ge a b = Le b a++type family Max (a :: Peano) (b :: Peano) :: Peano where+  Max Z b = b+  Max a Z = a+  Max (S a) (S b) = S (Max a b)++type family Min (a :: Peano) (b :: Peano) :: Peano where+  Min Z b = Z+  Min a Z = Z+  Min (S a) (S b) = S (Min a b)++-- Apply a constructor 'f' n-times to an argument 's'+type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where+  Repeat Z f s     = s+  Repeat (S m) f s = f (Repeat m f s)+++------------------------------------------------------------------------+-- ** Run time representation of Peano numbers++-- | The run time value, stored as an Word64+-- As these are unary numbers, we don't worry about overflow.+newtype PeanoRepr (n :: Peano) =+  PeanoRepr { peanoValue :: Word64 }++-- n is Phantom in the definition, but we don't want to allow coerce+type role PeanoRepr nominal++----------------------------------------------------------++-- | Because we have optimized the runtime representation,+-- we need to have a "view" that decomposes the representation+-- into the standard form.+data PeanoView (n :: Peano) where+  ZRepr :: PeanoView Z+  SRepr :: PeanoRepr n -> PeanoView (S n)++-- | Test whether a number is Zero or Successor+peanoView :: PeanoRepr n -> PeanoView n+peanoView (PeanoRepr i) =+  if i == 0 then unsafeCoerce ZRepr else unsafeCoerce (SRepr (PeanoRepr (i-1)))++-- | convert the view back to the runtime representation+viewRepr :: PeanoView n -> PeanoRepr n+viewRepr ZRepr     = PeanoRepr 0+viewRepr (SRepr n) = PeanoRepr (peanoValue n + 1)++----------------------------------------------------------++instance Hashable (PeanoRepr n) where+  hashWithSalt i (PeanoRepr x) = hashWithSalt i x++instance Eq (PeanoRepr m) where+  _ == _ = True++instance TestEquality PeanoRepr where+  testEquality (PeanoRepr m) (PeanoRepr n)+    | m == n = Just (unsafeCoerce Refl)+    | otherwise = Nothing++instance DecidableEq PeanoRepr where+  decEq (PeanoRepr m) (PeanoRepr n)+    | m == n    = Left $ unsafeCoerce Refl+    | otherwise = Right $+        \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]"++instance OrdF PeanoRepr where+  compareF (PeanoRepr m) (PeanoRepr n)+    | m < n     = unsafeCoerce LTF+    | m == n    = unsafeCoerce EQF+    | otherwise = unsafeCoerce GTF++instance PolyEq (PeanoRepr m) (PeanoRepr n) where+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y++-- Display as digits, not in unary+instance Show (PeanoRepr p) where+  show p = show (peanoValue p)++instance ShowF PeanoRepr++instance HashableF PeanoRepr where+  hashWithSaltF = hashWithSalt++----------------------------------------------------------+-- * Implicit runtime Peano numbers++type KnownPeano = KnownRepr PeanoRepr++instance KnownRepr PeanoRepr Z where+  knownRepr = viewRepr ZRepr+instance (KnownRepr PeanoRepr n) => KnownRepr PeanoRepr (S n) where+  knownRepr = viewRepr (SRepr knownRepr)++newtype DI a = Don'tInstantiate (KnownPeano a => Dict (KnownPeano a))++peanoInstance :: forall a . PeanoRepr a -> Dict (KnownPeano a)+peanoInstance s = with_sing_i Dict+  where+    with_sing_i :: (KnownPeano a => Dict (KnownPeano a)) -> Dict (KnownPeano a)+    with_sing_i si = unsafeCoerce (Don'tInstantiate si) s++-- | convert an explicit number to an implicit number+withKnownPeano :: forall n r. PeanoRepr n -> (KnownPeano n => r) -> r+withKnownPeano si r = case peanoInstance si of+                        Dict -> r++----------------------------------------------------------+-- * Operations on runtime numbers++-- | zero+zeroP :: PeanoRepr Z+zeroP = PeanoRepr 0++-- | Successor, Increment+succP :: PeanoRepr n -> PeanoRepr (S n)+succP (PeanoRepr i) = PeanoRepr (i+1)++-- | Get the predecessor (decrement)+predP :: PeanoRepr (S n) -> PeanoRepr n+predP (PeanoRepr i) = PeanoRepr (i-1)+++plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)+plusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a + b)++minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)+minusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a - b)++mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)+mulP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a * b)++maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)+maxP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (max a b)++minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)+minP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (min a b)++repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)+repeatP n f s = case peanoView n of+  ZRepr   -> s+  SRepr m -> f (repeatP m f s)++------------------------------------------------------------------------+-- * Some PeanoRepr++-- | Convert a Word64 to a PeanoRepr+mkPeanoRepr :: Word64 -> Some PeanoRepr+mkPeanoRepr n = Some (PeanoRepr n)++-- | Turn an @Integral@ value into a @PeanoRepr@.  Returns @Nothing@+--   if the given value is negative.+somePeano :: Integral a => a -> Maybe (Some PeanoRepr)+somePeano x | x >= 0 = Just . Some . PeanoRepr $! fromIntegral x+somePeano _ = Nothing++-- | Return the maximum of two representations.+maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr+maxPeano x y+  | peanoValue x >= peanoValue y = Some x+  | otherwise = Some y++-- | Return the minimum of two representations.+minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr+minPeano x y+  | peanoValue y >= peanoValue x = Some x+  | otherwise = Some y++------------------------------------------------------------------------+--  LocalWords:  PeanoRepr withKnownPeano runtime Peano unary
+ submodules/parameterized-utils/src/Data/Parameterized/TestEquality.hs view
@@ -0,0 +1,36 @@+{-|+Copyright        : (c) Galois, Inc 2014-2018+Maintainer       : Langston Barrett <langston@galois.com++Utilities for working with "Data.Type.TestEquality".++NB: This module contains an orphan instance.+-}++{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}++import Data.Functor.Compose+import Data.Type.Equality++testEqualityComposeBare :: forall f g x y.+                           (forall w z. f w -> f z -> Maybe (w :~: z))+                        -> Compose f g x+                        -> Compose f g y+                        -> Maybe (x :~: y)+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =+  case (testEquality_ x y :: Maybe (g x :~: g y)) of+    Just Refl -> Just (Refl :: x :~: y)+    Nothing   -> Nothing++testEqualityCompose :: forall f g x y. (TestEquality f)+                    => Compose f g x+                    -> Compose f g y+                    -> Maybe (x :~: y)+testEqualityCompose = testEqualityComposeBare testEquality++-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.+instance (TestEquality f) => TestEquality (Compose f g) where+  testEquality = testEqualityCompose
submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs view
@@ -7,8 +7,10 @@ -- This module declares classes for working with structures that accept -- a single parametric type parameter. ------------------------------------------------------------------------+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} module Data.Parameterized.TraversableF   ( FunctorF(..)@@ -24,10 +26,13 @@ import Control.Applicative import Control.Monad.Identity import Data.Coerce+import Data.Functor.Compose (Compose(..)) import Data.Monoid import GHC.Exts (build) --- | A parameterized type that is a function on all instances.+import Data.Parameterized.TraversableFC++-- | A parameterized type that is a functor on all instances. class FunctorF m where   fmapF :: (forall x . f x -> g x) -> m f -> m g @@ -37,7 +42,7 @@ ------------------------------------------------------------------------ -- FoldableF --- | This is a coercision used to avoid overhead associated+-- | This is a coercion used to avoid overhead associated -- with function composition. (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) (#.) _f = coerce@@ -112,5 +117,30 @@  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f ()) -> t e -> f ()+traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f () traverseF_ f = foldrF (\e r -> f e *> r) (pure ())++------------------------------------------------------------------------+-- TraversableF (Compose s t)++instance ( FunctorF (s :: (k -> *) -> *)+         , FunctorFC (t :: (l -> *) -> (k -> *))+         ) =>+         FunctorF (Compose s t) where+  fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v++instance ( TraversableF (s :: (k -> *) -> *)+         , TraversableFC (t :: (l -> *) -> (k -> *))+         ) =>+         FoldableF (Compose s t) where+  foldMapF = foldMapFDefault++-- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.+instance ( TraversableF (s :: (k -> *) -> *)+         , TraversableFC (t :: (l -> *) -> (k -> *))+         ) =>+         TraversableF (Compose s t) where+  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>+               (forall (u :: l). f u -> m (g u))+            -> Compose s t f -> m (Compose s t g)+  traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v
submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs view
@@ -150,12 +150,12 @@  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m a) -> (forall x. t f x -> m ()) traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ()) {-# INLINE traverseFC_ #-}  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m () forMFC_ v f = traverseFC_ f v {-# INLINE forMFC_ #-}
+ submodules/parameterized-utils/src/Data/Parameterized/Utils/Endian.hs view
@@ -0,0 +1,3 @@+module Data.Parameterized.Utils.Endian where++data Endian = LittleEndian | BigEndian deriving (Eq,Show,Ord)
+ submodules/parameterized-utils/src/Data/Parameterized/Vector.hs view
@@ -0,0 +1,507 @@+{-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}+{-# Language PatternGuards #-}+{-# Language TypeApplications, ScopedTypeVariables #-}+{-# Language Rank2Types, RoleAnnotations #-}+{-# Language CPP #-}+#if __GLASGOW_HASKELL__ >= 805+{-# Language NoStarIsType #-}+#endif+-- | A vector fixed-size vector of typed elements.+module Data.Parameterized.Vector+  ( Vector+    -- * Lists+  , fromList+  , toList++    -- * Length+  , length+  , nonEmpty+  , lengthInt++  -- * Indexing+  , elemAt+  , elemAtMaybe+  , elemAtUnsafe++  -- * Update+  , insertAt+  , insertAtMaybe++    -- * Sub sequences+  , uncons+  , slice+  , Data.Parameterized.Vector.take++    -- * Zipping+  , zipWith+  , zipWithM+  , zipWithM_+  , interleave++    -- * Reorder+  , shuffle+  , reverse+  , rotateL+  , rotateR+  , shiftL+  , shiftR++    -- * Construction+  , singleton+  , cons+  , snoc+  , generate+  , generateM++    -- * Splitting and joining+    -- ** General+  , joinWithM+  , joinWith+  , splitWith+  , splitWithA++    -- ** Vectors+  , split+  , join+  , append++  ) where++import qualified Data.Vector as Vector+import Data.Functor.Compose+import Data.Coerce+import Data.Vector.Mutable (MVector)+import qualified Data.Vector.Mutable as MVector+import Control.Monad.ST+import Data.Functor.Identity+import Data.Parameterized.NatRepr+import Data.Proxy+import Prelude hiding (length,reverse,zipWith)+import Numeric.Natural++import Data.Parameterized.Utils.Endian++-- | Fixed-size non-empty vectors.+data Vector n a where+  Vector :: (1 <= n) => !(Vector.Vector a) -> Vector n a++type role Vector nominal representational++instance Eq a => Eq (Vector n a) where+  (Vector x) == (Vector y) = x == y++instance Show a => Show (Vector n a) where+  show (Vector x) = show x++-- | Get the elements of the vector as a list, lowest index first.+toList :: Vector n a -> [a]+toList (Vector v) = Vector.toList v+{-# Inline toList #-}++-- | Length of the vector.+-- @O(1)@+length :: Vector n a -> NatRepr n+length (Vector xs) =+  activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing $ \mk ->+    mk (fromIntegral (Vector.length xs) :: Natural)+{-# INLINE length #-}++-- | The length of the vector as an "Int".+lengthInt :: Vector n a -> Int+lengthInt (Vector xs) = Vector.length xs+{-# Inline lengthInt #-}++elemAt :: ((i+1) <= n) => NatRepr i -> Vector n a -> a+elemAt n (Vector xs) = xs Vector.! widthVal n++-- | Get the element at the given index.+-- @O(1)@+elemAtMaybe :: Int -> Vector n a -> Maybe a+elemAtMaybe n (Vector xs) = xs Vector.!? n+{-# INLINE elemAt #-}++-- | Get the element at the given index.+-- Raises an exception if the element is not in the vector's domain.+-- @O(1)@+elemAtUnsafe :: Int -> Vector n a -> a+elemAtUnsafe n (Vector xs) = xs Vector.! n+{-# INLINE elemAtUnsafe #-}+++-- | Insert an element at the given index.+-- @O(n)@.+insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a+insertAt n a (Vector xs) = Vector (Vector.unsafeUpd xs [(widthVal n,a)])++-- | Insert an element at the given index.+-- Return 'Nothing' if the element is outside the vector bounds.+-- @O(n)@.+insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)+insertAtMaybe n a (Vector xs)+  | 0 <= n && n < Vector.length xs = Just (Vector (Vector.unsafeUpd xs [(n,a)]))+  | otherwise = Nothing+++-- | Proof that the length of this vector is not 0.+nonEmpty :: Vector n a -> LeqProof 1 n+nonEmpty (Vector _) = LeqProof+{-# Inline nonEmpty #-}+++-- | Remove the first element of the vector, and return the rest, if any.+uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))+uncons v@(Vector xs) = (Vector.head xs, mbTail)+  where+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)+  mbTail = case testStrictLeq (knownNat @1) (length v) of+             Left n2_leq_n ->+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))+                  return (Vector (Vector.tail xs))+             Right Refl    -> Left Refl+{-# Inline uncons #-}+++--------------------------------------------------------------------------------++-- | Make a vector of the given length and element type.+-- Returns "Nothing" if the input list does not have the right number of+-- elements.+-- @O(n)@.+fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)+fromList n xs+  | widthVal n == Vector.length v = Just (Vector v)+  | otherwise                     = Nothing+  where+  v = Vector.fromList xs+{-# INLINE fromList #-}+++-- | Extract a subvector of the given vector.+slice :: (i + w <= n, 1 <= w) =>+            NatRepr i {- ^ Start index -} ->+            NatRepr w {- ^ Width of sub-vector -} ->+            Vector n a -> Vector w a+slice i w (Vector xs) = Vector (Vector.slice (widthVal i) (widthVal w) xs)+{-# INLINE slice #-}++-- | Take the front (lower-indexes) part of the vector.+take :: forall n x a. (1 <= n) => NatRepr n -> Vector (n + x) a -> Vector n a+take | LeqProof <- prf = slice (knownNat @0)+  where+  prf = leqAdd (leqRefl (Proxy @n)) (Proxy @x)++--------------------------------------------------------------------------------++instance Functor (Vector n) where+  fmap f (Vector xs) = Vector (Vector.map f xs)+  {-# Inline fmap #-}++instance Foldable (Vector n) where+  foldMap f (Vector xs) = foldMap f xs++instance Traversable (Vector n) where+  traverse f (Vector xs) = Vector <$> traverse f xs+  {-# Inline traverse #-}++-- | Zip two vectors, potentially changing types.+-- @O(n)@+zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c+zipWith f (Vector xs) (Vector ys) = Vector (Vector.zipWith f xs ys)+{-# Inline zipWith #-}++zipWithM :: Monad m => (a -> b -> m c) ->+                       Vector n a -> Vector n b -> m (Vector n c)+zipWithM f (Vector xs) (Vector ys) = Vector <$> Vector.zipWithM f xs ys+{-# Inline zipWithM #-}++zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()+zipWithM_ f (Vector xs) (Vector ys) = Vector.zipWithM_ f xs ys+{-# Inline zipWithM_ #-}++{- | Interleave two vectors.  The elements of the first vector are+at even indexes in the result, the elements of the second are at odd indexes. -}+interleave ::+  forall n a. (1 <= n) => Vector n a -> Vector n a -> Vector (2 * n) a+interleave (Vector xs) (Vector ys)+  | LeqProof <- leqMulPos (Proxy @2) (Proxy @n) = Vector zs+  where+  len = Vector.length xs + Vector.length ys+  zs  = Vector.generate len (\i -> let v = if even i then xs else ys+                                   in v Vector.! (i `div` 2))+++--------------------------------------------------------------------------------++{- | Move the elements around, as specified by the given function.+  * Note: the reindexing function says where each of the elements+          in the new vector come from.+  * Note: it is OK for the same input element to end up in mulitple places+          in the result.+@O(n)@+-}+shuffle :: (Int -> Int) -> Vector n a -> Vector n a+shuffle f (Vector xs) = Vector ys+  where+  ys = Vector.generate (Vector.length xs) (\i -> xs Vector.! f i)+{-# Inline shuffle #-}++-- | Reverse the vector.+reverse :: forall a n. (1 <= n) => Vector n a -> Vector n a+reverse x = shuffle (\i -> lengthInt x - i - 1) x++-- | Rotate "left".  The first element of the vector is on the "left", so+-- rotate left moves all elemnts toward the corresponding smaller index.+-- Elements that fall off the beginning end up at the end.+rotateL :: Int -> Vector n a -> Vector n a+rotateL !n xs = shuffle rotL xs+  where+  !len   = lengthInt xs+  rotL i = (i + n) `mod` len          -- `len` is known to be >= 1+{-# Inline rotateL #-}++-- | Rotate "right".  The first element of the vector is on the "left", so+-- rotate right moves all elemnts toward the corresponding larger index.+-- Elements that fall off the end, end up at the beginning.+rotateR :: Int -> Vector n a -> Vector n a+rotateR !n xs = shuffle rotR xs+  where+  !len   = lengthInt xs+  rotR i = (i - n) `mod` len        -- `len` is known to be >= 1+{-# Inline rotateR #-}++{- | Move all elements towards smaller indexes.+Elements that fall off the front are ignored.+Empty slots are filled in with the given element.+@O(n)@. -}+shiftL :: Int -> a -> Vector n a -> Vector n a+shiftL !x a (Vector xs) = Vector ys+  where+  !len = Vector.length xs+  ys   = Vector.generate len (\i -> let j = i + x+                                    in if j >= len then a else xs Vector.! j)+{-# Inline shiftL #-}++{- | Move all elements towards the larger indexes.+Elements that "fall" off the end are ignored.+Empty slots are filled in with the given element.+@O(n)@. -}+shiftR :: Int -> a -> Vector n a -> Vector n a+shiftR !x a (Vector xs) = Vector ys+  where+  !len = Vector.length xs+  ys   = Vector.generate len (\i -> let j = i - x+                                    in if j < 0 then a else xs Vector.! j)+{-# Inline shiftR #-}++-------------------------------------------------------------------------------i++-- | Append two vectors. The first one is at lower indexes in the result.+append :: Vector m a -> Vector n a -> Vector (m + n) a+append v1@(Vector xs) v2@(Vector ys) =+  case leqAddPos (length v1) (length v2) of { LeqProof ->+    Vector (xs Vector.++ ys)+  }+{-# Inline append #-}++--------------------------------------------------------------------------------+-- Constructing Vectors++-- | Vector with exactly one element+singleton :: forall a. a -> Vector 1 a+singleton a = Vector (Vector.singleton a)++leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)+leqLen v =+  let leqSucc :: forall f z. f z -> LeqProof z (z + 1)+      leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)+  in leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))++-- | Add an element to the head of a vector+cons :: forall n a. a -> Vector n a -> Vector (n+1) a+cons a v@(Vector x) = case leqLen v of LeqProof -> (Vector (Vector.cons a x))++-- | Add an element to the tail of a vector+snoc :: forall n a. Vector n a -> a -> Vector (n+1) a+snoc v@(Vector x) a = case leqLen v of LeqProof -> (Vector (Vector.snoc x a))++-- | This newtype wraps Vector so that we can curry it in the call to+-- @natRecBounded@. It adds 1 to the length so that the base case is+-- a @Vector@ of non-zero length.+newtype Vector' a n = MkVector' (Vector (n+1) a)++unVector' :: Vector' a n -> Vector (n+1) a+unVector' (MkVector' v) = v++snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)+snoc' v = MkVector' . snoc (unVector' v)++generate' :: forall h a+           . NatRepr h+          -> (forall n. (n <= h) => NatRepr n -> a)+          -> Vector' a h+generate' h gen =+  case isZeroOrGT1 h of+    Left Refl -> base+    Right LeqProof ->+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->+      natRecBounded (decNat h) (decNat h) base step+      }+  where base :: Vector' a 0+        base = MkVector' $ singleton (gen (knownNat @0))+        step :: forall m. (1 <= h, m <= h - 1)+             => NatRepr m -> Vector' a m -> Vector' a (m + 1)+        step m v =+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->+          case (leqAdd2 (LeqProof :: LeqProof m (h-1))+                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->+            snoc' v (gen (incNat m))+          }}++-- | Apply a function to each element in a range starting at zero;+-- return the a vector of values obtained.+-- cf. both @natFromZero@ and @Data.Vector.generate@+generate :: forall h a+          . NatRepr h+         -> (forall n. (n <= h) => NatRepr n -> a)+         -> Vector (h + 1) a+generate h gen = unVector' (generate' h gen)++-- | Since @Vector@ is traversable, we can pretty trivially sequence+-- @natFromZeroVec@ inside a monad.+generateM :: forall m h a. (Monad m)+          => NatRepr h+          -> (forall n. (n <= h) => NatRepr n -> m a)+          -> m (Vector (h + 1) a)+generateM h gen = sequence $ generate h gen++--------------------------------------------------------------------------------++coerceVec :: Coercible a b => Vector n a -> Vector n b+coerceVec = coerce++-- | Monadically join a vector of values, using the given function.+-- This functionality can sometimes be reproduced by creating a newtype+-- wrapper and using @joinWith@, this implementation is provided for+-- convenience.+joinWithM ::+  forall m f n w.+  (1 <= w, Monad m) =>+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))+  {- ^ A function for appending contained elements.+       Earlier vector indexes are the first argument of the join function.+       Pass a different function to implmenet little/big endian behaviors -} ->+  NatRepr w -> Vector n (f w) -> m (f (n * w))++joinWithM jn w = fmap fst . go+  where+  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))+  go exprs =+    case uncons exprs of+      (a, Left Refl) -> return (a, w)+      (a, Right rest) ->+        case nonEmpty rest                of { LeqProof ->+        case leqMulPos (length rest) w    of { LeqProof ->+        case nonEmpty exprs               of { LeqProof ->+        case lemmaMul w (length exprs)    of { Refl -> do+          -- @siddharthist: This could probably be written applicatively?+          (res, sz) <- go rest+          joined <- jn sz a res+          return (joined, addNat w sz)+        }}}}++-- | Join a vector of values, using the given function.+joinWith ::+  forall f n w.+  (1 <= w) =>+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))+  {- ^ A function for appending contained elements.+       Earlier vector indexes are the first argument of the join function.+       Pass a different function to implmenet little/big endian behaviors -} ->+  NatRepr w -> Vector n (f w) -> f (n * w)+joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v+{-# Inline joinWith #-}++-- | Split a bit-vector into a vector of bit-vectors.+-- If "LittleEndian", then less significant bits go into smaller indexes.+-- If "BigEndian", then less significant bits go into larger indexes.+splitWith :: forall f w n.+  (1 <= w, 1 <= n) =>+  Endian ->+  (forall i. (i + w <= n * w) =>+             NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)+  {- ^ A function for slicing out a chunk of length @w@, starting at @i@ -} ->+  NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)+splitWith endian select n w val = Vector (Vector.create initializer)+  where+  len          = widthVal n+  start :: Int+  next :: Int -> Int+  (start,next) = case endian of+                   LittleEndian -> (0, succ)+                   BigEndian    -> (len - 1, pred)++  initializer :: forall s. ST s (MVector s (f w))+  initializer =+    do LeqProof <- return (leqMulPos n w)+       LeqProof <- return (leqMulMono n w)++       v <- MVector.new len+       let fill :: Int -> NatRepr i -> ST s ()+           fill loc i =+             let end = addNat i w in+             case testLeq end inLen of+               Just LeqProof ->+                 do MVector.write v loc (select inLen i val)+                    fill (next loc) end+               Nothing -> return ()+++       fill start (knownNat @0)+       return v++  inLen :: NatRepr (n * w)+  inLen = natMultiply n w+{-# Inline splitWith #-}++-- We can sneakily put our functor in the parameter "f" of @splitWith@ using the+-- @Compose@ newtype.+-- | An applicative version of @splitWith@.+splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) =>+  Endian ->+  (forall i. (i + w <= n * w) =>+             NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))+  {- ^ f function for slicing out f chunk of length @w@, starting at @i@ -} ->+  NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))+splitWithA e select n w val = traverse getCompose $+  splitWith @(Compose f g) e select' n w $ Compose (pure val)+  where -- Wrap everything in Compose+        select' :: (forall i. (i + w <= n * w)+                => NatRepr (n * w) -> NatRepr i -> Compose f g (n * w) -> Compose f g w)+        -- Whatever we pass in as "val" is what's passed to select anyway,+        -- so there's no need to examine the argument. Just use "val" directly here.+        select' nw i _ = Compose $ select nw i val++newtype Vec a n = Vec (Vector n a)++vSlice :: (i + w <= l, 1 <= w) =>+  NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w+vSlice w _ i (Vec xs) = Vec (slice i w xs)+{-# Inline vSlice #-}++-- | Append the two bit vectors.  The first argument is+-- at the lower indexes of the resulting vector.+vAppend :: NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)+vAppend _ (Vec xs) (Vec ys) = Vec (append xs ys)+{-# Inline vAppend #-}++-- | Split a vector into a vector of vectors.+split :: (1 <= w, 1 <= n) =>+        NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)+split n w xs = coerceVec (splitWith LittleEndian (vSlice w) n w (Vec xs))+{-# Inline split #-}++-- | Join a vector of vectors into a single vector.+join :: (1 <= w) => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a+join w xs = ys+  where Vec ys = joinWith vAppend w (coerceVec xs)+{-# Inline join #-}
submodules/parameterized-utils/test/Test/Context.hs view
@@ -16,6 +16,7 @@ import Data.Parameterized.TraversableFC import Data.Parameterized.Some +import qualified Data.Parameterized.Context as C import qualified Data.Parameterized.Context.Safe as S import qualified Data.Parameterized.Context.Unsafe as U @@ -167,4 +168,11 @@          case testEquality x y of            Just Refl -> return $ vals1 == vals2            Nothing   -> return $ vals1 /= vals2++   , testProperty "append_take" $ \vals1 vals2 -> ioProperty $ do+         Some x <- return $ mkUAsgn vals1+         Some y <- return $ mkUAsgn vals2+         let z = x U.<++> y+         let x' = C.take (U.size x) (U.size y) z+         return $ isJust $ testEquality x x'    ]
+ submodules/parameterized-utils/test/Test/Vector.hs view
@@ -0,0 +1,67 @@+{-# Language DataKinds #-}+{-# Language ExplicitForAll #-}+{-# Language TypeOperators #-}+{-# Language TypeFamilies #-}+{-# Language FlexibleInstances #-}+{-# Language ScopedTypeVariables #-}+{-# Language StandaloneDeriving #-}+{-# Language CPP #-}+#if __GLASGOW_HASKELL__ >= 805+{-# Language NoStarIsType #-}+#endif+module Test.Vector+( vecTests+) where++import Test.Tasty+import Test.Tasty.QuickCheck (Arbitrary(..), Gen, testProperty)++import Data.Parameterized.NatRepr+import Data.Parameterized.Vector+import GHC.TypeLits+import Prelude hiding (reverse)++instance KnownNat n => Arbitrary (NatRepr n) where+  arbitrary = return knownNat++-- GHC thinks that this instances overlaps with the+-- "Arbitrary a => Arbitrary (Maybe a)" instance from QuickCheck, but it doesn't:+-- there is no "Arbitrary a => Arbitrary (Vector n a)".+--+-- While it might seem like this would just successfully generate a lot+-- of "Nothing", it does a pretty good job. Just try changing one of the tests!+instance {-# OVERLAPS #-} forall a n. (1 <= n, Arbitrary a, KnownNat n)+    => Arbitrary (Maybe (Vector n a)) where+  arbitrary = do+    n <- (arbitrary :: Gen (NatRepr n))+    l <- (arbitrary :: Gen [a])+    return $ fromList n l++instance Show (Int -> Ordering) where+  show _ = "unshowable"++-- We use @Ordering@ just because it's simple+vecTests :: IO TestTree+vecTests = testGroup "Vector" <$> return+  [ testProperty "reverse100" $+      \n v -> fromList (n :: NatRepr 100) (v :: [Ordering]) ==+              (reverse <$> (reverse <$> (fromList n v)))+  , testProperty "reverseSingleton" $+      \n v -> fromList (n :: NatRepr 1) (v :: [Ordering]) ==+              (reverse <$> (fromList n v))+  , testProperty "split-join" $+      \n w v -> (v :: Maybe (Vector (5 * 5) Ordering)) ==+                (join (n :: NatRepr 5) . split n (w :: NatRepr 5) <$> v)+  -- @cons@ is the same for vectors or lists+  , testProperty "cons" $+      \n v x -> (cons x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==+                (fromList (incNat n) (x:v))+  -- @snoc@ is like appending to a list+  , testProperty "snoc" $+      \n v x -> (flip snoc x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==+                (fromList (incNat n) (v ++ [x]))+  -- @generate@ is like mapping a function over indices+  , testProperty "generate" $+      \n f -> Just (generate (n :: NatRepr 55) ((f :: Int -> Ordering) . widthVal)) ==+              (fromList (incNat n) (map f [0..widthVal n]) :: Maybe (Vector 56 Ordering))+  ]
submodules/parameterized-utils/test/UnitTest.hs view
@@ -4,6 +4,7 @@  import qualified Test.Context import qualified Test.NatRepr+import qualified Test.Vector  main :: IO () main = tests >>= defaultMainWithIngredients ingrs@@ -19,4 +20,5 @@ tests = testGroup "ParameterizedUtils" <$> sequence   [ Test.Context.contextTests   , Test.NatRepr.natTests+  , Test.Vector.vecTests   ]