parameterized-utils 1.0.1 → 2.0

raw patch · 34 files changed

+2383/−322 lines, 34 filesdep +constraintsdep ~QuickCheckdep ~basedep ~hashablesetup-changednew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: constraints

Dependency ranges changed: QuickCheck, base, hashable, hashtables, lens, tasty, tasty-ant-xml, tasty-hunit, tasty-quickcheck, vector

API changes (from Hackage documentation)

Files

• Changelog.md +138/−0
• Setup.hs +0/−2
• parameterized-utils.cabal +51/−34
• src/Data/Parameterized/BoolRepr.hs +121/−0
• src/Data/Parameterized/Classes.hs +26/−4
• src/Data/Parameterized/ClassesC.hs +53/−0
• src/Data/Parameterized/Compose.hs +46/−0
• src/Data/Parameterized/Context.hs +39/−5
• src/Data/Parameterized/Context/Safe.hs +28/−8
• src/Data/Parameterized/Context/Unsafe.hs +35/−17
• src/Data/Parameterized/Ctx.hs +1/−1
• src/Data/Parameterized/Ctx/Proofs.hs +3/−2
• src/Data/Parameterized/DecidableEq.hs +38/−0
• src/Data/Parameterized/HashTable.hs +5/−4
• src/Data/Parameterized/List.hs +5/−4
• src/Data/Parameterized/Map.hs +99/−40
• src/Data/Parameterized/NatRepr.hs +191/−104
• src/Data/Parameterized/NatRepr/Internal.hs +99/−0
• src/Data/Parameterized/Nonce.hs +51/−44
• src/Data/Parameterized/Nonce/Transformers.hs +3/−2
• src/Data/Parameterized/Pair.hs +2/−1
• src/Data/Parameterized/Peano.hs +501/−0
• src/Data/Parameterized/Some.hs +2/−1
• src/Data/Parameterized/SymbolRepr.hs +2/−3
• src/Data/Parameterized/TH/GADT.hs +16/−11
• src/Data/Parameterized/TraversableF.hs +36/−5
• src/Data/Parameterized/TraversableFC.hs +5/−4
• src/Data/Parameterized/Utils/BinTree.hs +10/−10
• src/Data/Parameterized/Utils/Endian.hs +16/−0
• src/Data/Parameterized/Vector.hs +560/−0
• src/Data/Parameterized/WithRepr.hs +115/−0
• test/Test/Context.hs +14/−16
• test/Test/Vector.hs +70/−0
• test/UnitTest.hs +2/−0

@@ -0,0 +1,138 @@+# Changelog for the `parameterized-utils` package++## 2.0 -- *2019 Apr 03*++  * Drop support for GHC versions prior to GHC 8.2+  * Various Haddock and module updates.+  * Data.Parameterized.Classes+    - Added function: `ordFCompose`+    - Added `OrdF` instance for `Compose`+  * Data.Parameterized.ClassesC+    - Marked as `Safe` haskell via pragma+    - Added `OrdC` instance for `Some`+  * Data.Parameterized.Compose+    - Update `testEqualityComposeBare` to be more kind-polymorphic.+    - Marked as `Safe` haskell via pragma+  * Data.Parameterized.Context+    - Added `diffIsAppend` function to extract the contextual+      difference between two `Context`s (as a `Diff`) as an `IsAppend`+      (new) data value if the left is a sub-context of the right.+  * Data.Parameterized.NatRepr+    - Change runtime representation from `Int` to `Natural`+    - Add function `intValue` to recover an `Int` from a `NatRepr`.+    - Add constructor function `mkNatRepr` to construct a `NatRepr`+      from a `Natural`.+    - Removed awkward backdoor for directly creating `NatRepr` values;+      the single needed internal usage is now handled internally.+  * Data.Parameterized.Peano+    - Newly added module.+    - Defines a type `Peano` and `PeanoRepr` for representing a+      type-level natural at runtime.+    - The runtime representation of `PeanoRepr` is `Word64`+    - Has both safe and unsafe implementations.+  * Data.Parameterized.WithRepr+    - Newly added module.+    - This module declares a class `IsRepr` with a single method+      `withRepr` that can be used to derive a 'KnownRepr' constraint+      from an explicit 'Repr' argument. Clients of this method need+      only create an empty instance. The default implementation+      suffices.++## 1.0.8 -- *2019 Feb 01*++  * Data.Parameterized.Map+    - Fixed `MapF` functions `filter` and `filterWithKey`+    - Added `MapF` function: `mapWithKey`+  * Data.Parameterized.NatRepr+    - Un-deprecate `withKnownNat`+  * Data.Parameterized.Context+    - Updated some haddock documentation (esp. `CtxEmbedding` data structure).+  * Data.Parameterized.Nonce+    - Fixed `newIONonceGenerator` haddock documentation (IO monad, not ST monad).+    - Added `countNoncesGenerated` for profiling Nonce usage.+  * Data.Parameterized.TraversableF+    - Added `FunctorF`, `FoldableF`, and `TraversableF` instances for+      `Compose` from Data.Functor.Compose+  * Data.Parameterized.ClassesC+    - Newly added module.+    - Declares `TestEqualityC` and `OrdC` classes for working with+      types that have kind `(k -> *) -> *` for any `k`.+  * Data.Parameterized.Compose+    - Newly added module.+    - Orphan instance and `testEqualityComposeBare` function for+      working with Data.Functor.Compose.+  * Data.Parameterized.TestEquality+    - Newly added module.+    - Utilities for working with Data.Type.TestEquality.++## 1.0.7 -- *2018 Nov 17*++  * Data.Parameterized.Map+    - Added `MapF` functions:+      - `filter`+      - `filterWithKey`++## 1.0.6 -- *2018 Nov 19*++  * Add support for GHC 8.6.+  * Data.Parameterized.Map+    - Added functions:+       - `foldlWithKey` and `foldlWithKey'` (strict)+       - `foldrWithKey` and `foldrWithKey'` (strict)+       - `mapMaybeWithKey`++## 1.0.5 -- *2018 Sep 04*++  * Data.Parameterized.Context+      - Add function: `take`, `appendEmbedding`, `appendDiff`+      - Diff is type role nominal in both parameters.++## 1.0.4 -- *2018 Aug 29*++  * Data.Parameterized.Context+    - Add `traverseAndCollect`.  Allows traversal of an Assignment in+      order from left to right, collecting the results of a visitor+      function monoidically.+  * Data.Parameterized.DecidableEq+    - Newly added module.  The `DecidableEq` class represents+      decideable equality on a type family as a superclass of+      `TestEquality`, where the latter cannot provide evidence of+      non-equality.+  * Data.Parameterized.NatRepr+    - Add `DecidableEq` instance for NatRepr.+    - Add functions:+      - `decideLeq`+      - `isZeroOrGT1`+      - `lessThanIrreflexive`+      - `lessThanAsymmetric`+      - `natRecStrong`  -- recursor with strong induction+      - `natRecBounded` -- bounded recursor+      - `natFromZero`+  * Data.Parameterized.Vector+    - Add construction functions: `singleton`, `cons`, `snoc`, `generate`, and `generateM`+    - Add functions: `splitWithA` (applicative `splitWith`).++## 1.0.3 -- *2018 Aug 24*++  * Move `lemmaMul` from Vector to NatRepr.+  * Add stricter role annotations:+    - `NatRepr` is nominal.+    - `Vector` is nominal in the first parameter and representational in the second.+  * Data.Parameterized.NatRepr+    - Provide a backdoor for directly creating `NatRepr` values.  Use carefully.+  * Data.Parameterized.Vector+    - Add Show and Eq instances+    - Add functions: `joinWithM`, `reverse`++## 1.0.2 -- *2018 Aug 23*++  * Allow function passed to `traverseF_`, `traverseFC_`, and+    `forMFC_` to return a value instead of null (`()`).+  * Data.Parameterized.Vector+    - Newly added module.  A fixed-size vector of typed elements.+  * Data.Parameterized.Utils.Endian+    - Newly added module.  Used in Vector.++## 1.0.1 -- *2018 Aug 13*++  Baseline for changelog tracking.

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

@@ -1,12 +1,14 @@ Name:          parameterized-utils-Version:       1.0.1+Version:       2.0 Author:        Galois Inc.-Maintainer:    jhendrix@galois.com+Maintainer:    jhendrix@galois.com, kquick@galois.com+stability:     stable Build-type:    Simple Cabal-version: >= 1.9.2-license: BSD3-license-file: LICENSE-category: Data Structures, Dependent Types+Copyright:     ©2016-2019 Galois, Inc.+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@@ -14,6 +16,10 @@   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.+extra-source-files: Changelog.md+homepage:      https://github.com/GaloisInc/parameterized-utils+bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues+tested-with:   GHC==8.2.2, GHC==8.4.4, GHC==8.6.4  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -21,7 +27,7 @@ -- Unsafe.Coerce and Data.Coerce.  These alternate implementations -- impose a significant performance hit. flag unsafe-operations-  Description: Use unsafe operations to improve performance+  Description: Use unsafe operations (e.g. coercions) to improve performance   Default: True  source-repository head@@ -29,30 +35,34 @@   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+  build-depends: base >= 4.10 && < 5+               , th-abstraction >=0.1 && <0.3+               , constraints == 0.10.*+               , containers+               , deepseq+               , ghc-prim+               , hashable == 1.2.*+               , hashtables == 1.2.*+               , lens == 4.17.*+               , mtl+               , template-haskell+               , text+               , vector == 0.12.*    hs-source-dirs: src    exposed-modules:     Data.Parameterized+    Data.Parameterized.BoolRepr                       Data.Parameterized.Classes+    Data.Parameterized.ClassesC+    Data.Parameterized.Compose     Data.Parameterized.Context     Data.Parameterized.Context.Safe     Data.Parameterized.Context.Unsafe     Data.Parameterized.Ctx     Data.Parameterized.Ctx.Proofs+    Data.Parameterized.DecidableEq     Data.Parameterized.HashTable     Data.Parameterized.List     Data.Parameterized.Map@@ -60,14 +70,21 @@     Data.Parameterized.Nonce     Data.Parameterized.Nonce.Transformers     Data.Parameterized.Nonce.Unsafe+    Data.Parameterized.Pair+    Data.Parameterized.Peano     Data.Parameterized.Some     Data.Parameterized.SymbolRepr-    Data.Parameterized.Pair     Data.Parameterized.TH.GADT     Data.Parameterized.TraversableF     Data.Parameterized.TraversableFC     Data.Parameterized.Utils.BinTree+    Data.Parameterized.Utils.Endian+    Data.Parameterized.Vector+    Data.Parameterized.WithRepr                   +  other-modules:+    Data.Parameterized.NatRepr.Internal+   ghc-options: -Wall    if flag(unsafe-operations)@@ -80,21 +97,21 @@    ghc-options: -Wall -  main-is:UnitTest.hs+  main-is: UnitTest.hs   other-modules:     Test.Context     Test.NatRepr+    Test.Vector -  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+  build-depends: base+               , hashable+               , hashtables+               , ghc-prim+               , lens+               , mtl+               , parameterized-utils+               , tasty == 1.2.*+               , tasty-ant-xml == 1.1.*+               , tasty-hunit >= 0.9 && < 0.11+               , tasty-quickcheck >= 0.8.1 && < 0.11+               , QuickCheck >= 2.7 && < 2.14

@@ -0,0 +1,121 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Data.Parameterized.BoolRepr+  ( module Data.Type.Bool+  , BoolRepr(..)+  , ifRepr, notRepr, (%&&), (%||)+  , KnownBool++  , someBool++  -- * Re-exports+  , TestEquality(..)+  , (:~:)(..)+  , Data.Parameterized.Some.Some+  )+where++import           Data.Parameterized.Classes+import           Data.Parameterized.DecidableEq+import           Data.Parameterized.Some++import           Data.Type.Bool+import           Data.Hashable++-- | +data BoolRepr (b :: Bool) where+  FalseRepr :: BoolRepr 'False+  TrueRepr  :: BoolRepr 'True++  +-- | conditional +ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)+ifRepr TrueRepr b _ = b+ifRepr FalseRepr _ c = c++-- | negation+notRepr :: BoolRepr b -> BoolRepr (Not b)+notRepr TrueRepr = FalseRepr+notRepr FalseRepr = TrueRepr++-- | Conjunction +(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)+FalseRepr %&& _ = FalseRepr+TrueRepr  %&& a = a+infixr 3 %&&++-- | Disjunction +(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)+FalseRepr %|| a = a+TrueRepr  %|| _ = TrueRepr+infixr 2 %||  ++instance Hashable (BoolRepr n) where+  hashWithSalt i TrueRepr  = hashWithSalt i True+  hashWithSalt i FalseRepr = hashWithSalt i False+++instance Eq (BoolRepr m) where+  _ == _ = True++instance TestEquality BoolRepr where+  testEquality TrueRepr TrueRepr   = Just Refl+  testEquality FalseRepr FalseRepr = Just Refl+  testEquality _ _ = Nothing++instance DecidableEq BoolRepr where+  decEq TrueRepr  TrueRepr  = Left Refl+  decEq FalseRepr FalseRepr = Left Refl+  decEq TrueRepr  FalseRepr = Right $ \case {}+  decEq FalseRepr TrueRepr  = Right $ \case {}++instance OrdF BoolRepr where+  compareF TrueRepr  TrueRepr  = EQF+  compareF FalseRepr FalseRepr = EQF+  compareF TrueRepr  FalseRepr = GTF+  compareF FalseRepr TrueRepr  = LTF++instance PolyEq (BoolRepr m) (BoolRepr n) where+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y++instance Show (BoolRepr m) where+  show FalseRepr = "FalseRepr"+  show TrueRepr  = "TrueRepr"+  +instance ShowF BoolRepr++instance HashableF BoolRepr where+  hashWithSaltF = hashWithSalt+++----------------------------------------------------------+-- * Implicit runtime booleans++type KnownBool = KnownRepr BoolRepr++instance KnownRepr BoolRepr 'True where+  knownRepr = TrueRepr+instance KnownRepr BoolRepr 'False where+  knownRepr = FalseRepr++someBool :: Bool -> Some BoolRepr+someBool True  = Some TrueRepr+someBool False = Some FalseRepr

