bv-sized 0.4.0 → 0.5.0

raw patch · 37 files changed

+6710/−82 lines, 37 filesdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• LICENSE +2/−2
• README.md +34/−14
• bv-sized.cabal +2/−2
• changelog.md +4/−0
• src/Data/BitVector/Sized.hs +21/−39
• src/Data/BitVector/Sized/App.hs +183/−16
• src/Data/BitVector/Sized/BitLayout.hs +21/−7
• stack.yaml +2/−2
• submodules/parameterized-utils/.git +1/−0
• submodules/parameterized-utils/.gitignore +23/−0
• submodules/parameterized-utils/LICENSE +30/−0
• submodules/parameterized-utils/README.md +7/−0
• submodules/parameterized-utils/parameterized-utils.cabal +100/−0
• submodules/parameterized-utils/src/Data/Parameterized.hs +19/−0
• submodules/parameterized-utils/src/Data/Parameterized/Classes.hs +286/−0
• submodules/parameterized-utils/src/Data/Parameterized/Context.hs +341/−0
• submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs +989/−0
• submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs +1213/−0
• submodules/parameterized-utils/src/Data/Parameterized/Ctx.hs +99/−0
• submodules/parameterized-utils/src/Data/Parameterized/Ctx/Proofs.hs +23/−0
• submodules/parameterized-utils/src/Data/Parameterized/HashTable.hs +97/−0
• submodules/parameterized-utils/src/Data/Parameterized/List.hs +244/−0
• submodules/parameterized-utils/src/Data/Parameterized/Map.hs +548/−0
• submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs +527/−0
• submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs +158/−0
• submodules/parameterized-utils/src/Data/Parameterized/Nonce/Transformers.hs +70/−0
• submodules/parameterized-utils/src/Data/Parameterized/Nonce/Unsafe.hs +107/−0
• submodules/parameterized-utils/src/Data/Parameterized/Pair.hs +51/−0
• submodules/parameterized-utils/src/Data/Parameterized/Some.hs +59/−0
• submodules/parameterized-utils/src/Data/Parameterized/SymbolRepr.hs +106/−0
• submodules/parameterized-utils/src/Data/Parameterized/TH/GADT.hs +488/−0
• submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs +116/−0
• submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs +161/−0
• submodules/parameterized-utils/src/Data/Parameterized/Utils/BinTree.hs +368/−0
• submodules/parameterized-utils/test/Test/Context.hs +170/−0
• submodules/parameterized-utils/test/Test/NatRepr.hs +18/−0
• submodules/parameterized-utils/test/UnitTest.hs +22/−0

@@ -1,4 +1,4 @@-Copyright Ben Selfridge (c) 2018+Copyright Ben Selfridge, Galois Inc. (c) 2018  All rights reserved. @@ -13,7 +13,7 @@       disclaimer in the documentation and/or other materials provided       with the distribution. -    * Neither the name of Ben Selfridge nor the names of other+    * Neither the name of Galois Inc. nor the names of other       contributors may be used to endorse or promote products derived       from this software without specific prior written permission. 

@@ -1,21 +1,41 @@-# bv-sized+bv-sized - A Haskell library for manipulating width-parameterized bitvectors+=== -## Overview+copyright (c) Ben Selfridge, Galois Inc. 2018 -This library defines a `BitVector` datatype that is parameterized by the vector width.+This library defines a `BitVector` datatype that is parameterized by the vector+width. -## Additional features+Requirements+=== -### BitLayout+The following are a list of mandatory and secondary requirements for bv-sized. -We also provides a module called `BitLayout`, which is handy for defining mappings-from smaller `BitVector`s into larger ones. This module is particularly useful when-defining encodings in an instruction set.+Mandatory Requirements+=== -### App+- Must support integer arithmetic on bitvectors of arbitrary width, assuming a+  two's-complement representation. -To aid in building expression languages over `BitVector`s, we provide a module called-App, which supports combining expressions over `BitVector`s using the `BitVector`-operations and evaluating said expressions. It can be used in a pure context or in-conjunction with a state monad. This module was inspired by the `App` type in-[macaw](https://github.com/GaloisInc/macaw), Galois's binary analysis framework.+- Must support the construction of symbolic expressions involving bitvectors,+  and evaluating those expressions in such a way that the "pure" bitvector+  expression language can be embedded in a larger expression language. (See+  Data.BitVector.Sized.App)++- Declarative descriptions of bit encodings within an instruction word for the+  purposes of ISA definitions and the like. (See Data.BitVector.Sized.BitLayout)++Secondary Requirements+===++None.++Current Status+===++The library is relatively stable and supports all the above requirements.++Other information+===++* contact: benselfridge@galois.com

@@ -1,5 +1,5 @@ name:                bv-sized-version:             0.4.0+version:             0.5.0 category:            Bit Vectors synopsis:            a BitVector datatype that is parameterized by the vector width description:@@ -20,7 +20,7 @@                      , Data.BitVector.Sized.App                      , Data.BitVector.Sized.BitLayout   build-depends:       base >= 4.7 && < 5-                     , containers >= 0.5.11 && < 0.6+                     , containers >= 0.5.10 && < 0.6                      , lens >= 4 && < 5                      , mtl >= 2 && < 3                      , parameterized-utils

@@ -1,5 +1,9 @@ # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized) +## 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+ ## 0.4.0 *April 2018*   * Added App module for BitVector expression languages and evaluation 

@@ -2,13 +2,13 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-}  {-| Module      : Data.BitVector.Sized-Copyright   : (c) Benjamin Selfridge, 2018-                  Galois Inc.-License     : BSD3+Copyright   : (c) Galois Inc. 2018+License     : BSD-3 Maintainer  : benselfridge@galois.com Stability   : experimental Portability : portable@@ -45,7 +45,6 @@   , bvExtract, bvExtractWithRepr   , bvZext, bvZextWithRepr   , bvSext, bvSextWithRepr-  , bvMulFU, bvMulFS, bvMulFSU     -- * Conversions to Integer   , bvIntegerU   , bvIntegerS@@ -328,30 +327,6 @@ bvSextWithRepr repr bv = BV repr (truncBits width (bvIntegerS bv))   where width = natValue repr --- | Fully multiply two bit vectors as unsigned integers, returning a bit vector--- whose length is equal to the sum of the inputs.-bvMulFU :: BitVector w -> BitVector w' -> BitVector (w+w')-bvMulFU (BV wRepr x) (BV wRepr' y) = BV (wRepr `addNat` wRepr') (x*y)---- | Fully multiply two bit vectors as signed integers, returning a bit vector whose--- length is equal to the sum of the inputs.-bvMulFS :: BitVector w -> BitVector w' -> BitVector (w+w')-bvMulFS bv1@(BV wRepr _) bv2@(BV wRepr' _) = BV prodRepr (truncBits width (x'*y'))-  where x' = bvIntegerS bv1-        y' = bvIntegerS bv2-        prodRepr = wRepr `addNat` wRepr'-        width = natValue prodRepr---- | Fully multiply two bit vectors, treating the first as a signed integer and the--- second as an unsigned integer, returning a bit vector whose length is equal to the--- sum of the inputs.-bvMulFSU :: BitVector w -> BitVector w' -> BitVector (w+w')-bvMulFSU bv1@(BV wRepr _) bv2@(BV wRepr' _) = BV prodRepr (truncBits width (x'*y'))-  where x' = bvIntegerS bv1-        y' = bvIntegerU bv2-        prodRepr = wRepr `addNat` wRepr'-        width = natValue prodRepr- ---------------------------------------- -- Byte decomposition @@ -364,7 +339,19 @@ 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 ""@@ -384,6 +371,12 @@ 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@@ -447,14 +440,3 @@ instance Pretty (BitVector w) where   -- | Pretty print a bit vector (shows its width)   pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x--------------------------------------------- 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

@@ -1,14 +1,16 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-}  {-| Module      : Data.BitVector.Sized.App-Copyright   : (c) Benjamin Selfridge, 2018-                  Galois Inc.-License     : None (yet)+Copyright   : (c) Galois Inc. 2018+License     : BSD-3 Maintainer  : benselfridge@galois.com Stability   : experimental Portability : portable@@ -30,11 +32,42 @@   ( BVApp(..)   , evalBVApp   , evalBVAppM+  -- * Smart constructors+  , BVExpr(..)+  , litBV+  -- ** Bitwise+  , andE+  , orE+  , xorE+  , notE+  -- ** Arithmetic+  , addE+  , subE+  , mulE+  , quotuE+  , quotsE+  , remuE+  , remsE+  , sllE+  , srlE+  , sraE+  -- ** Comparison+  , eqE+  , ltuE+  , ltsE+  -- ** Width-changing+  , zextE, zextEWithRepr+  , sextE, sextEWithRepr+  , extractE, extractEWithRepr+  , concatE+  -- ** Control+  , iteE   ) where  import Control.Monad.Identity import Data.BitVector.Sized import Data.Parameterized+import Data.Parameterized.TH.GADT import Foreign.Marshal.Utils (fromBool) import GHC.TypeLits @@ -58,11 +91,9 @@   -- Arithmetic operations   AddApp   :: !(expr w) -> !(expr w) -> BVApp expr w   SubApp   :: !(expr w) -> !(expr w) -> BVApp expr w-  MulSApp  :: !(expr w) -> !(expr w) -> BVApp expr (w+w)-  MulUApp  :: !(expr w) -> !(expr w) -> BVApp expr (w+w)-  MulSUApp :: !(expr w) -> !(expr w) -> BVApp expr (w+w)-  DivUApp  :: !(expr w) -> !(expr w) -> BVApp expr w-  DivSApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  MulApp   :: !(expr w) -> !(expr w) -> BVApp expr w+  QuotUApp :: !(expr w) -> !(expr w) -> BVApp expr w+  QuotSApp :: !(expr w) -> !(expr w) -> BVApp expr w   RemUApp  :: !(expr w) -> !(expr w) -> BVApp expr w   RemSApp  :: !(expr w) -> !(expr w) -> BVApp expr w @@ -80,6 +111,35 @@   -- Other operations   IteApp :: !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w +$(return [])++instance TestEquality expr => TestEquality (BVApp expr) where+  testEquality = $(structuralTypeEquality [t|BVApp|]+                   [ (AnyType `TypeApp` AnyType, [|testEquality|]) ])++instance TestEquality expr => Eq (BVApp expr w) where+  (==) = \x y -> isJust (testEquality x y)++instance OrdF expr => OrdF (BVApp expr) where+  compareF = $(structuralTypeOrd [t|BVApp|]+                [ (AnyType `TypeApp` AnyType, [|compareF|]) ])++instance OrdF expr => Ord (BVApp expr w) where+  compare a b =+    case compareF a b of+      LTF -> LT+      EQF -> EQ+      GTF -> GT++instance FunctorFC BVApp where+  fmapFC = fmapFCDefault++instance FoldableFC BVApp where+  foldMapFC = foldMapFCDefault++instance TraversableFC BVApp where+  traverseFC = $(structuralTraversal [t|BVApp|] [])+ -- | Evaluate a 'BVApp' given a monadic evaluation function for the parameterized type @expr@. evalBVAppM :: Monad m            => (forall w' . expr w' -> m (BitVector w')) -- ^ expression evaluator@@ -95,11 +155,9 @@ evalBVAppM eval (SllApp e1 e2) = bvShiftL  <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2) evalBVAppM eval (SrlApp e1 e2) = bvShiftRL <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2) evalBVAppM eval (SraApp e1 e2) = bvShiftRA <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2)-evalBVAppM eval (MulSApp  e1 e2) = bvMulFS  <$> eval e1 <*> eval e2-evalBVAppM eval (MulUApp  e1 e2) = bvMulFU  <$> eval e1 <*> eval e2-evalBVAppM eval (MulSUApp e1 e2) = bvMulFSU <$> eval e1 <*> eval e2-evalBVAppM eval (DivSApp  e1 e2) = bvQuotS  <$> eval e1 <*> eval e2-evalBVAppM eval (DivUApp  e1 e2) = bvQuotU  <$> eval e1 <*> eval e2+evalBVAppM eval (MulApp e1 e2) = bvMul <$> eval e1 <*> eval e2+evalBVAppM eval (QuotSApp e1 e2) = bvQuotS  <$> eval e1 <*> eval e2+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 (EqApp  e1 e2) = fromBool <$> ((==)  <$> eval e1 <*> eval e2)@@ -114,12 +172,121 @@   return $ e1Val `bvConcat` e2Val evalBVAppM eval (IteApp eTest eT eF) = do   testVal <- eval eTest-  tVal <- eval eT-  fVal <- eval eF-  return $ if testVal == 1 then tVal else fVal+  case testVal of+    1 -> eval eT+    _ -> eval eF  -- | Evaluate a 'BVApp' given a pure evaluation function for the parameterized type @expr@. evalBVApp :: (forall w' . expr w' -> BitVector w') -- ^ expression evaluator           -> BVApp expr w                          -- ^ application           -> BitVector w evalBVApp eval bvApp = runIdentity $ evalBVAppM (return . eval) bvApp++-- | Typeclass for embedding 'BVApp' constructors into larger expression types.+class BVExpr (expr :: Nat -> *) where+  appExpr :: BVApp expr w -> expr w++-- | Literal bit vector.+litBV :: BVExpr expr => BitVector w -> expr w+litBV = appExpr . LitBVApp++-- | Bitwise and.+andE :: BVExpr expr => expr w -> expr w -> expr w+andE e1 e2 = appExpr (AndApp e1 e2)++-- | Bitwise or.+orE :: BVExpr expr => expr w -> expr w -> expr w+orE e1 e2 = appExpr (OrApp e1 e2)++-- | Bitwise xor.+xorE :: BVExpr expr => expr w -> expr w -> expr w+xorE e1 e2 = appExpr (XorApp e1 e2)++-- | Bitwise not.+notE :: BVExpr expr => expr w -> expr w+notE e = appExpr (NotApp e)++-- | Add two expressions.+addE :: BVExpr expr => expr w -> expr w -> expr w+addE e1 e2 = appExpr (AddApp e1 e2)++-- | Subtract the second expression from the first.+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+-- 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.+quotsE :: BVExpr expr => expr w -> expr w -> expr w+quotsE e1 e2 = appExpr (QuotSApp e1 e2)++-- | Unsigned divide two 'BitVectors', 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.+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.+remuE :: BVExpr expr => expr w -> expr w -> expr w+remuE e1 e2 = appExpr (RemUApp e1 e2)++-- | 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)++-- | Left logical shift the first expression by the second.+srlE :: BVExpr expr => expr w -> expr w -> expr w+srlE e1 e2 = appExpr (SrlApp e1 e2)++-- | Left logical shift the first expression by the second.+sraE :: BVExpr expr => expr w -> expr w -> expr w+sraE e1 e2 = appExpr (SraApp e1 e2)++-- | Test for equality of two expressions.+eqE :: BVExpr expr => expr w -> expr w -> expr 1+eqE e1 e2 = appExpr (EqApp e1 e2)++-- | Signed less than+ltsE :: BVExpr expr => expr w -> expr w -> expr 1+ltsE e1 e2 = appExpr (LtsApp e1 e2)++-- | Unsigned less than+ltuE :: BVExpr expr => expr w -> expr w -> expr 1+ltuE e1 e2 = appExpr (LtuApp e1 e2)++-- | Zero-extension+zextE :: (BVExpr expr, KnownNat w') => expr w -> expr w'+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)++-- | 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)++-- | 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)++-- | Concatenation+concatE :: BVExpr expr => expr w -> expr w' -> expr (w+w')+concatE e1 e2 = appExpr (ConcatApp e1 e2)++-- | Conditional branch.+iteE :: BVExpr expr => expr 1 -> expr w -> expr w -> expr w+iteE t e1 e2 = appExpr (IteApp t e1 e2)

@@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -9,9 +10,8 @@  {-| Module      : Data.BitVector.Sized.BitLayout-Copyright   : (c) Benjamin Selfridge, 2018-                  Galois Inc.-License     : BSD3+Copyright   : (c) Galois Inc. 2018+License     : BSD-3 Maintainer  : benselfridge@galois.com Stability   : experimental Portability : portable@@ -27,17 +27,19 @@   , chunk     -- * BitLayout   , BitLayout-  , empty, (<:)+  , empty, singleChunk, (<:)   , inject   , extract-    -- * Lens-  , layoutLens+    -- * Lenses+  , layoutLens, layoutsLens   ) where  import Data.BitVector.Sized import Data.Foldable+import qualified Data.Functor.Product as P import Control.Lens (lens, Simple, Lens) import Data.Parameterized+import Data.Parameterized.List import qualified Data.Sequence as S import Data.Sequence (Seq) import GHC.TypeLits@@ -151,6 +153,10 @@ empty :: KnownNat t => BitLayout t 0 empty = BitLayout knownNat knownNat S.empty +-- | Construct a 'BitLayout' with one chunk.+singleChunk :: (KnownNat w, KnownNat w') => Int -> BitLayout w w'+singleChunk idx = chunk idx <: empty+ -- TODO: Should this be in Maybe? -- | Add a 'Chunk' to a 'BitLayout'. If the 'Chunk' does not fit, either because the -- resulting 'BitLayout' would be too long or because it would overlap with a 'Chunk'@@ -243,6 +249,14 @@         -> BitVector s extract (BitLayout _ sRepr chunks) = extractAll sRepr 0 (toList chunks) --- | Lens for bit layout.+-- | Lens for a 'BitLayout'. layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s) layoutLens layout = lens (extract layout) (inject layout)++-- | Lens for a parameterized 'List' of 'BitLayout's.+layoutsLens :: forall ws . List (BitLayout 32) ws -> Simple Lens (BitVector 32) (List BitVector ws)+layoutsLens layouts = lens+  (\bv -> imap (const $ flip extract bv) layouts)+  (\bv bvFlds -> ifoldr (\_ (P.Pair fld layout) bv' -> inject layout bv' fld)+                 bv+                 (izipWith (const P.Pair) bvFlds layouts))

@@ -1,12 +1,12 @@-resolver: lts-10.8+resolver: lts-12.5  packages: - .+- submodules/parameterized-utils  extra-deps: - containers-0.5.11.0 - lens-4.16-- parameterized-utils-1.0.0 - prettyclass-1.0.0.0 - random-1.1 - QuickCheck-2.11.3

@@ -0,0 +1,1 @@+gitdir: ../../.git/modules/submodules/parameterized-utils

@@ -0,0 +1,23 @@+/build/+/dependencies/+/dependencies+.cabal-sandbox+.stack-work+**/cabal.config+cabal.sandbox.config+dist+TAGS+unitTest.tix+hpc_report+stack.yaml+/dist-newstyle+.*.swp+.vagrant+graphmod+.hlint.yaml+cabal.project.local+dist-newstyle/+.boring+_darcs/+.cmd_history+*~

@@ -0,0 +1,30 @@+Copyright (c) 2013-2016 Galois Inc.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++  * Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++  * Redistributions in binary form must reproduce the above copyright+    notice, this list of conditions and the following disclaimer in+    the documentation and/or other materials provided with the+    distribution.++  * Neither the name of Galois, Inc. nor the names of its contributors+    may be used to endorse or promote products derived from this+    software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,7 @@+The parameterized-utils module contains a collection of typeclasses+and datatypes for working with parameterized types, that is types that+have a type argument.  One example would be a algebraic data type+for expressions, that use a type parameter to describe the type of the+expression.++This packaged provides collections classes for these parameterized types.

@@ -0,0 +1,100 @@+Name:          parameterized-utils+Version:       1.0.0+Author:        Galois Inc.+Maintainer:    jhendrix@galois.com+Build-type:    Simple+Cabal-version: >= 1.9.2+license: BSD3+license-file: LICENSE+category: Data Structures, Dependent Types+Synopsis: Classes and data structures for working with data-kind indexed types+Description:+  This packages contains collection classes and type representations+  used for working with values that have a single parameter.  It's+  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.++-- Many (but not all, sadly) uses of unsafe operations are+-- controlled by this compile flag.  When this flag is set+-- to False, alternate implementations are used to avoid+-- Unsafe.Coerce and Data.Coerce.  These alternate implementations+-- impose a significant performance hit.+flag unsafe-operations+  Description: Use unsafe operations to improve performance+  Default: True++source-repository head+  type: git+  location: https://github.com/GaloisInc/parameterized-utils++library+  build-depends:+    base >= 4.7 && < 4.12,+    th-abstraction >=0.1 && <0.3,+    containers,+    deepseq,+    ghc-prim,+    hashable,+    hashtables,+    lens,+    mtl,+    template-haskell,+    text,+    vector++  hs-source-dirs: src++  exposed-modules:+    Data.Parameterized+    Data.Parameterized.Classes+    Data.Parameterized.Context+    Data.Parameterized.Context.Safe+    Data.Parameterized.Context.Unsafe+    Data.Parameterized.Ctx+    Data.Parameterized.Ctx.Proofs+    Data.Parameterized.HashTable+    Data.Parameterized.List+    Data.Parameterized.Map+    Data.Parameterized.NatRepr+    Data.Parameterized.Nonce+    Data.Parameterized.Nonce.Transformers+    Data.Parameterized.Nonce.Unsafe+    Data.Parameterized.Some+    Data.Parameterized.SymbolRepr+    Data.Parameterized.Pair+    Data.Parameterized.TH.GADT+    Data.Parameterized.TraversableF+    Data.Parameterized.TraversableFC+    Data.Parameterized.Utils.BinTree++  ghc-options: -Wall++  if flag(unsafe-operations)+    cpp-options: -DUNSAFE_OPS+++test-suite parameterizedTests+  type: exitcode-stdio-1.0+  hs-source-dirs: test++  ghc-options: -Wall++  main-is:UnitTest.hs+  other-modules:+    Test.Context+    Test.NatRepr++  build-depends:+    base,+    hashable,+    hashtables,+    ghc-prim,+    lens,+    mtl,+    parameterized-utils,+    tasty,+    tasty-ant-xml,+    tasty-hunit,+    tasty-quickcheck >= 0.8.1,+    QuickCheck >= 2.7

@@ -0,0 +1,19 @@+module Data.Parameterized+( module Data.Parameterized.Classes       +, module Data.Parameterized.Ctx           +, module Data.Parameterized.TraversableF  +, module Data.Parameterized.TraversableFC +, module Data.Parameterized.NatRepr       +, module Data.Parameterized.Pair          +, module Data.Parameterized.Some          +, module Data.Parameterized.SymbolRepr    +) where++import Data.Parameterized.Classes+import Data.Parameterized.Ctx+import Data.Parameterized.TraversableF+import Data.Parameterized.TraversableFC+import Data.Parameterized.NatRepr+import Data.Parameterized.Pair+import Data.Parameterized.Some+import Data.Parameterized.SymbolRepr    

