rerefined 0.4.0 → 0.5.0

raw patch · 9 files changed

+106/−54 lines, 9 filesdep ~basedep ~type-level-showPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, type-level-show

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• README.md +1/−1
• rerefined.cabal +6/−5
• src/Rerefined/Predicate/Logical.hs +6/−28
• src/Rerefined/Predicate/Logical/Equivalences.hs +0/−19
• src/Rerefined/Predicate/Logical/Normalize.hs +10/−0
• src/Rerefined/Predicate/Normalize.hs +12/−0
• src/Rerefined/Predicates/Operators.hs +67/−0
• src/Rerefined/Refine.hs +0/−1

@@ -1,3 +1,7 @@+## 0.5.0 (2024-05-26)+* add tentative operator versions of predicates+* clear up WIP normalization story+ ## 0.4.0 (2024-05-11) * add `Eq`, `Ord`, `Arbitrary` instances * simplify modules (fewer)

@@ -32,7 +32,7 @@ in the code).  rerefined has a single-constructor error type which can be easily and-efficiently turned into a `String` in a single pass.+efficiently turned into a string-like in a single pass.  ### No insidious `Typeable` contexts See [refined#101](https://github.com/nikita-volkov/refined/issues/101).

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.4.0+version:        0.5.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data@@ -19,7 +19,6 @@ tested-with:     GHC==9.8   , GHC==9.6-  , GHC==9.4 extra-source-files:     README.md     CHANGELOG.md@@ -37,20 +36,22 @@       Rerefined.Predicate.Fail       Rerefined.Predicate.Logical       Rerefined.Predicate.Logical.And-      Rerefined.Predicate.Logical.Equivalences       Rerefined.Predicate.Logical.If       Rerefined.Predicate.Logical.Iff       Rerefined.Predicate.Logical.Nand       Rerefined.Predicate.Logical.Nor+      Rerefined.Predicate.Logical.Normalize       Rerefined.Predicate.Logical.Not       Rerefined.Predicate.Logical.Or       Rerefined.Predicate.Logical.Xor+      Rerefined.Predicate.Normalize       Rerefined.Predicate.Relational       Rerefined.Predicate.Relational.Internal       Rerefined.Predicate.Relational.Length       Rerefined.Predicate.Relational.Value       Rerefined.Predicate.Succeed       Rerefined.Predicates+      Rerefined.Predicates.Operators       Rerefined.Refine       Rerefined.Refine.TH   other-modules:@@ -71,10 +72,10 @@   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:       QuickCheck >=2.14 && <2.16-    , base >=4.17 && <5+    , base >=4.18 && <5     , mono-traversable >=1.0.17.0 && <1.1     , template-haskell >=2.19.0.0 && <2.22     , text >=2.0 && <2.2     , text-builder-linear >=0.1.2 && <0.2-    , type-level-show >=0.1.0 && <0.2+    , type-level-show >=0.2.1 && <0.3   default-language: GHC2021

