predicate-typed 0.6.0.1 → 0.6.2.0
raw patch · 21 files changed
+1234/−150 lines, 21 filesdep ~base
Dependency ranges changed: base
Files
- doctest/doctests.hs +14/−0
- doctests.hs +0/−14
- predicate-typed.cabal +39/−18
- src/Predicate/Core.hs +11/−4
- src/Predicate/Examples/Common.hs +2/−1
- src/Predicate/Examples/Refined2.hs +1/−0
- src/Predicate/Examples/Refined3.hs +2/−1
- src/Predicate/Prelude.hs +88/−32
- src/Predicate/Refined.hs +6/−5
- src/Predicate/Refined1.hs +879/−0
- src/Predicate/Refined2.hs +4/−3
- src/Predicate/Refined3.hs +4/−3
- src/Predicate/TH_Orphans.hs +1/−1
- src/Predicate/Util.hs +61/−35
- src/Predicate/Util_TH.hs +79/−21
- test/TastyExtras.hs +8/−2
- test/TestJson.hs +1/−0
- test/TestPredicate.hs +10/−3
- test/TestRefined.hs +1/−2
- test/TestRefined2.hs +18/−1
- test/TestRefined3.hs +5/−4
+ doctest/doctests.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE CPP #-} +import Test.DocTest +-- main = doctest ["src", "--verbose"] +main :: IO () + +#if __GLASGOW_HASKELL__ >= 806 +main = doctest ["src","-XNoStarIsType"] +#else +main = doctest ["src"] +#endif + + +-- stack exec doctest -- "src/Predicate.hs" +-- stack exec doctest -- src
− doctests.hs
@@ -1,14 +0,0 @@-{-# LANGUAGE CPP #-} -import Test.DocTest --- main = doctest ["src", "--verbose"] -main :: IO () - -#if __GLASGOW_HASKELL__ >= 806 -main = doctest ["src","-XNoStarIsType"] -#else -main = doctest ["src"] -#endif - - --- stack exec doctest -- "src/Predicate.hs" --- stack exec doctest -- src
predicate-typed.cabal view
@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: f1f9e40a4b553c8230e185e0f814bef7d0729733e864694a8ccff37ce4306c6f+-- hash: 19bf59cd87614fe3ec3d9b00eb00da00ba01f97272fd8de160851fd4f0f9d8f7 name: predicate-typed-version: 0.6.0.1+version: 0.6.2.0 synopsis: Predicates, Refinement types and Dsl description: Please see the README on GitHub at <https://github.com/gbwey/predicate-typed#readme> category: Data@@ -33,6 +33,7 @@ Predicate.Examples.Refined3 Predicate.Prelude Predicate.Refined+ Predicate.Refined1 Predicate.Refined2 Predicate.Refined3 Predicate.TH_Orphans@@ -42,7 +43,7 @@ Paths_predicate_typed hs-source-dirs: src- ghc-options: -fomit-interface-pragmas -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Widentities -fhide-source-paths+ ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wmissing-export-lists -Wpartial-fields -Wredundant-constraints build-depends: QuickCheck , aeson@@ -68,22 +69,34 @@ , these , time , tree-view >=0.5- if impl(ghc >= 8.6)- default-extensions: NoStarIsType- ghc-options: -Wmissing-export-lists -Wpartial-fields -Wredundant-constraints default-language: Haskell2010 test-suite doctests type: exitcode-stdio-1.0 main-is: doctests.hs+ other-modules:+ Predicate+ Predicate.Core+ Predicate.Examples.Common+ Predicate.Examples.Refined2+ Predicate.Examples.Refined3+ Predicate.Prelude+ Predicate.Refined+ Predicate.Refined1+ Predicate.Refined2+ Predicate.Refined3+ Predicate.TH_Orphans+ Predicate.Util+ Predicate.Util_TH+ Paths_predicate_typed hs-source-dirs:- ./. src- ghc-options: -threaded -fomit-interface-pragmas+ doctest+ ghc-options: -threaded build-depends: QuickCheck , aeson- , base >=4.7 && <5+ , base , binary , bytestring , comonad@@ -107,15 +120,25 @@ , these , time , tree-view >=0.5- if impl(ghc >= 8.6)- default-extensions: NoStarIsType- ghc-options: -Wno-missing-export-lists default-language: Haskell2010 test-suite predicate-typed-test type: exitcode-stdio-1.0 main-is: TestSpec.hs other-modules:+ Predicate+ Predicate.Core+ Predicate.Examples.Common+ Predicate.Examples.Refined2+ Predicate.Examples.Refined3+ Predicate.Prelude+ Predicate.Refined+ Predicate.Refined1+ Predicate.Refined2+ Predicate.Refined3+ Predicate.TH_Orphans+ Predicate.Util+ Predicate.Util_TH TastyExtras TestJson TestPredicate@@ -124,12 +147,13 @@ TestRefined3 Paths_predicate_typed hs-source-dirs:+ src test- ghc-options: -threaded -rtsopts -with-rtsopts=-N -fomit-interface-pragmas+ ghc-options: -threaded -rtsopts -with-rtsopts=-N build-depends: QuickCheck , aeson- , base >=4.7 && <5+ , base , binary , bytestring , comonad@@ -156,7 +180,4 @@ , these , time , tree-view >=0.5- if impl(ghc >= 8.6)- default-extensions: NoStarIsType- ghc-options: -Wno-missing-export-lists default-language: Haskell2010
src/Predicate/Core.hs view
@@ -15,6 +15,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NoStarIsType #-} {- | Dsl for evaluating and displaying type level expressions -} @@ -30,13 +31,16 @@ -- ** display evaluation tree , pe , pe2 + , pe2a , pe2n , pu + , pua , pun , pe3 , pl , plc , pz + , peWith -- ** P class , P(..) @@ -56,7 +60,6 @@ import Data.Kind (Type) import Data.These (These(..)) import Data.Functor.Identity -import Data.Semigroup ((<>)) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications @@ -460,7 +463,7 @@ type PP '() a = () eval _ opts _ = pure $ mkNode opts (PresentT ()) ["'()"] [] --- todo: the type has to be [a] so we still need type PP '[p] a = [PP p a] to keep the types in line +-- the type has to be [a] so we still need type PP '[p] a = [PP p a] to keep the types in line -- | extracts the value level representation of the type level '[] -- @@ -722,11 +725,13 @@ let b = Proxy @a in pure $ mkNode opts (PresentT b) ["'Proxy" <> show1 opts " | " a] [] -pe, pe2, pe2n, pu, pun, pe3, pl, plc, pz :: forall p a . (Show (PP p a), P p a) => a -> IO (BoolT (PP p a)) +pe, pe2, pe2a, pe2n, pu, pua, pun, pe3, pl, plc, pz :: forall p a . (Show (PP p a), P p a) => a -> IO (BoolT (PP p a)) -- | displays the evaluation tree in plain text without colors pe = peWith @p o0 --- | displays the evaluation tree using colors +-- | displays the evaluation tree using colors without background colors pe2 = peWith @p o2 +-- | displays the evaluation tree using colors with background colors +pe2a = peWith @p o2 { oColor = color1 } -- | same as 'pe2' but truncates the display tree width: see 'o2n' pe2n = peWith @p o2n -- | same as 'pe2' but allows for wider data @@ -742,6 +747,8 @@ -- pu @'(Id, "abc", 123) [1..4] -- @ pu = peWith @p ou +-- | displays the evaluation tree using unicode and colors with background colors +pua = peWith @p ou { oColor = color1 } -- | same as 'pu' but truncates the display tree width: see 'ou' pun = peWith @p oun
src/Predicate/Examples/Common.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE NoStarIsType #-} {- | Common predicates for use with Refined, Refined2, and Refined3 -} @@ -145,7 +146,7 @@ type Ip4fmt = PrintL 4 "%03d.%03d.%03d.%03d" Id -- | regular expression for an octet -type OctetRE = "(25[0-5]|2[0..4][0-9]|1[0-9][0-9]|[1-9][0-9]|[0-9])" -- no padded numbers allowed +type OctetRE = "(25[0-5]|2[0-4][0-9]|1[0-9][0-9]|[1-9][0-9]|[0-9])" -- no padded numbers allowed --type Ip4StrictRE = "^" <%> OctetRE <%> "\\." <%> OctetRE <%> "\\." <%> OctetRE <%> "\\." <%> OctetRE <%> "$" -- | regular expression for an ip4 address type Ip4StrictRE = "^" <%> IntersperseT "\\." (RepeatT 4 OctetRE) <%> "$"
src/Predicate/Examples/Refined2.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE NoStarIsType #-} {- | Contains prepackaged 3-tuples to use with 'Refined2' -}
src/Predicate/Examples/Refined3.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE NoStarIsType #-} {- | Contains prepackaged 4-tuples and proxies to use with 'Refined3' -} @@ -138,7 +139,7 @@ ccn = mkProxy3 -- works but have to add all the constraints -ccn' :: (PP ns String ~ [Integer], KnownNat (SumT ns), P ns [Char]) => Proxy (Ccn ns) +ccn' :: (PP ns String ~ [Integer], KnownNat (SumT ns), P ns String) => Proxy (Ccn ns) ccn' = mkProxy3' cc11 :: Proxy (Ccn '[4,4,3]) -- or Proxy CC11
src/Predicate/Prelude.hs view
@@ -2,7 +2,7 @@ -- the mkNode opts (FailT msg) [msg] .. -- repetitive: needs to add value -- no types referring to types otherwise we lose use of _ as Type {-# OPTIONS -Wall #-} -{-# OPTIONS -Wcompat #-} +{-# OPTIONS -Wno-compat #-} {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# OPTIONS -Wredundant-constraints #-} @@ -25,6 +25,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE NoOverloadedLists #-} +{-# LANGUAGE NoStarIsType #-} {- | Dsl for evaluating and displaying type level expressions @@ -98,7 +99,7 @@ -- ** character expressions , IsLower , IsUpper - , IsNumber + , IsDigit , IsSpace , IsPunctuation , IsControl @@ -109,7 +110,7 @@ , IsLowerAll , IsUpperAll - , IsNumberAll + , IsDigitAll , IsSpaceAll , IsPunctuationAll , IsControlAll @@ -346,6 +347,7 @@ , Ix' , IxL , type (!!) + , type (!!?) , Lookup , LookupDef , LookupDef' @@ -355,6 +357,7 @@ -- cons / uncons expressions , type (:+) , type (+:) + , type (++) , Uncons , Unsnoc , Head @@ -553,7 +556,6 @@ import Data.Maybe import Control.Arrow import qualified Data.Semigroup as SG -import Data.Semigroup (Semigroup(..)) import Numeric import Data.Char import Data.Function @@ -1404,7 +1406,7 @@ -- True -- TrueT -- --- >>> pz @(Map '(IsControl, IsLatin1, IsHexDigit, IsOctDigit, IsNumber, IsPunctuation, IsSeparator, IsSpace) Id) "abc134" +-- >>> pz @(Map '(IsControl, IsLatin1, IsHexDigit, IsOctDigit, IsDigit, IsPunctuation, IsSeparator, IsSpace) Id) "abc134" -- Present [(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False)] -- PresentT [(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False)] -- @@ -1424,19 +1426,19 @@ -- | predicate for determining if the character is a digit -- --- >>> pz @IsNumber 'g' +-- >>> pz @IsDigit 'g' -- False -- FalseT -- --- >>> pz @IsNumber '9' +-- >>> pz @IsDigit '9' -- True -- TrueT -- -data IsNumber -type IsNumberT = IsCharSet 'CNumber -instance P IsNumberT x => P IsNumber x where - type PP IsNumber x = Bool - eval _ = evalBool (Proxy @IsNumberT) +data IsDigit +type IsDigitT = IsCharSet 'CNumber +instance P IsDigitT x => P IsDigit x where + type PP IsDigit x = Bool + eval _ = evalBool (Proxy @IsDigitT) data IsSpace type IsSpaceT = IsCharSet 'CSpace @@ -1538,23 +1540,23 @@ -- True ((>>) True | {True (&*) True}) -- TrueT -- --- >>> pz @( '(IsControlAll, IsLatin1All , IsHexDigitAll , IsOctDigitAll , IsNumberAll , IsPunctuationAll , IsSeparatorAll , IsSpaceAll ) ) "abc134" +-- >>> pz @( '(IsControlAll, IsLatin1All , IsHexDigitAll , IsOctDigitAll , IsDigitAll , IsPunctuationAll , IsSeparatorAll , IsSpaceAll ) ) "abc134" -- Present (False,True,True,False,False,False,False,False) -- PresentT (False,True,True,False,False,False,False,False) -- --- >>> pl @(SplitAts [1,2,10] Id >> Para '[IsLowerAll, IsNumberAll, IsUpperAll ]) "abdefghi" +-- >>> pl @(SplitAts [1,2,10] Id >> Para '[IsLowerAll, IsDigitAll, IsUpperAll ]) "abdefghi" -- Present [True,False,False] ((>>) [True,False,False] | {Para(0) [True,False,False] | ["a","bd","efghi"]}) -- PresentT [True,False,False] -- --- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsNumberAll, IsUpperAll ]) "a98efghi" +-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll ]) "a98efghi" -- False ((>>) False | {Bool(2) [] (IsUpperAll | "efghi")}) -- FalseT -- --- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsNumberAll, IsUpperAll || IsLowerAll ]) "a98efghi" +-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll || IsLowerAll ]) "a98efghi" -- True ((>>) True | {Bools}) -- TrueT -- --- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsNumberAll, IsUpperAll || IsLowerAll ]) "a98efgHi" +-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll || IsLowerAll ]) "a98efgHi" -- False ((>>) False | {Bool(2) [] (False || False | (IsUpperAll | "efgHi") || (IsLowerAll | "efgHi"))}) -- FalseT -- @@ -1622,19 +1624,19 @@ -- | predicate for determining if the string is all digits -- --- >>> pz @IsNumberAll "213G" +-- >>> pz @IsDigitAll "213G" -- False -- FalseT -- --- >>> pz @IsNumberAll "929" +-- >>> pz @IsDigitAll "929" -- True -- TrueT -- -data IsNumberAll -type IsNumberAllT = IsCharSetAll 'CNumber -instance P IsNumberAllT x => P IsNumberAll x where - type PP IsNumberAll x = Bool - eval _ = evalBool (Proxy @IsNumberAllT) +data IsDigitAll +type IsDigitAllT = IsCharSetAll 'CNumber +instance P IsDigitAllT x => P IsDigitAll x where + type PP IsDigitAll x = Bool + eval _ = evalBool (Proxy @IsDigitAllT) -- | predicate for determining if the string is all spaces -- @@ -1788,7 +1790,7 @@ case chkSize opts msg0 p [hh pp] of Left e -> e Right () -> - let d = map (:[]) p + let d = map pure p in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp] -- | similar to 'show' @@ -3014,7 +3016,7 @@ let l = length q diff = if n<=l then 0 else n-l bs = if lft - then (replicate diff p) <> q + then replicate diff p <> q else q <> replicate diff p in mkNode opts (PresentT bs) [show01 opts msg1 bs q] (hhs <> [hh qq]) @@ -3110,7 +3112,7 @@ in mkNode opts (PresentT ret) [show01' opts msg1 ret "n=" n <> show1 opts " | " p] [hh pp, hh qq] splitAtNeg :: Int -> [a] -> ([a], [a]) -splitAtNeg n as = splitAt (if n<0 then (length as + n) else n) as +splitAtNeg n as = splitAt (if n<0 then length as + n else n) as data Take n p @@ -5449,6 +5451,14 @@ -- Present Nothing -- PresentT Nothing -- +-- >>> pl @((Id !!? Char1 "d") > MkJust 99 || Length Id <= 3) (M.fromList $ zip "abcd" [1..]) +-- False (False || False | (Just 4 > Just 99) || (4 <= 3)) +-- FalseT +-- +-- >>> pz @((Id !!? Char1 "d") > MkJust 2 || Length Id <= 3) (M.fromList $ zip "abcd" [1..]) +-- True +-- TrueT +-- data Lookup p q instance (P q a @@ -5473,6 +5483,14 @@ Nothing -> mkNode opts (PresentT Nothing) [msg1 <> " not found"] hhs Just ret -> mkNode opts (PresentT (Just ret)) [show01' opts msg1 ret "p=" p <> show1 opts " | q=" q] hhs +data p !!? q +type BangBangQT p q = Lookup p q + +instance P (BangBangQT p q) a => P (p !!? q) a where + type PP (p !!? q) a = PP (BangBangQT p q) a + eval _ = eval (Proxy @(BangBangQT p q)) + + -- | 'Data.List.ands' -- -- >>> pz @(Ands Id) [True,True,True] @@ -5543,6 +5561,46 @@ Just i -> " i="++show i in mkNodeB opts (or p) [msg1 <> w <> show1 opts " | " p] [hh pp] + +-- | similar to (++) +-- +-- >>> pz @(Fst Id ++ Snd Id) ([9,10,11],[1,2,3,4]) +-- Present [9,10,11,1,2,3,4] +-- PresentT [9,10,11,1,2,3,4] +-- +-- >>> pz @(Snd Id ++ Fst Id) ([],[5]) +-- Present [5] +-- PresentT [5] +-- +-- >>> pz @(Char1 "xyz" :+ W "ab" ++ W "cdefg") () +-- Present "xabcdefg" +-- PresentT "xabcdefg" +-- +-- >>> pz @([1,2,3] ++ EmptyList _) "somestuff" +-- Present [1,2,3] +-- PresentT [1,2,3] +-- +data p ++ q +infixr 5 ++ + +instance (P p x + , P q x + , Show (PP p x) + , PP p x ~ [a] + , PP q x ~ [a] + ) => P (p ++ q) x where + type PP (p ++ q) x = PP q x + eval _ opts z = do + let msg0 = "(++)" + lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z [] + pure $ case lr of + Left e -> e + Right (p,q,pp,qq) -> + let b = p ++ q + in mkNode opts (PresentT b) [show01' opts msg0 b "p=" p <> show1 opts " | q=" q] [hh pp, hh qq] + + + -- cant directly create a singleton type using '[] since the type of '[] is unknown. instead use 'Singleton' or 'EmptyT' -- | similar to cons @@ -6513,7 +6571,6 @@ --type OneP = Guard (PrintF "expected list of length 1 but found length=%d" Len) (Len == 1) >> Head Id -- k or prt has access to (Int,a) where Int is the current guard position: hence need to use PrintT --- todo: better explanation of how this works -- passthru but adds the length of ps (replaces LenT in the type synonym to avoid type synonyms being expanded out) -- | Guards contain a type level list of tuples the action to run on failure of the predicate and the predicate itself @@ -8132,7 +8189,7 @@ in case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of Left e -> e Right () -> - let d = intercalate p (map (:[]) q) + let d = intercalate p (map pure q) in mkNode opts (PresentT d) [show01 opts msg0 d p <> show1 opts " | " q] hhs -- | uses PrintF to format output @@ -8673,8 +8730,8 @@ Left e -> pure e Right ss -> do mb <- runIO $ case fh of - FStdout -> fmap (left show) $ E.try @E.SomeException $ hPutStr stdout ss - FStderr -> fmap (left show) $ E.try @E.SomeException $ hPutStr stderr ss + FStdout -> fmap (left show) $ E.try @E.SomeException $ putStr ss + FStderr -> fmap (left show) $ E.try @E.SomeException $ putStr ss FOther s w -> do b <- doesFileExist s if b && w == WFWrite then pure $ Left $ "file [" <> s <> "] already exists" @@ -10270,7 +10327,6 @@ -- Present (1999-01-01,2001-02-12) (Both) -- PresentT (1999-01-01,2001-02-12) -- --- todo: add topMessage somehow? data Both p q instance ( ExtractL1C (PP q x) , ExtractL2C (PP q x)
src/Predicate/Refined.hs view
@@ -19,6 +19,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE NoStarIsType #-} {- | Simple refinement type with only one type and a predicate -} @@ -49,7 +50,7 @@ , unRavelTIO , rapply , rapply0 - , rapply1 + , rapplyLift -- ** unsafe create methods , unsafeRefined @@ -73,10 +74,10 @@ import qualified Text.Read.Lex as RL import qualified Data.Binary as B import Data.Binary (Binary) -import Data.Semigroup ((<>)) import Data.String import Data.Maybe import Data.Hashable (Hashable(..)) +import GHC.Stack -- $setup -- >>> :set -XDataKinds @@ -276,13 +277,13 @@ rapply0 opts f a b = rapply opts f (newRefinedT opts a) (newRefinedT opts b) -- | same as 'rapply' except we already have valid 'Refined' values as input -rapply1 :: forall m p a . (RefinedC p a, Monad m) +rapplyLift :: forall m p a . (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> Refined p a -> Refined p a -> RefinedT m (Refined p a) -rapply1 opts f (Refined a) (Refined b) = newRefinedT opts (f a b) +rapplyLift opts f (Refined a) (Refined b) = newRefinedT opts (f a b) -- | attempts to lift a refinement type to another refinement type by way of transformation function -- you can control both the predicate and the type @@ -421,7 +422,7 @@ unsafeRefined = Refined -- | a way to unsafely create a 'Refined' value but run the predicate -unsafeRefined' :: forall p a . RefinedC p a => POpts -> a -> Refined p a +unsafeRefined' :: forall p a . (RefinedC p a, HasCallStack) => POpts -> a -> Refined p a unsafeRefined' opts a = let tt = runIdentity $ evalBool (Proxy @p) opts a in case getValueLR opts "" tt [] of
+ src/Predicate/Refined1.hs view
@@ -0,0 +1,879 @@+{-# OPTIONS -Wall #-} +{-# OPTIONS -Wcompat #-} +{-# OPTIONS -Wincomplete-record-updates #-} +{-# OPTIONS -Wincomplete-uni-patterns #-} +{-# OPTIONS -Wno-redundant-constraints #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveLift #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE NoStarIsType #-} +-- | +-- Refinement type allowing the external type to differ from the internal type +-- doesnt store the output value but runs on demand but has calculate each time and could fail later +-- see 'Refined1' +-- +-- @ +-- similar to 'Predicate.Refined2.Refined2' but also provides: +-- * quickCheck methods +-- * ability to combine refinement types +-- * a canonical output value using the \'fmt\' parameter +-- @ +-- +module Predicate.Refined1 ( + + -- ** Refined1 + Refined1(unRefined1) + , Refined1C + + -- ** display results + , prtEval1 + , prtEval1P + , prtEval1PIO + , prt1IO + , prt1 + , prt1Impl + , Msg1 (..) + , RResults1 (..) + + -- ** evaluation methods + , eval1 + , eval1P + + -- ** create a wrapped Refined1 value + , newRefined1T + , newRefined1TP + , newRefined1TPIO + , withRefined1T + , withRefined1TIO + , withRefined1TP + + -- ** proxy methods + , mkProxy1 + , mkProxy1' + , MakeR1 + + -- ** unsafe methods for creating Refined1 + , unsafeRefined1 + , unsafeRefined1' + + -- ** combine Refined1 values + , convertRefined1TP + , rapply1 + , rapply1P + + -- ** QuickCheck methods + , arbRefined1 + , arbRefined1With + + -- ** emulate Refined1 using Refined + , RefinedEmulate + , eval1PX + , eval1X + + -- ** extract from 4-tuple + , T4_1 + , T4_2 + , T4_3 + , T4_4 + + ) where +import Predicate.Refined +import Predicate.Core +import Predicate.Util +import Data.Functor.Identity (Identity(..)) +import Data.Tree +import Data.Proxy +import Control.Monad.Except +import Control.Monad.Writer (tell) +import Data.Aeson (ToJSON(..), FromJSON(..)) +import qualified Language.Haskell.TH.Syntax as TH +import System.Console.Pretty +import Test.QuickCheck +import qualified GHC.Read as GR +import qualified Text.ParserCombinators.ReadPrec as PCR +import qualified Text.Read.Lex as RL +import qualified Data.Binary as B +import Data.Binary (Binary) +import Data.Maybe (fromMaybe) +import Control.Lens ((^?),ix) +import Data.Tree.Lens (root) +import Data.Char (isSpace) +import Data.String +import Data.Hashable (Hashable(..)) +import GHC.Stack + +-- $setup +-- >>> :set -XDataKinds +-- >>> :set -XTypeApplications +-- >>> :set -XTypeOperators +-- >>> :set -XOverloadedStrings +-- >>> :m + Predicate.Prelude + +-- | Refinement type that differentiates the input from output: similar to 'Predicate.Refined3.Refined3' but only creates the output value as needed. +-- +-- * @i@ is the input type +-- * @ip@ converts @i@ to @PP ip i@ which is the internal type and stored in 'unRefined1' +-- * @op@ validates that internal type using @PP op (PP ip i) ~ Bool@ +-- * @fmt@ outputs the internal type @PP fmt (PP ip i) ~ i@ (not stored anywhere but created on demand) +-- * @PP fmt (PP ip i)@ should be valid as input for Refined1 +-- +-- Setting @ip@ to @Id@ and @fmt@ to @Id@ makes it equivalent to 'Refined.Refined': see 'RefinedEmulate' +-- +-- Setting the input type @i@ to 'GHC.Base.String' resembles the corresponding Read/Show instances but with an additional predicate on the read value +-- +-- * __read__ a string using /ip/ into an internal type and store in 'unRefined1' +-- * __validate__ 'unRefined1' using the predicate /op/ +-- * __show__ 'unRefined1' using /fmt/ (does not store the formatted result unlike 'Predicate.Refined3.Refined3') +-- +-- Although a common scenario is String as input, you are free to choose any input type you like +-- +-- >>> prtEval1 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fe" +-- Right (Refined1 {unRefined1 = 254}) +-- +-- >>> prtEval1 @(ReadBase Int 16 Id) @(Lt 253) @(PrintF "%x" Id) oz "00fe" +-- Left Step 2. False Boolean Check(op) | FalseP +-- +-- >>> prtEval1 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fg" +-- Left Step 1. Initial Conversion(ip) Failed | invalid base 16 +-- +-- >>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) ol "198.162.3.1.5" +-- Left Step 2. False Boolean Check(op) | {length invalid:5 == 4} +-- +-- >>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1.5" +-- Left Step 2. Failed Boolean Check(op) | found length=5 +-- +-- >>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1" +-- Right (Refined1 {unRefined1 = [198,162,3,1]}) +-- +-- >>> :m + Data.Time.Calendar.WeekDate +-- >>> prtEval1 @(MkDay >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,13) +-- Right (Refined1 {unRefined1 = (2019-10-13,41,7)}) +-- +-- >>> prtEval1 @(MkDay >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) @(UnMkDay (Fst Id)) ol (2019,10,12) +-- Left Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7} +-- +-- >>> prtEval1 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,12) +-- Left Step 2. Failed Boolean Check(op) | expected a Sunday +-- +-- >>> type T4 k = '(MkDay >> 'Just Id, Guard "expected a Sunday" (Thd Id == 7) >> 'True, UnMkDay (Fst Id), k) +-- >>> prtEval1P (Proxy @(T4 _)) oz (2019,10,12) +-- Left Step 2. Failed Boolean Check(op) | expected a Sunday +-- +-- >>> prtEval1P (Proxy @(T4 _)) oz (2019,10,13) +-- Right (Refined1 {unRefined1 = (2019-10-13,41,7)}) +-- +newtype Refined1 ip op fmt i = Refined1 { unRefined1 :: PP ip i } + +type role Refined1 nominal nominal nominal nominal + +-- | directly load values into 'Refined1'. It still checks to see that those values are valid +unsafeRefined1' :: forall ip op fmt i + . (HasCallStack, Show i, Show (PP ip i), Refined1C ip op fmt i) + => POpts + -> i + -> Refined1 ip op fmt i +unsafeRefined1' opts i = + let (ret,mr) = eval1 @ip @op @fmt opts i + in fromMaybe (error $ show (prt1Impl opts ret)) mr + +-- | directly load values into 'Refined1' without any checking +unsafeRefined1 :: forall ip op fmt i . PP ip i -> Refined1 ip op fmt i +unsafeRefined1 = Refined1 + + +-- | Provides the constraints on Refined1 +type Refined1C ip op fmt i = + ( P ip i + , P op (PP ip i) + , PP op (PP ip i) ~ Bool -- the internal value needs to pass the predicate check + , P fmt (PP ip i) + , PP fmt (PP ip i) ~ i -- the output type must match the original input type + ) + +deriving instance (Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined1 ip op fmt i) +deriving instance (Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined1 ip op fmt i) +deriving instance (TH.Lift (PP ip i), TH.Lift (PP fmt (PP ip i))) => TH.Lift (Refined1 ip op fmt i) + +instance (Refined1C ip op fmt String, Show (PP ip String)) => IsString (Refined1 ip op fmt String) where + fromString s = + let (ret,mr) = eval1 @ip @op @fmt o2 s + in fromMaybe (error $ "Refined1(fromString):" ++ show (prt1Impl o2 ret)) mr + +-- read instance from -ddump-deriv +-- | 'Read' instance for 'Refined1' +-- +-- >>> reads @(Refined1 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 {unRefined1 = 254}" +-- [(Refined1 {unRefined1 = 254},"")] +-- +-- >>> reads @(Refined1 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 {unRefined1 = 300}" +-- [] +-- +-- >>> reads @(Refined1 (ReadBase Int 16 Id) (Id < 0) (ShowBase 16 Id) String) "Refined1 {unRefined1 = -1234}" +-- [(Refined1 {unRefined1 = -1234},"")] +-- +-- >>> reads @(Refined1 (Map (ReadP Int Id) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) (PrintL 4 "%d.%d.%d.%d" Id) String) "Refined1 {unRefined1 = [192,168,0,1]}" +-- [(Refined1 {unRefined1 = [192,168,0,1]},"")] +-- +instance ( Eq i + , Show i + , Eq (PP ip i) + , Show (PP ip i) + , Refined1C ip op fmt i + , Read (PP ip i) + , Read (PP fmt (PP ip i)) + ) => Read (Refined1 ip op fmt i) where + readPrec + = GR.parens + (PCR.prec + 11 + (do GR.expectP (RL.Ident "Refined1") + GR.expectP (RL.Punc "{") + fld1 <- readField + "unRefined1" (PCR.reset GR.readPrec) + GR.expectP (RL.Punc "}") + + let (_ret,mr) = runIdentity $ eval1MSkip @_ @ip @op @fmt oz fld1 + case mr of + Nothing -> fail "" + Just (Refined1 r1) + | r1 == fld1 -> pure (Refined1 r1) + | otherwise -> fail "" -- cant display a decent failure message + )) + readList = GR.readListDefault + readListPrec = GR.readListPrecDefault + +-- | 'ToJSON' instance for 'Refined1' +-- +-- >>> import qualified Data.Aeson as A +-- >>> A.encode (unsafeRefined1 @(ReadBase Int 16 Id) @(Between 0 255 Id) @(ShowBase 16 Id) 254) +-- "\"fe\"" +-- +-- >>> A.encode (unsafeRefined1 @Id @'True @Id 123) +-- "123" +-- +instance (Show (PP fmt (PP ip i)), ToJSON (PP fmt (PP ip i)), P fmt (PP ip i)) => ToJSON (Refined1 ip op fmt i) where + toJSON (Refined1 x) = + let ss = runIdentity $ eval (Proxy @fmt) o2 x + in case getValAndPE ss of + (Right b,_) -> toJSON b + (Left e,t3) -> error $ "oops tojson failed " ++ show e ++ " t3=" ++ show t3 + + +-- | 'FromJSON' instance for 'Refined1' +-- +-- >>> import qualified Data.Aeson as A +-- >>> A.eitherDecode' @(Refined1 (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe\"" +-- Right (Refined1 {unRefined1 = 254}) +-- +-- >>> removeAnsi $ A.eitherDecode' @(Refined1 (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe443a\"" +-- Error in $: Refined1:Step 2. False Boolean Check(op) | {True && False | (16663610 < 256)} +-- <BLANKLINE> +-- *** Step 1. Success Initial Conversion(ip) [16663610] *** +-- <BLANKLINE> +-- P ReadBase(Int,16) 16663610 | "00fe443a" +-- | +-- `- P Id "00fe443a" +-- <BLANKLINE> +-- *** Step 2. False Boolean Check(op) *** +-- <BLANKLINE> +-- False True && False | (16663610 < 256) +-- | +-- +- True 16663610 > 10 +-- | | +-- | +- P Id 16663610 +-- | | +-- | `- P '10 +-- | +-- `- False 16663610 < 256 +-- | +-- +- P Id 16663610 +-- | +-- `- P '256 +-- <BLANKLINE> +-- +instance (Show ( PP fmt (PP ip i)) + , Show (PP ip i) + , Refined1C ip op fmt i + , FromJSON i + ) => FromJSON (Refined1 ip op fmt i) where + parseJSON z = do + i <- parseJSON @i z + let (ret,mr) = eval1 @ip @op @fmt o2 i + case mr of + Nothing -> fail $ "Refined1:" ++ show (prt1Impl o2 ret) + Just r -> return r + +{- +instance (Arbitrary (PP ip i) + , Show (PP ip i) + , Show i + , Refined1C ip op fmt i + ) => Arbitrary (Refined1 ip op fmt i) where + arbitrary = suchThatMap (arbitrary @(PP ip i)) $ eval1MQuickIdentity @ip @op @fmt +-} +arbRefined1 :: forall ip op fmt i . + ( Arbitrary (PP ip i) + , Refined1C ip op fmt i + ) => Proxy '(ip,op,fmt,i) + -> Gen (Refined1 ip op fmt i) +arbRefined1 = flip arbRefined1With id + +-- | uses arbitrary to generate the internal 'unRefined1' and then uses \'fmt\' to fill create output value +arbRefined1With :: + forall ip op fmt i + . (Arbitrary (PP ip i) + , Refined1C ip op fmt i) + => Proxy '(ip,op,fmt,i) + -> (PP ip i -> PP ip i) + -> Gen (Refined1 ip op fmt i) +arbRefined1With _ f = + suchThatMap (f <$> arbitrary @(PP ip i)) $ eval1MQuickIdentity @ip @op @fmt + +-- | 'Binary' instance for 'Refined1' +-- +-- >>> import Control.Arrow ((+++)) +-- >>> import Control.Lens +-- >>> import Data.Time +-- >>> type K1 = MakeR1 '(ReadP Day Id, 'True, ShowP Id, String) +-- >>> type K2 = MakeR1 '(ReadP Day Id, Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id, ShowP Id, String) +-- >>> r = unsafeRefined1' oz "2019-04-23" :: K1 +-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r) +-- Refined1 {unRefined1 = 2019-04-23} +-- +-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r) +-- Refined1:Step 2. False Boolean Check(op) | {2019-05-30 <= 2019-04-23} +-- <BLANKLINE> +-- *** Step 1. Success Initial Conversion(ip) [2019-04-23] *** +-- <BLANKLINE> +-- P ReadP Day 2019-04-23 +-- | +-- `- P Id "2019-04-23" +-- <BLANKLINE> +-- *** Step 2. False Boolean Check(op) *** +-- <BLANKLINE> +-- False 2019-05-30 <= 2019-04-23 +-- | +-- +- P Id 2019-04-23 +-- | +-- +- P ReadP Day 2019-05-30 +-- | | +-- | `- P '2019-05-30 +-- | +-- `- P ReadP Day 2019-06-01 +-- | +-- `- P '2019-06-01 +-- <BLANKLINE> +-- + +instance ( Show (PP fmt (PP ip i)) + , Show (PP ip i) + , Refined1C ip op fmt i + , Binary i + ) => Binary (Refined1 ip op fmt i) where + get = do + i <- B.get @i + let (ret,mr) = eval1 @ip @op @fmt o2 i + case mr of + Nothing -> fail $ "Refined1:" ++ show (prt1Impl o2 ret) + Just r -> return r + put (Refined1 x) = + let ss = runIdentity $ eval (Proxy @fmt) o2 x + in case getValAndPE ss of + (Right b,_) -> B.put @i b + (Left e,t3) -> error $ "oops tojson failed " ++ show e ++ " t3=" ++ show t3 + +-- | 'Hashable' instance for 'Refined1' +instance (Refined1C ip op fmt i + , Hashable (PP ip i) + ) => Hashable (Refined1 ip op fmt i) where + hashWithSalt s (Refined1 a) = s + hash a + +-- | creates a 4-tuple proxy (see 'withRefined1TP' 'newRefined1TP' 'eval1P' 'prtEval1P') +-- +-- use type application to set the 4-tuple or set the individual parameters directly +-- +-- set the 4-tuple directly +-- +-- >>> eg1 = mkProxy1 @'(ReadP Int Id, Gt 10, ShowP Id, String) +-- >>> prtEval1P eg1 ol "24" +-- Right (Refined1 {unRefined1 = 24}) +-- +-- skip the 4-tuple and set each parameter individually using type application +-- +-- >>> eg2 = mkProxy1 @_ @(ReadP Int Id) @(Gt 10) @(ShowP Id) +-- >>> prtEval1P eg2 ol "24" +-- Right (Refined1 {unRefined1 = 24}) +-- +mkProxy1 :: forall z ip op fmt i . z ~ '(ip,op,fmt,i) => Proxy '(ip,op,fmt,i) +mkProxy1 = Proxy + +-- | same as 'mkProxy1' but checks to make sure the proxy is consistent with the 'Refined1C' constraint +mkProxy1' :: forall z ip op fmt i . (z ~ '(ip,op,fmt,i), Refined1C ip op fmt i) => Proxy '(ip,op,fmt,i) +mkProxy1' = Proxy + +-- | type family for converting from a 4-tuple '(ip,op,fmt,i) to a 'Refined1' type +type family MakeR1 p where + MakeR1 '(ip,op,fmt,i) = Refined1 ip op fmt i + +withRefined1TIO :: forall ip op fmt i m b + . (MonadIO m, Refined1C ip op fmt i, Show (PP ip i), Show i) + => POpts + -> i + -> (Refined1 ip op fmt i -> RefinedT m b) + -> RefinedT m b +withRefined1TIO opts = (>>=) . newRefined1TPIO (Proxy @'(ip,op,fmt,i)) opts + +-- | create a 'Refined1' value using a continuation +-- +-- This first example reads a hex string and makes sure it is between 100 and 200 and then +-- reads a binary string and adds the values together +-- +-- >>> :set -XPolyKinds +-- >>> b16 = Proxy @'(ReadBase Int 16 Id, Between 100 200 Id, ShowBase 16 Id, String) +-- >>> b2 = Proxy @'(ReadBase Int 2 Id, 'True, ShowBase 2 Id, String) +-- >>> prtRefinedTIO $ withRefined1TP b16 oz "a3" $ \x -> withRefined1TP b2 oz "1001110111" $ \y -> pure (unRefined1 x + unRefined1 y) +-- 794 +-- +-- this example fails as the the hex value is out of range +-- +-- >>> prtRefinedTIO $ withRefined1TP b16 o0 "a388" $ \x -> withRefined1TP b2 o0 "1001110111" $ \y -> pure (x,y) +-- <BLANKLINE> +-- *** Step 1. Success Initial Conversion(ip) [41864] *** +-- <BLANKLINE> +-- P ReadBase(Int,16) 41864 | "a388" +-- | +-- `- P Id "a388" +-- <BLANKLINE> +-- *** Step 2. False Boolean Check(op) *** +-- <BLANKLINE> +-- False 41864 <= 200 +-- | +-- +- P Id 41864 +-- | +-- +- P '100 +-- | +-- `- P '200 +-- <BLANKLINE> +-- failure msg[Step 2. False Boolean Check(op) | {41864 <= 200}] +-- +withRefined1T :: forall ip op fmt i m b + . (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i) + => POpts + -> i + -> (Refined1 ip op fmt i -> RefinedT m b) + -> RefinedT m b +withRefined1T opts = (>>=) . newRefined1TP (Proxy @'(ip,op,fmt,i)) opts + +withRefined1TP :: forall m ip op fmt i b proxy + . (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> (Refined1 ip op fmt i -> RefinedT m b) + -> RefinedT m b +withRefined1TP p opts = (>>=) . newRefined1TP p opts + +newRefined1T :: forall m ip op fmt i . (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) + => POpts + -> i + -> RefinedT m (Refined1 ip op fmt i) +newRefined1T = newRefined1TP (Proxy @'(ip,op,fmt,i)) + +-- | create a wrapped 'Refined1' type +-- +-- >>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) oz (2019,11,1) +-- Refined1 {unRefined1 = (2019-11-01,44,5)} +-- +-- >>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, Thd Id == 5, UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2) +-- failure msg[Step 2. False Boolean Check(op) | {6 == 5}] +-- +-- >>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, Msg "wrong day:" (Thd Id == 5), UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2) +-- failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}] +-- +newRefined1TP :: forall m ip op fmt i proxy + . (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> RefinedT m (Refined1 ip op fmt i) +newRefined1TP = newRefined1TPImpl (return . runIdentity) + +newRefined1TPIO :: forall m ip op fmt i proxy + . (Refined1C ip op fmt i + , MonadIO m + , Show (PP ip i) + , Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> RefinedT m (Refined1 ip op fmt i) +newRefined1TPIO = newRefined1TPImpl liftIO + +newRefined1TPImpl :: forall n m ip op fmt i proxy + . (Refined1C ip op fmt i + , Monad m + , MonadEval n + , Show (PP ip i) + , Show (PP fmt (PP ip i))) + => (forall x . n x -> RefinedT m x) + -> proxy '(ip,op,fmt,i) + -> POpts + -> i + -> RefinedT m (Refined1 ip op fmt i) +newRefined1TPImpl f _ opts i = do + (ret,mr) <- f $ eval1M opts i + let m1 = prt1Impl opts ret + tell [m1Long m1] + case mr of + Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1 + Just r -> return r + +newRefined1TPSkipIPImpl :: forall n m ip op fmt i proxy + . (Refined1C ip op fmt i + , Monad m + , MonadEval n + , Show (PP ip i) + , Show (PP fmt (PP ip i))) + => (forall x . n x -> RefinedT m x) + -> proxy '(ip,op,fmt,i) + -> POpts + -> PP ip i + -> RefinedT m (Refined1 ip op fmt i) +newRefined1TPSkipIPImpl f _ opts a = do + (ret,mr) <- f $ eval1MSkip opts a + let m1 = prt1Impl opts ret + tell [m1Long m1] + case mr of + Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1 + Just r -> return r + +-- | attempts to cast a wrapped 'Refined1' to another 'Refined1' with different predicates +convertRefined1TP :: forall m ip op fmt i ip1 op1 fmt1 i1 . + ( Refined1C ip1 op1 fmt1 i1 + , Monad m + , Show (PP ip i) + , PP ip i ~ PP ip1 i1 + , Show i1) + => Proxy '(ip, op, fmt, i) + -> Proxy '(ip1, op1, fmt1, i1) + -> POpts + -> RefinedT m (Refined1 ip op fmt i) + -> RefinedT m (Refined1 ip1 op1 fmt1 i1) +convertRefined1TP _ _ opts ma = do + Refined1 x <- ma + -- we skip the input value @Id and go straight to the internal value so PP fmt (PP ip i) /= i for this call + Refined1 a <- newRefined1TPSkipIPImpl (return . runIdentity) (Proxy @'(ip1, op1, fmt1, i1)) opts x + return (Refined1 a) + +-- | applies a binary operation to two wrapped 'Refined1' parameters +rapply1 :: forall m ip op fmt i . + ( Refined1C ip op fmt i + , Monad m + , Show (PP ip i) + , Show i) + => POpts + -> (PP ip i -> PP ip i -> PP ip i) + -> RefinedT m (Refined1 ip op fmt i) + -> RefinedT m (Refined1 ip op fmt i) + -> RefinedT m (Refined1 ip op fmt i) +rapply1 = rapply1P (Proxy @'(ip,op,fmt,i)) + +-- prtRefinedT $ rapply1P base16 (+) (newRefined1TP Proxy "ff") (newRefined1TP Proxy "22") + +-- | same as 'rapply1' but uses a 4-tuple proxy instead +rapply1P :: forall m ip op fmt i proxy . + ( Refined1C ip op fmt i + , Monad m + , Show (PP ip i) + , Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> (PP ip i -> PP ip i -> PP ip i) + -> RefinedT m (Refined1 ip op fmt i) + -> RefinedT m (Refined1 ip op fmt i) + -> RefinedT m (Refined1 ip op fmt i) +rapply1P p opts f ma mb = do + tell [bgColor Blue "=== a ==="] + Refined1 x <- ma + tell [bgColor Blue "=== b ==="] + Refined1 y <- mb + -- we skip the input value @Id and go straight to the internal value so PP fmt (PP ip i) /= i for this call + tell [bgColor Blue "=== a `op` b ==="] + Refined1 a <- newRefined1TPSkipIPImpl (return . runIdentity) p opts (f x y) + return (Refined1 a) + +-- | An ADT that summarises the results of evaluating Refined1 representing all possible states +data RResults1 a b = + RF String (Tree PE) -- Left e + | RTF a (Tree PE) String (Tree PE) -- Right a + Left e + | RTFalse a (Tree PE) (Tree PE) -- Right a + Right False + | RTTrueF a (Tree PE) (Tree PE) String (Tree PE) -- Right a + Right True + Left e + | RTTrueT a (Tree PE) (Tree PE) b (Tree PE) -- Right a + Right True + Right b + deriving Show + +-- | same as 'prtEval1P' but runs in IO +prtEval1PIO :: forall ip op fmt i proxy + . ( Refined1C ip op fmt i + , Show (PP ip i) + , Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> IO (Either String (Refined1 ip op fmt i)) +prtEval1PIO _ opts i = do + x <- eval1M opts i + prt1IO opts x + +-- | same as 'prtEval1P' but skips the proxy and allows you to set each parameter individually using type application +prtEval1 :: forall ip op fmt i + . ( Refined1C ip op fmt i + , Show (PP ip i) + , Show i) + => POpts + -> i + -> Either Msg1 (Refined1 ip op fmt i) +prtEval1 = prtEval1P Proxy + +-- | create a Refined1 using a 4-tuple proxy and aggregate the results on failure +prtEval1P :: forall ip op fmt i proxy + . ( Refined1C ip op fmt i + , Show (PP ip i) + , Show i) + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> Either Msg1 (Refined1 ip op fmt i) +prtEval1P _ opts = prt1 opts . eval1 opts + +-- | create a Refined1 value using a 4-tuple proxy (see 'mkProxy1') +-- +-- use 'mkProxy1' to package all the types together as a 4-tuple +-- +eval1P :: forall ip op fmt i proxy . Refined1C ip op fmt i + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i)) +eval1P _ opts = runIdentity . eval1M opts + +-- | same as 'eval1P' but can pass the parameters individually using type application +eval1 :: forall ip op fmt i . Refined1C ip op fmt i + => POpts + -> i + -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i)) +eval1 = eval1P Proxy + +eval1M :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i) + => POpts + -> i + -> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i)) +eval1M opts i = do + ll <- eval (Proxy @ip) opts i + case getValAndPE ll of + (Right a, t1) -> do + rr <- evalBool (Proxy @op) opts a + case getValAndPE rr of + (Right True,t2) -> do + ss <- eval (Proxy @fmt) opts a + pure $ case getValAndPE ss of + (Right b,t3) -> (RTTrueT a t1 t2 b t3, Just (Refined1 a)) + (Left e,t3) -> (RTTrueF a t1 t2 e t3, Nothing) + (Right False,t2) -> pure (RTFalse a t1 t2, Nothing) + (Left e,t2) -> pure (RTF a t1 e t2, Nothing) + (Left e,t1) -> pure (RF e t1, Nothing) + +-- | creates Refined1 value but skips the initial conversion +eval1MSkip :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i) + => POpts + -> PP ip i + -> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i)) +eval1MSkip opts a = do + rr <- evalBool (Proxy @op) opts a + case getValAndPE rr of + (Right True,t2) -> do + ss <- eval (Proxy @fmt) opts a + pure $ case getValAndPE ss of + (Right b,t3) -> (RTTrueT a mkNodeSkipP t2 b t3, Just (Refined1 a)) + (Left e,t3) -> (RTTrueF a mkNodeSkipP t2 e t3, Nothing) + (Right False,t2) -> pure (RTFalse a mkNodeSkipP t2, Nothing) + (Left e,t2) -> pure (RTF a mkNodeSkipP e t2, Nothing) + +-- | calculates from internal value +eval1MQuickIdentity :: forall ip op fmt i . Refined1C ip op fmt i + => PP ip i + -> Maybe (Refined1 ip op fmt i) +eval1MQuickIdentity = runIdentity . eval1MQuick + +-- from PP ip i +eval1MQuick :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i) + => PP ip i + -> m (Maybe (Refined1 ip op fmt i)) +eval1MQuick a = do + let opts = oz + rr <- evalBool (Proxy @op) opts a + case getValLRFromTT rr of + Right True -> do + ss <- eval (Proxy @fmt) opts a + pure $ case getValLRFromTT ss of + Right _ -> Just (Refined1 a) + _ -> Nothing + _ -> pure Nothing + +prt1IO :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> IO (Either String r) +prt1IO opts (ret,mr) = do + let m1 = prt1Impl opts ret + unless (hasNoTree opts) $ putStrLn $ m1Long m1 + return $ maybe (Left (m1Desc m1 <> " | " <> m1Short m1)) Right mr + +prt1 :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> Either Msg1 r +prt1 opts (ret,mr) = maybe (Left $ prt1Impl opts ret) Right mr + +data Msg1 = Msg1 { m1Desc :: !String + , m1Short :: !String + , m1Long :: !String + } deriving Eq + +instance Show Msg1 where + show (Msg1 a b c) = a <> " | " <> b <> (if null c then "" else "\n" <> c) + +prt1Impl :: (Show a, Show b) + => POpts + -> RResults1 a b + -> Msg1 +prt1Impl opts v = + let outmsg msg = "\n*** " <> msg <> " ***\n\n" + msg1 a = outmsg ("Step 1. Success Initial Conversion(ip) [" ++ show a ++ "]") + mkMsg1 m n r | hasNoTree opts = Msg1 m n "" + | otherwise = Msg1 m n r + in case v of + RF e t1 -> + let (m,n) = ("Step 1. Initial Conversion(ip) Failed", e) + r = outmsg m + <> prtTreePure opts t1 + in mkMsg1 m n r + RTF a t1 e t2 -> + let (m,n) = ("Step 2. Failed Boolean Check(op)", e) + r = msg1 a + <> fixLite opts a t1 + <> outmsg m + <> prtTreePure opts t2 + in mkMsg1 m n r + RTFalse a t1 t2 -> + let (m,n) = ("Step 2. False Boolean Check(op)", z) + z = case t2 ^? root . pStrings . ix 0 of + Just w -> if null (dropWhile isSpace w) then "FalseP" else "{" <> w <> "}" + Nothing -> "FalseP" + r = msg1 a + <> fixLite opts a t1 + <> outmsg m + <> prtTreePure opts t2 + in mkMsg1 m n r + RTTrueF a t1 t2 e t3 -> + let (m,n) = ("Step 3. Failed Output Conversion(fmt)", e) + r = msg1 a + <> fixLite opts a t1 + <> outmsg "Step 2. Success Boolean Check(op)" + <> prtTreePure opts t2 + <> outmsg m + <> prtTreePure opts t3 + in mkMsg1 m n r + RTTrueT a t1 t2 b t3 -> + let (m,n) = ("Step 3. Success Output Conversion(fmt)", show b) + r = msg1 a + <> fixLite opts a t1 + <> outmsg "Step 2. Success Boolean Check(op)" + <> prtTreePure opts t2 + <> outmsg m + <> fixLite opts b t3 + in mkMsg1 m n r + +-- | similar to 'eval1P' but it emulates 'Refined1' but using 'Refined' +-- +-- takes a 4-tuple proxy as input but outputs the Refined value and the result separately +-- +-- * initial conversion using \'ip\' and stores that in 'Refined' +-- * runs the boolean predicate \'op\' to make sure to validate the converted value from 1. +-- * runs \'fmt\' against the converted value from 1. +-- * returns both the 'Refined' and the output from 3. +-- * if any of the above steps fail the process stops it and dumps out 'RResults1' +-- +eval1PX :: forall ip op fmt i proxy . Refined1C ip op fmt i + => proxy '(ip,op,fmt,i) + -> POpts + -> i + -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i))) +eval1PX _ opts i = runIdentity $ do + ll <- eval (Proxy @ip) opts i + case getValAndPE ll of + (Right a,t1) -> do + rr <- evalBool (Proxy @op) opts a + case getValAndPE rr of + (Right True,t2) -> do + ss <- eval (Proxy @fmt) opts a + pure $ case getValAndPE ss of + (Right b,t3) -> (RTTrueT a t1 t2 b t3, Just (unsafeRefined a, b)) + (Left e,t3) -> (RTTrueF a t1 t2 e t3, Nothing) + (Right False,t2) -> pure (RTFalse a t1 t2, Nothing) + (Left e,t2) -> pure (RTF a t1 e t2, Nothing) + (Left e,t1) -> pure (RF e t1, Nothing) + +-- | same as 'eval1PX' but allows you to set the parameters individually using type application +eval1X :: forall ip op fmt i . Refined1C ip op fmt i + => POpts + -> i + -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i))) +eval1X = eval1PX (Proxy @'(ip,op,fmt,i)) + +-- | emulates 'Refined' using 'Refined1' by setting the input conversion and output formatting as noops +type RefinedEmulate p a = Refined1 Id p Id a + +-- | used by 'Refined1' to extract \'ip\' from a promoted 4-tuple +-- +-- >>> pl @(T4_1 Predicate.Examples.Refined3.Ip4) "1.2.3.4" +-- Present [1,2,3,4] (Map [1,2,3,4] | ["1","2","3","4"]) +-- PresentT [1,2,3,4] +-- +type family T4_1 x where + T4_1 '(a,b,c,d) = a + +-- | used by 'Refined1' for extracting the boolean predicate \'op\' from a promoted 4-tuple +-- +-- >>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4] +-- Error octet 2 out of range 0-255 found 308 +-- FailT "octet 2 out of range 0-255 found 308" +-- +-- >>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4,8] +-- Error Guards:invalid length(5) expected 4 +-- FailT "Guards:invalid length(5) expected 4" +-- +type family T4_2 x where + T4_2 '(a,b,c,d) = b + +-- | used by 'Refined1' for extracting \'fmt\' from a promoted 4-tuple +-- +-- >>> pl @(T4_3 Predicate.Examples.Refined3.Ip4) [141,513,9,4] +-- Present "141.513.009.004" (PrintL(4) [141.513.009.004] | s=%03d.%03d.%03d.%03d) +-- PresentT "141.513.009.004" +-- +type family T4_3 x where + T4_3 '(a,b,c,d) = c + +-- | used by 'Refined1' for extracting the input type \'i\' from a promoted 4-tuple +type family T4_4 x where + T4_4 '(a,b,c,d) = d +
src/Predicate/Refined2.hs view
@@ -21,6 +21,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE NoStarIsType #-} {- | Refinement type allowing the external type to differ from the internal type see 'Refined2' @@ -87,9 +88,9 @@ import Control.Lens ((^?),ix) import Data.Tree.Lens (root) import Data.Char (isSpace) -import Data.Semigroup ((<>)) import Data.String import Data.Hashable (Hashable(..)) +import GHC.Stack -- $setup -- >>> :set -XDataKinds @@ -134,13 +135,13 @@ -- >>> prtEval2 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) oz (2019,10,12) -- Left Step 2. Failed Boolean Check(op) | expected a Sunday -- -data Refined2 ip op i = Refined2 { r2In :: PP ip i, r2Out :: i } +data Refined2 ip op i = Refined2 { r2In :: !(PP ip i), r2Out :: i } type role Refined2 nominal nominal nominal -- | directly load values into 'Refined2'. It still checks to see that those values are valid unsafeRefined2' :: forall ip op i - . (Show (PP ip i), Refined2C ip op i) + . (Show (PP ip i), Refined2C ip op i, HasCallStack) => POpts -> i -> Refined2 ip op i
src/Predicate/Refined3.hs view
@@ -21,6 +21,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE NoStarIsType #-} -- | -- Refinement type allowing the external type to differ from the internal type -- see 'Refined3' @@ -111,9 +112,9 @@ import Control.Lens ((^?),ix) import Data.Tree.Lens (root) import Data.Char (isSpace) -import Data.Semigroup ((<>)) import Data.String import Data.Hashable (Hashable(..)) +import GHC.Stack -- $setup -- >>> :set -XDataKinds @@ -175,13 +176,13 @@ -- >>> prtEval3P (Proxy @(T4 _)) oz (2019,10,13) -- Right (Refined3 {r3In = (2019-10-13,41,7), r3Out = (2019,10,13)}) -- -data Refined3 ip op fmt i = Refined3 { r3In :: PP ip i, r3Out :: PP fmt (PP ip i) } +data Refined3 ip op fmt i = Refined3 { r3In :: !(PP ip i), r3Out :: PP fmt (PP ip i) } type role Refined3 nominal nominal nominal nominal -- | directly load values into 'Refined3'. It still checks to see that those values are valid unsafeRefined3' :: forall ip op fmt i - . (Show i, Show (PP ip i), Refined3C ip op fmt i) + . (HasCallStack, Show i, Show (PP ip i), Refined3C ip op fmt i) => POpts -> i -> Refined3 ip op fmt i
src/Predicate/TH_Orphans.hs view
@@ -3,7 +3,7 @@ {-# LANGUAGE DeriveLift #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE PackageImports #-} +{-# LANGUAGE NoStarIsType #-} {- | Mainly contains useful Template Haskell Lift instances for Date Time -}
src/Predicate/Util.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS -Wall #-} -{-# OPTIONS -Wcompat #-} +{-# OPTIONS -Wno-compat #-} {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# LANGUAGE TypeOperators #-} @@ -21,10 +21,8 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE NoStarIsType #-} {- | Utility methods for Predicate / methods for displaying the evaluation tree -} @@ -72,6 +70,7 @@ -- ** display options , POpts(..) , ODebug(..) + , Disp(..) , defOpts , oz , ol @@ -91,6 +90,7 @@ , color2 , color3 , color4 + , color5 , colorMe , zero , lite @@ -209,13 +209,12 @@ import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as N import Data.Either -import Data.Semigroup ((<>)) import qualified Text.Read.Lex as L import Text.ParserCombinators.ReadPrec import qualified GHC.Read as GR import qualified Data.ByteString.Lazy.Char8 as BL8 import qualified Data.ByteString.Char8 as BS8 - +import GHC.Stack -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications @@ -234,7 +233,25 @@ FalseT :: BoolT Bool -- false predicate TrueT :: BoolT Bool -- true predicate PresentT :: !a -> BoolT a -- non predicate value +{- too restrictive +instance Semigroup a => Semigroup (BoolT a) where + PresentT a <> PresentT a1 = PresentT (a <> a1) +-} +-- | semigroup instance for 'BoolT' +-- +instance Semigroup (BoolT a) where + FailT s <> FailT s1 = FailT (s <> s1) + FailT s <> _ = FailT s + _ <> FailT s = FailT s + FalseT <> _ = FalseT + _ <> FalseT = FalseT + TrueT <> TrueT = TrueT + TrueT <> PresentT a = PresentT a + PresentT a <> TrueT = PresentT a + PresentT a <> PresentT _ = PresentT a + + deriving instance Show a => Show (BoolT a) deriving instance Eq a => Eq (BoolT a) @@ -327,7 +344,6 @@ getValueLRHide :: POpts -> String -> TT a -> [Holder] -> Either (TT x) a getValueLRHide = getValueLRImpl False --- todo: OVerbose? but only works on error -- elide FailT msg in tStrings[0] if showError is False -- | a helper method to add extra context on failure to the tree or extract the value at the root of the tree getValueLRImpl :: Bool -> POpts -> String -> TT a -> [Holder] -> Either (TT x) a @@ -369,7 +385,7 @@ { oWidth = 200 , oDebug = ONormal , oDisp = Ansi - , oColor = color1 + , oColor = color5 } data ODebug = @@ -390,7 +406,7 @@ -- | same as 'ol' but with colors olc :: POpts -olc = ol { oColor = color1 } +olc = ol { oColor = color5 } -- | displays the detailed evaluation tree without colors. o0 :: POpts @@ -451,7 +467,7 @@ -- | color palettes -- -- italics dont work but underline does -color0, color1, color2, color3, color4 :: (String, PColor) +color0, color1, color2, color3, color4, color5 :: (String, PColor) -- | no colors are displayed color0 = ("color0", PColor $ flip const) @@ -459,32 +475,39 @@ -- | default color palette color1 = ("color1",) $ PColor $ \case - FailP {} -> bgColor Magenta + FailP {} -> bgColor Blue FalseP -> bgColor Red - TrueP -> bgColor Green - PresentP -> bgColor Yellow + TrueP -> colorize Foreground Black . bgColor Cyan + PresentP -> colorize Foreground Black . bgColor Yellow color2 = ("color2",) $ PColor $ \case FailP {} -> bgColor Magenta FalseP -> bgColor Red - TrueP -> bgColor White - PresentP -> bgColor Yellow + TrueP -> colorize Foreground Black . bgColor White + PresentP -> colorize Foreground Black . bgColor Yellow color3 = ("color3",) $ PColor $ \case FailP {} -> bgColor Blue FalseP -> color Red TrueP -> color White - PresentP -> bgColor Yellow + PresentP -> colorize Foreground Black . bgColor Yellow color4 = ("color4",) $ PColor $ \case - FailP {} -> bgColor Cyan + FailP {} -> bgColor Red FalseP -> color Red TrueP -> color Green - PresentP -> bgColor Yellow + PresentP -> colorize Foreground Black . bgColor Yellow +color5 = + ("color5",) $ PColor $ \case + FailP {} -> color Blue + FalseP -> color Red + TrueP -> color Cyan + PresentP -> color Yellow + -- | fix PresentT Bool to TrueT or FalseT fixBoolT :: TT Bool -> TT Bool fixBoolT t = @@ -572,11 +595,13 @@ -- | compile a regex using the type level symbol compileRegex :: forall rs a . GetROpts rs => POpts -> String -> String -> [Holder] -> Either (TT a) RH.Regex -compileRegex opts nm s hhs = - let rs = getROpts @rs - mm = nm <> " " <> show rs - in flip left (RH.compileM (B8.pack s) rs) - $ \e -> mkNode opts (FailT "Regex failed to compile") [mm <> " compile failed with regex msg[" <> e <> "]"] hhs +compileRegex opts nm s hhs + | null s = Left (mkNode opts (FailT "Regex cannot be empty") [nm] hhs) + | otherwise = + let rs = getROpts @rs + mm = nm <> " " <> show rs + in flip left (RH.compileM (B8.pack s) rs) + $ \e -> mkNode opts (FailT "Regex failed to compile") [mm <> " compile failed with regex msg[" <> e <> "]"] hhs -- | extract the regex options from the type level list class GetROpts (os :: [ROpt]) where @@ -1090,47 +1115,47 @@ instance InductListC 2 a where type InductListP 2 a = (a,(a,())) inductListC [a,b] = (b,(a,())) - inductListC _ = errorInProgram $ "inductListC: expected 2 values" + inductListC _ = errorInProgram "inductListC: expected 2 values" instance InductListC 3 a where type InductListP 3 a = (a,(a,(a,()))) inductListC [a,b,c] = (c,(b,(a,()))) - inductListC _ = errorInProgram $ "inductListC: expected 3 values" + inductListC _ = errorInProgram "inductListC: expected 3 values" instance InductListC 4 a where type InductListP 4 a = (a,(a,(a,(a,())))) inductListC [a,b,c,d] = (d,(c,(b,(a,())))) - inductListC _ = errorInProgram $ "inductListC: expected 4 values" + inductListC _ = errorInProgram "inductListC: expected 4 values" instance InductListC 5 a where type InductListP 5 a = (a,(a,(a,(a,(a,()))))) inductListC [a,b,c,d,e] = (e,(d,(c,(b,(a,()))))) - inductListC _ = errorInProgram $ "inductListC: expected 5 values" + inductListC _ = errorInProgram "inductListC: expected 5 values" instance InductListC 6 a where type InductListP 6 a = (a,(a,(a,(a,(a,(a,())))))) inductListC [a,b,c,d,e,f] = (f,(e,(d,(c,(b,(a,())))))) - inductListC _ = errorInProgram $ "inductListC: expected 6 values" + inductListC _ = errorInProgram "inductListC: expected 6 values" instance InductListC 7 a where type InductListP 7 a = (a,(a,(a,(a,(a,(a,(a,()))))))) inductListC [a,b,c,d,e,f,g] = (g,(f,(e,(d,(c,(b,(a,()))))))) - inductListC _ = errorInProgram $ "inductListC: expected 7 values" + inductListC _ = errorInProgram "inductListC: expected 7 values" instance InductListC 8 a where type InductListP 8 a = (a,(a,(a,(a,(a,(a,(a,(a,())))))))) inductListC [a,b,c,d,e,f,g,h] = (h,(g,(f,(e,(d,(c,(b,(a,())))))))) - inductListC _ = errorInProgram $ "inductListC: expected 8 values" + inductListC _ = errorInProgram "inductListC: expected 8 values" instance InductListC 9 a where type InductListP 9 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,()))))))))) inductListC [a,b,c,d,e,f,g,h,i] = (i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))) - inductListC _ = errorInProgram $ "inductListC: expected 9 values" + inductListC _ = errorInProgram "inductListC: expected 9 values" instance InductListC 10 a where type InductListP 10 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,())))))))))) inductListC [a,b,c,d,e,f,g,h,i,j] = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))) - inductListC _ = errorInProgram $ "inductListC: expected 10 values" + inductListC _ = errorInProgram "inductListC: expected 10 values" instance InductListC 11 a where type InductListP 11 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,()))))))))))) inductListC [a,b,c,d,e,f,g,h,i,j,k] = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))) - inductListC _ = errorInProgram $ "inductListC: expected 11 values" + inductListC _ = errorInProgram "inductListC: expected 11 values" instance InductListC 12 a where type InductListP 12 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,())))))))))))) inductListC [a,b,c,d,e,f,g,h,i,j,k,l] = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))) - inductListC _ = errorInProgram $ "inductListC: expected 12 values" + inductListC _ = errorInProgram "inductListC: expected 12 values" -- partially apply the 2nd arg to an ADT -- $ and & work with functions only -- doesnt apply more than once because we need to eval it @@ -1148,6 +1173,7 @@ FlipT d p q = d q p type family IfT (b :: Bool) (t :: k) (f :: k) :: k where + -- IfT b x x = x -- todo: benefit? now it needs to eval both sides IfT 'True t f = t IfT 'False t f = f @@ -1209,7 +1235,7 @@ in concat $ unfoldr f e Right a -> show a -errorInProgram :: String -> x +errorInProgram :: HasCallStack => String -> x errorInProgram s = error $ "programmer error:" <> s readField :: String -> ReadPrec a -> ReadPrec a
src/Predicate/Util_TH.hs view
@@ -1,3 +1,4 @@+-- stack exec -- ghc-pkg unregister ghc-lib-parser-8.8.0.20190424 --force {-# OPTIONS -Wall #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} @@ -6,6 +7,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE NoStarIsType #-} {- | Template Haskell methods for creating Refined, Refined2, and Refined3 refinement types -} @@ -15,6 +17,10 @@ refinedTH , refinedTH' + -- ** Refined1 + , refined1TH + , refined1TH' + -- ** Refined2 , refined2TH , refined2TH' @@ -26,25 +32,24 @@ import Predicate.Util import Predicate.Core import Predicate.Refined +import Predicate.Refined1 import Predicate.Refined2 import Predicate.Refined3 import qualified Language.Haskell.TH.Syntax as TH import Data.Functor.Identity -import Data.Semigroup ((<>)) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators +-- >>> :set -XTemplateHaskell +-- >>> :m + Predicate.Prelude -- | creates a 'Refined.Refined' refinement type with terse output -- --- @ --- >$$(refinedTH 123) :: Refined (Between 100 125 Id) Int +-- >>> $$(refinedTH 123) :: Refined (Between 100 125 Id) Int -- Refined {unRefined = 123} --- it :: Refined (Between 100 125 Id) Int --- @ -- -- @ -- >$$(refinedTH 99) :: Refined (Between 100 125 Id) Int @@ -68,11 +73,8 @@ -- -- allows you to specify display options (eg 'ou' for unicode / 'o2' for ansi) -- --- @ --- >$$(refinedTH' o2 123) :: Refined (Between 100 125 Id) Int +-- >>> $$(refinedTH' o2 123) :: Refined (Between 100 125 Id) Int -- Refined {unRefined = 123} --- it :: Refined (Between 100 125 Id) Int --- @ -- -- @ -- >$$(refinedTH' o2 99) :: Refined (FailS "asdf" >> Between 100 125 Id) Int @@ -106,13 +108,75 @@ in fail $ msg1 ++ msg0 ++ ": predicate failed with " ++ show bp ++ " " ++ top Just r -> TH.TExp <$> TH.lift r --- | creates a 'Refined2.Refined2' refinement type with terse output +-- | creates a 'Refined1.Refined1' refinement type with terse output -- +-- >>> $$(refined1TH 100) :: Refined1 Id (Between 100 125 Id) Id Int +-- Refined1 {unRefined1 = 100} +-- +-- >>> $$(refined1TH 100) :: Refined1 Id (Between 100 125 Id) Id Int +-- Refined1 {unRefined1 = 100} +-- +refined1TH :: forall ip op fmt i + . (Show i, Show (PP ip i), TH.Lift i, TH.Lift (PP ip i), Refined1C ip op fmt i) + => i + -> TH.Q (TH.TExp (Refined1 ip op fmt i)) +refined1TH = refined1TH' ol + +-- | creates a 'Refined1.Refined1' refinement type +-- +-- allows you to specify display options (eg 'ou' for unicode / 'o2' for ansi) +-- +-- >>> $$(refined1TH' o2 100) :: Refined1 Id (Between 100 125 Id) Id Int +-- Refined1 {unRefined1 = 100} +-- -- @ --- >$$(refined2TH 100) :: Refined2 Id (Between 100 125 Id) Id Int --- Refined2 {r2In = 100, r2Out = 100} +-- >$$(refined1TH' o2 99) :: Refined1 Id (Between 100 125 Id) Id Int +-- +-- <interactive>:127:4: error: +-- * +-- *** Step 1. Success Initial Conversion(ip) [99] *** +-- +-- P Id 99 +-- +-- *** Step 2. False Boolean Check(op) *** +-- +-- False 100 <= 99 +-- | +-- +- P Id 99 +-- | +-- +- P '100 +-- | +-- `- P '125 +-- +-- refined1TH: predicate failed with Step 2. False Boolean Check(op) | {100 <= 99} +-- * In the Template Haskell splice $$(refined1TH' o2 99) +-- In the expression: +-- $$(refined1TH' o2 99) :: Refined1 Id (Between 100 125 Id) Id Int +-- In an equation for \'it\': +-- it = $$(refined1TH' o2 99) :: Refined1 Id (Between 100 125 Id) Id Int -- @ -- +refined1TH' :: forall ip op fmt i + . (Show i, Show (PP ip i), TH.Lift i, TH.Lift (PP ip i), Refined1C ip op fmt i) + => POpts + -> i + -> TH.Q (TH.TExp (Refined1 ip op fmt i)) +refined1TH' opts i = do + let msg0 = "refined1TH" + (ret,mr) = eval1 @ip @op @fmt opts i + m1 = prt1Impl opts ret + case mr of + Nothing -> + let msg1 = if hasNoTree opts then "" else m1Long m1 ++ "\n" + in fail $ msg1 ++ msg0 ++ ": predicate failed with " ++ (m1Desc m1 <> " | " <> m1Short m1) + Just r -> TH.TExp <$> TH.lift r + + +-- | creates a 'Refined2.Refined2' refinement type with terse output +-- +-- >>> $$(refined2TH 100) :: Refined2 Id (Between 100 125 Id) Int +-- Refined2 {r2In = 100, r2Out = 100} +-- refined2TH :: forall ip op i . (Show (PP ip i), TH.Lift i, TH.Lift (PP ip i), Refined2C ip op i) => i @@ -123,10 +187,8 @@ -- -- allows you to specify display options (eg 'ou' for unicode / 'o2' for ansi) -- --- @ --- >$$(refined2TH' o2 100) :: Refined2 Id (Between 100 125 Id) Int +-- >>> $$(refined2TH' o2 100) :: Refined2 Id (Between 100 125 Id) Int -- Refined2 {r2In = 100, r2Out = 100} --- @ -- -- @ -- >$$(refined2TH' o2 99) :: Refined2 Id (Between 100 125 Id) Int @@ -172,10 +234,8 @@ -- | creates a 'Refined3.Refined3' refinement type with terse output -- --- @ --- >$$(refined3TH 100) :: Refined3 Id (Between 100 125 Id) Id Int +-- >>> $$(refined3TH 100) :: Refined3 Id (Between 100 125 Id) Id Int -- Refined3 {r3In = 100, r3Out = 100} --- @ -- refined3TH :: forall ip op fmt i . (Show i, Show (PP ip i), TH.Lift i, TH.Lift (PP ip i), Refined3C ip op fmt i) @@ -187,10 +247,8 @@ -- -- allows you to specify display options (eg 'ou' for unicode / 'o2' for ansi) -- --- @ --- >$$(refined3TH' o2 100) :: Refined3 Id (Between 100 125 Id) Id Int +-- >>> $$(refined3TH' o2 100) :: Refined3 Id (Between 100 125 Id) Id Int -- Refined3 {r3In = 100, r3Out = 100} --- @ -- -- @ -- >$$(refined3TH' o2 99) :: Refined3 Id (Between 100 125 Id) Id Int
test/TastyExtras.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS -Wall #-} -{-# OPTIONS -Wcompat #-} +{-# OPTIONS -Wno-compat #-} {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# LANGUAGE TypeOperators #-} @@ -12,6 +12,7 @@ {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoStarIsType #-} module TastyExtras where import Test.Tasty import Test.Tasty.HUnit @@ -19,7 +20,6 @@ import Data.Aeson import Data.List import Text.Show.Functions () -import Data.Semigroup (Semigroup(..)) expectIO :: (HasCallStack, Show a) => IO (Either String a) -> (Either String a -> Either String ()) -> IO () expectIO iolr p = do @@ -52,6 +52,12 @@ expectPE :: (Show a, Eq a, HasCallStack) => BoolT a -> IO (BoolT a) -> IO () expectPE bp m = do + x <- m + print (x,bp) + x @?= bp + +expectEQR :: (Show a, Eq a, HasCallStack) => a -> IO a -> IO () +expectEQR bp m = do x <- m print (x,bp) x @?= bp
test/TestJson.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE NoStarIsType #-} module TestJson where import TastyExtras import Test.Tasty
test/TestPredicate.hs view
@@ -13,6 +13,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NoStarIsType #-} module TestPredicate where import Safe import TastyExtras @@ -42,7 +43,9 @@ allTests :: [IO ()] allTests = - [expectPE (PresentT LT) $ pl @("aa" ==! Id) "aaaa" + [ expectPE (PresentT [False,True,True,False]) $ pl @'[Gt 5, Lt 9, Same 4, W 'False] 4 + , expectPE (PresentT [21,19,20,40,60,2]) $ pl @'[Succ Id, Pred Id, Id, Id + Id, Id * 3, Id `Mod` 3] 20 + , expectPE (PresentT LT) $ pl @("aa" ==! Id) "aaaa" , expectPE FalseT $ pl @(FromEnum ("aa" ==! Id) >> Same 1) "aaaa" , expectPE (PresentT (Right 1)) $ pl @(HeadDef 'False Id +++ Id) (Right @[Bool] 1) -- need @[Bool] cos we said 'False! , expectPE (PresentT (Left True)) $ pl @(HeadDef 'False Id +++ Id) (Left @_ @Int [True,False]) -- need @[Bool] cos we said 'False! @@ -250,7 +253,7 @@ , expectPE (PresentT (True,3.4)) $ pl @(Fst (Snd (Thd Id))) (1,'a',('x',((True,3.4),999))) , expectPE (PresentT 7) $ pl @(Fst Id) (7,999.12) , expectPE (PresentT (M.fromList [(1,'a')])) $ pl @(MaybeIn MEmptyP Id) (Just (M.fromList [(1,'a')])) - , expectPE (PresentT (M.fromList [])) $ pl @(MaybeIn MEmptyP Id) (Nothing @(M.Map () ())) + , expectPE (PresentT M.empty) $ pl @(MaybeIn MEmptyP Id) (Nothing @(M.Map () ())) , expectPE (PresentT [("1",["1"]),("2",["2"]),("3",["3"]),("4",["4"])]) $ pl @(Rescan "(\\d)+?" Id) "1234" , expectPE (PresentT [("1234",["4"])]) $ pl @(Rescan "(\\d)+" Id) "1234" , expectPE (PresentT [("1.2",["1",".2","2"]),("3.4",["3",".4","4"])]) $ pl @(Rescan "(\\d{1,3})(\\.(\\d{1,3}))+?" Id) "1.2.3.4" -- overcapturing @@ -626,7 +629,7 @@ , expectPE (PresentT [True,True,True,True]) $ pl @('True <$ Id) [1..4] , expectPE (PresentT (Compose (Just "aaaa"))) $ pl @(Char1 "ab" <$ Id) (Compose $ Just [1..4]) , expectPE (PresentT (4,("aa",'x'))) $ pl @'(4,'(Fst Id,Snd Id)) ("aa",'x') - , expectPE (PresentT (4,"aa",'x')) $ pl @'(4,(Fst Id),Snd Id) ("aa",'x') + , expectPE (PresentT (4,"aa",'x')) $ pl @'(4,Fst Id,Snd Id) ("aa",'x') , expectPE (PresentT (Just [10])) $ pl @(Pure2 []) (Just 10) , expectPE (PresentT "hello") $ pl @Extract (10,"hello") , expectPE (PresentT (M.fromList [(4,"x"),(5,"dd")])) $ pl @(FromList (M.Map _ _)) [(4,"x"),(5,"dd")] @@ -840,6 +843,10 @@ , expectPE (PresentT [3996,998]) $ pl @'[Id * 4, Pred Id] 999 , expectPE (PresentT (These [1,2,3,4] "Abcdef")) $ pz @(MkThat _ "Abc" <> MkThis _ '[1,2] <> MkThese [3,4] "def") () + + -- test semigroup interaction + , expectEQR (These (PresentT 6) (FailT "xyzhello")) $ fmap This (pz @Predicate.Sum [1,2,3]) <> fmap That (pz @(FailS "xyz") 5) <> fmap That (pz @(FailS "hello") 1) + , expectEQR (These (PresentT 6) (PresentT ("5",6))) $ fmap This (pz @Predicate.Sum [1,2,3]) <> fmap That (pz @(ShowP Id &&& Succ Id) 5) ] type Fizzbuzz = '(Id, If (Id `Mod` 3==0) "fizz" "" <> If (Id `Mod` 5==0) "buzz" "")
test/TestRefined.hs view
@@ -17,6 +17,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoStarIsType #-} module TestRefined where import TastyExtras import Test.Tasty @@ -32,8 +33,6 @@ import Data.Aeson import Control.Monad.Cont import Text.Show.Functions () ---import GHC.TypeNats (Nat) -import Data.Semigroup (Semigroup(..)) suite :: TestTree suite =
test/TestRefined2.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoStarIsType #-} module TestRefined2 where import TastyExtras import Test.Tasty @@ -319,7 +320,23 @@ => Either (Results2 i) r -> (RResults2 i, Maybe r) -> IO () -expect2 lhs (rhs,mr) = do +expect2 lhs (rhs,mr) = (@?=) (maybe (Left $ toRResults2 rhs) Right mr) lhs +{- + +test\TestRefined2.hs:77:33: error: + Cannot apply expression of type Proxy _0 + to a visible type argument (Ccn 11) + In the first argument of testRefined2P, namely + (Proxy @_ @(Ccn 11)) + In the first argument of expectRight, namely + (testRefined2P (Proxy @_ @(Ccn 11)) ol "123-45-6---789-03-") + In the expression: + expectRight + (testRefined2P (Proxy @_ @(Ccn 11)) ol "123-45-6---789-03-") + | +77 | , expectRight (testRefined2P (Proxy @(Ccn 11)) ol "123-45-6---789-03-") + | ^^^^^^^^^^^^^^^^^^ +-}
test/TestRefined3.hs view
@@ -17,6 +17,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoStarIsType #-} module TestRefined3 where import TastyExtras import Test.Tasty @@ -43,7 +44,6 @@ import Data.Tree import Data.Maybe import Data.Tree.Lens ---import GHC.TypeLits (Nat) suite :: TestTree suite = @@ -177,7 +177,7 @@ , expect3 (Left $ XTFalse [1,2,3,4,5,6,7,8,9,0,1] "") $ eval3P cc11 oz "12345678901" , expect3 (Right $ unsafeRefined3 ([12,13,14],TimeOfDay 12 13 14) "12:13:14") $ eval3P hms2E ol "12:13:14" - , expect3 (Left (XTF ([12,13,99], TimeOfDay 12 13 99) "seconds invalid: found 99")) $ eval3P hms2E ol "12:13:99" +-- , expect3 (Left (XTF ([12,13,99], TimeOfDay 12 13 99) "seconds invalid: found 99")) $ eval3P hms2E ol "12:13:99" , expect3 (Right (unsafeRefined3 [1,2,3,4] "001.002.003.004")) $ eval3 @Ip4ip @Ip4op' @(ParaN 4 (PrintF "%03d" Id) >> Concat (Intercalate '["."] Id)) ol "1.2.3.4" , expect3 (Right (unsafeRefined3 [1,2,3,4] "abc__002__3__zzz")) $ eval3 @Ip4ip @Ip4op' @(Para '[W "abc",PrintF "%03d" Id,PrintF "%d" Id,W "zzz"] >> Concat (Intercalate '["__"] Id)) ol "1.2.3.4" @@ -194,7 +194,8 @@ [ testProperty "base16" $ forAll (arbRefined3 (mkProxy3 @'(ReadBase Int 16 Id, 'True, ShowBase 16 Id, String))) (\r -> evalQuick @(ReadBase Int 16 Id) (r3Out r) === Right (r3In r)) , testProperty "readshow" $ forAll (arbRefined3 Proxy :: Gen HexLtR3) (\r -> read @HexLtR3 (show r) === r) - , testProperty "jsonroundtrip" $ forAll (arbRefined3 Proxy :: Gen HexLtR3) (\r -> testRefined3PJ Proxy ol (r3Out r) === Right r) + , testProperty "jsonroundtrip1" $ forAll (arbRefined3 Proxy :: Gen HexLtR3) + (\r -> testRefined3PJ Proxy ol (r3Out r) === Right r) ] type HexLtR3 = Refined3 (ReadBase Int 16 Id) (Id < 500) (ShowBase 16 Id) String @@ -368,6 +369,6 @@ => Either (Results3 i j) r -> (RResults3 i j, Maybe r) -> IO () -expect3 lhs (rhs,mr) = do +expect3 lhs (rhs,mr) = (@?=) (maybe (Left $ toRResults3 rhs) Right mr) lhs