@@ -1,6 +1,7 @@ {-|-Copyright        : (c) Galois, Inc 2014-2015-Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : Classes for working with type of kind @k -> *@+Copyright   : (c) Galois, Inc 2014-2019+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@@ -37,6 +38,7 @@   , orderingF_refl   , toOrdering   , fromOrdering+  , ordFCompose     -- * Typeclass generalizations   , ShowF(..)   , showsF@@ -55,11 +57,14 @@   ) where  import Data.Functor.Const+import Data.Functor.Compose (Compose(..)) import Data.Hashable import Data.Maybe (isJust) import Data.Proxy import Data.Type.Equality as Equality +import Data.Parameterized.Compose ()+ -- We define these type alias here to avoid importing Control.Lens -- modules, as this apparently causes problems with the safe Hasekll -- checking.@@ -134,8 +139,8 @@ 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 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)@@ -193,6 +198,23 @@             -> (a ~ b => OrderingF c d)             -> OrderingF c d lexCompareF x y = joinOrderingF (compareF x y)++-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated+-- for the \"inner\" functor. The type-level evidence of equality is deduced+-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.+ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y.+                (forall w z. f w -> f z -> OrderingF w z)+            -> Compose f g x+            -> Compose f g y+            -> OrderingF x y+ordFCompose ordF_ (Compose x) (Compose y) =+  case ordF_ x y of+    LTF -> LTF+    GTF -> GTF+    EQF -> EQF++instance OrdF f => OrdF (Compose f g) where+  compareF x y = ordFCompose compareF x y  ------------------------------------------------------------------------ -- ShowF