@@ -0,0 +1,286 @@+{-|+Copyright        : (c) Galois, Inc 2014-2015+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This module declares classes for working with types with the kind+@k -> *@ for any kind @k@.  These are generalizations of the+"Data.Functor.Classes" types as they work with any kind @k@, and are+not restricted to '*'.+-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+#if MIN_VERSION_base(4,9,0)+{-# LANGUAGE Safe #-}+#else+{-# LANGUAGE Trustworthy #-}+#endif+module Data.Parameterized.Classes+  ( -- * Equality exports+    Equality.TestEquality(..)+  , (Equality.:~:)(..)+  , EqF(..)+  , PolyEq(..)+    -- * Ordering generalization+  , OrdF(..)+  , lexCompareF+  , OrderingF(..)+  , joinOrderingF+  , orderingF_refl+  , toOrdering+  , fromOrdering+    -- * Typeclass generalizations+  , ShowF(..)+  , showsF+  , HashableF(..)+  , CoercibleF(..)+    -- * Optics generalizations+  , IndexF+  , IxValueF+  , IxedF(..)+  , IxedF'(..)+  , AtF(..)+    -- * KnownRepr+  , KnownRepr(..)+    -- * Re-exports+  , Data.Maybe.isJust+  ) where++import Data.Functor.Const+import Data.Hashable+import Data.Maybe (isJust)+import Data.Proxy+import Data.Type.Equality as Equality++-- We define these type alias here to avoid importing Control.Lens+-- modules, as this apparently causes problems with the safe Hasekll+-- checking.+type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s+type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s++------------------------------------------------------------------------+-- CoercibleF++-- | An instance of 'CoercibleF' gives a way to coerce between+--   all the types of a family.  We generally use this to witness+--   the fact that the type parameter to @rtp@ is a phantom type+--   by giving an implementation in terms of Data.Coerce.coerce.+class CoercibleF (rtp :: k -> *) where+  coerceF :: rtp a -> rtp b++instance CoercibleF (Const x) where+  coerceF (Const x) = Const x++------------------------------------------------------------------------+-- EqF++-- | @EqF@ provides a method @eqF@ for testing whether two parameterized+-- types are equal.+--+-- Unlike 'TestEquality', this only works when the type arguments are+-- the same, and does not provide a proof that the types have the same+-- type when they are equal. Thus this can be implemented over+-- parameterized types that are unable to provide evidence that their+-- type arguments are equal.+class EqF (f :: k -> *) where+  eqF :: f a -> f a -> Bool++instance Eq a => EqF (Const a) where+  eqF (Const x) (Const y) = x == y++------------------------------------------------------------------------+-- PolyEq++-- | A polymorphic equality operator that generalizes 'TestEquality'.+class PolyEq u v where+  polyEqF :: u -> v -> Maybe (u :~: v)++  polyEq :: u -> v -> Bool+  polyEq x y = isJust (polyEqF x y)++------------------------------------------------------------------------+-- Ordering++-- | Ordering over two distinct types with a proof they are equal.+data OrderingF x y where+  LTF :: OrderingF x y+  EQF :: OrderingF x x+  GTF :: OrderingF x y++orderingF_refl :: OrderingF x y -> Maybe (x :~: y)+orderingF_refl o =+  case o of+    LTF -> Nothing+    EQF -> Just Refl+    GTF -> Nothing++-- | Convert 'OrderingF' to standard ordering.+toOrdering :: OrderingF x y -> Ordering+toOrdering LTF = LT+toOrdering EQF = EQ+toOrdering GTF = GT++-- | Convert standard ordering to 'OrderingF'.+fromOrdering :: Ordering -> OrderingF x x+fromOrdering LT = LTF+fromOrdering EQ = EQF+fromOrdering GT = GTF++-- | `joinOrderingF x y` first compares on x, returning an equivalent+-- value if it is not `EQF`.  If it is EQF, it returns `y`.+joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k)+              .  OrderingF a b+              -> (a ~ b => OrderingF c d)+              -> OrderingF c d+joinOrderingF EQF y = y+joinOrderingF LTF _ = LTF+joinOrderingF GTF _ = GTF++------------------------------------------------------------------------+-- OrdF++-- | A parameterized type that can be compared on distinct instances.+class TestEquality ktp => OrdF (ktp :: k -> *) where+  {-# MINIMAL compareF #-}++  -- | compareF compares two keys with different type parameters.+  -- Instances must ensure that keys are only equal if the type+  -- parameters are equal.+  compareF :: ktp x -> ktp y -> OrderingF x y++  leqF :: ktp x -> ktp y -> Bool+  leqF x y =+    case compareF x y of+      LTF -> True+      EQF -> True+      GTF -> False++  ltF :: ktp x -> ktp y -> Bool+  ltF x y =+    case compareF x y of+      LTF -> True+      EQF -> False+      GTF -> False++  geqF :: ktp x -> ktp y -> Bool+  geqF x y =+    case compareF x y of+      LTF -> False+      EQF -> True+      GTF -> True++  gtF :: ktp x -> ktp y -> Bool+  gtF x y =+    case compareF x y of+      LTF -> False+      EQF -> False+      GTF -> True++-- | Compare two values, and if they are equal compare the next values,+-- otherwise return LTF or GTF+lexCompareF :: forall (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k)+             .  OrdF f+            => f a+            -> f b+            -> (a ~ b => OrderingF c d)+            -> OrderingF c d+lexCompareF x y = joinOrderingF (compareF x y)++------------------------------------------------------------------------+-- ShowF++-- | A parameterized type that can be shown on all instances.+--+-- To implement @'ShowF' g@, one should implement an instance @'Show'+-- (g tp)@ for all argument types @tp@, then write an empty instance+-- @instance 'ShowF' g@.+class ShowF (f :: k -> *) where+  -- | Provides a show instance for each type.+  withShow :: p f -> q tp -> (Show (f tp) => a) -> a++  default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a+  withShow _ _ x = x++  showF :: forall tp . f tp -> String+  showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x)++  -- | Like 'showsPrec', the precedence argument is /one more/ than the+  -- precedence of the enclosing context.+  showsPrecF :: forall tp. Int -> f tp -> String -> String+  showsPrecF p x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (showsPrec p x)++showsF :: ShowF f => f tp -> String -> String+showsF x = showsPrecF 0 x++instance Show x => ShowF (Const x)++------------------------------------------------------------------------+-- IxedF++type family IndexF       (m :: *) :: k -> *+type family IxValueF     (m :: *) :: k -> *++-- | Parameterized generalization of the lens @Ixed@ class.+class IxedF k m where+  -- | Given an index into a container, build a traversal that visits+  --   the given element in the container, if it exists.+  ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x)++-- | Parameterized generalization of the lens @Ixed@ class,+--   but with the guarantee that indexes exist in the container.+class IxedF k m => IxedF' k m where+  -- | Given an index into a container, build a lens that+  --   points into the given element in the container.+  ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x)++------------------------------------------------------------------------+-- AtF++-- | Parameterized generalization of the lens @At@ class.+class IxedF k m => AtF k m where+  -- | Given an index into a container, build a lens that points into+  --   the given position in the container, whether or not it currently+  --   exists.  Setting values of @atF@ to a @Just@ value will insert+  --   the value if it does not already exist.+  atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x))++------------------------------------------------------------------------+-- HashableF++-- | A default salt used in the implementation of 'hash'.+defaultSalt :: Int+#if WORD_SIZE_IN_BITS == 64+defaultSalt = 0xdc36d1615b7400a4+#else+defaultSalt = 0x087fc72c+#endif+{-# INLINE defaultSalt #-}++-- | A parameterized type that is hashable on all instances.+class HashableF (f :: k -> *) where+  hashWithSaltF :: Int -> f tp -> Int++  -- | Hash with default salt.+  hashF :: f tp -> Int+  hashF = hashWithSaltF defaultSalt++instance Hashable a => HashableF (Const a) where+  hashWithSaltF s (Const x) = hashWithSalt s x++------------------------------------------------------------------------+-- KnownRepr++-- | This class is parameterized by a kind @k@ (typically a data+-- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of+-- singleton types indexed by @k@), and an index parameter @ctx@ of+-- kind @k@.+class KnownRepr (f :: k -> *) (ctx :: k) where+  knownRepr :: f ctx

@@ -0,0 +1,341 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.Context+-- Copyright        : (c) Galois, Inc 2014-16+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module reexports either "Data.Parameterized.Context.Safe"+-- or "Data.Parameterized.Context.Unsafe" depending on the+-- the unsafe-operations compile-time flag.+--+-- It also defines some utility typeclasses for transforming+-- between curried and uncurried versions of functions over contexts.+------------------------------------------------------------------------++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ViewPatterns #-}+module Data.Parameterized.Context+ (+#ifdef UNSAFE_OPS+   module Data.Parameterized.Context.Unsafe+#else+   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++   -- * Static indexing and lenses for assignments+ , Idx+ , field+ , natIndex+ , natIndexProxy+   -- * Currying and uncurrying for assignments+ , CurryAssignment+ , CurryAssignmentClass(..)+ ) where++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.Parameterized.Classes+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC++#ifdef UNSAFE_OPS+import           Data.Parameterized.Context.Unsafe+#else+import           Data.Parameterized.Context.Safe+#endif+++-- | Create a single element context.+singleton :: f tp -> Assignment f (EmptyCtx ::> tp)+singleton = (empty :>)++-- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.+forIndexM :: forall ctx m+           . Applicative m+          => Size ctx+          -> (forall tp . Index ctx tp -> m ())+          -> m ()+forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ())++-- | Generate an assignment with some context type that is not known.+generateSome :: forall f+              . Int+             -> (Int -> Some f)+             -> Some (Assignment f)+generateSome n f = go n+  where go :: Int -> Some (Assignment f)+        go 0 = Some empty+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1))++-- | Generate an assignment with some context type that is not known.+generateSomeM :: forall m f+              .  Applicative m+              => Int+              -> (Int -> m (Some f))+              -> m (Some (Assignment f))+generateSomeM n f = go n+  where go :: Int -> m (Some (Assignment f))+        go 0 = pure (Some empty)+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1)++-- | Convert the assignment to a vector.+toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e+toVector a f = V.create $ do+  vm <- MV.new (sizeInt (size a))+  forIndexM (size a) $ \i -> do+    MV.write vm (indexVal i) (f (a ! i))+  return vm+{-# INLINABLE toVector #-}++--------------------------------------------------------------------------------+-- Patterns++-- | Pattern synonym for the empty assignment+pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx+pattern Empty <- (viewAssign -> AssignEmpty)+  where Empty = empty++infixl :>++-- | Pattern synonym for extending an assignment on the right+pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'+pattern (:>) a v <- (viewAssign -> AssignExtend a v)+  where a :> v = extend a v++-- The COMPLETE pragma was not defined until ghc 8.2.*+#if MIN_VERSION_base(4,10,0)+{-# COMPLETE (:>), Empty :: Assignment  #-}+#endif++--------------------------------------------------------------------------------+-- | Views++-- | Return true if assignment is empty.+null :: Assignment f ctx -> Bool+null a =+  case viewAssign a of+    AssignEmpty -> True+    AssignExtend{} -> False++decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)+decompose x = (Data.Parameterized.Context.init x, Data.Parameterized.Context.last x)++-- | Return assignment with all but the last block.+init :: Assignment f (ctx '::> tp) -> Assignment f ctx+init x =+  case viewAssign x of+    AssignExtend t _ -> t++-- | Return the last element in the assignment.+last :: Assignment f (ctx '::> tp) -> f tp+last x =+  case viewAssign x of+    AssignExtend _ e -> e++{-# DEPRECATED view "Use viewAssign or the Empty and :> patterns instead." #-}+-- | View an assignment as either empty or an assignment with one appended.+view :: forall f ctx . Assignment f ctx -> AssignView f ctx+view = viewAssign++--------------------------------------------------------------------------------+-- | Context embedding.++-- 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.++data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)+  = CtxEmbedding { _ctxeSize       :: Size ctx'+                 , _ctxeAssignment :: Assignment (Index ctx') ctx+                 }++-- Alternate encoding?+-- data CtxEmbedding ctx ctx' where+--   EIdentity  :: CtxEmbedding ctx ctx+--   ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)+--   ExtendOne  :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)++ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')+ctxeSize = lens _ctxeSize (\s v -> s { _ctxeSize = v })++ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx')+                       (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)+ctxeAssignment = lens _ctxeAssignment (\s v -> s { _ctxeAssignment = v })++class ApplyEmbedding (f :: Ctx k -> *) where+  applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx'++class ApplyEmbedding' (f :: Ctx k -> k' -> *) where+  applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v++class ExtendContext (f :: Ctx k -> *) where+  extendContext :: Diff ctx ctx' -> f ctx -> f ctx'++class ExtendContext' (f :: Ctx k -> k' -> *) where+  extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v++instance ApplyEmbedding' Index where+  applyEmbedding' ctxe idx = (ctxe ^. ctxeAssignment) ! idx++instance ExtendContext' Index where+  extendContext' = extendIndex'++-- -- This is the inefficient way of doing things.  A better way is to+-- -- just have a map between indices.+-- applyEmbedding :: CtxEmbedding ctx ctx'+--                -> Index ctx tp -> Index ctx' tp+-- applyEmbedding ctxe idx = (ctxe ^. ctxeAssignment) ! idx++identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx+identityEmbedding sz = CtxEmbedding sz (generate sz id)++-- emptyEmbedding :: CtxEmbedding EmptyCtx EmptyCtx+-- emptyEmbedding = identityEmbedding knownSize++extendEmbeddingRightDiff :: forall ctx ctx' ctx''.+                            Diff ctx' ctx''+                            -> CtxEmbedding ctx ctx'+                            -> CtxEmbedding ctx ctx''+extendEmbeddingRightDiff diff (CtxEmbedding sz' assgn) = CtxEmbedding (extSize sz' diff) updated+  where+    updated :: Assignment (Index ctx'') ctx+    updated = fmapFC (extendIndex' diff) assgn++extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)+extendEmbeddingRight = extendEmbeddingRightDiff knownDiff++extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)+extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))+  where+    updated :: CtxEmbedding ctx (ctx' ::> tp)+    updated = extendEmbeddingRight ctxe++--------------------------------------------------------------------------------+-- Static indexing based on type-level naturals++-- | Get a lens for an position in an 'Assignment' by zero-based, left-to-right position.+-- The position must be specified using @TypeApplications@ for the @n@ parameter.+field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)+field = ixF' (natIndex @n)++-- | Constraint synonym used for getting an 'Index' into a 'Ctx'.+-- @n@ is the zero-based, left-counted index into the list of types+-- @ctx@ which has the type @r@.+type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)++-- | Compute an 'Index' value for a particular position in a 'Ctx'. The+-- @TypeApplications@ extension will be needed to disambiguate the choice+-- of the type @n@.+natIndex :: forall n ctx r. Idx n ctx r => Index ctx r+natIndex = natIndex' @_ @(FromLeft ctx n)++-- | This version of 'natIndex' is suitable for use without the @TypeApplications@+-- extension.+natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r+natIndexProxy _ = natIndex @n++------------------------------------------------------------------------+-- Implementation+------------------------------------------------------------------------++-- | Class for computing 'Index' values for positions in a 'Ctx'.+class KnownContext ctx => Idx' (n :: Nat) (ctx :: Ctx k) (r :: k) | n ctx -> r where+  natIndex' :: Index ctx r++-- | Base-case+instance KnownContext xs => Idx' 0 (xs '::> x) x where+  natIndex' = lastIndex knownSize++-- | Inductive-step+instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) =>+  Idx' n (xs '::> x) r where++  natIndex' = skipIndex (natIndex' @_ @(n-1))+++--------------------------------------------------------------------------------+-- CurryAssignment++-- | This type family is used to define currying\/uncurrying operations+-- on assignments.  It is best understood by seeing its evaluation on+-- several examples:+--+-- > CurryAssignment EmptyCtx f x = x+-- > CurryAssignment (EmptyCtx ::> a) f x = f a -> x+-- > CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x+-- > CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x+type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where+   CurryAssignment EmptyCtx    f x = x+   CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x)++-- | This class implements two methods that witness the isomorphism between+--   curried and uncurried functions.+class CurryAssignmentClass (ctx :: Ctx k) where++  -- | Transform a function that accepts an assignment into one with a separate+  --   variable for each element of the assignment.+  curryAssignment   :: (Assignment f ctx -> x) -> CurryAssignment ctx f x++  -- | Transform a curried function into one that accepts an assignment value.+  uncurryAssignment :: CurryAssignment ctx f x -> (Assignment f ctx -> x)++instance CurryAssignmentClass EmptyCtx where+  curryAssignment k = k empty+  uncurryAssignment k _ = k++instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where+  curryAssignment k = curryAssignment (\asgn a -> k (asgn :> a))+  uncurryAssignment k asgn =+    case viewAssign asgn of+      AssignExtend asgn' x -> uncurryAssignment k asgn' x++-- | Create an assignment from a list of values.+fromList :: [Some f] -> Some (Assignment f)+fromList = go empty+  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)+        go prev [] = Some prev+        go prev (Some g:next) = (go $! prev `extend` g) next

@@ -0,0 +1,989 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.Context.Safe+-- Copyright        : (c) Galois, Inc 2014-2015+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module defines type contexts as a data-kind that consists of+-- a list of types.  Indexes are defined with respect to these contexts.+-- In addition, finite dependent products (Assignments) are defined over+-- type contexts.  The elements of an assignment can be accessed using+-- appropriately-typed indexes.+--+-- This module is intended to export exactly the same API as module+-- "Data.Parameterized.Context.Unsafe", so that they can be used+-- interchangeably.+--+-- This implementation is entirely typesafe, and provides a proof that+-- the signature implemented by this module is consistent.  Contexts,+-- indexes, and assignments are represented naively by linear sequences.+--+-- Compared to the implementation in "Data.Parameterized.Context.Unsafe",+-- this one suffers from the fact that the operation of extending an+-- the context of an index is /not/ a no-op. We therefore cannot use+-- 'Data.Coerce.coerce' to understand indexes in a new context without+-- actually breaking things.+--------------------------------------------------------------------------+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE IncoherentInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeInType #-}+module Data.Parameterized.Context.Safe+  ( module Data.Parameterized.Ctx+    -- * Size+  , Size+  , sizeInt+  , zeroSize+  , incSize+  , decSize+  , extSize+  , addSize+  , SizeView(..)+  , viewSize+  , KnownContext(..)+    -- * Diff+  , Diff+  , noDiff+  , extendRight+  , DiffView(..)+  , viewDiff+  , KnownDiff(..)+    -- * Indexing+  , Index+  , indexVal+  , baseIndex+  , skipIndex+  , lastIndex+  , nextIndex+  , extendIndex+  , extendIndex'+  , forIndex+  , forIndexRange+  , intIndex+    -- * Assignments+  , Assignment+  , size+  , Data.Parameterized.Context.Safe.replicate+  , generate+  , generateM+  , empty+  , extend+  , adjust+  , update+  , adjustM+  , AssignView(..)+  , viewAssign+  , (!)+  , (!^)+  , zipWith+  , zipWithM+  , (<++>)+  , traverseWithIndex+  ) where++import qualified Control.Category as Cat+import Control.DeepSeq+import qualified Control.Lens as Lens+import Control.Monad.Identity (Identity(..))+import Data.Hashable+import Data.List (intercalate)+import Data.Maybe (listToMaybe)+import Data.Type.Equality+import Prelude hiding (init, map, null, replicate, succ, zipWith)+import Data.Kind(Type)++#if !MIN_VERSION_base(4,8,0)+import Data.Functor+import Control.Applicative (Applicative(..))+#endif++import Data.Parameterized.Classes+import Data.Parameterized.Ctx+import Data.Parameterized.Some+import Data.Parameterized.TraversableFC++------------------------------------------------------------------------+-- Size++-- | A  indexed singleton type representing the size of a context.+data Size (ctx :: Ctx k) where+  SizeZero :: Size 'EmptyCtx+  SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)++-- | Convert a context size to an 'Int'.+sizeInt :: Size ctx -> Int+sizeInt SizeZero = 0+sizeInt (SizeSucc sz) = (+1) $! sizeInt sz++-- | The size of an empty context.+zeroSize :: Size 'EmptyCtx+zeroSize = SizeZero++-- | Increment the size to the next value.+incSize :: Size ctx -> Size (ctx '::> tp)+incSize sz = SizeSucc sz++decSize :: Size (ctx '::> tp) -> Size ctx+decSize (SizeSucc sz) = sz++-- | The total size of two concatenated contexts.+addSize :: Size x -> Size y -> Size (x <+> y)+addSize sx SizeZero = sx+addSize sx (SizeSucc sy) = SizeSucc (addSize sx sy)++-- | Allows interpreting a size.+data SizeView (ctx :: Ctx k) where+  ZeroSize :: SizeView 'EmptyCtx+  IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)++-- | View a size as either zero or a smaller size plus one.+viewSize :: Size ctx -> SizeView ctx+viewSize SizeZero = ZeroSize+viewSize (SizeSucc s) = IncSize s++------------------------------------------------------------------------+-- Size++-- | A context that can be determined statically at compiler time.+class KnownContext (ctx :: Ctx k) where+  knownSize :: Size ctx++instance KnownContext 'EmptyCtx where+  knownSize = zeroSize++instance KnownContext ctx => KnownContext (ctx '::> tp) where+  knownSize = incSize knownSize++------------------------------------------------------------------------+-- Diff++-- | Difference in number of elements between two contexts.+-- The first context must be a sub-context of the other.+data Diff (l :: Ctx k) (r :: Ctx k) where+  DiffHere :: Diff ctx ctx+  DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp)++-- | The identity difference.+noDiff :: Diff l l+noDiff = DiffHere++-- | Extend the difference to a sub-context of the right side.+extendRight :: Diff l r -> Diff l (r '::> tp)+extendRight diff = DiffThere diff++composeDiff :: Diff a b -> Diff b c -> Diff a c+composeDiff x DiffHere = x+composeDiff x (DiffThere y) = DiffThere (composeDiff x y)++instance Cat.Category Diff where+  id = DiffHere+  d1 . d2 = composeDiff d2 d1++-- | Extend the size by a given difference.+extSize :: Size l -> Diff l r -> Size r+extSize sz DiffHere = sz+extSize sz (DiffThere diff) = incSize (extSize sz diff)++data DiffView a b where+  NoDiff :: DiffView a a+  ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)++viewDiff :: Diff a b -> DiffView a b+viewDiff DiffHere = NoDiff+viewDiff (DiffThere diff) = ExtendRightDiff diff++------------------------------------------------------------------------+-- KnownDiff++-- | A difference that can be automatically inferred at compile time.+class KnownDiff (l :: Ctx k) (r :: Ctx k) where+  knownDiff :: Diff l r++instance KnownDiff l l where+  knownDiff = noDiff++instance KnownDiff l r => KnownDiff l (r '::> tp) where+  knownDiff = extendRight knownDiff++------------------------------------------------------------------------+-- Index++-- | An index is a reference to a position with a particular type in a+-- context.+data Index (ctx :: Ctx k) (tp :: k) where+  IndexHere :: Size ctx -> Index (ctx '::> tp) tp+  IndexThere :: !(Index ctx tp) -> Index (ctx '::> tp') tp++-- | Convert an index to an 'Int', where the index of the left-most type in the context is 0.+indexVal :: Index ctx tp -> Int+indexVal (IndexHere sz) = sizeInt sz+indexVal (IndexThere idx) = indexVal idx++instance Eq (Index ctx tp) where+  idx1 == idx2 = isJust (testEquality idx1 idx2)++instance TestEquality (Index ctx) where+  testEquality (IndexHere _) (IndexHere _) = Just Refl+  testEquality (IndexHere _) (IndexThere _) = Nothing+  testEquality (IndexThere _) (IndexHere _) = Nothing+  testEquality (IndexThere idx1) (IndexThere idx2) =+     case testEquality idx1 idx2 of+         Just Refl -> Just Refl+         Nothing -> Nothing++instance Ord (Index ctx tp) where+  compare i j = toOrdering (compareF i j)++instance OrdF (Index ctx) where+  compareF (IndexHere _) (IndexHere _) = EQF+  compareF (IndexThere _) (IndexHere _) = LTF+  compareF (IndexHere _) (IndexThere _) = GTF+  compareF (IndexThere idx1) (IndexThere idx2) = lexCompareF idx1 idx2 $ EQF++-- | Index for first element in context.+baseIndex :: Index ('EmptyCtx '::> tp) tp+baseIndex = IndexHere SizeZero++-- | Increase context while staying at same index.+skipIndex :: Index ctx x -> Index (ctx '::> y) x+skipIndex idx = IndexThere idx++-- | Return the index of an element one past the size.+nextIndex :: Size ctx -> Index (ctx '::> tp) tp+nextIndex sz = IndexHere sz++-- | Return the last index of a element.+lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp+lastIndex (SizeSucc s) = IndexHere s++{-# INLINE extendIndex #-}+extendIndex :: KnownDiff l r => Index l tp -> Index r tp+extendIndex = extendIndex' knownDiff++{-# INLINE extendIndex' #-}+extendIndex' :: Diff l r -> Index l tp -> Index r tp+extendIndex' DiffHere idx = idx+extendIndex' (DiffThere diff) idx = IndexThere (extendIndex' diff idx)++-- | Given a size @n@, an initial value @v0@, and a function @f@,+-- @forIndex n v0 f@ calls @f@ on each index less than @n@ starting+-- from @0@ and @v0@, with the value @v@ obtained from the last call.+forIndex :: forall ctx r+          . Size ctx+         -> (forall tp . r -> Index ctx tp -> r)+         -> r+         -> r+forIndex sz_top f = go id sz_top+ where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> r -> r+       go _ SizeZero = id+       go g (SizeSucc sz) = \r -> go (\i -> g (IndexThere i)) sz  $ f r (g (IndexHere sz))++data LDiff (l :: Ctx k) (r :: Ctx k) where+ LDiffHere :: LDiff a a+ LDiffThere :: !(LDiff (a::>x) b) -> LDiff a b++ldiffIndex :: Index a tp -> LDiff a b -> Index b tp+ldiffIndex i LDiffHere = i+ldiffIndex i (LDiffThere d) = ldiffIndex (IndexThere i) d++forIndexLDiff :: Size a+              -> LDiff a b+              -> (forall tp . Index b tp -> r -> r)+              -> r+              -> r+forIndexLDiff _ LDiffHere _ r = r+forIndexLDiff sz (LDiffThere d) f r =+  forIndexLDiff (SizeSucc sz) d f (f (ldiffIndex (IndexHere sz) d) r)++forIndexRangeImpl :: Int+                  -> Size a+                  -> LDiff a b+                  -> (forall tp . Index b tp -> r -> r)+                  -> r+                  -> r+forIndexRangeImpl 0 sz d f r = forIndexLDiff sz d f r+forIndexRangeImpl _ SizeZero _ _ r = r+forIndexRangeImpl i (SizeSucc sz) d f r =+  forIndexRangeImpl (i-1) sz (LDiffThere d) f r++-- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',+-- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and+-- 'f i (forIndexRange (i+1) n v0)' otherwise.+forIndexRange :: Int+              -> Size ctx+              -> (forall tp . Index ctx tp -> r -> r)+              -> r+              -> r+forIndexRange i sz f r = forIndexRangeImpl i sz LDiffHere f r++indexList :: forall ctx. Size ctx -> [Some (Index ctx)]+indexList sz_top = go id [] sz_top+ where go :: (forall tp. Index ctx' tp -> Index ctx tp)+          -> [Some (Index ctx)]+          -> Size ctx'+          -> [Some (Index ctx)]+       go _ ls SizeZero       = ls+       go g ls (SizeSucc sz)  = go (\i -> g (IndexThere i)) (Some (g (IndexHere sz)) : ls) sz++-- | Return index at given integer or nothing if integer is out of bounds.+intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))+intIndex n sz = listToMaybe $ drop n $ indexList sz++instance Show (Index ctx tp) where+   show = show . indexVal++instance ShowF (Index ctx)++------------------------------------------------------------------------+-- Assignment++-- | An assignment is a sequence that maps each index with type 'tp' to+-- a value of type 'f tp'.+data Assignment (f :: k -> Type) (ctx :: Ctx k) where+  AssignmentEmpty :: Assignment f EmptyCtx+  AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)++-- | View an assignment as either empty or an assignment with one appended.+data AssignView (f :: k -> Type) (ctx :: Ctx k) where+  AssignEmpty :: AssignView f EmptyCtx+  AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp)++viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx+viewAssign AssignmentEmpty = AssignEmpty+viewAssign (AssignmentExtend asgn x) = AssignExtend asgn x++instance NFData (Assignment f ctx) where+  rnf AssignmentEmpty = ()+  rnf (AssignmentExtend asgn x) = rnf asgn `seq` x `seq` ()++-- | Return number of elements in assignment.+size :: Assignment f ctx -> Size ctx+size AssignmentEmpty = SizeZero+size (AssignmentExtend asgn _) = SizeSucc (size asgn)++-- | Generate an assignment+generate :: forall ctx f+          . Size ctx+         -> (forall tp . Index ctx tp -> f tp)+         -> Assignment f ctx+generate sz_top f = go id sz_top+ where go :: forall ctx'+           . (forall tp. Index ctx' tp -> Index ctx tp)+          -> Size ctx'+          -> Assignment f ctx'+       go _ SizeZero = AssignmentEmpty+       go g (SizeSucc sz) =+            let ctx = go (\i -> g (IndexThere i)) sz+                x = f (g (IndexHere sz))+             in AssignmentExtend ctx x++-- | Generate an assignment+generateM :: forall ctx m f+           . Applicative m+          => Size ctx+          -> (forall tp . Index ctx tp -> m (f tp))+          -> m (Assignment f ctx)+generateM sz_top f = go id sz_top+ where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> m (Assignment f ctx')+       go _ SizeZero = pure AssignmentEmpty+       go g (SizeSucc sz) =+             AssignmentExtend <$> (go (\i -> g (IndexThere i)) sz) <*> f (g (IndexHere sz))++-- | @replicate n@ make a context with different copies of the same+-- polymorphic value.+replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx+replicate n c = generate n (\_ -> c)++-- | Create empty indexec vector.+empty :: Assignment f 'EmptyCtx+empty = AssignmentEmpty++extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)+extend asgn e = AssignmentExtend asgn e++{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}+adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)++{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}+update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx+update i v a = adjust (\_ -> v) i a++adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)+adjustM f = go (\x -> x)+ where+  go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')+  go g (IndexHere _)     (AssignmentExtend asgn x) = AssignmentExtend (map g asgn) <$> f (g x)+  go g (IndexThere idx)  (AssignmentExtend asgn x) = flip AssignmentExtend (g x)   <$> go g idx asgn+#if !MIN_VERSION_base(4,9,0)+-- GHC 7.10.3 and early does not recognize that the above definition is complete,+-- and so need the equation below.  GHC 8.0.1 does not require the additional+-- equation.+  go _ _ _ = error "SafeTypeContext.adjustM: impossible!"+#endif++type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx+type instance IxValueF (Assignment (f :: k -> Type) ctx) = f++instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where+  ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)+  ixF idx f = adjustM f idx++instance forall (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where+  ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)+  ixF' idx f = adjustM f idx++idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp+idxlookup f (AssignmentExtend _   x) (IndexHere _) = f x+idxlookup f (AssignmentExtend ctx _) (IndexThere idx) = idxlookup f ctx idx+idxlookup _ AssignmentEmpty _ = error "Data.Parameterized.Context.Safe.lookup: impossible case"++-- | Return value of assignment.+(!) :: Assignment f ctx -> Index ctx tp -> f tp+(!) asgn idx = idxlookup id asgn idx++-- | Return value of assignment, where the index is into an+--   initial sequence of the assignment.+(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp+a !^ i = a ! extendIndex i++instance TestEquality f => Eq (Assignment f ctx) where+  x == y = isJust (testEquality x y)++testEq :: (forall x y. f x -> f y -> Maybe (x :~: y))+       -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)+testEq _ AssignmentEmpty AssignmentEmpty = Just Refl+testEq test (AssignmentExtend ctx1 x1) (AssignmentExtend ctx2 x2) =+     case testEq test ctx1 ctx2 of+       Nothing -> Nothing+       Just Refl ->+          case test x1 x2 of+             Nothing -> Nothing+             Just Refl -> Just Refl+testEq _ AssignmentEmpty AssignmentExtend{} = Nothing+testEq _ AssignmentExtend{} AssignmentEmpty = Nothing++instance TestEqualityFC Assignment where+   testEqualityFC = testEq+instance TestEquality f => TestEquality (Assignment f) where+   testEquality x y = testEq testEquality x y+instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where+  polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y++compareAsgn :: (forall x y. f x -> f y -> OrderingF x y)+            -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2+compareAsgn _ AssignmentEmpty AssignmentEmpty = EQF+compareAsgn _ AssignmentEmpty _ = GTF+compareAsgn _ _ AssignmentEmpty = LTF+compareAsgn test (AssignmentExtend ctx1 x) (AssignmentExtend ctx2 y) =+  case compareAsgn test ctx1 ctx2 of+    LTF -> LTF+    GTF -> GTF+    EQF -> case test x y of+              LTF -> LTF+              GTF -> GTF+              EQF -> EQF++instance OrdFC Assignment where+  compareFC = compareAsgn++instance OrdF f => OrdF (Assignment f) where+  compareF = compareAsgn compareF++instance OrdF f => Ord (Assignment f ctx) where+  compare x y = toOrdering (compareF x y)+++instance Hashable (Index ctx tp) where+  hashWithSalt = hashWithSaltF+instance HashableF (Index ctx) where+  hashWithSaltF s i = hashWithSalt s (indexVal i)++instance HashableF f => HashableF (Assignment f) where+  hashWithSaltF = hashWithSalt++instance HashableF f => Hashable (Assignment f ctx) where+  hashWithSalt s AssignmentEmpty = s+  hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x++instance ShowF f => Show (Assignment f ctx) where+  show a = "[" ++ intercalate ", " (toList showF a) ++ "]"++instance ShowF f => ShowF (Assignment f)++instance FunctorFC Assignment where+  fmapFC = fmapFCDefault++instance FoldableFC Assignment where+  foldMapFC = foldMapFCDefault++instance TraversableFC Assignment where+  traverseFC = traverseF++-- | Map assignment+map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c+map = fmapFC++traverseF :: forall (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)+           . Applicative m+          => (forall tp . f tp -> m (g tp))+          -> Assignment f c+          -> m (Assignment g c)+traverseF _ AssignmentEmpty = pure AssignmentEmpty+traverseF f (AssignmentExtend asgn x) = pure AssignmentExtend <*> traverseF f asgn <*> f x++-- | Convert assignment to list.+toList :: (forall tp . f tp -> a)+       -> Assignment f c+       -> [a]+toList = toListFC++zipWithM :: Applicative m+         => (forall tp . f tp -> g tp -> m (h tp))+         -> Assignment f c+         -> Assignment g c+         -> m (Assignment h c)+zipWithM f x y = go x y+ where go AssignmentEmpty AssignmentEmpty = pure AssignmentEmpty+       go (AssignmentExtend asgn1 x1) (AssignmentExtend asgn2 x2) =+             AssignmentExtend <$> (zipWithM f asgn1 asgn2) <*> (f x1 x2)++zipWith :: (forall x . f x -> g x -> h x)+        -> Assignment f a+        -> Assignment g a+        -> Assignment h a+zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y+{-# INLINE zipWith #-}++traverseWithIndex :: Applicative m+                  => (forall tp . Index ctx tp -> f tp -> m (g tp))+                  -> Assignment f ctx+                  -> m (Assignment g ctx)+traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i)++(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)+x <++> AssignmentEmpty = x+x <++> AssignmentExtend y t = AssignmentExtend (x <++> y) t++------------------------------------------------------------------------+-- KnownRepr instances++instance (KnownRepr (Assignment f) ctx, KnownRepr f bt)+      => KnownRepr (Assignment f) (ctx ::> bt) where+  knownRepr = knownRepr `extend` knownRepr++instance KnownRepr (Assignment f) EmptyCtx where+  knownRepr = empty++--------------------------------------------------------------------------------------+-- lookups and update for lenses++data MyNat where+  MyZ :: MyNat+  MyS :: MyNat -> MyNat++type MyZ = 'MyZ+type MyS = 'MyS++data MyNatRepr :: MyNat -> Type where+  MyZR :: MyNatRepr MyZ+  MySR :: MyNatRepr n -> MyNatRepr (MyS n)++type family StrongCtxUpdate (n::MyNat) (ctx::Ctx k) (z::k) :: Ctx k where+  StrongCtxUpdate n       EmptyCtx     z = EmptyCtx+  StrongCtxUpdate MyZ     (ctx::>x)    z = ctx ::> z+  StrongCtxUpdate (MyS n) (ctx::>x)    z = (StrongCtxUpdate n ctx z) ::> x++type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> Type) :: Type where+  MyNatLookup n       EmptyCtx  f = ()+  MyNatLookup MyZ     (ctx::>x) f = f x+  MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f++mynat_lookup :: MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f+mynat_lookup _   AssignmentEmpty = ()+mynat_lookup MyZR     (AssignmentExtend _    x) = x+mynat_lookup (MySR n) (AssignmentExtend asgn _) = mynat_lookup n asgn++strong_ctx_update :: MyNatRepr n -> Assignment f ctx -> f tp -> Assignment f (StrongCtxUpdate n ctx tp)+strong_ctx_update _        AssignmentEmpty           _ = AssignmentEmpty+strong_ctx_update MyZR     (AssignmentExtend asgn _) z = AssignmentExtend asgn z+strong_ctx_update (MySR n) (AssignmentExtend asgn x) z = AssignmentExtend (strong_ctx_update n asgn z) x++------------------------------------------------------------------------+-- 1 field lens combinators++type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1)++instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where++  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 2 field lens combinators++type Assignment2 f x1 x2+   = Assignment f ('EmptyCtx '::> x1 '::> x2)++instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR+++------------------------------------------------------------------------+-- 3 field lens combinators++type Assignment3 f x1 x2 x3+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3)++instance Lens.Field1 (Assignment3 f t x2 x3)+                     (Assignment3 f u x2 x3)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment3 f x1 t x3)+                     (Assignment3 f x1 u x3)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field3 (Assignment3 f x1 x2 t)+                     (Assignment3 f x1 x2 u)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 4 field lens combinators++type Assignment4 f x1 x2 x3 x4+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4)++instance Lens.Field1 (Assignment4 f t x2 x3 x4)+                     (Assignment4 f u x2 x3 x4)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment4 f x1 t x3 x4)+                     (Assignment4 f x1 u x3 x4)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment4 f x1 x2 t x4)+                     (Assignment4 f x1 x2 u x4)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field4 (Assignment4 f x1 x2 x3 t)+                     (Assignment4 f x1 x2 x3 u)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR+++------------------------------------------------------------------------+-- 5 field lens combinators++type Assignment5 f x1 x2 x3 x4 x5+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5)++instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5)+                     (Assignment5 f u x2 x3 x4 x5)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5)+                     (Assignment5 f x1 u x3 x4 x5)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5)+                     (Assignment5 f x1 x2 u x4 x5)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5)+                     (Assignment5 f x1 x2 x3 u x5)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t)+                     (Assignment5 f x1 x2 x3 x4 u)+                     (f t)+                     (f u) where+  _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 6 field lens combinators++type Assignment6 f x1 x2 x3 x4 x5 x6+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6)++instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6)+                     (Assignment6 f u x2 x3 x4 x5 x6)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6)+                     (Assignment6 f x1 u x3 x4 x5 x6)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6)+                     (Assignment6 f x1 x2 u x4 x5 x6)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6)+                     (Assignment6 f x1 x2 x3 u x5 x6)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6)+                     (Assignment6 f x1 x2 x3 x4 u x6)+                     (f t)+                     (f u) where+  _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t)+                     (Assignment6 f x1 x2 x3 x4 x5 u)+                     (f t)+                     (f u) where+  _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 7 field lens combinators++type Assignment7 f x1 x2 x3 x4 x5 x6 x7+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7)++instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7)+                     (Assignment7 f u x2 x3 x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7)+                     (Assignment7 f x1 u x3 x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7)+                     (Assignment7 f x1 x2 u x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7)+                     (Assignment7 f x1 x2 x3 u x5 x6 x7)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7)+                     (Assignment7 f x1 x2 x3 x4 u x6 x7)+                     (f t)+                     (f u) where+  _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7)+                     (Assignment7 f x1 x2 x3 x4 x5 u x7)+                     (f t)+                     (f u) where+  _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t)+                     (Assignment7 f x1 x2 x3 x4 x5 x6 u)+                     (f t)+                     (f u) where+  _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 8 field lens combinators++type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8)++instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)+                     (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR+++instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)+                     (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)+                     (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)+                     (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)+                     (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)+                     (f t)+                     (f u) where+  _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)+                     (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)+                     (f t)+                     (f u) where+  _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)+                     (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)+                     (f t)+                     (f u) where+  _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)+                     (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)+                     (f t)+                     (f u) where+  _8 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR++------------------------------------------------------------------------+-- 9 field lens combinators++type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9)+++instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)+                     (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)+                     (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)+                     (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)+                     (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)+                     (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MySR $ MyZR++instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)+                     (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)+                     (f t)+                     (f u) where+  _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MySR $ MyZR++instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)+                     (f t)+                     (f u) where+  _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MySR $ MyZR++instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)+                     (f t)+                     (f u) where+  _8 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MySR $ MyZR++instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)+                     (f t)+                     (f u) where+  _9 = Lens.lens (mynat_lookup n) (strong_ctx_update n)+        where n = MyZR

@@ -0,0 +1,1213 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeInType #-}+module Data.Parameterized.Context.Unsafe+  ( module Data.Parameterized.Ctx+  , KnownContext(..)+    -- * Size+  , Size+  , sizeInt+  , zeroSize+  , incSize+  , decSize+  , extSize+  , addSize+  , SizeView(..)+  , viewSize+    -- * Diff+  , Diff+  , noDiff+  , extendRight+  , DiffView(..)+  , viewDiff+  , KnownDiff(..)+    -- * Indexing+  , Index+  , indexVal+  , baseIndex+  , skipIndex+  , lastIndex+  , nextIndex+  , extendIndex+  , extendIndex'+  , forIndex+  , forIndexRange+  , intIndex+    -- ** IndexRange+  , IndexRange+  , allRange+  , indexOfRange+  , dropHeadRange+  , dropTailRange+    -- * Assignments+  , Assignment+  , size+  , Data.Parameterized.Context.Unsafe.replicate+  , generate+  , generateM+  , empty+  , extend+  , adjust+  , update+  , adjustM+  , AssignView(..)+  , viewAssign+  , (!)+  , (!^)+  , Data.Parameterized.Context.Unsafe.zipWith+  , zipWithM+  , (<++>)+  , traverseWithIndex+  ) where++import qualified Control.Category as Cat+import           Control.DeepSeq+import           Control.Exception+import qualified Control.Lens as Lens+import           Control.Monad.Identity (Identity(..))+import           Data.Bits+import           Data.Coerce+import           Data.Hashable+import           Data.List (intercalate)+import           Data.Proxy+import           Unsafe.Coerce+import           Data.Kind(Type)++import           Data.Parameterized.Classes+import           Data.Parameterized.Ctx+import           Data.Parameterized.Ctx.Proofs+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC++------------------------------------------------------------------------+-- Size++-- | Represents the size of a context.+newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int }++type role Size nominal++-- | The size of an empty context.+zeroSize :: Size 'EmptyCtx+zeroSize = Size 0++-- | Increment the size to the next value.+incSize :: Size ctx -> Size (ctx '::> tp)+incSize (Size n) = Size (n+1)++decSize :: Size (ctx '::> tp) -> Size ctx+decSize (Size n) = assert (n > 0) (Size (n-1))++-- | Allows interpreting a size.+data SizeView (ctx :: Ctx k) where+  ZeroSize :: SizeView 'EmptyCtx+  IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)++-- | Project a size+viewSize :: Size ctx -> SizeView ctx+viewSize (Size 0) = unsafeCoerce ZeroSize+viewSize (Size n) = assert (n > 0) (unsafeCoerce (IncSize (Size (n-1))))++instance Show (Size ctx) where+  show (Size i) = show i++-- | A context that can be determined statically at compiler time.+class KnownContext (ctx :: Ctx k) where+  knownSize :: Size ctx++instance KnownContext 'EmptyCtx where+  knownSize = zeroSize++instance KnownContext ctx => KnownContext (ctx '::> tp) where+  knownSize = incSize knownSize++------------------------------------------------------------------------+-- Diff++-- | Difference in number of elements between two contexts.+-- The first context must be a sub-context of the other.+newtype Diff (l :: Ctx k) (r :: Ctx k)+      = Diff { _contextExtSize :: Int }++-- | The identity difference.+noDiff :: Diff l l+noDiff = Diff 0++-- | 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)++instance Cat.Category Diff where+  id = Diff 0+  Diff j . Diff i = Diff (i + j)++-- | Extend the size by a given difference.+extSize :: Size l -> Diff l r -> Size r+extSize (Size i) (Diff j) = Size (i+j)++-- | The total size of two concatenated contexts.+addSize :: Size x -> Size y -> Size (x <+> y)+addSize (Size x) (Size y) = Size (x + y)+++data DiffView a b where+  NoDiff :: DiffView a a+  ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)++viewDiff :: Diff a b -> DiffView a b+viewDiff (Diff i)+  | i == 0 = unsafeCoerce NoDiff+  | otherwise  = assert (i > 0) $ unsafeCoerce $ ExtendRightDiff (Diff (i-1))++------------------------------------------------------------------------+-- KnownDiff++-- | A difference that can be automatically inferred at compile time.+class KnownDiff (l :: Ctx k) (r :: Ctx k) where+  knownDiff :: Diff l r++instance KnownDiff l l where+  knownDiff = noDiff++instance {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where+  knownDiff = extendRight knownDiff++------------------------------------------------------------------------+-- Index++-- | An index is a reference to a position with a particular type in a+-- context.+newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int }++type role Index nominal nominal++instance Eq (Index ctx tp) where+  Index i == Index j = i == j++instance TestEquality (Index ctx) where+  testEquality (Index i) (Index j)+    | i == j = Just (unsafeCoerce Refl)+    | otherwise = Nothing++instance Ord (Index ctx tp) where+  Index i `compare` Index j = compare i j++instance OrdF (Index ctx) where+  compareF (Index i) (Index j)+    | i < j = LTF+    | i == j = unsafeCoerce EQF+    | otherwise = GTF++-- | Index for first element in context.+baseIndex :: Index ('EmptyCtx '::> tp) tp+baseIndex = Index 0++-- | Increase context while staying at same index.+skipIndex :: Index ctx x -> Index (ctx '::> y) x+skipIndex (Index i) = Index i++-- | Return the index of a element one past the size.+nextIndex :: Size ctx -> Index (ctx ::> tp) tp+nextIndex n = Index (sizeInt n)++-- | Return the last index of a element.+lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp+lastIndex n = Index (sizeInt n - 1)++{-# INLINE extendIndex #-}+extendIndex :: KnownDiff l r => Index l tp -> Index r tp+extendIndex = extendIndex' knownDiff++{-# INLINE extendIndex' #-}+extendIndex' :: Diff l r -> Index l tp -> Index r tp+extendIndex' _ = unsafeCoerce++-- | Given a size 'n', an initial value 'v0', and a function 'f', 'forIndex n v0 f'+-- is equivalent to 'v0' when 'n' is zero, and 'f (forIndex (n-1) v0) (n-1)' otherwise.+forIndex :: forall ctx r+          . Size ctx+         -> (forall tp . r -> Index ctx tp -> r)+         -> r+         -> r+forIndex n f r =+  case viewSize n of+    ZeroSize -> r+    IncSize p -> f (forIndex p (coerce f) r) (nextIndex p)++-- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',+-- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and+-- 'f i (forIndexRange (i+1) n v0)' otherwise.+forIndexRange :: forall ctx r+               . Int+              -> Size ctx+              -> (forall tp . Index ctx tp -> r -> r)+              -> r+              -> r+forIndexRange i (Size n) f r+  | i >= n = r+  | otherwise = f (Index i) (forIndexRange (i+1) (Size n) f r)++-- | Return index at given integer or nothing if integer is out of bounds.+intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))+intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))+             | otherwise = Nothing++instance Show (Index ctx tp) where+   show = show . indexVal++instance ShowF (Index ctx)++------------------------------------------------------------------------+-- IndexRange++-- | This represents a contiguous range of indices.+data IndexRange (ctx :: Ctx k) (sub :: Ctx k)+   = IndexRange {-# UNPACK #-} !Int+                {-# UNPACK #-} !Int++-- | Return a range containing all indices in the context.+allRange :: Size ctx -> IndexRange ctx ctx+allRange (Size n) = IndexRange 0 n++-- | `indexOfRange` returns the only index in a range.+indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e+indexOfRange (IndexRange i n) = assert (n == 1) $ Index i++-- | `dropTailRange r n` drops the last `n` elements in `r`.+dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x+dropTailRange (IndexRange i n) (Size j) = assert (n >= j) $ IndexRange i (n - j)++-- | `dropHeadRange r n` drops the first `n` elements in `r`.+dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y+dropHeadRange (IndexRange i n) (Size j) = assert (i' >= i && n >= j) $ IndexRange i' (n - j)+  where i' = i + j++------------------------------------------------------------------------+-- Height++data Height = Zero | Succ Height++type family Pred (k :: Height) :: Height+type instance Pred ('Succ h) = h++------------------------------------------------------------------------+-- BalancedTree++-- | A balanced tree where all leaves are at the same height.+--+-- The first parameter is the height of the tree.+-- The second is the parameterized value.+data BalancedTree h (f :: k -> Type) (p :: Ctx k) where+  BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)+  BalPair :: !(BalancedTree h f x)+          -> !(BalancedTree h f y)+          -> BalancedTree ('Succ h) f (x <+> y)++bal_size :: BalancedTree h f p -> Int+bal_size (BalLeaf _) = 1+bal_size (BalPair x y) = bal_size x + bal_size y+++instance TestEqualityFC (BalancedTree h) where+  testEqualityFC test (BalLeaf x) (BalLeaf y) = do+    Refl <- test x y+    return Refl+  testEqualityFC test (BalPair x1 x2) (BalPair y1 y2) = do+    Refl <- testEqualityFC test x1 y1+    Refl <- testEqualityFC test x2 y2+    return Refl+#if !MIN_VERSION_base(4,9,0)+  testEqualityFC _ _ _ = Nothing+#endif++instance OrdFC (BalancedTree h) where+  compareFC test (BalLeaf x) (BalLeaf y) =+    joinOrderingF (test x y) $ EQF+#if !MIN_VERSION_base(4,9,0)+  compareFC _ BalLeaf{} _ = LTF+  compareFC _ _ BalLeaf{} = GTF+#endif+  compareFC test (BalPair x1 x2) (BalPair y1 y2) =+    joinOrderingF (compareFC test x1 y1) $+    joinOrderingF (compareFC test x2 y2) $+    EQF++instance HashableF f => HashableF (BalancedTree h f) where+  hashWithSaltF s t =+    case t of+      BalLeaf x -> s `hashWithSaltF` x+      BalPair x y -> s `hashWithSaltF` x `hashWithSaltF` y++fmap_bal :: (forall tp . f tp -> g tp)+         -> BalancedTree h f c+         -> BalancedTree h g c+fmap_bal = go+  where go :: (forall tp . f tp -> g tp)+              -> BalancedTree h f c+              -> BalancedTree h g c+        go f (BalLeaf x) = BalLeaf (f x)+        go f (BalPair x y) = BalPair (go f x) (go f y)+{-# INLINABLE fmap_bal #-}++traverse_bal :: Applicative m+             => (forall tp . f tp -> m (g tp))+             -> BalancedTree h f c+             -> m (BalancedTree h g c)+traverse_bal = go+  where go :: Applicative m+              => (forall tp . f tp -> m (g tp))+              -> BalancedTree h f c+              -> m (BalancedTree h g c)+        go f (BalLeaf x) = BalLeaf <$> f x+        go f (BalPair x y) = BalPair <$> go f x <*> go f y+{-# INLINABLE traverse_bal #-}++instance ShowF f => Show (BalancedTree h f tp) where+  show (BalLeaf x) = showF x+  show (BalPair x y) = "BalPair " Prelude.++ show x Prelude.++ " " Prelude.++ show y++instance ShowF f => ShowF (BalancedTree h f)++unsafe_bal_generate :: forall ctx h f t+                     . Int -- ^ Height of tree to generate+                    -> Int -- ^ Starting offset for entries.+                    -> (forall tp . Index ctx tp -> f tp)+                    -> BalancedTree h f t+unsafe_bal_generate h o f+  | h <  0 = error "unsafe_bal_generate given negative height"+  | h == 0 = unsafeCoerce $ BalLeaf (f (Index o))+  | otherwise =+    let l = unsafe_bal_generate (h-1) o f+        o' = o + 1 `shiftL` (h-1)+        u = assert (o + bal_size l == o') $ unsafe_bal_generate (h-1) o' f+     in unsafeCoerce $ BalPair l u++unsafe_bal_generateM :: forall m ctx h f t+                      . Applicative m+                     => Int -- ^ Height of tree to generate+                     -> Int -- ^ Starting offset for entries.+                     -> (forall x . Index ctx x -> m (f x))+                     -> m (BalancedTree h f t)+unsafe_bal_generateM h o f+  | h == 0 = unsafeCoerce . BalLeaf <$> f (Index o)+  | otherwise =+    let o' = o + 1 `shiftL` (h-1)+        g lv uv = assert (o' == o + bal_size lv) $+           unsafeCoerce (BalPair lv uv)+      in g <$> unsafe_bal_generateM (h-1) o  f+           <*> unsafe_bal_generateM (h-1) o' f++-- | Lookup index in tree.+unsafe_bal_index :: BalancedTree h f a -- ^ Tree to lookup.+                 -> Int -- ^ Index to lookup.+                 -> Int  -- ^ Height of tree+                 -> f tp+unsafe_bal_index _ j i+  | seq j $ seq i $ False = error "bad unsafe_bal_index"+unsafe_bal_index (BalLeaf u) _ i = assert (i == 0) $ unsafeCoerce u+unsafe_bal_index (BalPair x y) j i+  | j `testBit` (i-1) = unsafe_bal_index y j $! (i-1)+  | otherwise         = unsafe_bal_index x j $! (i-1)++-- | Update value at index in tree.+unsafe_bal_adjust :: Functor m+                  => (f x -> m (f y))+                  -> BalancedTree h f a -- ^ Tree to update+                  -> Int -- ^ Index to lookup.+                  -> Int  -- ^ Height of tree+                  -> m (BalancedTree h f b)+unsafe_bal_adjust f (BalLeaf u) _ i = assert (i == 0) $+  (unsafeCoerce . BalLeaf <$> (f (unsafeCoerce u)))+unsafe_bal_adjust f (BalPair x y) j i+  | j `testBit` (i-1) = (unsafeCoerce . BalPair x      <$> (unsafe_bal_adjust f y j (i-1)))+  | otherwise         = (unsafeCoerce . flip BalPair y <$> (unsafe_bal_adjust f x j (i-1)))++{-# SPECIALIZE unsafe_bal_adjust+     :: (f x -> Identity (f y))+     -> BalancedTree h f a+     -> Int+     -> Int+     -> Identity (BalancedTree h f b)+  #-}++-- | Zip two balanced trees together.+bal_zipWithM :: Applicative m+             => (forall x . f x -> g x -> m (h x))+             -> BalancedTree u f a+             -> BalancedTree u g a+             -> m (BalancedTree u h a)+bal_zipWithM f (BalLeaf x) (BalLeaf y) = BalLeaf <$> f x y+bal_zipWithM f (BalPair x1 x2) (BalPair y1 y2) =+  BalPair <$> bal_zipWithM f x1 (unsafeCoerce y1)+          <*> bal_zipWithM f x2 (unsafeCoerce y2)+#if !MIN_VERSION_base(4,9,0)+bal_zipWithM _ _ _ = error "ilegal args to bal_zipWithM"+#endif+{-# INLINABLE bal_zipWithM #-}++------------------------------------------------------------------------+-- BinomialTree++data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where+  Empty :: BinomialTree h f EmptyCtx++  -- Contains size of the subtree, subtree, then element.+  PlusOne  :: !Int+           -> !(BinomialTree ('Succ h) f x)+           -> !(BalancedTree h f y)+           -> BinomialTree h f (x <+> y)++  -- Contains size of the subtree, subtree, then element.+  PlusZero  :: !Int+            -> !(BinomialTree ('Succ h) f x)+            -> BinomialTree h f x++tsize :: BinomialTree h f a -> Int+tsize Empty = 0+tsize (PlusOne s _ _) = 2*s+1+tsize (PlusZero  s _) = 2*s++t_cnt_size :: BinomialTree h f a -> Int+t_cnt_size Empty = 0+t_cnt_size (PlusOne _ l r) = t_cnt_size l + bal_size r+t_cnt_size (PlusZero  _ l) = t_cnt_size l++-- | Concatenate a binomial tree and a balanced tree.+append :: BinomialTree h f x+       -> BalancedTree h f y+       -> BinomialTree h f (x <+> y)+append Empty y = PlusOne 0 Empty y+append (PlusOne _ t x) y =+  case assoc t x y of+    Refl ->+      let t' = append t (BalPair x y)+       in PlusZero (tsize t') t'+append (PlusZero s t) x = PlusOne s t x++instance TestEqualityFC (BinomialTree h) where+  testEqualityFC _ Empty Empty = return Refl+  testEqualityFC test (PlusZero _ x1) (PlusZero _ y1) = do+    Refl <- testEqualityFC test x1 y1+    return Refl+  testEqualityFC test (PlusOne _ x1 x2) (PlusOne _ y1 y2) = do+    Refl <- testEqualityFC test x1 y1+    Refl <- testEqualityFC test x2 y2+    return Refl+  testEqualityFC _ _ _ = Nothing++instance OrdFC (BinomialTree h) where+  compareFC _ Empty Empty = EQF+  compareFC _ Empty _ = LTF+  compareFC _ _ Empty = GTF++  compareFC test (PlusZero _ x1) (PlusZero _ y1) =+    joinOrderingF (compareFC test x1 y1) $ EQF+  compareFC _ PlusZero{} _ = LTF+  compareFC _ _ PlusZero{} = GTF++  compareFC test (PlusOne _ x1 x2) (PlusOne _ y1 y2) =+    joinOrderingF (compareFC test x1 y1) $+    joinOrderingF (compareFC test x2 y2) $+    EQF++instance HashableF f => HashableF (BinomialTree h f) where+  hashWithSaltF s t =+    case t of+      Empty -> s+      PlusZero _ x   -> s `hashWithSaltF` x+      PlusOne  _ x y -> s `hashWithSaltF` x `hashWithSaltF` y++-- | Map over a binary tree.+fmap_bin :: (forall tp . f tp -> g tp)+         -> BinomialTree h f c+         -> BinomialTree h g c+fmap_bin _ Empty = Empty+fmap_bin f (PlusOne s t x) = PlusOne s (fmap_bin f t) (fmap_bal f x)+fmap_bin f (PlusZero s t)  = PlusZero s (fmap_bin f t)+{-# INLINABLE fmap_bin #-}++traverse_bin :: Applicative m+             => (forall tp . f tp -> m (g tp))+             -> BinomialTree h f c+             -> m (BinomialTree h g c)+traverse_bin _ Empty = pure Empty+traverse_bin f (PlusOne s t x) = PlusOne s  <$> traverse_bin f t <*> traverse_bal f x+traverse_bin f (PlusZero s t)  = PlusZero s <$> traverse_bin f t+{-# INLINABLE traverse_bin #-}++unsafe_bin_generate :: forall h f ctx t+                     . Int -- ^ Size of tree to generate+                    -> Int -- ^ Height of each element.+                    -> (forall x . Index ctx x -> f x)+                    -> BinomialTree h f t+unsafe_bin_generate sz h f+  | sz == 0 = unsafeCoerce Empty+  | sz `testBit` 0 =+    let s = sz `shiftR` 1+        t = unsafe_bin_generate s (h+1) f+        o = s * 2^(h+1)+        u = assert (o == t_cnt_size t) $ unsafe_bal_generate h o f+     in unsafeCoerce (PlusOne s t u)+  | otherwise =+    let s = sz `shiftR` 1+        t = unsafe_bin_generate (sz `shiftR` 1) (h+1) f+        r :: BinomialTree h f t+        r = PlusZero s t+    in r++unsafe_bin_generateM :: forall m h f ctx t+                      . Applicative m+                     => Int -- ^ Size of tree to generate+                     -> Int -- ^ Height of each element.+                     -> (forall x . Index ctx x -> m (f x))+                     -> m (BinomialTree h f t)+unsafe_bin_generateM sz h f+  | sz == 0 = pure (unsafeCoerce Empty)+  | sz `testBit` 0 =+    let s = sz `shiftR` 1+        t = unsafe_bin_generateM s (h+1) f+        -- Next offset+        o = s * 2^(h+1)+        u = unsafe_bal_generateM h o f+        r = unsafeCoerce (PlusOne s) <$> t <*> u+     in r+  | otherwise =+    let s = sz `shiftR` 1+        t = unsafe_bin_generateM s (h+1) f+        r :: m (BinomialTree h f t)+        r = PlusZero s <$> t+     in r++------------------------------------------------------------------------+-- Dropping++data DropResult f (ctx :: Ctx k) where+  DropEmpty :: DropResult f EmptyCtx+  DropExt   :: BinomialTree 'Zero f x+            -> f y+            -> DropResult f (x ::> y)++-- | 'bal_drop x y' returns the tree formed 'append x (init y)'+bal_drop :: forall h f x y+          . BinomialTree h f x+            -- ^ Bina+         -> BalancedTree h f y+         -> DropResult f (x <+> y)+bal_drop t (BalLeaf e) = DropExt t e+bal_drop t (BalPair x y) =+  unsafeCoerce (bal_drop (PlusOne (tsize t) (unsafeCoerce t) x) y)++bin_drop :: forall h f ctx+          . BinomialTree h f ctx+         -> DropResult f ctx+bin_drop Empty = DropEmpty+bin_drop (PlusZero _ u) = bin_drop u+bin_drop (PlusOne s t u) =+  let m = case t of+            Empty -> Empty+            _ -> PlusZero s t+   in bal_drop m u++------------------------------------------------------------------------+-- Indexing++-- | Lookup value in tree.+unsafe_bin_index :: BinomialTree h f a -- ^ Tree to lookup in.+                 -> Int+                 -> Int -- ^ Size of tree+                 -> f u+unsafe_bin_index _ _ i+  | seq i False = error "bad unsafe_bin_index"+unsafe_bin_index Empty _ _ = error "unsafe_bin_index reached end of list"+unsafe_bin_index (PlusOne sz t u) j i+  | sz == j `shiftR` (1+i) = unsafe_bal_index u j i+  | otherwise = unsafe_bin_index t j $! (1+i)+unsafe_bin_index (PlusZero sz t) j i+  | sz == j `shiftR` (1+i) = error "unsafe_bin_index stopped at PlusZero"+  | otherwise = unsafe_bin_index t j $! (1+i)++-- | Lookup value in tree.+unsafe_bin_adjust :: forall m h f x y a b+                   . Functor m+                  => (f x -> m (f y))+                  -> BinomialTree h f a -- ^ Tree to lookup in.+                  -> Int+                  -> Int -- ^ Size of tree+                  -> m (BinomialTree h f b)+unsafe_bin_adjust _ Empty _ _ = error "unsafe_bin_adjust reached end of list"+unsafe_bin_adjust f (PlusOne sz t u) j i+  | sz == j `shiftR` (1+i) =+    unsafeCoerce . PlusOne sz t        <$> (unsafe_bal_adjust f u j i)+  | otherwise =+    unsafeCoerce . flip (PlusOne sz) u <$> (unsafe_bin_adjust f t j (i+1))+unsafe_bin_adjust f (PlusZero sz t) j i+  | sz == j `shiftR` (1+i) = error "unsafe_bin_adjust stopped at PlusZero"+  | otherwise = PlusZero sz <$> (unsafe_bin_adjust f t j (i+1))+++{-# SPECIALIZE unsafe_bin_adjust+     :: (f x -> Identity (f y))+     -> BinomialTree h f a+     -> Int+     -> Int+     -> Identity (BinomialTree h f b)+  #-}++tree_zipWithM :: Applicative m+             => (forall x . f x -> g x -> m (h x))+             -> BinomialTree u f a+             -> BinomialTree u g a+             -> m (BinomialTree u h a)+tree_zipWithM _ Empty Empty = pure Empty+tree_zipWithM f (PlusOne s x1 x2) (PlusOne _ y1 y2) =+  PlusOne s <$> tree_zipWithM f x1 (unsafeCoerce y1)+            <*> bal_zipWithM  f x2 (unsafeCoerce y2)+tree_zipWithM f (PlusZero s x1) (PlusZero _ y1) =+  PlusZero s <$> tree_zipWithM f x1 y1+tree_zipWithM _ _ _ = error "ilegal args to tree_zipWithM"+{-# INLINABLE tree_zipWithM #-}++------------------------------------------------------------------------+-- Assignment++-- | An assignment is a sequence that maps each index with type 'tp' to+-- a value of type 'f tp'.+--+-- This assignment implementation uses a binomial tree implementation+-- that offers lookups and updates in time and space logarithmic with+-- respect to the number of elements in the context.+newtype Assignment (f :: k -> Type) (ctx :: Ctx k)+      = Assignment (BinomialTree 'Zero f ctx)++type role Assignment nominal nominal++instance NFData (Assignment f ctx) where+  rnf a = seq a ()++-- | Return number of elements in assignment.+size :: Assignment f ctx -> Size ctx+size (Assignment t) = Size (tsize t)++-- | @replicate n@ make a context with different copies of the same+-- polymorphic value.+replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx+replicate n c = generate n (\_ -> c)++-- | Generate an assignment+generate :: Size ctx+         -> (forall tp . Index ctx tp -> f tp)+         -> Assignment f ctx+generate n f  = Assignment r+  where r = unsafe_bin_generate (sizeInt n) 0 f+{-# NOINLINE generate #-}++-- | Generate an assignment+generateM :: Applicative m+          => Size ctx+          -> (forall tp . Index ctx tp -> m (f tp))+          -> m (Assignment f ctx)+generateM n f = Assignment <$> unsafe_bin_generateM (sizeInt n) 0 f+{-# NOINLINE generateM #-}++-- | Return empty assignment+empty :: Assignment f EmptyCtx+empty = Assignment Empty++extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)+extend (Assignment x) y = Assignment $ append x (BalLeaf y)++-- | Unexported index that returns an arbitrary type of expression.+unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u+unsafeIndex _ idx (Assignment t) = seq t $ unsafe_bin_index t idx 0++-- | Return value of assignment.+(!) :: Assignment f ctx -> Index ctx tp -> f tp+a ! Index i = assert (0 <= i && i < sizeInt (size a)) $+              unsafeIndex Proxy i a++-- | Return value of assignment, where the index is into an+--   initial sequence of the assignment.+(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp+a !^ i = a ! extendIndex i++instance TestEqualityFC Assignment where+   testEqualityFC test (Assignment x) (Assignment y) = do+     Refl <- testEqualityFC test x y+     return Refl++instance TestEquality f => TestEquality (Assignment f) where+  testEquality = testEqualityFC testEquality++instance TestEquality f => Eq (Assignment f ctx) where+  x == y = isJust (testEquality x y)++instance OrdFC Assignment where+  compareFC test (Assignment x) (Assignment y) =+     joinOrderingF (compareFC test x y) $ EQF++instance OrdF f => OrdF (Assignment f) where+  compareF = compareFC compareF++instance OrdF f => Ord (Assignment f ctx) where+  compare x y = toOrdering (compareF x y)++instance HashableF (Index ctx) where+  hashWithSaltF s i = hashWithSalt s (indexVal i)++instance Hashable (Index ctx tp) where+  hashWithSalt = hashWithSaltF++instance HashableF f => Hashable (Assignment f ctx) where+  hashWithSalt s (Assignment a) = hashWithSaltF s a++instance HashableF f => HashableF (Assignment f) where+  hashWithSaltF = hashWithSalt++instance ShowF f => Show (Assignment f ctx) where+  show a = "[" Prelude.++ intercalate ", " (toListFC showF a) Prelude.++ "]"++instance ShowF f => ShowF (Assignment f)++{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}+adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)++{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}+update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx+update i v a = adjust (\_ -> v) i a++-- | Modify the value of an assignment at a particular index.+adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)+adjustM f (Index i) (Assignment a) = Assignment <$> (unsafe_bin_adjust f a i 0)+{-# SPECIALIZE adjustM :: (f tp -> Identity (f tp)) -> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx) #-}++type instance IndexF       (Assignment f ctx) = Index ctx+type instance IxValueF     (Assignment f ctx) = f++instance forall (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) ctx) where+  ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)+  ixF' idx f = adjustM f idx++instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where+  ixF = ixF'++-- This is an unsafe version of update that changes the type of the expression.+unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'+unsafeUpdate i (Assignment a) e = Assignment (runIdentity (unsafe_bin_adjust (\_ -> Identity e) a i 0))++-- | View an assignment as either empty or an assignment with one appended.+data AssignView f ctx where+  AssignEmpty :: AssignView f EmptyCtx+  AssignExtend :: Assignment f ctx+               -> f tp+               -> AssignView f (ctx::>tp)++-- | View an assignment as either empty or an assignment with one appended.+viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx+viewAssign (Assignment x) =+  case bin_drop x of+    DropEmpty -> AssignEmpty+    DropExt t v -> AssignExtend (Assignment t) v++zipWith :: (forall x . f x -> g x -> h x)+        -> Assignment f a+        -> Assignment g a+        -> Assignment h a+zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y+{-# INLINE zipWith #-}++zipWithM :: Applicative m+         => (forall x . f x -> g x -> m (h x))+         -> Assignment f a+         -> Assignment g a+         -> m (Assignment h a)+zipWithM f (Assignment x) (Assignment y) = Assignment <$> tree_zipWithM f x y+{-# INLINABLE zipWithM #-}++instance FunctorFC Assignment where+  fmapFC = \f (Assignment x) -> Assignment (fmap_bin f x)+  {-# INLINE fmapFC #-}++instance FoldableFC Assignment where+  foldMapFC = foldMapFCDefault+  {-# INLINE foldMapFC #-}++instance TraversableFC Assignment where+  traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x+  {-# INLINE traverseFC #-}++traverseWithIndex :: Applicative m+                  => (forall tp . Index ctx tp -> f tp -> m (g tp))+                  -> Assignment f ctx+                  -> m (Assignment g ctx)+traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i)++------------------------------------------------------------------------+-- Appending++appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)+appendBal x (BalLeaf a) = x `extend` a+appendBal x (BalPair y z) =+  case assoc x y z of+    Refl -> x `appendBal` y `appendBal` z++appendBin :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)+appendBin x Empty = x+appendBin x (PlusOne _ y z) =+  case assoc x y z of+    Refl -> x `appendBin` y `appendBal` z+appendBin x (PlusZero _ y) = x `appendBin` y++(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)+x <++> Assignment y = x `appendBin` y++------------------------------------------------------------------------+-- KnownRepr instances++instance (KnownRepr (Assignment f) ctx, KnownRepr f bt)+      => KnownRepr (Assignment f) (ctx ::> bt) where+  knownRepr = knownRepr `extend` knownRepr++instance KnownRepr (Assignment f) EmptyCtx where+  knownRepr = empty++------------------------------------------------------------------------+-- Lens combinators++unsafeLens :: Int -> Lens.Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)+unsafeLens idx =+  Lens.lens (unsafeIndex Proxy idx) (unsafeUpdate idx)++------------------------------------------------------------------------+-- 1 field lens combinators++type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1)++instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where+  _1 = unsafeLens 0++------------------------------------------------------------------------+-- 2 field lens combinators++type Assignment2 f x1 x2+   = Assignment f ('EmptyCtx '::> x1 '::> x2)++instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where+  _1 = unsafeLens 0++instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where+  _2 = unsafeLens 1++------------------------------------------------------------------------+-- 3 field lens combinators++type Assignment3 f x1 x2 x3+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3)++instance Lens.Field1 (Assignment3 f t x2 x3)+                     (Assignment3 f u x2 x3)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0+++instance Lens.Field2 (Assignment3 f x1 t x3)+                     (Assignment3 f x1 u x3)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment3 f x1 x2 t)+                     (Assignment3 f x1 x2 u)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++------------------------------------------------------------------------+-- 4 field lens combinators++type Assignment4 f x1 x2 x3 x4+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4)++instance Lens.Field1 (Assignment4 f t x2 x3 x4)+                     (Assignment4 f u x2 x3 x4)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0+++instance Lens.Field2 (Assignment4 f x1 t x3 x4)+                     (Assignment4 f x1 u x3 x4)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment4 f x1 x2 t x4)+                     (Assignment4 f x1 x2 u x4)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment4 f x1 x2 x3 t)+                     (Assignment4 f x1 x2 x3 u)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++------------------------------------------------------------------------+-- 5 field lens combinators++type Assignment5 f x1 x2 x3 x4 x5+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5)++instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5)+                     (Assignment5 f u x2 x3 x4 x5)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0++instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5)+                     (Assignment5 f x1 u x3 x4 x5)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5)+                     (Assignment5 f x1 x2 u x4 x5)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5)+                     (Assignment5 f x1 x2 x3 u x5)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t)+                     (Assignment5 f x1 x2 x3 x4 u)+                     (f t)+                     (f u) where+  _5 = unsafeLens 4++------------------------------------------------------------------------+-- 6 field lens combinators++type Assignment6 f x1 x2 x3 x4 x5 x6+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6)++instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6)+                     (Assignment6 f u x2 x3 x4 x5 x6)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0+++instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6)+                     (Assignment6 f x1 u x3 x4 x5 x6)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6)+                     (Assignment6 f x1 x2 u x4 x5 x6)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6)+                     (Assignment6 f x1 x2 x3 u x5 x6)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6)+                     (Assignment6 f x1 x2 x3 x4 u x6)+                     (f t)+                     (f u) where+  _5 = unsafeLens 4++instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t)+                     (Assignment6 f x1 x2 x3 x4 x5 u)+                     (f t)+                     (f u) where+  _6 = unsafeLens 5++------------------------------------------------------------------------+-- 7 field lens combinators++type Assignment7 f x1 x2 x3 x4 x5 x6 x7+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7)++instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7)+                     (Assignment7 f u x2 x3 x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0+++instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7)+                     (Assignment7 f x1 u x3 x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7)+                     (Assignment7 f x1 x2 u x4 x5 x6 x7)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7)+                     (Assignment7 f x1 x2 x3 u x5 x6 x7)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7)+                     (Assignment7 f x1 x2 x3 x4 u x6 x7)+                     (f t)+                     (f u) where+  _5 = unsafeLens 4++instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7)+                     (Assignment7 f x1 x2 x3 x4 x5 u x7)+                     (f t)+                     (f u) where+  _6 = unsafeLens 5++instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t)+                     (Assignment7 f x1 x2 x3 x4 x5 x6 u)+                     (f t)+                     (f u) where+  _7 = unsafeLens 6++------------------------------------------------------------------------+-- 8 field lens combinators++type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8)++instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)+                     (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0+++instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)+                     (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)+                     (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)+                     (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)+                     (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)+                     (f t)+                     (f u) where+  _5 = unsafeLens 4++instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)+                     (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)+                     (f t)+                     (f u) where+  _6 = unsafeLens 5++instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)+                     (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)+                     (f t)+                     (f u) where+  _7 = unsafeLens 6++instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)+                     (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)+                     (f t)+                     (f u) where+  _8 = unsafeLens 7++------------------------------------------------------------------------+-- 9 field lens combinators++type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9+   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9)+++instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)+                     (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _1 = unsafeLens 0++instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)+                     (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _2 = unsafeLens 1++instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)+                     (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _3 = unsafeLens 2++instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)+                     (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _4 = unsafeLens 3++instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)+                     (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)+                     (f t)+                     (f u) where+  _5 = unsafeLens 4++instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)+                     (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)+                     (f t)+                     (f u) where+  _6 = unsafeLens 5++instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)+                     (f t)+                     (f u) where+  _7 = unsafeLens 6++instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)+                     (f t)+                     (f u) where+  _8 = unsafeLens 7++instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)+                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)+                     (f t)+                     (f u) where+  _9 = unsafeLens 8

@@ -0,0 +1,99 @@+{-|+Description      : Type-level lists.+Copyright        : (c) Galois, Inc 2015+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This module defines type-level lists used for representing the type of+variables in a context.+-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module Data.Parameterized.Ctx+  ( type Ctx(..)+  , EmptyCtx+  , SingleCtx+  , (::>)+  , type (<+>)++    -- * Type context manipulation+  , CtxSize+  , CtxLookup+  , CtxUpdate+  , CtxLookupRight+  , CtxUpdateRight+  , CheckIx+  , ValidIx+  , FromLeft+  ) where++import Data.Kind (Constraint)+import GHC.TypeLits (Nat, type (+), type (-), type (<=?), TypeError, ErrorMessage(..))++------------------------------------------------------------------------+-- Ctx++type EmptyCtx = 'EmptyCtx+type (c :: Ctx k) ::> (a::k) = c '::> a++type SingleCtx x = EmptyCtx ::> x++-- | Kind @'Ctx' k@ comprises lists of types of kind @k@.+data Ctx k+  = EmptyCtx+  | Ctx k ::> k++-- | Append two type-level contexts.+type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where+  x <+> EmptyCtx = x+  x <+> (y ::> e) = (x <+> y) ::> e+++-- | This type family computes the number of elements in a 'Ctx'+type family CtxSize (a :: Ctx k) :: Nat where+  CtxSize 'EmptyCtx   = 0+  CtxSize (xs '::> x) = 1 + CtxSize xs++-- | Helper type family used to generate descriptive error messages when+-- an index is larger than the length of the 'Ctx' being indexed.+type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint where+  CheckIx ctx n 'True = ()+  CheckIx ctx n 'False = TypeError ('Text "Index "            ':<>: 'ShowType n+                              ':<>: 'Text " out of range in " ':<>: 'ShowType ctx)++-- | A constraint that checks that the nat @n@ is a valid index into the+--   context @ctx@, and raises a type error if not.+type ValidIx (n :: Nat) (ctx :: Ctx k)+  = CheckIx ctx n (n+1 <=? CtxSize ctx)++-- | 'Ctx' is a snoc-list. In order to use the more intuitive left-to-right+-- ordering of elements the desired index is subtracted from the total+-- number of elements.+type FromLeft ctx n = CtxSize ctx - 1 - n++-- | Lookup the value in a context by number, from the right+type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where+  CtxLookupRight 0 (ctx '::> r) = r+  CtxLookupRight n (ctx '::> r) = CtxLookupRight (n-1) ctx++-- | Update the value in a context by number, from the right.  If the index+--   is out of range, the context is unchanged.+type family CtxUpdateRight (n :: Nat) (x::k) (ctx :: Ctx k) :: Ctx k where+  CtxUpdateRight n x 'EmptyCtx      = 'EmptyCtx+  CtxUpdateRight 0 x (ctx '::> old) = ctx '::> x+  CtxUpdateRight n x (ctx '::> y)   = CtxUpdateRight (n-1) x ctx '::> y++-- | Lookup the value in a context by number, from the left.+--   Produce a type error if the index is out of range.+type CtxLookup (n :: Nat) (ctx :: Ctx k)+  = CtxLookupRight (FromLeft ctx n) ctx++-- | Update the value in a context by number, from the left.  If the index+--   is out of range, the context is unchanged.+type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k)+  = CtxUpdateRight (FromLeft ctx n) x ctx

