rerefined 0.6.0 → 0.7.0

raw patch · 12 files changed

+395/−108 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• rerefined.cabal +3/−3
• src/Rerefined/Predicate/Logical/Normalize.hs +0/−10
• src/Rerefined/Predicate/Normalize.hs +0/−12
• src/Rerefined/Predicate/Relational.hs +4/−2
• src/Rerefined/Predicate/Relational/Internal.hs +48/−72
• src/Rerefined/Predicate/Relational/Length.hs +1/−1
• src/Rerefined/Predicate/Relational/Value.hs +1/−1
• src/Rerefined/Predicates.hs +1/−1
• src/Rerefined/Predicates/Operators.hs +6/−6
• src/Rerefined/Simplify.hs +277/−0
• src/Rerefined/Simplify/Relational.hs +50/−0

@@ -1,3 +1,7 @@+## 0.7.0 (2024-10-11)+* add predicate simplifier at `Rerefined.Simplify`+  * old "normalizer" stuff removed+ ## 0.6.0 (2024-10-01) * remove `Via` predicate, only need `validateVia` * swap `validateBool` args

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.6.0+version:        0.7.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data@@ -40,11 +40,9 @@       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@@ -55,6 +53,8 @@       Rerefined.Predicates.Operators       Rerefined.Refine       Rerefined.Refine.TH+      Rerefined.Simplify+      Rerefined.Simplify.Relational   other-modules:       Paths_rerefined   hs-source-dirs:

@@ -1,10 +0,0 @@-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

