diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2013-2016 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal new file mode 100644 --- /dev/null +++ b/parameterized-utils.cabal @@ -0,0 +1,100 @@ +Name: parameterized-utils +Version: 1.0.0 +Author: Galois Inc. +Maintainer: jhendrix@galois.com +Build-type: Simple +Cabal-version: >= 1.9.2 +license: BSD3 +license-file: LICENSE +category: Data Structures, Dependent Types +Synopsis: Classes and data structures for working with data-kind indexed types +Description: + This packages contains collection classes and type representations + used for working with values that have a single parameter. It's + intended for things like expression libraries where one wishes + to leverage the Haskell type-checker to improve type-safety by encoding + the object language type system into data kinds. + +-- Many (but not all, sadly) uses of unsafe operations are +-- controlled by this compile flag. When this flag is set +-- to False, alternate implementations are used to avoid +-- Unsafe.Coerce and Data.Coerce. These alternate implementations +-- impose a significant performance hit. +flag unsafe-operations + Description: Use unsafe operations to improve performance + Default: True + +source-repository head + type: git + location: https://github.com/GaloisInc/parameterized-utils + +library + build-depends: + base >= 4.7 && < 4.11, + th-abstraction >=0.1 && <0.3, + containers, + deepseq, + ghc-prim, + hashable, + hashtables, + lens, + mtl, + template-haskell, + text, + vector + + hs-source-dirs: src + + exposed-modules: + Data.Parameterized + Data.Parameterized.Classes + Data.Parameterized.Context + Data.Parameterized.Context.Safe + Data.Parameterized.Context.Unsafe + Data.Parameterized.Ctx + Data.Parameterized.Ctx.Proofs + Data.Parameterized.HashTable + Data.Parameterized.List + Data.Parameterized.Map + Data.Parameterized.NatRepr + Data.Parameterized.Nonce + Data.Parameterized.Nonce.Transformers + Data.Parameterized.Nonce.Unsafe + Data.Parameterized.Some + Data.Parameterized.SymbolRepr + Data.Parameterized.Pair + Data.Parameterized.TH.GADT + Data.Parameterized.TraversableF + Data.Parameterized.TraversableFC + Data.Parameterized.Utils.BinTree + + ghc-options: -Wall + + if flag(unsafe-operations) + cpp-options: -DUNSAFE_OPS + + +test-suite parameterizedTests + type: exitcode-stdio-1.0 + hs-source-dirs: test + + ghc-options: -Wall + + main-is:UnitTest.hs + other-modules: + Test.Context + Test.NatRepr + + build-depends: + base, + hashable, + hashtables, + ghc-prim, + lens, + mtl, + parameterized-utils, + tasty, + tasty-ant-xml, + tasty-hunit, + tasty-quickcheck >= 0.8.1, + QuickCheck >= 2.7 diff --git a/src/Data/Parameterized.hs b/src/Data/Parameterized.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized.hs @@ -0,0 +1,19 @@ +module Data.Parameterized +( module Data.Parameterized.Classes +, module Data.Parameterized.Ctx +, module Data.Parameterized.TraversableF +, module Data.Parameterized.TraversableFC +, module Data.Parameterized.NatRepr +, module Data.Parameterized.Pair +, module Data.Parameterized.Some +, module Data.Parameterized.SymbolRepr +) where + +import Data.Parameterized.Classes +import Data.Parameterized.Ctx +import Data.Parameterized.TraversableF +import Data.Parameterized.TraversableFC +import Data.Parameterized.NatRepr +import Data.Parameterized.Pair +import Data.Parameterized.Some +import Data.Parameterized.SymbolRepr diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Classes.hs @@ -0,0 +1,280 @@ +{-| +Copyright : (c) Galois, Inc 2014-2015 +Maintainer : Joe Hendrix + +This module declares classes for working with types with the kind +@k -> *@ for any kind @k@. These are generalizations of the +"Data.Functor.Classes" types as they work with any kind @k@, and are +not restricted to '*'. +-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +#if MIN_VERSION_base(4,9,0) +{-# LANGUAGE Safe #-} +#else +{-# LANGUAGE Trustworthy #-} +#endif +module Data.Parameterized.Classes + ( -- * Equality exports + Equality.TestEquality(..) + , (Equality.:~:)(..) + , EqF(..) + , PolyEq(..) + -- * Ordering generalization + , OrdF(..) + , lexCompareF + , OrderingF(..) + , joinOrderingF + , orderingF_refl + , toOrdering + , fromOrdering + -- * Typeclass generalizations + , ShowF(..) + , HashableF(..) + , CoercibleF(..) + -- * Optics generalizations + , IndexF + , IxValueF + , IxedF(..) + , IxedF'(..) + , AtF(..) + -- * KnownRepr + , KnownRepr(..) + -- * Re-exports + , Data.Maybe.isJust + ) where + +import Data.Functor.Const +import Data.Hashable +import Data.Maybe (isJust) +import Data.Proxy +import Data.Type.Equality as Equality + +-- We define these type alias here to avoid importing Control.Lens +-- modules, as this apparently causes problems with the safe Hasekll +-- checking. +type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s +type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s + +------------------------------------------------------------------------ +-- CoercibleF + +-- | An instance of 'CoercibleF' gives a way to coerce between +-- all the types of a family. We generally use this to witness +-- the fact that the type parameter to @rtp@ is a phantom type +-- by giving an implementation in terms of Data.Coerce.coerce. +class CoercibleF (rtp :: k -> *) where + coerceF :: rtp a -> rtp b + +instance CoercibleF (Const x) where + coerceF (Const x) = Const x + +------------------------------------------------------------------------ +-- EqF + +-- | @EqF@ provides a method @eqF@ for testing whether two parameterized +-- types are equal. +-- +-- Unlike 'TestEquality', this only works when the type arguments are +-- the same, and does not provide a proof that the types have the same +-- type when they are equal. Thus this can be implemented over +-- parameterized types that are unable to provide evidence that their +-- type arguments are equal. +class EqF (f :: k -> *) where + eqF :: f a -> f a -> Bool + +instance Eq a => EqF (Const a) where + eqF (Const x) (Const y) = x == y + +------------------------------------------------------------------------ +-- PolyEq + +-- | A polymorphic equality operator that generalizes 'TestEquality'. +class PolyEq u v where + polyEqF :: u -> v -> Maybe (u :~: v) + + polyEq :: u -> v -> Bool + polyEq x y = isJust (polyEqF x y) + +------------------------------------------------------------------------ +-- Ordering + +-- | Ordering over two distinct types with a proof they are equal. +data OrderingF x y where + LTF :: OrderingF x y + EQF :: OrderingF x x + GTF :: OrderingF x y + +orderingF_refl :: OrderingF x y -> Maybe (x :~: y) +orderingF_refl o = + case o of + LTF -> Nothing + EQF -> Just Refl + GTF -> Nothing + +-- | Convert 'OrderingF' to standard ordering. +toOrdering :: OrderingF x y -> Ordering +toOrdering LTF = LT +toOrdering EQF = EQ +toOrdering GTF = GT + +-- | Convert standard ordering to 'OrderingF'. +fromOrdering :: Ordering -> OrderingF x x +fromOrdering LT = LTF +fromOrdering EQ = EQF +fromOrdering GT = GTF + +-- | `joinOrderingF x y` first compares on x, returning an equivalent +-- value if it is not `EQF`. If it is EQF, it returns `y`. +joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k) + . OrderingF a b + -> (a ~ b => OrderingF c d) + -> OrderingF c d +joinOrderingF EQF y = y +joinOrderingF LTF _ = LTF +joinOrderingF GTF _ = GTF + +------------------------------------------------------------------------ +-- OrdF + +-- | A parameterized type that can be compared on distinct instances. +class TestEquality ktp => OrdF (ktp :: k -> *) where + {-# MINIMAL compareF #-} + + -- | compareF compares two keys with different type parameters. + -- Instances must ensure that keys are only equal if the type + -- parameters are equal. + compareF :: ktp x -> ktp y -> OrderingF x y + + leqF :: ktp x -> ktp y -> Bool + leqF x y = + case compareF x y of + LTF -> True + EQF -> True + GTF -> False + + ltF :: ktp x -> ktp y -> Bool + ltF x y = + case compareF x y of + LTF -> True + EQF -> False + GTF -> False + + geqF :: ktp x -> ktp y -> Bool + geqF x y = + case compareF x y of + LTF -> False + EQF -> True + GTF -> True + + gtF :: ktp x -> ktp y -> Bool + gtF x y = + case compareF x y of + LTF -> False + EQF -> False + GTF -> True + +-- | Compare two values, and if they are equal compare the next values, +-- otherwise return LTF or GTF +lexCompareF :: forall (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k) + . OrdF f + => f a + -> f b + -> (a ~ b => OrderingF c d) + -> OrderingF c d +lexCompareF x y = joinOrderingF (compareF x y) + +------------------------------------------------------------------------ +-- ShowF + +-- | A parameterized type that can be shown on all instances. +-- +-- To implement @'ShowF' g@, one should implement an instance @'Show' +-- (g tp)@ for all argument types @tp@, then write an empty instance +-- @instance 'ShowF' g@. +class ShowF (f :: k -> *) where + -- | Provides a show instance for each type. + withShow :: p f -> q tp -> (Show (f tp) => a) -> a + + default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a + withShow _ _ x = x + + showF :: forall tp . f tp -> String + showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x) + + showsF :: forall tp . f tp -> String -> String + showsF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (shows x) + +instance Show x => ShowF (Const x) + +------------------------------------------------------------------------ +-- IxedF + +type family IndexF (m :: *) :: k -> * +type family IxValueF (m :: *) :: k -> * + +-- | Parameterized generalization of the lens @Ixed@ class. +class IxedF k m where + -- | Given an index into a container, build a traversal that visits + -- the given element in the container, if it exists. + ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x) + +-- | Parameterized generalization of the lens @Ixed@ class, +-- but with the guarantee that indexes exist in the container. +class IxedF k m => IxedF' k m where + -- | Given an index into a container, build a lens that + -- points into the given element in the container. + ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x) + +------------------------------------------------------------------------ +-- AtF + +-- | Parameterized generalization of the lens @At@ class. +class IxedF k m => AtF k m where + -- | Given an index into a container, build a lens that points into + -- the given position in the container, whether or not it currently + -- exists. Setting values of @atF@ to a @Just@ value will insert + -- the value if it does not already exist. + atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x)) + +------------------------------------------------------------------------ +-- HashableF + +-- | A default salt used in the implementation of 'hash'. +defaultSalt :: Int +#if WORD_SIZE_IN_BITS == 64 +defaultSalt = 0xdc36d1615b7400a4 +#else +defaultSalt = 0x087fc72c +#endif +{-# INLINE defaultSalt #-} + +-- | A parameterized type that is hashable on all instances. +class HashableF (f :: k -> *) where + hashWithSaltF :: Int -> f tp -> Int + + -- | Hash with default salt. + hashF :: f tp -> Int + hashF = hashWithSaltF defaultSalt + +instance Hashable a => HashableF (Const a) where + hashWithSaltF s (Const x) = hashWithSalt s x + +------------------------------------------------------------------------ +-- KnownRepr + +-- | This class is parameterized by a kind @k@ (typically a data +-- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of +-- singleton types indexed by @k@), and an index parameter @ctx@ of +-- kind @k@. +class KnownRepr (f :: k -> *) (ctx :: k) where + knownRepr :: f ctx diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Context.hs @@ -0,0 +1,274 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.Context +-- Copyright : (c) Galois, Inc 2014-16 +-- Maintainer : Joe Hendrix +-- +-- This module reexports either "Data.Parameterized.Context.Safe" +-- or "Data.Parameterized.Context.Unsafe" depending on the +-- the unsafe-operations compile-time flag. +-- +-- It also defines some utility typeclasses for transforming +-- between curried and uncurried versions of functions over contexts. +------------------------------------------------------------------------ + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE ViewPatterns #-} +module Data.Parameterized.Context + ( +#ifdef UNSAFE_OPS + module Data.Parameterized.Context.Unsafe +#else + module Data.Parameterized.Context.Safe +#endif + , singleton + , toVector + , pattern (:>) + , pattern Empty + -- * Context extension and embedding utilities + , CtxEmbedding(..) + , ExtendContext(..) + , ExtendContext'(..) + , ApplyEmbedding(..) + , ApplyEmbedding'(..) + , identityEmbedding + , extendEmbeddingRightDiff + , extendEmbeddingRight + , extendEmbeddingBoth + , ctxeSize + , ctxeAssignment + + -- * Static indexing and lenses for assignments + , Idx + , getCtx + , setCtx + , field + , natIndex + , natIndexProxy + + -- * Currying and uncurrying for assignments + , CurryAssignment + , CurryAssignmentClass(..) + ) where + +import Prelude hiding (null) + +import GHC.TypeLits (Nat, type (-)) + +import Control.Lens hiding (Index, view, (:>), Empty) +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV + +#ifdef UNSAFE_OPS +import Data.Parameterized.Context.Unsafe +#else +import Data.Parameterized.Context.Safe +#endif + +import Data.Parameterized.TraversableFC + +-- | Create a single element context. +singleton :: f tp -> Assignment f (EmptyCtx ::> tp) +singleton = (empty :>) + +-- | Convert the assignment to a vector. +toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e +toVector a f = V.create $ do + vm <- MV.new (sizeInt (size a)) + forIndexM (size a) $ \i -> do + MV.write vm (indexVal i) (f (a ! i)) + return vm +{-# INLINABLE toVector #-} + +-------------------------------------------------------------------------------- +-- | Context embedding. + +-- This datastructure contains a proof that the first context is +-- embeddable in the second. This is useful if we want to add extend +-- an existing term under a larger context. + +data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) + = CtxEmbedding { _ctxeSize :: Size ctx' + , _ctxeAssignment :: Assignment (Index ctx') ctx + } + +-- Alternate encoding? +-- data CtxEmbedding ctx ctx' where +-- EIdentity :: CtxEmbedding ctx ctx +-- ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) +-- ExtendOne :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) + +ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx') +ctxeSize = lens _ctxeSize (\s v -> s { _ctxeSize = v }) + +ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') + (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2) +ctxeAssignment = lens _ctxeAssignment (\s v -> s { _ctxeAssignment = v }) + +class ApplyEmbedding (f :: Ctx k -> *) where + applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx' + +class ApplyEmbedding' (f :: Ctx k -> k' -> *) where + applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v + +class ExtendContext (f :: Ctx k -> *) where + extendContext :: Diff ctx ctx' -> f ctx -> f ctx' + +class ExtendContext' (f :: Ctx k -> k' -> *) where + extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v + +instance ApplyEmbedding' Index where + applyEmbedding' ctxe idx = (ctxe ^. ctxeAssignment) ! idx + +instance ExtendContext' Index where + extendContext' = extendIndex' + +-- -- This is the inefficient way of doing things. A better way is to +-- -- just have a map between indices. +-- applyEmbedding :: CtxEmbedding ctx ctx' +-- -> Index ctx tp -> Index ctx' tp +-- applyEmbedding ctxe idx = (ctxe ^. ctxeAssignment) ! idx + +identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx +identityEmbedding sz = CtxEmbedding sz (generate sz id) + +-- emptyEmbedding :: CtxEmbedding EmptyCtx EmptyCtx +-- emptyEmbedding = identityEmbedding knownSize + +extendEmbeddingRightDiff :: forall ctx ctx' ctx''. + Diff ctx' ctx'' + -> CtxEmbedding ctx ctx' + -> CtxEmbedding ctx ctx'' +extendEmbeddingRightDiff diff (CtxEmbedding sz' assgn) = CtxEmbedding (extSize sz' diff) updated + where + updated :: Assignment (Index ctx'') ctx + updated = fmapFC (extendIndex' diff) assgn + +extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) +extendEmbeddingRight = extendEmbeddingRightDiff knownDiff + +extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) +extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize)) + where + updated :: CtxEmbedding ctx (ctx' ::> tp) + updated = extendEmbeddingRight ctxe + +-- | Pattern synonym for the empty assignment +pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx +pattern Empty <- (view -> AssignEmpty) + where Empty = empty + +infixl :> + +-- | Pattern synonym for extending an assignment on the right +pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx' +pattern (:>) a v <- (view -> AssignExtend a v) + where a :> v = extend a v + +-- The COMPLETE pragma was not defined until ghc 8.2.* +#if MIN_VERSION_base(4,10,0) +{-# COMPLETE (:>), Empty :: Assignment #-} +#endif + +-------------------------------------------------------------------------------- +-- Static indexing based on type-level naturals + +-- | Get an element from an 'Assignment' by zero-based, left-to-right position. +-- The position must be specified using @TypeApplications@ for the @n@ parameter. +getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r +getCtx asgn = asgn ! natIndex @n + +setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx +setCtx = update (natIndex @n) + +-- | Get a lens for an position in an 'Assignment' by zero-based, left-to-right position. +-- The position must be specified using @TypeApplications@ for the @n@ parameter. +field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r) +field f = adjustM f (natIndex @n) + +-- | Constraint synonym used for getting an 'Index' into a 'Ctx'. +-- @n@ is the zero-based, left-counted index into the list of types +-- @ctx@ which has the type @r@. +type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r) + +-- | Compute an 'Index' value for a particular position in a 'Ctx'. The +-- @TypeApplications@ extension will be needed to disambiguate the choice +-- of the type @n@. +natIndex :: forall n ctx r. Idx n ctx r => Index ctx r +natIndex = natIndex' @_ @(FromLeft ctx n) + +-- | This version of 'natIndex' is suitable for use without the @TypeApplications@ +-- extension. +natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r +natIndexProxy _ = natIndex @n + +------------------------------------------------------------------------ +-- Implementation +------------------------------------------------------------------------ + +-- | Class for computing 'Index' values for positions in a 'Ctx'. +class KnownContext ctx => Idx' (n :: Nat) (ctx :: Ctx k) (r :: k) | n ctx -> r where + natIndex' :: Index ctx r + +-- | Base-case +instance KnownContext xs => Idx' 0 (xs '::> x) x where + natIndex' = lastIndex knownSize + +-- | Inductive-step +instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) => + Idx' n (xs '::> x) r where + + natIndex' = skip (natIndex' @_ @(n-1)) + + +-------------------------------------------------------------------------------- +-- CurryAssignment + +-- | This type family is used to define currying\/uncurrying operations +-- on assignments. It is best understood by seeing its evaluation on +-- several examples: +-- +-- > CurryAssignment EmptyCtx f x = x +-- > CurryAssignment (EmptyCtx ::> a) f x = f a -> x +-- > CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x +-- > CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x +type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where + CurryAssignment EmptyCtx f x = x + CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x) + +-- | This class implements two methods that witness the isomorphism between +-- curried and uncurried functions. +class CurryAssignmentClass (ctx :: Ctx k) where + + -- | Transform a function that accepts an assignment into one with a separate + -- variable for each element of the assignment. + curryAssignment :: (Assignment f ctx -> x) -> CurryAssignment ctx f x + + -- | Transform a curried function into one that accepts an assignment value. + uncurryAssignment :: CurryAssignment ctx f x -> (Assignment f ctx -> x) + +instance CurryAssignmentClass EmptyCtx where + curryAssignment k = k empty + uncurryAssignment k _ = k + +instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where + curryAssignment k = curryAssignment (\asgn a -> k (asgn :> a)) + uncurryAssignment k asgn = + case view asgn of + AssignExtend asgn' x -> uncurryAssignment k asgn' x diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Context/Safe.hs @@ -0,0 +1,961 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.Context.Safe +-- Copyright : (c) Galois, Inc 2014-2015 +-- Maintainer : Joe Hendrix +-- +-- This module defines type contexts as a data-kind that consists of +-- a list of types. Indexes are defined with respect to these contexts. +-- In addition, finite dependent products (Assignments) are defined over +-- type contexts. The elements of an assignment can be accessed using +-- appropriately-typed indexes. +-- +-- This module is intended to export exactly the same API as module +-- "Data.Parameterized.Context.Unsafe", so that they can be used +-- interchangeably. +-- +-- This implementation is entirely typesafe, and provides a proof that +-- the signature implemented by this module is consistent. Contexts, +-- indexes, and assignments are represented naively by linear sequences. +-- +-- Compared to the implementation in "Data.Parameterized.Context.Unsafe", +-- this one suffers from the fact that the operation of extending an +-- the context of an index is /not/ a no-op. We therefore cannot use +-- 'Data.Coerce.coerce' to understand indexes in a new context without +-- actually breaking things. +-------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Data.Parameterized.Context.Safe + ( module Data.Parameterized.Ctx + , Size + , sizeInt + , zeroSize + , incSize + , decSize + , extSize + , addSize + , SizeView(..) + , viewSize + , KnownContext(..) + -- * Diff + , Diff + , noDiff + , extendRight + , KnownDiff(..) + , DiffView(..) + , viewDiff + -- * Indexing + , Index + , indexVal + , base + , skip + , lastIndex + , nextIndex + , extendIndex + , extendIndex' + , forIndex + , intIndex + -- * Assignments + , Assignment + , size + , replicate + , generate + , generateM + , empty + , null + , extend + , update + , adjust + , adjustM + , init + , AssignView(..) + , view + , decompose + , (!) + , (!^) + , toList + , zipWith + , zipWithM + , (<++>) + , traverseWithIndex + ) where + +import qualified Control.Category as Cat +import Control.DeepSeq +import qualified Control.Lens as Lens +import Control.Monad.Identity (Identity(..)) +import Data.Hashable +import Data.List (intercalate) +import Data.Maybe (listToMaybe) +import Data.Type.Equality +import Prelude hiding (init, map, null, replicate, succ, zipWith) + +#if !MIN_VERSION_base(4,8,0) +import Data.Functor +import Control.Applicative (Applicative(..)) +#endif + +import Data.Parameterized.Classes +import Data.Parameterized.Ctx +import Data.Parameterized.Some +import Data.Parameterized.TraversableFC + +------------------------------------------------------------------------ +-- Size + +-- | An indexed singleton type representing the size of a context. +data Size (ctx :: Ctx k) where + SizeZero :: Size 'EmptyCtx + SizeSucc :: Size ctx -> Size (ctx '::> tp) + +-- | Convert a context size to an 'Int'. +sizeInt :: Size ctx -> Int +sizeInt SizeZero = 0 +sizeInt (SizeSucc sz) = (+1) $! sizeInt sz + +-- | The size of an empty context. +zeroSize :: Size 'EmptyCtx +zeroSize = SizeZero + +-- | Increment the size to the next value. +incSize :: Size ctx -> Size (ctx '::> tp) +incSize sz = SizeSucc sz + +decSize :: Size (ctx '::> tp) -> Size ctx +decSize (SizeSucc sz) = sz + +-- | The total size of two concatenated contexts. +addSize :: Size x -> Size y -> Size (x <+> y) +addSize sx SizeZero = sx +addSize sx (SizeSucc sy) = SizeSucc (addSize sx sy) + +-- | Allows interpreting a size. +data SizeView (ctx :: Ctx k) where + ZeroSize :: SizeView 'EmptyCtx + IncSize :: !(Size ctx) -> SizeView (ctx '::> tp) + +-- | View a size as either zero or a smaller size plus one. +viewSize :: Size ctx -> SizeView ctx +viewSize SizeZero = ZeroSize +viewSize (SizeSucc s) = IncSize s + +------------------------------------------------------------------------ +-- Size + +-- | A context that can be determined statically at compiler time. +class KnownContext (ctx :: Ctx k) where + knownSize :: Size ctx + +instance KnownContext 'EmptyCtx where + knownSize = zeroSize + +instance KnownContext ctx => KnownContext (ctx '::> tp) where + knownSize = incSize knownSize + +------------------------------------------------------------------------ +-- Diff + +-- | Difference in number of elements between two contexts. +-- The first context must be a sub-context of the other. +data Diff (l :: Ctx k) (r :: Ctx k) where + DiffHere :: Diff ctx ctx + DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp) + +-- | The identity difference. +noDiff :: Diff l l +noDiff = DiffHere + +-- | Extend the difference to a sub-context of the right side. +extendRight :: Diff l r -> Diff l (r '::> tp) +extendRight diff = DiffThere diff + +composeDiff :: Diff a b -> Diff b c -> Diff a c +composeDiff x DiffHere = x +composeDiff x (DiffThere y) = DiffThere (composeDiff x y) + +instance Cat.Category Diff where + id = DiffHere + d1 . d2 = composeDiff d2 d1 + +-- | Extend the size by a given difference. +extSize :: Size l -> Diff l r -> Size r +extSize sz DiffHere = sz +extSize sz (DiffThere diff) = incSize (extSize sz diff) + +data DiffView a b where + NoDiff :: DiffView a a + ExtendRightDiff :: Diff a b -> DiffView a (b ::> r) + +viewDiff :: Diff a b -> DiffView a b +viewDiff DiffHere = NoDiff +viewDiff (DiffThere diff) = ExtendRightDiff diff + +------------------------------------------------------------------------ +-- KnownDiff + +-- | A difference that can be automatically inferred at compile time. +class KnownDiff (l :: Ctx k) (r :: Ctx k) where + knownDiff :: Diff l r + +instance KnownDiff l l where + knownDiff = noDiff + +instance KnownDiff l r => KnownDiff l (r '::> tp) where + knownDiff = extendRight knownDiff + +------------------------------------------------------------------------ +-- Index + +-- | An index is a reference to a position with a particular type in a +-- context. +data Index (ctx :: Ctx k) (tp :: k) where + IndexHere :: Size ctx -> Index (ctx '::> tp) tp + IndexThere :: Index ctx tp -> Index (ctx '::> tp') tp + +-- | Convert an index to an 'Int', where the index of the left-most type in the context is 0. +indexVal :: Index ctx tp -> Int +indexVal (IndexHere sz) = sizeInt sz +indexVal (IndexThere idx) = indexVal idx + +instance Eq (Index ctx tp) where + idx1 == idx2 = isJust (testEquality idx1 idx2) + +instance TestEquality (Index ctx) where + testEquality (IndexHere _) (IndexHere _) = Just Refl + testEquality (IndexHere _) (IndexThere _) = Nothing + testEquality (IndexThere _) (IndexHere _) = Nothing + testEquality (IndexThere idx1) (IndexThere idx2) = + case testEquality idx1 idx2 of + Just Refl -> Just Refl + Nothing -> Nothing + +instance Ord (Index ctx tp) where + compare i j = toOrdering (compareF i j) + +instance OrdF (Index ctx) where + compareF (IndexHere _) (IndexHere _) = EQF + compareF (IndexThere _) (IndexHere _) = LTF + compareF (IndexHere _) (IndexThere _) = GTF + compareF (IndexThere idx1) (IndexThere idx2) = lexCompareF idx1 idx2 $ EQF + +-- | Index for first element in context. +base :: Index ('EmptyCtx '::> tp) tp +base = IndexHere SizeZero + +-- | Increase context while staying at same index. +skip :: Index ctx x -> Index (ctx '::> y) x +skip idx = IndexThere idx + +-- | Return the index of an element one past the size. +nextIndex :: Size ctx -> Index (ctx '::> tp) tp +nextIndex sz = IndexHere sz + +-- | Return the last index of a element. +lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp +lastIndex (SizeSucc s) = IndexHere s + +{-# INLINE extendIndex #-} +extendIndex :: KnownDiff l r => Index l tp -> Index r tp +extendIndex = extendIndex' knownDiff + +{-# INLINE extendIndex' #-} +extendIndex' :: Diff l r -> Index l tp -> Index r tp +extendIndex' DiffHere idx = idx +extendIndex' (DiffThere diff) idx = IndexThere (extendIndex' diff idx) + +-- | Given a size @n@, an initial value @v0@, and a function @f@, +-- @forIndex n v0 f@ calls @f@ on each index less than @n@ starting +-- from @0@ and @v0@, with the value @v@ obtained from the last call. +forIndex :: forall ctx r + . Size ctx + -> (forall tp . r -> Index ctx tp -> r) + -> r + -> r +forIndex sz_top f = go id sz_top + where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> r -> r + go _ SizeZero = id + go g (SizeSucc sz) = \r -> go (\i -> g (IndexThere i)) sz $ f r (g (IndexHere sz)) + + +indexList :: forall ctx. Size ctx -> [Some (Index ctx)] +indexList sz_top = go id [] sz_top + where go :: (forall tp. Index ctx' tp -> Index ctx tp) + -> [Some (Index ctx)] + -> Size ctx' + -> [Some (Index ctx)] + go _ ls SizeZero = ls + go g ls (SizeSucc sz) = go (\i -> g (IndexThere i)) (Some (g (IndexHere sz)) : ls) sz + +-- | Return index at given integer or nothing if integer is out of bounds. +intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) +intIndex n sz = listToMaybe $ drop n $ indexList sz + +instance Show (Index ctx tp) where + show = show . indexVal + +instance ShowF (Index ctx) + +------------------------------------------------------------------------ +-- Assignment + +-- | An assignment is a sequence that maps each index with type 'tp' to +-- a value of type 'f tp'. +data Assignment (f :: k -> *) (ctx :: Ctx k) where + AssignmentEmpty :: Assignment f EmptyCtx + AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp) + +-- | View an assignment as either empty or an assignment with one appended. +data AssignView (f :: k -> *) (ctx :: Ctx k) where + AssignEmpty :: AssignView f EmptyCtx + AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp) + +view :: forall f ctx . Assignment f ctx -> AssignView f ctx +view AssignmentEmpty = AssignEmpty +view (AssignmentExtend asgn x) = AssignExtend asgn x + +decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp) +decompose (AssignmentExtend a v) = (a,v) + +instance NFData (Assignment f ctx) where + rnf AssignmentEmpty = () + rnf (AssignmentExtend asgn x) = rnf asgn `seq` x `seq` () + +-- | Return number of elements in assignment. +size :: Assignment f ctx -> Size ctx +size AssignmentEmpty = SizeZero +size (AssignmentExtend asgn _) = SizeSucc (size asgn) + +-- | Generate an assignment +generate :: forall ctx f + . Size ctx + -> (forall tp . Index ctx tp -> f tp) + -> Assignment f ctx +generate sz_top f = go id sz_top + where go :: forall ctx' + . (forall tp. Index ctx' tp -> Index ctx tp) + -> Size ctx' + -> Assignment f ctx' + go _ SizeZero = AssignmentEmpty + go g (SizeSucc sz) = + let ctx = go (\i -> g (IndexThere i)) sz + x = f (g (IndexHere sz)) + in AssignmentExtend ctx x + +-- | Generate an assignment +generateM :: forall ctx m f + . Applicative m + => Size ctx + -> (forall tp . Index ctx tp -> m (f tp)) + -> m (Assignment f ctx) +generateM sz_top f = go id sz_top + where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> m (Assignment f ctx') + go _ SizeZero = pure AssignmentEmpty + go g (SizeSucc sz) = + AssignmentExtend <$> (go (\i -> g (IndexThere i)) sz) <*> f (g (IndexHere sz)) + +-- | @replicate n@ make a context with different copies of the same +-- polymorphic value. +replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx +replicate n c = generate n (\_ -> c) + +-- | Create empty indexec vector. +empty :: Assignment f 'EmptyCtx +empty = AssignmentEmpty + +-- | Return true if assignment is empty. +null :: Assignment f ctx -> Bool +null AssignmentEmpty = True +null _ = False + +extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp) +extend asgn e = AssignmentExtend asgn e + +update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx +update idx e asgn = adjust (\_ -> e) idx asgn + +adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx +adjust f idx m = runIdentity (adjustM (Identity . f) idx m) + +adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) +adjustM f = go (\x -> x) + where + go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx') + go g (IndexHere _) (AssignmentExtend asgn x) = AssignmentExtend (map g asgn) <$> f (g x) + go g (IndexThere idx) (AssignmentExtend asgn x) = flip AssignmentExtend (g x) <$> go g idx asgn +#if !MIN_VERSION_base(4,9,0) +-- GHC 7.10.3 and early does not recognize that the above definition is complete, +-- and so need the equation below. GHC 8.0.1 does not require the additional +-- equation. + go _ _ _ = error "SafeTypeContext.adjustM: impossible!" +#endif + +type instance IndexF (Assignment (f :: k -> *) ctx) = Index ctx +type instance IxValueF (Assignment (f :: k -> *) ctx) = f + +instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where + ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x) + ixF idx f = adjustM f idx + +instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where + ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x) + ixF' idx f = adjustM f idx + + +-- | Return assignment with all but the last block. +init :: Assignment f (ctx '::> tp) -> Assignment f ctx +init (AssignmentExtend asgn _) = asgn + +idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp +idxlookup f (AssignmentExtend _ x) (IndexHere _) = f x +idxlookup f (AssignmentExtend ctx _) (IndexThere idx) = idxlookup f ctx idx +idxlookup _ AssignmentEmpty _ = error "Data.Parameterized.Context.Safe.lookup: impossible case" + +-- | Return value of assignment. +(!) :: Assignment f ctx -> Index ctx tp -> f tp +(!) asgn idx = idxlookup id asgn idx + +-- | Return value of assignment, where the index is into an +-- initial sequence of the assignment. +(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp +a !^ i = a ! extendIndex i + +instance TestEquality f => Eq (Assignment f ctx) where + x == y = isJust (testEquality x y) + +testEq :: (forall x y. f x -> f y -> Maybe (x :~: y)) + -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2) +testEq _ AssignmentEmpty AssignmentEmpty = Just Refl +testEq test (AssignmentExtend ctx1 x1) (AssignmentExtend ctx2 x2) = + case testEq test ctx1 ctx2 of + Nothing -> Nothing + Just Refl -> + case test x1 x2 of + Nothing -> Nothing + Just Refl -> Just Refl +testEq _ AssignmentEmpty AssignmentExtend{} = Nothing +testEq _ AssignmentExtend{} AssignmentEmpty = Nothing + +instance TestEqualityFC Assignment where + testEqualityFC = testEq +instance TestEquality f => TestEquality (Assignment f) where + testEquality x y = testEq testEquality x y +instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where + polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y + +compareAsgn :: (forall x y. f x -> f y -> OrderingF x y) + -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2 +compareAsgn _ AssignmentEmpty AssignmentEmpty = EQF +compareAsgn _ AssignmentEmpty _ = GTF +compareAsgn _ _ AssignmentEmpty = LTF +compareAsgn test (AssignmentExtend ctx1 x) (AssignmentExtend ctx2 y) = + case compareAsgn test ctx1 ctx2 of + LTF -> LTF + GTF -> GTF + EQF -> case test x y of + LTF -> LTF + GTF -> GTF + EQF -> EQF + +instance OrdFC Assignment where + compareFC = compareAsgn + +instance OrdF f => OrdF (Assignment f) where + compareF = compareAsgn compareF + +instance OrdF f => Ord (Assignment f ctx) where + compare x y = toOrdering (compareF x y) + + +instance Hashable (Index ctx tp) where + hashWithSalt = hashWithSaltF +instance HashableF (Index ctx) where + hashWithSaltF s i = hashWithSalt s (indexVal i) + +instance HashableF f => HashableF (Assignment f) where + hashWithSaltF = hashWithSalt + +instance HashableF f => Hashable (Assignment f ctx) where + hashWithSalt s AssignmentEmpty = s + hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x + +instance ShowF f => Show (Assignment f ctx) where + show a = "[" ++ intercalate ", " (toList showF a) ++ "]" + +instance ShowF f => ShowF (Assignment f) + +instance FunctorFC Assignment where + fmapFC = fmapFCDefault + +instance FoldableFC Assignment where + foldMapFC = foldMapFCDefault + +instance TraversableFC Assignment where + traverseFC = traverseF + +-- | Map assignment +map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c +map = fmapFC + +traverseF :: forall (f:: k -> *) (g::k -> *) (m:: * -> *) (c::Ctx k) + . Applicative m + => (forall tp . f tp -> m (g tp)) + -> Assignment f c + -> m (Assignment g c) +traverseF _ AssignmentEmpty = pure AssignmentEmpty +traverseF f (AssignmentExtend asgn x) = pure AssignmentExtend <*> traverseF f asgn <*> f x + +-- | Convert assignment to list. +toList :: (forall tp . f tp -> a) + -> Assignment f c + -> [a] +toList = toListFC + +zipWithM :: Applicative m + => (forall tp . f tp -> g tp -> m (h tp)) + -> Assignment f c + -> Assignment g c + -> m (Assignment h c) +zipWithM f x y = go x y + where go AssignmentEmpty AssignmentEmpty = pure AssignmentEmpty + go (AssignmentExtend asgn1 x1) (AssignmentExtend asgn2 x2) = + AssignmentExtend <$> (zipWithM f asgn1 asgn2) <*> (f x1 x2) + +zipWith :: (forall x . f x -> g x -> h x) + -> Assignment f a + -> Assignment g a + -> Assignment h a +zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y +{-# INLINE zipWith #-} + +traverseWithIndex :: Applicative m + => (forall tp . Index ctx tp -> f tp -> m (g tp)) + -> Assignment f ctx + -> m (Assignment g ctx) +traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i) + +(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y) +x <++> AssignmentEmpty = x +x <++> AssignmentExtend y t = AssignmentExtend (x <++> y) t + +------------------------------------------------------------------------ +-- KnownRepr instances + +instance (KnownRepr (Assignment f) ctx, KnownRepr f bt) + => KnownRepr (Assignment f) (ctx ::> bt) where + knownRepr = knownRepr `extend` knownRepr + +instance KnownRepr (Assignment f) EmptyCtx where + knownRepr = empty + +-------------------------------------------------------------------------------------- +-- lookups and update for lenses + +data MyNat where + MyZ :: MyNat + MyS :: MyNat -> MyNat + +type MyZ = 'MyZ +type MyS = 'MyS + +data MyNatRepr :: MyNat -> * where + MyZR :: MyNatRepr MyZ + MySR :: MyNatRepr n -> MyNatRepr (MyS n) + +type family StrongCtxUpdate (n::MyNat) (ctx::Ctx k) (z::k) :: Ctx k where + StrongCtxUpdate n EmptyCtx z = EmptyCtx + StrongCtxUpdate MyZ (ctx::>x) z = ctx ::> z + StrongCtxUpdate (MyS n) (ctx::>x) z = (StrongCtxUpdate n ctx z) ::> x + +type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> *) :: * where + MyNatLookup n EmptyCtx f = () + MyNatLookup MyZ (ctx::>x) f = f x + MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f + +mynat_lookup :: MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f +mynat_lookup _ AssignmentEmpty = () +mynat_lookup MyZR (AssignmentExtend _ x) = x +mynat_lookup (MySR n) (AssignmentExtend asgn _) = mynat_lookup n asgn + +strong_ctx_update :: MyNatRepr n -> Assignment f ctx -> f tp -> Assignment f (StrongCtxUpdate n ctx tp) +strong_ctx_update _ AssignmentEmpty _ = AssignmentEmpty +strong_ctx_update MyZR (AssignmentExtend asgn _) z = AssignmentExtend asgn z +strong_ctx_update (MySR n) (AssignmentExtend asgn x) z = AssignmentExtend (strong_ctx_update n asgn z) x + +------------------------------------------------------------------------ +-- 1 field lens combinators + +type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1) + +instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where + + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 2 field lens combinators + +type Assignment2 f x1 x2 + = Assignment f ('EmptyCtx '::> x1 '::> x2) + +instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + + +------------------------------------------------------------------------ +-- 3 field lens combinators + +type Assignment3 f x1 x2 x3 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3) + +instance Lens.Field1 (Assignment3 f t x2 x3) + (Assignment3 f u x2 x3) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment3 f x1 t x3) + (Assignment3 f x1 u x3) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field3 (Assignment3 f x1 x2 t) + (Assignment3 f x1 x2 u) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 4 field lens combinators + +type Assignment4 f x1 x2 x3 x4 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4) + +instance Lens.Field1 (Assignment4 f t x2 x3 x4) + (Assignment4 f u x2 x3 x4) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment4 f x1 t x3 x4) + (Assignment4 f x1 u x3 x4) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment4 f x1 x2 t x4) + (Assignment4 f x1 x2 u x4) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field4 (Assignment4 f x1 x2 x3 t) + (Assignment4 f x1 x2 x3 u) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + + +------------------------------------------------------------------------ +-- 5 field lens combinators + +type Assignment5 f x1 x2 x3 x4 x5 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5) + +instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5) + (Assignment5 f u x2 x3 x4 x5) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5) + (Assignment5 f x1 u x3 x4 x5) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5) + (Assignment5 f x1 x2 u x4 x5) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5) + (Assignment5 f x1 x2 x3 u x5) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t) + (Assignment5 f x1 x2 x3 x4 u) + (f t) + (f u) where + _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 6 field lens combinators + +type Assignment6 f x1 x2 x3 x4 x5 x6 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6) + +instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6) + (Assignment6 f u x2 x3 x4 x5 x6) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6) + (Assignment6 f x1 u x3 x4 x5 x6) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6) + (Assignment6 f x1 x2 u x4 x5 x6) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6) + (Assignment6 f x1 x2 x3 u x5 x6) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6) + (Assignment6 f x1 x2 x3 x4 u x6) + (f t) + (f u) where + _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t) + (Assignment6 f x1 x2 x3 x4 x5 u) + (f t) + (f u) where + _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 7 field lens combinators + +type Assignment7 f x1 x2 x3 x4 x5 x6 x7 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7) + +instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7) + (Assignment7 f u x2 x3 x4 x5 x6 x7) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7) + (Assignment7 f x1 u x3 x4 x5 x6 x7) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7) + (Assignment7 f x1 x2 u x4 x5 x6 x7) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7) + (Assignment7 f x1 x2 x3 u x5 x6 x7) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7) + (Assignment7 f x1 x2 x3 x4 u x6 x7) + (f t) + (f u) where + _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7) + (Assignment7 f x1 x2 x3 x4 x5 u x7) + (f t) + (f u) where + _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t) + (Assignment7 f x1 x2 x3 x4 x5 x6 u) + (f t) + (f u) where + _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 8 field lens combinators + +type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8) + +instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8) + (Assignment8 f u x2 x3 x4 x5 x6 x7 x8) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + + +instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8) + (Assignment8 f x1 u x3 x4 x5 x6 x7 x8) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8) + (Assignment8 f x1 x2 u x4 x5 x6 x7 x8) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8) + (Assignment8 f x1 x2 x3 u x5 x6 x7 x8) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8) + (Assignment8 f x1 x2 x3 x4 u x6 x7 x8) + (f t) + (f u) where + _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8) + (Assignment8 f x1 x2 x3 x4 x5 u x7 x8) + (f t) + (f u) where + _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8) + (Assignment8 f x1 x2 x3 x4 x5 x6 u x8) + (f t) + (f u) where + _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t) + (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u) + (f t) + (f u) where + _8 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR + +------------------------------------------------------------------------ +-- 9 field lens combinators + +type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9) + + +instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9) + (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _1 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9) + (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _2 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9) + (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _3 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9) + (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9) + (f t) + (f u) where + _4 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9) + (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9) + (f t) + (f u) where + _5 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MySR $ MyZR + +instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9) + (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9) + (f t) + (f u) where + _6 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MySR $ MyZR + +instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9) + (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9) + (f t) + (f u) where + _7 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MySR $ MyZR + +instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9) + (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9) + (f t) + (f u) where + _8 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MySR $ MyZR + +instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t) + (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u) + (f t) + (f u) where + _9 = Lens.lens (mynat_lookup n) (strong_ctx_update n) + where n = MyZR diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Context/Unsafe.hs @@ -0,0 +1,1278 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Parameterized.Context.Unsafe + ( module Data.Parameterized.Ctx + , Size + , sizeInt + , zeroSize + , incSize + , decSize + , extSize + , addSize + , SizeView(..) + , viewSize + , KnownContext(..) + -- * Diff + , Diff + , noDiff + , extendRight + , KnownDiff(..) + , DiffView(..) + , viewDiff + -- * Indexing + , Index + , indexVal + , base + , skip + , lastIndex + , nextIndex + , extendIndex + , extendIndex' + , forIndex + , forIndexRange + , forIndexM + , intIndex + -- ** IndexRange + , IndexRange + , allRange + , indexOfRange + , dropHeadRange + , dropTailRange + -- * Assignments + , Assignment + , size + , replicate + , generate + , generateM + , generateSome + , generateSomeM + , empty + , null + , extend + , update + , adjust + , adjustM + , init + , last + , AssignView(..) + , view + , decompose + , fromList + , (!) + , (!^) + , zipWith + , zipWithM + , (<++>) + , traverseWithIndex + ) where + +import Control.Applicative hiding (empty) +import qualified Control.Category as Cat +import Control.DeepSeq +import Control.Exception +import qualified Control.Lens as Lens +import Control.Monad.Identity (Identity(..)) +import Data.Bits +import Data.Coerce +import Data.Hashable +import Data.List (intercalate) +import Data.Proxy +import Unsafe.Coerce + +import Prelude hiding (init, last, map, null, replicate, succ, zipWith, (++)) +import qualified Prelude + +import Data.Parameterized.Classes +import Data.Parameterized.Ctx +import Data.Parameterized.Ctx.Proofs +import Data.Parameterized.Some +import Data.Parameterized.TraversableFC + +------------------------------------------------------------------------ +-- Size + +-- | Represents the size of a context. +newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int } + +-- | The size of an empty context. +zeroSize :: Size 'EmptyCtx +zeroSize = Size 0 + +-- | Increment the size to the next value. +incSize :: Size ctx -> Size (ctx '::> tp) +incSize (Size n) = Size (n+1) + +decSize :: Size (ctx '::> tp) -> Size ctx +decSize (Size n) = assert (n > 0) (Size (n-1)) + +-- | Allows interpreting a size. +data SizeView (ctx :: Ctx k) where + ZeroSize :: SizeView 'EmptyCtx + IncSize :: !(Size ctx) -> SizeView (ctx '::> tp) + +-- | Project a size +viewSize :: Size ctx -> SizeView ctx +viewSize (Size 0) = unsafeCoerce ZeroSize +viewSize (Size n) = assert (n > 0) (unsafeCoerce (IncSize (Size (n-1)))) + +instance Show (Size ctx) where + show (Size i) = show i + +-- | A context that can be determined statically at compiler time. +class KnownContext (ctx :: Ctx k) where + knownSize :: Size ctx + +instance KnownContext 'EmptyCtx where + knownSize = zeroSize + +instance KnownContext ctx => KnownContext (ctx '::> tp) where + knownSize = incSize knownSize + +------------------------------------------------------------------------ +-- Diff + +-- | Difference in number of elements between two contexts. +-- The first context must be a sub-context of the other. +newtype Diff (l :: Ctx k) (r :: Ctx k) + = Diff { _contextExtSize :: Int } + +-- | The identity difference. +noDiff :: Diff l l +noDiff = Diff 0 + +-- | Extend the difference to a sub-context of the right side. +extendRight :: Diff l r -> Diff l (r '::> tp) +extendRight (Diff i) = Diff (i+1) + +instance Cat.Category Diff where + id = Diff 0 + Diff j . Diff i = Diff (i + j) + +-- | Extend the size by a given difference. +extSize :: Size l -> Diff l r -> Size r +extSize (Size i) (Diff j) = Size (i+j) + +-- | The total size of two concatenated contexts. +addSize :: Size x -> Size y -> Size (x <+> y) +addSize (Size x) (Size y) = Size (x + y) + + +data DiffView a b where + NoDiff :: DiffView a a + ExtendRightDiff :: Diff a b -> DiffView a (b ::> r) + +viewDiff :: Diff a b -> DiffView a b +viewDiff (Diff i) + | i == 0 = unsafeCoerce NoDiff + | otherwise = assert (i > 0) $ unsafeCoerce $ ExtendRightDiff (Diff (i-1)) + +------------------------------------------------------------------------ +-- KnownDiff + +-- | A difference that can be automatically inferred at compile time. +class KnownDiff (l :: Ctx k) (r :: Ctx k) where + knownDiff :: Diff l r + +instance KnownDiff l l where + knownDiff = noDiff + +instance {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where + knownDiff = extendRight knownDiff + +------------------------------------------------------------------------ +-- Index + +-- | An index is a reference to a position with a particular type in a +-- context. +newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int } + +instance Eq (Index ctx tp) where + Index i == Index j = i == j + +instance TestEquality (Index ctx) where + testEquality (Index i) (Index j) + | i == j = Just (unsafeCoerce Refl) + | otherwise = Nothing + +instance Ord (Index ctx tp) where + Index i `compare` Index j = compare i j + +instance OrdF (Index ctx) where + compareF (Index i) (Index j) + | i < j = LTF + | i == j = unsafeCoerce EQF + | otherwise = GTF + +-- | Index for first element in context. +base :: Index ('EmptyCtx '::> tp) tp +base = Index 0 + +-- | Increase context while staying at same index. +skip :: Index ctx x -> Index (ctx '::> y) x +skip (Index i) = Index i + +-- | Return the index of a element one past the size. +nextIndex :: Size ctx -> Index (ctx ::> tp) tp +nextIndex n = Index (sizeInt n) + +-- | Return the last index of a element. +lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp +lastIndex n = Index (sizeInt n - 1) + +{-# INLINE extendIndex #-} +extendIndex :: KnownDiff l r => Index l tp -> Index r tp +extendIndex = extendIndex' knownDiff + +{-# INLINE extendIndex' #-} +extendIndex' :: Diff l r -> Index l tp -> Index r tp +extendIndex' _ = unsafeCoerce + +-- | Given a size 'n', an initial value 'v0', and a function 'f', 'forIndex n v0 f' +-- is equivalent to 'v0' when 'n' is zero, and 'f (forIndex (n-1) v0) (n-1)' otherwise. +forIndex :: forall ctx r + . Size ctx + -> (forall tp . r -> Index ctx tp -> r) + -> r + -> r +forIndex n f r = + case viewSize n of + ZeroSize -> r + IncSize p -> f (forIndex p (coerce f) r) (nextIndex p) + +-- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f', +-- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and +-- 'f i (forIndexRange (i+1) n v0)' otherwise. +forIndexRange :: forall ctx r + . Int + -> Size ctx + -> (forall tp . Index ctx tp -> r -> r) + -> r + -> r +forIndexRange i (Size n) f r + | i >= n = r + | otherwise = f (Index i) (forIndexRange (i+1) (Size n) f r) + +-- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'. +forIndexM :: forall ctx m + . Applicative m + => Size ctx + -> (forall tp . Index ctx tp -> m ()) + -> m () +forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ()) + +-- | Return index at given integer or nothing if integer is out of bounds. +intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) +intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i)) + | otherwise = Nothing + +instance Show (Index ctx tp) where + show = show . indexVal + +instance ShowF (Index ctx) + +------------------------------------------------------------------------ +-- IndexRange + +-- | This represents a contiguous range of indices. +data IndexRange (ctx :: Ctx k) (sub :: Ctx k) + = IndexRange {-# UNPACK #-} !Int + {-# UNPACK #-} !Int + +-- | Return a range containing all indices in the context. +allRange :: Size ctx -> IndexRange ctx ctx +allRange (Size n) = IndexRange 0 n + +-- | `indexOfRange` returns the only index in a range. +indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e +indexOfRange (IndexRange i n) = assert (n == 1) $ Index i + +-- | `dropTailRange r n` drops the last `n` elements in `r`. +dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x +dropTailRange (IndexRange i n) (Size j) = assert (n >= j) $ IndexRange i (n - j) + +-- | `dropHeadRange r n` drops the first `n` elements in `r`. +dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y +dropHeadRange (IndexRange i n) (Size j) = assert (i' >= i && n >= j) $ IndexRange i' (n - j) + where i' = i + j + +------------------------------------------------------------------------ +-- Height + +data Height = Zero | Succ Height + +type family Pred (k :: Height) :: Height +type instance Pred ('Succ h) = h + +------------------------------------------------------------------------ +-- BalancedTree + +-- | A balanced tree where all leaves are at the same height. +-- +-- The first parameter is the height of the tree. +-- The second is the parameterized value. +data BalancedTree h (f :: k -> *) (p :: Ctx k) where + BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x) + BalPair :: !(BalancedTree h f x) + -> !(BalancedTree h f y) + -> BalancedTree ('Succ h) f (x <+> y) + +bal_size :: BalancedTree h f p -> Int +bal_size (BalLeaf _) = 1 +bal_size (BalPair x y) = bal_size x + bal_size y + + +instance TestEqualityFC (BalancedTree h) where + testEqualityFC test (BalLeaf x) (BalLeaf y) = do + Refl <- test x y + return Refl + testEqualityFC test (BalPair x1 x2) (BalPair y1 y2) = do + Refl <- testEqualityFC test x1 y1 + Refl <- testEqualityFC test x2 y2 + return Refl +#if !MIN_VERSION_base(4,9,0) + testEqualityFC _ _ _ = Nothing +#endif + +instance OrdFC (BalancedTree h) where + compareFC test (BalLeaf x) (BalLeaf y) = + joinOrderingF (test x y) $ EQF +#if !MIN_VERSION_base(4,9,0) + compareFC _ BalLeaf{} _ = LTF + compareFC _ _ BalLeaf{} = GTF +#endif + compareFC test (BalPair x1 x2) (BalPair y1 y2) = + joinOrderingF (compareFC test x1 y1) $ + joinOrderingF (compareFC test x2 y2) $ + EQF + +instance HashableF f => HashableF (BalancedTree h f) where + hashWithSaltF s t = + case t of + BalLeaf x -> s `hashWithSaltF` x + BalPair x y -> s `hashWithSaltF` x `hashWithSaltF` y + +fmap_bal :: (forall tp . f tp -> g tp) + -> BalancedTree h f c + -> BalancedTree h g c +fmap_bal = go + where go :: (forall tp . f tp -> g tp) + -> BalancedTree h f c + -> BalancedTree h g c + go f (BalLeaf x) = BalLeaf (f x) + go f (BalPair x y) = BalPair (go f x) (go f y) +{-# INLINABLE fmap_bal #-} + +traverse_bal :: Applicative m + => (forall tp . f tp -> m (g tp)) + -> BalancedTree h f c + -> m (BalancedTree h g c) +traverse_bal = go + where go :: Applicative m + => (forall tp . f tp -> m (g tp)) + -> BalancedTree h f c + -> m (BalancedTree h g c) + go f (BalLeaf x) = BalLeaf <$> f x + go f (BalPair x y) = BalPair <$> go f x <*> go f y +{-# INLINABLE traverse_bal #-} + +instance ShowF f => Show (BalancedTree h f tp) where + show (BalLeaf x) = showF x + show (BalPair x y) = "BalPair " Prelude.++ show x Prelude.++ " " Prelude.++ show y + +instance ShowF f => ShowF (BalancedTree h f) + +unsafe_bal_generate :: forall ctx h f t + . Int -- ^ Height of tree to generate + -> Int -- ^ Starting offset for entries. + -> (forall tp . Index ctx tp -> f tp) + -> BalancedTree h f t +unsafe_bal_generate h o f + | h < 0 = error "unsafe_bal_generate given negative height" + | h == 0 = unsafeCoerce $ BalLeaf (f (Index o)) + | otherwise = + let l = unsafe_bal_generate (h-1) o f + o' = o + 1 `shiftL` (h-1) + u = assert (o + bal_size l == o') $ unsafe_bal_generate (h-1) o' f + in unsafeCoerce $ BalPair l u + +unsafe_bal_generateM :: forall m ctx h f t + . Applicative m + => Int -- ^ Height of tree to generate + -> Int -- ^ Starting offset for entries. + -> (forall x . Index ctx x -> m (f x)) + -> m (BalancedTree h f t) +unsafe_bal_generateM h o f + | h == 0 = unsafeCoerce . BalLeaf <$> f (Index o) + | otherwise = + let o' = o + 1 `shiftL` (h-1) + g lv uv = assert (o' == o + bal_size lv) $ + unsafeCoerce (BalPair lv uv) + in g <$> unsafe_bal_generateM (h-1) o f + <*> unsafe_bal_generateM (h-1) o' f + +-- | Lookup index in tree. +unsafe_bal_index :: BalancedTree h f a -- ^ Tree to lookup. + -> Int -- ^ Index to lookup. + -> Int -- ^ Height of tree + -> f tp +unsafe_bal_index _ j i + | seq j $ seq i $ False = error "bad unsafe_bal_index" +unsafe_bal_index (BalLeaf u) _ i = assert (i == 0) $ unsafeCoerce u +unsafe_bal_index (BalPair x y) j i + | j `testBit` (i-1) = unsafe_bal_index y j $! (i-1) + | otherwise = unsafe_bal_index x j $! (i-1) + +-- | Update value at index in tree. +unsafe_bal_adjust :: Functor m + => (f x -> m (f y)) + -> BalancedTree h f a -- ^ Tree to update + -> Int -- ^ Index to lookup. + -> Int -- ^ Height of tree + -> m (BalancedTree h f b) +unsafe_bal_adjust f (BalLeaf u) _ i = assert (i == 0) $ + (unsafeCoerce . BalLeaf <$> (f (unsafeCoerce u))) +unsafe_bal_adjust f (BalPair x y) j i + | j `testBit` (i-1) = (unsafeCoerce . BalPair x <$> (unsafe_bal_adjust f y j (i-1))) + | otherwise = (unsafeCoerce . flip BalPair y <$> (unsafe_bal_adjust f x j (i-1))) + +{-# SPECIALIZE unsafe_bal_adjust + :: (f x -> Identity (f y)) + -> BalancedTree h f a + -> Int + -> Int + -> Identity (BalancedTree h f b) + #-} + +-- | Zip two balanced trees together. +bal_zipWithM :: Applicative m + => (forall x . f x -> g x -> m (h x)) + -> BalancedTree u f a + -> BalancedTree u g a + -> m (BalancedTree u h a) +bal_zipWithM f (BalLeaf x) (BalLeaf y) = BalLeaf <$> f x y +bal_zipWithM f (BalPair x1 x2) (BalPair y1 y2) = + BalPair <$> bal_zipWithM f x1 (unsafeCoerce y1) + <*> bal_zipWithM f x2 (unsafeCoerce y2) +#if !MIN_VERSION_base(4,9,0) +bal_zipWithM _ _ _ = error "ilegal args to bal_zipWithM" +#endif +{-# INLINABLE bal_zipWithM #-} + +------------------------------------------------------------------------ +-- BinomialTree + +data BinomialTree (h::Height) (f :: k -> *) :: Ctx k -> * where + Empty :: BinomialTree h f EmptyCtx + + -- Contains size of the subtree, subtree, then element. + PlusOne :: !Int + -> !(BinomialTree ('Succ h) f x) + -> !(BalancedTree h f y) + -> BinomialTree h f (x <+> y) + + -- Contains size of the subtree, subtree, then element. + PlusZero :: !Int + -> !(BinomialTree ('Succ h) f x) + -> BinomialTree h f x + +tsize :: BinomialTree h f a -> Int +tsize Empty = 0 +tsize (PlusOne s _ _) = 2*s+1 +tsize (PlusZero s _) = 2*s + +t_cnt_size :: BinomialTree h f a -> Int +t_cnt_size Empty = 0 +t_cnt_size (PlusOne _ l r) = t_cnt_size l + bal_size r +t_cnt_size (PlusZero _ l) = t_cnt_size l + +-- | Concatenate a binomial tree and a balanced tree. +append :: BinomialTree h f x + -> BalancedTree h f y + -> BinomialTree h f (x <+> y) +append Empty y = PlusOne 0 Empty y +append (PlusOne _ t x) y = + case assoc t x y of + Refl -> + let t' = append t (BalPair x y) + in PlusZero (tsize t') t' +append (PlusZero s t) x = PlusOne s t x + +instance TestEqualityFC (BinomialTree h) where + testEqualityFC _ Empty Empty = return Refl + testEqualityFC test (PlusZero _ x1) (PlusZero _ y1) = do + Refl <- testEqualityFC test x1 y1 + return Refl + testEqualityFC test (PlusOne _ x1 x2) (PlusOne _ y1 y2) = do + Refl <- testEqualityFC test x1 y1 + Refl <- testEqualityFC test x2 y2 + return Refl + testEqualityFC _ _ _ = Nothing + +instance OrdFC (BinomialTree h) where + compareFC _ Empty Empty = EQF + compareFC _ Empty _ = LTF + compareFC _ _ Empty = GTF + + compareFC test (PlusZero _ x1) (PlusZero _ y1) = + joinOrderingF (compareFC test x1 y1) $ EQF + compareFC _ PlusZero{} _ = LTF + compareFC _ _ PlusZero{} = GTF + + compareFC test (PlusOne _ x1 x2) (PlusOne _ y1 y2) = + joinOrderingF (compareFC test x1 y1) $ + joinOrderingF (compareFC test x2 y2) $ + EQF + +instance HashableF f => HashableF (BinomialTree h f) where + hashWithSaltF s t = + case t of + Empty -> s + PlusZero _ x -> s `hashWithSaltF` x + PlusOne _ x y -> s `hashWithSaltF` x `hashWithSaltF` y + +-- | Map over a binary tree. +fmap_bin :: (forall tp . f tp -> g tp) + -> BinomialTree h f c + -> BinomialTree h g c +fmap_bin _ Empty = Empty +fmap_bin f (PlusOne s t x) = PlusOne s (fmap_bin f t) (fmap_bal f x) +fmap_bin f (PlusZero s t) = PlusZero s (fmap_bin f t) +{-# INLINABLE fmap_bin #-} + +traverse_bin :: Applicative m + => (forall tp . f tp -> m (g tp)) + -> BinomialTree h f c + -> m (BinomialTree h g c) +traverse_bin _ Empty = pure Empty +traverse_bin f (PlusOne s t x) = PlusOne s <$> traverse_bin f t <*> traverse_bal f x +traverse_bin f (PlusZero s t) = PlusZero s <$> traverse_bin f t +{-# INLINABLE traverse_bin #-} + +unsafe_bin_generate :: forall h f ctx t + . Int -- ^ Size of tree to generate + -> Int -- ^ Height of each element. + -> (forall x . Index ctx x -> f x) + -> BinomialTree h f t +unsafe_bin_generate sz h f + | sz == 0 = unsafeCoerce Empty + | sz `testBit` 0 = + let s = sz `shiftR` 1 + t = unsafe_bin_generate s (h+1) f + o = s * 2^(h+1) + u = assert (o == t_cnt_size t) $ unsafe_bal_generate h o f + in unsafeCoerce (PlusOne s t u) + | otherwise = + let s = sz `shiftR` 1 + t = unsafe_bin_generate (sz `shiftR` 1) (h+1) f + r :: BinomialTree h f t + r = PlusZero s t + in r + +unsafe_bin_generateM :: forall m h f ctx t + . Applicative m + => Int -- ^ Size of tree to generate + -> Int -- ^ Height of each element. + -> (forall x . Index ctx x -> m (f x)) + -> m (BinomialTree h f t) +unsafe_bin_generateM sz h f + | sz == 0 = pure (unsafeCoerce Empty) + | sz `testBit` 0 = + let s = sz `shiftR` 1 + t = unsafe_bin_generateM s (h+1) f + -- Next offset + o = s * 2^(h+1) + u = unsafe_bal_generateM h o f + r = unsafeCoerce (PlusOne s) <$> t <*> u + in r + | otherwise = + let s = sz `shiftR` 1 + t = unsafe_bin_generateM s (h+1) f + r :: m (BinomialTree h f t) + r = PlusZero s <$> t + in r + +------------------------------------------------------------------------ +-- Dropping + +type family InitCtx (x :: Ctx k) :: Ctx k +type instance InitCtx (x ::> y) = x + +type family LastCtx (x :: Ctx k) :: k +type instance LastCtx (x ::> y) = y + +-- +data DropResult f (ctx :: Ctx k) where + DropEmpty :: DropResult f EmptyCtx + DropExt :: BinomialTree 'Zero f (InitCtx ctx) + -> f (LastCtx ctx) + -> DropResult f ctx + +-- | 'bal_drop x y' returns the tree formed 'append x (init y)' +bal_drop :: forall h f x y + . BinomialTree h f x + -- ^ Bina + -> BalancedTree h f y + -> DropResult f (x <+> y) +bal_drop t (BalLeaf e) = DropExt t e +bal_drop t (BalPair x y) = + unsafeCoerce (bal_drop (PlusOne (tsize t) (unsafeCoerce t) x) y) + +bin_drop :: forall h f ctx + . BinomialTree h f ctx + -> DropResult f ctx +bin_drop Empty = DropEmpty +bin_drop (PlusZero _ u) = bin_drop u +bin_drop (PlusOne s t u) = + let m = case t of + Empty -> Empty + _ -> PlusZero s t + in bal_drop m u + +------------------------------------------------------------------------ +-- Indexing + +-- | Lookup value in tree. +unsafe_bin_index :: BinomialTree h f a -- ^ Tree to lookup in. + -> Int + -> Int -- ^ Size of tree + -> f u +unsafe_bin_index _ _ i + | seq i False = error "bad unsafe_bin_index" +unsafe_bin_index Empty _ _ = error "unsafe_bin_index reached end of list" +unsafe_bin_index (PlusOne sz t u) j i + | sz == j `shiftR` (1+i) = unsafe_bal_index u j i + | otherwise = unsafe_bin_index t j $! (1+i) +unsafe_bin_index (PlusZero sz t) j i + | sz == j `shiftR` (1+i) = error "unsafe_bin_index stopped at PlusZero" + | otherwise = unsafe_bin_index t j $! (1+i) + +-- | Lookup value in tree. +unsafe_bin_adjust :: forall m h f x y a b + . Functor m + => (f x -> m (f y)) + -> BinomialTree h f a -- ^ Tree to lookup in. + -> Int + -> Int -- ^ Size of tree + -> m (BinomialTree h f b) +unsafe_bin_adjust _ Empty _ _ = error "unsafe_bin_adjust reached end of list" +unsafe_bin_adjust f (PlusOne sz t u) j i + | sz == j `shiftR` (1+i) = + unsafeCoerce . PlusOne sz t <$> (unsafe_bal_adjust f u j i) + | otherwise = + unsafeCoerce . flip (PlusOne sz) u <$> (unsafe_bin_adjust f t j (i+1)) +unsafe_bin_adjust f (PlusZero sz t) j i + | sz == j `shiftR` (1+i) = error "unsafe_bin_adjust stopped at PlusZero" + | otherwise = PlusZero sz <$> (unsafe_bin_adjust f t j (i+1)) + + +{-# SPECIALIZE unsafe_bin_adjust + :: (f x -> Identity (f y)) + -> BinomialTree h f a + -> Int + -> Int + -> Identity (BinomialTree h f b) + #-} + +tree_zipWithM :: Applicative m + => (forall x . f x -> g x -> m (h x)) + -> BinomialTree u f a + -> BinomialTree u g a + -> m (BinomialTree u h a) +tree_zipWithM _ Empty Empty = pure Empty +tree_zipWithM f (PlusOne s x1 x2) (PlusOne _ y1 y2) = + PlusOne s <$> tree_zipWithM f x1 (unsafeCoerce y1) + <*> bal_zipWithM f x2 (unsafeCoerce y2) +tree_zipWithM f (PlusZero s x1) (PlusZero _ y1) = + PlusZero s <$> tree_zipWithM f x1 y1 +tree_zipWithM _ _ _ = error "ilegal args to tree_zipWithM" +{-# INLINABLE tree_zipWithM #-} + +------------------------------------------------------------------------ +-- Assignment + +type role Assignment representational nominal + +-- | An assignment is a sequence that maps each index with type 'tp' to +-- a value of type 'f tp'. +newtype Assignment (f :: k -> *) (ctx :: Ctx k) + = Assignment (BinomialTree 'Zero f ctx) + +instance NFData (Assignment f ctx) where + rnf a = seq a () + +-- | Return number of elements in assignment. +size :: Assignment f ctx -> Size ctx +size (Assignment t) = Size (tsize t) + +-- | Generate an assignment with some context type that is not known. +generateSome :: forall f + . Int + -> (Int -> Some f) + -> Some (Assignment f) +generateSome n f = go n + where go :: Int -> Some (Assignment f) + go 0 = Some empty + go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1)) + +-- | Generate an assignment with some context type that is not known. +generateSomeM :: forall m f + . Applicative m + => Int + -> (Int -> m (Some f)) + -> m (Some (Assignment f)) +generateSomeM n f = go n + where go :: Int -> m (Some (Assignment f)) + go 0 = pure (Some empty) + go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1) + +-- | @replicate n@ make a context with different copies of the same +-- polymorphic value. +replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx +replicate n c = generate n (\_ -> c) + +-- | Generate an assignment +generate :: Size ctx + -> (forall tp . Index ctx tp -> f tp) + -> Assignment f ctx +generate n f = Assignment r + where r = unsafe_bin_generate (sizeInt n) 0 f +{-# NOINLINE generate #-} + +-- | Generate an assignment +generateM :: Applicative m + => Size ctx + -> (forall tp . Index ctx tp -> m (f tp)) + -> m (Assignment f ctx) +generateM n f = Assignment <$> unsafe_bin_generateM (sizeInt n) 0 f +{-# NOINLINE generateM #-} + +-- | Return empty assignment +empty :: Assignment f EmptyCtx +empty = Assignment Empty + +-- | Return true if assignment is empty. +null :: Assignment f ctx -> Bool +null (Assignment Empty) = True +null (Assignment _) = False + +extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x) +extend (Assignment x) y = Assignment $ append x (BalLeaf y) + +-- | Unexported index that returns an arbitrary type of expression. +unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u +unsafeIndex _ idx (Assignment t) = seq t $ unsafe_bin_index t idx 0 + +-- | Return value of assignment. +(!) :: Assignment f ctx -> Index ctx tp -> f tp +a ! Index i = assert (0 <= i && i < sizeInt (size a)) $ + unsafeIndex Proxy i a + +-- | Return value of assignment, where the index is into an +-- initial sequence of the assignment. +(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp +a !^ i = a ! extendIndex i + +instance TestEqualityFC Assignment where + testEqualityFC test (Assignment x) (Assignment y) = do + Refl <- testEqualityFC test x y + return Refl + +instance TestEquality f => TestEquality (Assignment f) where + testEquality = testEqualityFC testEquality + +instance TestEquality f => Eq (Assignment f ctx) where + x == y = isJust (testEquality x y) + +instance OrdFC Assignment where + compareFC test (Assignment x) (Assignment y) = + joinOrderingF (compareFC test x y) $ EQF + +instance OrdF f => OrdF (Assignment f) where + compareF = compareFC compareF + +instance OrdF f => Ord (Assignment f ctx) where + compare x y = toOrdering (compareF x y) + +instance HashableF (Index ctx) where + hashWithSaltF s i = hashWithSalt s (indexVal i) + +instance Hashable (Index ctx tp) where + hashWithSalt = hashWithSaltF + +instance HashableF f => Hashable (Assignment f ctx) where + hashWithSalt s (Assignment a) = hashWithSaltF s a + +instance HashableF f => HashableF (Assignment f) where + hashWithSaltF = hashWithSalt + +instance ShowF f => Show (Assignment f ctx) where + show a = "[" Prelude.++ intercalate ", " (toListFC showF a) Prelude.++ "]" + +instance ShowF f => ShowF (Assignment f) + +-- | Modify the value of an assignment at a particular index. +adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) +adjustM f (Index i) (Assignment a) = Assignment <$> (unsafe_bin_adjust f a i 0) +{-# SPECIALIZE adjustM :: (f tp -> Identity (f tp)) -> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx) #-} + +type instance IndexF (Assignment f ctx) = Index ctx +type instance IxValueF (Assignment f ctx) = f + +instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where + ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x) + ixF idx f = adjustM f idx + +instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where + ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x) + ixF' idx f = adjustM f idx + + +-- | Modify the value of an assignment at a particular index. +adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx +adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn) + +-- | Update the assignment at a particular index. +update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx +update i v a = adjust (\_ -> v) i a + +-- This is an unsafe version of update that changes the type of the expression. +unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx' +unsafeUpdate i (Assignment a) e = Assignment (runIdentity (unsafe_bin_adjust (\_ -> Identity e) a i 0)) + +-- | View an assignment as either empty or an assignment with one appended. +data AssignView f ctx where + AssignEmpty :: AssignView f EmptyCtx + AssignExtend :: Assignment f ctx + -> f tp + -> AssignView f (ctx::>tp) + +-- | View an assignment as either empty or an assignment with one appended. +view :: forall f ctx . Assignment f ctx -> AssignView f ctx +view (Assignment x) = + case bin_drop x of + DropEmpty -> AssignEmpty + DropExt t v -> unsafeCoerce $ AssignExtend (Assignment (unsafeCoerce t)) v + +-- | Return assignment with all but the last block. +init :: Assignment f (ctx '::> tp) -> Assignment f ctx +init (Assignment x) = + case bin_drop x of + DropExt t _ -> Assignment t + +-- | Return the last element in the assignment. +last :: Assignment f (ctx '::> tp) -> f tp +last x = + case view x of + AssignExtend _ e -> e + +decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp) +decompose x = case view x of AssignExtend a v -> (a,v) + +zipWith :: (forall x . f x -> g x -> h x) + -> Assignment f a + -> Assignment g a + -> Assignment h a +zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y +{-# INLINE zipWith #-} + +zipWithM :: Applicative m + => (forall x . f x -> g x -> m (h x)) + -> Assignment f a + -> Assignment g a + -> m (Assignment h a) +zipWithM f (Assignment x) (Assignment y) = Assignment <$> tree_zipWithM f x y +{-# INLINABLE zipWithM #-} + +instance FunctorFC Assignment where + fmapFC = \f (Assignment x) -> Assignment (fmap_bin f x) + {-# INLINE fmapFC #-} + +instance FoldableFC Assignment where + foldMapFC = foldMapFCDefault + {-# INLINE foldMapFC #-} + +instance TraversableFC Assignment where + traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x + {-# INLINE traverseFC #-} + +traverseWithIndex :: Applicative m + => (forall tp . Index ctx tp -> f tp -> m (g tp)) + -> Assignment f ctx + -> m (Assignment g ctx) +traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i) + +-- | Create an assignment from a list of values. +fromList :: [Some f] -> Some (Assignment f) +fromList = go empty + where go :: Assignment f ctx -> [Some f] -> Some (Assignment f) + go prev [] = Some prev + go prev (Some g:next) = (go $! prev `extend` g) next + +------------------------------------------------------------------------ +-- Appending + +appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y) +appendBal x (BalLeaf a) = x `extend` a +appendBal x (BalPair y z) = + case assoc x y z of + Refl -> x `appendBal` y `appendBal` z + +appendBin :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y) +appendBin x Empty = x +appendBin x (PlusOne _ y z) = + case assoc x y z of + Refl -> x `appendBin` y `appendBal` z +appendBin x (PlusZero _ y) = x `appendBin` y + +(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y) +x <++> Assignment y = x `appendBin` y + +------------------------------------------------------------------------ +-- KnownRepr instances + +instance (KnownRepr (Assignment f) ctx, KnownRepr f bt) + => KnownRepr (Assignment f) (ctx ::> bt) where + knownRepr = knownRepr `extend` knownRepr + +instance KnownRepr (Assignment f) EmptyCtx where + knownRepr = empty + +------------------------------------------------------------------------ +-- Lens combinators + +unsafeLens :: Int -> Lens.Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u) +unsafeLens idx = + Lens.lens (unsafeIndex Proxy idx) (unsafeUpdate idx) + +------------------------------------------------------------------------ +-- 1 field lens combinators + +type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1) + +instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where + _1 = unsafeLens 0 + +------------------------------------------------------------------------ +-- 2 field lens combinators + +type Assignment2 f x1 x2 + = Assignment f ('EmptyCtx '::> x1 '::> x2) + +instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where + _1 = unsafeLens 0 + +instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where + _2 = unsafeLens 1 + +------------------------------------------------------------------------ +-- 3 field lens combinators + +type Assignment3 f x1 x2 x3 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3) + +instance Lens.Field1 (Assignment3 f t x2 x3) + (Assignment3 f u x2 x3) + (f t) + (f u) where + _1 = unsafeLens 0 + + +instance Lens.Field2 (Assignment3 f x1 t x3) + (Assignment3 f x1 u x3) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment3 f x1 x2 t) + (Assignment3 f x1 x2 u) + (f t) + (f u) where + _3 = unsafeLens 2 + +------------------------------------------------------------------------ +-- 4 field lens combinators + +type Assignment4 f x1 x2 x3 x4 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4) + +instance Lens.Field1 (Assignment4 f t x2 x3 x4) + (Assignment4 f u x2 x3 x4) + (f t) + (f u) where + _1 = unsafeLens 0 + + +instance Lens.Field2 (Assignment4 f x1 t x3 x4) + (Assignment4 f x1 u x3 x4) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment4 f x1 x2 t x4) + (Assignment4 f x1 x2 u x4) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment4 f x1 x2 x3 t) + (Assignment4 f x1 x2 x3 u) + (f t) + (f u) where + _4 = unsafeLens 3 + +------------------------------------------------------------------------ +-- 5 field lens combinators + +type Assignment5 f x1 x2 x3 x4 x5 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5) + +instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5) + (Assignment5 f u x2 x3 x4 x5) + (f t) + (f u) where + _1 = unsafeLens 0 + +instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5) + (Assignment5 f x1 u x3 x4 x5) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5) + (Assignment5 f x1 x2 u x4 x5) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5) + (Assignment5 f x1 x2 x3 u x5) + (f t) + (f u) where + _4 = unsafeLens 3 + +instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t) + (Assignment5 f x1 x2 x3 x4 u) + (f t) + (f u) where + _5 = unsafeLens 4 + +------------------------------------------------------------------------ +-- 6 field lens combinators + +type Assignment6 f x1 x2 x3 x4 x5 x6 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6) + +instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6) + (Assignment6 f u x2 x3 x4 x5 x6) + (f t) + (f u) where + _1 = unsafeLens 0 + + +instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6) + (Assignment6 f x1 u x3 x4 x5 x6) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6) + (Assignment6 f x1 x2 u x4 x5 x6) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6) + (Assignment6 f x1 x2 x3 u x5 x6) + (f t) + (f u) where + _4 = unsafeLens 3 + +instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6) + (Assignment6 f x1 x2 x3 x4 u x6) + (f t) + (f u) where + _5 = unsafeLens 4 + +instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t) + (Assignment6 f x1 x2 x3 x4 x5 u) + (f t) + (f u) where + _6 = unsafeLens 5 + +------------------------------------------------------------------------ +-- 7 field lens combinators + +type Assignment7 f x1 x2 x3 x4 x5 x6 x7 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7) + +instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7) + (Assignment7 f u x2 x3 x4 x5 x6 x7) + (f t) + (f u) where + _1 = unsafeLens 0 + + +instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7) + (Assignment7 f x1 u x3 x4 x5 x6 x7) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7) + (Assignment7 f x1 x2 u x4 x5 x6 x7) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7) + (Assignment7 f x1 x2 x3 u x5 x6 x7) + (f t) + (f u) where + _4 = unsafeLens 3 + +instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7) + (Assignment7 f x1 x2 x3 x4 u x6 x7) + (f t) + (f u) where + _5 = unsafeLens 4 + +instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7) + (Assignment7 f x1 x2 x3 x4 x5 u x7) + (f t) + (f u) where + _6 = unsafeLens 5 + +instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t) + (Assignment7 f x1 x2 x3 x4 x5 x6 u) + (f t) + (f u) where + _7 = unsafeLens 6 + +------------------------------------------------------------------------ +-- 8 field lens combinators + +type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8) + +instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8) + (Assignment8 f u x2 x3 x4 x5 x6 x7 x8) + (f t) + (f u) where + _1 = unsafeLens 0 + + +instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8) + (Assignment8 f x1 u x3 x4 x5 x6 x7 x8) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8) + (Assignment8 f x1 x2 u x4 x5 x6 x7 x8) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8) + (Assignment8 f x1 x2 x3 u x5 x6 x7 x8) + (f t) + (f u) where + _4 = unsafeLens 3 + +instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8) + (Assignment8 f x1 x2 x3 x4 u x6 x7 x8) + (f t) + (f u) where + _5 = unsafeLens 4 + +instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8) + (Assignment8 f x1 x2 x3 x4 x5 u x7 x8) + (f t) + (f u) where + _6 = unsafeLens 5 + +instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8) + (Assignment8 f x1 x2 x3 x4 x5 x6 u x8) + (f t) + (f u) where + _7 = unsafeLens 6 + +instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t) + (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u) + (f t) + (f u) where + _8 = unsafeLens 7 + +------------------------------------------------------------------------ +-- 9 field lens combinators + +type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9 + = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9) + + +instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9) + (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _1 = unsafeLens 0 + +instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9) + (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _2 = unsafeLens 1 + +instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9) + (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9) + (f t) + (f u) where + _3 = unsafeLens 2 + +instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9) + (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9) + (f t) + (f u) where + _4 = unsafeLens 3 + +instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9) + (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9) + (f t) + (f u) where + _5 = unsafeLens 4 + +instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9) + (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9) + (f t) + (f u) where + _6 = unsafeLens 5 + +instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9) + (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9) + (f t) + (f u) where + _7 = unsafeLens 6 + +instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9) + (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9) + (f t) + (f u) where + _8 = unsafeLens 7 + +instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t) + (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u) + (f t) + (f u) where + _9 = unsafeLens 8 diff --git a/src/Data/Parameterized/Ctx.hs b/src/Data/Parameterized/Ctx.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Ctx.hs @@ -0,0 +1,99 @@ +{-| +Description : Type-level lists. +Copyright : (c) Galois, Inc 2015 +Maintainer : Joe Hendrix + +This module defines type-level lists used for representing the type of +variables in a context. +-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Parameterized.Ctx + ( type Ctx(..) + , EmptyCtx + , SingleCtx + , (::>) + , type (<+>) + + -- * Type context manipulation + , CtxSize + , CtxLookup + , CtxUpdate + , CtxLookupRight + , CtxUpdateRight + , CheckIx + , ValidIx + , FromLeft + ) where + +import Data.Kind (Constraint) +import GHC.TypeLits (Nat, type (+), type (-), type (<=?), TypeError, ErrorMessage(..)) + +------------------------------------------------------------------------ +-- Ctx + +type EmptyCtx = 'EmptyCtx +type (c :: Ctx k) ::> (a::k) = c '::> a + +type SingleCtx x = EmptyCtx ::> x + +-- | Kind @'Ctx' k@ comprises lists of types of kind @k@. +data Ctx k + = EmptyCtx + | Ctx k ::> k + +-- | Append two type-level contexts. +type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where + x <+> EmptyCtx = x + x <+> (y ::> e) = (x <+> y) ::> e + + +-- | This type family computes the number of elements in a 'Ctx' +type family CtxSize (a :: Ctx k) :: Nat where + CtxSize 'EmptyCtx = 0 + CtxSize (xs '::> x) = 1 + CtxSize xs + +-- | Helper type family used to generate descriptive error messages when +-- an index is larger than the length of the 'Ctx' being indexed. +type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint where + CheckIx ctx n 'True = () + CheckIx ctx n 'False = TypeError ('Text "Index " ':<>: 'ShowType n + ':<>: 'Text " out of range in " ':<>: 'ShowType ctx) + +-- | A constraint that checks that the nat @n@ is a valid index into the +-- context @ctx@, and raises a type error if not. +type ValidIx (n :: Nat) (ctx :: Ctx k) + = CheckIx ctx n (n+1 <=? CtxSize ctx) + +-- | 'Ctx' is a snoc-list. In order to use the more intuitive left-to-right +-- ordering of elements the desired index is subtracted from the total +-- number of elements. +type FromLeft ctx n = CtxSize ctx - 1 - n + +-- | Lookup the value in a context by number, from the right +type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where + CtxLookupRight 0 (ctx '::> r) = r + CtxLookupRight n (ctx '::> r) = CtxLookupRight (n-1) ctx + +-- | Update the value in a context by number, from the right. If the index +-- is out of range, the context is unchanged. +type family CtxUpdateRight (n :: Nat) (x::k) (ctx :: Ctx k) :: Ctx k where + CtxUpdateRight n x 'EmptyCtx = 'EmptyCtx + CtxUpdateRight 0 x (ctx '::> old) = ctx '::> x + CtxUpdateRight n x (ctx '::> y) = CtxUpdateRight (n-1) x ctx '::> y + +-- | Lookup the value in a context by number, from the left. +-- Produce a type error if the index is out of range. +type CtxLookup (n :: Nat) (ctx :: Ctx k) + = CtxLookupRight (FromLeft ctx n) ctx + +-- | Update the value in a context by number, from the left. If the index +-- is out of range, the context is unchanged. +type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) + = CtxUpdateRight (FromLeft ctx n) x ctx diff --git a/src/Data/Parameterized/Ctx/Proofs.hs b/src/Data/Parameterized/Ctx/Proofs.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Ctx/Proofs.hs @@ -0,0 +1,23 @@ +{-| +Copyright : (c) Galois, Inc 2015 +Maintainer : Joe Hendrix + +This reflects type level proofs involving contexts. +-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +module Data.Parameterized.Ctx.Proofs + ( leftId + , assoc + ) where + +import Data.Type.Equality +import Unsafe.Coerce + +import Data.Parameterized.Ctx + +leftId :: p x -> (EmptyCtx <+> x) :~: x +leftId _ = unsafeCoerce Refl + +assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z +assoc _ _ _ = unsafeCoerce Refl diff --git a/src/Data/Parameterized/HashTable.hs b/src/Data/Parameterized/HashTable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/HashTable.hs @@ -0,0 +1,97 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.HashTable +-- Copyright : (c) Galois, Inc 2014 +-- Maintainer : Joe Hendrix +-- +-- This module provides a ST-based hashtable for parameterized keys and values. +-- +-- NOTE: This API makes use of unsafeCoerce to implement the parameterized +-- hashtable abstraction. This should be typesafe provided the +-- 'TestEquality' instance on the key type is implemented soundly. +------------------------------------------------------------------------ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Trustworthy #-} +module Data.Parameterized.HashTable + ( HashTable + , new + , newSized + , clone + , lookup + , insert + , member + , delete + , clear + , Data.Parameterized.Classes.HashableF(..) + , Control.Monad.ST.RealWorld + ) where + +import Control.Applicative +import Control.Monad.ST +import qualified Data.HashTable.ST.Cuckoo as H +import GHC.Exts (Any) +import Unsafe.Coerce + +import Prelude hiding (lookup) + +import Data.Parameterized.Classes +import Data.Parameterized.Some + +-- | A hash table mapping nonces to values. +newtype HashTable s (key :: k -> *) (val :: k -> *) + = HashTable (H.HashTable s (Some key) Any) + +-- | Create a new empty table. +new :: ST s (HashTable s key val) +new = HashTable <$> H.new + +-- | Create a new empty table to hold 'n' elements. +newSized :: Int -> ST s (HashTable s k v) +newSized n = HashTable <$> H.newSized n + +-- | Create a hash table that is a copy of the current one. +clone :: (HashableF key, TestEquality key) + => HashTable s key val + -> ST s (HashTable s key val) +clone (HashTable tbl) = do + -- Create a new table + r <- H.new + -- Insert existing elements in + H.mapM_ (uncurry (H.insert r)) tbl + -- Return table + return $! HashTable r + +-- | Lookup value of key in table. +lookup :: (HashableF key, TestEquality key) + => HashTable s key val + -> key tp + -> ST s (Maybe (val tp)) +lookup (HashTable h) k = fmap unsafeCoerce <$> H.lookup h (Some k) +{-# INLINE lookup #-} + +-- | Insert new key and value mapping into table. +insert :: (HashableF key, TestEquality key) + => HashTable s (key :: k -> *) (val :: k -> *) + -> key tp + -> val tp + -> ST s () +insert (HashTable h) k v = H.insert h (Some k) (unsafeCoerce v) + +-- | Return true if the key is in the hash table. +member :: (HashableF key, TestEquality key) + => HashTable s (key :: k -> *) (val :: k -> *) + -> key (tp :: k) + -> ST s Bool +member (HashTable h) k = isJust <$> H.lookup h (Some k) + +-- | Delete an element from the hash table. +delete :: (HashableF key, TestEquality key) + => HashTable s (key :: k -> *) (val :: k -> *) + -> key (tp :: k) + -> ST s () +delete (HashTable h) k = H.delete h (Some k) + +clear :: (HashableF key, TestEquality key) + => HashTable s (key :: k -> *) (val :: k -> *) -> ST s () +clear (HashTable h) = H.mapM_ (\(k,_) -> H.delete h k) h diff --git a/src/Data/Parameterized/List.hs b/src/Data/Parameterized/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/List.hs @@ -0,0 +1,220 @@ +{-| +Copyright : (c) Galois, Inc 2017 +Maintainer : Joe Hendrix + +This module defines a list over two parameters. The first +is a fixed type-level function @k -> *@ for some kind @k@, and the +second is a list of types with kind k that provide the indices for +the values in the list. + +This type is closely related to the @Context@ type in +@Data.Parameterized.Context@. +-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +module Data.Parameterized.List + ( List(..) + , Index(..) + , indexValue + , (!!) + , update + , indexed + , imap + , ifoldr + , itraverse + -- * Constants + , index0 + , index1 + , index2 + , index3 + ) where + +import qualified Control.Lens as Lens +import Prelude hiding ((!!)) + +import Data.Parameterized.Classes +import Data.Parameterized.TraversableFC + +-- | Parameterized list of elements. +data List :: (k -> *) -> [k] -> * where + Nil :: List f '[] + (:<) :: f tp -> List f tps -> List f (tp : tps) + +infixr 5 :< + +instance ShowF f => Show (List f sh) where + show Nil = "Nil" + show (elt :< rest) = showF elt ++ " :< " ++ show rest + +instance ShowF f => ShowF (List f) + +instance FunctorFC List where + fmapFC _ Nil = Nil + fmapFC f (x :< xs) = f x :< fmapFC f xs + +instance FoldableFC List where + foldrFC _ z Nil = z + foldrFC f z (x :< xs) = f x (foldrFC f z xs) + +instance TraversableFC List where + traverseFC _ Nil = pure Nil + traverseFC f (h :< r) = (:<) <$> f h <*> traverseFC f r + +instance TestEquality f => TestEquality (List f) where + testEquality Nil Nil = Just Refl + testEquality (xh :< xl) (yh :< yl) = do + Refl <- testEquality xh yh + Refl <- testEquality xl yl + pure Refl + testEquality _ _ = Nothing + +instance OrdF f => OrdF (List f) where + compareF Nil Nil = EQF + compareF Nil _ = LTF + compareF _ Nil = GTF + compareF (xh :< xl) (yh :< yl) = + lexCompareF xh yh $ + lexCompareF xl yl $ + EQF + + +instance KnownRepr (List f) '[] where + knownRepr = Nil + +instance (KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f) (s ': sh) where + knownRepr = knownRepr :< knownRepr + +-------------------------------------------------------------------------------- +-- Indexed operations + + +-- | Represents an index into a type-level list. Used in place of integers to +-- 1. ensure that the given index *does* exist in the list +-- 2. guarantee that it has the given kind +data Index :: [k] -> k -> * where + IndexHere :: Index (x:r) x + IndexThere :: !(Index r y) -> Index (x:r) y + +deriving instance Eq (Index l x) +deriving instance Show (Index l x) + +instance ShowF (Index l) + +instance TestEquality (Index l) where + testEquality IndexHere IndexHere = Just Refl + testEquality (IndexThere x) (IndexThere y) = testEquality x y + testEquality _ _ = Nothing + +instance OrdF (Index l) where + compareF IndexHere IndexHere = EQF + compareF IndexHere IndexThere{} = LTF + compareF IndexThere{} IndexHere = GTF + compareF (IndexThere x) (IndexThere y) = compareF x y + +instance Ord (Index sh x) where + x `compare` y = toOrdering $ x `compareF` y + +-- | Return the index as an integer. +indexValue :: Index l tp -> Integer +indexValue = go 0 + where go :: Integer -> Index l tp -> Integer + go i IndexHere = i + go i (IndexThere x) = seq j $ go j x + where j = i+1 + +-- | Index 0 +index0 :: Index (x:r) x +index0 = IndexHere + +-- | Index 1 +index1 :: Index (x0:x1:r) x1 +index1 = IndexThere index0 + +-- | Index 2 +index2 :: Index (x0:x1:x2:r) x2 +index2 = IndexThere index1 + +-- | Index 3 +index3 :: Index (x0:x1:x2:x3:r) x3 +index3 = IndexThere index2 + +-- | Return the value in a list at a given index +(!!) :: List f l -> Index l x -> f x +l !! (IndexThere i) = + case l of + _ :< r -> r !! i +l !! IndexHere = + case l of + (h :< _) -> h + +-- | Update the 'List' at an index +update :: List f l -> Index l s -> (f s -> f s) -> List f l +update vals IndexHere upd = + case vals of + x :< rest -> upd x :< rest +update vals (IndexThere th) upd = + case vals of + x :< rest -> x :< update rest th upd + +-- | Provides a lens for manipulating the element at the given index. +indexed :: Index l x -> Lens.Simple Lens.Lens (List f l) (f x) +indexed IndexHere f (x :< rest) = (:< rest) <$> f x +indexed (IndexThere i) f (x :< rest) = (x :<) <$> indexed i f rest + +-------------------------------------------------------------------------------- +-- Indexed operations + +-- | Map over the elements in the list, and provide the index into +-- each element along with the element itself. +imap :: forall f g l + . (forall x . Index l x -> f x -> g x) + -> List f l + -> List g l +imap f = go id + where + go :: forall l' + . (forall tp . Index l' tp -> Index l tp) + -> List f l' + -> List g l' + go g l = + case l of + Nil -> Nil + e :< rest -> f (g IndexHere) e :< go (g . IndexThere) rest + +-- | Right-fold with an additional index. +ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b +ifoldr f seed0 l = go id l seed0 + where + go :: forall tps + . (forall tp . Index tps tp -> Index sh tp) + -> List a tps + -> b + -> b + go g ops b = + case ops of + Nil -> b + a :< rest -> f (g IndexHere) a (go (\ix -> g (IndexThere ix)) rest b) + +-- | Traverse with an additional index. +itraverse :: forall a b sh t + . Applicative t + => (forall tp . Index sh tp -> a tp -> t (b tp)) + -> List a sh + -> t (List b sh) +itraverse f = go id + where + go :: forall tps . (forall tp . Index tps tp -> Index sh tp) + -> List a tps + -> t (List b tps) + go g l = + case l of + Nil -> pure Nil + e :< rest -> (:<) <$> f (g IndexHere) e <*> go (\ix -> g (IndexThere ix)) rest diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Map.hs @@ -0,0 +1,546 @@ +{-| +Copyright : (c) Galois, Inc 2014-2017 + +This module defines finite maps where the key and value types are +parameterized by an arbitrary kind. + +Some code was adapted from containers. +-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TypeFamilies #-} +module Data.Parameterized.Map + ( MapF + -- * Construction + , Data.Parameterized.Map.empty + , singleton + , insert + , insertWith + , delete + , union + -- * Query + , null + , lookup + , member + , notMember + , size + -- * Conversion + , keys + , elems + , fromList + , toList + , fromKeys + , fromKeysM + -- * Filter + , filterGt + , filterLt + -- * Folds + , foldrWithKey + -- * Traversal + , map + , mapMaybe + , traverseWithKey + , traverseWithKey_ + -- * Complex interface. + , UpdateRequest(..) + , Updated(..) + , updatedValue + , updateAtKey + , mergeWithKeyM + , module Data.Parameterized.Classes + -- * Pair + , Pair(..) + ) where + +import Control.Applicative hiding (empty) +import Control.Lens (Traversal', Lens') +import Control.Monad.Identity +import Data.List (intercalate, foldl') +import Data.Maybe () + +import Data.Parameterized.Classes +import Data.Parameterized.Some +import Data.Parameterized.Pair ( Pair(..) ) +import Data.Parameterized.TraversableF +import Data.Parameterized.Utils.BinTree + ( MaybeS(..) + , fromMaybeS + , Updated(..) + , updatedValue + , TreeApp(..) + , bin + , IsBinTree(..) + , balanceL + , balanceR + , glue + ) +import qualified Data.Parameterized.Utils.BinTree as Bin + +#if MIN_VERSION_base(4,8,0) +import Prelude hiding (lookup, map, traverse, null) +#else +import Prelude hiding (lookup, map, null) +#endif + +------------------------------------------------------------------------ +-- Pair + +comparePairKeys :: OrdF k => Pair k a -> Pair k a -> Ordering +comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y) +{-# INLINABLE comparePairKeys #-} + +------------------------------------------------------------------------ +-- MapF + +-- | A map from parameterized keys to values with the same paramter type. +data MapF (k :: v -> *) (a :: v -> *) where + Bin :: {-# UNPACK #-} + !Size -- Number of elements in tree. + -> !(k x) + -> !(a x) + -> !(MapF k a) + -> !(MapF k a) + -> MapF k a + Tip :: MapF k a + +type Size = Int + +-- | Return empty map +empty :: MapF k a +empty = Tip + +-- | Return true if map is empty +null :: MapF k a -> Bool +null Tip = True +null Bin{} = False + +-- | Return map containing a single element +singleton :: k tp -> a tp -> MapF k a +singleton k x = Bin 1 k x Tip Tip + +instance Bin.IsBinTree (MapF k a) (Pair k a) where + asBin (Bin _ k v l r) = BinTree (Pair k v) l r + asBin Tip = TipTree + + tip = Tip + bin (Pair k v) l r = Bin (size l + size r + 1) k v l r + + size Tip = 0 + size (Bin sz _ _ _ _) = sz + +instance (TestEquality k, EqF a) => Eq (MapF k a) where + x == y = size x == size y && toList x == toList y + +------------------------------------------------------------------------ +-- Traversals + +#ifdef __GLASGOW_HASKELL__ +{-# NOINLINE [1] map #-} +{-# NOINLINE [1] traverse #-} +{-# RULES +"map/map" forall (f :: (forall tp . f tp -> g tp)) (g :: (forall tp . g tp -> h tp)) xs + . map g (map f xs) = map (g . f) xs +"map/traverse" forall (f :: (forall tp . f tp -> m (g tp))) (g :: (forall tp . g tp -> h tp)) xs + . fmap (map g) (traverse f xs) = traverse (\v -> g <$> f v) xs +"traverse/map" + forall (f :: (forall tp . f tp -> g tp)) (g :: (forall tp . g tp -> m (h tp))) xs + . traverse g (map f xs) = traverse (\v -> g (f v)) xs +"traverse/traverse" + forall (f :: (forall tp . f tp -> m (g tp))) (g :: (forall tp . g tp -> m (h tp))) xs + . traverse f xs >>= traverse g = traverse (\v -> f v >>= g) xs + #-} +#endif + +-- | Modify elements in a map +map :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g +map _ Tip = Tip +map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r) + +-- | Run partial map over elements. +mapMaybe :: (forall tp . f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g +mapMaybe _ Tip = Tip +mapMaybe f (Bin _ k x l r) = + case f x of + Just y -> Bin.link (Pair k y) (mapMaybe f l) (mapMaybe f r) + Nothing -> Bin.merge (mapMaybe f l) (mapMaybe f r) + +-- | Traverse elements in a map +traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g) +traverse _ Tip = pure Tip +traverse f (Bin sx kx x l r) = Bin sx kx <$> f x <*> traverse f l <*> traverse f r + +-- | Traverse elements in a map +traverseWithKey + :: Applicative m + => (forall tp . ktp tp -> f tp -> m (g tp)) + -> MapF ktp f + -> m (MapF ktp g) +traverseWithKey _ Tip = pure Tip +traverseWithKey f (Bin sx kx x l r) = + Bin sx kx <$> f kx x <*> traverseWithKey f l <*> traverseWithKey f r + +-- | Traverse elements in a map without returning result. +traverseWithKey_ + :: Applicative m + => (forall tp . ktp tp -> f tp -> m ()) + -> MapF ktp f + -> m () +traverseWithKey_ _ Tip = pure () +traverseWithKey_ f (Bin _ kx x l r) = f kx x *> traverseWithKey_ f l *> traverseWithKey_ f r + + +type instance IndexF (MapF k v) = k +type instance IxValueF (MapF k v) = v + +-- | Turn a map key into a traversal that visits the indicated element in the map, if it exists. +instance forall (k:: a -> *) v. OrdF k => IxedF a (MapF k v) where + ixF :: k x -> Traversal' (MapF k v) (v x) + ixF i f m = updatedValue <$> updateAtKey i (pure Nothing) (\x -> Set <$> f x) m + +-- | Turn a map key into a lens that points into the indicated position in the map. +instance forall (k:: a -> *) v. OrdF k => AtF a (MapF k v) where + atF :: k x -> Lens' (MapF k v) (Maybe (v x)) + atF i f m = updatedValue <$> updateAtKey i (f Nothing) (\x -> maybe Delete Set <$> f (Just x)) m + + +-- | Lookup value in map. +lookup :: OrdF k => k tp -> MapF k a -> Maybe (a tp) +lookup k0 = seq k0 (go k0) + where + go :: OrdF k => k tp -> MapF k a -> Maybe (a tp) + go _ Tip = Nothing + go k (Bin _ kx x l r) = + case compareF k kx of + LTF -> go k l + GTF -> go k r + EQF -> Just x +{-# INLINABLE lookup #-} + +-- | Return true if key is bound in map. +member :: OrdF k => k tp -> MapF k a -> Bool +member k0 = seq k0 (go k0) + where + go :: OrdF k => k tp -> MapF k a -> Bool + go _ Tip = False + go k (Bin _ kx _ l r) = + case compareF k kx of + LTF -> go k l + GTF -> go k r + EQF -> True +{-# INLINABLE member #-} + +-- | Return true if key is not bound in map. +notMember :: OrdF k => k tp -> MapF k a -> Bool +notMember k m = not $ member k m +{-# INLINABLE notMember #-} + +instance FunctorF (MapF ktp) where + fmapF = map + +instance FoldableF (MapF ktp) where + foldrF f z = go z + where go z' Tip = z' + go z' (Bin _ _ x l r) = go (f x (go z' r)) l + +instance TraversableF (MapF ktp) where + traverseF = traverse + +instance (ShowF ktp, ShowF rtp) => Show (MapF ktp rtp) where + show m = showMap showF showF m + +-- | Return all keys of the map in ascending order. +keys :: MapF k a -> [Some k] +keys = foldrWithKey (\k _ l -> Some k : l) [] + +-- | Return all elements of the map in the ascending order of their keys. +elems :: MapF k a -> [Some a] +elems = foldrF (\e l -> Some e : l) [] + +-- | Perform a fold with the key also provided. +foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b +foldrWithKey f z = go z + where + go z' Tip = z' + go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l + +showMap :: (forall tp . ktp tp -> String) + -> (forall tp . rtp tp -> String) + -> MapF ktp rtp + -> String +showMap ppk ppv m = "{ " ++ intercalate ", " l ++ " }" + where l = foldrWithKey (\k a l0 -> (ppk k ++ " -> " ++ ppv a) : l0) [] m + +------------------------------------------------------------------------ +-- filter + +compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering +compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x) + +-- | @filterGt k m@ returns submap of @m@ that only contains entries +-- that are larger than @k@. +filterGt :: OrdF k => k tp -> MapF k v -> MapF k v +filterGt k m = fromMaybeS m (Bin.filterGt (compareKeyPair k) m) +{-# INLINABLE filterGt #-} + +-- | @filterLt k m@ returns submap of @m@ that only contains entries +-- that are smaller than @k@. +filterLt :: OrdF k => k tp -> MapF k v -> MapF k v +filterLt k m = fromMaybeS m (Bin.filterLt (compareKeyPair k) m) +{-# INLINABLE filterLt #-} + +------------------------------------------------------------------------ +-- User operations + +-- | Insert a binding into the map, replacing the existing binding if needed. +insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a +insert = \k v m -> seq k $ updatedValue (Bin.insert comparePairKeys (Pair k v) m) +{-# INLINABLE insert #-} +-- {-# SPECIALIZE Bin.insert :: OrdF k => Pair k a -> MapF k a -> Updated (MapF k a) #-} + +-- | Insert a binding into the map, replacing the existing binding if needed. +insertWithImpl :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> Updated (MapF k a) +insertWithImpl f k v t = seq k $ + case t of + Tip -> Bin.Updated (Bin 1 k v Tip Tip) + Bin sz yk yv l r -> + case compareF k yk of + LTF -> + case insertWithImpl f k v l of + Bin.Updated l' -> Bin.Updated (Bin.balanceL (Pair yk yv) l' r) + Bin.Unchanged l' -> Bin.Unchanged (Bin sz yk yv l' r) + GTF -> + case insertWithImpl f k v r of + Bin.Updated r' -> Bin.Updated (Bin.balanceR (Pair yk yv) l r') + Bin.Unchanged r' -> Bin.Unchanged (Bin sz yk yv l r') + EQF -> Bin.Unchanged (Bin sz yk (f v yv) l r) +{-# INLINABLE insertWithImpl #-} + +-- | @insertWith f new m@ inserts the binding into @m@. +-- +-- It inserts @f new old@ if @m@ already contains an equivaltn value +-- @old@, and @new@ otherwise. It returns an Unchanged value if the +-- map stays the same size and an updated value if a new entry was +-- inserted. +insertWith :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a +insertWith = \f k v t -> seq k $ updatedValue (insertWithImpl f k v t) +{-# INLINABLE insertWith #-} + +-- | Delete a value from the map if present. +delete :: OrdF k => k tp -> MapF k a -> MapF k a +delete = \k m -> seq k $ fromMaybeS m $ Bin.delete (p k) m + where p :: OrdF k => k tp -> Pair k a -> Ordering + p k (Pair kx _) = toOrdering (compareF k kx) +{-# INLINABLE delete #-} +{-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-} + +-- | Union two sets +union :: OrdF k => MapF k a -> MapF k a -> MapF k a +union t1 t2 = Bin.union comparePairKeys t1 t2 +{-# INLINABLE union #-} +-- {-# SPECIALIZE Bin.union compare :: OrdF k => MapF k a -> MapF k a -> MapF k a #-} + +------------------------------------------------------------------------ +-- updateAtKey + +-- | Update request tells when to do with value +data UpdateRequest v + = -- | Keep the current value. + Keep + -- | Set the value to a new value. + | Set !v + -- | Delete a value. + | Delete + +data AtKeyResult k a where + AtKeyUnchanged :: AtKeyResult k a + AtKeyInserted :: MapF k a -> AtKeyResult k a + AtKeyModified :: MapF k a -> AtKeyResult k a + AtKeyDeleted :: MapF k a -> AtKeyResult k a + +atKey' :: (OrdF k, Functor f) + => k tp + -> f (Maybe (a tp)) -- ^ Function to call if no element is found. + -> (a tp -> f (UpdateRequest (a tp))) + -> MapF k a + -> f (AtKeyResult k a) +atKey' k onNotFound onFound t = + case asBin t of + TipTree -> ins <$> onNotFound + where ins Nothing = AtKeyUnchanged + ins (Just v) = AtKeyInserted (singleton k v) + BinTree yp@(Pair kx y) l r -> + case compareF k kx of + LTF -> ins <$> atKey' k onNotFound onFound l + where ins AtKeyUnchanged = AtKeyUnchanged + ins (AtKeyInserted l') = AtKeyInserted (balanceL yp l' r) + ins (AtKeyModified l') = AtKeyModified (bin yp l' r) + ins (AtKeyDeleted l') = AtKeyDeleted (balanceR yp l' r) + GTF -> ins <$> atKey' k onNotFound onFound r + where ins AtKeyUnchanged = AtKeyUnchanged + ins (AtKeyInserted r') = AtKeyInserted (balanceR yp l r') + ins (AtKeyModified r') = AtKeyModified (bin yp l r') + ins (AtKeyDeleted r') = AtKeyDeleted (balanceL yp l r') + EQF -> ins <$> onFound y + where ins Keep = AtKeyUnchanged + ins (Set x) = AtKeyModified (bin (Pair kx x) l r) + ins Delete = AtKeyDeleted (glue l r) +{-# INLINABLE atKey' #-} + +-- | Log-time algorithm that allows a value at a specific key to be added, replaced, +-- or deleted. +updateAtKey :: (OrdF k, Functor f) + => k tp -- ^ Key to update + -> f (Maybe (a tp)) + -- ^ Action to call if nothing is found + -> (a tp -> f (UpdateRequest (a tp))) + -- ^ Action to call if value is found. + -> MapF k a + -- ^ Map to update + -> f (Updated (MapF k a)) +updateAtKey k onNotFound onFound t = ins <$> atKey' k onNotFound onFound t + where ins AtKeyUnchanged = Unchanged t + ins (AtKeyInserted t') = Updated t' + ins (AtKeyModified t') = Updated t' + ins (AtKeyDeleted t') = Updated t' +{-# INLINABLE updateAtKey #-} + +-- | Create a Map from a list of pairs. +fromList :: OrdF k => [Pair k a] -> MapF k a +fromList = foldl' (\m (Pair k a) -> insert k a m) Data.Parameterized.Map.empty + +toList :: MapF k a -> [Pair k a] +toList = foldrWithKey (\k x m -> Pair k x : m) [] + +-- | Generate a map from a foldable collection of keys and a +-- function from keys to values. +fromKeys :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *) + . (Monad m, Foldable t, OrdF a) + => (forall tp . a tp -> m (v tp)) + -- ^ Function for evaluating a register value. + -> t (Some a) + -- ^ Set of X86 registers + -> m (MapF a v) +fromKeys f = foldM go empty + where go :: MapF a v -> Some a -> m (MapF a v) + go m (Some k) = (\v -> insert k v m) <$> f k + +-- | Generate a map from a foldable collection of keys and a monadic +-- function from keys to values. +fromKeysM :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *) + . (Monad m, Foldable t, OrdF a) + => (forall tp . a tp -> m (v tp)) + -- ^ Function for evaluating a register value. + -> t (Some a) + -- ^ Set of X86 registers + -> m (MapF a v) +fromKeysM f = foldM go empty + where go :: MapF a v -> Some a -> m (MapF a v) + go m (Some k) = (\v -> insert k v m) <$> f k + +filterGtMaybe :: OrdF k => MaybeS (k x) -> MapF k a -> MapF k a +filterGtMaybe NothingS m = m +filterGtMaybe (JustS k) m = filterGt k m + +filterLtMaybe :: OrdF k => MaybeS (k x) -> MapF k a -> MapF k a +filterLtMaybe NothingS m = m +filterLtMaybe (JustS k) m = filterLt k m + +-- | Merge bindings in two maps to get a third. +mergeWithKeyM :: forall k a b c m + . (Applicative m, OrdF k) + => (forall tp . k tp -> a tp -> b tp -> m (Maybe (c tp))) + -> (MapF k a -> m (MapF k c)) + -> (MapF k b -> m (MapF k c)) + -> MapF k a + -> MapF k b + -> m (MapF k c) +mergeWithKeyM f g1 g2 = go + where + go Tip t2 = g2 t2 + go t1 Tip = g1 t1 + go t1 t2 = hedgeMerge NothingS NothingS t1 t2 + + hedgeMerge :: MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k b -> m (MapF k c) + hedgeMerge _ _ t1 Tip = g1 t1 + hedgeMerge blo bhi Tip (Bin _ kx x l r) = + g2 $ Bin.link (Pair kx x) (filterGtMaybe blo l) (filterLtMaybe bhi r) + hedgeMerge blo bhi (Bin _ kx x l r) t2 = + let Bin.PairS found trim_t2 = trimLookupLo kx bhi t2 + resolve_g1 :: MapF k c -> MapF k c -> MapF k c -> MapF k c + resolve_g1 Tip = Bin.merge + resolve_g1 (Bin _ k' x' Tip Tip) = Bin.link (Pair k' x') + resolve_g1 _ = error "mergeWithKey: Bad function g1" + resolve_f Nothing = Bin.merge + resolve_f (Just x') = Bin.link (Pair kx x') + in case found of + Nothing -> + resolve_g1 <$> g1 (singleton kx x) + <*> hedgeMerge blo bmi l (trim blo bmi t2) + <*> hedgeMerge bmi bhi r trim_t2 + Just x2 -> + resolve_f <$> f kx x x2 + <*> hedgeMerge blo bmi l (trim blo bmi t2) + <*> hedgeMerge bmi bhi r trim_t2 + where bmi = JustS kx +{-# INLINABLE mergeWithKeyM #-} + +{-------------------------------------------------------------------- + [trim blo bhi t] trims away all subtrees that surely contain no + values between the range [blo] to [bhi]. The returned tree is either + empty or the key of the root is between @blo@ and @bhi@. +--------------------------------------------------------------------} +trim :: OrdF k => MaybeS (k x) -> MaybeS (k y) -> MapF k a -> MapF k a +trim NothingS NothingS t = t +trim (JustS lk) NothingS t = filterGt lk t +trim NothingS (JustS hk) t = filterLt hk t +trim (JustS lk) (JustS hk) t = filterMiddle lk hk t + +-- | Returns only entries that are strictly between the two keys. +filterMiddle :: OrdF k => k x -> k y -> MapF k a -> MapF k a +filterMiddle lo hi (Bin _ k _ _ r) + | k `leqF` lo = filterMiddle lo hi r +filterMiddle lo hi (Bin _ k _ l _) + | k `geqF` hi = filterMiddle lo hi l +filterMiddle _ _ t = t +{-# INLINABLE filterMiddle #-} + + + +-- Helper function for 'mergeWithKey'. The @'trimLookupLo' lk hk t@ performs both +-- @'trim' (JustS lk) hk t@ and @'lookup' lk t@. + +-- See Note: Type of local 'go' function +trimLookupLo :: OrdF k => k tp -> MaybeS (k y) -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) +trimLookupLo lk NothingS t = greater lk t + where greater :: OrdF k => k tp -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) + greater lo t'@(Bin _ kx x l r) = + case compareF lo kx of + LTF -> Bin.PairS (lookup lo l) t' + EQF -> Bin.PairS (Just x) r + GTF -> greater lo r + greater _ Tip = Bin.PairS Nothing Tip +trimLookupLo lk (JustS hk) t = middle lk hk t + where middle :: OrdF k => k tp -> k y -> MapF k a -> Bin.PairS (Maybe (a tp)) (MapF k a) + middle lo hi t'@(Bin _ kx x l r) = + case compareF lo kx of + LTF | kx `ltF` hi -> Bin.PairS (lookup lo l) t' + | otherwise -> middle lo hi l + EQF -> Bin.PairS (Just x) (lesser hi r) + GTF -> middle lo hi r + middle _ _ Tip = Bin.PairS Nothing Tip + + lesser :: OrdF k => k y -> MapF k a -> MapF k a + lesser hi (Bin _ k _ l _) | k `geqF` hi = lesser hi l + lesser _ t' = t' diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/NatRepr.hs @@ -0,0 +1,479 @@ +{-| +Copyright : (c) Galois, Inc 2014-2015 +Maintainer : Joe Hendrix + +This defines a type 'NatRepr' for representing a type-level natural +at runtime. This can be used to branch on a type-level value. For +each @n@, @NatRepr n@ contains a single value containing the vlaue +@n@. This can be used to help use type-level variables on code +with data dependendent types. + +The 'TestEquality' instance for 'NatRepr' is implemented using +'unsafeCoerce', as is the `isZeroNat` function. This should be +typesafe because we maintain the invariant that the integer value +contained in a NatRepr value matches its static type. +-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE Trustworthy #-} +#if MIN_VERSION_base(4,9,0) +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} +#endif +module Data.Parameterized.NatRepr + ( NatRepr + , natValue + , knownNat + , withKnownNat + , IsZeroNat(..) + , isZeroNat + , NatComparison(..) + , compareNat + , decNat + , predNat + , incNat + , addNat + , subNat + , halfNat + , withDivModNat + , natMultiply + , someNat + , maxNat + , natRec + , natForEach + , NatCases(..) + , testNatCases + -- * Bitvector utilities + , widthVal + , minUnsigned + , maxUnsigned + , minSigned + , maxSigned + , toUnsigned + , toSigned + , unsignedClamp + , signedClamp + -- * LeqProof + , LeqProof(..) + , testLeq + , testStrictLeq + , leqRefl + , leqTrans + , leqAdd2 + , leqSub2 + , leqMulCongr + -- * LeqProof combinators + , leqProof + , withLeqProof + , isPosNat + , leqAdd + , leqSub + , leqMulPos + , addIsLeq + , withAddLeq + , addPrefixIsLeq + , withAddPrefixLeq + , addIsLeqLeft1 + , dblPosIsPos + -- * Arithmetic proof + , plusComm + , plusMinusCancel + , withAddMulDistribRight + -- * Re-exports typelists basics +-- , NatK + , type (+) + , type (-) + , type (*) + , type (<=) + , Equality.TestEquality(..) + , (Equality.:~:)(..) + , Data.Parameterized.Some.Some + ) where + +import Data.Bits ((.&.)) +import Data.Hashable +import Data.Proxy as Proxy +import Data.Type.Equality as Equality +import GHC.TypeLits as TypeLits +import Unsafe.Coerce + +import Data.Parameterized.Classes +import Data.Parameterized.Some + +maxInt :: Integer +maxInt = toInteger (maxBound :: Int) + +------------------------------------------------------------------------ +-- Nat + +-- | A runtime presentation of a type-level 'Nat'. +-- +-- This can be used for performing dynamic checks on a type-level natural +-- numbers. +newtype NatRepr (n::Nat) = NatRepr { natValue :: Integer + -- ^ The underlying integer value of the number. + } + deriving (Hashable) + +-- | Return the value of the nat representation. +widthVal :: NatRepr n -> Int +widthVal (NatRepr i) | i < maxInt = fromInteger i + | otherwise = error "Width is too large." + +instance Eq (NatRepr m) where + _ == _ = True + +instance TestEquality NatRepr where + testEquality (NatRepr m) (NatRepr n) + | m == n = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | Result of comparing two numbers. +data NatComparison m n where + -- First number is less than second. + NatLT :: !(NatRepr y) -> NatComparison x (x+(y+1)) + NatEQ :: NatComparison x x + -- First number is greater than second. + NatGT :: !(NatRepr y) -> NatComparison (x+(y+1)) x + +compareNat :: NatRepr m -> NatRepr n -> NatComparison m n +compareNat m n = + case compare (natValue m) (natValue n) of + LT -> unsafeCoerce $ NatLT (NatRepr (natValue n - natValue m - 1)) + EQ -> unsafeCoerce $ NatEQ + GT -> unsafeCoerce $ NatGT (NatRepr (natValue m - natValue n - 1)) + +instance OrdF NatRepr where + compareF x y = + case compareNat x y of + NatLT _ -> LTF + NatEQ -> EQF + NatGT _ -> GTF + +instance PolyEq (NatRepr m) (NatRepr n) where + polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y + +instance Show (NatRepr n) where + show (NatRepr n) = show n + +instance ShowF NatRepr + +instance HashableF NatRepr where + hashWithSaltF = hashWithSalt + +-- | This generates a NatRepr from a type-level context. +knownNat :: forall n . KnownNat n => NatRepr n +knownNat = NatRepr (natVal (Proxy :: Proxy n)) + +instance (KnownNat n) => KnownRepr NatRepr n where + knownRepr = knownNat + +{-# DEPRECATED withKnownNat "This function is potentially unsafe and is schedueled to be removed." #-} +withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r +withKnownNat (NatRepr nVal) v = + case someNatVal nVal of + Just (SomeNat (Proxy :: Proxy n')) -> + case unsafeCoerce (Refl :: 0 :~: 0) :: n :~: n' of + Refl -> v + Nothing -> error "withKnownNat: inner value in NatRepr is not a natural" + +data IsZeroNat n where + ZeroNat :: IsZeroNat 0 + NonZeroNat :: IsZeroNat (n+1) + +isZeroNat :: NatRepr n -> IsZeroNat n +isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat +isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat + +-- | Decrement a @NatRepr@ +decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1) +decNat (NatRepr i) = NatRepr (i-1) + +-- | Get the predicessor of a nat +predNat :: NatRepr (n+1) -> NatRepr n +predNat (NatRepr i) = NatRepr (i-1) + +-- | Increment a @NatRepr@ +incNat :: NatRepr n -> NatRepr (n+1) +incNat (NatRepr x) = NatRepr (x+1) + +halfNat :: NatRepr (n+n) -> NatRepr n +halfNat (NatRepr x) = NatRepr (x `div` 2) + +addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n) +addNat (NatRepr m) (NatRepr n) = NatRepr (m+n) + +subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n) +subNat (NatRepr m) (NatRepr n) = NatRepr (m-n) + +withDivModNat :: forall n m a. + NatRepr n + -> NatRepr m + -> (forall div mod. (n ~ ((div * m) + mod)) => + NatRepr div -> NatRepr mod -> a) + -> a +withDivModNat n m f = + case ( Some (NatRepr divPart), Some (NatRepr modPart)) of + ( Some (divn :: NatRepr div), Some (modn :: NatRepr mod) ) + -> case unsafeCoerce (Refl :: 0 :~: 0) of + (Refl :: (n :~: ((div * m) + mod))) -> f divn modn + where + (divPart, modPart) = divMod (natValue n) (natValue m) + +natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m) +natMultiply (NatRepr n) (NatRepr m) = NatRepr (n * m) + +------------------------------------------------------------------------ +-- Operations for using NatRepr as a bitwidth. + +-- | Return minimum unsigned value for bitvector with given width (always 0). +minUnsigned :: NatRepr w -> Integer +minUnsigned _ = 0 + +-- | Return maximum unsigned value for bitvector with given width. +maxUnsigned :: NatRepr w -> Integer +maxUnsigned w = 2^(natValue w) - 1 + +-- | Return minimum value for bitvector in 2s complement with given width. +minSigned :: (1 <= w) => NatRepr w -> Integer +minSigned w = negate (2^(natValue w - 1)) + +-- | Return maximum value for bitvector in 2s complement with given width. +maxSigned :: (1 <= w) => NatRepr w -> Integer +maxSigned w = 2^(natValue w - 1) - 1 + +-- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@. +toUnsigned :: NatRepr w -> Integer -> Integer +toUnsigned w i = maxUnsigned w .&. i + +-- | @toSigned w i@ interprets the least-significant @w@ bits in @i@ as a +-- signed number in two's complement notation and returns that value. +toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer +toSigned w i0 + | i > maxSigned w = i - 2^(natValue w) + | otherwise = i + where i = i0 .&. maxUnsigned w + +-- | @unsignedClamp w i@ rounds @i@ to the nearest value between +-- @0@ and @2^w-i@ (inclusive). +unsignedClamp :: NatRepr w -> Integer -> Integer +unsignedClamp w i + | i < minUnsigned w = minUnsigned w + | i > maxUnsigned w = maxUnsigned w + | otherwise = i + +-- | @signedClamp w i@ rounds @i@ to the nearest value between +-- @-2^(w-1)@ and @2^(w-1)-i@ (inclusive). +signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer +signedClamp w i + | i < minSigned w = minSigned w + | i > maxSigned w = maxSigned w + | otherwise = i + +------------------------------------------------------------------------ +-- Some NatRepr + +someNat :: Integer -> Maybe (Some NatRepr) +someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n))) + | otherwise = Nothing + +-- | Return the maximum of two nat representations. +maxNat :: NatRepr m -> NatRepr n -> Some NatRepr +maxNat x y + | natValue x >= natValue y = Some x + | otherwise = Some y + +------------------------------------------------------------------------ +-- Arithmetic + +-- | Produce evidence that + is commutative. +plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m +plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n) + +-- | Cancel an add followed b a subtract +plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m +plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m) + +withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p + -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a +withAddMulDistribRight _n _m _p f = + case unsafeCoerce (Refl :: 0 :~: 0) of + (Refl :: (((n * p) + (m * p)) :~: ((n + m) * p)) ) -> f + +------------------------------------------------------------------------ +-- LeqProof + +-- | @LeqProof m n@ is a type whose values are only inhabited when @m@ +-- is less than or equal to @n@. +data LeqProof m n where + LeqProof :: (m <= n) => LeqProof m n + +testStrictLeq :: forall m n + . (m <= n) + => NatRepr m + -> NatRepr n + -> Either (LeqProof (m+1) n) (m :~: n) +testStrictLeq (NatRepr m) (NatRepr n) + | m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0)) + | otherwise = Right (unsafeCoerce (Refl :: m :~: m)) +{-# NOINLINE testStrictLeq #-} + +-- As for NatComparison above, but works with LeqProof +data NatCases m n where + -- First number is less than second. + NatCaseLT :: LeqProof (m+1) n -> NatCases m n + NatCaseEQ :: NatCases m m + -- First number is greater than second. + NatCaseGT :: LeqProof (n+1) m -> NatCases m n + +testNatCases :: forall m n + . NatRepr m + -> NatRepr n + -> NatCases m n +testNatCases m n = + case compare (natValue m) (natValue n) of + LT -> NatCaseLT (unsafeCoerce (LeqProof :: LeqProof 0 0)) + EQ -> unsafeCoerce $ (NatCaseEQ :: NatCases m m) + GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0)) +{-# NOINLINE testNatCases #-} + +-- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@. +testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n) +testLeq (NatRepr m) (NatRepr n) + | m <= n = Just (unsafeCoerce (LeqProof :: LeqProof 0 0)) + | otherwise = Nothing +{-# NOINLINE testLeq #-} + +-- | Apply reflexivity to LeqProof +leqRefl :: forall f n . f n -> LeqProof n n +leqRefl _ = LeqProof + + +-- | Apply transitivity to LeqProof +leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p +leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0) +{-# NOINLINE leqTrans #-} + +-- | Add both sides of two inequalities +leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h) +leqAdd2 x y = seq x $ seq y $ unsafeCoerce (LeqProof :: LeqProof 0 0) +{-# NOINLINE leqAdd2 #-} + +-- | Subtract sides of two inequalities. +leqSub2 :: LeqProof x_l x_h + -> LeqProof y_l y_h + -> LeqProof (x_l-y_h) (x_h-y_l) +leqSub2 LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0) +{-# NOINLINE leqSub2 #-} + +------------------------------------------------------------------------ +-- LeqProof combinators + +-- | Create a leqProof using two proxies +leqProof :: (m <= n) => f m -> f n -> LeqProof m n +leqProof _ _ = LeqProof + +withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a +withLeqProof p a = + case p of + LeqProof -> a + +-- | Test whether natural number is positive. +isPosNat :: NatRepr n -> Maybe (LeqProof 1 n) +isPosNat = testLeq (knownNat :: NatRepr 1) + +-- | Congruence rule for multiplication +leqMulCongr :: LeqProof a x + -> LeqProof b y + -> LeqProof (a*b) (x*y) +leqMulCongr LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 1 1) +{-# NOINLINE leqMulCongr #-} + +-- | Multiplying two positive numbers results in a positive number. +leqMulPos :: forall p q x y + . (1 <= x, 1 <= y) + => p x + -> q y + -> LeqProof 1 (x*y) +leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y) + +-- | Produce proof that adding a value to the larger element in an LeqProof +-- is larger +leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p) +leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p) + +-- | Produce proof that subtracting a value from the smaller element is smaller. +leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n +leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p) + +addIsLeq :: f n -> g m -> LeqProof n (n + m) +addIsLeq n m = leqAdd (leqRefl n) m + +addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n) +addPrefixIsLeq m n = + case plusComm n m of + Refl -> addIsLeq n m + +dblPosIsPos :: forall n . LeqProof 1 n -> LeqProof 1 (n+n) +dblPosIsPos x = leqAdd x Proxy + +addIsLeqLeft1 :: forall n n' m . LeqProof (n + n') m -> LeqProof n m +addIsLeqLeft1 p = + case plusMinusCancel n n' of + Refl -> leqSub p le + where n :: Proxy n + n = Proxy + n' :: Proxy n' + n' = Proxy + le :: LeqProof n' (n + n') + le = addPrefixIsLeq n n' + +{-# INLINE withAddPrefixLeq #-} +withAddPrefixLeq :: NatRepr n -> NatRepr m -> ((m <= n + m) => a) -> a +withAddPrefixLeq n m = withLeqProof (addPrefixIsLeq n m) + +withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a +withAddLeq n m f = withLeqProof (addIsLeq n m) (f (addNat n m)) + +natForEach' :: forall l h a + . NatRepr l + -> NatRepr h + -> (forall n. LeqProof l n -> LeqProof n h -> NatRepr n -> a) + -> [a] +natForEach' l h f + | Just LeqProof <- testLeq l h = + let f' :: forall n. LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a + f' = \lp hp -> f (addIsLeqLeft1 lp) hp + in f LeqProof LeqProof l : natForEach' (incNat l) h f' + | otherwise = [] + +-- | Apply a function to each element in a range; return the list of values +-- obtained. +natForEach :: forall l h a + . NatRepr l + -> NatRepr h + -> (forall n. (l <= n, n <= h) => NatRepr n -> a) + -> [a] +natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f) + +-- | Recursor for natural numbeers. +natRec :: forall m f + . NatRepr m + -> f 0 + -> (forall n. NatRepr n -> f n -> f (n + 1)) + -> f m +natRec n f0 ih = go n + where + go :: forall n'. NatRepr n' -> f n' + go n' = case isZeroNat n' of + ZeroNat -> f0 + NonZeroNat -> let n'' = predNat n' in ih n'' (go n'') diff --git a/src/Data/Parameterized/Nonce.hs b/src/Data/Parameterized/Nonce.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Nonce.hs @@ -0,0 +1,158 @@ +{-| +Copyright : (c) Galois, Inc 2014-2016 +Maintainer : Joe Hendrix + +This module provides a simple generator of new indexes in the ST monad. +It is predictable and not intended for cryptographic purposes. + +This module also provides a global nonce generator that will generate +2^64 nonces before looping. + +NOTE: The 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply +compare the generated nonce values and then assert to the compiler +(via 'unsafeCoerce') that the types ascribed to the nonces are equal +if their values are equal. +-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE Trustworthy #-} +#if MIN_VERSION_base(4,9,0) +{-# LANGUAGE TypeInType #-} +#endif +module Data.Parameterized.Nonce + ( -- * NonceGenerator + NonceGenerator + , freshNonce + , Nonce + , indexValue + -- * Accessing a nonce generator + , newSTNonceGenerator + , newIONonceGenerator + , withIONonceGenerator + , withSTNonceGenerator + , withGlobalSTNonceGenerator + , GlobalNonceGenerator + , globalNonceGenerator + ) where + +import Control.Monad.ST +import Data.Hashable +import Data.IORef +import Data.STRef +import Data.Typeable +import Data.Word +import Unsafe.Coerce +import System.IO.Unsafe (unsafePerformIO) + +import Data.Parameterized.Classes +import Data.Parameterized.Some + +#if MIN_VERSION_base(4,9,0) +import Data.Kind +#endif + +-- | Provides a monadic action for getting fresh typed names. +-- +-- The first type parameter @m@ is the monad used for generating names, and +-- the second parameter @s@ is used for the counter. +data NonceGenerator (m :: * -> *) (s :: *) = NonceGenerator { +#if MIN_VERSION_base(4,9,0) +-- We have to make the k explicit in GHC 8.0 to avoid a warning. + freshNonce :: forall k (tp :: k) . m (Nonce s tp) +#else + freshNonce :: forall (tp :: k) . m (Nonce s tp) +#endif + } + +-- | Create a new counter. +withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r +withGlobalSTNonceGenerator f = runST $ do + r <- newSTRef (toEnum 0) + f $! NonceGenerator { + freshNonce = do + i <- readSTRef r + writeSTRef r $! succ i + return $! Nonce i + } + +-- | Create a new nonce generator in the ST monad. +newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t))) +newSTNonceGenerator = g <$> newSTRef (toEnum 0) + where g r = Some $! + NonceGenerator { + freshNonce = do + i <- readSTRef r + writeSTRef r $! succ i + return $! Nonce i + } + +-- | Create a new nonce generator in the ST monad. +newIONonceGenerator :: IO (Some (NonceGenerator IO)) +newIONonceGenerator = g <$> newIORef (toEnum 0) + where g r = Some $! + NonceGenerator { + freshNonce = do + i <- readIORef r + writeIORef r $! succ i + return $! Nonce i + } + +-- | Run a ST computation with a new nonce generator in the ST monad. +withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> (ST t) r) -> ST t r +withSTNonceGenerator f = do + Some r <- newSTNonceGenerator + f r + +-- | Create a new nonce generator in the IO monad. +withIONonceGenerator :: (forall s . NonceGenerator IO s -> IO r) -> IO r +withIONonceGenerator f = do + Some r <- newIONonceGenerator + f r + +-- | An index generated by the counter. +newtype Nonce (s :: *) (tp :: k) = Nonce { indexValue :: Word64 } + deriving (Eq, Ord, Hashable, Show) + +-- Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce +-- from casting the types of nonces, which it would otherwise be able to do +-- because tp is a phantom type parameter. This partially helps to protect +-- the nonce abstraction. +type role Nonce nominal nominal + +instance TestEquality (Nonce s) where + testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl) + | otherwise = Nothing + +instance OrdF (Nonce s) where + compareF x y = + case compare (indexValue x) (indexValue y) of + LT -> LTF + EQ -> unsafeCoerce EQF + GT -> GTF + +instance HashableF (Nonce s) where + hashWithSaltF s (Nonce x) = hashWithSalt s x + +instance ShowF (Nonce s) + +------------------------------------------------------------------------ +-- GlobalNonceGenerator + +data GlobalNonceGenerator + +globalNonceIORef :: IORef Word64 +globalNonceIORef = unsafePerformIO (newIORef 0) +{-# NOINLINE globalNonceIORef #-} + +-- | A nonce generator that uses a globally-defined counter. +globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator +globalNonceGenerator = + NonceGenerator + { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n)) + } diff --git a/src/Data/Parameterized/Nonce/Transformers.hs b/src/Data/Parameterized/Nonce/Transformers.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Nonce/Transformers.hs @@ -0,0 +1,70 @@ +{-| +Copyright : (c) Galois, Inc 2014-2016 +Maintainer : Eddy Westbrook + +This module provides a typeclass and monad transformers for generating +nonces. +-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module Data.Parameterized.Nonce.Transformers + ( MonadNonce(..) + , NonceT(..) + , NonceST + , NonceIO + , getNonceSTGen + , runNonceST + , runNonceIO + , module Data.Parameterized.Nonce + ) where + +import Control.Monad.Reader +import Control.Monad.ST +import Control.Monad.State + +import Data.Parameterized.Nonce + + +-- | A 'MonadNonce' is a monad that can generate fresh 'Nonce's in a given set +-- (where we view the phantom type parameter of 'Nonce' as a designator of the +-- set that the 'Nonce' came from). +class Monad m => MonadNonce m where + type NonceSet m :: * + freshNonceM :: forall (tp :: k) . m (Nonce (NonceSet m) tp) + +-- | This transformer adds a nonce generator to a given monad. +newtype NonceT s m a = + NonceT { runNonceT :: ReaderT (NonceGenerator m s) m a } + deriving (Functor, Applicative, Monad) + +instance MonadTrans (NonceT s) where + lift m = NonceT $ lift m + +instance Monad m => MonadNonce (NonceT s m) where + type NonceSet (NonceT s m) = s + freshNonceM = NonceT $ lift . freshNonce =<< ask + +instance MonadNonce m => MonadNonce (StateT s m) where + type NonceSet (StateT s m) = NonceSet m + freshNonceM = lift $ freshNonceM + +-- | Helper type to build a 'MonadNonce' from the 'ST' monad. +type NonceST t s = NonceT s (ST t) + +-- | Helper type to build a 'MonadNonce' from the 'IO' monad. +type NonceIO s = NonceT s IO + +-- | Return the actual 'NonceGenerator' used in an 'ST' computation. +getNonceSTGen :: NonceST t s (NonceGenerator (ST t) s) +getNonceSTGen = NonceT ask + +-- | Run a 'NonceST' computation with a fresh 'NonceGenerator'. +runNonceST :: (forall t s. NonceST t s a) -> a +runNonceST m = runST $ withSTNonceGenerator $ runReaderT $ runNonceT m + +-- | Run a 'NonceIO' computation with a fresh 'NonceGenerator' inside 'IO'. +runNonceIO :: (forall s. NonceIO s a) -> IO a +runNonceIO m = withIONonceGenerator $ runReaderT $ runNonceT m diff --git a/src/Data/Parameterized/Nonce/Unsafe.hs b/src/Data/Parameterized/Nonce/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Nonce/Unsafe.hs @@ -0,0 +1,107 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.NonceGenerator +-- Description : A counter in the ST monad. +-- Copyright : (c) Galois, Inc 2014 +-- Maintainer : Joe Hendrix +-- Stability : provisional +-- +-- This module provides a simple generator of new indexes in the ST monad. +-- It is predictable and not intended for cryptographic purposes. +-- +-- NOTE: the 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply +-- compare the generated nonce values and then assert to the compiler +-- (via 'unsafeCoerce') that the types ascribed to the nonces are equal +-- if their values are equal. This is only OK because of the discipline +-- by which nonces should be used: they should only be generated from +-- a 'NonceGenerator' (i.e., should not be built directly), and nonces from +-- different generators must never be compared! Arranging to compare +-- Nonces from different origins would allow users to build 'unsafeCoerce' +-- via the 'testEquality' function. +-- +-- A somewhat safer API would be to brand the generated Nonces with the +-- state type variable of the NonceGenerator whence they came, and to only +-- provide NonceGenerators via a Rank-2 continuation-passing API, similar to +-- 'runST'. This would (via a meta-argument involving parametricity) +-- help to prevent nonces of different origin from being compared. +-- However, this would force us to push the 'ST' type brand into a significant +-- number of other structures and APIs. +-- +-- Another alternative would be to use 'unsafePerformIO' magic to make +-- a global nonce generator, and make that the only way to generate nonces. +-- It is not clear that this is actually an improvement from a type safety +-- point of view, but an argument could be made. +-- +-- For now, be careful using Nonces, and ensure that you do not mix +-- Nonces from different NonceGenerators. +------------------------------------------------------------------------ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE Unsafe #-} +module Data.Parameterized.Nonce.Unsafe + ( NonceGenerator + , newNonceGenerator + , freshNonce + , atLimit + , Nonce + , indexValue + ) where + +import Control.Monad.ST +import Data.Hashable +import Data.STRef +import Data.Word +import Unsafe.Coerce + +import Data.Parameterized.Classes + +-- | A simple type that for getting fresh indices in the 'ST' monad. +-- The type parameter @s@ is used for the 'ST' monad parameter. +newtype NonceGenerator s = NonceGenerator (STRef s Word64) + +-- | Create a new counter. +newNonceGenerator :: ST s (NonceGenerator s) +newNonceGenerator = NonceGenerator `fmap` newSTRef (toEnum 0) + +-- | An index generated by the counter. +newtype Nonce (tp :: k) = Nonce { indexValue :: Word64 } + deriving (Eq, Ord, Hashable, Show) + +-- Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce +-- from casting the types of nonces, which it would otherwise be able to do +-- because tp is a phantom type parameter. This partially helps to protect +-- the nonce abstraction. +type role Nonce nominal + +instance TestEquality Nonce where + testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl) + | otherwise = Nothing + +instance OrdF Nonce where + compareF x y = + case compare (indexValue x) (indexValue y) of + LT -> LTF + EQ -> unsafeCoerce EQF + GT -> GTF + +instance HashableF Nonce where + hashWithSaltF s (Nonce x) = hashWithSalt s x + +instance ShowF Nonce + +{-# INLINE freshNonce #-} +-- | Get a fresh index and increment the counter. +freshNonce :: NonceGenerator s -> ST s (Nonce tp) +freshNonce (NonceGenerator r) = do + i <- readSTRef r + writeSTRef r $! succ i + return (Nonce i) + +-- | Return true if counter has reached the limit, and can't be +-- incremented without risk of error. +atLimit :: NonceGenerator s -> ST s Bool +atLimit (NonceGenerator r) = do + i <- readSTRef r + return (i == maxBound) diff --git a/src/Data/Parameterized/Pair.hs b/src/Data/Parameterized/Pair.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Pair.hs @@ -0,0 +1,51 @@ +{-| +Copyright : (c) Galois, Inc 2017 + +This module defines a 2-tuple where both elements are parameterized over the +same existentially quantified parameter. + +-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module Data.Parameterized.Pair + ( Pair(..) + , fstPair + , sndPair + , viewPair + ) where + +import Data.Parameterized.Classes +import Data.Parameterized.Some +import Data.Parameterized.TraversableF + +-- | Like a 2-tuple, but with an existentially quantified parameter that both of +-- the elements share. +data Pair (a :: k -> *) (b :: k -> *) where + Pair :: !(a tp) -> !(b tp) -> Pair a b + +instance (TestEquality a, EqF b) => Eq (Pair a b) where + Pair xa xb == Pair ya yb = + case testEquality xa ya of + Just Refl -> eqF xb yb + Nothing -> False + +instance FunctorF (Pair a) where + fmapF f (Pair x y) = Pair x (f y) + +instance FoldableF (Pair a) where + foldMapF f (Pair _ y) = f y + foldrF f z (Pair _ y) = f y z + +-- | Extract the first element of a pair. +fstPair :: Pair a b -> Some a +fstPair (Pair x _) = Some x + +-- | Extract the second element of a pair. +sndPair :: Pair a b -> Some b +sndPair (Pair _ y) = Some y + +-- | Project out of Pair. +viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c +viewPair f (Pair x y) = f x y diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Some.hs @@ -0,0 +1,59 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.Some +-- Copyright : (c) Galois, Inc 2014 +-- Maintainer : Joe Hendrix +-- +-- This module provides 'Some', a GADT that hides a type parameter. +------------------------------------------------------------------------ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module Data.Parameterized.Some + ( Some(..) + , viewSome + , mapSome + , traverseSome + , traverseSome_ + ) where + +import Data.Hashable +import Data.Parameterized.Classes + + +data Some (f:: k -> *) = forall x . Some (f x) + +instance TestEquality f => Eq (Some f) where + Some x == Some y = isJust (testEquality x y) + +instance OrdF f => Ord (Some f) where + compare (Some x) (Some y) = toOrdering (compareF x y) + +instance HashableF f => Hashable (Some f) where + hashWithSalt s (Some x) = hashWithSaltF s x + hash (Some x) = hashF x + +instance ShowF f => Show (Some f) where + show (Some x) = showF x + +-- | Project out of Some. +viewSome :: (forall tp . f tp -> r) -> Some f -> r +viewSome f (Some x) = f x + +-- | Apply function to inner value. +mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g +mapSome f (Some x) = Some $! f x + +{-# INLINE traverseSome #-} +-- | Modify the inner value. +traverseSome :: Functor m + => (forall tp . f tp -> m (g tp)) + -> Some f + -> m (Some g) +traverseSome f (Some x) = Some `fmap` f x + +{-# INLINE traverseSome_ #-} +-- | Modify the inner value. +traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m () +traverseSome_ f (Some x) = (\_ -> ()) `fmap` f x diff --git a/src/Data/Parameterized/SymbolRepr.hs b/src/Data/Parameterized/SymbolRepr.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/SymbolRepr.hs @@ -0,0 +1,106 @@ +{-| +Copyright : (c) Galois, Inc 2014-2015 +Maintainer : Joe Hendrix + +This defines a type family 'SymbolRepr' for representing a type-level string +(AKA symbol) at runtime. This can be used to branch on a type-level value. + +The 'TestEquality' and 'OrdF' instances for 'SymbolRepr' are implemented using +'unsafeCoerce'. This should be typesafe because we maintain the invariant +that the string value contained in a SymbolRepr value matches its static type. + +At the type level, symbols have very few operations, so SymbolRepr +correspondingly has very few functions that manipulate them. +-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE Trustworthy #-} +module Data.Parameterized.SymbolRepr + ( -- * SymbolRepr + SymbolRepr + , symbolRepr + , knownSymbol + , someSymbol + -- * Re-exports + , type GHC.Symbol + , GHC.KnownSymbol + ) where + +import GHC.TypeLits as GHC +import Unsafe.Coerce (unsafeCoerce) + +import Data.Hashable +import Data.Proxy +import qualified Data.Text as Text + +import Data.Parameterized.Classes +import Data.Parameterized.Some + +-- | A runtime representation of a GHC type-level symbol. +newtype SymbolRepr (nm::GHC.Symbol) + = SymbolRepr { symbolRepr :: Text.Text + -- ^ The underlying text representation of the symbol + } +-- INVARIANT: The contained runtime text value matches the value +-- of the type level symbol. The SymbolRepr constructor +-- is not exported so we can maintain this invariant in this +-- module. + +-- | Generate a symbol representative at runtime. The type-level +-- symbol will be abstract, as it is hidden by the 'Some' constructor. +someSymbol :: Text.Text -> Some SymbolRepr +someSymbol nm = Some (SymbolRepr nm) + +-- | Generate a value representative for the type level symbol. +knownSymbol :: GHC.KnownSymbol s => SymbolRepr s +knownSymbol = go Proxy + where go :: GHC.KnownSymbol s => Proxy s -> SymbolRepr s + go p = SymbolRepr $! packSymbol (GHC.symbolVal p) + + -- NOTE here we explicitly test that unpacking the packed text value + -- gives the desired string. This is to avoid pathological corner cases + -- involving string values that have no text representation. + packSymbol str + | Text.unpack txt == str = txt + | otherwise = error $ "Unrepresentable symbol! "++ str + where txt = Text.pack str + +instance (GHC.KnownSymbol s) => KnownRepr SymbolRepr s where + knownRepr = knownSymbol + +instance TestEquality SymbolRepr where + testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y) + | x == y = Just (unsafeCoerce (Refl :: x :~: x)) + | otherwise = Nothing +instance OrdF SymbolRepr where + compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y) + | x < y = LTF + | x == y = unsafeCoerce (EQF :: OrderingF x x) + | otherwise = GTF + +-- These instances are trivial by the invariant +-- that the contained string matches the type-level +-- symbol +instance Eq (SymbolRepr x) where + _ == _ = True +instance Ord (SymbolRepr x) where + compare _ _ = EQ + +instance HashableF SymbolRepr where + hashWithSaltF = hashWithSalt +instance Hashable (SymbolRepr nm) where + hashWithSalt s (SymbolRepr nm) = hashWithSalt s nm + +instance Show (SymbolRepr nm) where + show (SymbolRepr nm) = Text.unpack nm + +instance ShowF SymbolRepr diff --git a/src/Data/Parameterized/TH/GADT.hs b/src/Data/Parameterized/TH/GADT.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/TH/GADT.hs @@ -0,0 +1,443 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.TH.GADT +-- Copyright : (c) Galois, Inc 2013-2014 +-- Maintainer : Joe Hendrix +-- +-- This module declares template Haskell primitives so that it is easier +-- to work with GADTs that have many constructors. +------------------------------------------------------------------------ +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE EmptyCase #-} +module Data.Parameterized.TH.GADT + ( structuralEquality + , structuralTypeEquality + , structuralTypeOrd + , structuralTraversal + , structuralShowsPrec + , structuralHash + , PolyEq(..) + -- * Template haskell utilities that may be useful in other contexts. + , DataD + , lookupDataType' + , asTypeCon + , conPat + , TypePat(..) + , dataParamTypes + , assocTypePats + ) where + +import Control.Monad +import Data.Hashable (hashWithSalt) +import Data.Maybe +import Data.Set (Set) +import qualified Data.Set as Set +import Language.Haskell.TH +import Language.Haskell.TH.Datatype + + +import Data.Parameterized.Classes + +------------------------------------------------------------------------ +-- Template Haskell utilities + +type DataD = DatatypeInfo + +lookupDataType' :: Name -> Q DatatypeInfo +lookupDataType' = reifyDatatype + +-- | Given a constructor and string, this generates a pattern for matching +-- the expression, and the names of variables bound by pattern in order +-- they appear in constructor. +conPat :: + ConstructorInfo {- ^ constructor information -} -> + String {- ^ generated name prefix -} -> + Q (Pat, [Name]) {- ^ pattern and bound names -} +conPat con pre = do + nms <- newNames pre (length (constructorFields con)) + return (ConP (constructorName con) (VarP <$> nms), nms) + + +-- | Return an expression corresponding to the constructor. +-- Note that this will have the type of a function expecting +-- the argumetns given. +conExpr :: ConstructorInfo -> Exp +conExpr = ConE . constructorName + +------------------------------------------------------------------------ +-- TypePat + +data TypePat + = TypeApp TypePat TypePat -- ^ The application of a type. + | AnyType -- ^ Match any type. + | DataArg Int -- ^ Match the ith argument of the data type we are traversing. + | ConType TypeQ -- ^ Match a ground type. + +matchTypePat :: [Type] -> TypePat -> Type -> Q Bool +matchTypePat d (TypeApp p q) (AppT x y) = do + r <- matchTypePat d p x + case r of + True -> matchTypePat d q y + False -> return False +matchTypePat _ AnyType _ = return True +matchTypePat tps (DataArg i) tp + | i < 0 || i > length tps = error $ "Illegal type pattern index " ++ show i + | otherwise = do + return $ stripSigT (tps !! i) == tp + where + -- th-abstraction can annotate type parameters with their kinds, + -- we ignore these for matching + stripSigT (SigT t _) = t + stripSigT t = t +matchTypePat _ (ConType tpq) tp = do + tp' <- tpq + return (tp' == tp) +matchTypePat _ _ _ = return False + +dataParamTypes :: DatatypeInfo -> [Type] +dataParamTypes = datatypeVars + +-- | Find value associated with first pattern that matches given pat if any. +assocTypePats :: [Type] -> [(TypePat,v)] -> Type -> Q (Maybe v) +assocTypePats _ [] _ = return Nothing +assocTypePats dTypes ((p,v):pats) tp = do + r <- matchTypePat dTypes p tp + case r of + True -> return (Just v) + False -> assocTypePats dTypes pats tp + +------------------------------------------------------------------------ +-- Contructor cases + +typeVars :: TypeSubstitution a => a -> Set Name +typeVars = Set.fromList . freeVariables + + +-- | @declareStructuralEquality@ declares a structural equality predicate. +structuralEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ +structuralEquality tpq pats = + [| \x y -> isJust ($(structuralTypeEquality tpq pats) x y) |] + +joinEqMaybe :: Name -> Name -> ExpQ -> ExpQ +joinEqMaybe x y r = do + [| if $(varE x) == $(varE y) then $(r) else Nothing |] + +joinTestEquality :: ExpQ -> Name -> Name -> ExpQ -> ExpQ +joinTestEquality f x y r = + [| case $(f) $(varE x) $(varE y) of + Nothing -> Nothing + Just Refl -> $(r) + |] + +matchEqArguments :: [Type] + -- ^ Types bound by data arguments. + -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments + -> Name + -- ^ Name of constructor. + -> Set Name + -> [Type] + -> [Name] + -> [Name] + -> ExpQ +matchEqArguments dTypes pats cnm bnd (tp:tpl) (x:xl) (y:yl) = do + doesMatch <- assocTypePats dTypes pats tp + case doesMatch of + Just q -> do + let bnd' = + case tp of + AppT _ (VarT nm) -> Set.insert nm bnd + _ -> bnd + joinTestEquality q x y (matchEqArguments dTypes pats cnm bnd' tpl xl yl) + Nothing | typeVars tp `Set.isSubsetOf` bnd -> do + joinEqMaybe x y (matchEqArguments dTypes pats cnm bnd tpl xl yl) + Nothing -> do + fail $ "Unsupported argument type " ++ show tp + ++ " in " ++ show (ppr cnm) ++ "." +matchEqArguments _ _ _ _ [] [] [] = [| Just Refl |] +matchEqArguments _ _ _ _ [] _ _ = error "Unexpected end of types." +matchEqArguments _ _ _ _ _ [] _ = error "Unexpected end of names." +matchEqArguments _ _ _ _ _ _ [] = error "Unexpected end of names." + +mkSimpleEqF :: [Type] -- ^ Data declaration types + -> Set Name + -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments + -> ConstructorInfo + -> [Name] + -> ExpQ + -> Bool -- ^ wildcard case required + -> ExpQ +mkSimpleEqF dTypes bnd pats con xv yQ multipleCases = do + -- Get argument types for constructor. + let nm = constructorName con + (yp,yv) <- conPat con "y" + let rv = matchEqArguments dTypes pats nm bnd (constructorFields con) xv yv + caseE yQ $ match (pure yp) (normalB rv) [] + : [ match wildP (normalB [| Nothing |]) [] | multipleCases ] + +-- | Match equational form. +mkEqF :: DatatypeInfo -- ^ Data declaration. + -> [(TypePat,ExpQ)] + -> ConstructorInfo + -> [Name] + -> ExpQ + -> Bool -- ^ wildcard case required + -> ExpQ +mkEqF d pats con = + let dVars = datatypeVars d + bnd | null dVars = Set.empty + | otherwise = typeVars (init dVars) + in mkSimpleEqF dVars bnd pats con + +-- | @structuralTypeEquality f@ returns a function with the type: +-- forall x y . f x -> f y -> Maybe (x :~: y) +structuralTypeEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ +structuralTypeEquality tpq pats = do + d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq + + let multipleCons = not (null (drop 1 (datatypeCons d))) + trueEqs yQ = [ do (xp,xv) <- conPat con "x" + match (pure xp) (normalB (mkEqF d pats con xv yQ multipleCons)) [] + | con <- datatypeCons d + ] + + if null (datatypeCons d) + then [| \x -> case x of {} |] + else [| \x y -> $(caseE [| x |] (trueEqs [| y |])) |] + +-- | @structuralTypeEquality f@ returns a function with the type: +-- forall x y . f x -> f y -> OrderingF x y +-- +-- This implementation avoids matching on both the first and second +-- parameters in a simple case expression in order to avoid stressing +-- GHC's coverage checker. In the case that the first and second parameters +-- have unique constructors, a simple numeric comparison is done to +-- compute the result. +structuralTypeOrd :: + TypeQ -> + [(TypePat,ExpQ)] {- ^ List of type patterns to match. -} -> + ExpQ +structuralTypeOrd tpq l = do + d <- reifyDatatype =<< asTypeCon "structuralTypeEquality" =<< tpq + + let withNumber :: ExpQ -> (Maybe ExpQ -> ExpQ) -> ExpQ + withNumber yQ k + | null (drop 1 (datatypeCons d)) = k Nothing + | otherwise = [| let yn :: Int + yn = $(caseE yQ (constructorNumberMatches (datatypeCons d))) + in $(k (Just [| yn |])) |] + + if null (datatypeCons d) + then [| \x -> case x of {} |] + else [| \x y -> $(withNumber [|y|] $ \mbYn -> caseE [| x |] (outerOrdMatches d [|y|] mbYn)) |] + where + constructorNumberMatches :: [ConstructorInfo] -> [MatchQ] + constructorNumberMatches cons = + [ match (recP (constructorName con) []) + (normalB (litE (integerL i))) + [] + | (i,con) <- zip [0..] cons ] + + outerOrdMatches :: DatatypeInfo -> ExpQ -> Maybe ExpQ -> [MatchQ] + outerOrdMatches d yExp mbYn = + [ do (pat,xv) <- conPat con "x" + match (pure pat) + (normalB (do xs <- mkOrdF d l con i mbYn xv + caseE yExp xs)) + [] + | (i,con) <- zip [0..] (datatypeCons d) ] + +-- | Generate a list of fresh names using the base name +-- numbered 1 to n to make them useful in conjunction with +-- @-dsuppress-unqiues@. +newNames :: + String {- ^ base name -} -> + Int {- ^ quantity -} -> + Q [Name] {- ^ list of names: base1, base2.. -} +newNames base n = traverse (\i -> newName (base ++ show i)) [1..n] + + +joinCompareF :: ExpQ -> Name -> Name -> ExpQ -> ExpQ +joinCompareF f x y r = do + [| case $(f) $(varE x) $(varE y) of + LTF -> LTF + GTF -> GTF + EQF -> $(r) + |] + +-- | Compare two variables and use following comparison if they are different. +-- +-- This returns an 'OrdF' instance. +joinCompareToOrdF :: Name -> Name -> ExpQ -> ExpQ +joinCompareToOrdF x y r = + [| case compare $(varE x) $(varE y) of + LT -> LTF + GT -> GTF + EQ -> $(r) + |] + + -- Match expression with given type to variables +matchOrdArguments :: [Type] + -- ^ Types bound by data arguments + -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments + -> Name + -- ^ Name of constructor. + -> Set Name + -- ^ Names bound in data declaration + -> [Type] + -- ^ Types for constructors + -> [Name] + -- ^ Variables bound in first pattern + -> [Name] + -- ^ Variables bound in second pattern + -> ExpQ +matchOrdArguments dTypes pats cnm bnd (tp : tpl) (x:xl) (y:yl) = do + doesMatch <- assocTypePats dTypes pats tp + case doesMatch of + Just f -> do + let bnd' = case tp of + AppT _ (VarT nm) -> Set.insert nm bnd + _ -> bnd + joinCompareF f x y (matchOrdArguments dTypes pats cnm bnd' tpl xl yl) + Nothing | typeVars tp `Set.isSubsetOf` bnd -> do + joinCompareToOrdF x y (matchOrdArguments dTypes pats cnm bnd tpl xl yl) + Nothing -> + fail $ "Unsupported argument type " ++ show (ppr tp) + ++ " in " ++ show (ppr cnm) ++ "." +matchOrdArguments _ _ _ _ [] [] [] = [| EQF |] +matchOrdArguments _ _ _ _ [] _ _ = error "Unexpected end of types." +matchOrdArguments _ _ _ _ _ [] _ = error "Unexpected end of names." +matchOrdArguments _ _ _ _ _ _ [] = error "Unexpected end of names." + +mkSimpleOrdF :: [Type] -- ^ Data declaration types + -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments + -> ConstructorInfo -- ^ Information about the second constructor + -> Integer -- ^ First constructor's index + -> Maybe ExpQ -- ^ Optional second constructor's index + -> [Name] -- ^ Name from first pattern + -> Q [MatchQ] +mkSimpleOrdF dTypes pats con xnum mbYn xv = do + (yp,yv) <- conPat con "y" + let rv = matchOrdArguments dTypes pats (constructorName con) Set.empty (constructorFields con) xv yv + -- Return match expression + return $ match (pure yp) (normalB rv) [] + : case mbYn of + Nothing -> [] + Just yn -> [match wildP (normalB [| if xnum < $yn then LTF else GTF |]) []] + +-- | Match equational form. +mkOrdF :: DatatypeInfo -- ^ Data declaration. + -> [(TypePat,ExpQ)] -- ^ Patterns for matching arguments + -> ConstructorInfo + -> Integer + -> Maybe ExpQ -- ^ optional right constructr index + -> [Name] + -> Q [MatchQ] +mkOrdF d pats = mkSimpleOrdF (datatypeVars d) pats + +-- | Find the first recurseArg f var tp@ applies @f@ to @var@ where @var@ has type @tp@. +recurseArg :: (Type -> Q (Maybe ExpQ)) + -> ExpQ -- ^ Function to apply + -> ExpQ + -> Type + -> Q (Maybe Exp) +recurseArg m f v tp = do + mr <- m tp + case mr of + Just g -> Just <$> [| $(g) $(f) $(v) |] + Nothing -> + case tp of + AppT (ConT _) (AppT (VarT _) _) -> Just <$> [| traverse $(f) $(v) |] + AppT (VarT _) _ -> Just <$> [| $(f) $(v) |] + _ -> return Nothing + +-- | @traverseAppMatch f c@ builds a case statement that matches a term with +-- the constructor @c@ and applies @f@ to each argument. +traverseAppMatch :: (Type -> Q (Maybe ExpQ)) -- Pattern match function + -> ExpQ -- ^ Function to apply to each argument recursively. + -> ConstructorInfo -- ^ Constructor to match. + -> MatchQ -- ^ Match expression that +traverseAppMatch pats fv c0 = do + (pat,patArgs) <- conPat c0 "p" + exprs <- zipWithM (recurseArg pats fv) (varE <$> patArgs) (constructorFields c0) + + let mkRes :: ExpQ -> [(Name, Maybe Exp)] -> ExpQ + mkRes e [] = e + mkRes e ((v,Nothing):r) = + mkRes (appE e (varE v)) r + mkRes e ((_,Just{}):r) = do + v <- newName "r" + lamE [varP v] (mkRes (appE e (varE v)) r) + + -- Apply the remaining argument to the expression in list. + let applyRest :: ExpQ -> [Exp] -> ExpQ + applyRest e [] = e + applyRest e (a:r) = applyRest [| $(e) <*> $(pure a) |] r + + -- Apply the first argument to the list + let applyFirst :: ExpQ -> [Exp] -> ExpQ + applyFirst e [] = [| pure $(e) |] + applyFirst e (a:r) = applyRest [| $(e) <$> $(pure a) |] r + + let pargs = patArgs `zip` exprs + let rhs = applyFirst (mkRes (pure (conExpr c0)) pargs) (catMaybes exprs) + match (pure pat) (normalB rhs) [] + +-- | @structuralTraversal tp@ generates a function that applies +-- a traversal @f@ to the subterms with free variables in @tp@. +structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ +structuralTraversal tpq pats0 = do + d <- reifyDatatype =<< asTypeCon "structuralTraversal" =<< tpq + f <- newName "f" + a <- newName "a" + lamE [varP f, varP a] $ + caseE (varE a) + (traverseAppMatch (assocTypePats (datatypeVars d) pats0) (varE f) <$> datatypeCons d) + +asTypeCon :: Monad m => String -> Type -> m Name +asTypeCon _ (ConT nm) = return nm +asTypeCon fn _ = fail $ fn ++ " expected type constructor." + +-- | @structuralHash tp@ generates a function with the type +-- @Int -> tp -> Int@ that hashes type. +structuralHash :: TypeQ -> ExpQ +structuralHash tpq = do + d <- reifyDatatype =<< asTypeCon "structuralHash" =<< tpq + s <- newName "s" + a <- newName "a" + lamE [varP s, varP a] $ + caseE (varE a) (zipWith (matchHashCtor (varE s)) [0..] (datatypeCons d)) + +matchHashCtor :: ExpQ -> Integer -> ConstructorInfo -> MatchQ +matchHashCtor s0 i c = do + (pat,vars) <- conPat c "x" + let args = [| $(litE (IntegerL i)) :: Int |] : (varE <$> vars) + let go s e = [| hashWithSalt $(s) $(e) |] + let rhs = foldl go s0 args + match (pure pat) (normalB rhs) [] + +-- | @structuralShow tp@ generates a function with the type +-- @tp -> ShowS@ that shows the constructor. +structuralShowsPrec :: TypeQ -> ExpQ +structuralShowsPrec tpq = do + d <- reifyDatatype =<< asTypeCon "structuralShowPrec" =<< tpq + p <- newName "_p" + a <- newName "a" + lamE [varP p, varP a] $ + caseE (varE a) (matchShowCtor (varE p) <$> datatypeCons d) + +showCon :: ExpQ -> Name -> Int -> MatchQ +showCon p nm n = do + vars <- newNames "x" n + let pat = ConP nm (VarP <$> vars) + let go s e = [| $(s) . showChar ' ' . showsPrec 10 $(varE e) |] + let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |] + let rhs | null vars = ctor + | otherwise = [| showParen ($(p) >= 10) $(foldl go ctor vars) |] + match (pure pat) (normalB rhs) [] + +matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ +matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con)) diff --git a/src/Data/Parameterized/TraversableF.hs b/src/Data/Parameterized/TraversableF.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/TraversableF.hs @@ -0,0 +1,117 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.TraversableF +-- Copyright : (c) Galois, Inc 2014-2015 +-- Maintainer : Joe Hendrix +-- +-- This module declares classes for working with structures that accept +-- a single parametric type parameter. +------------------------------------------------------------------------ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Trustworthy #-} +module Data.Parameterized.TraversableF + ( FunctorF(..) + , FoldableF(..) + , TraversableF(..) + , traverseF_ + , fmapFDefault + , foldMapFDefault + , allF + , anyF + ) where + +import Control.Applicative +import Control.Monad.Identity +import Data.Coerce +import Data.Functor.Const +import Data.Monoid +import GHC.Exts (build) + +-- | A parameterized type that is a function on all instances. +class FunctorF m where + fmapF :: (forall x . f x -> g x) -> m f -> m g + +instance FunctorF (Const x) where + fmapF _ = coerce + +------------------------------------------------------------------------ +-- FoldableF + +-- | This is a coercision used to avoid overhead associated +-- with function composition. +(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) +(#.) _f = coerce + +-- | This is a generalization of the @Foldable@ class to +-- structures over parameterized terms. +class FoldableF (t :: (k -> *) -> *) where + {-# MINIMAL foldMapF | foldrF #-} + + -- | Map each element of the structure to a monoid, + -- and combine the results. + foldMapF :: Monoid m => (forall s . e s -> m) -> t e -> m + foldMapF f = foldrF (mappend . f) mempty + + -- | Right-associative fold of a structure. + foldrF :: (forall s . e s -> b -> b) -> b -> t e -> b + foldrF f z t = appEndo (foldMapF (Endo #. f) t) z + + -- | Left-associative fold of a structure. + foldlF :: (forall s . b -> e s -> b) -> b -> t e -> b + foldlF f z t = appEndo (getDual (foldMapF (\e -> Dual (Endo (\r -> f r e))) t)) z + + -- | Right-associative fold of a structure, + -- but with strict application of the operator. + foldrF' :: (forall s . e s -> b -> b) -> b -> t e -> b + foldrF' f0 z0 xs = foldlF (f' f0) id xs z0 + where f' f k x z = k $! f x z + + -- | Left-associative fold of a parameterized structure + -- with a strict accumulator. + foldlF' :: (forall s . b -> e s -> b) -> b -> t e -> b + foldlF' f0 z0 xs = foldrF (f' f0) id xs z0 + where f' f x k z = k $! f z x + + -- | Convert structure to list. + toListF :: (forall tp . f tp -> a) -> t f -> [a] + toListF f t = build (\c n -> foldrF (\e v -> c (f e) v) n t) + +-- | Return 'True' if all values satisfy predicate. +allF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool +allF p = getAll #. foldMapF (All #. p) + +-- | Return 'True' if any values satisfy predicate. +anyF :: FoldableF t => (forall tp . f tp -> Bool) -> t f -> Bool +anyF p = getAny #. foldMapF (Any #. p) + +instance FoldableF (Const x) where + foldMapF _ _ = mempty + +------------------------------------------------------------------------ +-- TraversableF + +class (FunctorF t, FoldableF t) => TraversableF t where + traverseF :: Applicative m + => (forall s . e s -> m (f s)) + -> t e + -> m (t f) + +instance TraversableF (Const x) where + traverseF _ (Const x) = pure (Const x) + +-- | This function may be used as a value for `fmapF` in a `FunctorF` +-- instance. +fmapFDefault :: TraversableF t => (forall s . e s -> f s) -> t e -> t f +fmapFDefault f = runIdentity #. traverseF (Identity #. f) +{-# INLINE fmapFDefault #-} + +-- | This function may be used as a value for `Data.Foldable.foldMap` +-- in a `Foldable` instance. +foldMapFDefault :: (TraversableF t, Monoid m) => (forall s . e s -> m) -> t e -> m +foldMapFDefault f = getConst #. traverseF (Const #. f) + +-- | Map each element of a structure to an action, evaluate +-- these actions from left to right, and ignore the results. +traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s -> f ()) -> t e -> f () +traverseF_ f = foldrF (\e r -> f e *> r) (pure ()) diff --git a/src/Data/Parameterized/TraversableFC.hs b/src/Data/Parameterized/TraversableFC.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/TraversableFC.hs @@ -0,0 +1,162 @@ +------------------------------------------------------------------------ +-- | +-- Module : Data.Parameterized.TraversableFC +-- Copyright : (c) Galois, Inc 2014-2015 +-- Maintainer : Joe Hendrix +-- +-- This module declares classes for working with structures that accept +-- a parametric type parameter followed by some fixed kind. +------------------------------------------------------------------------ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE TypeOperators #-} +module Data.Parameterized.TraversableFC + ( TestEqualityFC(..) + , OrdFC(..) + , ShowFC(..) + , HashableFC(..) + , FunctorFC(..) + , FoldableFC(..) + , TraversableFC(..) + , traverseFC_ + , forMFC_ + , fmapFCDefault + , foldMapFCDefault + , allFC + , anyFC + , lengthFC + ) where + +import Control.Applicative (Const(..) ) +import Control.Monad.Identity ( Identity (..) ) +import Data.Coerce +import Data.Monoid +import GHC.Exts (build) +import Data.Type.Equality + +import Data.Parameterized.Classes + +-- | A parameterized type that is a function on all instances. +class FunctorFC m where + fmapFC :: forall f g. (forall x . f x -> g x) -> + (forall x . m f x -> m g x) + +-- | A parameterized class for types which can be shown, when given +-- functions to show parameterized subterms. +class ShowFC (t :: (k -> *) -> l -> *) where + {-# MINIMAL showFC | showsPrecFC #-} + + showFC :: forall f. (forall x. f x -> String) + -> (forall x. t f x -> String) + showFC sh x = showsPrecFC (\_prec z rest -> sh z ++ rest) 0 x [] + + showsPrecFC :: forall f. (forall x. Int -> f x -> ShowS) -> + (forall x. Int -> t f x -> ShowS) + showsPrecFC sh _prec x rest = showFC (\z -> sh 0 z []) x ++ rest + + +-- | A parameterized class for types which can be hashed, when given +-- functions to hash parameterized subterms. +class HashableFC (t :: (k -> *) -> l -> *) where + hashWithSaltFC :: forall f. (forall x. Int -> f x -> Int) -> + (forall x. Int -> t f x -> Int) + +-- | A parameterized class for types which can be tested for parameterized equality, +-- when given an equality test for subterms. +class TestEqualityFC (t :: (k -> *) -> l -> *) where + testEqualityFC :: forall f. (forall x y. f x -> f y -> (Maybe (x :~: y))) -> + (forall x y. t f x -> t f y -> (Maybe (x :~: y))) + +-- | A parameterized class for types which can be tested for parameterized ordering, +-- when given an comparison test for subterms. +class TestEqualityFC t => OrdFC (t :: (k -> *) -> l -> *) where + compareFC :: forall f. (forall x y. f x -> f y -> OrderingF x y) -> + (forall x y. t f x -> t f y -> OrderingF x y) + +------------------------------------------------------------------------ +-- FoldableF + +-- | This is a coercision used to avoid overhead associated +-- with function composition. +(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) +(#.) _f = coerce + +-- | This is a generalization of the @Foldable@ class to +-- structures over parameterized terms. +class FoldableFC (t :: (k -> *) -> l -> *) where + {-# MINIMAL foldMapFC | foldrFC #-} + + -- | Map each element of the structure to a monoid, + -- and combine the results. + foldMapFC :: Monoid m => (forall s . e s -> m) -> t e c -> m + foldMapFC f = foldrFC (mappend . f) mempty + + -- | Right-associative fold of a structure. + foldrFC :: (forall s . e s -> b -> b) -> b -> t e c -> b + foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z + + -- | Left-associative fold of a structure. + foldlFC :: (forall s . b -> e s -> b) -> b -> t e c -> b + foldlFC f z t = appEndo (getDual (foldMapFC (\e -> Dual (Endo (\r -> f r e))) t)) z + + -- | Right-associative fold of a structure, + -- but with strict application of the operator. + foldrFC' :: (forall s . e s -> b -> b) -> b -> t e c -> b + foldrFC' f0 z0 xs = foldlFC (f' f0) id xs z0 + where f' f k x z = k $! f x z + + -- | Left-associative fold of a parameterized structure + -- with a strict accumulator. + foldlFC' :: (forall s . b -> e s -> b) -> b -> t e c -> b + foldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0 + where f' f x k z = k $! f z x + + -- | Convert structure to list. + toListFC :: (forall tp . f tp -> a) -> t f c -> [a] + toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t) + +-- | Return 'True' if all values satisfy predicate. +allFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool +allFC p = getAll #. foldMapFC (All #. p) + +-- | Return 'True' if any values satisfy predicate. +anyFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool +anyFC p = getAny #. foldMapFC (Any #. p) + +-- | Return number of elements in list. +lengthFC :: FoldableFC t => t e c -> Int +lengthFC = foldrFC (const (+1)) 0 + +------------------------------------------------------------------------ +-- TraversableF + +class (FunctorFC t, FoldableFC t) => TraversableFC t where + traverseFC :: Applicative m + => (forall s . e s -> m (f s)) + -> t e c + -> m (t f c) + +-- | This function may be used as a value for `fmapF` in a `FunctorF` +-- instance. +fmapFCDefault :: TraversableFC t => (forall s . e s -> f s) -> t e c -> t f c +fmapFCDefault = \f -> runIdentity . traverseFC (Identity . f) +{-# INLINE fmapFCDefault #-} + +-- | This function may be used as a value for `Data.Foldable.foldMap` +-- in a `Foldable` instance. +foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall s . e s -> m) -> t e c -> m +foldMapFCDefault = \f -> getConst . traverseFC (Const . f) +{-# INLINE foldMapFCDefault #-} + +-- | Map each element of a structure to an action, evaluate +-- these actions from left to right, and ignore the results. +traverseFC_ :: (FoldableFC t, Applicative f) => (forall s . e s -> f ()) -> t e c -> f () +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 f) => t e c -> (forall s . e s -> f ()) -> f () +forMFC_ v f = traverseFC_ f v +{-# INLINE forMFC_ #-} diff --git a/src/Data/Parameterized/Utils/BinTree.hs b/src/Data/Parameterized/Utils/BinTree.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/Utils/BinTree.hs @@ -0,0 +1,368 @@ +{-| +Description : Utilities for balanced binary trees. +Copyright : (c) Galois, Inc 2014 +Maintainer : Joe Hendrix +-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Safe #-} +module Data.Parameterized.Utils.BinTree + ( MaybeS(..) + , fromMaybeS + , Updated(..) + , updatedValue + , TreeApp(..) + , IsBinTree(..) + , balanceL + , balanceR + , glue + , merge + , filterGt + , filterLt + , insert + , delete + , union + , link + , PairS(..) + ) where + +import Control.Applicative + +------------------------------------------------------------------------ +-- MaybeS + +-- | A strict version of 'Maybe' +data MaybeS v + = JustS !v + | NothingS + +instance Functor MaybeS where + fmap _ NothingS = NothingS + fmap f (JustS v) = JustS (f v) + +instance Alternative MaybeS where + empty = NothingS + mv@JustS{} <|> _ = mv + NothingS <|> v = v + +instance Applicative MaybeS where + pure = JustS + + NothingS <*> _ = NothingS + JustS{} <*> NothingS = NothingS + JustS f <*> JustS x = JustS (f x) + +fromMaybeS :: a -> MaybeS a -> a +fromMaybeS r NothingS = r +fromMaybeS _ (JustS v) = v + +------------------------------------------------------------------------ +-- Updated + +-- | Updated a contains a value that has been flagged on whether it was +-- modified by an operation. +data Updated a + = Updated !a + | Unchanged !a + +updatedValue :: Updated a -> a +updatedValue (Updated a) = a +updatedValue (Unchanged a) = a + +------------------------------------------------------------------------ +-- IsBinTree + +data TreeApp e t + = BinTree !e !t !t + | TipTree + +class IsBinTree t e | t -> e where + asBin :: t -> TreeApp e t + tip :: t + + bin :: e -> t -> t -> t + size :: t -> Int + +delta,ratio :: Int +delta = 3 +ratio = 2 + +-- `balanceL p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@. +-- +-- It assumes that @l@ and @r@ are close to being balanced, and that only +-- @l@ may contain too many elements. +balanceL :: (IsBinTree c e) => e -> c -> c -> c +balanceL p l r = do + case asBin l of + BinTree l_pair ll lr | size l > max 1 (delta*size r) -> + case asBin lr of + BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) -> + bin lr_pair (bin l_pair ll lrl) (bin p lrr r) + _ -> bin l_pair ll (bin p lr r) + + _ -> bin p l r +{-# INLINE balanceL #-} + +-- `balanceR p l r` returns a balanced tree for the sequence @l ++ [p] ++ r@. +-- +-- It assumes that @l@ and @r@ are close to being balanced, and that only +-- @r@ may contain too many elements. +balanceR :: (IsBinTree c e) => e -> c -> c -> c +balanceR p l r = do + case asBin r of + BinTree r_pair rl rr | size r > max 1 (delta*size l) -> + case asBin rl of + BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) -> + (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr + _ -> bin r_pair (bin p l rl) rr + _ -> bin p l r +{-# INLINE balanceR #-} + +-- | Insert a new maximal element. +insertMax :: IsBinTree c e => e -> c -> c +insertMax p t = + case asBin t of + TipTree -> bin p tip tip + BinTree q l r -> balanceR q l (insertMax p r) + +-- | Insert a new minimal element. +insertMin :: IsBinTree c e => e -> c -> c +insertMin p t = + case asBin t of + TipTree -> bin p tip tip + BinTree q l r -> balanceL q (insertMin p l) r + +-- | link is called to insert a key and value between two disjoint subtrees. +link :: IsBinTree c e => e -> c -> c -> c +link p l r = + case (asBin l, asBin r) of + (TipTree, _) -> insertMin p r + (_, TipTree) -> insertMax p l + (BinTree py ly ry, BinTree pz lz rz) + | delta*size l < size r -> balanceL pz (link p l lz) rz + | delta*size r < size l -> balanceR py ly (link p ry r) + | otherwise -> bin p l r +{-# INLINE link #-} + +-- | A Strict pair +data PairS f s = PairS !f !s + +deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c +deleteFindMin p l r = + case asBin l of + TipTree -> PairS p r + BinTree lp ll lr -> + case deleteFindMin lp ll lr of + PairS q l' -> PairS q (balanceR p l' r) +{-# INLINABLE deleteFindMin #-} + +deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c +deleteFindMax p l r = + case asBin r of + TipTree -> PairS p l + BinTree rp rl rr -> + case deleteFindMax rp rl rr of + PairS q r' -> PairS q (balanceL p l r') +{-# INLINABLE deleteFindMax #-} + +-- | Concatenate two trees that are ordered with respect to each other. +merge :: IsBinTree c e => c -> c -> c +merge l r = + case (asBin l, asBin r) of + (TipTree, _) -> r + (_, TipTree) -> l + (BinTree x lx rx, BinTree y ly ry) + | delta*size l < size r -> balanceL y (merge l ly) ry + | delta*size r < size l -> balanceR x lx (merge rx r) + | size l > size r -> + case deleteFindMax x lx rx of + PairS q l' -> balanceR q l' r + | otherwise -> + case deleteFindMin y ly ry of + PairS q r' -> balanceL q l r' +{-# INLINABLE merge #-} + +------------------------------------------------------------------------ +-- Ordered operations + +-- | @insert p m@ inserts the binding into @m@. It returns +-- an Unchanged value if the map stays the same size and an updated +-- value if a new entry was inserted. +insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c +insert comp x t = + case asBin t of + TipTree -> Updated (bin x tip tip) + BinTree y l r -> + case comp x y of + LT -> + case insert comp x l of + Updated l' -> Updated (balanceL y l' r) + Unchanged l' -> Unchanged (bin y l' r) + GT -> + case insert comp x r of + Updated r' -> Updated (balanceR y l r') + Unchanged r' -> Unchanged (bin y l r') + EQ -> Unchanged (bin x l r) +{-# INLINABLE insert #-} + +-- | 'glue l r' concatenates @l@ and @r@. +-- +-- It assumes that @l@ and @r@ are already balanced with respect to each other. +glue :: IsBinTree c e => c -> c -> c +glue l r = + case (asBin l, asBin r) of + (TipTree, _) -> r + (_, TipTree) -> l + (BinTree x lx rx, BinTree y ly ry) + | size l > size r -> + case deleteFindMax x lx rx of + PairS q l' -> balanceR q l' r + | otherwise -> + case deleteFindMin y ly ry of + PairS q r' -> balanceL q l r' +{-# INLINABLE glue #-} + +delete :: IsBinTree c e + => (e -> Ordering) + -- ^ Predicate that returns whether the entry is less than, greater than, or equal + -- to the key we are entry that we are looking for. + -> c + -> MaybeS c +delete k t = + case asBin t of + TipTree -> NothingS + BinTree p l r -> + case k p of + LT -> (\l' -> balanceR p l' r) <$> delete k l + GT -> (\r' -> balanceL p l r') <$> delete k r + EQ -> JustS (glue l r) +{-# INLINABLE delete #-} + +------------------------------------------------------------------------ +-- filter + +-- | Returns only entries that are less than predicate with respect to the ordering +-- and Nothing if no elements are discared. +filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c +filterGt k t = + case asBin t of + TipTree -> NothingS + BinTree x l r -> + case k x of + LT -> (\l' -> link x l' r) <$> filterGt k l + GT -> filterGt k r <|> JustS r + EQ -> JustS r +{-# INLINABLE filterGt #-} + + +-- | @filterLt' k m@ returns submap of @m@ that only contains entries +-- that are smaller than @k@. If no entries are deleted then return Nothing. +filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c +filterLt k t = + case asBin t of + TipTree -> NothingS + BinTree x l r -> + case k x of + LT -> filterLt k l <|> JustS l + GT -> (\r' -> link x l r') <$> filterLt k r + EQ -> JustS l +{-# INLINABLE filterLt #-} + +------------------------------------------------------------------------ +-- Union + +-- Insert a new key and value in the map if it is not already present. +-- Used by `union`. +insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c +insertR comp e m = fromMaybeS m (go e m) + where + go :: e -> c -> MaybeS c + go x t = + case asBin t of + TipTree -> JustS (bin x tip tip) + BinTree y l r -> + case comp x y of + LT -> (\l' -> balanceL y l' r) <$> go x l + GT -> (\r' -> balanceR y l r') <$> go x r + EQ -> NothingS +{-# INLINABLE insertR #-} + +-- | Union two sets +union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c +union comp t1 t2 = + case (asBin t1, asBin t2) of + (TipTree, _) -> t2 + (_, TipTree) -> t1 + (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1 + (BinTree x l r, _) -> + link x + (hedgeUnion_UB comp x l t2) + (hedgeUnion_LB comp x r t2) +{-# INLINABLE union #-} + +-- | Hedge union where we only add elements in second map if key is +-- strictly above a lower bound. +hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c +hedgeUnion_LB comp lo t1 t2 = + case (asBin t1, asBin t2) of + (_, TipTree) -> t1 + (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2) + -- Prune left tree. + (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r + -- Special case when t2 is a single element. + (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1 + -- Split on left-and-right subtrees of t1. + (BinTree x l r, _) -> + link x + (hedgeUnion_LB_UB comp lo x l t2) + (hedgeUnion_LB comp x r t2) +{-# INLINABLE hedgeUnion_LB #-} + +-- | Hedge union where we only add elements in second map if key is +-- strictly below a upper bound. +hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c +hedgeUnion_UB comp hi t1 t2 = + case (asBin t1, asBin t2) of + (_, TipTree) -> t1 + (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2) + -- Prune right tree. + (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l + -- Special case when t2 is a single element. + (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1 + -- Split on left-and-right subtrees of t1. + (BinTree x l r, _) -> + link x + (hedgeUnion_UB comp x l t2) + (hedgeUnion_LB_UB comp x hi r t2) +{-# INLINABLE hedgeUnion_UB #-} + +-- | Hedge union where we only add elements in second map if key is +-- strictly between a lower and upper bound. +hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c +hedgeUnion_LB_UB comp lo hi t1 t2 = + case (asBin t1, asBin t2) of + (_, TipTree) -> t1 + -- Prune left tree. + (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r + -- Prune right tree. + (_, BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l + -- When t1 becomes empty (assumes lo <= k <= hi) + (TipTree, BinTree x l r) -> + case (filterGt (comp lo) l, filterLt (comp hi) r) of + -- No variables in t2 were eliminated. + (NothingS, NothingS) -> t2 + -- Relink t2 with filtered elements removed. + (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r') + -- Special case when t2 is a single element. + (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1 + -- Split on left-and-right subtrees of t1. + (BinTree x l r, _) -> + link x + (hedgeUnion_LB_UB comp lo x l t2) + (hedgeUnion_LB_UB comp x hi r t2) +{-# INLINABLE hedgeUnion_LB_UB #-} diff --git a/test/Test/Context.hs b/test/Test/Context.hs new file mode 100644 --- /dev/null +++ b/test/Test/Context.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +module Test.Context +( contextTests +) where + +import Test.Tasty +import Test.QuickCheck +import Test.Tasty.QuickCheck + +import Data.Parameterized.Classes +import Data.Parameterized.TraversableFC +import Data.Parameterized.Some + +import qualified Data.Parameterized.Context.Safe as S +import qualified Data.Parameterized.Context.Unsafe as U + +data Payload (ty :: *) where + IntPayload :: Int -> Payload Int + StringPayload :: String -> Payload String + BoolPayload :: Bool -> Payload Bool + +instance TestEquality Payload where + testEquality (IntPayload x) (IntPayload y) = if x == y then Just Refl else Nothing + testEquality (StringPayload x) (StringPayload y) = if x == y then Just Refl else Nothing + testEquality (BoolPayload x) (BoolPayload y) = if x == y then Just Refl else Nothing + testEquality _ _ = Nothing + +instance Show (Payload tp) where + show (IntPayload x) = show x + show (StringPayload x) = show x + show (BoolPayload x) = show x + +instance ShowF Payload + +instance Arbitrary (Some Payload) where + arbitrary = oneof + [ Some . IntPayload <$> arbitrary + , Some . StringPayload <$> arbitrary + , Some . BoolPayload <$> arbitrary + ] + +type UAsgn = U.Assignment Payload +type SAsgn = S.Assignment Payload + +mkUAsgn :: [Some Payload] -> Some UAsgn +mkUAsgn = go U.empty + where go :: UAsgn ctx -> [Some Payload] -> Some UAsgn + go a [] = Some a + go a (Some x : xs) = go (U.extend a x) xs + +mkSAsgn :: [Some Payload] -> Some SAsgn +mkSAsgn = go S.empty + where go :: SAsgn ctx -> [Some Payload] -> Some SAsgn + go a [] = Some a + go a (Some x : xs) = go (S.extend a x) xs + +instance Arbitrary (Some UAsgn) where + arbitrary = mkUAsgn <$> arbitrary +instance Arbitrary (Some SAsgn) where + arbitrary = mkSAsgn <$> arbitrary + +twiddle :: Payload a -> Payload a +twiddle (IntPayload n) = IntPayload (n+1) +twiddle (StringPayload str) = StringPayload (str++"asdf") +twiddle (BoolPayload b) = BoolPayload (not b) + +contextTests :: IO TestTree +contextTests = testGroup "Context" <$> return + [ testProperty "safe_index_eq" $ \v vs i -> ioProperty $ do + let vals = v:vs + let i' = min (max 0 i) (length vals - 1) + Some a <- return $ mkSAsgn vals + Just (Some idx) <- return $ S.intIndex i' (S.size a) + return (Some (a S.! idx) == vals !! i') + , testProperty "unsafe_index_eq" $ \v vs i -> ioProperty $ do + let vals = v:vs + let i' = min (max 0 i) (length vals - 1) + Some a <- return $ mkUAsgn vals + Just (Some idx) <- return $ U.intIndex i' (U.size a) + return (Some (a U.! idx) == vals !! i') + , testProperty "safe_tolist" $ \vals -> ioProperty $ do + Some a <- return $ mkSAsgn vals + let vals' = toListFC Some a + return (vals == vals') + , testProperty "unsafe_tolist" $ \vals -> ioProperty $ do + Some a <- return $ mkUAsgn vals + let vals' = toListFC Some a + return (vals == vals') + , testProperty "adjust_test" $ \v vs i -> ioProperty $ do + let vals = v:vs + Some x <- return $ mkUAsgn vals + Some y <- return $ mkSAsgn vals + let i' = min (max 0 i) (length vals - 1) + + Just (Some idx_x) <- return $ U.intIndex i' (U.size x) + Just (Some idx_y) <- return $ S.intIndex i' (S.size y) + + let x' = U.adjust twiddle idx_x x + let y' = S.adjust twiddle idx_y y + + return (toListFC Some x' == toListFC Some y') + , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do + Some x <- return $ mkSAsgn vals1 + Some y <- return $ mkSAsgn vals2 + case testEquality x y of + Just Refl -> return $ vals1 == vals2 + Nothing -> return $ vals1 /= vals2 + , testProperty "unsafe_eq" $ \vals1 vals2 -> ioProperty $ do + Some x <- return $ mkUAsgn vals1 + Some y <- return $ mkUAsgn vals2 + case testEquality x y of + Just Refl -> return $ vals1 == vals2 + Nothing -> return $ vals1 /= vals2 + ] diff --git a/test/Test/NatRepr.hs b/test/Test/NatRepr.hs new file mode 100644 --- /dev/null +++ b/test/Test/NatRepr.hs @@ -0,0 +1,18 @@ +module Test.NatRepr +( natTests +) where + +import Test.Tasty +import Test.Tasty.QuickCheck + +import Data.Parameterized.NatRepr +import Data.Parameterized.Some +import GHC.TypeLits + +natTests :: IO TestTree +natTests = testGroup "Nat" <$> return + [ testProperty "withKnownNat" $ \nInt -> + case someNat nInt of + Nothing -> nInt < 0 + Just (Some r) -> nInt == withKnownNat r (natVal r) + ] diff --git a/test/UnitTest.hs b/test/UnitTest.hs new file mode 100644 --- /dev/null +++ b/test/UnitTest.hs @@ -0,0 +1,22 @@ +import Test.Tasty +import Test.Tasty.Ingredients +import Test.Tasty.Runners.AntXML + +import qualified Test.Context +import qualified Test.NatRepr + +main :: IO () +main = tests >>= defaultMainWithIngredients ingrs + +ingrs :: [Ingredient] +ingrs = + [ antXMLRunner + ] + ++ + defaultIngredients + +tests :: IO TestTree +tests = testGroup "ParameterizedUtils" <$> sequence + [ Test.Context.contextTests + , Test.NatRepr.natTests + ]