summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorjle <>2019-08-13 07:24:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-08-13 07:24:00 (GMT)
commitb90f1e23930a398b869f16060f8ed0145d87db2c (patch)
tree454dc79c110c4f8f2a98047d77dcf84c0a7ce6f3
parentc40a10ee95e0ce53c845657bdbe5cde3e19ba62d (diff)
version 0.1.2.0HEAD0.1.2.0master
-rw-r--r--CHANGELOG.md13
-rw-r--r--list-witnesses.cabal9
-rw-r--r--src/Data/Type/List/Edit.hs219
-rw-r--r--src/Data/Type/List/Sublist.hs383
4 files changed, 578 insertions, 46 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5cb4632..45d935e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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
---------------
diff --git a/list-witnesses.cabal b/list-witnesses.cabal
index 739c2d7..a61a6e5 100644
--- a/list-witnesses.cabal
+++ b/list-witnesses.cabal
@@ -4,10 +4,10 @@ cabal-version: 1.12
--
-- 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 @@ maintainer: justin@jle.im
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 @@ library
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
diff --git a/src/Data/Type/List/Edit.hs b/src/Data/Type/List/Edit.hs
index 6ac53e7..6a14d30 100644
--- a/src/Data/Type/List/Edit.hs
+++ b/src/Data/Type/List/Edit.hs
@@ -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 @@ module Data.Type.List.Edit (
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 @@ data Insert :: [k] -> [k] -> k -> Type where
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 @@ data Delete :: [k] -> [k] -> k -> Type where
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 @@ data Substitute :: [k] -> [k] -> k -> k -> Type where
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 @@ instance C.Category Edit where
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 @@ deleteRec = \case
-- 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 @@ type family SuccSubstitutedIx b bs x y z (s :: SubstitutedIx bs x y z) :: Substi
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)
diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs
index 3503444..4ee8049 100644
--- a/src/Data/Type/List/Sublist.hs
+++ b/src/Data/Type/List/Sublist.hs
@@ -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 @@ prefixLens p = prefixToAppend p $ \a -> splitRecIso a . _1
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 @@ data Suffix :: [k] -> [k] -> Type where
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 @@ data Append :: [k] -> [k] -> [k] -> Type where
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 @@ shiftIndex = \case
-- @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 @@ data Interleave :: [k] -> [k] -> [k] -> Type where
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
@@ -324,6 +658,19 @@ unweaveRec = \case
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@.
--