**diff options**

author | jle <> | 2019-08-13 07:24:00 (GMT) |
---|---|---|

committer | hdiff <hdiff@hdiff.luite.com> | 2019-08-13 07:24:00 (GMT) |

commit | b90f1e23930a398b869f16060f8ed0145d87db2c (patch) | |

tree | 454dc79c110c4f8f2a98047d77dcf84c0a7ce6f3 | |

parent | c40a10ee95e0ce53c845657bdbe5cde3e19ba62d (diff) |

-rw-r--r-- | CHANGELOG.md | 13 | ||||

-rw-r--r-- | list-witnesses.cabal | 9 | ||||

-rw-r--r-- | src/Data/Type/List/Edit.hs | 219 | ||||

-rw-r--r-- | src/Data/Type/List/Sublist.hs | 383 |

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@. -- |