list-witnesses 0.1.1.1 → 0.1.2.0

raw patch · 4 files changed

+578/−46 lines, 4 filesdep +functor-productsdep ~decidablePVP ok

version bump matches the API change (PVP)

Dependencies added: functor-products

Dependency ranges changed: decidable

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• list-witnesses.cabal +5/−4
• src/Data/Type/List/Edit.hs +195/−24
• src/Data/Type/List/Sublist.hs +365/−18

@@ -1,6 +1,19 @@ Changelog ========= +Version 0.1.2.0+---------------++*August 12, 2019*++<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.2.0>++*   Add predicates (`IsInsert`, `IsPrefix`, etc.) and `Auto` and `Decidable`+    instances for most of the data types, for auto-generation and searches.+*   Add some functions for creating `Append`s and witnesses of concatenation+    type families from `Append`s.+*   `interleavedIxes`, for more manipulation of `Interleave`+ Version 0.1.1.1 --------------- 

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: a6892eb45e6aae7a7e7c3f4b23c95bdd2299a3a95a190137567cd326e5045529+-- hash: 7abc29a51e67cb59dca3b968d5864b7bcfd1126df6a3bb4166c3eddd2999129f  name:           list-witnesses-version:        0.1.1.1+version:        0.1.2.0 synopsis:       Witnesses for working with type-level lists description:    Collection of assorted inductive witnesses and functions for working with                 type-level lists.@@ -24,7 +24,7 @@ copyright:      (c) Justin Le 2018 license:        BSD3 license-file:   LICENSE-tested-with:    GHC >= 8.4+tested-with:    GHC >= 8.6 build-type:     Simple extra-source-files:     README.md@@ -45,7 +45,8 @@   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns   build-depends:       base >=4.7 && <5-    , decidable >=0.1.5+    , decidable >=0.2+    , functor-products     , microlens     , profunctors     , singletons