@@ -0,0 +1,53 @@+{-|+Description : Classes for working with type of kind @(k -> *) -> *@+Copyright   : (c) Galois, Inc 2014-2019+Maintainer  : Langston Barrett <langston@galois.com>++This module declares classes for working with types with the kind+@(k -> *) -> *@ for any kind @k@.++These classes generally require type-level evidence for operations+on their subterms, but don't actually provide it themselves (because+their types are not themselves parameterized, unlike those in+"Data.Parameterized.TraverableFC").++Note that there is still some ambiguity around naming conventions, see+<https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.+-}++{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.ClassesC+  ( TestEqualityC(..)+  , OrdC(..)+  ) where++import Data.Type.Equality ((:~:)(..))+import Data.Maybe (isJust)+import Data.Parameterized.Classes (OrderingF, toOrdering)+import Data.Parameterized.Some (Some(..))++class TestEqualityC (t :: (k -> *) -> *) where+  testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))+                -> t f+                -> t f+                -> Bool++class TestEqualityC t => OrdC (t :: (k -> *) -> *) where+  compareC :: (forall x y. f x -> g y -> OrderingF x y)+           -> t f+           -> t g+           -> Ordering++-- | This instance demonstrates where the above class is useful: namely, in+-- types with existential quantification.+instance TestEqualityC Some where+  testEqualityC subterms (Some someone) (Some something) =+    isJust (subterms someone something)++instance OrdC Some where+  compareC subterms (Some someone) (Some something) =+    toOrdering (subterms someone something)

@@ -0,0 +1,46 @@+{-|+Description : utilities for working with "Data.Functor.Compose"+Copyright   : (c) Galois, Inc 2014-2019+Maintainer  : Langston Barrett <langston@galois.com>++Utilities for working with "Data.Functor.Compose".++NB: This module contains an orphan instance. It will be included in GHC 8.10,+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+-}++{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Safe #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Data.Parameterized.Compose+  ( testEqualityComposeBare+  ) where++import Data.Functor.Compose+import Data.Type.Equality++-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.+--+-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y.+                           (forall w z. f w -> f z -> Maybe (w :~: z))+                        -> Compose f g x+                        -> Compose f g y+                        -> Maybe (x :~: y)+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =+  case (testEquality_ x y :: Maybe (g x :~: g y)) of+    Just Refl -> Just (Refl :: x :~: y)+    Nothing   -> Nothing++testEqualityCompose :: forall (f :: k -> *) (g :: l -> k) x y. (TestEquality f)+                    => Compose f g x+                    -> Compose f g y+                    -> Maybe (x :~: y)+testEqualityCompose = testEqualityComposeBare testEquality++instance (TestEquality f) => TestEquality (Compose f g) where+  testEquality = testEqualityCompose

@@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- | -- Module           : Data.Parameterized.Context--- Copyright        : (c) Galois, Inc 2014-16+-- Copyright        : (c) Galois, Inc 2014-2019 -- Maintainer       : Joe Hendrix <jhendrix@galois.com> -- -- This module reexports either "Data.Parameterized.Context.Safe"@@ -46,10 +46,13 @@   , Data.Parameterized.Context.init   , Data.Parameterized.Context.last   , Data.Parameterized.Context.view+  , Data.Parameterized.Context.take   , forIndexM   , generateSome   , generateSomeM   , fromList+  , traverseAndCollect+     -- * Context extension and embedding utilities   , CtxEmbedding(..)   , ExtendContext(..)@@ -60,6 +63,7 @@   , extendEmbeddingRightDiff   , extendEmbeddingRight   , extendEmbeddingBoth+  , appendEmbedding   , ctxeSize   , ctxeAssignment @@ -80,10 +84,12 @@   , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6   ) where +import           Control.Applicative (liftA2) import           Control.Lens hiding (Index, (:>), Empty) import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import           GHC.TypeLits (Nat, type (-))+import           Data.Monoid ((<>))  import           Data.Parameterized.Classes import           Data.Parameterized.Some@@ -159,7 +165,7 @@ #endif  ----------------------------------------------------------------------------------- | Views+-- Views  -- | Return true if assignment is empty. null :: Assignment f ctx -> Bool@@ -188,10 +194,15 @@ view :: forall f ctx . Assignment f ctx -> AssignView f ctx view = viewAssign +take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx+take sz sz' asgn =+  let diff = appendDiff sz' in+  generate sz (\i -> asgn ! extendIndex' diff i)+ ----------------------------------------------------------------------------------- | Context embedding.+-- Context embedding. --- This datastructure contains a proof that the first context is+-- | This datastructure contains a proof that the first context is -- embeddable in the second.  This is useful if we want to add extend -- an existing term under a larger context. @@ -255,6 +266,11 @@ extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) extendEmbeddingRight = extendEmbeddingRightDiff knownDiff +appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')+appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))+  where+  diff = appendDiff sz'+ extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))   where@@ -305,7 +321,7 @@   ----------------------------------------------------------------------------------- CurryAssignment+-- * CurryAssignment  -- | This type family is used to define currying\/uncurrying operations -- on assignments.  It is best understood by seeing its evaluation on@@ -346,6 +362,24 @@   where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)         go prev [] = Some prev         go prev (Some g:next) = (go $! prev `extend` g) next+++newtype Collector m w a = Collector { runCollector :: m w }+instance Functor (Collector m w) where+  fmap _ (Collector x) = Collector x+instance (Applicative m, Monoid w) => Applicative (Collector m w) where+  pure _ = Collector (pure mempty)+  Collector x <*> Collector y = Collector (liftA2 (<>) x y)++-- | Visit each of the elements in an @Assignment@ in order+--   from left to right and collect the results using the provided @Monoid@.+traverseAndCollect ::+  (Monoid w, Applicative m) =>+  (forall tp. Index ctx tp -> f tp -> m w) ->+  Assignment f ctx ->+  m w+traverseAndCollect f =+  runCollector . traverseWithIndex (\i x -> Collector (f i x))  -------------------------------------------------------------------------------- -- Size and Index values

@@ -32,7 +32,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE IncoherentInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -60,9 +59,12 @@   , Diff   , noDiff   , extendRight+  , appendDiff   , DiffView(..)   , viewDiff   , KnownDiff(..)+  , IsAppend(..)+  , diffIsAppend     -- * Indexing   , Index   , indexVal@@ -186,6 +188,10 @@ extendRight :: Diff l r -> Diff l (r '::> tp) extendRight diff = DiffThere diff +appendDiff :: Size r -> Diff l (l <+> r)+appendDiff SizeZero = DiffHere+appendDiff (SizeSucc sz) = DiffThere (appendDiff sz)+ composeDiff :: Diff a b -> Diff b c -> Diff a c composeDiff x DiffHere = x composeDiff x (DiffThere y) = DiffThere (composeDiff x y)@@ -199,6 +205,18 @@ extSize sz DiffHere = sz extSize sz (DiffThere diff) = incSize (extSize sz diff) +-- | Proof that @r = l <+> app@ for some @app@+data IsAppend l r where+  IsAppend :: Size app -> IsAppend l (l <+> app)++-- | If @l@ is a sub-context of @r@ then extract out their "contextual+-- difference", i.e., the @app@ such that @r = l <+> app@+diffIsAppend :: Diff l r -> IsAppend l r+diffIsAppend DiffHere = IsAppend zeroSize+diffIsAppend (DiffThere diff) =+  case diffIsAppend diff of+    IsAppend sz -> IsAppend (incSize sz)+ data DiffView a b where   NoDiff :: DiffView a a   ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)@@ -280,9 +298,10 @@ 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.+-- | Given a size @n@, an initial value @v0@, and a function @f@, the+-- expression @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)@@ -321,9 +340,10 @@ 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.+-- | Given an index @i@, size @n@, a function @f@, value @v@, and a+-- function @f@, the expression @forIndexRange i n f v@ is equivalent+-- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@+-- otherwise. forIndexRange :: Int               -> Size ctx               -> (forall tp . Index ctx tp -> r -> r)@@ -409,7 +429,7 @@ replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx replicate n c = generate n (\_ -> c) --- | Create empty indexec vector.+-- | Create empty indexed vector. empty :: Assignment f 'EmptyCtx empty = AssignmentEmpty 

@@ -1,6 +1,5 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE GADTs #-}@@ -32,9 +31,12 @@   , Diff   , noDiff   , extendRight+  , appendDiff   , DiffView(..)   , viewDiff   , KnownDiff(..)+  , IsAppend(..)+  , diffIsAppend     -- * Indexing   , Index   , indexVal@@ -147,6 +149,8 @@ newtype Diff (l :: Ctx k) (r :: Ctx k)       = Diff { _contextExtSize :: Int } +type role Diff nominal nominal+ -- | The identity difference. noDiff :: Diff l l noDiff = Diff 0@@ -155,6 +159,9 @@ extendRight :: Diff l r -> Diff l (r '::> tp) extendRight (Diff i) = Diff (i+1) +appendDiff :: Size r -> Diff l (l <+> r)+appendDiff (Size r) = Diff r+ instance Cat.Category Diff where   id = Diff 0   Diff j . Diff i = Diff (i + j)@@ -168,6 +175,15 @@ addSize (Size x) (Size y) = Size (x + y)  +-- | Proof that @r = l <+> app@ for some @app@+data IsAppend l r where+  IsAppend :: Size app -> IsAppend l (l <+> app)++-- | If @l@ is a sub-context of @r@ then extract out their "contextual+-- difference", i.e., the @app@ such that @r = l <+> app@+diffIsAppend :: Diff l r -> IsAppend l r+diffIsAppend (Diff i) = unsafeCoerce $ IsAppend (Size i)+ data DiffView a b where   NoDiff :: DiffView a a   ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)@@ -240,8 +256,9 @@ 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.+-- | Given a size @n@, an initial value @v0@, and a function @f@, the+-- expression @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)@@ -252,9 +269,10 @@     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.+-- | Given an index @i@, size @n@, a function @f@, value @v@, and a+-- function @f@, the expression @forIndex i n f v@ is equivalent to+-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@+-- otherwise. forIndexRange :: forall ctx r                . Int               -> Size ctx@@ -291,11 +309,11 @@ 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 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 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@@ -309,7 +327,7 @@ type instance Pred ('Succ h) = h  --------------------------------------------------------------------------- BalancedTree+-- * BalancedTree  -- | A balanced tree where all leaves are at the same height. --@@ -459,12 +477,12 @@   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"+bal_zipWithM _ _ _ = error "illegal args to bal_zipWithM" #endif {-# INLINABLE bal_zipWithM #-}  --------------------------------------------------------------------------- BinomialTree+-- * BinomialTree  data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where   Empty :: BinomialTree h f EmptyCtx@@ -605,7 +623,7 @@             -> f y             -> DropResult f (x ::> y) --- | 'bal_drop x y' returns the tree formed 'append x (init 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@@ -686,10 +704,10 @@ {-# INLINABLE tree_zipWithM #-}  --------------------------------------------------------------------------- Assignment+-- * Assignment --- | An assignment is a sequence that maps each index with type 'tp' to--- a value of type 'f tp'.+-- | 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@@ -719,7 +737,7 @@   where r = unsafe_bin_generate (sizeInt n) 0 f {-# NOINLINE generate #-} --- | Generate an assignment+-- | Generate an assignment in an 'Applicative' context generateM :: Applicative m           => Size ctx           -> (forall tp . Index ctx tp -> m (f tp))@@ -813,7 +831,7 @@ 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.+-- | Represent an assignment as either empty or an assignment with one appended. data AssignView f ctx where   AssignEmpty :: AssignView f EmptyCtx   AssignExtend :: Assignment f ctx

@@ -1,6 +1,6 @@ {-| Description      : Type-level lists.-Copyright        : (c) Galois, Inc 2015+Copyright        : (c) Galois, Inc 2015-2019 Maintainer       : Joe Hendrix <jhendrix@galois.com>  This module defines type-level lists used for representing the type of

@@ -1,6 +1,7 @@ {-|-Copyright        : (c) Galois, Inc 2015-Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : type-level proofs involving contexts+Copyright   : (c) Galois, Inc 2015-2019+Maintainer  : Joe Hendrix <jhendrix@galois.com>  This reflects type level proofs involving contexts. -}

@@ -0,0 +1,38 @@+{-|+Description : Decideable equality (i.e. evidence of non-equality) on type families+Copyright   : (c) Galois, Inc 2014-2019+Maintainer  : Langston Barrett <langston@galois.com>++This defines a class @DecidableEq@, which represents decidable equality on a+type family.++This is different from GHC's @TestEquality@ in that it provides evidence+of non-equality. In fact, it is a superclass of @TestEquality@.+-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Safe #-}+module Data.Parameterized.DecidableEq+  ( DecidableEq(..)+  ) where++import Data.Void (Void)+import Data.Type.Equality ((:~:))++-- | Decidable equality.+class DecidableEq f where+  decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)++-- TODO: instances for sums, products of types with decidable equality++-- import Data.Type.Equality ((:~:), TestEquality(..))+-- instance (DecidableEq f) => TestEquality f where+--   testEquality a b =+--     case decEq a b of+--       Left  prf -> Just prf+--       Right _   -> Nothing

@@ -1,13 +1,14 @@ ------------------------------------------------------------------------ -- | -- Module           : Data.Parameterized.HashTable--- Copyright        : (c) Galois, Inc 2014+-- Description      : a hash table for parameterized keys and values+-- Copyright        : (c) Galois, Inc 2014-2019 -- Maintainer       : Joe Hendrix <jhendrix@galois.com> ----- This module provides a ST-based hashtable for parameterized keys and values.+-- 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+-- NOTE: This API makes use of 'unsafeCoerce' to implement the parameterized+-- hashtable abstraction.  This should be type-safe provided that the -- 'TestEquality' instance on the key type is implemented soundly. ------------------------------------------------------------------------ {-# LANGUAGE KindSignatures #-}

@@ -1,10 +1,11 @@ {-|-Copyright        : (c) Galois, Inc 2017-Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : A type-indexed parameterized list+Copyright   : (c) Galois, Inc 2017-2019+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+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@@ -99,7 +100,7 @@   knownRepr = knownRepr :< knownRepr  ----------------------------------------------------------------------------------- Indexed operations+-- * Indexed operations   -- | Represents an index into a type-level list. Used in place of integers to

@@ -1,5 +1,6 @@ {-|-Copyright        : (c) Galois, Inc 2014-2017+Description : Finite maps with parameterized key and value types+Copyright   : (c) Galois, Inc 2014-2019  This module defines finite maps where the key and value types are parameterized by an arbitrary kind.@@ -8,17 +9,14 @@ -} {-# 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 #-}@@ -45,13 +43,21 @@   , fromKeys   , fromKeysM    -- * Filter+  , filter+  , filterWithKey   , filterGt   , filterLt     -- * Folds+  , foldlWithKey+  , foldlWithKey'   , foldrWithKey-    -- * Traversal+  , foldrWithKey'+  , foldMapWithKey+    -- * Traversals   , map+  , mapWithKey   , mapMaybe+  , mapMaybeWithKey   , traverseWithKey   , traverseWithKey_     -- * Complex interface.@@ -65,18 +71,18 @@   , Pair(..)   ) where -import Control.Applicative hiding (empty)-import Control.Lens (Traversal', Lens')-import Control.Monad.Identity-import Data.List (intercalate, foldl')-import Data.Maybe ()-import Data.Kind(Type)+import           Control.Applicative hiding (empty)+import           Control.Lens (Traversal', Lens')+import           Control.Monad.Identity+import           Data.Kind (Type)+import           Data.List (intercalate, foldl')+import           Data.Monoid -import Data.Parameterized.Classes-import Data.Parameterized.Some-import Data.Parameterized.Pair ( Pair(..) )-import Data.Parameterized.TraversableF-import Data.Parameterized.Utils.BinTree+import           Data.Parameterized.Classes+import           Data.Parameterized.Some+import           Data.Parameterized.Pair ( Pair(..) )+import           Data.Parameterized.TraversableF+import           Data.Parameterized.Utils.BinTree   ( MaybeS(..)   , fromMaybeS   , Updated(..)@@ -91,13 +97,13 @@ import qualified Data.Parameterized.Utils.BinTree as Bin  #if MIN_VERSION_base(4,8,0)-import Prelude hiding (lookup, map, traverse, null)+import           Prelude hiding (filter, lookup, map, traverse, null) #else-import Prelude hiding (lookup, map, null)+import           Prelude hiding (filter, lookup, map, null) #endif  --------------------------------------------------------------------------- Pair+-- * Pair  comparePairKeys :: OrdF k => Pair k a -> Pair k a -> Ordering comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y)@@ -106,7 +112,7 @@ ------------------------------------------------------------------------ -- MapF --- | A map from parameterized keys to values with the same paramter type.+-- | A map from parameterized keys to values with the same parameter type. data MapF (k :: v -> Type) (a :: v -> Type) where   Bin :: {-# UNPACK #-}          !Size -- Number of elements in tree.@@ -146,7 +152,7 @@   x == y = size x == size y && toList x == toList y  --------------------------------------------------------------------------- Traversals+-- * Traversals  #ifdef __GLASGOW_HASKELL__ {-# NOINLINE [1] map #-}@@ -165,18 +171,30 @@  #-} #endif ++-- | Apply function to all elements in map.+mapWithKey+  :: (forall tp . ktp tp -> f tp -> g tp)+  -> MapF ktp f+  -> MapF ktp g+mapWithKey _ Tip = Tip+mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r)+ -- | Modify elements in a map map :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g-map _ Tip = Tip-map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r)+map f = mapWithKey (\_ x -> f x) --- | Run partial map over elements.+-- | Map keys and elements and collect `Just` results.+mapMaybeWithKey :: (forall tp . k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k g+mapMaybeWithKey _ Tip = Tip+mapMaybeWithKey f (Bin _ k x l r) =+  case f k x of+    Just y -> Bin.link (Pair k y) (mapMaybeWithKey f l) (mapMaybeWithKey f r)+    Nothing -> Bin.merge (mapMaybeWithKey f l) (mapMaybeWithKey f r)++-- | Map elements and collect `Just` results. mapMaybe :: (forall tp . f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g-mapMaybe _ Tip = Tip-mapMaybe f (Bin _ k x l r) =-  case f x of-    Just y -> Bin.link (Pair k y) (mapMaybe f l) (mapMaybe f r)-    Nothing -> Bin.merge (mapMaybe f l) (mapMaybe f r)+mapMaybe f = mapMaybeWithKey (\_ x -> f x)  -- | Traverse elements in a map traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)@@ -270,13 +288,43 @@ elems :: MapF k a -> [Some a] elems = foldrF (\e l -> Some e : l) [] --- | Perform a fold with the key also provided.+-- | Perform a left fold with the key also provided.+foldlWithKey :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b+foldlWithKey _ z Tip = z+foldlWithKey f z (Bin _ kx x l r) =+  let lz = foldlWithKey f z l+      kz = f lz kx x+   in foldlWithKey f kz r++-- | Perform a strict left fold with the key also provided.+foldlWithKey' :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b+foldlWithKey' _ z Tip = z+foldlWithKey' f z (Bin _ kx x l r) =+  let lz = foldlWithKey f z l+      kz = seq lz $ f lz kx x+   in seq kz $ foldlWithKey f kz r++-- | Perform a right fold with the key also provided. foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b-foldrWithKey f z = go z-  where-    go z' Tip = z'-    go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l+foldrWithKey _ z Tip = z+foldrWithKey f z (Bin _ kx x l r) =+  let rz = foldrWithKey f z r+      kz = f kx x rz+   in foldrWithKey f kz l +-- | Perform a strict right fold with the key also provided.+foldrWithKey' :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b+foldrWithKey' _ z Tip = z+foldrWithKey' f z (Bin _ kx x l r) =+  let rz = foldrWithKey f z r+      kz = seq rz $ f kx x rz+   in seq kz $ foldrWithKey f kz l++-- | Fold the keys and values using the given monoid.+foldMapWithKey :: Monoid m => (forall s . k s -> a s -> m) -> MapF k a -> m+foldMapWithKey _ Tip = mempty+foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r+ showMap :: (forall tp . ktp tp -> String)         -> (forall tp . rtp tp -> String)         -> MapF ktp rtp@@ -287,6 +335,17 @@ ------------------------------------------------------------------------ -- filter +-- | Return entries with values that satisfy a predicate.+filter :: (forall tp . f tp -> Bool) -> MapF k f -> MapF k f+filter f = filterWithKey (\_ v -> f v)++-- | Return key-value pairs that satisfy a predicate.+filterWithKey :: (forall tp . k tp -> f tp -> Bool) -> MapF k f -> MapF k f+filterWithKey _ Tip = Tip+filterWithKey f (Bin _ k x l r)+  | f k x     = Bin.link (Pair k x) (filterWithKey f l) (filterWithKey f r)+  | otherwise = Bin.merge (filterWithKey f l) (filterWithKey f r)+ compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x) @@ -331,9 +390,9 @@  -- | @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+-- It inserts @f new old@ if @m@ already contains an equivalent 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)@@ -356,7 +415,7 @@ ------------------------------------------------------------------------ -- updateAtKey --- | Update request tells when to do with value+-- | 'UpdateRequest' tells what to do with a found value data UpdateRequest v    = -- | Keep the current value.      Keep@@ -443,9 +502,9 @@ 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.+           -- ^ Function for evaluating an input value to store the result in the map.            -> t (Some a)-           -- ^ Set of X86 registers+           -- ^ Set of input values (traversed via folding)            -> m (MapF a v) fromKeysM f = foldM go empty   where go :: MapF a v -> Some a -> m (MapF a v)

@@ -1,21 +1,26 @@ {-|-Copyright        : (c) Galois, Inc 2014-2015-Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : Type level natural number representation at runtime+Copyright   : (c) Galois, Inc 2014-2019+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+each @n@, @NatRepr n@ contains a single value containing the value @n@.  This can be used to help use type-level variables on code with data dependendent types. -The 'TestEquality' instance for 'NatRepr' is implemented using-'unsafeCoerce', as is the `isZeroNat` function. This should be-typesafe because we maintain the invariant that the integer value+The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'+are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This+should be typesafe because we maintain the invariant that the integer value contained in a NatRepr value matches its static type. -} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -24,19 +29,25 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} #if MIN_VERSION_base(4,9,0) {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} #endif+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif module Data.Parameterized.NatRepr   ( NatRepr   , natValue+  , intValue   , knownNat   , withKnownNat   , IsZeroNat(..)   , isZeroNat+  , isZeroOrGT1   , NatComparison(..)   , compareNat   , decNat@@ -49,11 +60,18 @@   , withDivModNat   , natMultiply   , someNat+  , mkNatRepr   , maxNat   , natRec+  , natRecStrong+  , natRecBounded   , natForEach+  , natFromZero   , NatCases(..)   , testNatCases+    -- * Strict order+  , lessThanIrreflexive+  , lessThanAsymmetric     -- * Bitvector utilities   , widthVal   , minUnsigned@@ -66,6 +84,7 @@   , signedClamp     -- * LeqProof   , LeqProof(..)+  , decideLeq   , testLeq   , testStrictLeq   , leqRefl@@ -98,6 +117,7 @@   , withSubMulDistribRight   , mulCancelR   , mul2Plus+  , lemmaMul     -- * Re-exports typelists basics --  , NatK   , type (+)@@ -109,92 +129,35 @@   , Data.Parameterized.Some.Some   ) where -import Data.Bits ((.&.))-import Data.Hashable-import Data.Proxy as Proxy+import Data.Bits ((.&.), bit)+import Data.Data import Data.Type.Equality as Equality-import GHC.TypeLits as TypeLits+import Data.Void as Void+import Numeric.Natural+import GHC.TypeNats as TypeNats import Unsafe.Coerce -import Data.Parameterized.Classes+import Data.Parameterized.NatRepr.Internal import Data.Parameterized.Some -maxInt :: Integer-maxInt = toInteger (maxBound :: Int)----------------------------------------------------------------------------- Nat+maxInt :: Natural+maxInt = fromIntegral (maxBound :: Int) --- | 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)+intValue :: NatRepr n -> Integer+intValue n = toInteger (natValue n)+{-# INLINE intValue #-}  -- | 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 :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))-  NatEQ :: NatComparison x x-  -- First number is greater than second.-  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x--compareNat :: NatRepr m -> NatRepr n -> NatComparison m n-compareNat m n =-  case compare (natValue m) (natValue n) of-    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))-    EQ -> unsafeCoerce  NatEQ-    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))--instance OrdF NatRepr where-  compareF x y =-    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+widthVal (NatRepr i) | i <= maxInt = fromIntegral i+                     | otherwise   = error ("Width is too large: " ++ show i) -{-# DEPRECATED withKnownNat "This function is potentially unsafe and is schedueled to be removed." #-} withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r withKnownNat (NatRepr nVal) v =   case someNatVal nVal of-    Just (SomeNat (Proxy :: Proxy n')) ->-      case unsafeCoerce (Refl :: 0 :~: 0) :: n :~: n' of+    SomeNat (Proxy :: Proxy n') ->+      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of         Refl -> v-    Nothing -> error "withKnownNat: inner value in NatRepr is not a natural"  data IsZeroNat n where   ZeroNat    :: IsZeroNat 0@@ -204,11 +167,35 @@ isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat +-- | Every nat is either zero or >= 1.+isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)+isZeroOrGT1 n =+  case isZeroNat n of+    ZeroNat    -> Left Refl+    NonZeroNat -> Right $+      -- We have n = m + 1 for some m.+      let+        -- | x <= x + 1+        leqSucc:: forall x. LeqProof x (x+1)+        leqSucc = leqAdd2 (LeqProof :: LeqProof x x) (LeqProof :: LeqProof 0 1)+        leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y+        leqPlus fx =+          case (plusComm fx (knownNat @1) :: x + 1 :~: 1 + x)    of { Refl ->+          case (plusMinusCancel (knownNat @1) fx :: 1+x-x :~: 1) of { Refl ->+          case (LeqProof :: LeqProof (x+1) y)                    of { LeqProof ->+          case (LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ->+            leqTrans (LeqProof :: LeqProof 1 (y-x))+                     (leqSub (LeqProof :: LeqProof y y)+                             (leqTrans (leqSucc :: LeqProof x (x+1))+                                       (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)+          }}}}+      in leqPlus (predNat n)+ -- | Decrement a @NatRepr@ decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1) decNat (NatRepr i) = NatRepr (i-1) --- | Get the predicessor of a nat+-- | Get the predecessor of a nat predNat :: NatRepr (n+1) -> NatRepr n predNat (NatRepr i) = NatRepr (i-1) @@ -254,15 +241,15 @@  -- | Return maximum unsigned value for bitvector with given width. maxUnsigned :: NatRepr w -> Integer-maxUnsigned w = 2^(natValue w) - 1+maxUnsigned w = bit (widthVal w) - 1 --- | Return minimum value for bitvector in 2s complement with given width.+-- | Return minimum value for bitvector in two's complement with given width. minSigned :: (1 <= w) => NatRepr w -> Integer-minSigned w = negate (2^(natValue w - 1))+minSigned w = negate (bit (widthVal w - 1)) --- | Return maximum value for bitvector in 2s complement with given width.+-- | Return maximum value for bitvector in two's complement with given width. maxSigned :: (1 <= w) => NatRepr w -> Integer-maxSigned w = 2^(natValue w - 1) - 1+maxSigned w = bit (widthVal w - 1) - 1  -- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@. toUnsigned :: NatRepr w -> Integer -> Integer@@ -272,7 +259,7 @@ -- signed number in two's complement notation and returns that value. toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer toSigned w i0-    | i > maxSigned w = i - 2^(natValue w)+    | i > maxSigned w = i - bit (widthVal w)     | otherwise       = i   where i = i0 .&. maxUnsigned w @@ -295,10 +282,16 @@ ------------------------------------------------------------------------ -- Some NatRepr -someNat :: Integer -> Maybe (Some NatRepr)-someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n)))-          | otherwise = Nothing+-- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@+--   if the given value is negative.+someNat :: Integral a => a -> Maybe (Some NatRepr)+someNat x | x >= 0 = Just . Some . NatRepr $! fromIntegral x+someNat _ = Nothing +-- | Turn a @Natural@ into the corresponding @NatRepr@+mkNatRepr :: Natural -> Some NatRepr+mkNatRepr n = Some (NatRepr n)+ -- | Return the maximum of two nat representations. maxNat :: NatRepr m -> NatRepr n -> Some NatRepr maxNat x y@@ -308,11 +301,11 @@ ------------------------------------------------------------------------ -- Arithmetic --- | Produce evidence that + is commutative.+-- | 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.+-- | Produce evidence that @*@ is commutative. mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m) mulComm _ _ = unsafeCoerce Refl @@ -320,7 +313,7 @@ mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of                Refl -> Refl --- | Cancel an add followed b a subtract+-- | Cancel an add followed by a subtract plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m) @@ -345,8 +338,6 @@   case unsafeCoerce (Refl :: 0 :~: 0) of     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f -- ------------------------------------------------------------------------ -- LeqProof @@ -355,6 +346,13 @@ data LeqProof m n where   LeqProof :: (m <= n) => LeqProof m n +-- | (<=) is a decidable relation on nats.+decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)+decideLeq (NatRepr m) (NatRepr n)+  | m <= n    = Left $ unsafeCoerce (LeqProof :: LeqProof 0 0)+  | otherwise = Right $+      \x -> seq x $ error "Impossible [decidable <= on NatRepr]"+ testStrictLeq :: forall m n                . (m <= n)               => NatRepr m@@ -384,6 +382,31 @@     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0)) {-# NOINLINE testNatCases #-} +-- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.+lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void+lessThanIrreflexive a prf =+  let prf1 :: LeqProof (1 + a - a) (a - a)+      prf1 = leqSub2 prf (LeqProof :: LeqProof a a)+      prf2 :: 1 + a - a :~: 1+      prf2 = plusMinusCancel (knownNat @1) a+      prf3 :: a - a :~: 0+      prf3 = plusMinusCancel (knownNat @0) a+      prf4 :: LeqProof 1 0+      prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }+  in case prf4 of {}++-- | The strict order on the naturals is irreflexive.+lessThanAsymmetric :: forall m f n+                    . LeqProof (n+1) m+                   -> LeqProof (m+1) n+                   -> f n+                   -> Void+lessThanAsymmetric nLTm mLTn n =+  case plusComm n (knownNat @1) :: n + 1 :~: 1 + n of { Refl ->+  case leqAdd (LeqProof :: LeqProof m m) (knownNat @1) :: LeqProof m (m+1) of+    LeqProof -> lessThanIrreflexive n $ leqTrans (leqTrans nLTm LeqProof) mLTn+  }+ -- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@. testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n) testLeq (NatRepr m) (NatRepr n)@@ -395,7 +418,6 @@ leqRefl :: forall f n . f n -> LeqProof n n leqRefl _ = LeqProof - -- | Apply transitivity to LeqProof leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)@@ -509,19 +531,84 @@            -> [a] natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f) +-- | Apply a function to each element in a range starting at zero;+-- return the list of values obtained.+natFromZero :: forall h a+            . NatRepr h+           -> (forall n. (n <= h) => NatRepr n -> a)+           -> [a]+natFromZero = natForEach (knownNat @0)+ -- | Recursor for natural numbeers.-natRec :: forall m f-       .  NatRepr m-       -> f 0+natRec :: forall p f+       .  NatRepr p+       -> f 0 {- ^ base case -}        -> (forall n. NatRepr n -> f n -> f (n + 1))-       -> f m-natRec n f0 ih = go n-  where-    go :: forall n'. NatRepr n' -> f n'-    go n' = case isZeroNat n' of-              ZeroNat    -> f0-              NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')+       -> f p+natRec n base ind =+  case isZeroNat n of+    ZeroNat    -> base+    NonZeroNat -> let n' = predNat n+                  in ind n' (natRec n' base ind) +-- | Strong induction variant of the recursor.+natRecStrong :: forall p f+             .  NatRepr p+             -> f 0 {- ^ base case -}+             -> (forall n.+                  NatRepr n ->+                  (forall m. (m <= n) => NatRepr m -> f m) ->+                  f (n + 1)) {- ^ inductive step -}+             -> f p+natRecStrong p base ind = natRecStrong' base ind p+  where -- We can't use use "flip" or some other basic combinator+        -- because type variables can't be instantiated to contain "forall"s.+        natRecStrong' :: forall p' f'+                      .  f' 0 {- ^ base case -}+                      -> (forall n.+                            NatRepr n ->+                            (forall m. (m <= n) => NatRepr m -> f' m) ->+                            f' (n + 1)) {- ^ inductive step -}+                      -> NatRepr p'+                      -> f' p'+        natRecStrong' base' ind' n =+          case isZeroNat n of+            ZeroNat    -> base'+            NonZeroNat -> ind' (predNat n) (natRecStrong' base' ind')++-- | Bounded recursor for natural numbers.+--+-- If you can prove:+-- - Base case: f 0+-- - Inductive step: if n <= h and (f n) then (f (n + 1))+-- You can conclude: for all n <= h, (f (n + 1)).+natRecBounded :: forall m h f. (m <= h)+              => NatRepr m+              -> NatRepr h+              -> f 0+              -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))+              -> f (m + 1)+natRecBounded m h base indH =+  case isZeroOrGT1 m of+    Left Refl      -> indH (knownNat @0) base+    Right LeqProof ->+      case decideLeq m h of+        Left LeqProof {- :: m <= h -} ->+          let -- Since m is non-zero, it is n + 1 for some n.+              lemma :: LeqProof (m-1) h+              lemma = leqSub (LeqProof :: LeqProof m h) (LeqProof :: LeqProof 1 m)+          in indH m $+            case lemma of { LeqProof ->+            case minusPlusCancel m (knownNat @1) of { Refl ->+              natRecBounded @(m - 1) @h @f (predNat m) h base indH+            }}+        Right f {- :: (m <= h) -> Void -} ->+          absurd $ f (LeqProof :: LeqProof m h)+ mulCancelR ::   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2) mulCancelR _ _ _ = unsafeCoerce Refl++-- | Used in @Vector@+lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)+lemmaMul = unsafeCoerce Refl