@@ -0,0 +1,23 @@+{-|+Copyright        : (c) Galois, Inc 2015+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This reflects type level proofs involving contexts.+-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeOperators #-}+module Data.Parameterized.Ctx.Proofs+  ( leftId+  , assoc+  ) where++import Data.Type.Equality+import Unsafe.Coerce++import Data.Parameterized.Ctx++leftId :: p x -> (EmptyCtx <+> x) :~: x+leftId _ = unsafeCoerce Refl++assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z+assoc _ _ _ = unsafeCoerce Refl

@@ -0,0 +1,97 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.HashTable+-- Copyright        : (c) Galois, Inc 2014+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module provides a ST-based hashtable for parameterized keys and values.+--+-- NOTE: This API makes use of unsafeCoerce to implement the parameterized+-- hashtable abstraction.  This should be typesafe provided the+-- 'TestEquality' instance on the key type is implemented soundly.+------------------------------------------------------------------------+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Trustworthy #-}+module Data.Parameterized.HashTable+  ( HashTable+  , new+  , newSized+  , clone+  , lookup+  , insert+  , member+  , delete+  , clear+  , Data.Parameterized.Classes.HashableF(..)+  , Control.Monad.ST.RealWorld+  ) where++import Control.Applicative+import Control.Monad.ST+import qualified Data.HashTable.ST.Cuckoo as H+import GHC.Exts (Any)+import Unsafe.Coerce++import Prelude hiding (lookup)++import Data.Parameterized.Classes+import Data.Parameterized.Some++-- | A hash table mapping nonces to values.+newtype HashTable s (key :: k -> *) (val :: k -> *)+      = HashTable (H.HashTable s (Some key) Any)++-- | Create a new empty table.+new :: ST s (HashTable s key val)+new = HashTable <$> H.new++-- | Create a new empty table to hold 'n' elements.+newSized :: Int -> ST s (HashTable s k v)+newSized n = HashTable <$> H.newSized n++-- | Create a hash table that is a copy of the current one.+clone :: (HashableF key, TestEquality key)+      => HashTable s key val+      -> ST s (HashTable s key val)+clone (HashTable tbl) = do+  -- Create a new table+  r <- H.new+  -- Insert existing elements in+  H.mapM_ (uncurry (H.insert r)) tbl+  -- Return table+  return $! HashTable r++-- | Lookup value of key in table.+lookup :: (HashableF key, TestEquality key)+       => HashTable s key val+       -> key tp+       -> ST s (Maybe (val tp))+lookup (HashTable h) k = fmap unsafeCoerce <$> H.lookup h (Some k)+{-# INLINE lookup #-}++-- | Insert new key and value mapping into table.+insert :: (HashableF key, TestEquality key)+       => HashTable s (key :: k -> *) (val :: k -> *)+       -> key tp+       -> val tp+       -> ST s ()+insert (HashTable h) k v = H.insert h (Some k) (unsafeCoerce v)++-- | Return true if the key is in the hash table.+member :: (HashableF key, TestEquality key)+       => HashTable s (key :: k -> *) (val :: k -> *)+       -> key (tp :: k)+       -> ST s Bool+member (HashTable h) k = isJust <$> H.lookup h (Some k)++-- | Delete an element from the hash table.+delete :: (HashableF key, TestEquality key)+       => HashTable s (key :: k -> *) (val :: k -> *)+       -> key (tp :: k)+       -> ST s ()+delete (HashTable h) k = H.delete h (Some k)++clear :: (HashableF key, TestEquality key)+      => HashTable s (key :: k -> *) (val :: k -> *) -> ST s ()+clear (HashTable h) = H.mapM_ (\(k,_) -> H.delete h k) h

@@ -0,0 +1,244 @@+{-|+Copyright        : (c) Galois, Inc 2017+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This module defines a list over two parameters.  The first+is a fixed type-level function @k -> *@ for some kind @k@, and the+second is a list of types with kind k that provide the indices for+the values in the list.++This type is closely related to the @Context@ type in+@Data.Parameterized.Context@.+-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeOperators #-}+module Data.Parameterized.List+  ( List(..)+  , Index(..)+  , indexValue+  , (!!)+  , update+  , indexed+  , imap+  , ifoldr+  , izipWith+  , itraverse+    -- * Constants+  , index0+  , index1+  , index2+  , index3+  ) where++import qualified Control.Lens as Lens+import Prelude hiding ((!!))++import Data.Parameterized.Classes+import Data.Parameterized.TraversableFC++-- | Parameterized list of elements.+data List :: (k -> *) -> [k] -> * where+  Nil  :: List f '[]+  (:<) :: f tp -> List f tps -> List f (tp : tps)++infixr 5 :<++instance ShowF f => Show (List f sh) where+  showsPrec _ Nil = showString "Nil"+  showsPrec p (elt :< rest) = showParen (p > precCons) $+    -- Unlike a derived 'Show' instance, we don't print parens implied+    -- by right associativity.+    showsPrecF (precCons+1) elt . showString " :< " . showsPrec 0 rest+    where+      precCons = 5++instance ShowF f => ShowF (List f)++instance FunctorFC List where+  fmapFC _ Nil = Nil+  fmapFC f (x :< xs) = f x :< fmapFC f xs++instance FoldableFC List where+  foldrFC _ z Nil = z+  foldrFC f z (x :< xs) = f x (foldrFC f z xs)++instance TraversableFC List where+  traverseFC _ Nil = pure Nil+  traverseFC f (h :< r) = (:<) <$> f h <*> traverseFC f r++instance TestEquality f => TestEquality (List f) where+  testEquality Nil Nil = Just Refl+  testEquality (xh :< xl) (yh :< yl) = do+    Refl <- testEquality xh yh+    Refl <- testEquality xl yl+    pure Refl+  testEquality _ _ = Nothing++instance OrdF f => OrdF (List f) where+  compareF Nil Nil = EQF+  compareF Nil _ = LTF+  compareF _ Nil = GTF+  compareF (xh :< xl) (yh :< yl) =+    lexCompareF xh yh $+    lexCompareF xl yl $+    EQF+++instance KnownRepr (List f) '[] where+  knownRepr = Nil++instance (KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f) (s ': sh) where+  knownRepr = knownRepr :< knownRepr++--------------------------------------------------------------------------------+-- Indexed operations+++-- | Represents an index into a type-level list. Used in place of integers to+--   1. ensure that the given index *does* exist in the list+--   2. guarantee that it has the given kind+data Index :: [k] -> k -> *  where+  IndexHere :: Index (x:r) x+  IndexThere :: !(Index r y) -> Index (x:r) y++deriving instance Eq (Index l x)+deriving instance Show  (Index l x)++instance ShowF (Index l)++instance TestEquality (Index l) where+  testEquality IndexHere IndexHere = Just Refl+  testEquality (IndexThere x) (IndexThere y) = testEquality x y+  testEquality _ _ = Nothing++instance OrdF (Index l) where+  compareF IndexHere IndexHere = EQF+  compareF IndexHere IndexThere{} = LTF+  compareF IndexThere{} IndexHere = GTF+  compareF (IndexThere x) (IndexThere y) = compareF x y++instance Ord (Index sh x) where+  x `compare` y = toOrdering $ x `compareF` y++-- | Return the index as an integer.+indexValue :: Index l tp -> Integer+indexValue = go 0+  where go :: Integer -> Index l tp -> Integer+        go i IndexHere = i+        go i (IndexThere x) = seq j $ go j x+          where j = i+1++-- | Index 0+index0 :: Index (x:r) x+index0 = IndexHere++-- | Index 1+index1 :: Index (x0:x1:r) x1+index1 = IndexThere index0++-- | Index 2+index2 :: Index (x0:x1:x2:r) x2+index2 = IndexThere index1++-- | Index 3+index3 :: Index (x0:x1:x2:x3:r) x3+index3 = IndexThere index2++-- | Return the value in a list at a given index+(!!) :: List f l -> Index l x -> f x+l !! (IndexThere i) =+  case l of+    _ :< r -> r !! i+l !! IndexHere =+  case l of+    (h :< _) -> h++-- | Update the 'List' at an index+update :: List f l -> Index l s -> (f s -> f s) -> List f l+update vals IndexHere upd =+  case vals of+    x :< rest -> upd x :< rest+update vals (IndexThere th) upd =+  case vals of+    x :< rest -> x :< update rest th upd++-- | Provides a lens for manipulating the element at the given index.+indexed :: Index l x -> Lens.Simple Lens.Lens (List f l) (f x)+indexed IndexHere      f (x :< rest) = (:< rest) <$> f x+indexed (IndexThere i) f (x :< rest) = (x :<) <$> indexed i f rest++--------------------------------------------------------------------------------+-- Indexed operations++-- | Map over the elements in the list, and provide the index into+-- each element along with the element itself.+imap :: forall f g l+     . (forall x . Index l x -> f x -> g x)+     -> List f l+     -> List g l+imap f = go id+  where+    go :: forall l'+        . (forall tp . Index l' tp -> Index l tp)+       -> List f l'+       -> List g l'+    go g l =+      case l of+        Nil -> Nil+        e :< rest -> f (g IndexHere) e :< go (g . IndexThere) rest++-- | Right-fold with an additional index.+ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b+ifoldr f seed0 l = go id l seed0+  where+    go :: forall tps+        . (forall tp . Index tps tp -> Index sh tp)+       -> List a tps+       -> b+       -> b+    go g ops b =+      case ops of+        Nil -> b+        a :< rest -> f (g IndexHere) a (go (\ix -> g (IndexThere ix)) rest b)++-- | Zip up two lists with a zipper function, which can use the index.+izipWith :: forall a b c sh . (forall tp. Index sh tp -> a tp -> b tp -> c tp)+         -> List a sh+         -> List b sh+         -> List c sh+izipWith f = go id+  where+    go :: forall sh' .+          (forall tp . Index sh' tp -> Index sh tp)+       -> List a sh'+       -> List b sh'+       -> List c sh'+    go g as bs =+      case (as, bs) of+        (Nil, Nil) -> Nil+        (a :< as', b :< bs') ->+          f (g IndexHere) a b :< go (g . IndexThere) as' bs'++-- | Traverse with an additional index.+itraverse :: forall a b sh t+          . Applicative t+          => (forall tp . Index sh tp -> a tp -> t (b tp))+          -> List a sh+          -> t (List b sh)+itraverse f = go id+  where+    go :: forall tps . (forall tp . Index tps tp -> Index sh tp)+       -> List a tps+       -> t (List b tps)+    go g l =+      case l of+        Nil -> pure Nil+        e :< rest -> (:<) <$> f (g IndexHere) e <*> go (\ix -> g (IndexThere ix)) rest

@@ -0,0 +1,548 @@+{-|+Copyright        : (c) Galois, Inc 2014-2017++This module defines finite maps where the key and value types are+parameterized by an arbitrary kind.++Some code was adapted from containers.+-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+module Data.Parameterized.Map+  ( MapF+    -- * Construction+  , Data.Parameterized.Map.empty+  , singleton+  , insert+  , insertWith+  , delete+  , union+    -- * Query+  , null+  , lookup+  , member+  , notMember+  , size+    -- * Conversion+  , keys+  , elems+  , fromList+  , toList+  , fromKeys+  , fromKeysM+   -- * Filter+  , filterGt+  , filterLt+    -- * Folds+  , foldrWithKey+    -- * Traversal+  , map+  , mapMaybe+  , traverseWithKey+  , traverseWithKey_+    -- * Complex interface.+  , UpdateRequest(..)+  , Updated(..)+  , updatedValue+  , updateAtKey+  , mergeWithKeyM+  , module Data.Parameterized.Classes+    -- * Pair+  , 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 Data.Parameterized.Classes+import Data.Parameterized.Some+import Data.Parameterized.Pair ( Pair(..) )+import Data.Parameterized.TraversableF+import Data.Parameterized.Utils.BinTree+  ( MaybeS(..)+  , fromMaybeS+  , Updated(..)+  , updatedValue+  , TreeApp(..)+  , bin+  , IsBinTree(..)+  , balanceL+  , balanceR+  , glue+  )+import qualified Data.Parameterized.Utils.BinTree as Bin++#if MIN_VERSION_base(4,8,0)+import Prelude hiding (lookup, map, traverse, null)+#else+import Prelude hiding (lookup, map, null)+#endif++------------------------------------------------------------------------+-- Pair++comparePairKeys :: OrdF k => Pair k a -> Pair k a -> Ordering+comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y)+{-# INLINABLE comparePairKeys #-}++------------------------------------------------------------------------+-- MapF++-- | A map from parameterized keys to values with the same paramter type.+data MapF (k :: v -> Type) (a :: v -> Type) where+  Bin :: {-# UNPACK #-}+         !Size -- Number of elements in tree.+      -> !(k x)+      -> !(a x)+      -> !(MapF k a)+      -> !(MapF k a)+      -> MapF k a+  Tip :: MapF k a++type Size = Int++-- | Return empty map+empty :: MapF k a+empty = Tip++-- | Return true if map is empty+null :: MapF k a -> Bool+null Tip = True+null Bin{} = False++-- | Return map containing a single element+singleton :: k tp -> a tp -> MapF k a+singleton k x = Bin 1 k x Tip Tip++instance Bin.IsBinTree (MapF k a) (Pair k a) where+  asBin (Bin _ k v l r) = BinTree (Pair k v) l r+  asBin Tip = TipTree++  tip = Tip+  bin (Pair k v) l r = Bin (size l + size r + 1) k v l r++  size Tip              = 0+  size (Bin sz _ _ _ _) = sz++instance (TestEquality k, EqF a) => Eq (MapF k a) where+  x == y = size x == size y && toList x == toList y++------------------------------------------------------------------------+-- Traversals++#ifdef __GLASGOW_HASKELL__+{-# NOINLINE [1] map #-}+{-# NOINLINE [1] traverse #-}+{-# RULES+"map/map" forall (f :: (forall tp . f tp -> g tp)) (g :: (forall tp . g tp -> h tp)) xs+               . map g (map f xs) = map (g . f) xs+"map/traverse" forall (f :: (forall tp . f tp -> m (g tp))) (g :: (forall tp . g tp -> h tp)) xs+               . fmap (map g) (traverse f xs) = traverse (\v -> g <$> f v) xs+"traverse/map"+  forall (f :: (forall tp . f tp -> g tp)) (g :: (forall tp . g tp -> m (h tp))) xs+       . traverse g (map f xs) = traverse (\v -> g (f v)) xs+"traverse/traverse"+  forall (f :: (forall tp . f tp -> m (g tp))) (g :: (forall tp . g tp -> m (h tp))) xs+       . traverse f xs >>= traverse g = traverse (\v -> f v >>= g) xs+ #-}+#endif++-- | 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)++-- | Run partial map over elements.+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)++-- | Traverse elements in a map+traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)+traverse _ Tip = pure Tip+traverse f (Bin sx kx x l r) = Bin sx kx <$> f x <*> traverse f l <*> traverse f r++-- | Traverse elements in a map+traverseWithKey+  :: Applicative m+  => (forall tp . ktp tp -> f tp -> m (g tp))+  -> MapF ktp f+  -> m (MapF ktp g)+traverseWithKey _ Tip = pure Tip+traverseWithKey f (Bin sx kx x l r) =+   Bin sx kx <$> f kx x <*> traverseWithKey f l <*> traverseWithKey f r++-- | Traverse elements in a map without returning result.+traverseWithKey_+  :: Applicative m+  => (forall tp . ktp tp -> f tp -> m ())+  -> MapF ktp f+  -> m ()+traverseWithKey_ _ Tip = pure ()+traverseWithKey_ f (Bin _ kx x l r) = f kx x *> traverseWithKey_ f l *> traverseWithKey_ f r+++type instance IndexF   (MapF k v) = k+type instance IxValueF (MapF k v) = v++-- | Turn a map key into a traversal that visits the indicated element in the map, if it exists.+instance forall (k:: a -> Type) v. OrdF k => IxedF a (MapF k v) where+  ixF :: k x -> Traversal' (MapF k v) (v x)+  ixF i f m = updatedValue <$> updateAtKey i (pure Nothing) (\x -> Set <$> f x) m++-- | Turn a map key into a lens that points into the indicated position in the map.+instance forall (k:: a -> Type) v. OrdF k => AtF a (MapF k v) where+  atF :: k x -> Lens' (MapF k v) (Maybe (v x))+  atF i f m = updatedValue <$> updateAtKey i (f Nothing) (\x -> maybe Delete Set <$> f (Just x)) m+++-- | Lookup value in map.+lookup :: OrdF k => k tp -> MapF k a -> Maybe (a tp)+lookup k0 = seq k0 (go k0)+  where+    go :: OrdF k => k tp -> MapF k a -> Maybe (a tp)+    go _ Tip = Nothing+    go k (Bin _ kx x l r) =+      case compareF k kx of+        LTF -> go k l+        GTF -> go k r+        EQF -> Just x+{-# INLINABLE lookup #-}++-- | Return true if key is bound in map.+member :: OrdF k => k tp -> MapF k a -> Bool+member k0 = seq k0 (go k0)+  where+    go :: OrdF k => k tp -> MapF k a -> Bool+    go _ Tip = False+    go k (Bin _ kx _ l r) =+      case compareF k kx of+        LTF -> go k l+        GTF -> go k r+        EQF -> True+{-# INLINABLE member #-}++-- | Return true if key is not bound in map.+notMember :: OrdF k => k tp -> MapF k a -> Bool+notMember k m = not $ member k m+{-# INLINABLE notMember #-}++instance FunctorF (MapF ktp) where+  fmapF = map++instance FoldableF (MapF ktp) where+  foldrF f z = go z+    where go z' Tip             = z'+          go z' (Bin _ _ x l r) = go (f x (go z' r)) l++instance TraversableF (MapF ktp) where+  traverseF = traverse++instance (ShowF ktp, ShowF rtp) => Show (MapF ktp rtp) where+  show m = showMap showF showF m++-- | Return all keys of the map in ascending order.+keys :: MapF k a -> [Some k]+keys = foldrWithKey (\k _ l -> Some k : l) []++-- | Return all elements of the map in the ascending order of their keys.+elems :: MapF k a -> [Some a]+elems = foldrF (\e l -> Some e : l) []++-- | Perform a 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++showMap :: (forall tp . ktp tp -> String)+        -> (forall tp . rtp tp -> String)+        -> MapF ktp rtp+        -> String+showMap ppk ppv m = "{ " ++ intercalate ", " l ++ " }"+  where l = foldrWithKey (\k a l0 -> (ppk k ++ " -> " ++ ppv a) : l0) [] m++------------------------------------------------------------------------+-- filter++compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering+compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x)++-- | @filterGt k m@ returns submap of @m@ that only contains entries+-- that are larger than @k@.+filterGt :: OrdF k => k tp -> MapF k v -> MapF k v+filterGt k m = fromMaybeS m (Bin.filterGt (compareKeyPair k) m)+{-# INLINABLE filterGt #-}++-- | @filterLt k m@ returns submap of @m@ that only contains entries+-- that are smaller than @k@.+filterLt :: OrdF k => k tp -> MapF k v -> MapF k v+filterLt k m = fromMaybeS m (Bin.filterLt (compareKeyPair k) m)+{-# INLINABLE filterLt #-}++------------------------------------------------------------------------+-- User operations++-- | Insert a binding into the map, replacing the existing binding if needed.+insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a+insert = \k v m -> seq k $ updatedValue (Bin.insert comparePairKeys (Pair k v) m)+{-# INLINABLE insert #-}+-- {-# SPECIALIZE Bin.insert :: OrdF k => Pair k a -> MapF k a -> Updated (MapF k a) #-}++-- | Insert a binding into the map, replacing the existing binding if needed.+insertWithImpl :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> Updated (MapF k a)+insertWithImpl f k v t = seq k $+  case t of+    Tip -> Bin.Updated (Bin 1 k v Tip Tip)+    Bin sz yk yv l r ->+      case compareF k yk of+        LTF ->+          case insertWithImpl f k v l of+            Bin.Updated l'   -> Bin.Updated   (Bin.balanceL (Pair yk yv) l' r)+            Bin.Unchanged l' -> Bin.Unchanged (Bin sz yk yv l' r)+        GTF ->+          case insertWithImpl f k v r of+            Bin.Updated r'   -> Bin.Updated   (Bin.balanceR (Pair yk yv) l r')+            Bin.Unchanged r' -> Bin.Unchanged (Bin sz yk yv l r')+        EQF -> Bin.Unchanged (Bin sz yk (f v yv) l r)+{-# INLINABLE insertWithImpl #-}++-- | @insertWith f new m@ inserts the binding into @m@.+--+-- It inserts @f new old@ if @m@ already contains an equivaltn value+-- @old@, and @new@ otherwise.  It returns an Unchanged value if the+-- map stays the same size and an updated value if a new entry was+-- inserted.+insertWith :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a+insertWith = \f k v t -> seq k $ updatedValue (insertWithImpl f k v t)+{-# INLINABLE insertWith #-}++-- | Delete a value from the map if present.+delete :: OrdF k => k tp -> MapF k a -> MapF k a+delete = \k m -> seq k $ fromMaybeS m $ Bin.delete (p k) m+  where p :: OrdF k => k tp -> Pair k a -> Ordering+        p k (Pair kx _) = toOrdering (compareF k kx)+{-# INLINABLE delete #-}+{-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}++-- | Union two sets+union :: OrdF k => MapF k a -> MapF k a -> MapF k a+union t1 t2 = Bin.union comparePairKeys t1 t2+{-# INLINABLE union #-}+-- {-# SPECIALIZE Bin.union compare :: OrdF k => MapF k a -> MapF k a -> MapF k a #-}++------------------------------------------------------------------------+-- updateAtKey++-- | Update request tells when to do with value+data UpdateRequest v+   = -- | Keep the current value.+     Keep+     -- | Set the value to a new value.+   | Set !v+     -- | Delete a value.+   | Delete++data AtKeyResult k a where+  AtKeyUnchanged :: AtKeyResult k a+  AtKeyInserted :: MapF k a -> AtKeyResult k a+  AtKeyModified :: MapF k a -> AtKeyResult k a+  AtKeyDeleted  :: MapF k a -> AtKeyResult k a++atKey' :: (OrdF k, Functor f)+       => k tp+       -> f (Maybe (a tp)) -- ^ Function to call if no element is found.+       -> (a tp -> f (UpdateRequest (a tp)))+       -> MapF k a+       -> f (AtKeyResult k a)+atKey' k onNotFound onFound t =+  case asBin t of+    TipTree -> ins <$> onNotFound+      where ins Nothing  = AtKeyUnchanged+            ins (Just v) = AtKeyInserted (singleton k v)+    BinTree yp@(Pair kx y) l r ->+      case compareF k kx of+        LTF -> ins <$> atKey' k onNotFound onFound l+          where ins AtKeyUnchanged = AtKeyUnchanged+                ins (AtKeyInserted l') = AtKeyInserted (balanceL yp l' r)+                ins (AtKeyModified l') = AtKeyModified (bin      yp l' r)+                ins (AtKeyDeleted  l') = AtKeyDeleted  (balanceR yp l' r)+        GTF -> ins <$> atKey' k onNotFound onFound r+          where ins AtKeyUnchanged = AtKeyUnchanged+                ins (AtKeyInserted r') = AtKeyInserted (balanceR yp l r')+                ins (AtKeyModified r') = AtKeyModified (bin      yp l r')+                ins (AtKeyDeleted  r') = AtKeyDeleted  (balanceL yp l r')+        EQF -> ins <$> onFound y+          where ins Keep    = AtKeyUnchanged+                ins (Set x) = AtKeyModified (bin (Pair kx x) l r)+                ins Delete  = AtKeyDeleted (glue l r)+{-# INLINABLE atKey' #-}++-- | Log-time algorithm that allows a value at a specific key to be added, replaced,+-- or deleted.+updateAtKey :: (OrdF k, Functor f)+            => k tp -- ^ Key to update+            -> f (Maybe (a tp))+               -- ^ Action to call if nothing is found+            -> (a tp -> f (UpdateRequest (a tp)))+               -- ^ Action to call if value is found.+            -> MapF k a+               -- ^ Map to update+            -> f (Updated (MapF k a))+updateAtKey k onNotFound onFound t = ins <$> atKey' k onNotFound onFound t+  where ins AtKeyUnchanged = Unchanged t+        ins (AtKeyInserted t') = Updated t'+        ins (AtKeyModified t') = Updated t'+        ins (AtKeyDeleted  t') = Updated t'+{-# INLINABLE updateAtKey #-}++-- | Create a Map from a list of pairs.+fromList :: OrdF k => [Pair k a] -> MapF k a+fromList = foldl' (\m (Pair k a) -> insert k a m) Data.Parameterized.Map.empty++toList :: MapF k a -> [Pair k a]+toList = foldrWithKey (\k x m -> Pair k x : m) []++-- | Generate a map from a foldable collection of keys and a+-- function from keys to values.+fromKeys :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)+          .  (Monad m, Foldable t, OrdF a)+            => (forall tp . a tp -> m (v tp))+            -- ^ Function for evaluating a register value.+            -> t (Some a)+               -- ^ Set of X86 registers+            -> m (MapF a v)+fromKeys f = foldM go empty+  where go :: MapF a v -> Some a -> m (MapF a v)+        go m (Some k) = (\v -> insert k v m) <$> f k++-- | Generate a map from a foldable collection of keys and a monadic+-- function from keys to values.+fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)+          .  (Monad m, Foldable t, OrdF a)+           => (forall tp . a tp -> m (v tp))+           -- ^ Function for evaluating a register value.+           -> t (Some a)+           -- ^ Set of X86 registers+           -> m (MapF a v)+fromKeysM f = foldM go empty+  where go :: MapF a v -> Some a -> m (MapF a v)+        go m (Some k) = (\v -> insert k v m) <$> f k++filterGtMaybe :: OrdF k => MaybeS (k x) -> MapF k a -> MapF k a+filterGtMaybe NothingS m = m+filterGtMaybe (JustS k) m = filterGt k m++filterLtMaybe :: OrdF k => MaybeS (k x) -> MapF k a -> MapF k a+filterLtMaybe NothingS m = m+filterLtMaybe (JustS k) m = filterLt k m++-- | Merge bindings in two maps to get a third.+mergeWithKeyM :: forall k a b c m+               . (Applicative m, OrdF k)+              => (forall tp . k tp -> a tp -> b tp -> m (Maybe (c tp)))+              -> (MapF k a -> m (MapF k c))+              -> (MapF k b -> m (MapF k c))+              -> MapF k a+              -> MapF k b+              -> m (MapF k c)+mergeWithKeyM f g1 g2 = go+  where+    go Tip t2 = g2 t2+    go t1 Tip = g1 t1+    go t1 t2 = hedgeMerge NothingS NothingS t1 t2++    hedgeMerge :: MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k b -> m (MapF k c)+    hedgeMerge _   _   t1  Tip = g1 t1+    hedgeMerge blo bhi Tip (Bin _ kx x l r) =+      g2 $ Bin.link (Pair kx x) (filterGtMaybe blo l) (filterLtMaybe bhi r)+    hedgeMerge blo bhi (Bin _ kx x l r) t2 =+        let Bin.PairS found trim_t2 = trimLookupLo kx bhi t2+            resolve_g1 :: MapF k c -> MapF k c -> MapF k c -> MapF k c+            resolve_g1 Tip = Bin.merge+            resolve_g1 (Bin _ k' x' Tip Tip) = Bin.link (Pair k' x')+            resolve_g1 _ = error "mergeWithKey: Bad function g1"+            resolve_f Nothing = Bin.merge+            resolve_f (Just x') = Bin.link (Pair kx x')+         in case found of+              Nothing ->+                resolve_g1 <$> g1 (singleton kx x)+                           <*> hedgeMerge blo bmi l (trim blo bmi t2)+                           <*> hedgeMerge bmi bhi r trim_t2+              Just x2 ->+                resolve_f <$> f kx x x2+                          <*> hedgeMerge blo bmi l (trim blo bmi t2)+                          <*> hedgeMerge bmi bhi r trim_t2+      where bmi = JustS kx+{-# INLINABLE mergeWithKeyM #-}++{--------------------------------------------------------------------+  [trim blo bhi t] trims away all subtrees that surely contain no+  values between the range [blo] to [bhi]. The returned tree is either+  empty or the key of the root is between @blo@ and @bhi@.+--------------------------------------------------------------------}+trim :: OrdF k => MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k a+trim NothingS   NothingS   t = t+trim (JustS lk) NothingS   t = filterGt lk t+trim NothingS   (JustS hk) t = filterLt hk t+trim (JustS lk) (JustS hk) t = filterMiddle lk hk t++-- | Returns only entries that are strictly between the two keys.+filterMiddle :: OrdF k => k x -> k y -> MapF k a -> MapF k a+filterMiddle lo hi (Bin _ k _ _ r)+  | k `leqF` lo = filterMiddle lo hi r+filterMiddle lo hi (Bin _ k _ l _)+  | k `geqF` hi = filterMiddle lo hi l+filterMiddle _  _  t = t+{-# INLINABLE filterMiddle #-}++++-- Helper function for 'mergeWithKey'. The @'trimLookupLo' lk hk t@ performs both+-- @'trim' (JustS lk) hk t@ and @'lookup' lk t@.++-- See Note: Type of local 'go' function+trimLookupLo :: OrdF k => k tp -> MaybeS (k y) -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a)+trimLookupLo lk NothingS t = greater lk t+  where greater :: OrdF k => k tp -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a)+        greater lo t'@(Bin _ kx x l r) =+           case compareF lo kx of+             LTF -> Bin.PairS (lookup lo l) t'+             EQF -> Bin.PairS (Just x) r+             GTF -> greater lo r+        greater _ Tip = Bin.PairS Nothing Tip+trimLookupLo lk (JustS hk) t = middle lk hk t+  where middle :: OrdF k => k tp -> k y -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a)+        middle lo hi t'@(Bin _ kx x l r) =+          case compareF lo kx of+            LTF | kx `ltF` hi -> Bin.PairS (lookup lo l) t'+                | otherwise -> middle lo hi l+            EQF -> Bin.PairS (Just x) (lesser hi r)+            GTF -> middle lo hi r+        middle _ _ Tip = Bin.PairS Nothing Tip++        lesser :: OrdF k => k y -> MapF k a -> MapF k a+        lesser hi (Bin _ k _ l _) | k `geqF` hi = lesser hi l+        lesser _ t' = t'

@@ -0,0 +1,527 @@+{-|+Copyright        : (c) Galois, Inc 2014-2015+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This defines a type 'NatRepr' for representing a type-level natural+at runtime.  This can be used to branch on a type-level value.  For+each @n@, @NatRepr n@ contains a single value containing the vlaue+@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+contained in a NatRepr value matches its static type.+-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+#if MIN_VERSION_base(4,9,0)+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}+#endif+module Data.Parameterized.NatRepr+  ( NatRepr+  , natValue+  , knownNat+  , withKnownNat+  , IsZeroNat(..)+  , isZeroNat+  , NatComparison(..)+  , compareNat+  , decNat+  , predNat+  , incNat+  , addNat+  , subNat+  , divNat+  , halfNat+  , withDivModNat+  , natMultiply+  , someNat+  , maxNat+  , natRec+  , natForEach+  , NatCases(..)+  , testNatCases+    -- * Bitvector utilities+  , widthVal+  , minUnsigned+  , maxUnsigned+  , minSigned+  , maxSigned+  , toUnsigned+  , toSigned+  , unsignedClamp+  , signedClamp+    -- * LeqProof+  , LeqProof(..)+  , testLeq+  , testStrictLeq+  , leqRefl+  , leqTrans+  , leqAdd2+  , leqSub2+  , leqMulCongr+    -- * LeqProof combinators+  , leqProof+  , withLeqProof+  , isPosNat+  , leqAdd+  , leqSub+  , leqMulPos+  , leqAddPos+  , addIsLeq+  , withAddLeq+  , addPrefixIsLeq+  , withAddPrefixLeq+  , addIsLeqLeft1+  , dblPosIsPos+  , leqMulMono+    -- * Arithmetic proof+  , plusComm+  , mulComm+  , plusMinusCancel+  , minusPlusCancel+  , addMulDistribRight+  , withAddMulDistribRight+  , withSubMulDistribRight+  , mulCancelR+  , mul2Plus+    -- * Re-exports typelists basics+--  , NatK+  , type (+)+  , type (-)+  , type (*)+  , type (<=)+  , Equality.TestEquality(..)+  , (Equality.:~:)(..)+  , Data.Parameterized.Some.Some+  ) where++import Data.Bits ((.&.))+import Data.Hashable+import Data.Proxy as Proxy+import Data.Type.Equality as Equality+import GHC.TypeLits as TypeLits+import Unsafe.Coerce++import Data.Parameterized.Classes+import Data.Parameterized.Some++maxInt :: Integer+maxInt = toInteger (maxBound :: Int)++------------------------------------------------------------------------+-- Nat++-- | A runtime presentation of a type-level 'Nat'.+--+-- 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.+                                   }+  deriving (Hashable)++-- | Return the value of the nat representation.+widthVal :: NatRepr n -> Int+widthVal (NatRepr i) | i < maxInt = fromInteger i+                     | otherwise = error "Width is too large."++instance Eq (NatRepr m) where+  _ == _ = True++instance TestEquality NatRepr where+  testEquality (NatRepr m) (NatRepr n)+    | m == n = Just (unsafeCoerce Refl)+    | otherwise = Nothing++-- | Result of comparing two numbers.+data NatComparison m n where+  -- First number is less than second.+  NatLT :: !(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++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))++instance OrdF NatRepr where+  compareF x y =+    case compareNat x y of+      NatLT _ -> LTF+      NatEQ -> EQF+      NatGT _ -> GTF++instance PolyEq (NatRepr m) (NatRepr n) where+  polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y++instance Show (NatRepr n) where+  show (NatRepr n) = show n++instance ShowF NatRepr++instance HashableF NatRepr where+  hashWithSaltF = hashWithSalt++-- | This generates a NatRepr from a type-level context.+knownNat :: forall n . KnownNat n => NatRepr n+knownNat = NatRepr (natVal (Proxy :: Proxy n))++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+        Refl -> v+    Nothing -> error "withKnownNat: inner value in NatRepr is not a natural"++data IsZeroNat n where+  ZeroNat    :: IsZeroNat 0+  NonZeroNat :: IsZeroNat (n+1)++isZeroNat :: NatRepr n -> IsZeroNat n+isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat+isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat++-- | Decrement a @NatRepr@+decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1)+decNat (NatRepr i) = NatRepr (i-1)++-- | Get the predicessor of a nat+predNat :: NatRepr (n+1) -> NatRepr n+predNat (NatRepr i) = NatRepr (i-1)++-- | Increment a @NatRepr@+incNat :: NatRepr n -> NatRepr (n+1)+incNat (NatRepr x) = NatRepr (x+1)++halfNat :: NatRepr (n+n) -> NatRepr n+halfNat (NatRepr x) = NatRepr (x `div` 2)++addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n)+addNat (NatRepr m) (NatRepr n) = NatRepr (m+n)++subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n)+subNat (NatRepr m) (NatRepr n) = NatRepr (m-n)++divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m+divNat (NatRepr x) (NatRepr y) = NatRepr (div x y)++withDivModNat :: forall n m a.+                 NatRepr n+              -> NatRepr m+              -> (forall div mod. (n ~ ((div * m) + mod)) =>+                  NatRepr div -> NatRepr mod -> a)+              -> a+withDivModNat n m f =+  case ( Some (NatRepr divPart), Some (NatRepr modPart)) of+     ( Some (divn :: NatRepr div), Some (modn :: NatRepr mod) )+       -> case unsafeCoerce (Refl :: 0 :~: 0) of+            (Refl :: (n :~: ((div * m) + mod))) -> f divn modn+  where+    (divPart, modPart) = divMod (natValue n) (natValue m)++natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)+natMultiply (NatRepr n) (NatRepr m) = NatRepr (n * m)++------------------------------------------------------------------------+-- Operations for using NatRepr as a bitwidth.++-- | Return minimum unsigned value for bitvector with given width (always 0).+minUnsigned :: NatRepr w -> Integer+minUnsigned _ = 0++-- | Return maximum unsigned value for bitvector with given width.+maxUnsigned :: NatRepr w -> Integer+maxUnsigned w = 2^(natValue 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))++-- | Return maximum value for bitvector in 2s complement with given width.+maxSigned :: (1 <= w) => NatRepr w -> Integer+maxSigned w = 2^(natValue w - 1) - 1++-- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@.+toUnsigned :: NatRepr w -> Integer -> Integer+toUnsigned w i = maxUnsigned w .&. i++-- | @toSigned w i@ interprets the least-significant @w@ bits in @i@ as a+-- 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)+    | otherwise       = i+  where i = i0 .&. maxUnsigned w++-- | @unsignedClamp w i@ rounds @i@ to the nearest value between+-- @0@ and @2^w-1@ (inclusive).+unsignedClamp :: NatRepr w -> Integer -> Integer+unsignedClamp w i+  | i < minUnsigned w = minUnsigned w+  | i > maxUnsigned w = maxUnsigned w+  | otherwise         = i++-- | @signedClamp w i@ rounds @i@ to the nearest value between+-- @-2^(w-1)@ and @2^(w-1)-1@ (inclusive).+signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer+signedClamp w i+  | i < minSigned w = minSigned w+  | i > maxSigned w = maxSigned w+  | otherwise       = i++------------------------------------------------------------------------+-- Some NatRepr++someNat :: Integer -> Maybe (Some NatRepr)+someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n)))+          | otherwise = Nothing++-- | Return the maximum of two nat representations.+maxNat :: NatRepr m -> NatRepr n -> Some NatRepr+maxNat x y+  | natValue x >= natValue y = Some x+  | otherwise = Some y++------------------------------------------------------------------------+-- Arithmetic++-- | Produce evidence that + is commutative.+plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m+plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n)++-- | Produce evidence that * is commutative.+mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)+mulComm _ _ = unsafeCoerce Refl++mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)+mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of+               Refl -> Refl++-- | Cancel an add followed b a subtract+plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m+plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m)++minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m+minusPlusCancel _ _ = unsafeCoerce (Refl :: m :~: m)++addMulDistribRight :: forall n m p f g h. f n -> g m -> h p+                    -> ((n * p) + (m * p)) :~: ((n + m) * p)+addMulDistribRight _n _m _p = unsafeCoerce Refl++++withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p+                    -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a+withAddMulDistribRight n m p f =+  case addMulDistribRight n m p of+    Refl -> f++withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p+                    -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a+withSubMulDistribRight _n _m _p f =+  case unsafeCoerce (Refl :: 0 :~: 0) of+    (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f++++------------------------------------------------------------------------+-- LeqProof++-- | @LeqProof m n@ is a type whose values are only inhabited when @m@+-- is less than or equal to @n@.+data LeqProof m n where+  LeqProof :: (m <= n) => LeqProof m n++testStrictLeq :: forall m n+               . (m <= n)+              => NatRepr m+              -> NatRepr n+              -> Either (LeqProof (m+1) n) (m :~: n)+testStrictLeq (NatRepr m) (NatRepr n)+  | m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0))+  | otherwise = Right (unsafeCoerce (Refl :: m :~: m))+{-# NOINLINE testStrictLeq #-}++-- As for NatComparison above, but works with LeqProof+data NatCases m n where+  -- First number is less than second.+  NatCaseLT :: LeqProof (m+1) n -> NatCases m n+  NatCaseEQ :: NatCases m m+  -- First number is greater than second.+  NatCaseGT :: LeqProof (n+1) m -> NatCases m n++testNatCases ::  forall m n+              . NatRepr m+             -> NatRepr n+             -> NatCases m n+testNatCases m n =+  case compare (natValue m) (natValue n) of+    LT -> NatCaseLT (unsafeCoerce (LeqProof :: LeqProof 0 0))+    EQ -> unsafeCoerce $ (NatCaseEQ :: NatCases m m)+    GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0))+{-# NOINLINE testNatCases #-}++-- | @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)+   | m <= n    = Just (unsafeCoerce (LeqProof :: LeqProof 0 0))+   | otherwise = Nothing+{-# NOINLINE testLeq #-}++-- | Apply reflexivity to LeqProof+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)+{-# NOINLINE leqTrans #-}++-- | Add both sides of two inequalities+leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)+leqAdd2 x y = seq x $ seq y $ unsafeCoerce (LeqProof :: LeqProof 0 0)+{-# NOINLINE leqAdd2 #-}++-- | Subtract sides of two inequalities.+leqSub2 :: LeqProof x_l x_h+        -> LeqProof y_l y_h+        -> LeqProof (x_l-y_h) (x_h-y_l)+leqSub2 LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)+{-# NOINLINE leqSub2 #-}++------------------------------------------------------------------------+-- LeqProof combinators++-- | Create a leqProof using two proxies+leqProof :: (m <= n) => f m -> g n -> LeqProof m n+leqProof _ _ = LeqProof++withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a+withLeqProof p a =+  case p of+    LeqProof -> a++-- | Test whether natural number is positive.+isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)+isPosNat = testLeq (knownNat :: NatRepr 1)++-- | Congruence rule for multiplication+leqMulCongr :: LeqProof a x+            -> LeqProof b y+            -> LeqProof (a*b) (x*y)+leqMulCongr LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 1 1)+{-# NOINLINE leqMulCongr #-}++-- | Multiplying two positive numbers results in a positive number.+leqMulPos :: forall p q x y+          .  (1 <= x, 1 <= y)+          => p x+          -> q y+          -> LeqProof 1 (x*y)+leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y)++leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)+leqMulMono x y = leqMulCongr (leqProof (Proxy :: Proxy 1) x) (leqRefl y)++-- | Produce proof that adding a value to the larger element in an LeqProof+-- is larger+leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)+leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p)++leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)+leqAddPos m n = leqAdd (leqProof (Proxy :: Proxy 1) m) n++-- | Produce proof that subtracting a value from the smaller element is smaller.+leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n+leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p)++addIsLeq :: f n -> g m -> LeqProof n (n + m)+addIsLeq n m = leqAdd (leqRefl n) m++addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)+addPrefixIsLeq m n =+  case plusComm n m of+    Refl -> addIsLeq n m++dblPosIsPos :: forall n . LeqProof 1 n -> LeqProof 1 (n+n)+dblPosIsPos x = leqAdd x Proxy++addIsLeqLeft1 :: forall n n' m . LeqProof (n + n') m -> LeqProof n m+addIsLeqLeft1 p =+    case plusMinusCancel n n' of+      Refl -> leqSub p le+  where n :: Proxy n+        n = Proxy+        n' :: Proxy n'+        n' = Proxy+        le :: LeqProof n' (n + n')+        le = addPrefixIsLeq n n'++{-# INLINE withAddPrefixLeq #-}+withAddPrefixLeq :: NatRepr n -> NatRepr m -> ((m <= n + m) => a) -> a+withAddPrefixLeq n m = withLeqProof (addPrefixIsLeq n m)++withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a+withAddLeq n m f = withLeqProof (addIsLeq n m) (f (addNat n m))++natForEach' :: forall l h a+            . NatRepr l+            -> NatRepr h+            -> (forall n. LeqProof l n -> LeqProof n h -> NatRepr n -> a)+            -> [a]+natForEach' l h f+  | Just LeqProof  <- testLeq l h =+    let f' :: forall n. LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a+        f' = \lp hp -> f (addIsLeqLeft1 lp) hp+     in f LeqProof LeqProof l : natForEach' (incNat l) h f'+  | otherwise             = []++-- | Apply a function to each element in a range; return the list of values+-- obtained.+natForEach :: forall l h a+            . NatRepr l+           -> NatRepr h+           -> (forall n. (l <= n, n <= h) => NatRepr n -> a)+           -> [a]+natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f)++-- | Recursor for natural numbeers.+natRec :: forall m f+       .  NatRepr m+       -> f 0+       -> (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'')++mulCancelR ::+  (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)+mulCancelR _ _ _ = unsafeCoerce Refl

@@ -0,0 +1,158 @@+{-|+Copyright        : (c) Galois, Inc 2014-2016+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This module provides a simple generator of new indexes in the ST monad.+It is predictable and not intended for cryptographic purposes.++This module also provides a global nonce generator that will generate+2^64 nonces before looping.++NOTE: The 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply+compare the generated nonce values and then assert to the compiler+(via 'unsafeCoerce') that the types ascribed to the nonces are equal+if their values are equal.+-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE Trustworthy #-}+#if MIN_VERSION_base(4,9,0)+{-# LANGUAGE TypeInType #-}+#endif+module Data.Parameterized.Nonce+  ( -- * NonceGenerator+    NonceGenerator+  , freshNonce+  , Nonce+  , indexValue+    -- * Accessing a nonce generator+  , newSTNonceGenerator+  , newIONonceGenerator+  , withIONonceGenerator+  , withSTNonceGenerator+  , withGlobalSTNonceGenerator+  , GlobalNonceGenerator+  , globalNonceGenerator+  ) where++import Control.Monad.ST+import Data.Hashable+import Data.IORef+import Data.STRef+import Data.Typeable+import Data.Word+import Unsafe.Coerce+import System.IO.Unsafe (unsafePerformIO)++import Data.Parameterized.Classes+import Data.Parameterized.Some++#if MIN_VERSION_base(4,9,0)+import Data.Kind+#endif++-- | Provides a monadic action for getting fresh typed names.+--+-- 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 {+#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)+#else+    freshNonce :: forall (tp :: k) . m (Nonce s tp)+#endif+  }++-- | 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+    }++-- | 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+            }++-- | 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+            }++-- | 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+withSTNonceGenerator f = do+  Some r <- newSTNonceGenerator+  f r++-- | Create a new nonce generator in the IO monad.+withIONonceGenerator :: (forall s . NonceGenerator IO s -> IO r) -> IO r+withIONonceGenerator f = do+  Some r <- newIONonceGenerator+  f r++-- | An index generated by the counter.+newtype Nonce (s :: *) (tp :: k) = Nonce { indexValue :: Word64 }+  deriving (Eq, Ord, Hashable, Show)++--  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce+--  from casting the types of nonces, which it would otherwise be able to do+--  because tp is a phantom type parameter.  This partially helps to protect+--  the nonce abstraction.+type role Nonce nominal nominal++instance TestEquality (Nonce s) where+  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)+                   | otherwise = Nothing++instance OrdF (Nonce s) where+  compareF x y =+    case compare (indexValue x) (indexValue y) of+      LT -> LTF+      EQ -> unsafeCoerce EQF+      GT -> GTF++instance HashableF (Nonce s) where+  hashWithSaltF s (Nonce x) = hashWithSalt s x++instance ShowF (Nonce s)++------------------------------------------------------------------------+-- GlobalNonceGenerator++data GlobalNonceGenerator++globalNonceIORef :: IORef Word64+globalNonceIORef = unsafePerformIO (newIORef 0)+{-# NOINLINE globalNonceIORef #-}++-- | A nonce generator that uses a globally-defined counter.+globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator+globalNonceGenerator =+  NonceGenerator+  { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n))+  }

@@ -0,0 +1,70 @@+{-|+Copyright        : (c) Galois, Inc 2014-2016+Maintainer       : Eddy Westbrook <westbrook@galois.com>++This module provides a typeclass and monad transformers for generating+nonces.+-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+module Data.Parameterized.Nonce.Transformers+  ( MonadNonce(..)+  , NonceT(..)+  , NonceST+  , NonceIO+  , getNonceSTGen+  , runNonceST+  , runNonceIO+  , module Data.Parameterized.Nonce+  ) where++import Control.Monad.Reader+import Control.Monad.ST+import Control.Monad.State++import Data.Parameterized.Nonce+++-- | A 'MonadNonce' is a monad that can generate fresh 'Nonce's in a given set+-- (where we view the phantom type parameter of 'Nonce' as a designator of the+-- set that the 'Nonce' came from).+class Monad m => MonadNonce m where+  type NonceSet m :: *+  freshNonceM :: forall (tp :: k) . m (Nonce (NonceSet m) tp)++-- | This transformer adds a nonce generator to a given monad.+newtype NonceT s m a =+  NonceT { runNonceT :: ReaderT (NonceGenerator m s) m a }+  deriving (Functor, Applicative, Monad)++instance MonadTrans (NonceT s) where+  lift m = NonceT $ lift m++instance Monad m => MonadNonce (NonceT s m) where+  type NonceSet (NonceT s m) = s+  freshNonceM = NonceT $ lift . freshNonce =<< ask++instance MonadNonce m => MonadNonce (StateT s m) where+  type NonceSet (StateT s m) = NonceSet m+  freshNonceM = lift $ freshNonceM++-- | Helper type to build a 'MonadNonce' from the 'ST' monad.+type NonceST t s = NonceT s (ST t)++-- | Helper type to build a 'MonadNonce' from the 'IO' monad.+type NonceIO s = NonceT s IO++-- | Return the actual 'NonceGenerator' used in an 'ST' computation.+getNonceSTGen :: NonceST t s (NonceGenerator (ST t) s)+getNonceSTGen = NonceT ask++-- | Run a 'NonceST' computation with a fresh 'NonceGenerator'.+runNonceST :: (forall t s. NonceST t s a) -> a+runNonceST m = runST $ withSTNonceGenerator $ runReaderT $ runNonceT m++-- | Run a 'NonceIO' computation with a fresh 'NonceGenerator' inside 'IO'.+runNonceIO :: (forall s. NonceIO s a) -> IO a+runNonceIO m = withIONonceGenerator $ runReaderT $ runNonceT m

@@ -0,0 +1,107 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.NonceGenerator+-- Description      : A counter in the ST monad.+-- Copyright        : (c) Galois, Inc 2014+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+-- Stability        : provisional+--+-- This module provides a simple generator of new indexes in the ST monad.+-- It is predictable and not intended for cryptographic purposes.+--+-- NOTE: the 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply+-- compare the generated nonce values and then assert to the compiler+-- (via 'unsafeCoerce') that the types ascribed to the nonces are equal+-- if their values are equal.  This is only OK because of the discipline+-- by which nonces should be used: they should only be generated from+-- a 'NonceGenerator' (i.e., should not be built directly), and nonces from+-- different generators must never be compared!  Arranging to compare+-- Nonces from different origins would allow users to build 'unsafeCoerce'+-- via the 'testEquality' function.+--+-- A somewhat safer API would be to brand the generated Nonces with the+-- state type variable of the NonceGenerator whence they came, and to only+-- provide NonceGenerators via a Rank-2 continuation-passing API, similar to+-- 'runST'. This would (via a meta-argument involving parametricity)+-- help to prevent nonces of different origin from being compared.+-- However, this would force us to push the 'ST' type brand into a significant+-- number of other structures and APIs.+--+-- Another alternative would be to use 'unsafePerformIO' magic to make+-- a global nonce generator, and make that the only way to generate nonces.+-- It is not clear that this is actually an improvement from a type safety+-- point of view, but an argument could be made.+--+-- For now, be careful using Nonces, and ensure that you do not mix+-- Nonces from different NonceGenerators.+------------------------------------------------------------------------+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE Unsafe #-}+module Data.Parameterized.Nonce.Unsafe+  ( NonceGenerator+  , newNonceGenerator+  , freshNonce+  , atLimit+  , Nonce+  , indexValue+  ) where++import Control.Monad.ST+import Data.Hashable+import Data.STRef+import Data.Word+import Unsafe.Coerce++import Data.Parameterized.Classes++-- | A simple type that for getting fresh indices in the 'ST' monad.+-- The type parameter @s@ is used for the 'ST' monad parameter.+newtype NonceGenerator s = NonceGenerator (STRef s Word64)++-- | Create a new counter.+newNonceGenerator :: ST s (NonceGenerator s)+newNonceGenerator = NonceGenerator `fmap` newSTRef (toEnum 0)++-- | An index generated by the counter.+newtype Nonce (tp :: k) = Nonce { indexValue :: Word64 }+  deriving (Eq, Ord, Hashable, Show)++--  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce+--  from casting the types of nonces, which it would otherwise be able to do+--  because tp is a phantom type parameter.  This partially helps to protect+--  the nonce abstraction.+type role Nonce nominal++instance TestEquality Nonce where+  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)+                   | otherwise = Nothing++instance OrdF Nonce where+  compareF x y =+    case compare (indexValue x) (indexValue y) of+      LT -> LTF+      EQ -> unsafeCoerce EQF+      GT -> GTF++instance HashableF Nonce where+  hashWithSaltF s (Nonce x) = hashWithSalt s x++instance ShowF Nonce++{-# INLINE freshNonce #-}+-- | Get a fresh index and increment the counter.+freshNonce :: NonceGenerator s -> ST s (Nonce tp)+freshNonce (NonceGenerator r) = do+  i <- readSTRef r+  writeSTRef r $! succ i+  return (Nonce i)++-- | Return true if counter has reached the limit, and can't be+-- incremented without risk of error.+atLimit :: NonceGenerator s -> ST s Bool+atLimit (NonceGenerator r) = do+  i <- readSTRef r+  return (i == maxBound)

@@ -0,0 +1,51 @@+{-|+Copyright        : (c) Galois, Inc 2017++This module defines a 2-tuple where both elements are parameterized over the+same existentially quantified parameter.++-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+module Data.Parameterized.Pair+  ( Pair(..)+  , fstPair+  , sndPair+  , viewPair+  ) where++import Data.Parameterized.Classes+import Data.Parameterized.Some+import Data.Parameterized.TraversableF++-- | Like a 2-tuple, but with an existentially quantified parameter that both of+-- the elements share.+data Pair (a :: k -> *) (b :: k -> *) where+  Pair :: !(a tp) -> !(b tp) -> Pair a b++instance (TestEquality a, EqF b) => Eq (Pair a b) where+  Pair xa xb == Pair ya yb =+    case testEquality xa ya of+      Just Refl -> eqF xb yb+      Nothing -> False++instance FunctorF (Pair a) where+  fmapF f (Pair x y) = Pair x (f y)++instance FoldableF (Pair a) where+  foldMapF f (Pair _ y) = f y+  foldrF f z (Pair _ y) = f y z++-- | Extract the first element of a pair.+fstPair :: Pair a b -> Some a+fstPair (Pair x _) = Some x++-- | Extract the second element of a pair.+sndPair :: Pair a b -> Some b+sndPair (Pair _ y) = Some y++-- | Project out of Pair.+viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c+viewPair f (Pair x y) = f x y

@@ -0,0 +1,59 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.Some+-- Copyright        : (c) Galois, Inc 2014+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module provides 'Some', a GADT that hides a type parameter.+------------------------------------------------------------------------+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+module Data.Parameterized.Some+  ( Some(..)+  , viewSome+  , mapSome+  , traverseSome+  , traverseSome_+  ) where++import Data.Hashable+import Data.Parameterized.Classes+++data Some (f:: k -> *) = forall x . Some (f x)++instance TestEquality f => Eq (Some f) where+  Some x == Some y = isJust (testEquality x y)++instance OrdF f => Ord (Some f) where+  compare (Some x) (Some y) = toOrdering (compareF x y)++instance HashableF f => Hashable (Some f) where+  hashWithSalt s (Some x) = hashWithSaltF s x+  hash (Some x) = hashF x++instance ShowF f => Show (Some f) where+  show (Some x) = showF x++-- | Project out of Some.+viewSome :: (forall tp . f tp -> r) -> Some f -> r+viewSome f (Some x) = f x++-- | Apply function to inner value.+mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g+mapSome f (Some x) = Some $! f x++{-# INLINE traverseSome #-}+-- | Modify the inner value.+traverseSome :: Functor m+             => (forall tp . f tp -> m (g tp))+             -> Some f+             -> m (Some g)+traverseSome f (Some x) = Some `fmap` f x++{-# INLINE traverseSome_ #-}+-- | Modify the inner value.+traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m ()+traverseSome_ f (Some x) = (\_ -> ()) `fmap` f x

@@ -0,0 +1,106 @@+{-|+Copyright        : (c) Galois, Inc 2014-2015+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This defines a type family 'SymbolRepr' for representing a type-level string+(AKA symbol) at runtime.  This can be used to branch on a type-level value.++The 'TestEquality' and 'OrdF' instances for 'SymbolRepr' are implemented using+'unsafeCoerce'.  This should be typesafe because we maintain the invariant+that the string value contained in a SymbolRepr value matches its static type.++At the type level, symbols have very few operations, so SymbolRepr+correspondingly has very few functions that manipulate them.+-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Trustworthy #-}+module Data.Parameterized.SymbolRepr+  ( -- * SymbolRepr+    SymbolRepr+  , symbolRepr+  , knownSymbol+  , someSymbol+    -- * Re-exports+  , type GHC.Symbol+  , GHC.KnownSymbol+  ) where++import GHC.TypeLits as GHC+import Unsafe.Coerce (unsafeCoerce)++import Data.Hashable+import Data.Proxy+import qualified Data.Text as Text++import Data.Parameterized.Classes+import Data.Parameterized.Some++-- | A runtime representation of a GHC type-level symbol.+newtype SymbolRepr (nm::GHC.Symbol)+  = SymbolRepr { symbolRepr :: Text.Text+                 -- ^ The underlying text representation of the symbol+               }+-- INVARIANT: The contained runtime text value matches the value+-- of the type level symbol.  The SymbolRepr constructor+-- is not exported so we can maintain this invariant in this+-- module.++-- | Generate a symbol representative at runtime.  The type-level+--   symbol will be abstract, as it is hidden by the 'Some' constructor.+someSymbol :: Text.Text -> Some SymbolRepr+someSymbol nm = Some (SymbolRepr nm)++-- | Generate a value representative for the type level symbol.+knownSymbol :: GHC.KnownSymbol s => SymbolRepr s+knownSymbol = go Proxy+  where go :: GHC.KnownSymbol s => Proxy s -> SymbolRepr s+        go p = SymbolRepr $! packSymbol (GHC.symbolVal p)++        -- NOTE here we explicitly test that unpacking the packed text value+        -- gives the desired string.  This is to avoid pathological corner cases+        -- involving string values that have no text representation.+        packSymbol str+           | Text.unpack txt == str = txt+           | otherwise = error $ "Unrepresentable symbol! "++ str+         where txt = Text.pack str++instance (GHC.KnownSymbol s) => KnownRepr SymbolRepr s where+  knownRepr = knownSymbol++instance TestEquality SymbolRepr where+   testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)+      | x == y    = Just (unsafeCoerce (Refl :: x :~: x))+      | otherwise = Nothing+instance OrdF SymbolRepr where+   compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)+      | x <  y    = LTF+      | x == y    = unsafeCoerce (EQF :: OrderingF x x)+      | otherwise = GTF++-- These instances are trivial by the invariant+-- that the contained string matches the type-level+-- symbol+instance Eq (SymbolRepr x) where+   _ == _ = True+instance Ord (SymbolRepr x) where+   compare _ _ = EQ++instance HashableF SymbolRepr where+  hashWithSaltF = hashWithSalt+instance Hashable (SymbolRepr nm) where+  hashWithSalt s (SymbolRepr nm) = hashWithSalt s nm++instance Show (SymbolRepr nm) where+  show (SymbolRepr nm) = Text.unpack nm++instance ShowF SymbolRepr

@@ -0,0 +1,488 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.TH.GADT+-- Copyright        : (c) Galois, Inc 2013-2014+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module declares template Haskell primitives so that it is easier+-- to work with GADTs that have many constructors.+------------------------------------------------------------------------+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE EmptyCase #-}+module Data.Parameterized.TH.GADT+  ( -- * Instance generators+    -- $typePatterns+  structuralEquality+  , structuralTypeEquality+  , structuralTypeOrd+  , structuralTraversal+  , structuralShowsPrec+  , structuralHash+  , PolyEq(..)+    -- * Template haskell utilities that may be useful in other contexts.+  , DataD+  , lookupDataType'+  , asTypeCon+  , conPat+  , TypePat(..)+  , dataParamTypes+  , assocTypePats+  ) where++import Control.Monad+import Data.Hashable (hashWithSalt)+import Data.Maybe+import Data.Set (Set)+import qualified Data.Set as Set+import Language.Haskell.TH+import Language.Haskell.TH.Datatype+++import Data.Parameterized.Classes++------------------------------------------------------------------------+-- Template Haskell utilities++type DataD = DatatypeInfo++lookupDataType' :: Name -> Q DatatypeInfo+lookupDataType' = reifyDatatype++-- | Given a constructor and string, this generates a pattern for matching+-- the expression, and the names of variables bound by pattern in order+-- they appear in constructor.+conPat ::+  ConstructorInfo {- ^ constructor information -} ->+  String          {- ^ generated name prefix   -} ->+  Q (Pat, [Name]) {- ^ pattern and bound names -}+conPat con pre = do+  nms <- newNames pre (length (constructorFields con))+  return (ConP (constructorName con) (VarP <$> nms), nms)+++-- | Return an expression corresponding to the constructor.+-- Note that this will have the type of a function expecting+-- the argumetns given.+conExpr :: ConstructorInfo -> Exp+conExpr = ConE . constructorName++------------------------------------------------------------------------+-- TypePat++-- | A type used to describe (and match) types appearing in generated pattern+-- matches inside of the TH generators in this module ('structuralEquality',+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal')+data TypePat+   = TypeApp TypePat TypePat -- ^ The application of a type.+   | AnyType       -- ^ Match any type.+   | DataArg Int   -- ^ Match the ith argument of the data type we are traversing.+   | ConType TypeQ -- ^ Match a ground type.++matchTypePat :: [Type] -> TypePat -> Type -> Q Bool+matchTypePat d (TypeApp p q) (AppT x y) = do+  r <- matchTypePat d p x+  case r of+    True -> matchTypePat d q y+    False -> return False+matchTypePat _ AnyType _ = return True+matchTypePat tps (DataArg i) tp+  | i < 0 || i > length tps = error $ "Illegal type pattern index " ++ show i+  | otherwise = do+    return $ stripSigT (tps !! i) == tp+  where+    -- th-abstraction can annotate type parameters with their kinds,+    -- we ignore these for matching+    stripSigT (SigT t _) = t+    stripSigT t          = t+matchTypePat _ (ConType tpq) tp = do+  tp' <- tpq+  return (tp' == tp)+matchTypePat _ _ _ = return False++dataParamTypes :: DatatypeInfo -> [Type]+dataParamTypes = datatypeVars++-- | Find value associated with first pattern that matches given pat if any.+assocTypePats :: [Type] -> [(TypePat,v)] -> Type -> Q (Maybe v)+assocTypePats _ [] _ = return Nothing+assocTypePats dTypes ((p,v):pats) tp = do+  r <- matchTypePat dTypes p tp+  case r of+    True -> return (Just v)+    False -> assocTypePats dTypes pats tp++------------------------------------------------------------------------+-- Contructor cases++typeVars :: TypeSubstitution a => a -> Set Name+typeVars = Set.fromList . freeVariables+++-- | @structuralEquality@ declares a structural equality predicate.+structuralEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ+structuralEquality tpq pats =+  [| \x y -> isJust ($(structuralTypeEquality tpq pats) x y) |]++joinEqMaybe :: Name -> Name -> ExpQ -> ExpQ+joinEqMaybe x y r = do+  [| if $(varE x) == $(varE y) then $(r) else Nothing |]++joinTestEquality :: ExpQ -> Name -> Name -> ExpQ -> ExpQ+joinTestEquality f x y r =+  [| case $(f) $(varE x) $(varE y) of+      Nothing -> Nothing+      Just Refl -> $(r)+   |]++matchEqArguments :: [Type]+                    -- ^ Types bound by data arguments.+                  -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+                 -> Name+                     -- ^ Name of constructor.+                 -> Set Name+                 -> [Type]+                 -> [Name]+                 -> [Name]+                 -> ExpQ+matchEqArguments dTypes pats cnm bnd (tp:tpl) (x:xl) (y:yl) = do+  doesMatch <- assocTypePats dTypes pats tp+  case doesMatch of+    Just q -> do+      let bnd' =+            case tp of+              AppT _ (VarT nm) -> Set.insert nm bnd+              _ -> bnd+      joinTestEquality q x y (matchEqArguments dTypes pats cnm bnd' tpl xl yl)+    Nothing | typeVars tp `Set.isSubsetOf` bnd -> do+      joinEqMaybe x y        (matchEqArguments dTypes pats cnm bnd  tpl xl yl)+    Nothing -> do+      fail $ "Unsupported argument type " ++ show tp+          ++ " in " ++ show (ppr cnm) ++ "."+matchEqArguments _ _ _ _ [] [] [] = [| Just Refl |]+matchEqArguments _ _ _ _ [] _  _  = error "Unexpected end of types."+matchEqArguments _ _ _ _ _  [] _  = error "Unexpected end of names."+matchEqArguments _ _ _ _ _  _  [] = error "Unexpected end of names."++mkSimpleEqF :: [Type] -- ^ Data declaration types+            -> Set Name+             -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+             -> ConstructorInfo+             -> [Name]+             -> ExpQ+             -> Bool -- ^ wildcard case required+             -> ExpQ+mkSimpleEqF dTypes bnd pats con xv yQ multipleCases = do+  -- Get argument types for constructor.+  let nm = constructorName con+  (yp,yv) <- conPat con "y"+  let rv = matchEqArguments dTypes pats nm bnd (constructorFields con) xv yv+  caseE yQ $ match (pure yp) (normalB rv) []+           : [ match wildP (normalB [| Nothing |]) [] | multipleCases ]++-- | Match equational form.+mkEqF :: DatatypeInfo -- ^ Data declaration.+      -> [(TypePat,ExpQ)]+      -> ConstructorInfo+      -> [Name]+      -> ExpQ+      -> Bool -- ^ wildcard case required+      -> ExpQ+mkEqF d pats con =+  let dVars = datatypeVars d+      bnd | null dVars = Set.empty+          | otherwise  = typeVars (init dVars)+  in mkSimpleEqF dVars bnd pats con++-- | @structuralTypeEquality f@ returns a function with the type:+--   forall x y . f x -> f y -> Maybe (x :~: y)+structuralTypeEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ+structuralTypeEquality tpq pats = do+  d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq++  let multipleCons = not (null (drop 1 (datatypeCons d)))+      trueEqs yQ = [ do (xp,xv) <- conPat con "x"+                        match (pure xp) (normalB (mkEqF d pats con xv yQ multipleCons)) []+                   | con <- datatypeCons d+                   ]++  if null (datatypeCons d)+    then [| \x -> case x of {} |]+    else [| \x y -> $(caseE [| x |] (trueEqs [| y |])) |]++-- | @structuralTypeOrd f@ returns a function with the type:+--   forall x y . f x -> f y -> OrderingF x y+--+-- This implementation avoids matching on both the first and second+-- parameters in a simple case expression in order to avoid stressing+-- GHC's coverage checker. In the case that the first and second parameters+-- have unique constructors, a simple numeric comparison is done to+-- compute the result.+structuralTypeOrd ::+  TypeQ ->+  [(TypePat,ExpQ)] {- ^ List of type patterns to match. -} ->+  ExpQ+structuralTypeOrd tpq l = do+  d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq++  let withNumber :: ExpQ -> (Maybe ExpQ -> ExpQ) -> ExpQ+      withNumber yQ k+        | null (drop 1 (datatypeCons d)) = k Nothing+        | otherwise =  [| let yn :: Int+                              yn = $(caseE yQ (constructorNumberMatches (datatypeCons d)))+                          in $(k (Just [| yn |])) |]++  if null (datatypeCons d)+    then [| \x -> case x of {} |]+    else [| \x y -> $(withNumber [|y|] $ \mbYn -> caseE [| x |] (outerOrdMatches d [|y|] mbYn)) |]+  where+    constructorNumberMatches :: [ConstructorInfo] -> [MatchQ]+    constructorNumberMatches cons =+      [ match (recP (constructorName con) [])+              (normalB (litE (integerL i)))+              []+      | (i,con) <- zip [0..] cons ]++    outerOrdMatches :: DatatypeInfo -> ExpQ -> Maybe ExpQ -> [MatchQ]+    outerOrdMatches d yExp mbYn =+      [ do (pat,xv) <- conPat con "x"+           match (pure pat)+                 (normalB (do xs <- mkOrdF d l con i mbYn xv+                              caseE yExp xs))+                 []+      | (i,con) <- zip [0..] (datatypeCons d) ]++-- | Generate a list of fresh names using the base name+-- numbered 1 to n to make them useful in conjunction with+-- @-dsuppress-unqiues@.+newNames ::+  String   {- ^ base name                     -} ->+  Int      {- ^ quantity                      -} ->+  Q [Name] {- ^ list of names: base1, base2.. -}+newNames base n = traverse (\i -> newName (base ++ show i)) [1..n]+++joinCompareF :: ExpQ -> Name -> Name -> ExpQ -> ExpQ+joinCompareF f x y r = do+  [| case $(f) $(varE x) $(varE y) of+      LTF -> LTF+      GTF -> GTF+      EQF -> $(r)+   |]++-- | Compare two variables and use following comparison if they are different.+--+-- This returns an 'OrdF' instance.+joinCompareToOrdF :: Name -> Name -> ExpQ -> ExpQ+joinCompareToOrdF x y r =+  [| case compare $(varE x) $(varE y) of+      LT -> LTF+      GT -> GTF+      EQ -> $(r)+   |]++  -- Match expression with given type to variables+matchOrdArguments :: [Type]+                     -- ^ Types bound by data arguments+                  -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+                  -> Name+                     -- ^ Name of constructor.+                  -> Set Name+                    -- ^ Names bound in data declaration+                  -> [Type]+                     -- ^ Types for constructors+                  -> [Name]+                     -- ^ Variables bound in first pattern+                  -> [Name]+                     -- ^ Variables bound in second pattern+                  -> ExpQ+matchOrdArguments dTypes pats cnm bnd (tp : tpl) (x:xl) (y:yl) = do+  doesMatch <- assocTypePats dTypes pats tp+  case doesMatch of+    Just f -> do+      let bnd' = case tp of+                   AppT _ (VarT nm) -> Set.insert nm bnd+                   _ -> bnd+      joinCompareF f x y (matchOrdArguments dTypes pats cnm bnd' tpl xl yl)+    Nothing | typeVars tp `Set.isSubsetOf` bnd -> do+      joinCompareToOrdF x y (matchOrdArguments dTypes pats cnm bnd tpl xl yl)+    Nothing ->+      fail $ "Unsupported argument type " ++ show (ppr tp)+             ++ " in " ++ show (ppr cnm) ++ "."+matchOrdArguments _ _ _ _ [] [] [] = [| EQF |]+matchOrdArguments _ _ _ _ [] _  _  = error "Unexpected end of types."+matchOrdArguments _ _ _ _ _  [] _  = error "Unexpected end of names."+matchOrdArguments _ _ _ _ _  _  [] = error "Unexpected end of names."++mkSimpleOrdF :: [Type] -- ^ Data declaration types+             -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+             -> ConstructorInfo -- ^ Information about the second constructor+             -> Integer -- ^ First constructor's index+             -> Maybe ExpQ -- ^ Optional second constructor's index+             -> [Name]  -- ^ Name from first pattern+             -> Q [MatchQ]+mkSimpleOrdF dTypes pats con xnum mbYn xv = do+  (yp,yv) <- conPat con "y"+  let rv = matchOrdArguments dTypes pats (constructorName con) Set.empty (constructorFields con) xv yv+  -- Return match expression+  return $ match (pure yp) (normalB rv) []+         : case mbYn of+             Nothing -> []+             Just yn -> [match wildP (normalB [| if xnum < $yn then LTF else GTF |]) []]++-- | Match equational form.+mkOrdF :: DatatypeInfo -- ^ Data declaration.+       -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments+       -> ConstructorInfo+       -> Integer+       -> Maybe ExpQ -- ^ optional right constructr index+       -> [Name]+       -> Q [MatchQ]+mkOrdF d pats = mkSimpleOrdF (datatypeVars d) pats++-- | Find the first recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@.+recurseArg :: (Type -> Q (Maybe ExpQ))+           -> ExpQ -- ^ Function to apply+           -> ExpQ+           -> Type+           -> Q (Maybe Exp)+recurseArg m f v tp = do+  mr <- m tp+  case mr of+    Just g ->  Just <$> [| $(g) $(f) $(v) |]+    Nothing ->+      case tp of+        AppT (ConT _) (AppT (VarT _) _) -> Just <$> [| traverse $(f) $(v) |]+        AppT (VarT _) _ -> Just <$> [| $(f) $(v) |]+        _ -> return Nothing++-- | @traverseAppMatch f c@ builds a case statement that matches a term with+-- the constructor @c@ and applies @f@ to each argument.+traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- Pattern match function+                 -> ExpQ -- ^ Function to apply to each argument recursively.+                 -> ConstructorInfo -- ^ Constructor to match.+                 -> MatchQ -- ^ Match expression that+traverseAppMatch pats fv c0 = do+  (pat,patArgs) <- conPat c0 "p"+  exprs <- zipWithM (recurseArg pats fv) (varE <$> patArgs) (constructorFields c0)++  let mkRes :: ExpQ -> [(Name, Maybe Exp)] -> ExpQ+      mkRes e [] = e+      mkRes e ((v,Nothing):r) =+        mkRes (appE e (varE v)) r+      mkRes e ((_,Just{}):r) = do+        v <- newName "r"+        lamE [varP v] (mkRes (appE e (varE v)) r)++  -- Apply the remaining argument to the expression in list.+  let applyRest :: ExpQ -> [Exp] -> ExpQ+      applyRest e [] = e+      applyRest e (a:r) = applyRest [| $(e) <*> $(pure a) |] r++  -- Apply the first argument to the list+  let applyFirst :: ExpQ -> [Exp] -> ExpQ+      applyFirst e [] = [| pure $(e) |]+      applyFirst e (a:r) = applyRest [| $(e) <$> $(pure a) |] r++  let pargs = patArgs `zip` exprs+  let rhs = applyFirst (mkRes (pure (conExpr c0)) pargs) (catMaybes exprs)+  match (pure pat) (normalB rhs) []++-- | @structuralTraversal tp@ generates a function that applies+-- a traversal @f@ to the subterms with free variables in @tp@.+structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ+structuralTraversal tpq pats0 = do+  d <- reifyDatatype =<< asTypeCon "structuralTraversal" =<< tpq+  f <- newName "f"+  a <- newName "a"+  lamE [varP f, varP a] $+      caseE (varE a)+      (traverseAppMatch (assocTypePats (datatypeVars d) pats0) (varE f) <$> datatypeCons d)++asTypeCon :: Monad m => String -> Type -> m Name+asTypeCon _ (ConT nm) = return nm+asTypeCon fn _ = fail $ fn ++ " expected type constructor."++-- | @structuralHash tp@ generates a function with the type+-- @Int -> tp -> Int@ that hashes type.+structuralHash :: TypeQ -> ExpQ+structuralHash tpq = do+  d <- reifyDatatype =<< asTypeCon "structuralHash" =<< tpq+  s <- newName "s"+  a <- newName "a"+  lamE [varP s, varP a] $+    caseE (varE a) (zipWith (matchHashCtor (varE s)) [0..] (datatypeCons d))++matchHashCtor :: ExpQ -> Integer  -> ConstructorInfo -> MatchQ+matchHashCtor s0 i c = do+  (pat,vars) <- conPat c "x"+  let args = [| $(litE (IntegerL i)) :: Int |] : (varE <$> vars)+  let go s e = [| hashWithSalt $(s) $(e) |]+  let rhs = foldl go s0 args+  match (pure pat) (normalB rhs) []++-- | @structuralShow tp@ generates a function with the type+-- @tp -> ShowS@ that shows the constructor.+structuralShowsPrec :: TypeQ -> ExpQ+structuralShowsPrec tpq = do+  d <- reifyDatatype =<< asTypeCon "structuralShowPrec" =<< tpq+  p <- newName "_p"+  a <- newName "a"+  lamE [varP p, varP a] $+    caseE (varE a) (matchShowCtor (varE p) <$> datatypeCons d)++showCon :: ExpQ -> Name -> Int -> MatchQ+showCon p nm n = do+  vars <- newNames "x" n+  let pat = ConP nm (VarP <$> vars)+  let go s e = [| $(s) . showChar ' ' . showsPrec 10 $(varE e) |]+  let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |]+  let rhs | null vars = ctor+          | otherwise = [| showParen ($(p) >= 10) $(foldl go ctor vars) |]+  match (pure pat) (normalB rhs) []++matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ+matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con))++-- $typePatterns+--+-- The Template Haskell instance generators 'structuralEquality',+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal'+-- employ heuristics to generate valid instances in the majority of cases.  Most+-- failures in the heuristics occur on sub-terms that are type indexed.  To+-- handle cases where these functions fail to produce a valid instance, they+-- take a list of exceptions in the form of their second parameter, which has+-- type @[('TypePat', 'ExpQ')]@.  Each 'TypePat' is a /matcher/ that tells the+-- TH generator to use the 'ExpQ' to process the matched sub-term.  Consider the+-- following example:+--+-- > data T a b where+-- >   C1 :: NatRepr n -> T () n+-- >+-- > instance TestEquality (T a) where+-- >   testEquality = $(structuralTypeEquality [t|T|]+-- >                    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])+-- >                    ])+--+-- The exception list says that 'structuralTypeEquality' should use+-- 'testEquality' to compare any sub-terms of type @'NatRepr' n@ in a value of+-- type @T@.+--+-- * 'AnyType' means that the type parameter in that position can be instantiated as any type+--+-- * @'DataArg' n@ means that the type parameter in that position is the @n@-th+--   type parameter of the GADT being traversed (@T@ in the example)+--+-- * 'TypeApp' is type application+--+-- * 'ConType' specifies a base type+--+-- The exception list could have equivalently (and more precisely) have been specified as:+--+-- > [(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]+--+-- The use of 'DataArg' says that the type parameter of the 'NatRepr' must+-- be the same as the second type parameter of @T@.

@@ -0,0 +1,116 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.TraversableF+-- Copyright        : (c) Galois, Inc 2014-2015+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module declares classes for working with structures that accept+-- a single parametric type parameter.+------------------------------------------------------------------------+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Trustworthy #-}+module Data.Parameterized.TraversableF+  ( FunctorF(..)+  , FoldableF(..)+  , TraversableF(..)+  , traverseF_+  , fmapFDefault+  , foldMapFDefault+  , allF+  , anyF+  ) where++import Control.Applicative+import Control.Monad.Identity+import Data.Coerce+import Data.Monoid+import GHC.Exts (build)++-- | A parameterized type that is a function on all instances.+class FunctorF m where+  fmapF :: (forall x . f x -> g x) -> m f -> m g++instance FunctorF (Const x) where+  fmapF _ = coerce++------------------------------------------------------------------------+-- FoldableF++-- | This is a coercision used to avoid overhead associated+-- with function composition.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)+(#.) _f = coerce++-- | This is a generalization of the @Foldable@ class to+-- structures over parameterized terms.+class FoldableF (t :: (k -> *) -> *) where+  {-# MINIMAL foldMapF | foldrF #-}++  -- | Map each element of the structure to a monoid,+  -- and combine the results.+  foldMapF :: Monoid m => (forall s . e s -> m) -> t e -> m+  foldMapF f = foldrF (mappend . f) mempty++  -- | Right-associative fold of a structure.+  foldrF :: (forall s . e s -> b -> b) -> b -> t e -> b+  foldrF f z t = appEndo (foldMapF (Endo #. f) t) z++  -- | Left-associative fold of a structure.+  foldlF :: (forall s . b -> e s -> b) -> b -> t e -> b+  foldlF f z t = appEndo (getDual (foldMapF (\e -> Dual (Endo (\r -> f r e))) t)) z++  -- | Right-associative fold of a structure,+  -- but with strict application of the operator.+  foldrF' :: (forall s . e s -> b -> b) -> b -> t e -> b+  foldrF' f0 z0 xs = foldlF (f' f0) id xs z0+    where f' f k x z = k $! f x z++  -- | Left-associative fold of a parameterized structure+  -- with a strict accumulator.+  foldlF' :: (forall s . b -> e s -> b) -> b -> t e -> b+  foldlF' f0 z0 xs = foldrF (f' f0) id xs z0+    where f' f x k z = k $! f z x++  -- | Convert structure to list.+  toListF :: (forall tp . f tp -> a) -> t f -> [a]+  toListF f t = build (\c n -> foldrF (\e v -> c (f e) v) n t)++-- | Return 'True' if all values satisfy predicate.+allF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool+allF p = getAll #. foldMapF (All #. p)++-- | Return 'True' if any values satisfy predicate.+anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool+anyF p = getAny #. foldMapF (Any #. p)++instance FoldableF (Const x) where+  foldMapF _ _ = mempty++------------------------------------------------------------------------+-- TraversableF++class (FunctorF t, FoldableF t) => TraversableF t where+  traverseF :: Applicative m+            => (forall s . e s -> m (f s))+            -> t e+            -> m (t f)++instance TraversableF (Const x) where+  traverseF _ (Const x) = pure (Const x)++-- | This function may be used as a value for `fmapF` in a `FunctorF`+-- instance.+fmapFDefault :: TraversableF t => (forall s . e s -> f s) -> t e -> t f+fmapFDefault f = runIdentity #. traverseF (Identity #. f)+{-# INLINE fmapFDefault #-}++-- | This function may be used as a value for `Data.Foldable.foldMap`+-- in a `Foldable` instance.+foldMapFDefault :: (TraversableF t, Monoid m) => (forall s . e s -> m) -> t e -> m+foldMapFDefault f = getConst #. traverseF (Const #. f)++-- | 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_ f = foldrF (\e r -> f e *> r) (pure ())

@@ -0,0 +1,161 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.TraversableFC+-- Copyright        : (c) Galois, Inc 2014-2015+-- Maintainer       : Joe Hendrix <jhendrix@galois.com>+--+-- This module declares classes for working with structures that accept+-- a parametric type parameter followed by some fixed kind.+------------------------------------------------------------------------+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeOperators #-}+module Data.Parameterized.TraversableFC+  ( TestEqualityFC(..)+  , OrdFC(..)+  , ShowFC(..)+  , HashableFC(..)+  , FunctorFC(..)+  , FoldableFC(..)+  , TraversableFC(..)+  , traverseFC_+  , forMFC_+  , fmapFCDefault+  , foldMapFCDefault+  , allFC+  , anyFC+  , lengthFC+  ) where++import Control.Applicative (Const(..) )+import Control.Monad.Identity ( Identity (..) )+import Data.Coerce+import Data.Monoid+import GHC.Exts (build)+import Data.Type.Equality++import Data.Parameterized.Classes++-- | A parameterized type that is a function on all instances.+class FunctorFC (t :: (k -> *) -> l -> *) where+  fmapFC :: forall f g. (forall x. f x -> g x) ->+                        (forall x. t f x -> t g x)++-- | A parameterized class for types which can be shown, when given+--   functions to show parameterized subterms.+class ShowFC (t :: (k -> *) -> l -> *) where+  {-# MINIMAL showFC | showsPrecFC #-}++  showFC :: forall f. (forall x. f x -> String)+         -> (forall x. t f x -> String)+  showFC sh x = showsPrecFC (\_prec z rest -> sh z ++ rest) 0 x []++  showsPrecFC :: forall f. (forall x. Int -> f x -> ShowS) ->+                           (forall x. Int -> t f x -> ShowS)+  showsPrecFC sh _prec x rest = showFC (\z -> sh 0 z []) x ++ rest+++-- | A parameterized class for types which can be hashed, when given+--   functions to hash parameterized subterms.+class HashableFC (t :: (k -> *) -> l -> *) where+  hashWithSaltFC :: forall f. (forall x. Int -> f x -> Int) ->+                              (forall x. Int -> t f x -> Int)++-- | A parameterized class for types which can be tested for parameterized equality,+--   when given an equality test for subterms.+class TestEqualityFC (t :: (k -> *) -> l -> *) where+  testEqualityFC :: forall f. (forall x y. f x -> f y -> (Maybe (x :~: y))) ->+                              (forall x y. t f x -> t f y -> (Maybe (x :~: y)))++-- | A parameterized class for types which can be tested for parameterized ordering,+--   when given an comparison test for subterms.+class TestEqualityFC t => OrdFC (t :: (k -> *) -> l -> *) where+  compareFC :: forall f. (forall x y. f x -> f y -> OrderingF x y) ->+                         (forall x y. t f x -> t f y -> OrderingF x y)++------------------------------------------------------------------------+-- FoldableF++-- | This is a coercision used to avoid overhead associated+-- with function composition.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)+(#.) _f = coerce++-- | This is a generalization of the @Foldable@ class to+-- structures over parameterized terms.+class FoldableFC (t :: (k -> *) -> l -> *) where+  {-# MINIMAL foldMapFC | foldrFC #-}++  -- | Map each element of the structure to a monoid,+  -- and combine the results.+  foldMapFC :: forall f m. Monoid m => (forall x. f x -> m) -> (forall x. t f x -> m)+  foldMapFC f = foldrFC (mappend . f) mempty++  -- | Right-associative fold of a structure.+  foldrFC :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)+  foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z++  -- | Left-associative fold of a structure.+  foldlFC :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)+  foldlFC f z t = appEndo (getDual (foldMapFC (\e -> Dual (Endo (\r -> f r e))) t)) z++  -- | Right-associative fold of a structure,+  -- but with strict application of the operator.+  foldrFC' :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)+  foldrFC' f0 z0 xs = foldlFC (f' f0) id xs z0+    where f' f k x z = k $! f x z++  -- | Left-associative fold of a parameterized structure+  -- with a strict accumulator.+  foldlFC' :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)+  foldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0+    where f' f x k z = k $! f z x++  -- | Convert structure to list.+  toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])+  toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)++-- | Return 'True' if all values satisfy predicate.+allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)+allFC p = getAll #. foldMapFC (All #. p)++-- | Return 'True' if any values satisfy predicate.+anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)+anyFC p = getAny #. foldMapFC (Any #. p)++-- | Return number of elements in list.+lengthFC :: FoldableFC t => t f x -> Int+lengthFC = foldrFC (const (+1)) 0++------------------------------------------------------------------------+-- TraversableF++class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *) where+  traverseFC :: forall f g m. Applicative m+             => (forall x. f x -> m (g x))+             -> (forall x. t f x -> m (t g x))++-- | This function may be used as a value for `fmapF` in a `FunctorF`+-- instance.+fmapFCDefault :: TraversableFC t => forall f g. (forall x. f x -> g x) -> (forall x. t f x -> t g x)+fmapFCDefault = \f -> runIdentity . traverseFC (Identity . f)+{-# INLINE fmapFCDefault #-}++-- | This function may be used as a value for `Data.Foldable.foldMap`+-- in a `Foldable` instance.+foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)+foldMapFCDefault = \f -> getConst . traverseFC (Const . f)+{-# INLINE foldMapFCDefault #-}++-- | 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_ 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_ v f = traverseFC_ f v+{-# INLINE forMFC_ #-}

@@ -0,0 +1,368 @@+{-|+Description      : Utilities for balanced binary trees.+Copyright        : (c) Galois, Inc 2014+Maintainer       : Joe Hendrix <jhendrix@galois.com>+-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Safe #-}+module Data.Parameterized.Utils.BinTree+  ( MaybeS(..)+  , fromMaybeS+  , Updated(..)+  , updatedValue+  , TreeApp(..)+  , IsBinTree(..)+  , balanceL+  , balanceR+  , glue+  , merge+  , filterGt+  , filterLt+  , insert+  , delete+  , union+  , link+  , PairS(..)+  ) where++import Control.Applicative++------------------------------------------------------------------------+-- MaybeS++-- | A strict version of 'Maybe'+data MaybeS v+   = JustS !v+   | NothingS++instance Functor MaybeS where+  fmap _ NothingS = NothingS+  fmap f (JustS v) = JustS (f v)++instance Alternative MaybeS where+  empty = NothingS+  mv@JustS{} <|> _ = mv+  NothingS <|> v = v++instance Applicative MaybeS where+  pure = JustS++  NothingS <*> _ = NothingS+  JustS{} <*> NothingS = NothingS+  JustS f <*> JustS x = JustS (f x)++fromMaybeS :: a -> MaybeS a -> a+fromMaybeS r NothingS = r+fromMaybeS _ (JustS v) = v++------------------------------------------------------------------------+-- Updated++-- | Updated a contains a value that has been flagged on whether it was+-- modified by an operation.+data Updated a+   = Updated   !a+   | Unchanged !a++updatedValue :: Updated a -> a+updatedValue (Updated a) = a+updatedValue (Unchanged a) = a++------------------------------------------------------------------------+-- IsBinTree++data TreeApp e t+   = BinTree !e !t !t+   | TipTree++class IsBinTree t e | t -> e where+  asBin :: t -> TreeApp e t+  tip :: t++  bin :: e -> t -> t -> t+  size :: t -> Int++delta,ratio :: Int+delta = 3+ratio = 2++-- `balanceL p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.+--+-- It assumes that @l@ and @r@ are close to being balanced, and that only+-- @l@ may contain too many elements.+balanceL :: (IsBinTree c e) => e -> c -> c -> c+balanceL p l r = do+  case asBin l of+    BinTree l_pair ll lr | size l > max 1 (delta*size r) ->+      case asBin lr of+        BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) ->+          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)+        _ -> bin l_pair ll (bin p lr r)++    _ -> bin p l r+{-# INLINE balanceL #-}++-- `balanceR p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.+--+-- It assumes that @l@ and @r@ are close to being balanced, and that only+-- @r@ may contain too many elements.+balanceR :: (IsBinTree c e) => e -> c -> c -> c+balanceR p l r = do+  case asBin r of+    BinTree r_pair rl rr | size r > max 1 (delta*size l) ->+      case asBin rl of+        BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) ->+          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr+        _ -> bin r_pair (bin p l rl) rr+    _ -> bin p l r+{-# INLINE balanceR #-}++-- | Insert a new maximal element.+insertMax :: IsBinTree c e => e -> c -> c+insertMax p t =+  case asBin t of+    TipTree -> bin p tip tip+    BinTree q l r -> balanceR q l (insertMax p r)++-- | Insert a new minimal element.+insertMin :: IsBinTree c e => e -> c -> c+insertMin p t =+  case asBin t of+    TipTree -> bin p tip tip+    BinTree q l r -> balanceL q (insertMin p l) r++-- | link is called to insert a key and value between two disjoint subtrees.+link :: IsBinTree c e => e -> c -> c -> c+link p l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> insertMin p r+    (_, TipTree) -> insertMax p l+    (BinTree py ly ry, BinTree pz lz rz)+     | delta*size l < size r -> balanceL pz (link p l lz) rz+     | delta*size r < size l -> balanceR py ly (link p ry r)+     | otherwise             -> bin p l r+{-# INLINE link #-}++-- | A Strict pair+data PairS f s = PairS !f !s++deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c+deleteFindMin p l r =+  case asBin l of+    TipTree -> PairS p r+    BinTree lp ll lr ->+      case deleteFindMin lp ll lr of+        PairS q l' -> PairS q (balanceR p l' r)+{-# INLINABLE deleteFindMin #-}++deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c+deleteFindMax p l r =+  case asBin r of+    TipTree -> PairS p l+    BinTree rp rl rr ->+      case deleteFindMax rp rl rr of+        PairS q r' -> PairS q (balanceL p l r')+{-# INLINABLE deleteFindMax #-}++-- | Concatenate two trees that are ordered with respect to each other.+merge :: IsBinTree c e => c -> c -> c+merge l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> r+    (_, TipTree) -> l+    (BinTree x lx rx, BinTree y ly ry)+      | delta*size l < size r -> balanceL y (merge l ly) ry+      | delta*size r < size l -> balanceR x lx (merge rx r)+      | size l > size r ->+        case deleteFindMax x lx rx of+          PairS q l' -> balanceR q l' r+      | otherwise ->+        case deleteFindMin y ly ry of+          PairS q r' -> balanceL q l r'+{-# INLINABLE merge #-}++------------------------------------------------------------------------+-- Ordered operations++-- | @insert p m@ inserts the binding into @m@.  It returns+-- an Unchanged value if the map stays the same size and an updated+-- value if a new entry was inserted.+insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c+insert comp x t =+  case asBin t of+    TipTree -> Updated (bin x tip tip)+    BinTree y l r ->+      case comp x y of+        LT ->+          case insert comp x l of+            Updated l'   -> Updated   (balanceL y l' r)+            Unchanged l' -> Unchanged (bin       y l' r)+        GT ->+          case insert comp x r of+            Updated r'   -> Updated   (balanceR y l r')+            Unchanged r' -> Unchanged (bin       y l r')+        EQ -> Unchanged (bin x l r)+{-# INLINABLE insert #-}++-- | 'glue l r' concatenates @l@ and @r@.+--+-- It assumes that @l@ and @r@ are already balanced with respect to each other.+glue :: IsBinTree c e => c -> c -> c+glue l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> r+    (_, TipTree) -> l+    (BinTree x lx rx, BinTree y ly ry)+     | size l > size r ->+       case deleteFindMax x lx rx of+         PairS q l' -> balanceR q l' r+     | otherwise ->+       case deleteFindMin y ly ry of+         PairS q r' -> balanceL q l r'+{-# INLINABLE glue #-}++delete :: IsBinTree c e+       => (e -> Ordering)+          -- ^ Predicate that returns whether the entry is less than, greater than, or equal+          -- to the key we are entry that we are looking for.+       -> c+       -> MaybeS c+delete k t =+  case asBin t of+    TipTree -> NothingS+    BinTree p l r ->+      case k p of+        LT -> (\l' -> balanceR p l' r) <$> delete k l+        GT -> (\r' -> balanceL p l r') <$> delete k r+        EQ -> JustS (glue l r)+{-# INLINABLE delete #-}++------------------------------------------------------------------------+-- filter++-- | Returns only entries that are less than predicate with respect to the ordering+-- and Nothing if no elements are discared.+filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c+filterGt k t =+  case asBin t of+    TipTree -> NothingS+    BinTree x l r ->+      case k x of+        LT -> (\l' -> link x l' r) <$> filterGt k l+        GT -> filterGt k r <|> JustS r+        EQ -> JustS r+{-# INLINABLE filterGt #-}+++-- | @filterLt' k m@ returns submap of @m@ that only contains entries+-- that are smaller than @k@.  If no entries are deleted then return Nothing.+filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c+filterLt k t =+  case asBin t of+    TipTree -> NothingS+    BinTree x l r ->+      case k x of+        LT -> filterLt k l <|> JustS l+        GT -> (\r' -> link x l r') <$> filterLt k r+        EQ -> JustS l+{-# INLINABLE filterLt #-}++------------------------------------------------------------------------+-- Union++-- Insert a new key and value in the map if it is not already present.+-- Used by `union`.+insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c+insertR comp e m = fromMaybeS m (go e m)+  where+    go :: e -> c -> MaybeS c+    go x t =+      case asBin t of+        TipTree -> JustS (bin x tip tip)+        BinTree y l r ->+          case comp x y of+            LT -> (\l' -> balanceL y l' r) <$> go x l+            GT -> (\r' -> balanceR y l r') <$> go x r+            EQ -> NothingS+{-# INLINABLE insertR #-}++-- | Union two sets+union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c+union comp t1 t2 =+  case (asBin t1, asBin t2) of+    (TipTree, _) -> t2+    (_, TipTree) -> t1+    (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_UB comp x   l t2)+           (hedgeUnion_LB comp x r   t2)+{-# INLINABLE union #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly above a lower bound.+hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c+hedgeUnion_LB comp lo t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2)+    -- Prune left tree.+    (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_LB_UB comp lo x  l t2)+           (hedgeUnion_LB    comp x     r t2)+{-# INLINABLE hedgeUnion_LB #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly below a upper bound.+hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c+hedgeUnion_UB comp hi t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2)+    -- Prune right tree.+    (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree))  -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_UB    comp x      l t2)+           (hedgeUnion_LB_UB comp x  hi  r t2)+{-# INLINABLE hedgeUnion_UB #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly between a lower and upper bound.+hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c+hedgeUnion_LB_UB comp lo hi t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    -- Prune left tree.+    (_,   BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r+    -- Prune right tree.+    (_,   BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l+    -- When t1 becomes empty (assumes lo <= k <= hi)+    (TipTree, BinTree x l r) ->+      case (filterGt (comp lo) l, filterLt (comp hi) r) of+        -- No variables in t2 were eliminated.+        (NothingS, NothingS) -> t2+        -- Relink t2 with filtered elements removed.+        (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r')+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_LB_UB comp lo x  l t2)+           (hedgeUnion_LB_UB comp x  hi r t2)+{-# INLINABLE hedgeUnion_LB_UB #-}

@@ -0,0 +1,170 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+module Test.Context+( contextTests+) where++import Test.Tasty+import Test.QuickCheck+import Test.Tasty.QuickCheck++import Control.Lens+import Data.Parameterized.Classes+import Data.Parameterized.TraversableFC+import Data.Parameterized.Some++import qualified Data.Parameterized.Context.Safe as S+import qualified Data.Parameterized.Context.Unsafe as U++data Payload (ty :: *) where+  IntPayload    :: Int -> Payload Int+  StringPayload :: String -> Payload String+  BoolPayload   :: Bool -> Payload Bool++instance TestEquality Payload where+  testEquality (IntPayload x) (IntPayload y) = if x == y then Just Refl else Nothing+  testEquality (StringPayload x) (StringPayload y) = if x == y then Just Refl else Nothing+  testEquality (BoolPayload x) (BoolPayload y) = if x == y then Just Refl else Nothing+  testEquality _ _ = Nothing++instance Show (Payload tp) where+  show (IntPayload x) = show x+  show (StringPayload x) = show x+  show (BoolPayload x) = show x++instance ShowF Payload++instance Arbitrary (Some Payload) where+  arbitrary = oneof+    [ Some . IntPayload <$> arbitrary+    , Some . StringPayload <$> arbitrary+    , Some . BoolPayload <$> arbitrary+    ]++type UAsgn = U.Assignment Payload+type SAsgn = S.Assignment Payload++mkUAsgn :: [Some Payload] -> Some UAsgn+mkUAsgn = go U.empty+ where go :: UAsgn ctx -> [Some Payload] -> Some UAsgn+       go a [] = Some a+       go a (Some x : xs) = go (U.extend a x) xs++mkSAsgn :: [Some Payload] -> Some SAsgn+mkSAsgn = go S.empty+ where go :: SAsgn ctx -> [Some Payload] -> Some SAsgn+       go a [] = Some a+       go a (Some x : xs) = go (S.extend a x) xs++instance Arbitrary (Some UAsgn) where+  arbitrary = mkUAsgn <$> arbitrary+instance Arbitrary (Some SAsgn) where+  arbitrary = mkSAsgn <$> arbitrary++twiddle :: Payload a -> Payload a+twiddle (IntPayload n) = IntPayload (n+1)+twiddle (StringPayload str) = StringPayload (str++"asdf")+twiddle (BoolPayload b) = BoolPayload (not b)++contextTests :: IO TestTree+contextTests = testGroup "Context" <$> return+   [ testProperty "safe_index_eq" $ \v vs i -> ioProperty $ do+         let vals = v:vs+         let i' = min (max 0 i) (length vals - 1)+         Some a <- return $ mkSAsgn vals+         Just (Some idx) <- return $ S.intIndex i' (S.size a)+         return (Some (a S.! idx) == vals !! i')+   , testProperty "unsafe_index_eq" $ \v vs i -> ioProperty $ do+         let vals = v:vs+         let i' = min (max 0 i) (length vals - 1)+         Some a <- return $ mkUAsgn vals+         Just (Some idx) <- return $ U.intIndex i' (U.size a)+         return (Some (a U.! idx) == vals !! i')+   , testProperty "safe_tolist" $ \vals -> ioProperty $ do+         Some a <- return $ mkSAsgn vals+         let vals' = toListFC Some a+         return (vals == vals')+   , testProperty "unsafe_tolist" $ \vals -> ioProperty $ do+         Some a <- return $ mkUAsgn vals+         let vals' = toListFC Some a+         return (vals == vals')+   , testProperty "adjust test monadic" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array+         Some x <- return $ mkUAsgn vals+         Some y <- return $ mkSAsgn vals+         let i' = min (max 0 i) (length vals - 1)++         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++         x' <- U.adjustM (return . twiddle) idx_x x+         y' <- S.adjustM (return . twiddle) idx_y y++         return (toListFC Some x' == toListFC Some y')++   , testProperty "adjust test" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array+         Some x <- return $ mkUAsgn vals+         Some y <- return $ mkSAsgn vals+         let i' = min (max 0 i) (length vals - 1)++         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++         let x' = over (ixF idx_x) twiddle x+             y' = (ixF idx_y) %~ twiddle $ y+             x'' = U.adjust twiddle idx_x x+             y'' = S.adjust twiddle idx_y y++         return (toListFC Some x' == toListFC Some y' &&+                 -- adjust actually modified the entry+                 toListFC Some x /= toListFC Some x' &&+                 toListFC Some y /= toListFC Some y' &&+                 -- verify new version is equivalent to older deprecated version+                 toListFC Some x'' == toListFC Some x' &&+                 toListFC Some y'' == toListFC Some y')++   , testProperty "update test" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array+         Some x <- return $ mkUAsgn vals+         Some y <- return $ mkSAsgn vals+         let i' = min (max 0 i) (length vals - 1)++         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++         let x' = over (ixF idx_x) twiddle x+             y' = (ixF idx_y) %~ twiddle $ y+             updX = set (ixF idx_x) (x' U.! idx_x) x+             updY = (ixF idx_y) .~  (y' S.! idx_y) $ y+             updX' = U.update idx_x (x' U.! idx_x) x+             updY' = S.update idx_y (y' S.! idx_y) y++         return (toListFC Some updX == toListFC Some updY &&+                 -- update actually modified the entry+                 toListFC Some x /= toListFC Some updX &&+                 toListFC Some y /= toListFC Some updY &&+                 -- update modified the expected entry+                 toListFC Some x' == toListFC Some updX &&+                 toListFC Some y' == toListFC Some updY &&+                 -- verify new version is equivalent to older deprecated version+                 toListFC Some updX == toListFC Some updX' &&+                 toListFC Some updY == toListFC Some updY'+                )++   , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do+         Some x <- return $ mkSAsgn vals1+         Some y <- return $ mkSAsgn vals2+         case testEquality x y of+           Just Refl -> return $ vals1 == vals2+           Nothing   -> return $ vals1 /= vals2+   , testProperty "unsafe_eq" $ \vals1 vals2 -> ioProperty $ do+         Some x <- return $ mkUAsgn vals1+         Some y <- return $ mkUAsgn vals2+         case testEquality x y of+           Just Refl -> return $ vals1 == vals2+           Nothing   -> return $ vals1 /= vals2+   ]

@@ -0,0 +1,18 @@+module Test.NatRepr+( natTests+) where++import Test.Tasty+import Test.Tasty.QuickCheck++import Data.Parameterized.NatRepr+import Data.Parameterized.Some+import GHC.TypeLits++natTests :: IO TestTree+natTests = testGroup "Nat" <$> return+  [ testProperty "withKnownNat" $ \nInt ->+      case someNat nInt of+        Nothing -> nInt < 0+        Just (Some r) -> nInt == withKnownNat r (natVal r)+  ]

@@ -0,0 +1,22 @@+import Test.Tasty+import Test.Tasty.Ingredients+import Test.Tasty.Runners.AntXML++import qualified Test.Context+import qualified Test.NatRepr++main :: IO ()+main = tests >>= defaultMainWithIngredients ingrs++ingrs :: [Ingredient]+ingrs =+   [ antXMLRunner+   ]+   +++   defaultIngredients++tests :: IO TestTree+tests = testGroup "ParameterizedUtils" <$> sequence+  [ Test.Context.contextTests+  , Test.NatRepr.natTests+  ]