@@ -1,14 +1,19 @@-{-# LANGUAGE EmptyCase            #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE KindSignatures       #-}-{-# LANGUAGE LambdaCase           #-}-{-# LANGUAGE RankNTypes           #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE StandaloneDeriving   #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeInType           #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE EmptyCase             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeInType            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE UndecidableInstances  #-}  -- | -- Module      : Data.Type.List.Edit@@ -22,13 +27,17 @@ -- Witnesses regarding single-item edits of lists. module Data.Type.List.Edit (   -- * Simple edits-    Insert(..)-  , Delete(..)+    Insert(..), autoInsert+  , Delete(..), autoDelete   , insToDel   , delToIns-  , Substitute(..)+  , Substitute(..), autoSubstitute   , flipSub   , subToDelIns+  -- ** Predicates+  , IsInsert, InsertedInto+  , IsDelete, DeletedFrom+  , IsSubstitute   -- ** Singletons   , SInsert(..)   , SDelete(..)@@ -61,10 +70,15 @@  import           Data.Kind import           Data.Singletons-import           Data.Type.Universe-import           Data.Vinyl.Core-import           Lens.Micro-import qualified Control.Category      as C+import           Data.Singletons.Decide+import           Data.Singletons.Prelude+import           Data.Singletons.Sigma+import           Data.Type.Functor.Product+import           Data.Type.Predicate+import           Data.Type.Predicate.Auto+import           Data.Type.Predicate.Param+import           Lens.Micro hiding         ((%~))+import qualified Control.Category          as C  -- | An @'Insert' as bs x@ is a witness that you can insert @x@ into some -- position in list @as@ to produce list @bs@.  It is essentially 'Delete'@@ -86,6 +100,94 @@  deriving instance Show (Insert as bs x) +-- | A type-level predicate that a given value can be used as an insertion+-- to change @as@ to @bs@.+--+-- @since 0.1.2.0+type IsInsert as bs = TyPred (Insert as bs)++instance Auto (IsInsert as (x ': as)) x where+    auto = InsZ++instance Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where+    auto = InsS (auto @_ @(IsInsert as bs) @x)++instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where+    decide z = case sing @bs of+      SNil -> Disproved $ \case {}+      y `SCons` (ys@Sing :: Sing bs') -> case y %~ z of+        Proved Refl -> case sing @as %~ ys of+          Proved Refl -> Proved InsZ+          Disproved v -> case sing @as of+            SNil -> Disproved $ \case+              InsZ -> v Refl+            x `SCons` (Sing :: Sing as') -> case x %~ y of+              Proved Refl -> case decide @(IsInsert as' bs') z of+                Proved i -> Proved $ InsS i+                Disproved u -> Disproved $ \case+                  InsZ -> u InsZ+                  InsS i -> u i+              Disproved u -> Disproved $ \case+                InsZ   -> v Refl+                InsS _ -> u Refl+        Disproved v -> case sing @as of+          SNil -> Disproved $ \case+            InsZ -> v Refl+          x `SCons` (Sing :: Sing as') -> case x %~ y of+            Proved Refl -> case decide @(IsInsert as' bs') z of+              Proved i -> Proved $ InsS i+              Disproved u -> Disproved $ \case+                InsZ -> u InsZ+                InsS i -> u i+            Disproved u -> Disproved $ \case+              InsZ   -> v Refl+              InsS _ -> u Refl++-- | If @bs@ satisfies @'InsertedInto' as@, it means that there exists some+-- element @x@ such that @'IsInsert' as bs \@\@ x@: you can get @bs@ by+-- inserting @x@ into @as@ somewhere.+--+-- In other words, @'InsertedInto' as@ is satisfied by @bs@ if you can turn+-- @as@ into @bs@ by inserting one individual item.+--+-- You can find this element (if it exists) using 'search', or the+-- 'Decidable' instance of @'Found' ('InsertedInto' as)@:+--+-- @+-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsInsert' as bs))+-- @+--+-- This will find you the single element you need to insert into @as@ to+-- get @bs@, if it exists.+--+-- @since 0.1.2.0+type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)++instance (SDecide k, SingI (as :: [k])) => Decidable (Found (InsertedInto as)) where+    decide = \case+      SNil -> Disproved $ \(_ :&: i) -> case i of {}+      y `SCons` ys -> case sing @as %~ ys of+        Proved Refl -> Proved $ y :&: InsZ+        Disproved v -> case sing @as of+          SNil -> Disproved $ \(_ :&: i) -> case i of+            InsZ -> v Refl+          x `SCons` (Sing :: Sing as') -> case x %~ y of+            Proved Refl -> case decide @(Found (InsertedInto as')) ys of+              Proved (z :&: i) -> Proved $ z :&: InsS i+              Disproved u      -> Disproved $ \(z :&: i) -> case i of+                InsZ    -> u $ z :&: InsZ+                InsS i' -> u $ z :&: i'+            Disproved u -> Disproved $ \(_ :&: i) -> case i of+              InsZ   -> v Refl+              InsS _ -> u Refl++-- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known+-- statically.+--+-- @since 0.1.2.0+autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x+autoInsert = auto @_ @(IsInsert as bs) @x+ -- | Kind-indexed singleton for 'Insert'. data SInsert as bs x :: Insert as bs x -> Type where     SInsZ :: SInsert as (x ': as) x 'InsZ@@ -117,6 +219,54 @@  deriving instance Show (Delete as bs x) +-- | A type-level predicate that a given value can be used as a deletion+-- to change @as@ to @bs@.+--+-- @since 0.1.2.0+type IsDelete as bs = TyPred (Delete as bs)++instance Auto (IsDelete (x ': as) as) x where+    auto = DelZ++instance Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where+    auto = DelS (auto @_ @(IsDelete as bs) @x)++instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where+    decide = mapDecision insToDel delToIns . decide @(IsInsert bs as)++-- | If @bs@ satisfies @'DeletedFrom' as@, it means that there exists some+-- element @x@ such that @'IsDelete' as bs \@\@ x@: you can get @bs@ by+-- deleting @x@ from @as@ somewhere.+--+-- In other words, @'DeletedFrom' as@ is satisfied by @bs@ if you can turn+-- @as@ into @bs@ by deleting one individual item.+--+-- You can find this element (if it exists) using 'search', or the+-- 'Decidable' instance of @'Found' ('DeletedFrom' as)@.+--+-- @+-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsDelete' as bs))+-- @+--+-- This will find you the single element you need to delete from @as@ to+-- get @bs@, if it exists.+--+-- @since 0.1.2.0+type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k)++instance (SDecide k, SingI (as :: [k])) => Decidable (Found (DeletedFrom as)) where+    decide (Sing :: Sing bs) =+        mapDecision (mapSigma (sing @IdSym0) insToDel)+                    (mapSigma (sing @IdSym0) delToIns)+      $ decide @(Found (InsertedInto bs)) (sing @as)++-- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known+-- statically.+--+-- @since 0.1.2.0+autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x+autoDelete = auto @_ @(IsDelete as bs) @x+ -- | Kind-indexed singleton for 'Delete'. data SDelete as bs x :: Delete as bs x -> Type where     SDelZ :: SDelete (x ': as) as x 'DelZ@@ -147,6 +297,26 @@  deriving instance Show (Substitute as bs x y) +-- | A type-level predicate that a given value can be used as+-- a substitution of @x@ to change @as@ to @bs@.+--+-- @since 0.1.2.0+type IsSubstitute as bs x = TyPred (Substitute as bs x)++instance Auto (IsSubstitute (x ': as) (y ': as) x) y where+    auto = SubZ++instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where+    auto = SubS (auto @_ @(IsSubstitute as bs x) @y)++-- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are+-- known statically.+--+-- @since 0.1.2.0+autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y+autoSubstitute = auto @_ @(IsSubstitute as bs x) @y++ -- | Kind-indexed singleton for 'Substitute'. data SSubstitute as bs x y :: Substitute as bs x y -> Type where     SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ@@ -193,7 +363,8 @@     id = ENil     xs . ys = compEdit ys xs --- | Reverse an 'Edit' script.  O(n^2).  Please do not use.+-- | Reverse an 'Edit' script.  O(n^2).  Please do not use ever in any+-- circumstance. -- -- TODO: Make O(n) using diff lists. flipEdit :: Edit as bs -> Edit bs as@@ -241,8 +412,8 @@ -- The number of 'SubS' in the index essentially indicates the index to -- edit at. ----- This is similar to 'rlensC' from /vinyl/, but is built explicitly and--- inductively, instead of using typeclass magic.+-- This is similar to 'Data.Vinyl.Lens.rlensC' from /vinyl/, but is built+-- explicitly and inductively, instead of using typeclass magic. recLens     :: forall as bs x y f. ()     => Substitute as bs x y@@ -472,9 +643,9 @@     SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)     SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i) --- | Type-level version of 'subsituteIndex'.  Because of how GADTs and type--- families interact, the type-level lists and kinds of the insertion and--- index must be provided.+-- | Type-level version of 'substituteIndex'.  Because of how GADTs and+-- type families interact, the type-level lists and kinds of the insertion+-- and index must be provided. type family SubstituteIndex as bs x y z (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where     SubstituteIndex (z ': as) (y ': as) z y z 'SubZ     'IZ     = 'GotSubbed 'IZ     SubstituteIndex (x ': as) (y ': as) x y z 'SubZ     ('IS i) = 'NotSubbed ('IS i)

@@ -1,13 +1,19 @@-{-# LANGUAGE EmptyCase           #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving  #-}-{-# LANGUAGE TupleSections       #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE EmptyCase             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TupleSections         #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeInType            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE ViewPatterns          #-}  -- | -- Module      : Data.Type.List.Sublist@@ -22,31 +28,53 @@ module Data.Type.List.Sublist (   -- * Prefix and Suffix   -- ** Prefix-    Prefix(..)+    Prefix(..), IsPrefix, autoPrefix   , takeRec, prefixLens, takeIndex, weakenIndex   -- ** Suffix-  , Suffix(..)+  , Suffix(..), IsSuffix, autoSuffix   , dropRec, suffixLens, dropIndex, shiftIndex   -- * Append-  , Append(..)+  , Append(..), IsAppend, autoAppend, withAppend   , prefixToAppend, suffixToAppend   , appendToPrefix, appendToSuffix, splitAppend   -- ** Application   , splitRec, appendRec, splitRecIso   , splitIndex+  -- ** Witnesses+  -- *** Singletons+  , pattern AppendWit+  , appendWit, implyAppend, unAppendWit+  -- *** Vinyl+  , pattern AppendWitV+  , appendWitV, implyAppendV, unAppendWitV+  -- *** Both+  , pattern AppendWit'+  , convertAppends+  , AppendedTo   -- * Interleave-  , Interleave(..)+  , Interleave(..), IsInterleave, autoInterleave   , interleaveRec, unweaveRec, interleaveRecIso   , injectIndexL, injectIndexR, unweaveIndex+  , interleavedIxes   ) where  import           Data.Bifunctor import           Data.Kind import           Data.Profunctor-import           Data.Type.Universe-import           Data.Vinyl.Core-import           Lens.Micro+import           Data.Singletons+import           Data.Singletons.Decide+import           Data.Singletons.Prelude.List+import           Data.Singletons.Sigma+import           Data.Type.Functor.Product+import           Data.Type.Predicate+import           Data.Type.Predicate.Auto+import           Data.Type.Predicate.Param+import           Data.Vinyl hiding            ((:~:))+import           GHC.Generics                 ((:+:)(..))+import           Lens.Micro hiding            ((%~)) import           Lens.Micro.Extras+import qualified Data.Vinyl.Recursive         as VR+import qualified Data.Vinyl.TypeLevel         as V  -- | A @'Prefix' as bs@ witnesses that @as@ is a prefix of @bs@. --@@ -78,6 +106,37 @@ takeRec :: Prefix as bs -> Rec f bs -> Rec f as takeRec p = view (prefixLens p) +-- | A type-level predicate that a given list has @as@ as a prefix.+--+-- @since 0.1.2.0+type IsPrefix as = TyPred (Prefix as)++instance Auto (IsPrefix '[]) bs where+    auto = PreZ++instance Auto (IsPrefix as) bs => Auto (IsPrefix (a ': as)) (a ': bs) where+    auto = PreS (auto @_ @(IsPrefix as) @bs)++instance (SDecide k, SingI (as :: [k])) => Decidable (IsPrefix as) where+    decide = case sing @as of+      SNil         -> \_ -> Proved PreZ+      x `SCons` (Sing :: Sing as') -> \case+        SNil -> Disproved $ \case {}+        y `SCons` (ys :: Sing bs') -> case x %~ y of+          Proved Refl -> case decide @(IsPrefix as') ys of+            Proved p -> Proved (PreS p)+            Disproved v -> Disproved $ \case+              PreS p -> v p+          Disproved v -> Disproved $ \case+            PreS _ -> v Refl++-- | Automatically generate a 'Prefix' if @as@ and @bs@ are known+-- statically.+--+-- @since 0.1.2.0+autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs+autoPrefix = auto @_ @(IsPrefix as) @bs+ -- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@. -- -- Some examples:@@ -100,6 +159,35 @@  deriving instance Show (Suffix as bs) +-- | A type-level predicate that a given list has @as@ as a suffix.+--+-- @since 0.1.2.0+type IsSuffix as = TyPred (Suffix as)++instance Auto (IsSuffix as) as where+    auto = SufZ++instance Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where+    auto = SufS (auto @_ @(IsSuffix as) @bs)++instance (SDecide k, SingI (as :: [k])) => Decidable (IsSuffix as) where+    decide = \case+      SNil -> case sing @as of+        SNil -> Proved SufZ+        _ `SCons` _ -> Disproved $ \case {}+      _ `SCons` ys -> case decide @(IsSuffix as) ys of+        Proved s    -> Proved $ SufS s+        Disproved v -> Disproved $ \case+          SufZ   -> error "help me"+          SufS s -> v s++-- | Automatically generate a 'Suffix' if @as@ and @bs@ are known+-- statically.+--+-- @since 0.1.2.0+autoSuffix :: forall as bs. Auto (IsSuffix as) bs => Suffix as bs+autoSuffix = auto @_ @(IsSuffix as) @bs+ -- | A lens into the suffix of a 'Rec'. suffixLens :: Suffix as bs -> Lens' (Rec f bs) (Rec f as) suffixLens p = suffixToAppend p $ \a -> splitRecIso a . _2@@ -129,6 +217,181 @@  deriving instance Show (Append as bs cs) +-- | A type-level predicate that a given list is the result of appending of+-- @as@ and @bs@.+--+-- @since 0.1.2.0+type IsAppend as bs = TyPred (Append as bs)++-- | A parameterized predicate that you can use with 'select': With an+-- @'AppendedTo' as@, you can give @bs@ and get @cs@ in return, where @cs@+-- is the appending of @as@ and @bs@.+--+-- Run it with:+--+-- @+-- 'selectTC' :: SingI as => Sing bs -> 'Σ' [k] ('IsAppend' as bs)+-- @+--+-- 'select' for 'AppendedTo' is pretty much just 'withAppend'.+--+-- @since 0.1.2.0+type AppendedTo as = TyPP (Append as)++instance Auto (IsAppend '[] as) as where+    auto = AppZ++instance Auto (IsAppend as bs) cs => Auto (IsAppend (a ': as) bs) (a ': cs) where+    auto = AppS (auto @_ @(IsAppend as bs) @cs)++instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsAppend as bs) where+    decide = case sing @as of+      SNil         -> \cs -> case sing @bs %~ cs of+        Proved Refl -> Proved AppZ+        Disproved v -> Disproved $ \case+          AppZ -> v Refl+      x `SCons` (Sing :: Sing as') -> \case+        SNil -> Disproved $ \case {}+        y `SCons` (ys :: Sing bs') -> case x %~ y of+          Proved Refl -> case decide @(IsAppend as' bs) ys of+            Proved p -> Proved (AppS p)+            Disproved v -> Disproved $ \case+              AppS p -> v p+          Disproved v -> Disproved $ \case+            AppS _ -> v Refl++instance SingI as => Decidable (Found (AppendedTo as))+instance SingI as => Provable (Found (AppendedTo as)) where+    prove ys = withAppend (singProd (sing @as)) (singProd ys) $ \s x -> prodSing s :&: x++-- | Automatically generate an 'Append' if @as@, @bs@ and @cs@ are known+-- statically.+--+-- @since 0.1.2.0+autoAppend :: forall as bs cs. Auto (IsAppend as bs) cs => Append as bs cs+autoAppend = auto @_ @(IsAppend as bs) @cs++-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using+-- @++@ from "Data.Singletons.Prelude.List".+--+-- @since 0.1.2.0+appendWit :: Append as bs cs -> (as ++ bs) :~: cs+appendWit = \case+    AppZ   -> Refl+    AppS a -> case appendWit a of+      Refl -> Refl++-- | The inverse of 'appendWit': if we know @(as ++ bs) ~ cs@ (using @++@+-- from "Data.Singletons.Prelude.List"), we can create an @'Append' as bs+-- cs@ given structure witnesses 'Sing'.+--+-- @since 0.1.2.0+unAppendWit+    :: (as ++ bs) ~ cs+    => Rec f as+    -> Rec f bs+    -> Append as bs cs+unAppendWit = \case+    RNil    -> \_   -> AppZ+    _ :& xs -> AppS . unAppendWit xs++-- | A useful pattern synonym for using 'Append' with @++@ from+-- "Data.Singletons.Prelude.List".+--+-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever+-- you use it to match on an @'Append' as bs cs@.+--+-- As an /expression/, this constructs an @'Append' as bs cs@ as long as+-- you have @(as ++ bs) ~ cs@ in the context.+--+-- @since 0.1.2.0+pattern AppendWit :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs+pattern AppendWit <- (appendWit @as @bs @cs -> Refl)+  where+    AppendWit = unAppendWit @as @bs @cs pureShape pureShape+{-# COMPLETE AppendWit #-}++-- | 'appendWit' stated as a 'Predicate' implication.+--+-- @since 0.1.2.0+implyAppend :: IsAppend as bs --> EqualTo (as ++ bs)+implyAppend _ = appendWit++-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using+-- @++@ from "Data.Vinyl.TypeLevel".+--+-- @since 0.1.2.0+appendWitV :: Append as bs cs -> (as V.++ bs) :~: cs+appendWitV = \case+    AppZ -> Refl+    AppS a -> case appendWitV a of+      Refl -> Refl++-- | The inverse of 'appendWitV': if we know @(as ++ bs) ~ cs@ (using @++@+-- from "Data.Vinyl.TypeLevel"), we can create an @'Append' as bs cs@ given+-- structure witnesses 'Sing'.+--+-- @since 0.1.2.0+unAppendWitV+    :: (as V.++ bs) ~ cs+    => Rec f as+    -> Rec f bs+    -> Append as bs cs+unAppendWitV = \case+    RNil     -> \_   -> AppZ+    _ :& xs -> AppS . unAppendWitV xs++-- | A useful pattern synonym for using 'Append' with @++@ from+-- "Data.Vinyl.TypeLevel".+--+-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever+-- you use it to match on an @'Append' as bs cs@.+--+-- As an /expression/, this constructs an @'Append' as bs cs@ as long as+-- you have @(as ++ bs) ~ cs@ in the context.+--+-- @since 0.1.2.0+pattern AppendWitV :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as V.++ bs) ~ cs => Append as bs cs+pattern AppendWitV <- (appendWitV @as @bs @cs -> Refl)+  where+    AppendWitV = unAppendWitV @as @bs @cs pureShape pureShape+{-# COMPLETE AppendWitV #-}++-- | Combine the powers of 'AppendWit' and 'AppendWitV' by matching on an+-- 'Append' to witness @(as ++ bs) ~ cs@ for /both/ @++@ from+-- "Data.Singletons.Prelude.List" and "Data.Vinyl.TypeLevel".  This also+-- witnesses that @(as ++ bs) ~ (as ++ bs)@ (for the two different @++@s)+-- by transitive property.+--+-- @since 0.1.2.0+pattern AppendWit' :: forall as bs cs. (RecApplicative as, RecApplicative bs) => ((as ++ bs) ~ cs, (as V.++ bs) ~ cs) => Append as bs cs+pattern AppendWit' <- ((\a -> (a,a)) -> (AppendWit, AppendWitV))+  where+    AppendWit' = AppendWit+{-# COMPLETE AppendWitV #-}++-- | 'appendWitV' stated as a 'Predicate' implication.+--+-- @since 0.1.2.0+implyAppendV :: IsAppend as bs --> EqualTo (as V.++ bs)+implyAppendV _ = appendWitV++-- | Given a witness @'Append' as bs cs@, prove that singleton's @++@ from+-- "Data.Singletons.Prelude.List" is the same as vinyl's @++@+-- "Data.Vinyl.TypeLevel".+convertAppends :: Append as bs cs -> (as ++ bs) :~: (as V.++ bs)+convertAppends a = case appendWit a of+    Refl -> case appendWitV a of+      Refl -> Refl++-- | Given @as@ and @bs@, create an @'Append' as bs cs@ with, with @cs@+-- existentially quantified+withAppend :: Rec f as -> Rec f bs -> (forall cs. Rec f cs -> Append as bs cs -> r) -> r+withAppend = \case+    RNil -> \ys f -> f ys AppZ+    x :& xs -> \ys f -> withAppend xs ys $ \zs a ->+      f (x :& zs) (AppS a)+ -- | Witness an isomorphism between 'Rec' and two parts that compose it. -- -- Read this type signature as:@@ -278,7 +541,7 @@ -- @bs. It is constructed by selectively zipping items from @as@ and @bs@ -- together, like mergesort or riffle shuffle. ----- You construct a 'Interleave' from @as@ and @bs@ by picking "which item" from+-- You construct an 'Interleave' from @as@ and @bs@ by picking "which item" from -- @as@ and @bs@ to add to @cs@. -- -- Some examples:@@ -298,6 +561,77 @@  deriving instance Show (Interleave as bs cs) +-- | A type-level predicate that a given list is the "interleave" of @as@+-- and @bs@.+--+-- @since 0.1.2.0+type IsInterleave as bs = TyPred (Interleave as bs)++instance Auto (IsInterleave '[] '[]) '[] where+    auto = IntZ++instance Auto (IsInterleave as bs) cs => Auto (IsInterleave (a ': as) bs) (a ': cs) where+    auto = IntL (auto @_ @(IsInterleave as bs) @cs)++instance Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where+    auto = IntR (auto @_ @(IsInterleave as bs) @cs)++instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInterleave as bs) where+    decide = case sing @as of+      SNil -> case sing @bs of+        SNil -> \case+          SNil -> Proved IntZ+          _ `SCons` _ -> Disproved $ \case {}+        y `SCons` (Sing :: Sing bs') -> \case+          z `SCons` (zs :: Sing cs') -> case y %~ z of+            Proved Refl -> case decide @(IsInterleave '[] bs') zs of+              Proved i -> Proved $ IntR i+              Disproved v -> Disproved $ \case+                IntR i -> v i+            Disproved v -> Disproved $ \case+              IntR _ -> v Refl+          SNil -> Disproved $ \case {}+      x `SCons` (Sing :: Sing as') -> case sing @bs of+        SNil -> \case+          z `SCons` (zs :: Sing cs') -> case x %~ z of+            Proved Refl -> case decide @(IsInterleave as' '[]) zs of+              Proved i -> Proved $ IntL i+              Disproved v -> Disproved $ \case+                IntL i -> v i+            Disproved v -> Disproved $ \case+              IntL _ -> v Refl+          SNil -> Disproved $ \case {}+        y `SCons` (Sing :: Sing bs') -> \case+          SNil -> Disproved $ \case {}+          z `SCons` (zs :: Sing cs') -> case x %~ z of+            Proved Refl -> case decide @(IsInterleave as' bs) zs of+              Proved i    -> Proved $ IntL i+              Disproved v -> case y %~ z of+                Proved Refl -> case decide @(IsInterleave as bs') zs of+                  Proved i -> Proved $ IntR i+                  Disproved u -> Disproved $ \case+                    IntL i -> v i+                    IntR i -> u i+                Disproved u -> Disproved $ \case+                  IntL i -> v i+                  IntR _ -> u Refl+            Disproved v -> case y %~ z of+              Proved Refl -> case decide @(IsInterleave as bs') zs of+                Proved i -> Proved $ IntR i+                Disproved u -> Disproved $ \case+                  IntL _ -> v Refl+                  IntR i -> u i+              Disproved u -> Disproved $ \case+                IntL _ -> v Refl+                IntR _ -> u Refl++-- | Automatically generate an 'Interleave' if @as@ and @bs@ are known+-- statically.+--+-- @since 0.1.2.0+autoInterleave :: forall as bs cs. Auto (IsInterleave as bs) cs => Interleave as bs cs+autoInterleave = auto @_ @(IsInterleave as bs) @cs+ -- | Given two 'Rec's, interleave the two to create a combined 'Rec'. -- -- @since 0.1.1.0@@ -323,6 +657,19 @@       x :& xs -> first  (x :&) . unweaveRec m $ xs     IntR m -> \case       x :& xs -> second (x :&) . unweaveRec m $ xs++-- | Turn an 'Interleave' into a 'Rec' of indices from either sublist.+--+-- Warning: O(n^2)+--+-- @since 0.1.2.0+interleavedIxes :: Interleave as bs cs -> Rec (Index as :+: Index bs) cs+interleavedIxes = \case+    IntZ   -> RNil+    IntL i -> L1 IZ :& VR.rmap (\case L1 i' -> L1 (IS i'); R1 j -> R1 j)+                               (interleavedIxes i)+    IntR j -> R1 IZ :& VR.rmap (\case L1 i -> L1 i; R1 j' -> R1 (IS j'))+                               (interleavedIxes j)  -- | Interleave an 'Index' on @as@ into a full index on @cs@, which is @as@ -- interleaved with @bs@.