list-witnesses 0.1.2.0 → 0.1.3.0

raw patch · 3 files changed

+268/−4 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• list-witnesses.cabal +2/−2
• src/Data/Type/List/Sublist.hs +256/−2

@@ -1,6 +1,16 @@ Changelog ========= +Version 0.1.3.0+---------------++*August 23, 2019*++<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.3.0>++*   Add `Subset` and associated methods+*   `interleaveShapes`, `swapInterleave`, `appendShape`, `prefixShape`+ Version 0.1.2.0 --------------- 

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 7abc29a51e67cb59dca3b968d5864b7bcfd1126df6a3bb4166c3eddd2999129f+-- hash: 719f24db96d689225456161daf1be9b65869796716720c8702c4de187265dc65  name:           list-witnesses-version:        0.1.2.0+version:        0.1.3.0 synopsis:       Witnesses for working with type-level lists description:    Collection of assorted inductive witnesses and functions for working with                 type-level lists.

@@ -30,6 +30,7 @@   -- ** Prefix     Prefix(..), IsPrefix, autoPrefix   , takeRec, prefixLens, takeIndex, weakenIndex+  , prefixShape   -- ** Suffix   , Suffix(..), IsSuffix, autoSuffix   , dropRec, suffixLens, dropIndex, shiftIndex@@ -37,6 +38,7 @@   , Append(..), IsAppend, autoAppend, withAppend   , prefixToAppend, suffixToAppend   , appendToPrefix, appendToSuffix, splitAppend+  , appendShape   -- ** Application   , splitRec, appendRec, splitRecIso   , splitIndex@@ -55,10 +57,21 @@   , Interleave(..), IsInterleave, autoInterleave   , interleaveRec, unweaveRec, interleaveRecIso   , injectIndexL, injectIndexR, unweaveIndex-  , interleavedIxes+  , interleavedIxes, swapInterleave+  , interleaveShapes+  -- * Subset+  , Subset(..), IsSubset, autoSubset+  , subsetComplement+  , interleaveRToSubset, interleaveLToSubset+  , subsetToInterleaveLeft, subsetToInterleaveRight+  , subsetRec, getSubset+  , subsetShapes+  , subsetIxes+  , weakenSubsetIndex, strengthenSubsetIndex   ) where  import           Data.Bifunctor+import           Data.Functor.Compose import           Data.Kind import           Data.Profunctor import           Data.Singletons@@ -137,6 +150,16 @@ autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs autoPrefix = auto @_ @(IsPrefix as) @bs +-- | Get the 'Shape' associated with a 'Prefix'.+--+-- @since 0.1.3.0+prefixShape+    :: Prefix as bs+    -> Shape [] as+prefixShape = \case+    PreZ   -> RNil+    PreS p -> Proxy :& prefixShape p+ -- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@. -- -- Some examples:@@ -392,6 +415,16 @@     x :& xs -> \ys f -> withAppend xs ys $ \zs a ->       f (x :& zs) (AppS a) +-- | Get the 'Shape' associated with an 'Append''s prefix.+--+-- @since 0.1.3.0+appendShape+    :: Append as bs cs+    -> Shape [] as+appendShape = \case+    AppZ   -> RNil+    AppS a -> Proxy :& appendShape a+ -- | Witness an isomorphism between 'Rec' and two parts that compose it. -- -- Read this type signature as:@@ -538,7 +571,7 @@     SufS s -> IS . shiftIndex s  -- | A @'Interleave' as bs cs@ witnesses that @cs@ is @as@ interleaved with--- @bs. It is constructed by selectively zipping items from @as@ and @bs@+-- @bs@. It is constructed by selectively zipping items from @as@ and @bs@ -- together, like mergesort or riffle shuffle. -- -- You construct an 'Interleave' from @as@ and @bs@ by picking "which item" from@@ -730,3 +763,224 @@     -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))     -> p (Rec g cs)           (f (Rec g cs)) interleaveRecIso m = dimap (unweaveRec m) ((fmap . uncurry) (interleaveRec m))++-- | Swap the two halves of an 'Interleave'.+--+-- @since 0.1.3.0+swapInterleave+    :: Interleave as bs cs+    -> Interleave bs as cs+swapInterleave = \case+    IntZ   -> IntZ+    IntL i -> IntR $ swapInterleave i+    IntR i -> IntL $ swapInterleave i++-- | Get the 'Shape's associated with an 'Interleave'.+--+-- @since 0.1.3.0+interleaveShapes+    :: Interleave as bs cs+    -> (Shape [] as, Shape [] bs, Shape [] cs)+interleaveShapes = \case+    IntZ   -> (RNil, RNil, RNil)+    IntL i ->+      let (as         , bs         , cs         ) = interleaveShapes i+      in  (Proxy :& as, bs         , Proxy :& cs)+    IntR i ->+      let (as         , bs         , cs         ) = interleaveShapes i+      in  (as         , Proxy :& bs, Proxy :& cs)++-- | A @'Subset' as bs@ witnesses that @as@ is some subset of @bs@, with+-- items in the same order.  It is constructed by specifying+-- what item to include or exclude in @bs@ from @as@.  It is essentially+-- 'Interleave', but without one of the two initial parameters.+--+-- You construct an 'Subset' from @cs@ by picking "which item" from+-- @bs@ to add to @as@.+--+-- Some examples:+--+-- @+-- SubsetNo  (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[]      '[1,2,3]+-- SubsetYes (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[1]     '[1,2,3]+-- SubsetNo  (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[3]     '[1,2,3]+-- SubsetYes (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[1,3]   '[1,2,3]+-- SubsetYes (SubsetYes (SubsetYes SubsetNil)) :: Subset '[1,2,3] '[1,2,3]+-- @+--+-- @since 0.1.3.0+data Subset :: [k] -> [k] -> Type where+    SubsetNil :: Subset '[] '[]+    SubsetNo  :: Subset as bs -> Subset as        (b ': bs)+    SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs)++-- | Drop the right side of an 'Interleave', leaving only the left side.+interleaveLToSubset :: Interleave as bs cs -> Subset as cs+interleaveLToSubset = \case+    IntZ   -> SubsetNil+    IntL i -> SubsetYes . interleaveLToSubset $ i+    IntR i -> SubsetNo  . interleaveLToSubset $ i++-- | Drop the left side of an 'Interleave', leaving only the right side.+interleaveRToSubset :: Interleave as bs cs -> Subset bs cs+interleaveRToSubset = \case+    IntZ   -> SubsetNil+    IntL i -> SubsetNo  . interleaveRToSubset $ i+    IntR i -> SubsetYes . interleaveRToSubset $ i++-- | Convert a 'Subset' into an left 'Interleave', recovering the dropped+-- items.+subsetToInterleaveLeft+    :: Subset as cs+    -> (forall bs. Interleave as bs cs -> r)+    -> r+subsetToInterleaveLeft = \case+    SubsetNil   -> \f -> f IntZ+    SubsetNo  s -> \f -> subsetToInterleaveLeft s (f . IntR)+    SubsetYes s -> \f -> subsetToInterleaveLeft s (f . IntL)++-- | Convert a 'Subset' into an right 'Interleave', recovering the dropped+-- items.+subsetToInterleaveRight+    :: Subset bs cs+    -> (forall as. Interleave as bs cs -> r)+    -> r+subsetToInterleaveRight = \case+    SubsetNil   -> \f -> f IntZ+    SubsetNo  s -> \f -> subsetToInterleaveRight s (f . IntL)+    SubsetYes s -> \f -> subsetToInterleaveRight s (f . IntR)++-- | @as@ is a subset of @cs@; this function recovers @bs@, the subset of+-- @cs@ that is not @as@.+subsetComplement+    :: Subset as cs+    -> (forall bs. Subset bs cs -> r)+    -> r+subsetComplement = \case+    SubsetNil   -> \f -> f SubsetNil+    SubsetNo  s -> \f -> subsetComplement s (f . SubsetYes)+    SubsetYes s -> \f -> subsetComplement s (f . SubsetNo)++deriving instance Show (Subset as bs)+++-- | A type-level predicate that a given list is a "superset" of @as@, in+-- correct order+--+-- @since 0.1.2.0+type IsSubset as = TyPred (Subset as)++instance Auto (IsSubset '[]) '[] where+    auto = SubsetNil++instance Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where+    auto = SubsetNo (auto @_ @(IsSubset as) @bs)++instance Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where+    auto = SubsetYes (auto @_ @(IsSubset as) @bs)++instance (SDecide k, SingI (as :: [k])) => Decidable (IsSubset as) where+    decide = case sing @as of+      SNil -> \case+        SNil -> Proved SubsetNil+        _ `SCons` ys -> case decide @(IsSubset '[]) ys of+          Proved s    -> Proved $ SubsetNo s+          Disproved v -> Disproved $ \case+            SubsetNo s -> v s+      x `SCons` (Sing :: Sing as') -> \case+        SNil -> Disproved $ \case {}+        y `SCons` ys -> case x %~ y of+          Proved Refl -> case decide @(IsSubset as') ys of+            Proved s    -> Proved $ SubsetYes s+            Disproved v -> case decide @(IsSubset as) ys of+              Proved s    -> Proved $ SubsetNo s+              Disproved u -> Disproved $ \case+                SubsetNo s  -> u s+                SubsetYes s -> v s+          Disproved v -> case decide @(IsSubset as) ys of+            Proved s    -> Proved $ SubsetNo s+            Disproved u -> Disproved $ \case+              SubsetNo s  -> u s+              SubsetYes _ -> v Refl++-- | Automatically generate an 'Subset' if @as@ and @bs@ are known+-- statically.+autoSubset :: forall as bs. Auto (IsSubset as) bs => Subset as bs+autoSubset = auto @_ @(IsSubset as) @bs++-- | A lens into a subset of a record, indicated by a 'Subset'.+subsetRec :: Subset as bs -> Lens' (Rec f bs) (Rec f as)+subsetRec = \case+    SubsetNil   -> id+    SubsetNo  s -> \f -> \case+      x :& xs -> (x :&) <$> subsetRec s f xs+    SubsetYes s -> \f -> \case+      x :& xs -> fmap (uncurry (:&))+               . getCompose+               . subsetRec s (Compose . fmap (\(y :& ys) -> (y,ys)) . f . (x :&))+               $ xs++-- | Take a subset out of a 'Rec'.  An alias for @'view' ('subsetRec' s)@.+getSubset+    :: Subset as bs+    -> Rec f bs+    -> Rec f as+getSubset = view . subsetRec++-- | Get all of the indices of all the items in a 'Subset'.+subsetIxes+    :: Subset as bs+    -> Rec (Index bs) as+subsetIxes s = getSubset s . imapProd const $ sp+  where+    (_, sp) = subsetShapes s++-- | Get the 'Shape's associated with a 'Subset'.+subsetShapes+    :: Subset as bs+    -> (Shape [] as, Shape [] bs)+subsetShapes = \case+    SubsetNil    -> (RNil, RNil)+    SubsetNo   s -> second (Proxy :&) $ subsetShapes s+    SubsetYes  s -> bimap (Proxy :&) (Proxy :&) $ subsetShapes s++-- | Because @as@ is a subset of @bs@, an index into @as@ should also be an+-- index into @bs@.  This performs that transformation.+--+-- This is like a version of 'injectIndexL' or 'injectIndexR', for+-- 'Subset'.+weakenSubsetIndex+    :: Subset as bs+    -> Index as a+    -> Index bs a+weakenSubsetIndex = \case+    SubsetNil   -> \case {}+    SubsetNo  s -> IS . weakenSubsetIndex s+    SubsetYes s -> \case+      IZ   -> IZ+      IS i -> IS $ weakenSubsetIndex s i++-- | Because @as@ is a subset of @bs@, we can /sometimes/ transform an+-- index into @bs@ into an index into @as@.  This performs that+-- transformation.  If it succeeds, it means that the index in @bs@ also+-- exists in @as@; otherwise, it means that the index in @bs@ was excluded+-- from @as@.+--+-- Note that if the index into @a@ was excluded from @as@, it doesn't+-- necessarily mean that there is no @a@ in @bs@ --- @bs@ could contain+-- a duplicate that was included into @as@.  This converts into an index to+-- the exact same item (positionlly) in the list, if it is possible.+--+-- This is like a version of 'unweaveIndex', but for 'Subset'.+strengthenSubsetIndex+    :: Subset as bs+    -> Index bs a+    -> Maybe (Index as a)+strengthenSubsetIndex = \case+    SubsetNil   -> \case {}+    SubsetNo  s -> \case+      IZ   -> Nothing+      IS i -> strengthenSubsetIndex s i+    SubsetYes s -> \case+      IZ   -> Just IZ+      IS i -> IS <$> strengthenSubsetIndex s i