rerefined 0.7.0 → 0.8.0

raw patch · 6 files changed

+367/−239 lines, 6 filesdep +rerefineddep +type-specPVP ok

version bump matches the API change (PVP)

Dependencies added: rerefined, type-spec

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• rerefined.cabal +34/−2
• src/Rerefined/Simplify.hs +27/−237
• src/Rerefined/Simplify/Core.hs +251/−0
• src/Rerefined/Simplify/Relational.hs +8/−0
• test/Main.hs +44/−0

@@ -1,3 +1,6 @@+## 0.8.0 (2024-10-12)+* tweak `Simplify` exports (should stay fairly stable now)+ ## 0.7.0 (2024-10-11) * add predicate simplifier at `Rerefined.Simplify`   * old "normalizer" stuff removed

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.7.0+version:        0.8.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data@@ -54,6 +54,7 @@       Rerefined.Refine       Rerefined.Refine.TH       Rerefined.Simplify+      Rerefined.Simplify.Core       Rerefined.Simplify.Relational   other-modules:       Paths_rerefined@@ -70,7 +71,7 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall -Wno-unticked-promoted-constructors+  ghc-options: -fhide-source-paths -Wall   build-depends:       QuickCheck >=2.14 && <2.16     , base >=4.18 && <5@@ -79,4 +80,35 @@     , text >=2.0 && <2.2     , text-builder-linear >=0.1.2 && <0.2     , type-level-show >=0.2.1 && <0.4+  default-language: GHC2021++test-suite spec+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      Paths_rerefined+  hs-source-dirs:+      test+  default-extensions:+      LambdaCase+      NoStarIsType+      DerivingVia+      DeriveAnyClass+      GADTs+      RoleAnnotations+      DefaultSignatures+      TypeFamilies+      DataKinds+      MagicHash+  ghc-options: -fhide-source-paths -Wall+  build-depends:+      QuickCheck >=2.14 && <2.16+    , base >=4.18 && <5+    , mono-traversable >=1.0.17.0 && <1.1+    , rerefined+    , template-haskell >=2.19.0.0 && <2.23+    , text >=2.0 && <2.2+    , text-builder-linear >=0.1.2 && <0.2+    , type-level-show >=0.2.1 && <0.4+    , type-spec >=0.4.0.0 && <0.5   default-language: GHC2021

@@ -2,53 +2,30 @@  {- | 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+See 'Rerefined.Simplify.Core' (internal module) for more details. -}  module Rerefined.Simplify   ( Simplify-  , SimplifyStep+  , TrySimplify+  , AssertSimplified   ) 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 )+import Rerefined.Simplify.Core ( SimplifyStep ) --- note that we can't modularize logical simplifications because they're--- mutually recursive with the main simplifier :(+import Data.Kind ( type Constraint )+import GHC.TypeError ( type TypeError, type ErrorMessage(..) )+import Rerefined.Predicate ( type PredicateName )  -- | 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.@@ -62,216 +39,29 @@     -- failed to simplify: give up, return the latest predicate     SimplifyLoop p Nothing   = p --- | Try to perform a single simplification step on the given predicate.+-- | Try to simplify 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+type TrySimplify p = TrySimplifyLoop p (SimplifyStep p) -    SimplifyNot Succeed = Just Fail-    SimplifyNot Fail    = Just Succeed+-- | Simplification loop which returns 'Nothing' for 0 simplifications.+type family TrySimplifyLoop p mp where+    -- got a simplification: continue with the regular simplifier+    TrySimplifyLoop p (Just p') = Just (Simplify' p') -    -- special relational-    SimplifyNot (CompareLength op      n) =-        Just (CompareLength (FlipRelOp op)      n)-    SimplifyNot (CompareValue  op sign n) =-        Just (CompareValue  (FlipRelOp op) sign n)+    -- couldn't simplify+    TrySimplifyLoop p Nothing   = Nothing -    -- recurse-    SimplifyNot p = OrElseNot (SimplifyStep p) Nothing+-- | Assert that a predicate may not be trivially simplified.+--+-- Returns the empty constraint on success, else emits a pretty type error.+--+-- Useful e.g. if you'd like to make sure a user isn't writing silly predicates.+type AssertSimplified p = AssertSimplified' p (TrySimplify p) -type family OrElseNot mp cont where-    OrElseNot (Just p') cont = Just (Not p')-    OrElseNot Nothing   cont = cont+type family AssertSimplified' p mp' :: Constraint where+    AssertSimplified' p Nothing   = ()+    AssertSimplified' p (Just p') = TypeError+        (    Text "Predicate is trivially simplifiable"+        :$$: Text "   " :<>: Text (PredicateName 0 p)+        :$$: Text "-> " :<>: Text (PredicateName 0 p') )

@@ -0,0 +1,251 @@+{-# LANGUAGE UndecidableInstances #-}++{- | Core predicate simplification algorithm.++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.++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++__Internal module. Exports may change without warning. Try not to use.__+-}++module Rerefined.Simplify.Core 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+  )++-- note that we can't modularize logical simplifications because they're+-- mutually recursive with the main simplifier :(++-- | 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

@@ -1,5 +1,13 @@ {-# LANGUAGE UndecidableInstances #-} +{- | Relational predicate simplification.++These bits aren't mutually recursive with the main simplifier, so we can keep+them separate for a bit of code hygiene.++__Internal module. Exports may change without warning. Try not to use.__+-}+ module Rerefined.Simplify.Relational where  import Rerefined.Predicate.Succeed

@@ -0,0 +1,44 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++module Main where++import Test.TypeSpec hiding ( And )+import Rerefined.Simplify+import Rerefined.Predicates+import Rerefined.Predicate+import TypeLevelShow.Utils ( type (++) )++-- | Pretty opaque predicate for simplification proofs.+data Opaque+instance Predicate Opaque where type PredicateName d Opaque = "p"++-- | Shorthand for the pretty opaque predicate.+type P = Opaque++main :: IO ()+main = print spec++spec :: Expect+    -- AND identity laws+    (And Fail    P       `SimplifiesTo` Fail+ -/- And P       Fail    `SimplifiesTo` Fail+ -/- And Succeed P       `SimplifiesTo` P+ -/- And P       Succeed `SimplifiesTo` P++     -- OR identity laws+ -/- Or  Succeed P       `SimplifiesTo` Succeed+ -/- Or  P       Succeed `SimplifiesTo` Succeed+ -/- Or  Fail    P       `SimplifiesTo` P+ -/- Or  P       Fail    `SimplifiesTo` P++     -- other+ -/- And (CompareLength RelOpLT 3) (CompareLength RelOpGT 3)+        `SimplifiesTo` Fail+    )+spec = Valid++-- | TODO I'd like to write my own failure message here, but type-spec is+--   complicated.+type SimplifiesTo p p' = It+    (PredicateName 0 p ++ " simplifies to " ++ PredicateName 0 p')+    (TrySimplify p `Is` Just p')