@@ -0,0 +1,99 @@+{-|+Copyright        : (c) Galois, Inc 2014-2018+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This internal module exports the 'NatRepr' type and its constructor. It is intended+for use only within parameterized-utils, and is excluded from the module export list.+-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.NatRepr.Internal where++import Data.Data+import Data.Hashable+import GHC.TypeNats+import Numeric.Natural+import Unsafe.Coerce++import Data.Parameterized.Classes+import Data.Parameterized.DecidableEq++------------------------------------------------------------------------+-- 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 :: Natural+                                     -- ^ The underlying natural value of the number.+                                   }+  deriving (Hashable, Data)++type role NatRepr nominal++instance Eq (NatRepr m) where+  _ == _ = True++instance TestEquality NatRepr where+  testEquality (NatRepr m) (NatRepr n)+    | m == n = Just (unsafeCoerce Refl)+    | otherwise = Nothing++instance DecidableEq NatRepr where+  decEq (NatRepr m) (NatRepr n)+    | m == n    = Left $ unsafeCoerce Refl+    | otherwise = Right $+        \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"++compareNat :: NatRepr m -> NatRepr n -> NatComparison m n+compareNat m n =+  case compare (natValue m) (natValue n) of+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))+    EQ -> unsafeCoerce  NatEQ+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))++-- | Result of comparing two numbers.+data NatComparison m n where+  -- First number is less than second.+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))+  NatEQ :: NatComparison x x+  -- First number is greater than second.+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x++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

