packages feed

rerefined 0.5.1 → 0.6.0

raw patch · 10 files changed

+42/−45 lines, 10 files

Files

CHANGELOG.md view
@@ -1,3 +1,7 @@+## 0.6.0 (2024-10-01)+* remove `Via` predicate, only need `validateVia`+* swap `validateBool` args+ ## 0.5.1 (2024-06-11) * add `Via` predicate
rerefined.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.36.1. -- -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.5.1+version:        0.6.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data
src/Rerefined/Predicate.hs view
@@ -38,6 +38,16 @@ predicateName = symbolVal' (proxy# @(PredicateName 0 p))  -- | Refine @a@ with predicate @p@.+--+-- Note that 'validate' implementations decide what failure information is+-- emitted. They don't even have to emit their own predicate name, even though+-- 'Predicate' is in the context. This is useful in certain cases such as+-- "Rerefined.Predicate.Via".+--+-- That does mean that the 'Predicate' context may not be used occasionally. But+-- it's very useful, since otherwise combinator predicates have to constantly+-- state @(Refine p a, Predicate p)@, and all predicates should have a pretty+-- name even if it doesn't get printed under normal circumstances. class Predicate p => Refine p a where     -- | Validate predicate @p@ for the given @a@.     --
src/Rerefined/Predicate/Common.hs view
@@ -30,8 +30,6 @@ validateBool     :: forall p     .  (Predicate p, KnownPredicateName p)-    => Proxy# p -> TBL.Builder -> Bool+    => Proxy# p -> Bool -> TBL.Builder     -> Maybe RefineFailure-validateBool p e = \case-  True  -> Nothing-  False -> validateFail p e []+validateBool p b msg = case b of True -> Nothing; False -> validateFail p msg []
src/Rerefined/Predicate/Relational/Length.hs view
@@ -46,7 +46,7 @@        , KnownPredicateName (CompareLength op n)     ) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure validateCompareLength p len =-    validateBool p ("length: "<>TBL.fromDec n) (reifyRelOp @op len n)+    validateBool p (reifyRelOp @op len n) $ "length: "<>TBL.fromDec n   where n = fromIntegral (natVal' (proxy# @n))  -- | Widen a length comparison predicate.
src/Rerefined/Predicate/Relational/Value.hs view
@@ -27,10 +27,8 @@   ) => Refine (CompareValue op sign n) a where     -- note that we show the reified 'Natural' rather than the coerced numeric     -- type, as otherwise we'd need a @'Show' a@-    validate p a =-        validateBool p-            ("bad value")-            (reifyRelOp @op a (reifySignedNat @sign @n))+    validate p a = validateBool p (reifyRelOp @op a (reifySignedNat @sign @n)) $+        "bad value"  data Sign = Pos | Neg
src/Rerefined/Predicate/Via.hs view
@@ -1,47 +1,29 @@-{-# LANGUAGE UndecidableInstances #-} -- for PredicateName-{-# LANGUAGE OverloadedStrings #-} -- for builder-{-# LANGUAGE AllowAmbiguousTypes #-} -- for validateVia+{-# LANGUAGE OverloadedStrings   #-} -- for builder+{-# LANGUAGE AllowAmbiguousTypes #-} -- 'validateVia' is designed for this  module Rerefined.Predicate.Via where  import Rerefined.Predicate.Common-import TypeLevelShow.Utils import GHC.Exts ( Proxy# ) -{- | Predicate @p@ is implemented via predicate @pVia@.+{- | Implement 'validate' for predicate @p@ via @pVia@.  This is useful when you need a unique data type for a predicate (e.g. for instances, clarity), but the predicate it tests already exists. In such cases, it would be nice to reuse the existing predicate, while printing both predicates-in failures.--'Via' assists in doing this. Implement your 'Predicate' instance as normal, then-implement 'Refine' with:--    'validate' = 'validateVia' \@pVia+in failures i.e. "predicate X, implemented via predicate Y, failed with Z". -Now when this predicate fails, it will print the @pVia@ failure with a wrapper-stating the name of the original predicate.+Call using visible type applications: -Note that you may not use @DerivingVia@ because it only works on the last-parameter of a multi-parameter type class, and I don't want to switch the order-of the 'Refine' parameters. Even if I did, @DerivingVia@ isn't much different to-or easier than this.+@+'validate' = 'validateVia' \@pVia+@ -}-data Via pVia p-instance (Predicate p, Predicate pVia)-  => Predicate (Via pVia p) where-    type PredicateName d (Via pVia p) = ShowParen (d > 9)-        ("Via " ++ PredicateName 10 p ++ " " ++ PredicateName 10 pVia)-instance (Refine pVia a, Predicate p, KnownPredicateName p)-  => Refine (Via pVia p) a where-    validate _p a =-        case validate (proxy# @pVia) a of-          Nothing -> Nothing-          Just e  -> validateFail (proxy# @p) "via" [e]- validateVia     :: forall pVia p a     .  (Refine pVia a, Predicate p, KnownPredicateName p)     => Proxy# p -> a -> Maybe RefineFailure-validateVia _p = validate (proxy# @(Via pVia p))+validateVia p a =+    case validate (proxy# @pVia) a of+      Nothing -> Nothing+      Just e  -> validateFail p "via" [e]
src/Rerefined/Predicates.hs view
@@ -5,7 +5,7 @@   -- * Base     Succeed   , Fail-  , Via, validateVia+  , validateVia    -- * Logical   , And, Iff, If, Nand, Nor, Not, Or, Xor
src/Rerefined/Refine.hs view
@@ -49,7 +49,7 @@ -- -- We may derive legal 'Functor', 'Traversable' instances for this as -- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to--- the functor structure. That is, you _may_ alter a 'Refined1' without+-- the functor structure. That is, you /may/ alter a 'Refined1' without -- re-asserting its predicate, provided your changes are made without altering -- the structure/shape of @f@ (e.g. 'fmap', 'traverse'). newtype Refined1 p f a = Refined1 (f a)@@ -80,7 +80,8 @@ unsafeRefine :: a -> Refined p a unsafeRefine = Refined --- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.+-- | Replace a 'Refined''s predicate without validating the new predicate+--   @pNew@. -- -- Unsafe. Use only when you can manually prove that the new predicate holds. unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a@@ -105,7 +106,7 @@ unsafeRefine1 :: f a -> Refined1 p f a unsafeRefine1 = Refined1 --- | Replace a 'Refined1''s predicate without validating the new prdicate+-- | Replace a 'Refined1''s predicate without validating the new predicate --   @pNew@. -- -- Unsafe. Use only when you can manually prove that the new predicate holds.
src/Rerefined/Refine/TH.hs view
@@ -9,6 +9,8 @@ import Data.Text qualified as Text  -- | Refine @a@ with predicate @p@ at compile time via Template Haskell.+--+-- Use like @$$('refineTH' \@p a)@. refineTH     :: forall p a m     .  (Refine p a, TH.Lift a, TH.Quote m, MonadFail m)@@ -18,6 +20,8 @@  -- | Refine @f a@ with functor predicate @p@ at compile time via Template --   Haskell.+--+-- Use like @$$('refine1TH' \@p a)@. refine1TH     :: forall p f a m     .  (Refine1 p f, TH.Lift (f a), TH.Quote m, MonadFail m)