@@ -1,12 +0,0 @@-{-# 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'

@@ -1,8 +1,10 @@ module Rerefined.Predicate.Relational-  ( CompareValue+  ( RelOp(..)+  , CompareValue   , Sign(..)   , CompareLength-  , LTE, GTE+  , WidenRelOp+  , FlipRelOp   ) where  import Rerefined.Predicate.Relational.Internal

@@ -1,111 +1,87 @@ {-# LANGUAGE AllowAmbiguousTypes #-}  -- for ReifyRelOp {-# LANGUAGE UndecidableInstances #-} -- for WidenRelOp -{- | Relational operator definitions.--Haskell base exports the type 'Ordering', which is an enum that states the-result of comparing two 'Ord's. We can utilize this to define /relational-operators/:--* 'LT', 'EQ' and 'GT' already map to relational operators.-* The others can be defined by combining the above with 'Or'. e.g. @'LT' ``Or``-  'EQ'@ -> "less than or equal" ('<=')--What's the point? We save on definitions, and get to reuse well-known data types-which most users will have intuition for. We do have to contest with-commutativity, but this is an extremely minor concern which can only come up if-you don't use the provided type synonyms, or do lots of type-level predicate-manipulation. And we provide those swapped-order instances anyway!--}+-- | Relational operator definitions.  module Rerefined.Predicate.Relational.Internal where -import Rerefined.Predicate.Logical.Or import GHC.TypeNats import Data.Type.Ord ( OrdCond ) import GHC.TypeLits ( Symbol ) -import Data.Kind ( Type )--type LTE = LT `Or` EQ+{- | Relational operator. --- | "not equal to" is equivalent to "strictly less than or greater than". We---   could use 'Rerefined.Predicate.Logical.Not.Not', but sticking with just---   'Or' keeps the internals simple.-type NEQ = LT `Or` GT+Constructor order is arbitrary due to @NEQ@, which obstructs ordering in a+meaningful way. -type GTE = GT `Or` EQ+Note that these operators may be defined by combining 'Ordering's in certain+ways: for example @'LT' OR 'EQ'@ could be @LTE@, @'LT' OR 'GT'@ could be @NEQ@.+This is convenient for user intuition, permitting the use of e.g. 'LT' as a+relational operator directly. However, it complicates type-level work, as now we+can't restrict relational operators to a given kind, and we have to handle+non-standard orderings like @'GT' OR 'LT'@.+-}+data RelOp+  = RelOpEQ  -- ^ @==@              equal to+  | RelOpNEQ -- ^ @/=@ less than             or greater than (also not equal to)+  | RelOpLT  -- ^ @<@  less than+  | RelOpLTE -- ^ @<=@ less than or equal to+  | RelOpGTE -- ^ @>=@              equal to or greater than+  | RelOpGT  -- ^ @>@                           greater than --- | Reify a relational operator type tag.------ Permitted operators are @Ordering@ constructors 'LT', 'EQ' and 'GT'; and--- combinations of these using 'Or'.-class ReifyRelOp op where+-- | Reify a 'RelOp'.+class ReifyRelOp (op :: RelOp) where     -- | Pretty @op@.     type ShowRelOp op :: Symbol -    -- | The term-level relational operator that @op@ describes.+    -- | The term-level relational operator that @op :: 'RelOp'@ describes.     reifyRelOp :: forall a. Ord a => a -> a -> Bool -instance ReifyRelOp LT where-    type ShowRelOp LT = "<"+instance ReifyRelOp RelOpLT  where+    type ShowRelOp RelOpLT  = "<"     reifyRelOp = (<) -instance ReifyRelOp LTE where-    type  ShowRelOp LTE = "<="+instance ReifyRelOp RelOpLTE where+    type ShowRelOp RelOpLTE = "<="     reifyRelOp = (<=) --- | Hidden instance. You won't see this if you use the type synonyms.-deriving via LTE instance ReifyRelOp (EQ `Or` LT)--instance ReifyRelOp EQ where-    type  ShowRelOp EQ = "=="+instance ReifyRelOp RelOpEQ  where+    type ShowRelOp RelOpEQ  = "=="     reifyRelOp = (==) -instance ReifyRelOp NEQ where-    type  ShowRelOp NEQ = "/="+instance ReifyRelOp RelOpNEQ where+    type ShowRelOp RelOpNEQ = "/="     reifyRelOp = (/=) --- | Hidden instance. You won't see this if you use the type synonyms.-deriving via NEQ instance ReifyRelOp (GT `Or` LT)--instance ReifyRelOp GTE where-    type ShowRelOp GTE = ">="+instance ReifyRelOp RelOpGTE where+    type ShowRelOp RelOpGTE = ">="     reifyRelOp = (>=) --- | Hidden instance. You won't see this if you use the type synonyms.-deriving via GTE instance ReifyRelOp (EQ `Or` GT)--instance ReifyRelOp GT where-    type ShowRelOp GT = ">"+instance ReifyRelOp RelOpGT  where+    type ShowRelOp RelOpGT  = ">"     reifyRelOp = (>)  -- | Can we widen the given 'RelOp' on the given 'Natural' from @n@ to @m@?-type WidenRelOp :: k -> Natural -> Natural -> Bool+type WidenRelOp :: RelOp -> Natural -> Natural -> Bool type family WidenRelOp op n m where     -- @n == m@? no problem     WidenRelOp op  n n = True      -- I'd love to simplify this, but 'CmpNat' is opaque.-    WidenRelOp LT  n m = OrdCond (CmpNat n m) True  True False-    WidenRelOp LTE n m = OrdCond (CmpNat n m) True  True False-    WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True-    WidenRelOp GT  n m = OrdCond (CmpNat n m) False True True--    -- | swapped LTE, lower down in equation list because less common-    WidenRelOp (EQ `Or` LT) n m =-        OrdCond (CmpNat n m) True  True False--    -- | swapped GTE, lower down in equation list because less common-    WidenRelOp (EQ `Or` GT) n m =-        OrdCond (CmpNat n m) False True True+    WidenRelOp RelOpLT  n m = OrdCond (CmpNat n m) True  True False+    WidenRelOp RelOpLTE n m = OrdCond (CmpNat n m) True  True False+    WidenRelOp RelOpGTE n m = OrdCond (CmpNat n m) False True True+    WidenRelOp RelOpGT  n m = OrdCond (CmpNat n m) False True True      -- can't widen (==) or (/=)-    WidenRelOp _   _ _ = False+    WidenRelOp op n m = False --- this gets clumsier due to kinding clashes (k vs. Ordering)-type NormalizeOrRelOp :: Type -> Type-type family NormalizeOrRelOp op where-    NormalizeOrRelOp (EQ `Or` LT) = LTE-    NormalizeOrRelOp (GT `Or` LT) = NEQ-    NormalizeOrRelOp (EQ `Or` GT) = GTE+-- | Flip a 'RelOp' to give the opposite comparison.+type FlipRelOp :: RelOp -> RelOp+type family FlipRelOp op where+    FlipRelOp RelOpEQ  = RelOpNEQ+    FlipRelOp RelOpNEQ = RelOpEQ+    FlipRelOp RelOpLT  = RelOpGTE+    FlipRelOp RelOpLTE = RelOpGT+    FlipRelOp RelOpGTE = RelOpLT+    FlipRelOp RelOpGT  = RelOpLTE

@@ -17,7 +17,7 @@ import Data.Text.Builder.Linear qualified as TBL  -- | Compare length to a type-level 'Natural' using the given 'RelOp'.-data CompareLength op (n :: Natural)+data CompareLength (op :: RelOp) (n :: Natural)  -- | Precedence of 4 (matching base relational operators e.g. '>='). instance Predicate (CompareLength op n) where

@@ -12,7 +12,7 @@ import GHC.TypeLits ( Symbol )  -- | Compare value to a type-level 'Natural' using the given 'RelOp'.-data CompareValue op (sign :: Sign) (n :: Natural)+data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)  -- | Precedence of 4 (matching base relational operators e.g. '>='). instance Predicate (CompareValue op sign n) where

@@ -11,10 +11,10 @@   , And, Iff, If, Nand, Nor, Not, Or, Xor    -- * Relational+  , RelOp(..)   , CompareValue   , Sign(..)   , CompareLength-  , LTE, GTE   ) where  import Rerefined.Predicate.Succeed

@@ -59,9 +59,9 @@ type (.->) = If  infix 4 .<, .<=, .==, ./=, .>=, .>-type (.<)  = LT-type (.<=) = LTE-type (.==) =  EQ-type (./=) = NEQ-type (.>=) = GTE-type (.>)  = GT+type (.<)  = RelOpLT+type (.<=) = RelOpLTE+type (.==) = RelOpEQ+type (./=) = RelOpNEQ+type (.>=) = RelOpGTE+type (.>)  = RelOpGT

@@ -0,0 +1,277 @@+{-# LANGUAGE UndecidableInstances #-}++{- | Primitive predicate simplifier.++This is related to an NP-complete problem (see Boolean satisfiability problem).+We focus on /immediate, operation-reducing simplifications/, and hope that the+input is formed in such a way that our rules match.++In short, the simplifier is largely contextless. It inspects (usually) a single+layer/depth at a time. So we can consistently simplify things like logical+identities. But don't expect simplifications hard to spot with the naked eye.++The simplifier may not be expectected to consistently implement any+transformations whatsoever. The only guarantees are++* the output has the same or fewer operations+* the output meaning is identical to the input++Implementation pitfalls:++* not extensible: only works for built-in logical & relational predicates+* no protection against non-termination e.g. if a pair of transformations loop+* very tedious to write. that's life+-}++module Rerefined.Simplify+  ( Simplify+  , SimplifyStep+  ) where++import Rerefined.Predicate.Succeed+import Rerefined.Predicate.Fail++import Rerefined.Predicate.Logical++import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp )+import Rerefined.Simplify.Relational+  ( SimplifyCompareLength+  , SimplifyCompareLengthAnd+  , SimplifyCompareLengthOr+  )++import Data.Kind ( Type )++-- note that we can't modularize logical simplifications because they're+-- mutually recursive with the main simplifier :(++-- | Simplify the given predicate.+--+-- Returns the input predicate if we were unable to simplify.+type Simplify :: Type -> Type+type Simplify p = Simplify' p++-- | Helper definition for reducing duplication.+type Simplify' p = SimplifyLoop p (SimplifyStep p)++-- | Simplification loop.+type family SimplifyLoop p mp where+    -- simplification step succeeded: try again on the simplified predicate+    SimplifyLoop p (Just p') = Simplify' p'++    -- failed to simplify: give up, return the latest predicate+    SimplifyLoop p Nothing   = p++-- | Try to perform a single simplification step on the given predicate.+--+-- Returns 'Nothing' if we were unable to simplify.+type family SimplifyStep p where+    SimplifyStep (Not  p)   = SimplifyNot  p++    SimplifyStep (And  l r) = SimplifyAnd  l r+    SimplifyStep (Or   l r) = SimplifyOr   l r+    SimplifyStep (Nand l r) = SimplifyNand l r+    SimplifyStep (Nor  l r) = SimplifyNor  l r+    SimplifyStep (Iff  l r) = SimplifyIff  l r+    SimplifyStep (Xor  l r) = SimplifyXor  l r+    SimplifyStep (If   l r) = SimplifyIf   l r++    SimplifyStep (CompareLength op n) = SimplifyCompareLength op n+    -- Don't think we can do anything for CompareValue.++    SimplifyStep p = Nothing++type family SimplifyAnd l r where+    -- identity laws+    SimplifyAnd p       Fail    = Just Fail+    SimplifyAnd Fail    p       = Just Fail+    SimplifyAnd p       Succeed = Just p+    SimplifyAnd Succeed p       = Just p++    SimplifyAnd p p = Just p++    -- distributivity+    SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z))++    -- special+    SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) =+        SimplifyCompareLengthAnd lop ln rop rn++    -- recurse+    SimplifyAnd l r =+        (OrElseAndL r (SimplifyStep l)+            (OrElseAndR l (SimplifyStep r)+                Nothing))++type family OrElseAndL r mp cont where+    OrElseAndL r Nothing   cont = cont+    OrElseAndL r (Just l') cont = Just (And l' r)++type family OrElseAndR l mp cont where+    OrElseAndR l Nothing   cont = cont+    OrElseAndR l (Just r') cont = Just (And l r')++type family SimplifyOr l r where+    -- identity laws+    SimplifyOr Succeed p       = Just Succeed+    SimplifyOr p       Succeed = Just Succeed+    SimplifyOr Fail    p       = Just p+    SimplifyOr p       Fail    = Just p++    SimplifyOr p p = Just p++    -- distributivity+    SimplifyOr (And x y) (And x z) = Just (And x (Or y z))++    -- special relational+    SimplifyOr (CompareLength lop ln) (CompareLength rop rn) =+        SimplifyCompareLengthOr lop ln rop rn++    -- recurse+    SimplifyOr l r =+        (OrElseOrL r (SimplifyStep l)+            (OrElseOrR l (SimplifyStep r)+                Nothing))++type family OrElseOrL r mp cont where+    OrElseOrL r Nothing   cont = cont+    OrElseOrL r (Just l') cont = Just (Or l' r)++type family OrElseOrR l mp cont where+    OrElseOrR l Nothing   cont = cont+    OrElseOrR l (Just r') cont = Just (Or l r')++type family SimplifyNand l r where+    -- identity laws+    SimplifyNand Fail    p       = Just Succeed+    SimplifyNand p       Fail    = Just Succeed+    SimplifyNand Succeed p       = Just (Not p)+    SimplifyNand p       Succeed = Just (Not p)++    SimplifyNand p p = Just (Not p)++    -- recurse+    SimplifyNand l r =+        (OrElseNandL r (SimplifyStep l)+            (OrElseNandR l (SimplifyStep r)+                Nothing))++type family OrElseNandL r mp cont where+    OrElseNandL r Nothing   cont = cont+    OrElseNandL r (Just l') cont = Just (Nand l' r)++type family OrElseNandR l mp cont where+    OrElseNandR l Nothing   cont = cont+    OrElseNandR l (Just r') cont = Just (Nand l r')++type family SimplifyNor l r where+    -- identity laws+    SimplifyNor Succeed p       = Just Fail+    SimplifyNor p       Succeed = Just Fail+    SimplifyNor Fail    p       = Just (Not p)+    SimplifyNor p       Fail    = Just (Not p)++    SimplifyNor p p = Just (Not p)++    -- recurse+    SimplifyNor l r =+        (OrElseNorL r (SimplifyStep l)+            (OrElseNorR l (SimplifyStep r)+                Nothing))++type family OrElseNorL r mp cont where+    OrElseNorL r Nothing   cont = cont+    OrElseNorL r (Just l') cont = Just (Nor l' r)++type family OrElseNorR l mp cont where+    OrElseNorR l Nothing   cont = cont+    OrElseNorR l (Just r') cont = Just (Nor l r')++type family SimplifyXor l r where+    -- identity laws+    SimplifyXor Fail    p       = Just p+    SimplifyXor p       Fail    = Just p+    SimplifyXor Succeed p       = Just (Not p)+    SimplifyXor p       Succeed = Just (Not p)++    SimplifyXor p p = Just Fail++    -- recurse+    SimplifyXor l r =+        (OrElseXorL r (SimplifyStep l)+            (OrElseXorR l (SimplifyStep r)+                Nothing))++type family OrElseXorL r mp cont where+    OrElseXorL r Nothing   cont = cont+    OrElseXorL r (Just l') cont = Just (Xor l' r)++type family OrElseXorR l mp cont where+    OrElseXorR l Nothing   cont = cont+    OrElseXorR l (Just r') cont = Just (Xor l r')++type family SimplifyIf l r where+    -- identity laws+    SimplifyIf Fail    p       = Just Succeed+    SimplifyIf p       Fail    = Just Succeed+    SimplifyIf Succeed p       = Just p+    SimplifyIf p       Succeed = Just p++    SimplifyIf p p = Just Succeed++    -- recurse+    SimplifyIf l r =+        (OrElseIfL r (SimplifyStep l)+            (OrElseIfR l (SimplifyStep r)+                Nothing))++type family OrElseIfL r mp cont where+    OrElseIfL r Nothing   cont = cont+    OrElseIfL r (Just l') cont = Just (If l' r)++type family OrElseIfR l mp cont where+    OrElseIfR l Nothing   cont = cont+    OrElseIfR l (Just r') cont = Just (If l r')++type family SimplifyIff l r where+    -- identity laws+    SimplifyIff Succeed p       = Just p+    SimplifyIff p       Succeed = Just p+    SimplifyIff Fail    p       = Just (Not p)+    SimplifyIff p       Fail    = Just (Not p)++    SimplifyIff p p = Just Succeed++    -- recurse+    SimplifyIff l r =+        (OrElseIffL r (SimplifyStep l)+            (OrElseIffR l (SimplifyStep r)+                Nothing))++type family OrElseIffL r mp cont where+    OrElseIffL r Nothing   cont = cont+    OrElseIffL r (Just l') cont = Just (Iff l' r)++type family OrElseIffR l mp cont where+    OrElseIffR l Nothing   cont = cont+    OrElseIffR l (Just r') cont = Just (Iff l r')++type family SimplifyNot p where+    -- double negation+    SimplifyNot (Not p) = Just p++    SimplifyNot Succeed = Just Fail+    SimplifyNot Fail    = Just Succeed++    -- special relational+    SimplifyNot (CompareLength op      n) =+        Just (CompareLength (FlipRelOp op)      n)+    SimplifyNot (CompareValue  op sign n) =+        Just (CompareValue  (FlipRelOp op) sign n)++    -- recurse+    SimplifyNot p = OrElseNot (SimplifyStep p) Nothing++type family OrElseNot mp cont where+    OrElseNot (Just p') cont = Just (Not p')+    OrElseNot Nothing   cont = cont

@@ -0,0 +1,50 @@+{-# LANGUAGE UndecidableInstances #-}++module Rerefined.Simplify.Relational where++import Rerefined.Predicate.Succeed+import Rerefined.Predicate.Fail++import Rerefined.Predicate.Relational+import GHC.TypeNats ( Natural, CmpNat )+import Data.Type.Ord ( OrdCond )++type family SimplifyCompareLength (op :: RelOp) (n :: Natural) where+    SimplifyCompareLength RelOpLT  0 = Just Fail+    SimplifyCompareLength RelOpLTE 0 = Just (CompareLength RelOpEQ 0)+    SimplifyCompareLength RelOpGTE 0 = Just Succeed+    SimplifyCompareLength RelOpGT  0 = Just (CompareLength RelOpEQ 0)++    SimplifyCompareLength op n = Nothing++type family SimplifyCompareLengthAnd+  (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where+    -- @<n AND >m@: @n<=m@ -> False+    SimplifyCompareLengthAnd RelOpLT  n RelOpGT  m =+        OrdCond (CmpNat n m)+            (Just Fail)+            (Just Fail)+            Nothing+    SimplifyCompareLengthAnd RelOpGT  m RelOpLT  n =+        OrdCond (CmpNat n m)+            (Just Fail)+            (Just Fail)+            Nothing++    SimplifyCompareLengthAnd lop ln rop rn = Nothing++type family SimplifyCompareLengthOr+  (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where+    -- @<n OR  >m@: @n==m@ -> NEQ; @n>m@ -> True (?)+    SimplifyCompareLengthOr RelOpLT  n RelOpGT  m =+        OrdCond (CmpNat n m)+            Nothing+            (Just (CompareLength RelOpNEQ n))+            (Just Succeed)+    SimplifyCompareLengthOr RelOpGT  m RelOpLT  n =+        OrdCond (CmpNat n m)+            Nothing+            (Just (CompareLength RelOpNEQ n))+            (Just Succeed)++    SimplifyCompareLengthOr lop ln rop rn = Nothing