list-witnesses 0.1.3.1 → 0.1.3.2

raw patch · 4 files changed

+67/−13 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• list-witnesses.cabal +2/−2
• src/Data/Type/List/Edit.hs +34/−4
• src/Data/Type/List/Sublist.hs +20/−7

@@ -1,6 +1,17 @@ Changelog ========= +Version 0.1.3.2+---------------++*August 25, 2019*++<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.3.2>++*   Fixed overlapping instance issues resulting from ambiguities in `Auto`+    instances for `Insert`, `Delete`, `Substitute`, `Suffix`, `Interleave`, and+    `Subset`.+ Version 0.1.3.1 --------------- 

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 4055090befaa2d0679560c0b267262ff97d3c618a1503a0e4d5497fdbf73242d+-- hash: b5cd1b4dd5aa9afa7ec4fbf2fbfb27e461d5361e5bd05a2edf0ad347669f5c77  name:           list-witnesses-version:        0.1.3.1+version:        0.1.3.2 synopsis:       Witnesses for working with type-level lists description:    Collection of assorted inductive witnesses and functions for working with                 type-level lists.

@@ -106,10 +106,11 @@ -- @since 0.1.2.0 type IsInsert as bs = TyPred (Insert as bs) +-- | Prefers the "earlier" insert if there is ambiguity instance Auto (IsInsert as (x ': as)) x where     auto = InsZ -instance Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where+instance {-# INCOHERENT #-} 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@@ -184,6 +185,14 @@ -- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known -- statically. --+-- Prefers the earlier insertion if there is an ambiguity.+--+-- @+-- InsS InsZ        :: Insert '[1,2] '[1,2,2] 2+-- InsS (InsS InsZ) :: Insert '[1,2] '[1,2,2] 2+-- autoInsert @'[1,2] @'[1,2,2] @2 == InsS InsZ+-- @+-- -- @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@@ -225,10 +234,11 @@ -- @since 0.1.2.0 type IsDelete as bs = TyPred (Delete as bs) +-- | Prefers the "earlier" delete if there is ambiguity instance Auto (IsDelete (x ': as) as) x where     auto = DelZ -instance Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where+instance {-# INCOHERENT #-} 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@@ -263,6 +273,14 @@ -- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known -- statically. --+-- Prefers the earlier deletion if there is an ambiguity.+--+-- @+-- DelS DelZ        :: Delete '[1,2,2] '[1,2] 2+-- DelS (DelS DelZ) :: Delete '[1,2,2] '[1,2] 2+-- autoDelete @'[1,2,2] @'[1,2] @2 == DelS DelZ+-- @+-- -- @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@@ -306,17 +324,28 @@ instance Auto (IsSubstitute (x ': as) (y ': as) x) y where     auto = SubZ +-- | Prefers the earlier subsitution if there is ambiguity. instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where     auto = SubS (auto @_ @(IsSubstitute as bs x) @y) +instance {-# INCOHERENT #-} Auto (IsSubstitute (x ': as) (x ': as) x) x where+    auto = SubZ+ -- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are -- known statically. --+-- Prefers the "earlier" substitution if there is an ambiguity+--+-- @+-- SubZ      :: Substitute '[1,1] '[1,1] 1 1+-- SubS SubZ :: Substitute '[1,1] '[1,1] 1 1+-- autoSubstitute @'[1,1] @'[1,1] @1 @1 == SubZ+-- @+-- -- @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@@ -341,7 +370,8 @@ -- | An @'Edit' as bs@ is a reversible edit script transforming @as@ into -- @bs@ through successive insertions, deletions, and substitutions. ----- TODO: implement Wagner-Fischer to minimize find a minimal edit distance+-- TODO: implement Wagner-Fischer or something similar to minimize find+-- a minimal edit distance data Edit :: [k] -> [k] -> Type where     ENil :: Edit as as     EIns :: Insert bs cs x -> Edit as bs -> Edit as cs

@@ -187,10 +187,13 @@ -- @since 0.1.2.0 type IsSuffix as = TyPred (Suffix as) -instance Auto (IsSuffix as) as where+instance Auto (IsSuffix '[]) '[] where     auto = SufZ -instance Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where+instance {-# OVERLAPPABLE #-} Auto (IsSuffix (a ': as)) (a ': as) where+    auto = SufZ++instance {-# OVERLAPPABLE #-} 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@@ -603,10 +606,11 @@ instance Auto (IsInterleave '[] '[]) '[] where     auto = IntZ +-- | Prefers 'IntL' if there is an ambiguity. 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+instance {-# INCOHERENT #-} 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@@ -658,9 +662,18 @@                 IntL _ -> v Refl                 IntR _ -> u Refl --- | Automatically generate an 'Interleave' if @as@ and @bs@ are known--- statically.+-- | Automatically generate an 'Interleave' if @as@, @bs@, and @cs@ are+-- known statically. --+-- Prefers the left side if there is an ambiguity:+--+-- @+-- IntL (IntR (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]+-- IntR (IntL (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]+--+-- autoInterleave @'[1] @'[1,2] '[1,1,2] == IntL (IntR (IntR IntZ)+-- @+-- -- @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@@ -873,10 +886,10 @@ instance Auto (IsSubset '[]) '[] where     auto = SubsetNil -instance Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where+instance {-# OVERLAPPING #-} 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+instance {-# OVERLAPPING #-} 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