decidable 0.2.1.0 → 0.3.0.0

raw patch · 5 files changed

+176/−61 lines, 5 filesdep ~basedep ~functor-productsdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, functor-products, singletons

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−0
• decidable.cabal +6/−6
• src/Data/Type/Predicate.hs +114/−31
• src/Data/Type/Predicate/Auto.hs +42/−23
• src/Data/Type/Predicate/Logic.hs +0/−1

@@ -1,6 +1,20 @@ Changelog ========= +Version 0.3.0.0+---------------++*Feburary 2, 2020*++<https://github.com/mstksg/decidable/releases/tag/v0.3.0.0>++*   Update to work with *singletons-2.6*, the type family update+*   Change `Evident` to now be a defunctionalization symbol for `Sing`, instead+    of a type synonym with `TyPred`, to match with *singletons-2.6*.  Most code+    in practice should be the same.+*   Fix instances for `FProd`s: now can prove and decide any `FProd f (Wit p)`,+    and can prove and decide and auto any `FProd f WrappedSing`.+ Version 0.2.1.0 --------------- 

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 6ed0b9a421c5cd0cbd622790a067c8e7f30ed4bda6034a6471ad2064980be446+-- hash: d32fc68e2c0f9fc18f6d1c665774f308fc7e98fa1f9d71d0de5ffe287b57bae7  name:           decidable-version:        0.2.1.0+version:        0.3.0.0 synopsis:       Combinators for manipulating dependently-typed predicates. description:    This library provides combinators and typeclasses for working and manipulating                 type-level predicates in Haskell, which are represented as matchable type-level@@ -22,7 +22,7 @@ copyright:      (c) Justin Le 2018 license:        BSD3 license-file:   LICENSE-tested-with:    GHC >= 8.6+tested-with:    GHC >= 8.8 build-type:     Simple extra-source-files:     README.md@@ -47,9 +47,9 @@       src   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns   build-depends:-      base >=4.11 && <5-    , functor-products+      base >=4.13 && <5+    , functor-products >=0.1.1     , microlens-    , singletons >=2.5+    , singletons >=2.6     , vinyl   default-language: Haskell2010