@@ -1,10 +1,12 @@-{-# LANGUAGE UndecidableInstances #-} -- TODO TMP+{- | Logical predicates. +Pretty predicates use infix propositional operators. This is chosen for+consistency. I'm not really sure which I prefer over all, perhaps best would be+to mix and match. Please let the maintainers know if you have a better idea.+-}+ module Rerefined.Predicate.Logical   ( And, Iff, If, Nand, Nor, Not, Or, Xor-  , NormalizeLogicalStep-  , NormalizeLogical1Step-  , Result(..), Idk1'   ) where  import Rerefined.Predicate.Logical.And@@ -15,27 +17,3 @@ import Rerefined.Predicate.Logical.Not import Rerefined.Predicate.Logical.Or import Rerefined.Predicate.Logical.Xor--import Data.Kind ( Type )--- left = continue, right = normalized-type NormalizeLogicalStep :: (kl -> kr -> Type) -> kl -> kr -> Result kl-type family NormalizeLogicalStep op l r where-    NormalizeLogicalStep Or   l l = Cont  l-    NormalizeLogicalStep And  l l = Cont  l-    NormalizeLogicalStep Nand l l = Cont1 (Not l)-    NormalizeLogicalStep op   l r = Done (op l r)--data Result kl = Done Type | Cont kl | Cont1 Type--type NormalizeLogical1Step :: (k -> Type) -> k -> Result k-type family NormalizeLogical1Step op p where-    NormalizeLogical1Step Not (Not p) = Cont p-    NormalizeLogical1Step op  p       = Done (op p)--type family Idk1 res where-    Idk1 (Cont p) = Idk1' p-    Idk1 (Done p) = p--type family Idk1' p where-    Idk1' (Not p) = Idk1 (NormalizeLogical1Step Not p)-    Idk1' p = p

@@ -1,19 +0,0 @@--- | Logical equivalences.--module Rerefined.Predicate.Logical.Equivalences where--{----- TODO-rerefineDeMorgans1-    :: Refined (Not (Logical Or  l r))       a-    -> Refined (Logical And (Not l) (Not r)) a-rerefineDeMorgans1 = unsafeRerefine---- TODO-rerefineDeMorgans2-    :: Refined (Not (Logical And l r))       a-    -> Refined (Logical Or  (Not l) (Not r)) a-rerefineDeMorgans2 = unsafeRerefine---}

@@ -0,0 +1,10 @@+module Rerefined.Predicate.Logical.Normalize where++import Rerefined.Predicate.Logical++type family NormLogi p where+    NormLogi (Not (Not p)) = Just p+    NormLogi (Or   l l)    = Just l+    NormLogi (And  l l)    = Just l+    NormLogi (Nand l l)    = Just (Not l)+    NormLogi p             = Nothing

@@ -0,0 +1,12 @@+{-# LANGUAGE UndecidableInstances #-}++module Rerefined.Predicate.Normalize where++import Rerefined.Predicate.Logical.Normalize++type family Norm p where+    Norm p = Norm' p (NormLogi p)++type family Norm' p mp where+    Norm' p Nothing   = p+    Norm' p (Just p') = Norm p'

@@ -0,0 +1,67 @@+{- | Predicate re-exports using operators.++We stick with non-operators for base predicate definitions because, very simply,+there aren't enough symbols to go around. The operators we would want to use for+logical predicates are already being used on the term level, and I forsee a+future full of promoted functions, so I wouldn't want to take up the type-level+name.++Instead, I'm providing operators in separate modules. It's not ideal, because+predicates already have operators defined in their pretty printing, and they may+not coincide with available Haskell symbols. I'm not really sure how to do all+this, it's very tentative for now.+-}++module Rerefined.Predicates.Operators+  (+  -- * Logical+  -- $logical+    type (.&&), type (.||)+  , type (.<->), type (.->)+  , type (.!&), type (.!|)+  , type (.!), type (.!=)++  -- * Relational+  , type (.<), type (.<=), type (.==), type (./=), type (.>=), type (.>)+  ) where++import Rerefined.Predicate.Logical+import Rerefined.Predicate.Relational.Internal++{- $logical++Awkward mix of Boolean and propositional operators. Sorry. Let me know if you+have a better idea.+-}++infixr 3 .&&+type (.&&) = And++infixr 2 .||+type (.||) = Or++infixr 3 .!&+type (.!&) = Nand++infix 9 .!+type (.!) = Not++infixr 2 .!|+type (.!|) = Nor++infixr 4 .!=+type (.!=) = Xor++infixr 4 .<->+type (.<->) = Iff++infixr 4 .->+type (.->) = If++infix 4 .<, .<=, .==, ./=, .>=, .>+type (.<)  = LT+type (.<=) = LTE+type (.==) =  EQ+type (./=) = NEQ+type (.>=) = GTE+type (.>)  = GT

@@ -1,4 +1,3 @@-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE AllowAmbiguousTypes #-} -- for predicate reification {-# LANGUAGE UndecidableInstances #-} -- for KnownPredicateName in Arbitrary