@@ -1,12 +1,13 @@ {-|-Copyright        : (c) Galois, Inc 2014-2016-Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : Index generator in the ST monad.+Copyright   : (c) Galois, Inc 2014-2019+Maintainer  : Joe Hendrix <jhendrix@galois.com> -This module provides a simple generator of new indexes in the ST monad.+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.+2^64 nonces before repeating.  NOTE: The 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply compare the generated nonce values and then assert to the compiler@@ -16,6 +17,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-}@@ -29,6 +31,7 @@   ( -- * NonceGenerator     NonceGenerator   , freshNonce+  , countNoncesGenerated   , Nonce   , indexValue     -- * Accessing a nonce generator@@ -36,6 +39,7 @@   , newIONonceGenerator   , withIONonceGenerator   , withSTNonceGenerator+    -- * Global nonce generator   , withGlobalSTNonceGenerator   , GlobalNonceGenerator   , globalNonceGenerator@@ -53,7 +57,7 @@ import Data.Parameterized.Classes import Data.Parameterized.Some -#if MIN_VERSION_base(4,9,0)+#if MIN_VERSION_base(4,9,0) && __GLASGOW_HASKELL__ < 805 import Data.Kind #endif @@ -61,55 +65,55 @@ -- -- The first type parameter @m@ is the monad used for generating names, and -- the second parameter @s@ is used for the counter.-data NonceGenerator (m :: * -> *) (s :: *) = NonceGenerator {+data NonceGenerator (m :: * -> *) (s :: *) where+  STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s+  IONG :: !(IORef Word64) -> NonceGenerator IO s+ #if MIN_VERSION_base(4,9,0) -- We have to make the k explicit in GHC 8.0 to avoid a warning.-    freshNonce :: forall k (tp :: k) . m (Nonce s tp)+freshNonce :: forall m s k (tp :: k) . NonceGenerator m s -> m (Nonce s tp) #else-    freshNonce :: forall (tp :: k) . m (Nonce s tp)+freshNonce :: forall m s (tp :: k) . NonceGenerator m s -> m (Nonce s tp) #endif-  }+freshNonce (IONG r) =+  atomicModifyIORef' r $ \n -> (n+1, Nonce n)+freshNonce (STNG r) = do+  i <- readSTRef r+  writeSTRef r $! i+1+  return $ Nonce i+  -- (Weirdly, there's no atomicModifySTRef'.  Yes, only the IO monad+  -- does concurrency, but the ST monad is part of the IO monad via+  -- stToIO, so there's no guarantee that ST code won't be run in+  -- multiple threads.) --- | 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-    }+{-# INLINE freshNonce #-}+  -- Inlining is particularly necessary since there's no @Monad m@+  -- constraint on 'freshNonce', so SPECIALIZE doesn't work on it.  In+  -- this case, though, we get specialization for free from inlining.+  -- For instance, a @NonceGenerator IO s@ must be an @IONG@, so the+  -- simplifier eliminates the STNG branch. --- | Create a new nonce generator in the ST monad.+-- | The number of nonces generated so far by this generator.  Only+-- really useful for profiling.+countNoncesGenerated :: NonceGenerator m s -> m Integer+countNoncesGenerated (IONG r) = toInteger <$> readIORef r+countNoncesGenerated (STNG r) = toInteger <$> readSTRef r++-- | Create a new nonce generator in the 'ST' monad. newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))-newSTNonceGenerator = g <$> newSTRef (toEnum 0)-  where g r = Some $!-          NonceGenerator {-              freshNonce = do-                i <- readSTRef r-                writeSTRef r $! succ i-                return $! Nonce i-            }+newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0) --- | Create a new nonce generator in the ST monad.+-- | Create a new nonce generator in the 'ST' monad. newIONonceGenerator :: IO (Some (NonceGenerator IO))-newIONonceGenerator = g <$> newIORef (toEnum 0)-  where g r = Some $!-          NonceGenerator {-              freshNonce = do-                  i <- readIORef r-                  writeIORef r $! succ i-                  return $! Nonce i-            }+newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0) --- | Run a ST computation with a new nonce generator in the ST monad.+-- | 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.+-- | 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@@ -142,7 +146,7 @@ instance ShowF (Nonce s)  --------------------------------------------------------------------------- GlobalNonceGenerator+-- * GlobalNonceGenerator  data GlobalNonceGenerator @@ -152,7 +156,10 @@  -- | A nonce generator that uses a globally-defined counter. globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator-globalNonceGenerator =-  NonceGenerator-  { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n))-  }+globalNonceGenerator = IONG globalNonceIORef++-- | Create a new counter.+withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r+withGlobalSTNonceGenerator f = runST $ do+  r <- newSTRef (toEnum 0)+  f $! STNG r

@@ -1,6 +1,7 @@ {-|-Copyright        : (c) Galois, Inc 2014-2016-Maintainer       : Eddy Westbrook <westbrook@galois.com>+Description : A typeclass and monad transformers for generating nonces.+Copyright   : (c) Galois, Inc 2014-2019+Maintainer  : Eddy Westbrook <westbrook@galois.com>  This module provides a typeclass and monad transformers for generating nonces.

@@ -1,5 +1,6 @@ {-|-Copyright        : (c) Galois, Inc 2017+nDescription : A 2-tuple with identically parameterized elements+Copyright   : (c) Galois, Inc 2017-2019  This module defines a 2-tuple where both elements are parameterized over the same existentially quantified parameter.

@@ -0,0 +1,501 @@+{-|+Description: Representations of a type-level natural at runtime.+Copyright        : (c) Galois, Inc 2019++This defines a type 'Peano' and 'PeanoRepr' for representing a+type-level natural at runtime. These type-level numbers are defined+inductively instead of using GHC.TypeLits.++As a result, type-level computation defined recursively over these+numbers works more smoothly. (For example, see the type-level+function 'Repeat' below.)++Note: as in "NatRepr", in UNSAFE mode, the runtime representation of+these type-level natural numbers is 'Word64'.++-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++#if MIN_VERSION_base(4,9,0)+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}+#endif+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif+module Data.Parameterized.Peano+   ( -- * Peano+     Peano+     , Z , S++     -- * Basic arithmetic +     , Plus, Minus, Mul,  Max, Min+     , plusP, minusP, mulP, maxP, minP+     , zeroP, succP, predP++     -- * Counting+     , Repeat, CtxSizeP+     , repeatP, ctxSizeP+     +     -- * Comparisons+     , Le, Lt, Gt, Ge+     , leP, ltP, gtP, geP++     -- * Runtime representation+     , KnownPeano+     , PeanoRepr+     , PeanoView(..), peanoView, viewRepr++     -- * 'Some Peano'+     , mkPeanoRepr, peanoValue     +     , somePeano+     , maxPeano+     , minPeano+     , peanoLength++     -- * Properties+     , plusCtxSizeAxiom+     , minusPlusAxiom+     , ltMinusPlusAxiom++     -- * Re-exports+     , TestEquality(..)+     , (:~:)(..)+     , Data.Parameterized.Some.Some++     ) where++import           Data.Parameterized.BoolRepr+import           Data.Parameterized.Classes+import           Data.Parameterized.DecidableEq+import           Data.Parameterized.Some+import           Data.Parameterized.Context++import           Data.Hashable+import           Data.Word++#ifdef UNSAFE_OPS+import           Unsafe.Coerce(unsafeCoerce)+#endif++------------------------------------------------------------------------+-- * Peano arithmetic++-- | Unary representation for natural numbers+data Peano = Z | S Peano+-- | Peano zero+type Z = 'Z+-- | Peano successor+type S = 'S++-- Peano numbers are more about *counting* than arithmetic.+-- They are most useful as iteration arguments and list indices+-- However, for completeness, we define a few standard+-- operations.+++-- | Addition+type family Plus (a :: Peano) (b :: Peano) :: Peano where+  Plus Z     b = b+  Plus (S a) b = S (Plus a b)++-- | Subtraction+type family Minus (a :: Peano) (b :: Peano) :: Peano where+  Minus Z     b     = Z+  Minus (S a) (S b) = Minus a b+  Minus a    Z      = a++-- | Multiplication+type family Mul (a :: Peano) (b :: Peano) :: Peano where+  Mul Z     b = Z+  Mul (S a) b = Plus a (Mul a b)++-- | Less-than-or-equal+type family Le  (a :: Peano) (b :: Peano) :: Bool where+  Le  Z  b        = 'True+  Le  a  Z        = 'False+  Le  (S a) (S b) = Le a b++-- | Less-than+type family Lt  (a :: Peano) (b :: Peano) :: Bool where+  Lt a b = Le (S a) b++-- | Greater-than+type family Gt  (a :: Peano) (b :: Peano) :: Bool where+  Gt a b = Le b a++-- | Greater-than-or-equal+type family Ge  (a :: Peano) (b :: Peano) :: Bool where+  Ge a b = Lt b a++-- | Maximum+type family Max (a :: Peano) (b :: Peano) :: Peano where+  Max Z b = b+  Max a Z = a+  Max (S a) (S b) = S (Max a b)++-- | Minimum+type family Min (a :: Peano) (b :: Peano) :: Peano where+  Min Z b = Z+  Min a Z = Z+  Min (S a) (S b) = S (Min a b)++-- | Apply a constructor 'f' n-times to an argument 's'+type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where+  Repeat Z f s     = s+  Repeat (S m) f s = f (Repeat m f s)++-- | Calculate the size of a context+type family CtxSizeP (ctx :: Ctx k) :: Peano where+  CtxSizeP 'EmptyCtx   = Z+  CtxSizeP (xs '::> x) = S (CtxSizeP xs)++------------------------------------------------------------------------+-- * Run time representation of Peano numbers++#ifdef UNSAFE_OPS+-- | The run time value, stored as an Word64+-- As these are unary numbers, we don't worry about overflow.+newtype PeanoRepr (n :: Peano) =+  PeanoRepr { peanoValue :: Word64 }+-- n is Phantom in the definition, but we don't want to allow coerce+type role PeanoRepr nominal+#else+-- | Runtime value+type PeanoRepr = PeanoView+-- | Conversion+peanoValue :: PeanoRepr n -> Word64+peanoValue ZRepr     = 0+peanoValue (SRepr m) = 1 + peanoValue m+#endif+                                    +-- | When we have optimized the runtime representation,+-- we need to have a "view" that decomposes the representation+-- into the standard form.+data PeanoView (n :: Peano) where+  ZRepr :: PeanoView Z+  SRepr :: PeanoRepr n -> PeanoView (S n)++-- | Test whether a number is Zero or Successor+peanoView :: PeanoRepr n -> PeanoView n+#ifdef UNSAFE_OPS+peanoView (PeanoRepr i) =+  if i == 0+  then unsafeCoerce ZRepr+  else unsafeCoerce (SRepr (PeanoRepr (i-1)))+#else+peanoView = id+#endif++-- | convert the view back to the runtime representation+viewRepr :: PeanoView n -> PeanoRepr n+#ifdef UNSAFE_OPS+viewRepr ZRepr     = PeanoRepr 0+viewRepr (SRepr n) = PeanoRepr (peanoValue n + 1)+#else+viewRepr = id+#endif++----------------------------------------------------------+-- * Class instances++instance Hashable (PeanoRepr n) where+  hashWithSalt i x = hashWithSalt i (peanoValue x)++instance Eq (PeanoRepr m) where+  _ == _ = True++instance TestEquality PeanoRepr where+#ifdef UNSAFE_OPS+  testEquality (PeanoRepr m) (PeanoRepr n)+    | m == n = Just (unsafeCoerce Refl)+    | otherwise = Nothing+#else +  testEquality ZRepr ZRepr = Just Refl+  testEquality (SRepr m1) (SRepr m2)+    | Just Refl <- testEquality m1 m2+    = Just Refl+  testEquality _ _ = Nothing+  +#endif++instance DecidableEq PeanoRepr where+#ifdef UNSAFE_OPS+  decEq (PeanoRepr m) (PeanoRepr n)+    | m == n    = Left $ unsafeCoerce Refl+    | otherwise = Right $+        \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]"+#else+  decEq ZRepr ZRepr = Left Refl+  decEq (SRepr m1) (SRepr m2) =+    case decEq m1 m2 of+      Left Refl -> Left Refl+      Right f   -> Right $ \case Refl -> f Refl+  decEq ZRepr (SRepr _) =+      Right $ \case {}+  decEq (SRepr _) ZRepr =+      Right $ \case {}+#endif++instance OrdF PeanoRepr where+#ifdef UNSAFE_OPS+  compareF (PeanoRepr m) (PeanoRepr n)+    | m < n     = unsafeCoerce LTF+    | m == n    = unsafeCoerce EQF+    | otherwise = unsafeCoerce GTF+#else+  compareF ZRepr      ZRepr      = EQF+  compareF ZRepr      (SRepr _)  = LTF+  compareF (SRepr _)  ZRepr      = GTF+  compareF (SRepr m1) (SRepr m2) =+    case compareF m1 m2 of+       EQF -> EQF+       LTF -> LTF+       GTF -> GTF+#endif++instance PolyEq (PeanoRepr m) (PeanoRepr n) where+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y++-- Display as digits, not in unary+instance Show (PeanoRepr p) where+  show p = show (peanoValue p)++instance ShowF PeanoRepr++instance HashableF PeanoRepr where+  hashWithSaltF = hashWithSalt++----------------------------------------------------------+-- * Implicit runtime Peano numbers++-- | Implicit runtime representation+type KnownPeano = KnownRepr PeanoRepr++instance KnownRepr PeanoRepr Z where+  knownRepr = viewRepr ZRepr+instance (KnownRepr PeanoRepr n) => KnownRepr PeanoRepr (S n) where+  knownRepr = viewRepr (SRepr knownRepr)++----------------------------------------------------------+-- * Operations on runtime numbers+++-- | Zero+zeroP :: PeanoRepr Z+#ifdef UNSAFE_OPS+zeroP = PeanoRepr 0+#else+zeroP = ZRepr+#endif++-- | Successor, Increment+succP :: PeanoRepr n -> PeanoRepr (S n)+#ifdef UNSAFE_OPS+succP (PeanoRepr i) = PeanoRepr (i+1)+#else+succP = SRepr+#endif++-- | Get the predecessor (decrement)+predP :: PeanoRepr (S n) -> PeanoRepr n+#ifdef UNSAFE_OPS+predP (PeanoRepr i) = PeanoRepr (i-1)+#else+predP (SRepr i) = i+#endif++-- | Addition+plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)+#ifdef UNSAFE_OPS+plusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a + b)+#else+plusP (SRepr a) b = SRepr (plusP a b)+#endif++-- | Subtraction+minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)+#ifdef UNSAFE_OPS+minusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a - b)+#else+minusP ZRepr     _b        = ZRepr+minusP (SRepr a) (SRepr b) = minusP a b+minusP a ZRepr             = a+#endif++-- | Multiplication+mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)+#ifdef UNSAFE_OPS+mulP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a * b)+#else+mulP ZRepr     _b = ZRepr+mulP (SRepr a) b  = plusP a (mulP a b)+#endif++-- | Maximum+maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)+#ifdef UNSAFE_OPS+maxP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (max a b)+#else+maxP ZRepr     b         = b+maxP a         ZRepr     = a+maxP (SRepr a) (SRepr b) = SRepr (maxP a b)+#endif++-- | Minimum+minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)+#ifdef UNSAFE_OPS+minP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (min a b)+#else+minP ZRepr     _b        = ZRepr+minP _a        ZRepr     = ZRepr+minP (SRepr a) (SRepr b) = SRepr (minP a b)+#endif++-- | Less-than-or-equal-to+leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)+#ifdef UNSAFE_OPS+leP  (PeanoRepr a) (PeanoRepr b) =+  if a <= b then unsafeCoerce (TrueRepr)+            else unsafeCoerce(FalseRepr)+#else+leP ZRepr      ZRepr    = TrueRepr+leP ZRepr     (SRepr _) = TrueRepr+leP (SRepr _) ZRepr     = FalseRepr+leP (SRepr a) (SRepr b) = leP a b+#endif++-- | Less-than+ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)+ltP a b = leP (succP a) b++-- | Greater-than-or-equal-to+geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)+geP a b = ltP b a++-- | Greater-than+gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)+gtP a b = leP b a+++-- | Apply a constructor 'f' n-times to an argument 's'+repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)+repeatP n f s = case peanoView n of+  ZRepr   -> s+  SRepr m -> f (repeatP m f s)++-- | Calculate the size of a context+ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)+ctxSizeP r = case viewAssign r of+  AssignEmpty -> zeroP+  AssignExtend a _ -> succP (ctxSizeP a)++------------------------------------------------------------------------+-- * Some PeanoRepr++-- | Convert a 'Word64' to a 'PeanoRepr'+mkPeanoRepr :: Word64 -> Some PeanoRepr+#ifdef UNSAFE_OPS+mkPeanoRepr n = Some (PeanoRepr n)+#else+mkPeanoRepr 0 = Some ZRepr+mkPeanoRepr n = case mkPeanoRepr (n - 1) of+                 Some mr -> Some (SRepr mr)+#endif                 ++-- | Turn an @Integral@ value into a 'PeanoRepr'.  Returns @Nothing@+--   if the given value is negative.+somePeano :: Integral a => a -> Maybe (Some PeanoRepr)+somePeano x | x >= 0 = Just . mkPeanoRepr $! fromIntegral x+somePeano _ = Nothing++-- | Return the maximum of two representations.+maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr+maxPeano x y = Some (maxP x y)++-- | Return the minimum of two representations.+minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr+minPeano x y = Some (minP x y)++-- | List length as a Peano number+peanoLength :: [a] -> Some PeanoRepr+peanoLength [] = Some zeroP+peanoLength (_:xs) = case peanoLength xs of+  Some n -> Some (succP n)+++------------------------------------------------------------------------+-- * Properties about Peano numbers+--+-- The safe version of these properties includes a runtime proof of+-- the equality. The unsafe version has no run-time+-- computation. Therefore, in the unsafe version, the "Repr" arguments+-- can be used as proxies (i.e. called using 'undefined') but must be+-- supplied to the safe versions.+++-- | Context size commutes with context append+plusCtxSizeAxiom :: forall t1 t2 f.+  Assignment f t1 -> Assignment f t2 ->+  CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)+#ifdef UNSAFE_OPS+plusCtxSizeAxiom _t1 _t2 = unsafeCoerce Refl+#else+plusCtxSizeAxiom t1 t2 =+  case viewAssign t2 of+    AssignEmpty -> Refl+    AssignExtend t2' _+      | Refl <- plusCtxSizeAxiom t1 t2' -> Refl+#endif++-- | Minus distributes over plus+--+minusPlusAxiom :: forall n t t'.+  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->    +  Minus n (Plus t' t) :~: Minus (Minus n t') t+#ifdef UNSAFE_OPS+minusPlusAxiom _n _t _t' = unsafeCoerce Refl+#else+minusPlusAxiom n t t' = case peanoView t' of+  ZRepr -> Refl+  SRepr t1' -> case peanoView n of+      ZRepr -> Refl+      SRepr n1 -> case minusPlusAxiom n1 t t1' of+        Refl -> Refl+#endif++-- | We can reshuffle minus with less than+--+ltMinusPlusAxiom :: forall n t t'.+  (Lt t (Minus n t') ~ 'True) =>+  PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->+  Lt (Plus t' t) n :~: 'True+#ifdef UNSAFE_OPS+ltMinusPlusAxiom _n _t _t' = unsafeCoerce Refl+#else+ltMinusPlusAxiom n t t' = case peanoView n of+  SRepr m -> case peanoView t' of+     ZRepr -> Refl+     SRepr t1' -> case ltMinusPlusAxiom m t t1' of+        Refl -> Refl+#endif++------------------------------------------------------------------------+--  LocalWords:  PeanoRepr runtime Peano unary

@@ -1,8 +1,9 @@ ------------------------------------------------------------------------ -- | -- Module           : Data.Parameterized.Some--- Copyright        : (c) Galois, Inc 2014+-- Copyright        : (c) Galois, Inc 2014-2019 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>+-- Description : a GADT that hides a type parameter -- -- This module provides 'Some', a GADT that hides a type parameter. ------------------------------------------------------------------------

@@ -1,6 +1,7 @@ {-|-Copyright        : (c) Galois, Inc 2014-2015+Copyright        : (c) Galois, Inc 2014-2019 Maintainer       : Joe Hendrix <jhendrix@galois.com>+Description : a type family for representing a type-level string (AKA symbol) at runtime  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.@@ -16,13 +17,11 @@ {-# 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

@@ -1,8 +1,9 @@ ------------------------------------------------------------------------ -- | -- Module           : Data.Parameterized.TH.GADT--- Copyright        : (c) Galois, Inc 2013-2014+-- Copyright        : (c) Galois, Inc 2013-2019 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>+-- Description : Template Haskell primitives for working with large GADTs -- -- This module declares template Haskell primitives so that it is easier -- to work with GADTs that have many constructors.@@ -79,7 +80,7 @@ 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.+   | DataArg Int   -- ^ Match the i'th argument of the data type we are traversing.    | ConType TypeQ -- ^ Match a ground type.  matchTypePat :: [Type] -> TypePat -> Type -> Q Bool@@ -198,7 +199,9 @@   in mkSimpleEqF dVars bnd pats con  -- | @structuralTypeEquality f@ returns a function with the type:---   forall x y . f x -> f y -> Maybe (x :~: y)+--   @+--     forall x y . f x -> f y -> Maybe (x :~: y)+--   @ structuralTypeEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ structuralTypeEquality tpq pats = do   d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq@@ -214,7 +217,9 @@     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+--   @+--     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@@ -256,12 +261,12 @@       | (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@.+-- and numbered 1 to @n@ to make them useful in conjunction with+-- @-dsuppress-uniques@. newNames ::   String   {- ^ base name                     -} ->   Int      {- ^ quantity                      -} ->-  Q [Name] {- ^ list of names: base1, base2.. -}+  Q [Name] {- ^ list of names: @base1@, @base2@, ... -} newNames base n = traverse (\i -> newName (base ++ show i)) [1..n]  @@ -273,7 +278,7 @@       EQF -> $(r)    |] --- | Compare two variables and use following comparison if they are different.+-- | Compare two variables, returning the third argument if they are equal. -- -- This returns an 'OrdF' instance. joinCompareToOrdF :: Name -> Name -> ExpQ -> ExpQ@@ -284,7 +289,7 @@       EQ -> $(r)    |] -  -- Match expression with given type to variables+-- | Match expression with given type to variables matchOrdArguments :: [Type]                      -- ^ Types bound by data arguments                   -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments@@ -343,7 +348,7 @@        -> 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 f var tp@ applies @f@ to @var@ where @var@ has type @tp@. recurseArg :: (Type -> Q (Maybe ExpQ))            -> ExpQ -- ^ Function to apply            -> ExpQ@@ -361,7 +366,7 @@  -- | @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+traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- ^ Pattern match function                  -> ExpQ -- ^ Function to apply to each argument recursively.                  -> ConstructorInfo -- ^ Constructor to match.                  -> MatchQ -- ^ Match expression that

@@ -1,14 +1,17 @@ ------------------------------------------------------------------------ -- | -- Module           : Data.Parameterized.TraversableF--- Copyright        : (c) Galois, Inc 2014-2015+-- Copyright        : (c) Galois, Inc 2014-2019 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>+-- Description      : Traversing structures having a single parametric type -- -- This module declares classes for working with structures that accept -- a single parametric type parameter. ------------------------------------------------------------------------+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} module Data.Parameterized.TraversableF   ( FunctorF(..)@@ -24,9 +27,12 @@ import Control.Applicative import Control.Monad.Identity import Data.Coerce+import Data.Functor.Compose (Compose(..)) import Data.Monoid import GHC.Exts (build) +import Data.Parameterized.TraversableFC+ -- | A parameterized type that is a functor on all instances. class FunctorF m where   fmapF :: (forall x . f x -> g x) -> m f -> m g@@ -42,7 +48,7 @@ (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) (#.) _f = coerce --- | This is a generalization of the @Foldable@ class to+-- | This is a generalization of the 'Foldable' class to -- structures over parameterized terms. class FoldableF (t :: (k -> *) -> *) where   {-# MINIMAL foldMapF | foldrF #-}@@ -76,11 +82,11 @@   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.+-- | Return 'True' if all values satisfy the 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.+-- | Return 'True' if any values satisfy the predicate. anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool anyF p = getAny #. foldMapF (Any #. p) @@ -112,5 +118,30 @@  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f ()) -> t e -> f ()+traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f () traverseF_ f = foldrF (\e r -> f e *> r) (pure ())++------------------------------------------------------------------------+-- TraversableF (Compose s t)++instance ( FunctorF (s :: (k -> *) -> *)+         , FunctorFC (t :: (l -> *) -> (k -> *))+         ) =>+         FunctorF (Compose s t) where+  fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v++instance ( TraversableF (s :: (k -> *) -> *)+         , TraversableFC (t :: (l -> *) -> (k -> *))+         ) =>+         FoldableF (Compose s t) where+  foldMapF = foldMapFDefault++-- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.+instance ( TraversableF (s :: (k -> *) -> *)+         , TraversableFC (t :: (l -> *) -> (k -> *))+         ) =>+         TraversableF (Compose s t) where+  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>+               (forall (u :: l). f u -> m (g u))+            -> Compose s t f -> m (Compose s t g)+  traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v

@@ -3,6 +3,7 @@ -- Module           : Data.Parameterized.TraversableFC -- Copyright        : (c) Galois, Inc 2014-2015 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>+-- Description      : Traversing structures having a single parametric type followed by a fixed kind. -- -- This module declares classes for working with structures that accept -- a parametric type parameter followed by some fixed kind.@@ -77,12 +78,12 @@ ------------------------------------------------------------------------ -- FoldableF --- | This is a coercision used to avoid overhead associated+-- | This is a coercion used to avoid overhead associated -- with function composition. (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) (#.) _f = coerce --- | This is a generalization of the @Foldable@ class to+-- | This is a generalization of the 'Foldable' class to -- structures over parameterized terms. class FoldableFC (t :: (k -> *) -> l -> *) where   {-# MINIMAL foldMapFC | foldrFC #-}@@ -150,12 +151,12 @@  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m a) -> (forall x. t f x -> m ()) traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ()) {-# INLINE traverseFC_ #-}  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m () forMFC_ v f = traverseFC_ f v {-# INLINE forMFC_ #-}

@@ -1,6 +1,6 @@ {-| Description      : Utilities for balanced binary trees.-Copyright        : (c) Galois, Inc 2014+Copyright        : (c) Galois, Inc 2014-2019 Maintainer       : Joe Hendrix <jhendrix@galois.com> -} {-# LANGUAGE ConstraintKinds #-}@@ -64,7 +64,7 @@ ------------------------------------------------------------------------ -- Updated --- | Updated a contains a value that has been flagged on whether it was+-- | @Updated a@ contains a value that has been flagged on whether it was -- modified by an operation. data Updated a    = Updated   !a@@ -92,7 +92,7 @@ delta = 3 ratio = 2 --- `balanceL p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.+-- | @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.@@ -108,7 +108,7 @@     _ -> bin p l r {-# INLINE balanceL #-} --- `balanceR p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@.+-- | @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.@@ -137,7 +137,7 @@     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@ 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@@ -210,7 +210,7 @@         EQ -> Unchanged (bin x l r) {-# INLINABLE insert #-} --- | 'glue l r' concatenates @l@ and @r@.+-- | @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@@ -247,7 +247,7 @@ -- filter  -- | Returns only entries that are less than predicate with respect to the ordering--- and Nothing if no elements are discared.+-- and Nothing if no elements are discarded. filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c filterGt k t =   case asBin t of@@ -260,7 +260,7 @@ {-# INLINABLE filterGt #-}  --- | @filterLt' k m@ returns submap of @m@ that only contains entries+-- | @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 =@@ -276,8 +276,8 @@ ------------------------------------------------------------------------ -- Union --- Insert a new key and value in the map if it is not already present.--- Used by `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

@@ -0,0 +1,16 @@+{-|+Description: A common location for defining multi-byte value ordering.+Copyright        : (c) Galois, Inc 2019+-}++module Data.Parameterized.Utils.Endian where++-- | Determines the composition of smaller numeric values into larger values.+--+--  BigEndian = most significant values in the lowest index location / first+--  LittleEndian = least significant values in the lowest index location / first+--+--  Value: 0x01020304+--  BigEndian    = [ 0x01, 0x02, 0x03, 0x04 ]+--  LittleEndian = [ 0x04, 0x03, 0x02, 0x01 ]+data Endian = LittleEndian | BigEndian deriving (Eq,Show,Ord)

@@ -0,0 +1,560 @@+{-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}+{-# Language PatternGuards #-}+{-# Language TypeApplications, ScopedTypeVariables #-}+{-# Language Rank2Types, RoleAnnotations #-}+{-# Language CPP #-}+#if __GLASGOW_HASKELL__ >= 805+{-# Language NoStarIsType #-}+#endif+{-|+Copyright        : (c) Galois, Inc 2014-2019++A fixed-size vector of typed elements.++NB: This module contains an orphan instance. It will be included in GHC 8.10,+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.+-}+module Data.Parameterized.Vector+  ( Vector+    -- * Lists+  , fromList+  , toList++    -- * Length+  , length+  , nonEmpty+  , lengthInt++    -- * Indexing+  , elemAt+  , elemAtMaybe+  , elemAtUnsafe++    -- * Update+  , insertAt+  , insertAtMaybe++    -- * Sub sequences+  , uncons+  , slice+  , Data.Parameterized.Vector.take++    -- * Zipping+  , zipWith+  , zipWithM+  , zipWithM_+  , interleave++    -- * Reorder+  , shuffle+  , reverse+  , rotateL+  , rotateR+  , shiftL+  , shiftR++    -- * Construction+  , singleton+  , cons+  , snoc+  , generate+  , generateM++    -- * Splitting and joining+    -- ** General+  , joinWithM+  , joinWith+  , splitWith+  , splitWithA++    -- ** Vectors+  , split+  , join+  , append++  ) where++import qualified Data.Vector as Vector+import Data.Functor.Compose+import Data.Coerce+import Data.Vector.Mutable (MVector)+import qualified Data.Vector.Mutable as MVector+import Control.Monad.ST+import Data.Functor.Identity+import Data.Parameterized.NatRepr+import Data.Parameterized.NatRepr.Internal+import Data.Proxy+import Prelude hiding (length,reverse,zipWith)+import Numeric.Natural++import Data.Parameterized.Utils.Endian++-- | Fixed-size non-empty vectors.+data Vector n a where+  Vector :: (1 <= n) => !(Vector.Vector a) -> Vector n a++type role Vector nominal representational++instance Eq a => Eq (Vector n a) where+  (Vector x) == (Vector y) = x == y++instance Show a => Show (Vector n a) where+  show (Vector x) = show x++-- | Get the elements of the vector as a list, lowest index first.+toList :: Vector n a -> [a]+toList (Vector v) = Vector.toList v+{-# Inline toList #-}++-- NOTE: We are using the raw 'NatRepr' constructor here, which is unsafe.+-- | Length of the vector.+-- @O(1)@+length :: Vector n a -> NatRepr n+length (Vector xs) = NatRepr (fromIntegral (Vector.length xs) :: Natural)+{-# INLINE length #-}++-- | The length of the vector as an "Int".+lengthInt :: Vector n a -> Int+lengthInt (Vector xs) = Vector.length xs+{-# Inline lengthInt #-}++elemAt :: ((i+1) <= n) => NatRepr i -> Vector n a -> a+elemAt n (Vector xs) = xs Vector.! widthVal n++-- | Get the element at the given index.+-- @O(1)@+elemAtMaybe :: Int -> Vector n a -> Maybe a+elemAtMaybe n (Vector xs) = xs Vector.!? n+{-# INLINE elemAt #-}++-- | Get the element at the given index.+-- Raises an exception if the element is not in the vector's domain.+-- @O(1)@+elemAtUnsafe :: Int -> Vector n a -> a+elemAtUnsafe n (Vector xs) = xs Vector.! n+{-# INLINE elemAtUnsafe #-}+++-- | Insert an element at the given index.+-- @O(n)@.+insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a+insertAt n a (Vector xs) = Vector (Vector.unsafeUpd xs [(widthVal n,a)])++-- | Insert an element at the given index.+-- Return 'Nothing' if the element is outside the vector bounds.+-- @O(n)@.+insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)+insertAtMaybe n a (Vector xs)+  | 0 <= n && n < Vector.length xs = Just (Vector (Vector.unsafeUpd xs [(n,a)]))+  | otherwise = Nothing+++-- | Proof that the length of this vector is not 0.+nonEmpty :: Vector n a -> LeqProof 1 n+nonEmpty (Vector _) = LeqProof+{-# Inline nonEmpty #-}+++-- | Remove the first element of the vector, and return the rest, if any.+uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))+uncons v@(Vector xs) = (Vector.head xs, mbTail)+  where+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)+  mbTail = case testStrictLeq (knownNat @1) (length v) of+             Left n2_leq_n ->+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))+                  return (Vector (Vector.tail xs))+             Right Refl    -> Left Refl+{-# Inline uncons #-}+++--------------------------------------------------------------------------------++-- | Make a vector of the given length and element type.+-- Returns "Nothing" if the input list does not have the right number of+-- elements.+-- @O(n)@.+fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)+fromList n xs+  | widthVal n == Vector.length v = Just (Vector v)+  | otherwise                     = Nothing+  where+  v = Vector.fromList xs+{-# INLINE fromList #-}+++-- | Extract a subvector of the given vector.+slice :: (i + w <= n, 1 <= w) =>+            NatRepr i {- ^ Start index -} ->+            NatRepr w {- ^ Width of sub-vector -} ->+            Vector n a -> Vector w a+slice i w (Vector xs) = Vector (Vector.slice (widthVal i) (widthVal w) xs)+{-# INLINE slice #-}++-- | Take the front (lower-indexes) part of the vector.+take :: forall n x a. (1 <= n) => NatRepr n -> Vector (n + x) a -> Vector n a+take | LeqProof <- prf = slice (knownNat @0)+  where+  prf = leqAdd (leqRefl (Proxy @n)) (Proxy @x)++--------------------------------------------------------------------------------++instance Functor (Vector n) where+  fmap f (Vector xs) = Vector (Vector.map f xs)+  {-# Inline fmap #-}++instance Foldable (Vector n) where+  foldMap f (Vector xs) = foldMap f xs++instance Traversable (Vector n) where+  traverse f (Vector xs) = Vector <$> traverse f xs+  {-# Inline traverse #-}++-- | Zip two vectors, potentially changing types.+-- @O(n)@+zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c+zipWith f (Vector xs) (Vector ys) = Vector (Vector.zipWith f xs ys)+{-# Inline zipWith #-}++zipWithM :: Monad m => (a -> b -> m c) ->+                       Vector n a -> Vector n b -> m (Vector n c)+zipWithM f (Vector xs) (Vector ys) = Vector <$> Vector.zipWithM f xs ys+{-# Inline zipWithM #-}++zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()+zipWithM_ f (Vector xs) (Vector ys) = Vector.zipWithM_ f xs ys+{-# Inline zipWithM_ #-}++{- | Interleave two vectors.  The elements of the first vector are+at even indexes in the result, the elements of the second are at odd indexes. -}+interleave ::+  forall n a. (1 <= n) => Vector n a -> Vector n a -> Vector (2 * n) a+interleave (Vector xs) (Vector ys)+  | LeqProof <- leqMulPos (Proxy @2) (Proxy @n) = Vector zs+  where+  len = Vector.length xs + Vector.length ys+  zs  = Vector.generate len (\i -> let v = if even i then xs else ys+                                   in v Vector.! (i `div` 2))+++--------------------------------------------------------------------------------++{- | Move the elements around, as specified by the given function.+  * Note: the reindexing function says where each of the elements+          in the new vector come from.+  * Note: it is OK for the same input element to end up in mulitple places+          in the result.+@O(n)@+-}+shuffle :: (Int -> Int) -> Vector n a -> Vector n a+shuffle f (Vector xs) = Vector ys+  where+  ys = Vector.generate (Vector.length xs) (\i -> xs Vector.! f i)+{-# Inline shuffle #-}++-- | Reverse the vector.+reverse :: forall a n. (1 <= n) => Vector n a -> Vector n a+reverse x = shuffle (\i -> lengthInt x - i - 1) x++-- | Rotate "left".  The first element of the vector is on the "left", so+-- rotate left moves all elemnts toward the corresponding smaller index.+-- Elements that fall off the beginning end up at the end.+rotateL :: Int -> Vector n a -> Vector n a+rotateL !n xs = shuffle rotL xs+  where+  !len   = lengthInt xs+  rotL i = (i + n) `mod` len          -- `len` is known to be >= 1+{-# Inline rotateL #-}++-- | Rotate "right".  The first element of the vector is on the "left", so+-- rotate right moves all elemnts toward the corresponding larger index.+-- Elements that fall off the end, end up at the beginning.+rotateR :: Int -> Vector n a -> Vector n a+rotateR !n xs = shuffle rotR xs+  where+  !len   = lengthInt xs+  rotR i = (i - n) `mod` len        -- `len` is known to be >= 1+{-# Inline rotateR #-}++{- | Move all elements towards smaller indexes.+Elements that fall off the front are ignored.+Empty slots are filled in with the given element.+@O(n)@. -}+shiftL :: Int -> a -> Vector n a -> Vector n a+shiftL !x a (Vector xs) = Vector ys+  where+  !len = Vector.length xs+  ys   = Vector.generate len (\i -> let j = i + x+                                    in if j >= len then a else xs Vector.! j)+{-# Inline shiftL #-}++{- | Move all elements towards the larger indexes.+Elements that "fall" off the end are ignored.+Empty slots are filled in with the given element.+@O(n)@. -}+shiftR :: Int -> a -> Vector n a -> Vector n a+shiftR !x a (Vector xs) = Vector ys+  where+  !len = Vector.length xs+  ys   = Vector.generate len (\i -> let j = i - x+                                    in if j < 0 then a else xs Vector.! j)+{-# Inline shiftR #-}++-------------------------------------------------------------------------------i++-- | Append two vectors. The first one is at lower indexes in the result.+append :: Vector m a -> Vector n a -> Vector (m + n) a+append v1@(Vector xs) v2@(Vector ys) =+  case leqAddPos (length v1) (length v2) of { LeqProof ->+    Vector (xs Vector.++ ys)+  }+{-# Inline append #-}++--------------------------------------------------------------------------------+-- Constructing Vectors++-- | Vector with exactly one element+singleton :: forall a. a -> Vector 1 a+singleton a = Vector (Vector.singleton a)++leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)+leqLen v =+  let leqSucc :: forall f z. f z -> LeqProof z (z + 1)+      leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)+  in leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))++-- | Add an element to the head of a vector+cons :: forall n a. a -> Vector n a -> Vector (n+1) a+cons a v@(Vector x) = case leqLen v of LeqProof -> (Vector (Vector.cons a x))++-- | Add an element to the tail of a vector+snoc :: forall n a. Vector n a -> a -> Vector (n+1) a+snoc v@(Vector x) a = case leqLen v of LeqProof -> (Vector (Vector.snoc x a))++-- | This newtype wraps Vector so that we can curry it in the call to+-- @natRecBounded@. It adds 1 to the length so that the base case is+-- a @Vector@ of non-zero length.+newtype Vector' a n = MkVector' (Vector (n+1) a)++unVector' :: Vector' a n -> Vector (n+1) a+unVector' (MkVector' v) = v++snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)+snoc' v = MkVector' . snoc (unVector' v)++generate' :: forall h a+           . NatRepr h+          -> (forall n. (n <= h) => NatRepr n -> a)+          -> Vector' a h+generate' h gen =+  case isZeroOrGT1 h of+    Left Refl -> base+    Right LeqProof ->+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->+      natRecBounded (decNat h) (decNat h) base step+      }+  where base :: Vector' a 0+        base = MkVector' $ singleton (gen (knownNat @0))+        step :: forall m. (1 <= h, m <= h - 1)+             => NatRepr m -> Vector' a m -> Vector' a (m + 1)+        step m v =+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->+          case (leqAdd2 (LeqProof :: LeqProof m (h-1))+                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->+            snoc' v (gen (incNat m))+          }}++-- | Apply a function to each element in a range starting at zero;+-- return the a vector of values obtained.+-- cf. both @natFromZero@ and @Data.Vector.generate@+generate :: forall h a+          . NatRepr h+         -> (forall n. (n <= h) => NatRepr n -> a)+         -> Vector (h + 1) a+generate h gen = unVector' (generate' h gen)++-- | Since @Vector@ is traversable, we can pretty trivially sequence+-- @natFromZeroVec@ inside a monad.+generateM :: forall m h a. (Monad m)+          => NatRepr h+          -> (forall n. (n <= h) => NatRepr n -> m a)+          -> m (Vector (h + 1) a)+generateM h gen = sequence $ generate h gen++--------------------------------------------------------------------------------++coerceVec :: Coercible a b => Vector n a -> Vector n b+coerceVec = coerce++-- | Monadically join a vector of values, using the given function.+-- This functionality can sometimes be reproduced by creating a newtype+-- wrapper and using @joinWith@, this implementation is provided for+-- convenience.+joinWithM ::+  forall m f n w.+  (1 <= w, Monad m) =>+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))+  {- ^ A function for joining contained elements.  The first argument is+       the size of the accumulated third term, and the second argument+       is the element to join to the accumulated term.  The function+       can use any join strategy desired (prepending/"BigEndian",+       appending/"LittleEndian", etc.). -}+  -> NatRepr w+  -> Vector n (f w)+  -> m (f (n * w))++joinWithM jn w = fmap fst . go+  where+  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))+  go exprs =+    case uncons exprs of+      (a, Left Refl) -> return (a, w)+      (a, Right rest) ->+        case nonEmpty rest                of { LeqProof ->+        case leqMulPos (length rest) w    of { LeqProof ->+        case nonEmpty exprs               of { LeqProof ->+        case lemmaMul w (length exprs)    of { Refl -> do+          -- @siddharthist: This could probably be written applicatively?+          (res, sz) <- go rest+          joined <- jn sz a res+          return (joined, addNat w sz)+        }}}}++-- | Join a vector of vectors, using the given function to combine the+-- sub-vectors.+joinWith ::+  forall f n w.+  (1 <= w) =>+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))+  {- ^ A function for joining contained elements.  The first argument is+       the size of the accumulated third term, and the second argument+       is the element to join to the accumulated term.  The function+       can use any join strategy desired (prepending/"BigEndian",+       appending/"LittleEndian", etc.). -}+  -> NatRepr w+  -> Vector n (f w)+  -> f (n * w)+joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v+{-# Inline joinWith #-}++-- | Split a vector into a vector of vectors.+--+-- The "Endian" parameter determines the ordering of the inner+-- vectors.  If "LittleEndian", then less significant bits go into+-- smaller indexes.  If "BigEndian", then less significant bits go+-- into larger indexes.  See the documentation for 'split' for more+-- details.+splitWith :: forall f w n.+  (1 <= w, 1 <= n) =>+  Endian ->+  (forall i. (i + w <= n * w) =>+             NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)+  {- ^ A function for slicing out a chunk of length @w@, starting at @i@ -} ->+  NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)+splitWith endian select n w val = Vector (Vector.create initializer)+  where+  len          = widthVal n+  start :: Int+  next :: Int -> Int+  (start,next) = case endian of+                   LittleEndian -> (0, succ)+                   BigEndian    -> (len - 1, pred)++  initializer :: forall s. ST s (MVector s (f w))+  initializer =+    do LeqProof <- return (leqMulPos n w)+       LeqProof <- return (leqMulMono n w)++       v <- MVector.new len+       let fill :: Int -> NatRepr i -> ST s ()+           fill loc i =+             let end = addNat i w in+             case testLeq end inLen of+               Just LeqProof ->+                 do MVector.write v loc (select inLen i val)+                    fill (next loc) end+               Nothing -> return ()+++       fill start (knownNat @0)+       return v++  inLen :: NatRepr (n * w)+  inLen = natMultiply n w+{-# Inline splitWith #-}++-- We can sneakily put our functor in the parameter "f" of @splitWith@ using the+-- @Compose@ newtype.+-- | An applicative version of @splitWith@.+splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) =>+  Endian ->+  (forall i. (i + w <= n * w) =>+             NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))+  {- ^ f function for slicing out f chunk of length @w@, starting at @i@ -} ->+  NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))+splitWithA e select n w val = traverse getCompose $+  splitWith @(Compose f g) e select' n w $ Compose (pure val)+  where -- Wrap everything in Compose+        select' :: (forall i. (i + w <= n * w)+                => NatRepr (n * w) -> NatRepr i -> Compose f g (n * w) -> Compose f g w)+        -- Whatever we pass in as "val" is what's passed to select anyway,+        -- so there's no need to examine the argument. Just use "val" directly here.+        select' nw i _ = Compose $ select nw i val++newtype Vec a n = Vec (Vector n a)++vSlice :: (i + w <= l, 1 <= w) =>+  NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w+vSlice w _ i (Vec xs) = Vec (slice i w xs)+{-# Inline vSlice #-}++-- | Append the two bit vectors.  The first argument is+-- at the lower indexes of the resulting vector.+vAppend :: NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)+vAppend _ (Vec xs) (Vec ys) = Vec (append xs ys)+{-# Inline vAppend #-}++-- | Split a vector into a vector of vectors.  The default ordering of+-- the outer result vector is "LittleEndian".+--+-- For example:+-- @+--   let wordsize = knownNat :: NatRepr 3+--       vecsize = knownNat :: NatRepr 12+--       numwords = knownNat :: NatRepr 4  (12 / 3)+--       Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]+--   in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]"+-- @+-- whereas a BigEndian result would have been+-- @+--      [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]+-- @+split :: (1 <= w, 1 <= n) =>+         NatRepr n -- ^ Inner vector size+      -> NatRepr w -- ^ Outer vector size+      -> Vector (n * w) a -- ^ Input vector+      -> Vector n (Vector w a)+split n w xs = coerceVec (splitWith LittleEndian (vSlice w) n w (Vec xs))+{-# Inline split #-}++-- | Join a vector of vectors into a single vector.  Assumes an+-- append/"LittleEndian" join strategy: the order of the inner vectors+-- is preserved in the result vector.+--+-- @+--   let innersize = knownNat :: NatRepr 4+--       Just inner1 = fromList innersize [ 1, 2, 3, 4 ]+--       Just inner2 = fromList innersize [ 5, 6, 7, 8 ]+--       Just inner3 = fromList innersize [ 9, 10, 11, 12 ]+--       outersize = knownNat :: NatRepr 3+--       Just outer = fromList outersize [ inner1, inner2, inner3 ]+--   in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]+-- @+-- a prepend/"BigEndian" join strategy would have the result:+-- @+--   [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]+-- @+join :: (1 <= w) => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a+join w xs = ys+  where Vec ys = joinWith vAppend w (coerceVec xs)+{-# Inline join #-}

@@ -0,0 +1,115 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-|+Copyright        : (c) Galois, Inc 2019++This module declares a class with a single method that can be used to+derive a 'KnownRepr' constraint from an explicit 'Repr' argument.+Clients of this method need only create an empty instance. The default+implementation suffices.++For example, suppose we have defined a 'Repr' type for 'Peano' numbers:++@+data Peano = Z | S Peano++data PeanoRepr p where+    ZRepr :: PeanoRepr Z+    SRepr :: PeanoRepr p -> PeanoRepr (S p)++-- KnownRepr instances+@++Then the instance for this class+@+instance IsRepr PeanoRepr+@++means that functions with 'KnownRepr' constraints can be used after+pattern matching.++@+f :: KnownRepr PeanoRepr a => ...++example :: PeanoRepr n -> ...+example ZRepr = ...+example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...+@+++NOTE: The type 'f' must be a *singleton* type--- i.e.  for a given+type 'a' there should be only one value that inhabits 'f a'. If that+is not the case, this operation can be used to subvert coherence.++Credit: the unsafe implementation of 'withRepr' is taken from the+'withSingI' function in the singletons library+<http://hackage.haskell.org/package/singletons-2.5.1/>.  Packaging+this method in a class here makes it more flexible---we do not have to+define a dedicated 'Sing' type, but can use any convenient singleton+as a 'Repr'.++NOTE: if this module is compiled without UNSAFE_OPS, the default+method will not be available.++-}+module Data.Parameterized.WithRepr(IsRepr(..)) where++import Data.Parameterized.Classes++#ifdef UNSAFE_OPS+import Data.Constraint(Dict(..))+import Unsafe.Coerce(unsafeCoerce)++import Data.Parameterized.NatRepr (NatRepr)+import Data.Parameterized.SymbolRepr (SymbolRepr)+import Data.Parameterized.Peano (PeanoRepr)+import Data.Parameterized.Context(Assignment)+import Data.Parameterized.List(List)+#else+import Data.Parameterized.Peano (PeanoRepr,PeanoView(..))+#endif+import Data.Parameterized.BoolRepr++-- | Turn an explicit Repr value into an implict KnownRepr constraint+class IsRepr (f :: k -> *) where++  withRepr :: f a -> (KnownRepr f a => r) -> r++#ifdef UNSAFE_OPS+  withRepr si r = case reprInstance si of+                     Dict -> r++reprInstance :: forall f a . IsRepr f => f a -> Dict (KnownRepr f a)+reprInstance s = with_repr Dict+   where+     with_repr :: (KnownRepr f a => Dict (KnownRepr f a)) -> Dict (KnownRepr f a)+     with_repr si = unsafeCoerce (Don'tInstantiate si) s++newtype DI f a = Don'tInstantiate (KnownRepr f a => Dict (KnownRepr f a))+#endif+++------------------------------------+-- Instances for types defined in parameterized-utils++#ifdef UNSAFE_OPS+instance IsRepr NatRepr+instance IsRepr SymbolRepr+instance IsRepr PeanoRepr+instance IsRepr BoolRepr+instance IsRepr f => IsRepr (List f)+instance IsRepr f => IsRepr (Assignment f)+#else+-- awful, slow implementation for PeanoRepr+instance IsRepr PeanoRepr where+  withRepr ZRepr f     = f+  withRepr (SRepr m) f = withRepr m f++instance IsRepr BoolRepr where+  withRepr TrueRepr f = f+  withRepr FalseRepr f = f+#endif

@@ -16,6 +16,7 @@ import Data.Parameterized.TraversableFC import Data.Parameterized.Some +import qualified Data.Parameterized.Context as C import qualified Data.Parameterized.Context.Safe as S import qualified Data.Parameterized.Context.Unsafe as U @@ -114,18 +115,13 @@          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+         let x' = x & ixF idx_x %~ twiddle+             y' = y & ixF idx_y %~ twiddle           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')+                 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@@ -138,10 +134,8 @@           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+             updX = x & ixF idx_x .~ x' U.! idx_x+             updY = y & ixF idx_y .~ y' S.! idx_y           return (toListFC Some updX == toListFC Some updY &&                  -- update actually modified the entry@@ -149,10 +143,7 @@                  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'+                 toListFC Some y' == toListFC Some updY                 )     , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do@@ -167,4 +158,11 @@          case testEquality x y of            Just Refl -> return $ vals1 == vals2            Nothing   -> return $ vals1 /= vals2++   , testProperty "append_take" $ \vals1 vals2 -> ioProperty $ do+         Some x <- return $ mkUAsgn vals1+         Some y <- return $ mkUAsgn vals2+         let z = x U.<++> y+         let x' = C.take (U.size x) (U.size y) z+         return $ isJust $ testEquality x x'    ]

@@ -0,0 +1,70 @@+{-# Language DataKinds #-}+{-# Language ExplicitForAll #-}+{-# Language TypeOperators #-}+{-# Language TypeFamilies #-}+{-# Language FlexibleInstances #-}+{-# Language ScopedTypeVariables #-}+{-# Language StandaloneDeriving #-}+{-# Language CPP #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+#if __GLASGOW_HASKELL__ >= 805+{-# Language NoStarIsType #-}+#endif+module Test.Vector+( vecTests+) where++import Test.Tasty+import Test.Tasty.QuickCheck ( Arbitrary(..), testProperty, vectorOf )++import Data.Parameterized.NatRepr+import Data.Parameterized.Vector+import GHC.TypeLits+import Data.Semigroup+import Prelude hiding (reverse)+++instance KnownNat n => Arbitrary (NatRepr n) where+  arbitrary = return knownNat+++instance forall a n. ( 1 <= n+                     , Arbitrary a+                     , KnownNat n) =>+         Arbitrary (Vector n a) where+  arbitrary = do+    n <- arbitrary+    l <- vectorOf (widthVal n) arbitrary+    case fromList n l of+      Just v -> return v+      Nothing -> error ("fromList failure for size " <> show n)+++instance Show (Int -> Ordering) where+  show _ = "unshowable"++-- We use @Ordering@ just because it's simple+vecTests :: IO TestTree+vecTests = testGroup "Vector" <$> return+  [ testProperty "reverse100" $+      \n v -> fromList (n :: NatRepr 100) (v :: [Ordering]) ==+              (reverse <$> (reverse <$> (fromList n v)))+  , testProperty "reverseSingleton" $+      \n v -> fromList (n :: NatRepr 1) (v :: [Ordering]) ==+              (reverse <$> (fromList n v))+  , testProperty "split-join" $+      \n w v -> (v :: Vector (5 * 5) Ordering) ==+                (join (n :: NatRepr 5) $ split n (w :: NatRepr 5) $ v)+  -- @cons@ is the same for vectors or lists+  , testProperty "cons" $+      \n v x -> (cons x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==+                (fromList (incNat n) (x:v))+  -- @snoc@ is like appending to a list+  , testProperty "snoc" $+      \n v x -> (flip snoc x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==+                (fromList (incNat n) (v ++ [x]))+  -- @generate@ is like mapping a function over indices+  , testProperty "generate" $+      \n f -> Just (generate (n :: NatRepr 55) ((f :: Int -> Ordering) . widthVal)) ==+              (fromList (incNat n) (map f [0..widthVal n]) :: Maybe (Vector 56 Ordering))+  ]

@@ -4,6 +4,7 @@  import qualified Test.Context import qualified Test.NatRepr+import qualified Test.Vector  main :: IO () main = tests >>= defaultMainWithIngredients ingrs@@ -19,4 +20,5 @@ tests = testGroup "ParameterizedUtils" <$> sequence   [ Test.Context.contextTests   , Test.NatRepr.natTests+  , Test.Vector.vecTests   ]