@@ -134,7 +134,8 @@ -- @ -- 'Evident' :: 'Predicate' k -- @-type Evident = (TyPred Sing :: Predicate k)+data Evident :: Predicate k+type instance Apply Evident a = Sing a  -- | The always-false predicate --@@ -361,36 +362,118 @@ instance Provable Evident where     prove = id --- | @since 2.0.0-instance Provable (TyPred (Rec Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (Rec Sing))--- | @since 2.0.0-instance Provable (TyPred (PMaybe Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (PMaybe Sing))--- | @since 2.0.0-instance Provable (TyPred (NERec Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (NERec Sing))--- | @since 2.0.0-instance Provable (TyPred (PIdentity Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (PIdentity Sing))--- | @since 2.0.0-instance Provable (TyPred (PEither Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (PEither Sing))--- | @since 2.0.0-instance Provable (TyPred (PTup Sing)) where-    prove = singProd--- | @since 2.0.0-instance Decidable (TyPred (PTup Sing))+-- | @since 3.0.0+instance Decidable (TyPred WrappedSing)+-- | @since 3.0.0+instance Provable (TyPred WrappedSing) where+    prove = WrapSing+    ++-- | @since 3.0.0+instance Provable p => Provable (TyPred (Rec (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (Rec (Wit p))) where+    decide = \case+      SNil         -> Proved RNil+      x `SCons` xs -> case decide @p x of+        Proved p -> case decideTC xs of+          Proved ps -> Proved $ Wit p :& ps+          Disproved vs -> Disproved $ \case+            _ :& ps -> vs ps+        Disproved v -> Disproved $ \case+          Wit p :& _ -> v p++-- | @since 3.0.0+instance Provable (TyPred (Rec WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (Rec WrappedSing))++-- | @since 3.0.0+instance Provable p => Provable (TyPred (PMaybe (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where+    decide = \case+      SNothing -> Proved PNothing+      SJust x  -> mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)+                . decide @p+                $ x++-- | @since 3.0.0+instance Provable (TyPred (PMaybe WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (PMaybe WrappedSing))++-- | @since 3.0.0+instance Provable p => Provable (TyPred (NERec (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (NERec (Wit p))) where+    decide = \case+      x NE.:%| xs -> case decide @p x of+        Proved p -> case decideTC xs of+          Proved ps -> Proved $ Wit p :&| ps+          Disproved vs -> Disproved $ \case+            _ :&| ps -> vs ps+        Disproved v -> Disproved $ \case+          Wit p :&| _ -> v p++-- | @since 3.0.0+instance Provable (TyPred (NERec WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (NERec WrappedSing))++-- | @since 3.0.0+instance Provable p => Provable (TyPred (PIdentity (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where+    decide = \case+      SIdentity x -> mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)+                   . decide @p+                   $ x++-- | @since 3.0.0+instance Provable (TyPred (PIdentity WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (PIdentity WrappedSing))++-- | @since 3.0.0+instance Provable p => Provable (TyPred (PEither (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (PEither (Wit p))) where+    decide = \case+      SLeft  x -> Proved $ PLeft x+      SRight y -> mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)+                . decide @p+                $ y++-- | @since 3.0.0+instance Provable (TyPred (PEither WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (PEither WrappedSing))++-- | @since 3.0.0+instance Provable p => Provable (TyPred (PTup (Wit p))) where+    prove = mapProd (Wit . prove @p) . singProd+-- | @since 3.0.0+instance Decidable p => Decidable (TyPred (PTup (Wit p))) where+    decide (STuple2 x y) = mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)+                         . decide @p+                         $ y++-- | @since 3.0.0+instance Provable (TyPred (PTup WrappedSing)) where+    prove = mapProd WrapSing . singProd+-- | @since 3.0.0+instance Decidable (TyPred (PTup WrappedSing))  instance (Decidable p, SingI f) => Decidable (PMap f p) where     decide = decide @p . applySing (sing :: Sing f)

@@ -180,7 +180,7 @@     autoElem = IId  instance AutoElem f as a => Auto (In f as) a where-    auto = autoElem @f @as @a+    auto = autoElem @_ @f @as @a  -- | Helper class for deriving 'Auto' instances for 'All' predicates; each -- 'Universe' instance is expected to implement these if possible, to get@@ -200,7 +200,7 @@ instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where     autoAll = WitAll $ \case         IZ   -> auto @_ @p @a-        IS i -> runWitAll (autoAll @[] @p @as) i+        IS i -> runWitAll (autoAll @_ @[] @p @as) i  instance AutoAll Maybe p 'Nothing where     autoAll = WitAll $ \case {}@@ -217,7 +217,7 @@ instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where     autoAll = WitAll $ \case         NEHead   -> auto @_ @p @a-        NETail i -> runWitAll (autoAll @[] @p @as) i+        NETail i -> runWitAll (autoAll @_ @[] @p @as) i  instance Auto p a => AutoAll ((,) j) p '(w, a) where     autoAll = WitAll $ \case ISnd -> auto @_ @p @a@@ -227,7 +227,7 @@  -- | @since 0.1.2.0 instance AutoAll f p as => Auto (All f p) as where-    auto = autoAll @f @p @as+    auto = autoAll @_ @f @p @as  -- | @since 0.1.2.0 instance SingI a => Auto (NotNull []) (a ': as) where@@ -301,7 +301,7 @@  -- | @since 0.1.2.0 instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where-    auto = allNotNone sing $ autoAll @f @(Not p) @as+    auto = allNotNone sing $ autoAll @_ @f @(Not p) @as  -- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out -- a specific @a@ in @as@ where the predicate is disprovable at compile-time.@@ -321,21 +321,40 @@     auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))          $ auto @_ @(Not (Any f (Found p))) @as --- | @since 2.0.0-instance SingI as => Auto (TyPred (Rec Sing)) as where-    auto = singProd sing--- | @since 2.0.0-instance SingI as => Auto (TyPred (PMaybe Sing)) as where-    auto = singProd sing--- | @since 2.0.0-instance SingI as => Auto (TyPred (NERec Sing)) as where-    auto = singProd sing--- | @since 2.0.0-instance SingI as => Auto (TyPred (PEither Sing)) as where-    auto = singProd sing--- | @since 2.0.0-instance SingI as => Auto (TyPred (PTup Sing)) as where-    auto = singProd sing--- | @since 2.0.0-instance SingI as => Auto (TyPred (PIdentity Sing)) as where-    auto = singProd sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (Rec WrappedSing)) as where+    auto = proveTC sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where+    auto = proveTC sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (NERec WrappedSing)) as where+    auto = proveTC sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (PEither WrappedSing)) as where+    auto = proveTC sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (PTup WrappedSing)) as where+    auto = proveTC sing+-- | @since 3.0.0+instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where+    auto = proveTC sing++-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where+    auto = proveTC sing+-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where+    auto = proveTC sing+-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where+    auto = proveTC sing+-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where+    auto = proveTC sing+-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where+    auto = proveTC sing+-- | @since 3.0.0+instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where+    auto = proveTC sing

@@ -42,7 +42,6 @@  import           Data.Singletons import           Data.Singletons.Decide-import           Data.Singletons.Prelude.Bool (Sing(..)) import           Data.Type.Predicate import           Data.Void