predicate-typed 0.3.0.0 → 0.4.0.0
raw patch · 15 files changed
+837/−479 lines, 15 filesdep −assocdep ~th-liftdep ~these
Dependencies removed: assoc
Dependency ranges changed: th-lift, these
Files
- doctests.hs +7/−0
- predicate-typed.cabal +18/−12
- src/Predicate/Core.hs +1/−1
- src/Predicate/Prelude.hs +562/−250
- src/Predicate/Refined.hs +14/−7
- src/Predicate/Refined3.hs +44/−43
- src/Predicate/Refined3Helper.hs +15/−38
- src/Predicate/TH_Orphans.hs +1/−1
- src/Predicate/Util.hs +125/−76
- src/Predicate/Util_TH.hs +3/−3
- test/TastyExtras.hs +1/−2
- test/TestJson.hs +3/−3
- test/TestPredicate.hs +36/−36
- test/TestRefined.hs +2/−2
- test/TestRefined3.hs +5/−5
doctests.hs view
@@ -1,7 +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
predicate-typed.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: e5d65164036af58b0334ef901a340d7945c6977a38df30c57429cef3eb434369+-- hash: 23e1dabfe40eb6dfcb143179b06f919681d58062bc232517452b46889357c319 name: predicate-typed-version: 0.3.0.0+version: 0.4.0.0 synopsis: Predicates, Refinement types and Dsl description: Please see the README on GitHub at <https://github.com/gbwey/predicate-typed#readme> category: Data@@ -39,11 +39,10 @@ Paths_predicate_typed hs-source-dirs: src- ghc-options: -fomit-interface-pragmas+ ghc-options: -fomit-interface-pragmas -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Widentities -fhide-source-paths build-depends: QuickCheck , aeson- , assoc >=1 , base >=4.7 && <5 , binary , bytestring@@ -61,10 +60,13 @@ , safe , template-haskell , text- , th-lift >=0.8.0.1- , these >=1.0.0+ , th-lift+ , 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@@ -77,7 +79,6 @@ build-depends: QuickCheck , aeson- , assoc >=1 , base >=4.7 && <5 , binary , bytestring@@ -97,10 +98,13 @@ , safe , template-haskell , text- , th-lift >=0.8.0.1- , these >=1.0.0+ , th-lift+ , 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@@ -119,7 +123,6 @@ build-depends: QuickCheck , aeson- , assoc >=1 , base >=4.7 && <5 , binary , bytestring@@ -142,8 +145,11 @@ , tasty-quickcheck , template-haskell , text- , th-lift >=0.8.0.1- , these >=1.0.0+ , th-lift+ , 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
@@ -55,11 +55,11 @@ import Data.Kind (Type) import Data.These (These(..)) import Data.Functor.Identity +import Data.Semigroup ((<>)) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- | This is the core class. Each instance of this class can be combined into a dsl using 'Predicate.Prelude.>>' class P p a where
src/Predicate/Prelude.hs view
@@ -2,7 +2,6 @@ {-# OPTIONS -Wcompat #-} {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} -{-# OPTIONS -Wredundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleContexts #-} @@ -21,7 +20,6 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE NoOverloadedLists #-} {- | Dsl for evaluating and displaying type level expressions @@ -474,12 +472,22 @@ -- ** expression combinators , type ($) - , type (&) , Do + , Dot + , RDot , type (>>) , type (<<) , type (>>>) , DoN + , type ($$) + , type ($&) + , K + , Hide + , Hole + , Skip + , type (|>) + , type (>|) + , type (>|>) -- *** parallel expressions , Para @@ -490,12 +498,6 @@ , Prime , Luhn , Char1 - , Hide - , Hole - , Skip - , type (|>) - , type (>|) - , type (>|>) ) where import Predicate.Core import Predicate.Util @@ -518,12 +520,11 @@ import Data.Maybe import Control.Arrow import qualified Data.Semigroup as SG +import Data.Semigroup (Semigroup(..)) import Numeric import Data.Char import Data.Function -import Data.These (These(..), partitionThese) -import qualified Data.Bifunctor.Swap as SW (Swap(..)) -import qualified Data.Bifunctor.Assoc as AS (Assoc(..)) +import Data.These (These(..)) import Data.Ratio import Data.Time import Data.Coerce @@ -544,11 +545,11 @@ -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- >>> :set -XOverloadedStrings -- >>> :set -XNoOverloadedLists -- >>> import qualified Data.Map.Strict as M -- >>> import qualified Data.Text as T +-- >>> import Safe (readNote) -- | a type level predicate for a monotonic increasing list -- @@ -635,8 +636,8 @@ -- | similar to 'all' -- --- >>> pl @(All Even Id) [1,5,11,5,3] --- False (All i=0 (1 == 0) 5 false) +-- >>> pl @(All (Between 1 8) Id) [7,3,4,1,2,9,0,1] +-- False (All(8) i=5 (9 <= 8)) -- FalseT -- -- >>> pz @(All Odd Id) [1,5,11,5,3] @@ -648,7 +649,7 @@ -- TrueT -- -- >>> pe @(All Even Id) [1,5,11,5,3] --- False All i=0 (1 == 0) 5 false +-- False All(5) i=0 (1 == 0) -- | -- +- P Id [1,5,11,5,3] -- | @@ -725,12 +726,13 @@ ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] (toList q) pure $ case splitAndAlign opts [msg0] ts of Left e -> e - Right (vals, ixtts) -> + Right abcs -> let hhs = hh qq : map (hh . fixit) ts - in case filter (not . snd) (zip [0..] vals) of - [] -> mkNodeB opts True [msg0 ++ "(" ++ show (length q) ++ ")"] hhs - (i,_):fs -> let (_,tt) = ixtts !! i - in mkNodeB opts False [msg0 <> " i=" ++ showIndex i ++ " " <> topMessage tt ++ " " ++ show (length fs+1) ++ " false"] hhs + msg1 = msg0 ++ "(" ++ show (length q) ++ ")" + in case find (not . view _1) abcs of + Nothing -> mkNodeB opts True [msg1] hhs + Just (_,(i,_),tt) -> + mkNodeB opts False [msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt] hhs chkSize :: Foldable t => POpts -> String -> t a -> [Holder] -> Either (TT x) () chkSize opts msg0 xs hhs = @@ -742,12 +744,12 @@ showIndex i = show (i+0) -- | similar to 'any' -- --- >>> pz @(Any Even Id) [1,5,11,5,3] --- False +-- >>> pl @(Any Even Id) [1,5,11,5,3] +-- False (Any(5)) -- FalseT -- --- >>> pz @(Any Even Id) [1,5,112,5,3] --- True +-- >>> pl @(Any Even Id) [1,5,112,5,3] +-- True (Any(5) i=2 (0 == 0)) -- TrueT -- -- >>> pz @(Any Even Id) [] @@ -776,12 +778,13 @@ ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] (toList q) pure $ case splitAndAlign opts [msg0] ts of Left e -> e - Right (vals, ixtts) -> + Right abcs -> let hhs = hh qq : map (hh . fixit) ts - in case filter snd (zip [0..] vals) of - [] -> mkNodeB opts False [msg0 ++ "(" ++ show (length q) ++ ")"] hhs - (i,_):fs -> let (_,tt) = ixtts !! i - in mkNodeB opts True [msg0 <> " i=" ++ showIndex i ++ " " <> topMessage tt ++ " " ++ show (length fs+1) ++ " false"] hhs + msg1 = msg0 ++ "(" ++ show (length q) ++ ")" + in case find (view _1) abcs of + Nothing -> mkNodeB opts False [msg1] hhs + Just (_,(i,_),tt) -> + mkNodeB opts True [msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt] hhs -- | a type level predicate for all positive elements in a list @@ -1055,7 +1058,7 @@ -- Requires "Text.Show.Functions" -- -- >>> :m + Text.Show.Functions --- >>> pz @(ReplaceAll "^(\\d+)\\.(\\d+)\\.(\\d+)\\.(\\d+)$" (MakeRR3 (Fst Id)) (Snd Id)) (\ys -> intercalate " | " $ map (show . succ . read @Int) ys, "141.201.1.22") +-- >>> pz @(ReplaceAll "^(\\d+)\\.(\\d+)\\.(\\d+)\\.(\\d+)$" (MakeRR3 (Fst Id)) (Snd Id)) (\ys -> intercalate " | " $ map (show . succ . readNote @Int "invalid int") ys, "141.201.1.22") -- Present "142 | 202 | 2 | 23" -- PresentT "142 | 202 | 2 | 23" -- @@ -1306,8 +1309,11 @@ pure $ case getValueLR opts msg0 pp [] of Left e -> e Right p -> - let d = map (:[]) p - in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp] + case chkSize opts msg0 p [hh pp] of + Left e -> e + Right () -> + let d = map (:[]) p + in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp] -- | similar to 'show' -- @@ -1339,11 +1345,11 @@ -- | type level expression representing a formatted time -- similar to 'Data.Time.formatTime' using a type level 'Symbol' to get the formatting string -- --- >>> pz @(FormatTimeP "%F %T" Id) (read "2019-05-24 05:19:59" :: LocalTime) +-- >>> pz @(FormatTimeP "%F %T" Id) (readNote @LocalTime "invalid localtime" "2019-05-24 05:19:59") -- Present "2019-05-24 05:19:59" -- PresentT "2019-05-24 05:19:59" -- --- >>> pz @(FormatTimeP (Fst Id) (Snd Id)) ("the date is %d/%m/%Y", read "2019-05-24" :: Day) +-- >>> pz @(FormatTimeP (Fst Id) (Snd Id)) ("the date is %d/%m/%Y", readNote @Day "invalid day" "2019-05-24") -- Present "the date is 24/05/2019" -- PresentT "the date is 24/05/2019" -- @@ -1482,7 +1488,7 @@ -- | uncreate a 'Day' returning year month and day -- --- >>> pz @(UnMkDay Id) (read "2019-12-30") +-- >>> pz @(UnMkDay Id) (readNote "invalid day" "2019-12-30") -- Present (2019,12,30) -- PresentT (2019,12,30) -- @@ -1719,7 +1725,7 @@ (hh pp : [hh lhs | length ll > 1] ++ [hh rhs | length rr > 1]) ret <- ff as pure $ case getValueLR opts msg0 ret [hh qq] of - Left _e -> ret -- dont rewrap the error + Left _e -> ret -- dont rewrap else will double up messages: already handled Right xs -> mkNode opts (_tBool ret) [msg0 <> show0 opts " " xs] [hh qq, hh ret] -- | similar to 'length' @@ -1905,7 +1911,7 @@ extractL3C :: tp -> ExtractL3T tp instance ExtractL3C (a,b) where type ExtractL3T (a,b) = GL.TypeError ('GL.Text "Thd doesn't work for 2-tuples") - extractL3C _ = error "Thd doesn't work for 2-tuples" + extractL3C _ = errorInProgram "Thd doesn't work for 2-tuples" instance ExtractL3C (a,b,c) where type ExtractL3T (a,b,c) = c extractL3C (_,_,c) = c @@ -1951,10 +1957,10 @@ extractL4C :: tp -> ExtractL4T tp instance ExtractL4C (a,b) where type ExtractL4T (a,b) = GL.TypeError ('GL.Text "L4 doesn't work for 2-tuples") - extractL4C _ = error "L4 doesn't work for 2-tuples" + extractL4C _ = errorInProgram "L4 doesn't work for 2-tuples" instance ExtractL4C (a,b,c) where type ExtractL4T (a,b,c) = GL.TypeError ('GL.Text "L4 doesn't work for 3-tuples") - extractL4C _ = error "L4 doesn't work for 3-tuples" + extractL4C _ = errorInProgram "L4 doesn't work for 3-tuples" instance ExtractL4C (a,b,c,d) where type ExtractL4T (a,b,c,d) = d extractL4C (_,_,_,d) = d @@ -1993,13 +1999,13 @@ extractL5C :: tp -> ExtractL5T tp instance ExtractL5C (a,b) where type ExtractL5T (a,b) = GL.TypeError ('GL.Text "L5 doesn't work for 2-tuples") - extractL5C _ = error "L5 doesn't work for 2-tuples" + extractL5C _ = errorInProgram "L5 doesn't work for 2-tuples" instance ExtractL5C (a,b,c) where type ExtractL5T (a,b,c) = GL.TypeError ('GL.Text "L5 doesn't work for 3-tuples") - extractL5C _ = error "L5 doesn't work for 3-tuples" + extractL5C _ = errorInProgram "L5 doesn't work for 3-tuples" instance ExtractL5C (a,b,c,d) where type ExtractL5T (a,b,c,d) = GL.TypeError ('GL.Text "L5 doesn't work for 4-tuples") - extractL5C _ = error "L5 doesn't work for 4-tuples" + extractL5C _ = errorInProgram "L5 doesn't work for 4-tuples" instance ExtractL5C (a,b,c,d,e) where type ExtractL5T (a,b,c,d,e) = e extractL5C (_,_,_,_,e) = e @@ -2036,16 +2042,16 @@ extractL6C :: tp -> ExtractL6T tp instance ExtractL6C (a,b) where type ExtractL6T (a,b) = GL.TypeError ('GL.Text "L6 doesn't work for 2-tuples") - extractL6C _ = error "L6 doesn't work for 2-tuples" + extractL6C _ = errorInProgram "L6 doesn't work for 2-tuples" instance ExtractL6C (a,b,c) where type ExtractL6T (a,b,c) = GL.TypeError ('GL.Text "L6 doesn't work for 3-tuples") - extractL6C _ = error "L6 doesn't work for 3-tuples" + extractL6C _ = errorInProgram "L6 doesn't work for 3-tuples" instance ExtractL6C (a,b,c,d) where type ExtractL6T (a,b,c,d) = GL.TypeError ('GL.Text "L6 doesn't work for 4-tuples") - extractL6C _ = error "L6 doesn't work for 4-tuples" + extractL6C _ = errorInProgram "L6 doesn't work for 4-tuples" instance ExtractL6C (a,b,c,d,e) where type ExtractL6T (a,b,c,d,e) = GL.TypeError ('GL.Text "L6 doesn't work for 5-tuples") - extractL6C _ = error "L6 doesn't work for 5-tuples" + extractL6C _ = errorInProgram "L6 doesn't work for 5-tuples" instance ExtractL6C (a,b,c,d,e,f) where type ExtractL6T (a,b,c,d,e,f) = f extractL6C (_,_,_,_,_,f) = f @@ -2053,11 +2059,12 @@ -- | 'fromString' function where you need to provide the type \'t\' of the result -- +-- >>> :set -XFlexibleContexts -- >>> pz @(FromStringP (Identity _) Id) "abc" -- Present Identity "abc" -- PresentT (Identity "abc") -- --- >>> pz @(FromStringP (Seq.Seq _) Id) "abc" +-- >>> pz @(FromStringP (Seq.Seq Char) Id) "abc" -- Present fromList "abc" -- PresentT (fromList "abc") data FromStringP' t s @@ -2603,50 +2610,137 @@ data BinOp = BMult | BSub | BAdd deriving (Show,Eq) -type Mult p q = Bin 'BMult p q -type Add p q = Bin 'BAdd p q -type Sub p q = Bin 'BSub p q - -type p + q = Add p q +data p + q infixl 6 + -type p - q = Sub p q + +instance P (Bin 'BAdd p q) x => P (p + q) x where + type PP (p + q) x = PP (Bin 'BAdd p q) x + eval _ = eval (Proxy @(Bin 'BAdd p q)) + +data p - q infixl 6 - -type p * q = Mult p q + +instance P (Bin 'BSub p q) x => P (p - q) x where + type PP (p - q) x = PP (Bin 'BSub p q) x + eval _ = eval (Proxy @(Bin 'BSub p q)) + +data p * q infixl 7 * -type p > q = Cmp 'Cgt p q +instance P (Bin 'BMult p q) x => P (p * q) x where + type PP (p * q) x = PP (Bin 'BMult p q) x + eval _ = eval (Proxy @(Bin 'BMult p q)) + +data p > q infix 4 > -type p >= q = Cmp 'Cge p q + +instance P (Cmp 'CGt p q) x => P (p > q) x where + type PP (p > q) x = PP (Cmp 'CGt p q) x + eval _ = eval (Proxy @(Cmp 'CGt p q)) + +data p >= q infix 4 >= -type p == q = Cmp 'Ceq p q + +instance P (Cmp 'CGe p q) x => P (p >= q) x where + type PP (p >= q) x = PP (Cmp 'CGe p q) x + eval _ = eval (Proxy @(Cmp 'CGe p q)) + +data p == q infix 4 == -type p /= q = Cmp 'Cne p q -infix 4 /= -type p <= q = Cmp 'Cle p q + +instance P (Cmp 'CEq p q) x => P (p == q) x where + type PP (p == q) x = PP (Cmp 'CEq p q) x + eval _ = eval (Proxy @(Cmp 'CEq p q)) + +data p <= q infix 4 <= -type p < q = Cmp 'Clt p q + +instance P (Cmp 'CLe p q) x => P (p <= q) x where + type PP (p <= q) x = PP (Cmp 'CLe p q) x + eval _ = eval (Proxy @(Cmp 'CLe p q)) + +data p < q infix 4 < -type Gt n = Cmp 'Cgt I n -type Ge n = Cmp 'Cge I n -type Same n = Cmp 'Ceq I n -type Le n = Cmp 'Cle I n -type Lt n = Cmp 'Clt I n -type Ne n = Cmp 'Cne I n +instance P (Cmp 'CLt p q) x => P (p < q) x where + type PP (p < q) x = PP (Cmp 'CLt p q) x + eval _ = eval (Proxy @(Cmp 'CLt p q)) -type p >~ q = CmpI 'Cgt p q +data p /= q +infix 4 /= + +instance P (Cmp 'CNe p q) x => P (p /= q) x where + type PP (p /= q) x = PP (Cmp 'CNe p q) x + eval _ = eval (Proxy @(Cmp 'CNe p q)) + +--type p + q = Bin 'BAdd p q +--type p - q = Bin 'BSub p q +--type p * q = Bin 'BMult p q + +--type p > q = Cmp 'CGt p q +--type p >= q = Cmp 'CGe p q +--type p == q = Cmp 'CEq p q +--type p /= q = Cmp 'CNe p q +--type p <= q = Cmp 'CLe p q +--type p < q = Cmp 'CLt p q + +type Gt n = I > n +type Ge n = I >= n +type Same n = I == n +type Le n = I <= n +type Lt n = I < n +type Ne n = I /= n + +--type p >~ q = CmpI 'CGt p q +--type p >=~ q = CmpI 'CGe p q +--type p ==~ q = CmpI 'CEq p q +--type p <=~ q = CmpI 'CLe p q +--type p <~ q = CmpI 'CLt p q +--type p /=~ q = CmpI 'CNe p q + +data p >~ q infix 4 >~ -type p >=~ q = CmpI 'Cge p q + +instance P (CmpI 'CGt p q) x => P (p >~ q) x where + type PP (p >~ q) x = PP (CmpI 'CGt p q) x + eval _ = eval (Proxy @(CmpI 'CGt p q)) + +data p >=~ q infix 4 >=~ -type p ==~ q = CmpI 'Ceq p q + +instance P (CmpI 'CGe p q) x => P (p >=~ q) x where + type PP (p >=~ q) x = PP (CmpI 'CGe p q) x + eval _ = eval (Proxy @(CmpI 'CGe p q)) + +data p ==~ q infix 4 ==~ -type p /=~ q = CmpI 'Cne p q -infix 4 /=~ -type p <=~ q = CmpI 'Cle p q + +instance P (CmpI 'CEq p q) x => P (p ==~ q) x where + type PP (p ==~ q) x = PP (CmpI 'CEq p q) x + eval _ = eval (Proxy @(CmpI 'CEq p q)) + +data p <=~ q infix 4 <=~ -type p <~ q = CmpI 'Clt p q + +instance P (CmpI 'CLe p q) x => P (p <=~ q) x where + type PP (p <=~ q) x = PP (CmpI 'CLe p q) x + eval _ = eval (Proxy @(CmpI 'CLe p q)) + +data p <~ q infix 4 <~ +instance P (CmpI 'CLt p q) x => P (p <~ q) x where + type PP (p <~ q) x = PP (CmpI 'CLt p q) x + eval _ = eval (Proxy @(CmpI 'CLt p q)) + +data p /=~ q +infix 4 /=~ + +instance P (CmpI 'CNe p q) x => P (p /=~ q) x where + type PP (p /=~ q) x = PP (CmpI 'CNe p q) x + eval _ = eval (Proxy @(CmpI 'CNe p q)) + + class GetBinOp (k :: BinOp) where getBinOp :: (Num a, a ~ b) => (String, a -> b -> a) @@ -3126,17 +3220,29 @@ -- data Swap +class SwapC p where + swap :: p a b -> p b a +instance SwapC Either where + swap (Left a) = Right a + swap (Right a) = Left a +instance SwapC These where + swap (This a) = That a + swap (That b) = This b + swap (These a b) = These b a +instance SwapC (,) where + swap (a,b) = (b,a) + instance (Show (p a b) - , SW.Swap p + , SwapC p , Show (p b a) ) => P Swap (p a b) where type PP Swap (p a b) = p b a eval _ opts pab = let msg0 = "Swap" - d = SW.swap pab + d = swap pab in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pab] [] --- | assoc using 'AS.assoc' +-- | assoc using 'AssocC' -- -- >>> pz @Assoc (This (These 123 'x')) -- Present These 123 (This 'x') @@ -3160,17 +3266,56 @@ -- data Assoc +class AssocC p where + assoc :: p (p a b) c -> p a (p b c) + unassoc :: p a (p b c) -> p (p a b) c +instance AssocC Either where + assoc (Left (Left a)) = Left a + assoc (Left (Right b)) = Right (Left b) + assoc (Right b) = Right (Right b) + unassoc (Left a) = Left (Left a) + unassoc (Right (Left b)) = Left (Right b) + unassoc (Right (Right b)) = Right b +instance AssocC These where + assoc (This (This a)) = This a + assoc (This (That b)) = That (This b) + assoc (That b) = That (That b) + assoc (These (This a) c) = These a (That c) + assoc (These (That b) c) = That (These b c) + assoc (These (These a b) c) = These a (These b c) + assoc (This (These a b)) = These a (This b) + unassoc (This a) = This (This a) + unassoc (That (This b)) = This (That b) + unassoc (That (That b)) = That b + unassoc (These a (That c)) = These (This a) c + unassoc (That (These b c)) = These (That b) c + unassoc (These a (These b c)) = These (These a b) c + unassoc (These a (This b)) = This (These a b) + +partitionThese :: [These a b] -> ([a], [b], [(a, b)]) +partitionThese [] = ([], [], []) +partitionThese (t:ts) = case t of + This x -> (x : xs, ys, xys) + That y -> ( xs, y : ys, xys) + These x y -> ( xs, ys, (x,y) : xys) + where + ~(xs,ys,xys) = partitionThese ts + +instance AssocC (,) where + assoc ((a,b),c) = (a,(b,c)) + unassoc (a,(b,c)) = ((a,b),c) + instance (Show (p (p a b) c) , Show (p a (p b c)) - , AS.Assoc p + , AssocC p ) => P Assoc (p (p a b) c) where type PP Assoc (p (p a b) c) = p a (p b c) eval _ opts pabc = let msg0 = "Assoc" - d = AS.assoc pabc + d = assoc pabc in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pabc] [] --- | unassoc using 'AS.unassoc' +-- | unassoc using 'UnassocC' -- -- >>> pz @Unassoc (These 123 (This 'x')) -- Present This (These 123 'x') @@ -3196,12 +3341,12 @@ instance (Show (p (p a b) c) , Show (p a (p b c)) - , AS.Assoc p + , AssocC p ) => P Unassoc (p a (p b c)) where type PP Unassoc (p a (p b c)) = p (p a b) c eval _ opts pabc = let msg0 = "Unassoc" - d = AS.unassoc pabc + d = unassoc pabc in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pabc] [] -- | bounded 'succ' function @@ -3612,11 +3757,12 @@ -- Present 'w' -- PresentT 'w' -- --- >>> pz @(HeadDef (MEmptyT _) Id) ([] @(SG.Sum _)) +-- >>> :set -XFlexibleContexts +-- >>> pz @(HeadDef (MEmptyT _) Id) ([] :: [SG.Sum Int]) -- Present Sum {getSum = 0} -- PresentT (Sum {getSum = 0}) -- --- >>> pz @(HeadDef (MEmptyT _) '[ "abc","def","asdfadf" ]) () +-- >>> pz @(HeadDef (MEmptyT String) '[ "abc","def","asdfadf" ]) () -- Present "abc" -- PresentT "abc" -- @@ -4125,8 +4271,21 @@ -- Present 12 -- PresentT 12 -- -type FoldMap (t :: Type) p = Map (Wrap t Id) p >> Unwrap (MConcat Id) +data FoldMap (t :: Type) p +instance (PP p x ~ f (Unwrapped t) + , P p x + , Show t + , Show (Unwrapped t) + , Show (f (Unwrapped t)) + , Foldable f + , Monoid t + , Wrapped t + ) => P (FoldMap t p) x where + type PP (FoldMap t p) x = PP (Map (Wrap t Id) p >> Unwrap (MConcat Id)) x + eval _ = eval (Proxy @(Map (Wrap t Id) p >> Unwrap (MConcat Id))) +--type FoldMap (t :: Type) p = Map (Wrap t Id) p >> Unwrap (MConcat Id) + instance (PP p x ~ [a] , P p x , Show a @@ -4243,21 +4402,16 @@ -- | similar to 'Data.List.!!' leveraging 'Ixed' -- --- >>> import qualified Data.Map.Strict as M --- >>> pz @(Id !! 2) ["abc","D","eF","","G"] +-- >>>pz @(IxL Id 2 "notfound") ["abc","D","eF","","G"] -- Present "eF" -- PresentT "eF" -- --- >>> pz @(Id !! 20) ["abc","D","eF","","G"] --- Error (!!) index not found --- FailT "(!!) index not found" --- --- >>> pz @(Id !! "eF") (M.fromList (flip zip [0..] ["abc","D","eF","","G"])) --- Present 2 --- PresentT 2 +-- >>>pz @(IxL Id 20 "notfound") ["abc","D","eF","","G"] +-- Present "notfound" +-- PresentT "notfound" -- data IxL p q def -- p is the big value and q is the index and def is the default -type p !! q = IxL p q (Failp "(!!) index not found") +--type p !! q = IxL p q (Failp "(!!) index not found") instance (P q a , P p a , Show (PP p a) @@ -4285,6 +4439,34 @@ Right _ -> mkNode opts (_tBool rr) [msg1 <> " index not found"] [hh pp, hh qq] Just ret -> pure $ mkNode opts (PresentT ret) [show01' opts msg1 ret "p=" p <> show1 opts " | q=" q] [hh pp, hh qq] +-- | similar to 'Data.List.!!' leveraging 'Ixed' +-- +-- >>> pz @(Id !! 2) ["abc","D","eF","","G"] +-- Present "eF" +-- PresentT "eF" +-- +-- >>> pz @(Id !! 20) ["abc","D","eF","","G"] +-- Error (!!) index not found +-- FailT "(!!) index not found" +-- +-- >>> import qualified Data.Map.Strict as M +-- >>> pz @(Id !! "eF") (M.fromList (flip zip [0..] ["abc","D","eF","","G"])) +-- Present 2 +-- PresentT 2 +-- +data p !! q + +instance ( PP q a ~ Index (PP p a) + , P q a + , P p a + , Ixed (PP p a) + , Show (PP p a) + , Show (Index (PP p a)) + , Show (IxValue (PP p a)) + ) => P (p !! q) a where + type PP (p !! q) a = PP (IxL p q (Failp "(!!) index not found")) a + eval _ = eval (Proxy @(IxL p q (Failp "(!!) index not found"))) + -- | 'lookup' leveraging 'Ixed' -- -- >>> pz @(Lookup Id 2) ["abc","D","eF","","G"] @@ -4615,7 +4797,7 @@ -- Present ("ac",[]) -- PresentT ("ac",[]) -- --- >>> pz @PartitionEithers ([] @(Either _ _)) +-- >>> pz @PartitionEithers ([] :: [Either () Int]) -- Present ([],[]) -- PresentT ([],[]) -- @@ -4690,24 +4872,29 @@ case lr of Left e -> pure e Right (q,r,qq,rr) -> do - let msg1 = msg0 -- <> show0 opts " " q <> show0 opts " " r - ff i b as' rs - | i >= _MX = pure (rs, Left $ mkNode opts (FailT (msg1 <> ":failed at i=" <> showIndex i)) [msg1 <> " i=" <> showIndex i <> " (b,as')=" <> show (b,as')] []) - | otherwise = - case as' of - [] -> pure (rs, Right ()) -- ++ [((i,q), mkNode opts (PresentT q) [msg1 <> "(done)"] [])], Right ()) - a:as -> do - pp :: TT b <- eval (Proxy @p) opts (b,a) - case getValueLR opts (msg1 <> " i=" <> showIndex i <> " a=" <> show a) pp [] of - Left e -> pure (rs,Left e) - Right b' -> ff (i+1) b' as (rs ++ [((i,b), pp)]) - (ts,lrx) :: ([((Int, b), TT b)], Either (TT [b]) ()) <- ff 1 q r [] - pure $ case splitAndAlign opts [msg1] (((0,q), mkNode opts (PresentT q) [msg1 <> "(initial)"] []) : ts) of - Left _e -> error "cant happen!" - Right (vals,itts) -> - case lrx of - Left e -> mkNode opts (_tBool e) [msg1] (hh qq : hh rr : map (hh . fixit) itts ++ [hh e]) - Right () -> mkNode opts (PresentT vals) [show01' opts msg1 vals "b=" q <> show1 opts " | as=" r] (hh qq : hh rr : map (hh . fixit) itts) + case chkSize opts msg0 r [hh rr] of + Left e -> pure e + Right () -> do + let msg1 = msg0 -- <> show0 opts " " q <> show0 opts " " r + ff i b as' rs + | i >= _MX = pure (rs, Left $ mkNode opts (FailT (msg1 <> ":failed at i=" <> showIndex i)) [msg1 <> " i=" <> showIndex i <> " (b,as')=" <> show (b,as')] []) + | otherwise = + case as' of + [] -> pure (rs, Right ()) -- ++ [((i,q), mkNode opts (PresentT q) [msg1 <> "(done)"] [])], Right ()) + a:as -> do + pp :: TT b <- eval (Proxy @p) opts (b,a) + case getValueLR opts (msg1 <> " i=" <> showIndex i <> " a=" <> show a) pp [] of + Left e -> pure (rs,Left e) + Right b' -> ff (i+1) b' as (rs ++ [((i,b), pp)]) + (ts,lrx) :: ([((Int, b), TT b)], Either (TT [b]) ()) <- ff 1 q r [] + pure $ case splitAndAlign opts [msg1] (((0,q), mkNode opts (PresentT q) [msg1 <> "(initial)"] []) : ts) of + Left _e -> errorInProgram "Scanl" + Right abcs -> + let vals = map (view _1) abcs + itts = map (view _2 &&& view _3) abcs + in case lrx of + Left e -> mkNode opts (_tBool e) [msg1] (hh qq : hh rr : map (hh . fixit) itts ++ [hh e]) + Right () -> mkNode opts (PresentT vals) [show01' opts msg1 vals "b=" q <> show1 opts " | as=" r] (hh qq : hh rr : map (hh . fixit) itts) type family UnfoldT mbs where UnfoldT (Maybe (b,s)) = b @@ -4755,13 +4942,15 @@ Right w@(Just (_b,s')) -> ff (i+1) s' (rs ++ [((i,w), pp)]) (ts,lr) :: ([((Int, PP p s), TT (PP p s))], Either (TT [b]) ()) <- ff 1 q [] pure $ case splitAndAlign opts [msg1] ts of - Left _e -> error "cant happen" - Right (vals, itts) -> - case lr of - Left e -> mkNode opts (_tBool e) [msg1] (hh qq : map (hh . fixit) itts ++ [hh e]) - Right () -> - let ret = fst <$> catMaybes vals - in mkNode opts (PresentT ret) [show01' opts msg1 ret "s=" q ] (hh qq : map (hh . fixit) itts) + Left _e -> errorInProgram "Unfoldr" + Right abcs -> + let vals = map (view _1) abcs + itts = map (view _2 &&& view _3) abcs + in case lr of + Left e -> mkNode opts (_tBool e) [msg1] (hh qq : map (hh . fixit) itts ++ [hh e]) + Right () -> + let ret = fst <$> catMaybes vals + in mkNode opts (PresentT ret) [show01' opts msg1 ret "s=" q ] (hh qq : map (hh . fixit) itts) -- | similar to 'map' -- @@ -4790,7 +4979,9 @@ ts <- zipWithM (\i a -> ((i, a),) <$> eval (Proxy @p) opts a) [0::Int ..] (toList q) pure $ case splitAndAlign opts [msg0] ts of Left e -> e - Right (vals, _) -> mkNode opts (PresentT vals) [show01 opts msg0 vals q] (hh qq : map (hh . fixit) ts) + Right abcs -> + let vals = map (view _1) abcs + in mkNode opts (PresentT vals) [show01 opts msg0 vals q] (hh qq : map (hh . fixit) ts) -- | if p then run q else run r -- @@ -4893,10 +5084,11 @@ ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] q pure $ case splitAndAlign opts [msg0] ts of Left e -> e - Right (vals, tfs) -> - let w0 = partition fst $ zip vals tfs - zz1 = (map (snd . fst . snd) *** map (snd . fst . snd)) w0 - in mkNode opts (PresentT zz1) [show01' opts msg0 zz1 "s=" q] (hh qq : map (hh . fixit) tfs) + Right abcs -> + let itts = map (view _2 &&& view _3) abcs + w0 = partition (view _1) abcs + zz1 = (map (view (_2 . _2)) *** map (view (_2 . _2))) w0 + in mkNode opts (PresentT zz1) [show01' opts msg0 zz1 "s=" q] (hh qq : map (hh . fixit) itts) -- | similar to 'break' @@ -4928,7 +5120,7 @@ case chkSize opts msg0 q [hh qq] of Left e -> pure e Right () -> do - let ff [] zs = pure (zs, [], Nothing) -- [(ia,qq)] extras | the rest of the data | optional last pivot or error + let ff [] zs = pure (zs, [], Nothing) -- [(ia,qq)] extras | the rest of the data | optional last pivot or failure ff ((i,a):ias) zs = do pp <- evalBool (Proxy @p) opts a let v = ((i,a), pp) @@ -4936,7 +5128,7 @@ Right False -> ff ias (zs Seq.|> v) Right True -> pure (zs,map snd ias,Just v) Left _ -> pure (zs,map snd ias,Just v) - (ialls,rhs,mpivot) <- ff (zip [0::Int ..] q) Seq.empty + (ialls,rhs,mpivot) <- ff (itoList q) Seq.empty pure $ case mpivot of Nothing -> mkNode opts (PresentT (map (snd . fst) (toList ialls), rhs)) @@ -4949,7 +5141,7 @@ ([msg0] <> ["cnt=" <> show (length ialls, 1+length rhs)]) (hh qq : hh tt : map (hh . fixit) (toList (ialls Seq.|> iall))) - Right False -> error "shouldnt happen" + Right False -> errorInProgram "Break" Left e -> e -- | Fails the computation with a message @@ -5228,16 +5420,16 @@ -- FailT "arg1 failed" -- -- >>> pz @(Guards '[ '(PrintT "arg %d failed with value %d" Id,Gt 4), '(PrintT "%d %d" Id, Same 4)]) [17,3] --- Error 2 3 --- FailT "2 3" +-- Error 1 3 +-- FailT "1 3" -- -- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5] --- Error arg 3 failed with value 5 --- FailT "arg 3 failed with value 5" +-- Error arg 2 failed with value 5 +-- FailT "arg 2 failed with value 5" -- -- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5,99] --- Error Guards: data elements(4) /= predicates(3) --- FailT "Guards: data elements(4) /= predicates(3)" +-- Error Guards: predicates(3) /= data elements(4) +-- FailT "Guards: predicates(3) /= data elements(4)" -- data GuardsImpl (n :: Nat) (os :: [(k,k1)]) type GuardsQuick (prt :: k) (os :: [k1]) = Guards (ToGuardsT prt os) @@ -5250,7 +5442,7 @@ let msgbase0 = "Guards" n = getLen @ps if n /= length as then - let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")" + let xx = msgbase0 <> ": predicates(" <> show n <> ") /= data elements(" <> show (length as) <> ")" in pure $ mkNode opts (FailT xx) [xx] [] else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as @@ -5261,8 +5453,8 @@ eval _ opts as = let msg0 = "Guards" <> "(" <> show n <> ")" n :: Int = nat @n - in if not (null as) then error $ "programmer error: GuardsImpl base case has extra data " ++ show as - else pure $ mkNode opts (PresentT as) [msg0 <> " done!"] [] + in if not (null as) then errorInProgram $ "GuardsImpl base case has extra data " ++ show as + else pure $ mkNode opts (PresentT as) [msg0 <> " empty"] [] instance (PP prt (Int, a) ~ String , P prt (Int, a) @@ -5276,55 +5468,75 @@ ) => P (GuardsImpl n ('(prt,p) ': ps)) [a] where type PP (GuardsImpl n ('(prt,p) ': ps)) [a] = [a] eval _ opts as' = do - let msgbase1 = "Guard" <> "(" <> show (n-pos) <> ")" + let cpos = n-pos-1 + msgbase1 = "Guards" <> "(" <> show cpos <> ")" msgbase2 = "Guards" n :: Int = nat @n pos = getLen @ps case as' of a:as -> do - pp <- evalBool (Proxy @p) opts a - case getValueLR opts (msgbase1 <> " p failed") pp [] of - Left e -> pure e - Right False -> do - qq <- eval (Proxy @prt) opts (n-pos,a) -- only run prt when predicate is False - pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of - Left e -> e - Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else []) - Right True -> do - ss <- eval (Proxy @(GuardsImpl n ps)) opts as - pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of - Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! - Right zs -> mkNode opts (PresentT (a:zs)) [msgbase1 <> show0 opts " " a] [hh pp, hh ss] - _ -> error $ "programmer error: GuardsImpl n+1 case has no data" + pp <- evalBool (Proxy @p) opts a + case getValueLR opts (msgbase1 <> " p failed") pp [] of + Left e -> pure e + Right False -> do + qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False + pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of + Left e -> e + Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else []) + Right True -> do + if pos == 0 then -- we are at the bottom of the tree + pure $ mkNode opts (PresentT [a]) [msgbase2 <> "("++show n++") done!"] [hh pp] + else do + ss <- eval (Proxy @(GuardsImpl n ps)) opts as + pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of + Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! + Right zs -> (ss & tForest %~ \x -> fromTT pp : x) & tBool .~ PresentT (a:zs) +-- let tt = mkNode opts (PresentT (a:zs)) [msgbase1] [hh pp, hh ss] +-- in if top then mkNode opts (PresentT (a:zs)) [msgbase2 <> "("++show n++") done!"] [hh tt] +-- else tt + _ -> errorInProgram $ "GuardsImpl n+1 case has no data" + -- | boolean guard which checks a given a list of predicates against the list of values -- -- pulls the top message from the tree if a predicate is false -- -- >>> pl @(Bools '[ '(W "hh",Between 0 23), '(W "mm",Between 0 59), '(PrintT "<<<%d %d>>>" Id,Between 0 59) ] ) [12,93,14] --- False (GuardBool(1) [mm] (93 <= 59)) +-- False (Bools(1) [mm] (93 <= 59)) -- FalseT -- -- >>> pl @(Bools '[ '(W "hh",Between 0 23), '(W "mm",Between 0 59), '(PrintT "<<<%d %d>>>" Id,Between 0 59) ] ) [12,13,94] --- False (GuardBool(2) [<<<2 94>>>] (94 <= 59)) +-- False (Bools(2) [<<<2 94>>>] (94 <= 59)) -- FalseT -- -- >>> pl @(Bools '[ '(W "hh",Between 0 23), '(W "mm",Between 0 59), '(PrintT "<<<%d %d>>>" Id,Between 0 59) ] ) [12,13,14] --- True (GuardBool(0) 12) +-- True (Bools(3) done!) -- TrueT -- -- >>> pl @(BoolsQuick "abc" '[Between 0 23, Between 0 59, Between 0 59]) [12,13,14] --- True (GuardBool(0) 12) +-- True (Bools(3) done!) -- TrueT -- -- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23, Between 0 59, Between 0 59]) [12,13,14] --- True (GuardBool(0) 12) +-- True (Bools(3) done!) -- TrueT -- -- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23, Between 0 59, Between 0 59]) [12,13,99] --- False (GuardBool(2) [id=2 val=99] (99 <= 59)) +-- False (Bools(2) [id=2 val=99] (99 <= 59)) -- FalseT -- +-- >>> pl @(Bools '[ '("hours",Between 0 23), '("minutes",Between 0 59), '("seconds",Between 0 59) ] ) [12,13,14] +-- True (Bools(3) done!) +-- TrueT +-- +-- >>> pl @(Bools '[ '("hours",Between 0 23), '("minutes",Between 0 59), '("seconds",Between 0 59) ] ) [12,60,14] +-- False (Bools(1) [minutes] (60 <= 59)) +-- FalseT +-- +-- >>> pl @(Bools '[ '("hours",Between 0 23), '("minutes",Between 0 59), '("seconds",Between 0 59) ] ) [12,60,14,20] +-- False (Bools(3): predicates(3) /= data elements(4)) +-- FalseT +-- data Bools (ps :: [(k,k1)]) type BoolsQuick (prt :: k) (ps :: [k1]) = Bools (ToGuardsT prt ps) @@ -5334,12 +5546,15 @@ ) => P (Bools ps) [a] where type PP (Bools ps) [a] = Bool eval _ opts as = do - let msgbase0 = "Bools("++show n++")" + let msg0 = "Bools("++show n++")" n = getLen @ps - if n /= length as then - let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")" - in pure $ mkNode opts (FailT xx) [xx] [] - else evalBool (Proxy @(BoolsImpl (LenT ps) ps)) opts as + case chkSize opts msg0 as [] of + Left e -> pure e + Right () -> do + if n /= length as then + let msg1 = msg0 <> ": predicates(" <> show n <> ") /= data elements(" <> show (length as) <> ")" + in pure $ mkNodeB opts False [msg1] [] -- was FailT but now just FalseT + else evalBool (Proxy @(BoolsImpl (LenT ps) ps)) opts as data BoolsImpl (n :: Nat) (os :: [(k,k1)]) @@ -5350,8 +5565,8 @@ eval _ opts as = let msg0 = "Bools" <> "(" <> show n <> ")" n :: Int = nat @n - in if not (null as) then error $ "programmer error: BoolsImpl base case has extra data " ++ show as - else pure $ mkNodeB opts True [msg0 <> " done!"] [] + in if not (null as) then errorInProgram $ "BoolsImpl base case has extra data " ++ show as + else pure $ mkNodeB opts True [msg0 <> " empty"] [] instance (PP prt (Int, a) ~ String , P prt (Int, a) @@ -5361,42 +5576,44 @@ , PP p a ~ Bool , P (BoolsImpl n ps) [a] , PP (BoolsImpl n ps) [a] ~ Bool - , Show a +-- , Show a ) => P (BoolsImpl n ('(prt,p) ': ps)) [a] where type PP (BoolsImpl n ('(prt,p) ': ps)) [a] = Bool eval _ opts as' = do let cpos = n-pos-1 - msgbase1 = "GuardBool" <> "(" <> showIndex cpos <> ")" + msgbase1 = "Bools" <> "(" <> showIndex cpos <> ")" msgbase2 = "Bools" n :: Int = nat @n pos = getLen @ps case as' of a:as -> do - pp <- evalBool (Proxy @p) opts a - case getValueLR opts (msgbase1 <> " p failed") pp [] of - Left e -> pure e - Right False -> do - qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False - pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of - Left e -> e - Right msgx -> mkNodeB opts False [msgbase1 <> " [" <> msgx <> "] " <> topMessage pp] (hh pp : if isVerbose opts then [hh qq] else []) - Right True -> do - ss <- evalBool (Proxy @(BoolsImpl n ps)) opts as - pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of - Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! - Right True -> mkNodeB opts True [msgbase1 <> show0 opts " " a] [hh pp, hh ss] - Right False -> ss & tForest %~ \x -> fromTT pp : x - _ -> error $ "programmer error: BoolsImpl n+1 case has no data" + pp <- evalBool (Proxy @p) opts a + case getValueLR opts (msgbase1 <> " p failed") pp [] of + Left e -> pure e + Right False -> do + qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False + pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of + Left e -> e + Right msgx -> mkNodeB opts False [msgbase1 <> " [" <> msgx <> "] " <> topMessage pp] (hh pp : if isVerbose opts then [hh qq] else []) + Right True -> do + if pos == 0 then -- we are at the bottom of the tree + pure $ mkNodeB opts True [msgbase2 <> "("++show n++") done!"] [hh pp] + else do + ss <- evalBool (Proxy @(BoolsImpl n ps)) opts as + pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of + Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! + Right _ -> ss & tForest %~ \x -> fromTT pp : x + _ -> errorInProgram $ "BoolsImpl n+1 case has no data" -- | leverages 'RepeatT' for repeating predicates (passthrough method) -- -- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255)) [121,33,7,256] --- False (GuardBool(3) [id=3 must be between 0 and 255, found 256] (256 <= 255)) +-- False (Bools(3) [id=3 must be between 0 and 255, found 256] (256 <= 255)) -- FalseT -- --- >>> pz @(GuardsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255)) [121,33,7,44] --- Present [121,33,7,44] --- PresentT [121,33,7,44] +-- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255)) [121,33,7,44] +-- True (Bools(4) done!) +-- TrueT -- data BoolsN prt (n :: Nat) p @@ -5444,7 +5661,7 @@ let msgbase0 = "Guards" n = getLen @ps if n /= length as then - let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")" + let xx = msgbase0 <> ": predicates(" <> show n <> ") /= data elements(" <> show (length as) <> ")" in pure $ mkNode opts (FailT xx) [xx] [] else eval (Proxy @(GuardsImplX (LenT ps) ps)) opts as @@ -5455,7 +5672,7 @@ eval _ opts as = let msg0 = "Guards" <> "(" <> show n <> ")" n :: Int = nat @n - in if not (null as) then error $ "programmer error: GuardsImplX base case has extra data " ++ show as + in if not (null as) then errorInProgram $ "GuardsImplX base case has extra data " ++ show as else pure $ mkNode opts (PresentT as) [msg0 <> " done!"] [] instance (PP prt a ~ String @@ -5477,26 +5694,26 @@ pos = getLen @ps case as' of a:as -> do - pp <- evalBool (Proxy @p) opts a - case getValueLR opts (msgbase1 <> " p failed") pp [] of - Left e -> pure e - Right False -> do - qq <- eval (Proxy @prt) opts a -- only run prt when predicate is False - pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of - Left e -> e - Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else []) - Right True -> do - ss <- eval (Proxy @(GuardsImplX n ps)) opts as - pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of - Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! - Right zs -> mkNode opts (PresentT (a:zs)) [msgbase1 <> show0 opts " " a] [hh pp, hh ss] - _ -> error $ "programmer error: GuardsImplX n+1 case has no data" + pp <- evalBool (Proxy @p) opts a + case getValueLR opts (msgbase1 <> " p failed") pp [] of + Left e -> pure e + Right False -> do + qq <- eval (Proxy @prt) opts a -- only run prt when predicate is False + pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of + Left e -> e + Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else []) + Right True -> do + ss <- eval (Proxy @(GuardsImplX n ps)) opts as + pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of + Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time! + Right zs -> mkNode opts (PresentT (a:zs)) [msgbase1 <> show0 opts " " a] [hh pp, hh ss] + _ -> errorInProgram $ "GuardsImplX n+1 case has no data" -- | leverages 'RepeatT' for repeating predicates (passthrough method) -- -- >>> pz @(GuardsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255)) [121,33,7,256] --- Error id=4 must be between 0 and 255, found 256 --- FailT "id=4 must be between 0 and 255, found 256" +-- Error id=3 must be between 0 and 255, found 256 +-- FailT "id=3 must be between 0 and 255, found 256" -- -- >>> pz @(GuardsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255)) [121,33,7,44] -- Present [121,33,7,44] @@ -5555,7 +5772,7 @@ -- | similar to 'Guard' but uses the root message of the False predicate case as the failure message -- --- most uses of GuardSimple can be replaced by using 'ol' and a boolean predicate unless you require failure on error +-- most uses of GuardSimple can be replaced by using 'ol' and a boolean predicate unless you require failure -- -- >>> pz @(GuardSimple (Luhn Id)) [1..4] -- Error (Luhn map=[4,6,2,2] sum=14 ret=4 | [1,2,3,4]) @@ -5593,7 +5810,7 @@ -- | just run the effect but skip the value --- for example for use with Stdout so it doesnt interfere with the \'a\' on the rhs unless there is an error +-- for example for use with Stdout so it doesnt interfere with the \'a\' on the rhs unless there is an failure data Skip p type p |> q = Skip p >> q infixr 1 |> @@ -5867,6 +6084,23 @@ in mkNode opts (PresentT d) [msg0 <> " " <> p <> " " <> prettyOrd d <> " " <> q] [hh pp, hh qq] -- | compare two values using the given ordering \'o\' +-- +-- >>> pl @(Lt 4) 123 +-- False (123 < 4) +-- FalseT +-- +-- >>> pl @(Lt 4) 1 +-- True (1 < 4) +-- TrueT +-- +-- >>> pl @(Between (Negate 7) 20) (-4) +-- True (-7 <= -4 <= 20) +-- TrueT +-- +-- >>> pl @(Between (Negate 7) 20) 21 +-- False (21 <= 20) +-- FalseT +-- data Cmp (o :: OrderingP) p q instance (GetOrd o @@ -6097,7 +6331,7 @@ pure $ case getValueLR opts msg0 pp [] of Left e -> e Right p -> - let (t,f) = getThese (Proxy @th) + let (t,f) = getThese @th b = f p in mkNodeB opts b [msg0 <> " " <> t <> show1 opts " | " p] [] @@ -6202,8 +6436,9 @@ instance (KnownSymbol s, NullT s ~ 'False) => P (Char1 s) a where type PP (Char1 s) a = Char eval _ opts _ = - let c = head $ symb @s - in pure $ mkNode opts (PresentT c) ["Char1" <> show0 opts " " c] [] + case symb @s of + [] -> errorInProgram "Char1: found empty Symbol/string" + c:_ -> pure $ mkNode opts (PresentT c) ["Char1" <> show0 opts " " c] [] -- | similar to 'Data.Align.align' thats pads with 'Data.These.This' or 'Data.These.That' if one list is shorter than the other -- @@ -6245,8 +6480,12 @@ pure $ case lr of Left e -> e Right (p,q,pp,qq) -> - let d = simpleAlign p q - in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] [hh pp, hh qq] + let hhs = [hh pp, hh qq] + in case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of + Left e -> e + Right () -> + let d = simpleAlign p q + in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] hhs simpleAlign :: [a] -> [b] -> [These a b] simpleAlign as [] = map This as @@ -6260,7 +6499,7 @@ ':$$: 'GL.Text "t a = " ':<>: 'GL.ShowType z) --- todo: get ExtractAFromList error to fire if wrong Type +-- todo: get ExtractAFromList failure to fire if wrong Type -- | extract \'a\' from \'[a]\' which I need for type PP type family ExtractAFromList (as :: Type) :: Type where ExtractAFromList [a] = a @@ -6572,7 +6811,7 @@ getValidBase n = let xs = ['0'..'9'] <> ['a'..'z'] len = length xs - in if n > len || n < 2 then error $ "oops invalid base valid is 2 thru " ++ show len ++ " found " ++ show n + in if n > len || n < 2 then errorInProgram $ "getValidBase: oops invalid base valid is 2 thru " ++ show len ++ " found " ++ show n else take n xs -- | Display a number at base 2 to 36, similar to 'showIntAtBase' but supports signed numbers @@ -6645,8 +6884,12 @@ pure $ case lr of Left e -> e Right (p,q,pp,qq) -> - let d = intercalate p (map (:[]) q) - in mkNode opts (PresentT d) [show01 opts msg0 d p <> show1 opts " | " q] [hh pp, hh qq] + let hhs = [hh pp, hh qq] + in case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of + Left e -> e + Right () -> + let d = intercalate p (map (:[]) q) + in mkNode opts (PresentT d) [show01 opts msg0 d p <> show1 opts " | " q] hhs -- | uses PrintF to format output -- @@ -6703,8 +6946,8 @@ -- PresentT [10,21,120] -- -- >>> pz @(Para '[Id,Id + 1,Id * 4]) [10,20,30,40] --- Error Para: data elements(4) /= predicates(3) --- FailT "Para: data elements(4) /= predicates(3)" +-- Error Para: predicates(3) /= data elements(4) +-- FailT "Para: predicates(3) /= data elements(4)" -- data ParaImpl (n :: Nat) (os :: [k]) @@ -6717,7 +6960,7 @@ let msgbase0 = "Para" n = getLen @ps if n /= length as then - let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")" + let xx = msgbase0 <> ": predicates(" <> show n <> ") /= data elements(" <> show (length as) <> ")" in pure $ mkNode opts (FailT xx) [xx] [] else eval (Proxy @(ParaImpl (LenT ps) ps)) opts as @@ -6725,7 +6968,7 @@ instance GL.TypeError ('GL.Text "ParaImpl '[] invalid: requires at least one value in the list") => P (ParaImpl n ('[] :: [k])) [a] where type PP (ParaImpl n ('[] :: [k])) [a] = Void - eval _ _ _ = error "should not be called and yet..." + eval _ _ _ = errorInProgram "ParaImpl empty list" instance (Show (PP p a) , KnownNat n @@ -6744,9 +6987,9 @@ pure $ case getValueLR opts msgbase1 pp [] of Left e -> e -- show1 opts " " [b] fails but using 'b' is ok and (b : []) also works! - -- GE.List error + -- GE.List problem Right b -> mkNode opts (PresentT [b]) [msgbase1 <> show0 opts " " (b : []) <> show1 opts " | " a] [hh pp] - _ -> error $ "programmer error: ParaImpl base case should have exactly one element but found " ++ show as' + _ -> errorInProgram $ "ParaImpl base case should have exactly one element but found " ++ show as' instance (KnownNat n , GetLen ps @@ -6775,7 +7018,7 @@ pure $ case getValueLRHide opts (msgbase1 <> " rhs failed " <> show b) qq [hh pp] of Left e -> e Right bs -> mkNode opts (PresentT (b:bs)) [msgbase1 <> show0 opts " " (b:bs) <> show1 opts " | " as'] [hh pp, hh qq] - _ -> error $ "programmer error: ParaImpl n+1 case has no data left" + _ -> errorInProgram $ "ParaImpl n+1 case has no data left" -- | leverages 'Para' for repeating predicates (passthrough method) -- @@ -6784,8 +7027,8 @@ -- PresentT [2,3,4,5] -- -- >>> pz @(ParaN 4 (Succ Id)) "azwxm" --- Error Para: data elements(5) /= predicates(4) --- FailT "Para: data elements(5) /= predicates(4)" +-- Error Para: predicates(4) /= data elements(5) +-- FailT "Para: predicates(4) /= data elements(5)" -- -- >>> pz @(ParaN 4 (Succ Id)) "azwx" -- Present "b{xy" @@ -6844,17 +7087,17 @@ instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lhs requires at least one value in the list")) => P (CaseImpl n e ('[] :: [k]) (q ': qs) r) x where type PP (CaseImpl n e ('[] :: [k]) (q ': qs) r) x = Void - eval _ _ _ = error "should not be called and yet..." + eval _ _ _ = errorInProgram "CaseImpl lhs empty" instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: rhs requires at least one value in the list")) => P (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x where type PP (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x = Void - eval _ _ _ = error "should not be called and yet..." + eval _ _ _ = errorInProgram "CaseImpl rhs empty" instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lists are both empty")) => P (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x where type PP (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x = Void - eval _ _ _ = error "should not be called and yet..." + eval _ _ _ = errorInProgram "CaseImpl both lists empty" instance (P r x , P q (PP r x) @@ -7538,16 +7781,16 @@ -- | function application for expressions: similar to 'GHC.Base.$' -- --- pz @(Fst Id $ Snd Id) ((*16),4) +-- pz @(Fst Id $$ Snd Id) ((*16),4) -- Present 64 -- PresentT 64 -- --- pz @(Id $ "def") ("abc"<>) +-- pz @(Id $$ "def") ("abc"<>) -- Present "abcdef" -- PresentT "abcdef" -- -data p $ q -infixl 0 $ +data p $$ q +infixl 0 $$ instance (P p x , P q x @@ -7556,31 +7799,31 @@ , PP q x ~ a , Show a , Show b - ) => P (p $ q) x where - type PP (p $ q) x = FnT (PP p x) + ) => P (p $$ q) x where + type PP (p $$ q) x = FnT (PP p x) eval _ opts x = do - let msg0 = "($)" + let msg0 = "($$)" lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x [] pure $ case lr of Left e -> e Right (p,q,pp,qq) -> let d = p q - in mkNode opts (PresentT d) ["fn $ " <> show q <> " = " <> show d] [hh pp, hh qq] + in mkNode opts (PresentT d) ["fn $$ " <> show q <> " = " <> show d] [hh pp, hh qq] -- reify this so we can combine (type synonyms dont work as well) -- | flipped function application for expressions: similar to 'Control.Lens.&' -- --- pz @(Snd Id & Fst Id) ((*16),4) +-- pz @(Snd Id $& Fst Id) ((*16),4) -- Present 64 -- PresentT 64 -- --- pz @("def" & Id) ("abc"<>) +-- pz @("def" $& Id) ("abc"<>) -- Present "abcdef" -- PresentT "abcdef" -- -data q & p -- flips the args eg a & b & (,) = (b,a) -infixr 1 & +data q $& p -- flips the args eg a & b & (,) = (b,a) +infixr 1 $& instance (P p x , P q x @@ -7589,16 +7832,16 @@ , PP q x ~ a , Show a , Show b - ) => P (q & p) x where - type PP (q & p) x = FnT (PP p x) + ) => P (q $& p) x where + type PP (q $& p) x = FnT (PP p x) eval _ opts x = do - let msg0 = "(&)" + let msg0 = "($&)" lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x [] pure $ case lr of Left e -> e Right (p,q,pp,qq) -> let d = p q - in mkNode opts (PresentT d) ["fn & " <> show q <> " = " <> show d] [hh pp, hh qq] + in mkNode opts (PresentT d) ["fn $& " <> show q <> " = " <> show d] [hh pp, hh qq] type family FnT ab :: Type where FnT (a -> b) = b @@ -7961,7 +8204,7 @@ Right p -> mkNode opts (PresentT p) [msg0 <> " Left"] [hh qq, hh pp] --- | extract the Left value from an 'Either' otherwise fail with an error message +-- | extract the Left value from an 'Either' otherwise fail with a message -- -- if there is no Left value then \p\ is passed the Right value and the whole context -- @@ -8004,7 +8247,7 @@ Right p -> mkNode opts (FailT p) [msg0 <> " Right"] [hh qq, hh pp] --- | extract the Right value from an 'Either' otherwise fail with an error message +-- | extract the Right value from an 'Either' otherwise fail with a message -- -- if there is no Right value then \p\ is passed the Left value and the whole context -- @@ -8221,7 +8464,7 @@ Right p -> mkNode opts (PresentT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp] --- | extract the This value from a 'These' otherwise fail with an error message +-- | extract the This value from a 'These' otherwise fail with a message -- -- if there is no This value then \p\ is passed the whole context only -- @@ -8264,7 +8507,7 @@ Right p -> mkNode opts (FailT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp] --- | extract the That value from a 'These' otherwise fail with an error message +-- | extract the That value from a 'These' otherwise fail with a message -- -- if there is no That value then \p\ is passed the whole context only -- @@ -8309,7 +8552,7 @@ --- | extract the These value from a 'These' otherwise fail with an error message +-- | extract the These value from a 'These' otherwise fail with a message -- -- if there is no These value then \p\ is passed the whole context only -- @@ -8505,3 +8748,72 @@ case p of Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " found Nothing"] [hh pp] Just d -> mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp] + + +-- | dot +-- +-- >>>pl @(Dot '[Thd,Snd,Fst] Id) ((1,(2,9,10)),(3,4)) +-- Present 10 (Thd 10 | (2,9,10)) +-- PresentT 10 +-- +data Dot (ps :: [Type -> Type]) (q :: Type) +instance (P (DotExpandT ps q) a) => P (Dot ps q) a where + type PP (Dot ps q) a = PP (DotExpandT ps q) a + eval _ = eval (Proxy @(DotExpandT ps q)) + +type family DotExpandT (ps :: [Type -> Type]) (q :: Type) :: Type where + DotExpandT '[] _ = GL.TypeError ('GL.Text "'[] invalid: requires at least one predicate in the list") + DotExpandT '[p] q = p $ q + DotExpandT (p ': p1 ': ps) q = p $ DotExpandT (p1 ': ps) q + +-- | reversed dot +-- +-- >>>pl @(RDot '[Fst,Snd,Thd] Id) ((1,(2,9,10)),(3,4)) +-- Present 10 (Thd 10 | (2,9,10)) +-- PresentT 10 +-- +data RDot (ps :: [Type -> Type]) (q :: Type) +instance (P (RDotExpandT ps q) a) => P (RDot ps q) a where + type PP (RDot ps q) a = PP (RDotExpandT ps q) a + eval _ = eval (Proxy @(RDotExpandT ps q)) + +type family RDotExpandT (ps :: [Type -> Type]) (q :: Type) :: Type where + RDotExpandT '[] _ = GL.TypeError ('GL.Text "'[] invalid: requires at least one predicate in the list") + RDotExpandT '[p] q = p $ q + RDotExpandT (p ': p1 ': ps) q = RDotExpandT (p1 ': ps) (p $ q) + +-- | like 'GHC.Base.$' for expressions +-- +-- >>>pl @(Fst $ Snd $ Id) ((1,2),(3,4)) +-- Present 3 (Fst 3 | (3,4)) +-- PresentT 3 +-- +-- >>>pl @((<=) 4 $ Fst $ Snd $ Id) ((1,2),(3,4)) +-- False (4 <= 3) +-- FalseT +-- +data (p :: Type -> Type) $ (q :: Type) + +instance P (p q) a => P (p $ q) a where + type PP (p $ q) a = PP (p q) a + eval _ opts a = do + eval (Proxy @(p q)) opts a + +infixr 0 $ + +-- | creates a constant expression ignoring the second arguenent +-- +-- >>>pl @(RDot '[Fst,Snd,Thd,K "xxx"] Id) ((1,(2,9,10)),(3,4)) +-- Present "xxx" (K'xxx) +-- PresentT "xxx" +-- +-- >>>pl @(RDot '[Fst,Snd,Thd,K '("abc",Id)] Id) ((1,(2,9,10)),(3,4)) +-- Present ("abc",((1,(2,9,10)),(3,4))) (K'(,)) +-- PresentT ("abc",((1,(2,9,10)),(3,4))) +-- +data K (p :: k) (q :: Type) +instance P p a => P (K p q) a where + type PP (K p q) a = PP p a + eval _ = eval (Proxy @(Msg "K" p)) + +
src/Predicate/Refined.hs view
@@ -16,10 +16,9 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE DerivingVia #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE DeriveLift #-} +{-# LANGUAGE RoleAnnotations #-} {- | Simple refinement type with only one type and a predicate -} @@ -74,11 +73,12 @@ import qualified Text.Read.Lex as RL import qualified Data.Binary as B import Data.Binary (Binary) +import Data.Semigroup ((<>)) + -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- >>> :set -XOverloadedStrings -- >>> :m + Predicate.Prelude @@ -103,7 +103,7 @@ -- Left (FailP "bad length: found 3") -- -- >>> prtRefinedIO @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> GuardsN (PrintT "octet %d out of range %d" Id) 4 (Between 0 255) >> 'True) oz "141.213.1.444" --- Left (FailP "octet 4 out of range 444") +-- Left (FailP "octet 3 out of range 444") -- -- >>> prtRefinedIO @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> GuardsN (PrintT "octet %d out of range %d" Id) 4 (Between 0 255) >> 'True) oz "141.213.1x34.444" -- Left (FailP "ReadP Int (1x34) failed") @@ -130,6 +130,8 @@ -- Left FalseP newtype Refined p a = Refined { unRefined :: a } deriving (Show, Eq, Generic, TH.Lift) +type role Refined nominal nominal + -- | 'Read' instance for 'Refined' -- -- >>> reads @(Refined (Between 0 255) Int) "Refined {unRefined = 254}" @@ -138,6 +140,7 @@ -- >>> reads @(Refined (Between 0 255) Int) "Refined {unRefined = 300}" -- [] -- + instance (RefinedC p a, Read a) => Read (Refined p a) where readPrec = GR.parens @@ -145,11 +148,11 @@ 11 (do GR.expectP (RL.Ident "Refined") GR.expectP (RL.Punc "{") - fld0 <- GR.readField + fld0 <- readField "unRefined" (PCR.reset GR.readPrec) GR.expectP (RL.Punc "}") - let (_,mr) = runIdentity $ newRefined @p oz fld0 -- since we cant display the error message ... + let (_,mr) = runIdentity $ newRefined @p oz fld0 -- since we cant display the failure message ... case mr of Nothing -> fail "" Just _r -> pure (Refined fld0) @@ -371,7 +374,11 @@ newtype RefinedT m a = RefinedT { unRefinedT :: ExceptT String (WriterT [String] m) a } deriving (Functor, Applicative, Monad, MonadCont, MonadWriter [String], Show, MonadIO) - deriving MonadTrans via RefinedT + +instance MonadTrans RefinedT where + lift ma = RefinedT $ ExceptT $ WriterT $ do + a <- ma + return (Right a, []) instance Monad m => MonadError String (RefinedT m) where throwError e = RefinedT $ ExceptT $ WriterT $ return (Left e,[])
src/Predicate/Refined3.hs view
@@ -19,9 +19,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE DeriveLift #-} +{-# LANGUAGE RoleAnnotations #-} {- | Refinement type allowing the external type to differ from the internal type see 'Refined3' @@ -97,12 +96,12 @@ import Control.Lens ((^?),ix) import Data.Tree.Lens (root) import Data.Char (isSpace) +import Data.Semigroup ((<>)) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- >>> :set -XOverloadedStrings -- >>> :m + Predicate.Prelude @@ -161,6 +160,8 @@ -- 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) @@ -217,10 +218,10 @@ 11 (do GR.expectP (RL.Ident "Refined3") GR.expectP (RL.Punc "{") - fld1 <- GR.readField + fld1 <- readField "r3In" (PCR.reset GR.readPrec) GR.expectP (RL.Punc ",") - fld2 <- GR.readField + fld2 <- readField "r3Out" (PCR.reset GR.readPrec) GR.expectP (RL.Punc "}") @@ -229,7 +230,7 @@ Nothing -> fail "" Just (Refined3 _r1 r2) | r2 == fld2 -> pure (Refined3 fld1 fld2) - | otherwise -> fail "" -- cant display a decent error message + | otherwise -> fail "" -- cant display a decent failure message )) readList = GR.readListDefault readListPrec = GR.readListPrecDefault @@ -657,19 +658,19 @@ -> i -> m (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i)) eval3M opts i = do - ll@(fromTT -> t1) <- eval (Proxy @ip) opts i - case getValLR (_tBool ll) of - Right a -> do - rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a - case getValLR (_tBool rr) of - Right True -> do - ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a - pure $ case getValLR (_tBool ss) of - Right b -> (RTTrueT a t1 t2 b t3, Just (Refined3 a b)) - Left e -> (RTTrueF a t1 t2 e t3, Nothing) - Right False -> pure (RTFalse a t1 t2, Nothing) - Left e -> pure (RTF a t1 e t2, Nothing) - Left e -> pure (RF e t1, Nothing) + 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 (Refined3 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) -- | creates Refined3 value but skips the initial conversion eval3MSkip :: forall m ip op fmt i . (MonadEval m, Refined3C ip op fmt i) @@ -677,15 +678,15 @@ -> PP ip i -> m (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i)) eval3MSkip opts a = do - rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a - case getValLR (_tBool rr) of - Right True -> do - ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a - pure $ case getValLR (_tBool ss) of - Right b -> (RTTrueT a mkNodeSkipP t2 b t3, Just (Refined3 a b)) - Left e -> (RTTrueF a mkNodeSkipP t2 e t3, Nothing) - Right False -> pure (RTFalse a mkNodeSkipP t2, Nothing) - Left e -> pure (RTF a mkNodeSkipP e t2, Nothing) + 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 (Refined3 a b)) + (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 eval3MQuickIdentity :: forall ip op fmt i . Refined3C ip op fmt i @@ -700,10 +701,10 @@ eval3MQuick a = do let opts = oz rr <- evalBool (Proxy @op) opts a - case getValLR (_tBool rr) of + case getValLRFromTT rr of Right True -> do ss <- eval (Proxy @fmt) opts a - pure $ case getValLR (_tBool ss) of + pure $ case getValLRFromTT ss of Right b -> Just (Refined3 a b) _ -> Nothing _ -> pure Nothing @@ -788,19 +789,19 @@ -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i))) eval3PX _ opts i = runIdentity $ do - ll@(fromTT -> t1) <- eval (Proxy @ip) opts i - case getValLR (_tBool ll) of - Right a -> do - rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a - case getValLR (_tBool rr) of - Right True -> do - ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a - pure $ case getValLR (_tBool ss) of - Right b -> (RTTrueT a t1 t2 b t3, Just (unsafeRefined a, b)) - Left e -> (RTTrueF a t1 t2 e t3, Nothing) - Right False -> pure (RTFalse a t1 t2, Nothing) - Left e -> pure (RTF a t1 e t2, Nothing) - Left e -> pure (RF e t1, Nothing) + 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 'eval3PX' but allows you to set the parameters individually using type application eval3X :: forall ip op fmt i . Refined3C ip op fmt i
src/Predicate/Refined3Helper.hs view
@@ -14,8 +14,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE TypeApplications #-} {- | Contains prepackaged 4-tuples to use with 'Refined3' -} @@ -24,9 +22,6 @@ datetime1 , DateTime1 - , datetime1' - , DateTime1' - , daten , DateN , datetimen @@ -108,7 +103,6 @@ -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- | credit card with luhn algorithm -- @@ -146,40 +140,25 @@ -- | read in a valid datetime -- --- >>> prtEval3P (datetime1 @LocalTime) oz "2018-09-14 02:57:04" +-- >>> prtEval3P (datetime1 @LocalTime) ol "2018-09-14 02:57:04" -- Right (Refined3 {r3In = 2018-09-14 02:57:04, r3Out = "2018-09-14 02:57:04"}) -- --- >>> prtEval3P (datetime1' @LocalTime) oz "2018-09-14 99:98:97" --- Left Step 2. Failed Boolean Check(op) | invalid hours 99 --- --- >>> prtEval3P (datetime1 @LocalTime) ol "2018-09-14 99:98:97" --- Left Step 2. False Boolean Check(op) | {(>>) False | {GuardBool(0) [hours] (99 <= 23)}} --- --- >>> prtEval3P (datetime1' @LocalTime) oz "2018-09-14 23:01:97" --- Left Step 2. Failed Boolean Check(op) | invalid seconds 97 --- --- >>> prtEval3P (datetime1 @LocalTime) ol "2018-09-14 23:01:97" --- Left Step 2. False Boolean Check(op) | {(>>) False | {GuardBool(2) [seconds] (97 <= 59)}} --- --- >>> prtEval3P (Proxy @(DateTime1 UTCTime)) oz "2018-09-14 99:98:97" --- Right (Refined3 {r3In = 2018-09-18 04:39:37 UTC, r3Out = "2018-09-18 04:39:37"}) +-- >>> prtEval3P (datetime1 @LocalTime) ol "2018-09-99 12:12:12" +-- Left Step 1. Initial Conversion(ip) Failed | ParseTimeP LocalTime (%F %T) failed to parse -- datetime1 :: Proxy (DateTime1 t) datetime1 = mkProxy3 -type DateTime1 (t :: Type) = '(Dtip t, Dtop, Dtfmt, String) +type DateTime1 (t :: Type) = '(Dtip t, 'True, Dtfmt, String) type Dtip t = ParseTimeP t "%F %T" Id - -datetime1' :: Proxy (DateTime1' t) -datetime1' = mkProxy3 - -type DateTime1' (t :: Type) = '(Dtip t, Dtop', Dtfmt, String) +type Dtfmt = FormatTimeP "%F %T" Id +-- fixed in time-1.9 -- extra check to validate the time as parseTime doesnt validate the time component -- ZonedTime LocalTime and TimeOfDay don't do validation and allow invalid stuff through : eg 99:98:97 is valid -- UTCTime will do the same but any overages get tacked on to the day and time as necessary: makes the time valid! 99:98:97 becomes 04:39:37 -- 2018-09-14 99:00:96 becomes 2018-09-18 03:01:36 - +{- type Dtop' = Map (ReadP Int Id) (FormatTimeP "%H %M %S" Id >> Resplit "\\s+" Id) >> GuardsDetail "invalid %s %d" @@ -187,14 +166,13 @@ , '("minutes", Between 0 59) , '("seconds", Between 0 59) ] >> 'True -{- + type Dtop'' = Map (ReadP Int Id) (FormatTimeP "%H %M %S" Id >> Resplit "\\s+" Id) >> Guards '[ '(PrintT "guard %d invalid hours %d" Id, Between 0 23) , '(PrintT "guard %d invalid minutes %d" Id, Between 0 59) , '(PrintT "guard %d invalid seconds %d" Id, Between 0 59) ] >> 'True --} type Dtop = Map (ReadP Int Id) (FormatTimeP "%H %M %S" Id >> Resplit "\\s+" Id) @@ -202,8 +180,7 @@ , '("minutes",Between 0 59) , '("seconds",Between 0 59) ] - -type Dtfmt = FormatTimeP "%F %T" Id +-} ssn :: Proxy Ssn ssn = mkProxy3' @@ -214,10 +191,10 @@ -- Right (Refined3 {r3In = [134,1,2211], r3Out = "134-01-2211"}) -- -- >>> prtEval3P ssn ol "666-01-2211" --- Left Step 2. False Boolean Check(op) | {GuardBool(0) [number for group 0 invalid: found 666] (True && False | (666 /= 666))} +-- Left Step 2. False Boolean Check(op) | {Bools(0) [number for group 0 invalid: found 666] (True && False | (666 /= 666))} -- -- >>> prtEval3P ssn ol "667-00-2211" --- Left Step 2. False Boolean Check(op) | {GuardBool(1) [number for group 1 invalid: found 0] (1 <= 0)} +-- Left Step 2. False Boolean Check(op) | {Bools(1) [number for group 1 invalid: found 0] (1 <= 0)} -- type Ssn = '(Ssnip, Ssnop, Ssnfmt, String) @@ -240,10 +217,10 @@ -- Right (Refined3 {r3In = [23,13,59], r3Out = "23:13:59"}) -- -- >>> prtEval3P hms ol "23:13:60" --- Left Step 2. False Boolean Check(op) | {GuardBool(2) [seconds] (60 <= 59)} +-- Left Step 2. False Boolean Check(op) | {Bools(2) [seconds] (60 <= 59)} -- -- >>> prtEval3P hms ol "26:13:59" --- Left Step 2. False Boolean Check(op) | {GuardBool(0) [hours] (26 <= 23)} +-- Left Step 2. False Boolean Check(op) | {Bools(0) [hours] (26 <= 23)} -- hms :: Proxy Hms hms = mkProxy3' @@ -275,13 +252,13 @@ -- Right (Refined3 {r3In = [1,223,14,1], r3Out = "001.223.014.001"}) -- -- >>> prtEval3P ip ol "001.223.14.999" --- Left Step 2. False Boolean Check(op) | {GuardBool(3) [guard(3) octet out of range 0-255 found 999] (999 <= 255)} +-- Left Step 2. False Boolean Check(op) | {Bools(3) [guard(3) octet out of range 0-255 found 999] (999 <= 255)} -- -- >>> prtEval3P ip oz "001.223.14.999.1" -- Left Step 1. Initial Conversion(ip) Failed | Regex no results -- -- >>> prtEval3P ip ol "001.257.14.1" --- Left Step 2. False Boolean Check(op) | {GuardBool(1) [guard(1) octet out of range 0-255 found 257] (257 <= 255)} +-- Left Step 2. False Boolean Check(op) | {Bools(1) [guard(1) octet out of range 0-255 found 257] (257 <= 255)} -- type Ip = '(Ipip, Ipop, Ipfmt, String)
src/Predicate/TH_Orphans.hs view
@@ -7,7 +7,7 @@ {- | Mainly contains useful Template Haskell Lift instances for Date Time -} -module Predicate.TH_Orphans where +module Predicate.TH_Orphans () where import qualified Language.Haskell.TH.Syntax as TH import qualified Language.Haskell.TH.Lift as TL import Data.Time
src/Predicate/Util.hs view
@@ -2,7 +2,6 @@ {-# OPTIONS -Wcompat #-} {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} -{-# OPTIONS -Wredundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleContexts #-} @@ -60,8 +59,8 @@ , mkNodeSkipP -- ** tree manipulation + , getValAndPE , getValLRFromTT - , getValLR , fromTT , getValueLR , getValueLRHide @@ -150,7 +149,6 @@ , symb , GetNats(..) , GetSymbs(..) - , getLen , GetLen(..) , showThese , GetThese(..) @@ -163,7 +161,6 @@ , prtTTIO , prtTT , prtTree - , prtImpl , prtTreePure , prettyRational @@ -177,6 +174,8 @@ , prettyOrd , removeAnsi , MonadEval(..) + , errorInProgram + , readField ) where import qualified GHC.TypeNats as GN import Data.Ratio @@ -202,21 +201,23 @@ import Data.Sequence (Seq) import Control.Applicative (ZipList) import Data.Kind (Type) -import Data.These -import Data.These.Combinators +import Data.These (These(..)) import qualified Control.Exception as E import Control.DeepSeq import System.IO.Unsafe (unsafePerformIO) import Data.Bool -import Data.Foldable import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as N ---import Data.Maybe +import Data.Either +import Data.Semigroup ((<>)) +import qualified Text.Read.Lex as L +import Text.ParserCombinators.ReadPrec +import qualified GHC.Read as GR + -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- | represents the evaluation tree for predicates data TT a = TT { _tBool :: BoolT a -- ^ the value at this root node @@ -227,10 +228,10 @@ -- | contains the typed result from evaluating the expression tree -- data BoolT a where - FailT :: String -> BoolT a -- ^ failure with string - FalseT :: BoolT Bool -- ^ false predicate - TrueT :: BoolT Bool -- ^ true predicate - PresentT :: a -> BoolT a -- ^ non predicate value + FailT :: String -> BoolT a -- failure with string + FalseT :: BoolT Bool -- false predicate + TrueT :: BoolT Bool -- true predicate + PresentT :: a -> BoolT a -- non predicate value deriving instance Show a => Show (BoolT a) deriving instance Eq a => Eq (BoolT a) @@ -261,6 +262,7 @@ | PresentP -- ^ Any value deriving (Show, Eq) +-- | represents the untyped evaluation tree for final display data PE = PE { _pBool :: BoolP -- ^ holds the result of running the predicate , _pStrings :: [String] -- ^ optional strings to include in the results } deriving Show @@ -286,11 +288,8 @@ mkNodeSkipP :: Tree PE mkNodeSkipP = Node (PE TrueP ["skipped PP ip i = Id"]) [] -partitionTTExtended :: (w, TT a) -> ([((w, TT x), String)], [(w, TT a)]) -partitionTTExtended z@(_, t) = - case _tBool t of - FailT e -> ([(z & _2 . tBool .~ FailT e, e)], []) - _ -> ([], [z]) +getValAndPE :: TT a -> (Either String a, Tree PE) +getValAndPE tt = (getValLRFromTT tt, fromTT tt) getValLRFromTT :: TT a -> Either String a getValLRFromTT = getValLR . _tBool @@ -326,6 +325,7 @@ 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 @@ -617,26 +617,27 @@ POpts -> [String] -> [((Int, x), TT a)] - -> Either (TT w) - ([a] - ,[((Int, x), TT a)] - ) + -> Either (TT w) [(a, (Int, x), TT a)] splitAndAlign opts msgs ts = - case mconcat $ map partitionTTExtended ts of + case partitionEithers (map partitionTTExtended ts) of (excs@(e:_), _) -> Left $ mkNode opts (FailT (groupErrors (map snd excs))) (msgs <> ["excs=" <> show (length excs) <> " " <> formatList opts [fst e]]) (map (hh . snd) ts) - ([], tfs) -> Right (valsFromTTs (map snd ts), tfs) + ([], tfs) -> Right tfs +partitionTTExtended :: (w, TT a) -> Either ((w, TT x), String) (a, w, TT a) +partitionTTExtended (s, t) = + case _tBool t of + FailT e -> Left ((s, t & tBool .~ FailT e), e) + PresentT a -> Right (a,s,t) + TrueT -> Right (True,s,t) + FalseT -> Right (False,s,t) + formatList :: forall x z . Show x => POpts -> [((Int, x), z)] -> String formatList opts = unwords . map (\((i, a), _) -> "(i=" <> show i <> showAImpl opts OLite ", a=" a <> ")") --- | extract all root values from a list of trees -valsFromTTs :: [TT a] -> [a] -valsFromTTs = concatMap toList - instance Foldable TT where foldMap am = foldMap am . _tBool @@ -715,12 +716,12 @@ NullT ("" :: Symbol) = 'True NullT _ = 'False --- | helper method to fail with an error when True +-- | helper method to fail with a msg when True type family FailWhenT (b :: Bool) (msg :: GL.ErrorMessage) :: Constraint where FailWhenT 'False _ = () FailWhenT 'True e = GL.TypeError e --- | helper method to fail with an error when False +-- | helper method to fail with msg when False type family FailUnlessT (b :: Bool) (msg :: GL.ErrorMessage) :: Constraint where FailUnlessT 'True _ = () FailUnlessT 'False e = GL.TypeError e @@ -779,36 +780,74 @@ instance (KnownSymbol s, GetSymbs ss) => GetSymbs (s ': ss) where getSymbs = symb @s : getSymbs @ss --- | get the length of a typelevel list +-- | get the length of a typelevel container -- -- >>> getLen @'["abc","def","g"] -- 3 -- -getLen :: forall xs . GetLen xs => Int -getLen = getLenP (Proxy @xs) - --- really need a proxy for this to work --- | gets length of a typelevel list -class GetLen (xs :: [k]) where -- defaults to xs :: k (how to make it [k]) cos is not free - getLenP :: Proxy (xs :: [k]) -> Int +-- >>> getLen @'[] +-- 0 +-- +-- >>> getLen @(9 ':| '[1,2,3]) +-- 4 +-- +-- >>> getLen @('These 9 "Asfs") +-- 1 +-- +-- >>> getLen @('This 1) +-- 0 +-- +class GetLen xs where -- (xs :: [k]) will break it! ghc 8.6.5 + getLen :: Int instance GetLen '[] where - getLenP _ = 0 + getLen = 0 instance GetLen xs => GetLen (x ': xs) where - getLenP _ = 1 + getLenP (Proxy @xs) + getLen = 1 + getLen @xs +instance GetLen ('Just a) where + getLen = 1 +instance GetLen 'Nothing where + getLen = 0 +instance GetLen ('Left a) where + getLen = 0 +instance GetLen ('Right a) where + getLen = 1 +instance GetLen ('This a) where + getLen = 0 +instance GetLen ('That a) where + getLen = 1 +instance GetLen ('These a b) where + getLen = 1 +instance GetLen xs => GetLen (x ':| xs) where + getLen = 1 + getLen @xs + showThese :: These a b -> String -showThese = these (const "This") (const "That") (const (const "These")) +showThese = \case + This {} -> "This" + That {} -> "That" + These {} -> "These" --- hard without a Proxy -class GetThese (th :: These x y) where - getThese :: Proxy th -> (String, These w v -> Bool) +class GetThese th where + getThese :: (String, These w v -> Bool) instance GetThese ('This x) where - getThese _ = ("This", isThis) + getThese = ("This", isThis) instance GetThese ('That y) where - getThese _ = ("That", isThat) + getThese = ("That", isThat) instance GetThese ('These x y) where - getThese _ = ("These", isThese) + getThese = ("These", isThese) +isThis :: These a b -> Bool +isThis This {} = True +isThis _ = False + +isThat :: These a b -> Bool +isThat That {} = True +isThat _ = False + +isThese :: These a b -> Bool +isThese These {} = True +isThese _ = False + -- | get ordering from the typelevel class GetOrdering (cmp :: Ordering) where getOrdering :: Ordering @@ -827,21 +866,21 @@ instance GetBool 'False where getBool = False -data OrderingP = Cgt | Cge | Ceq | Cle | Clt | Cne deriving (Show, Eq, Enum, Bounded) +data OrderingP = CGt | CGe | CEq | CLe | CLt | CNe deriving (Show, Eq, Enum, Bounded) class GetOrd (k :: OrderingP) where getOrd :: Ord a => (String, a -> a -> Bool) -instance GetOrd 'Cgt where getOrd = (">", (>)) -instance GetOrd 'Cge where getOrd = (">=",(>=)) -instance GetOrd 'Ceq where getOrd = ("==",(==)) -instance GetOrd 'Cle where getOrd = ("<=",(<=)) -instance GetOrd 'Clt where getOrd = ("<", (<)) -instance GetOrd 'Cne where getOrd = ("/=",(/=)) +instance GetOrd 'CGt where getOrd = (">", (>)) +instance GetOrd 'CGe where getOrd = (">=",(>=)) +instance GetOrd 'CEq where getOrd = ("==",(==)) +instance GetOrd 'CLe where getOrd = ("<=",(<=)) +instance GetOrd 'CLt where getOrd = ("<", (<)) +instance GetOrd 'CNe where getOrd = ("/=",(/=)) toNodeString :: POpts -> PE -> String toNodeString opts bpe = - if hasNoTree opts then error $ "shouldnt be calling this if we are dropping details: toNodeString " <> show (oDebug opts) <> " " <> show bpe + if hasNoTree opts then errorInProgram $ "shouldnt be calling this if we are dropping details: toNodeString " <> show (oDebug opts) <> " " <> show bpe else showBoolP opts (_pBool bpe) <> " " <> displayMessages (_pStrings bpe) hasNoTree :: POpts -> Bool @@ -887,10 +926,7 @@ prtTT' o y = liftEval y >>= prtTree o . fromTT prtTree :: POpts -> Tree PE -> IO () -prtTree o = putStr . prtTreePure o -- prtImpl o . fmap (toNodeString o) - -prtImpl :: POpts -> Tree String -> IO () -prtImpl = (putStr .) . showImpl +prtTree o = putStr . prtTreePure o fixLite :: forall a . Show a => POpts -> a -> Tree PE -> String fixLite opts a t @@ -1035,54 +1071,54 @@ inductListC :: [a] -> InductListP n a instance (GL.TypeError ('GL.Text "InductListC: inductive tuple cannot be empty")) => InductListC 0 a where type InductListP 0 a = () - inductListC _ = error "InductListC 0: shouldnt be called" + inductListC _ = errorInProgram "InductListC 0: shouldnt be called" instance (GL.TypeError ('GL.Text "InductListC: inductive tuple cannot have one element")) => InductListC 1 a where type InductListP 1 a = a - inductListC _ = error "InductListC 1: shouldnt be called" + inductListC _ = errorInProgram "InductListC 1: shouldnt be called" instance InductListC 2 a where type InductListP 2 a = (a,(a,())) inductListC [a,b] = (b,(a,())) - inductListC _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 _ = error $ "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 @@ -1175,9 +1211,12 @@ catchitNF v = E.evaluate (Right $!! v) `E.catch` (\(E.SomeException e) -> pure $ Left ("IO e=" <> show e)) liftEval = id --- | strip ansi characters from a string +-- | strip ansi characters from a string and print it (for doctests) removeAnsi :: Show a => Either String a -> IO () -removeAnsi = +removeAnsi = putStrLn . removeAnsiImpl + +removeAnsiImpl :: Show a => Either String a -> String +removeAnsiImpl = \case Left e -> let esc = '\x1b' f :: String -> Maybe (String, String) @@ -1187,6 +1226,16 @@ (_,'m':s) -> Just ("",s) _ -> Nothing | otherwise -> Just $ break (==esc) (c:cs) - in putStrLn $ concat $ unfoldr f e - Right a -> print a + in concat $ unfoldr f e + Right a -> show a + +errorInProgram :: String -> x +errorInProgram s = error $ "programmer error:" <> s + +readField :: String -> ReadPrec a -> ReadPrec a +readField fieldName readVal = do + GR.expectP (L.Ident fieldName) + GR.expectP (L.Punc "=") + readVal +
src/Predicate/Util_TH.hs view
@@ -25,12 +25,12 @@ import Predicate.Util import qualified Language.Haskell.TH.Syntax as TH import Data.Functor.Identity +import Data.Semigroup ((<>)) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators --- >>> :set -XNoStarIsType -- | creates a 'Refined.Refined' refinement type with terse output -- @@ -53,7 +53,7 @@ -- @ -- refinedTH :: forall p i - . (Show i, TH.Lift i, RefinedC p i) + . (TH.Lift i, RefinedC p i) => i -> TH.Q (TH.TExp (Refined p i)) refinedTH = refinedTH' ol @@ -87,7 +87,7 @@ -- @ -- refinedTH' :: forall p i - . (Show i, TH.Lift i, RefinedC p i) + . (TH.Lift i, RefinedC p i) => POpts -> i -> TH.Q (TH.TExp (Refined p i))
test/TastyExtras.hs view
@@ -3,7 +3,6 @@ {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# OPTIONS -Wno-type-defaults #-} -{-# OPTIONS -Wno-redundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} @@ -13,7 +12,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE LambdaCase #-} module TastyExtras where import Test.Tasty @@ -22,6 +20,7 @@ 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
test/TestJson.hs view
@@ -12,7 +12,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE DeriveGeneric #-} module TestJson where import TastyExtras @@ -25,6 +24,7 @@ import GHC.Generics (Generic) import Data.Text (Text) import Data.Aeson +import qualified Data.ByteString as BS suite :: IO () suite = defaultMain $ testGroup "testrefined" @@ -36,12 +36,12 @@ ] testPerson :: IO (Either String [Person]) -testPerson = eitherDecodeFileStrict' "test1.json" +testPerson = BS.readFile "test1.json" >>= return . eitherDecodeStrict' testPerson1 :: Int -> IO (Either String [Person1]) testPerson1 i = do let fn = "test" ++ show i ++ ".json" - eitherDecodeFileStrict' fn + BS.readFile fn >>= return . eitherDecodeStrict' data Person = Person { firstName :: !Text
test/TestPredicate.hs view
@@ -3,7 +3,7 @@ {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# OPTIONS -Wno-type-defaults #-} -{-# OPTIONS -Wno-redundant-constraints #-} +-- {-# OPTIONS -Wno-redundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} @@ -14,8 +14,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NoStarIsType #-} module TestPredicate where +import Safe import TastyExtras import Test.Tasty import Test.Tasty.HUnit @@ -60,7 +60,7 @@ , expectPE TrueT $ pl @(Fst Id >> (Len <= 6)) ([2..7],True) , expectPE FalseT $ pl @(HeadDef 12 (Fst Id) >> Le 6) ([],True) , expectPE TrueT $ pl @(HeadDef 1 (Fst Id) >> Le 6) ([],True) - , expectPE (FailT "Head(empty)") $ pl @(Head (Fst Id) >> Le 6) ([] @Int, True) + , expectPE (FailT "Head(empty)") $ pl @(Head (Fst Id) >> Le 6) ([]::[Int], True) , expectPE FalseT $ pl @(HeadDef 10 (Fst Id) >> Le 6) ([],True) , expectPE (FailT "zz") $ pl @(HeadFail "zz" (Fst Id) >> Le 6) ([],True) , expectPE (FailT "failed1") $ pl @((HeadFail "failed1" (Fst Id) >> Le 6) || 'False) ([],True) @@ -110,9 +110,9 @@ , expectPE (PresentT (4,4)) $ pl @Dup 4 , expectPE (PresentT 3) $ pl @(Last Id) [1,2,3] , expectPE (PresentT 123) $ pl @(Just Id >> Id) (Just 123) - , expectPE (FailT "Asdf") $ pl @(HeadFail "Asdf" Id) ([] @()) -- breaks otherwise - , expectPE (FailT "Head(empty)") $ pl @(Head Id) ([] @Int) - , expectPE (FailT "Head(empty)") $ pl @(Head Id) ([] @Double) + , expectPE (FailT "Asdf") $ pl @(HeadFail "Asdf" Id) ([] :: [()]) -- breaks otherwise + , expectPE (FailT "Head(empty)") $ pl @(Head Id) ([] :: [Int]) + , expectPE (FailT "Head(empty)") $ pl @(Head Id) ([] :: [Double]) , expectPE (FailT "Succ bounded failed") $ pl @(SuccB' Id) GT , expectPE (PresentT LT) $ pl @(SuccB 'LT Id) GT , expectPE (PresentT EQ) $ pl @(SuccB 'GT Id) LT @@ -140,7 +140,7 @@ , expectPE FalseT $ pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head Id >> Gt (20 %- 1 )) [-23] , expectPE (PresentT (-1.0)) $ pl @(Negate Id >> Dup >> First (Succ Id) >> Swap >> Fst Id - Snd Id) 4 , expectPE (PresentT (Right 12)) $ pl @(Not Id +++ Id) (Right @Bool 12) - , expectPE (PresentT Cgt) $ pl @(FromEnum ("aa" ==! Id) >> ToEnum OrderingP Id) "aaaa" + , expectPE (PresentT CGt) $ pl @(FromEnum ("aa" ==! Id) >> ToEnum OrderingP Id) "aaaa" , expectPE (PresentT False) $ pl @(Msg "someval4" (Gt 4 >> Id)) 4 , expectPE (PresentT ()) $ pl @(Snd Id >> Snd Id >> Snd Id >> Snd Id >> Id) (1,('a',(3,(True,())))) , expectPE TrueT $ pl @(Re "\\d{4}-\\d{3}" Id) "1234-123" @@ -274,12 +274,12 @@ , expectPE (FailT "err") $ pl @(Guard "err" (Len > 2) >> Map (Succ Id) Id) [12] , expectPE (PresentT 12) $ pl @OneP [12] , expectPE (FailT "expected list of length 1 but found length=5") $ pl @OneP [1..5] - , expectPE (FailT "expected list of length 1 but found length=0") $ pl @OneP ([] @()) + , expectPE (FailT "expected list of length 1 but found length=0") $ pl @OneP ([] ::[()]) , expectPE (FailT "err(8)") $ pl @(Map (If (Lt 3) 'True (Failt _ "err")) Id) [1..10] , expectPE (FailT "someval(8)") $ pl @(Map (If (Lt 3) 'True (Failt _ "someval")) Id) [1..10] , expectPE (PresentT [True,True,False,False,False]) $ pl @(Map (If (Lt 3) 'True 'False) Id) [1..5] , expectPE (PresentT ["a","b","c"]) $ pl @(MaybeIn MEmptyP (Ones Id)) (Just @String "abc") - , expectPE (FailT "someval") $ pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) ([] @Int) + , expectPE (FailT "someval") $ pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) ([] :: [Int]) , expectPE (PresentT ([2,3],"[2,3]")) $ pl @(Guard "someval" (Len == 2) >> (Id &&& ShowP Id)) [2,3] , expectPE (FailT "someval") $ pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) [2,3,4] , expectPE (PresentT 55) $ pl @(Map (Wrap (SG.Sum _) Id) Id >> MConcat Id >> Unwrap Id) [1..10] @@ -401,23 +401,23 @@ , expectPE (PresentT [10,2,5]) $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 0 11, Between 1 4,Between 3 5]) [10::Int,2,5] , expectPE (PresentT [31,11,1999]) $ pl @(Rescan DdmmyyyyRE Id >> OneP >> Map (ReadBaseInt 10 Id) (Snd Id) >> Ddmmyyyyval) "31-11-1999" , expectPE (PresentT [31,11,1999]) $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,11,1999::Int] - , expectPE (FailT "Guards: data elements(2) /= predicates(3)") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,11::Int] - , expectPE (FailT "guard(2) 13 is out of range") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,13,1999::Int] - , expectPE (FailT "guard(1) 0 is out of range") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [0,44,1999::Int] + , expectPE (FailT "Guards: predicates(3) /= data elements(2)") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,11::Int] + , expectPE (FailT "guard(1) 13 is out of range") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,13,1999::Int] + , expectPE (FailT "guard(0) 0 is out of range") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [0,44,1999::Int] , expectPE (PresentT (fromGregorian 1999 11 30)) $ pl @(ReadP Day Id) "1999-11-30" , expectPE (FailT "ReadP Day (1999-02-29) failed") $ pl @(ReadP Day Id) "1999-02-29" , expectPE (PresentT (TimeOfDay 14 59 20)) $ pl @(ReadP TimeOfDay Id) "14:59:20" - , expectPE (PresentT (TimeOfDay 26 61 61)) $ pl @(ReadP TimeOfDay Id) "26:61:61" -- yep: this is valid! need to do your own validation +-- , expectPE (PresentT (TimeOfDay 26 61 61)) $ pl @(ReadP TimeOfDay Id) "26:61:61" -- yep: this is valid in <=time-1.8 ! need to do your own validation , expectPE (FailT "ParseTimeP TimeOfDay (%H:%M%S) failed to parse") $ pl @(ParseTimeP TimeOfDay "%H:%M%S" Id) "14:04:61" , expectPE (PresentT (TimeOfDay 23 13 59)) $ pl @(Guard "hh:mm:ss regex failed" (Re HmsRE Id) >> ReadP TimeOfDay Id) "23:13:59" , expectPE (FailT "hh:mm:ss regex failed") $ pl @(Guard "hh:mm:ss regex failed" (Re HmsRE Id) >> ReadP TimeOfDay Id) "23:13:60" - , expectPE (FailT "Guards: data elements(5) /= predicates(3)") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,11,2000,1,2::Int] + , expectPE (FailT "Guards: predicates(3) /= data elements(5)") $ pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31, Between 1 12, Between 1990 2050]) [31,11,2000,1,2::Int] , expectPE (PresentT [0,0,0,0,0,0,0,1,2,3]) $ pl @(PadL 10 0 Id) [1..3] , expectPE (PresentT (124,["1","2","2"])) $ pl @('Left Id >> (Succ Id &&& (Pred Id >> ShowP Id >> Ones Id))) (Left 123) , expectPE (PresentT [1,2,3,4]) $ pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255)) [1,2,3,4::Int] - , expectPE (FailT "Guards: data elements(5) /= predicates(4)") $ pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255)) [1,2,3,4,5::Int] - , expectPE (FailT "Guards: data elements(3) /= predicates(4)") $ pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255)) [1,2,3::Int] - , expectPE (PresentT (read "1999-01-01 12:12:12 Utc")) $ pl @(ParseTimeP UTCTime "%F %T" Id) "1999-01-01 12:12:12" + , expectPE (FailT "Guards: predicates(4) /= data elements(5)") $ pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255)) [1,2,3,4,5::Int] + , expectPE (FailT "Guards: predicates(4) /= data elements(3)") $ pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255)) [1,2,3::Int] + , expectPE (PresentT (readNote @UTCTime "failed to read utc" "1999-01-01 12:12:12 UTC")) $ pl @(ParseTimeP UTCTime "%F %T" Id) "1999-01-01 12:12:12" , expectPE (PresentT 123) $ pl @(JustDef 0 Id) (Just 123) , expectPE (PresentT 0) $ pl @(JustDef 0 Id) Nothing , expectPE (PresentT 12) $ pl @(LastDef 0 Id) [1..12] @@ -524,7 +524,7 @@ , expectPE (PresentT (Left 123)) $ pl @(Pure (Either String) Id >> Swap) 123 , expectPE (PresentT [13,2,1999]) $ pl @(Rescan DdmmyyyyRE Id >> OneP >> Map (ReadP Int Id) (Snd Id)) "13-02-1999" , expectPE (PresentT [3,2,1999]) $ pl @(Rescan DdmmyyyyRE Id >> OneP >> Map (ReadP Int Id) (Snd Id) >> Ddmmyyyyval) "03-02-1999" - , expectPE (FailT "guard(2) month 13 is out of range") $ pl @(Rescan DdmmyyyyRE Id >> OneP >> Map (ReadP Int Id) (Snd Id) >> Ddmmyyyyval) "12-13-1999" + , expectPE (FailT "guard(1) month 13 is out of range") $ pl @(Rescan DdmmyyyyRE Id >> OneP >> Map (ReadP Int Id) (Snd Id) >> Ddmmyyyyval) "12-13-1999" , expectPE (PresentT [[1],[2,3,4],[5,6,7,8],[9,10,11,12]]) $ pl @(SplitAts '[1,3,4] Id) [1..12] , expectPE (PresentT [[1,2,3],[4]]) $ pl @(SplitAts '[3,1,1,1] Id >> Filter (Not Null) Id) [1..4] , expectPE (PresentT 1) $ pl @(Msg (PrintF "digits=%d" Len) (Head Id)) [1..4] @@ -554,11 +554,11 @@ , expectPE (PresentT 23) $ pl @(Fst Id + Last (Snd Id)) (10,[12,13]) , expectPE (PresentT (-1,12)) $ pl @(DivMod (9 - Fst Id) (Last (Snd Id))) (10,[12,13]) , expectPE (PresentT [True,False,False,True]) $ pl @(Para '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99,-999] - , expectPE (FailT "Para: data elements(3) /= predicates(4)") $ pl @(Para '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99] - , expectPE (FailT "Para: data elements(7) /= predicates(4)") $ pl @(Para '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99,-999,1,1,2] - , expectPE (FailT "guard(2) err 002") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99,-999] - , expectPE (FailT "Guards: data elements(3) /= predicates(4)") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99] - , expectPE (FailT "Guards: data elements(7) /= predicates(4)") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'True, Lt 2 ]) [1,22,-99,-999,1,1,2] + , expectPE (FailT "Para: predicates(4) /= data elements(3)") $ pl @(Para '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99] + , expectPE (FailT "Para: predicates(4) /= data elements(7)") $ pl @(Para '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99,-999,1,1,2] + , expectPE (FailT "guard(1) err 002") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99,-999] + , expectPE (FailT "Guards: predicates(4) /= data elements(3)") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'False, Lt 2 ]) [1,2,-99] + , expectPE (FailT "Guards: predicates(4) /= data elements(7)") $ pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[ W 'True, Ge 12, W 'True, Lt 2 ]) [1,22,-99,-999,1,1,2] , expectPE TrueT $ pl @(Fst Id /= Snd Id) ("ab","xyzabw") , expectPE FalseT $ pl @(Fst Id == Snd Id) ("ab","xyzabw") , expectPE (PresentT 157) $ pl @(Fst Id * (Snd Id >> Fst Id) + (Snd Id >> Snd Id) `Div` 2) (12,(13,3)) @@ -611,13 +611,13 @@ , expectPE (FailT "PrintL(4) arg count=3") $ pl @(PrintL 4 "%03d.%03d.%03d.%03d" Id) [1,2,3::Int] , expectPE (PresentT "001.002.003.004") $ pl @(PrintL 4 "%03d.%03d.%03d.%03d" Id) [1,2,3,4::Int] - , expectPE (FailT "Pairs no data found") $ pl @Pairs ([] @()) + , expectPE (FailT "Pairs no data found") $ pl @Pairs ([] :: [()]) , expectPE (FailT "Pairs only one element found") $ pl @Pairs [1] , expectPE (PresentT [(1,2)]) $ pl @Pairs [1,2] , expectPE (PresentT [(1,2),(2,3)]) $ pl @Pairs [1,2,3] , expectPE (PresentT [(1,2),(2,3),(3,4)]) $ pl @Pairs [1,2,3,4] , expectPE (PresentT "1 2 3 004") $ pl @(PrintL 4 "%d %4d %-d %03d" Id) [1..4::Int] - , expectPE (PresentT "2019-08-17") $ pl @(FormatTimeP "%Y-%m-%d" Id) (read "2019-08-17" :: Day) + , expectPE (PresentT "2019-08-17") $ pl @(FormatTimeP "%Y-%m-%d" Id) (readNote @Day "invalid day" "2019-08-17") , expectPE (PresentT (20,20)) $ pl @(Dup << Fst Id * Snd Id) (4,5) , expectPE (PresentT (20,20)) $ pl @(Fst Id * Snd Id >> Dup) (4,5) , expectPE (PresentT (These "xxx" 4)) $ pl @(Fst Id <$ Snd Id) (4,These "xxx" 'a') @@ -630,10 +630,10 @@ , expectPE (PresentT "someval") $ pl @Extract ('x',"someval") , expectPE (PresentT (Just "cdef")) $ pl @(Fst Id <|> Snd Id) (Just "cdef",Just "ab") , expectPE (PresentT "cdefab") $ pl @(Fst Id <|> Snd Id) ("cdef","ab"::String) - , expectPE (PresentT (9,"abc")) $ pl @(I $ 9 $ "abc") (,) - , expectPE (PresentT ("abc",9)) $ pl @(9 & "abc" & I) (,) - , expectPE (PresentT "28") $ pl @(Fst Id $ Snd Id) (show . (7*),4) - , expectPE (PresentT (12,"12")) $ pl @(Fst Id $ Snd Id $ ShowP (Snd Id)) ((,),12) + , expectPE (PresentT (9,"abc")) $ pl @(I $$ 9 $$ "abc") (,) + , expectPE (PresentT ("abc",9)) $ pl @(9 $& "abc" $& I) (,) + , expectPE (PresentT "28") $ pl @(Fst Id $$ Snd Id) (show . (7*),4) + , expectPE (PresentT (12,"12")) $ pl @(Fst Id $$ Snd Id $$ ShowP (Snd Id)) ((,),12) -- , expectPE (PresentT (Just (This [1,2,3,4]))) $ pl @(ZipTheseF (Fst Id) (Snd Id)) (Just [1..4],Nothing @()) -- , expectPE (PresentT [These 1 'a',These 2 'b',These 3 'c',This 4]) $ pl @(ZipTheseF (Fst Id) (Snd Id)) ([1..4],['a'..'c']) , expectPE (PresentT [True,True,True,True]) $ pl @('True <$ Id) [1..4] @@ -710,9 +710,9 @@ ) (Fst Id)) '( 'True, Head Id) (Tail Id)) [1,4,7,6,16] , expectPE (PresentT [1,2,3,4]) $ pl @(Init Id) [1..5] - , expectPE (FailT "Init(empty)") $ pl @(Init Id) ([] @()) + , expectPE (FailT "Init(empty)") $ pl @(Init Id) ([] :: [()]) , expectPE (PresentT [2,3,4,5]) $ pl @(Tail Id) [1..5] - , expectPE (FailT "Tail(empty)") $ pl @(Tail Id) ([] @()) + , expectPE (FailT "Tail(empty)") $ pl @(Tail Id) ([] :: [()]) , expectPE (PresentT [10,12,13]) $ pl @(CatMaybes Id) [Just 10, Just 12, Nothing, Just 13] , expectPE (PresentT [5,4,3,2,1]) $ pl @(Foldl (Snd Id :+ Fst Id) (MEmptyT [_]) Id) [1..5] , expectPE (PresentT (map SG.Min [9,10,11,12,13])) $ pl @(EnumFromTo (Pure SG.Min 9) (Pure _ 13)) () @@ -732,15 +732,15 @@ , expectPE (PresentT [95,94,93]) $ pl @(IterateNUntil 3 (Id <= 90) (Pred Id)) 95 -- check for infinite loops , expectPE (FailT "Unfoldr (9999,1):failed at i=100") $ pl @(IterateNUntil 9999 'False I) 1 - , expectPE (FailT "Scanl:failed at i=100") $ pl @(Foldl (Fst Id) '() (EnumFromTo 1 9999)) () + , expectPE (FailT "Scanl list size exceeded") $ pl @(Foldl (Fst Id) '() (EnumFromTo 1 9999)) () , expectPE (PresentT "a=9 b=rhs") $ pl @(TheseX (PrintF "a=%d" (Succ (Snd Id))) ("b=" <> Snd Id) (PrintT "a=%d b=%s" (Snd Id)) Id) (These @Int 9 "rhs") , expectPE (PresentT "a=10") $ pl @(TheseX (PrintF "a=%d" (Succ (Snd Id))) ("b=" <> Snd Id) (PrintT "a=%d b=%s" (Snd Id)) Id) (This @Int 9) , expectPE (PresentT "b=rhs") $ pl @(TheseX (PrintF "a=%d" (Succ (Snd Id))) ("b=" <> Snd Id) (PrintT "a=%d b=%s" (Snd Id)) Id) (That @Int "rhs") - , expectPE (PresentT ([] @Int)) $ pl @(HeadDef (MEmptyT _) Id) (map (:[]) ([] @Int)) + , expectPE (PresentT ([] :: [Int])) $ pl @(HeadDef (MEmptyT _) Id) (map (:[]) ([] :: [Int])) , expectPE (PresentT ([10] :: [Int])) $ pl @(HeadDef (MEmptyT _) Id) (map (:[]) ([10..14] :: [Int])) , expectPE (PresentT 10) $ pl @(HeadDef (Fst Id) (Snd Id)) (99,[10..14]) - , expectPE (PresentT 99) $ pl @(HeadDef (Fst Id) (Snd Id)) (99,[] @Int) - , expectPE (PresentT 43) $ pl @(HeadDef 43 (Snd Id)) (99,[] @Int) + , expectPE (PresentT 99) $ pl @(HeadDef (Fst Id) (Snd Id)) (99,[] :: [Int]) + , expectPE (PresentT 43) $ pl @(HeadDef 43 (Snd Id)) (99,[] :: [Int]) , expectPE (PresentT (Just 'd')) $ pl @(Lookup "abcdef" 3) () , expectPE (PresentT (Just 5)) $ pl @(Lookup '[1,2,3,4,5,6] 4) () , expectPE (PresentT 5) $ pl @(LookupDef '[1,2,3,4,5,6] 4 Id) 23 @@ -811,7 +811,7 @@ , expectPE TrueT $ pl @(Between' (Fst Id >> Fst Id) (Fst Id >> Snd Id) (Snd Id)) ((1,4),3) , expectPE FalseT $ pl @(Between' (Fst Id >> Fst Id) (Fst Id >> Snd Id) (Snd Id)) ((1,4),10) , expectPE (FailT "no match on [03/29/0x7]") $ pl @(Map (ParseTimes Day '["%Y-%m-%d", "%m/%d/%y", "%b %d %Y"] Id) Id) ["2001-01-01", "Jan 24 2009", "03/29/0x7"] - , expectPE (PresentT [read @Day "2001-01-01", read @Day "2009-01-24", read @Day "2007-03-29"]) $ pl @(Map (ParseTimes Day '["%Y-%m-%d", "%m/%d/%y", "%b %d %Y"] Id) Id) ["2001-01-01", "Jan 24 2009", "03/29/07"] + , expectPE (PresentT [readNote @Day "invalid day" "2001-01-01", readNote @Day "invalid day" "2009-01-24", readNote @Day "invalid day" "2007-03-29"]) $ pl @(Map (ParseTimes Day '["%Y-%m-%d", "%m/%d/%y", "%b %d %Y"] Id) Id) ["2001-01-01", "Jan 24 2009", "03/29/07"] , expectPE (PresentT "gt3") $ pl @(Case (Snd Id >> Failp "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 15 , expectPE (PresentT "lt2") $ pl @(Case (Snd Id >> Failp "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 1
test/TestRefined.hs view
@@ -3,7 +3,7 @@ {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# OPTIONS -Wno-type-defaults #-} -{-# OPTIONS -Wno-redundant-constraints #-} +-- {-# OPTIONS -Wno-redundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} @@ -15,7 +15,6 @@ {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} @@ -35,6 +34,7 @@ import Control.Monad.Cont import Text.Show.Functions () import GHC.TypeNats (Nat) +import Data.Semigroup (Semigroup(..)) suite :: IO () suite = defaultMain $ testGroup "TestRefined" (namedTests <> orderTests unnamedTests <> allProps)
test/TestRefined3.hs view
@@ -3,7 +3,7 @@ {-# OPTIONS -Wincomplete-record-updates #-} {-# OPTIONS -Wincomplete-uni-patterns #-} {-# OPTIONS -Wno-type-defaults #-} -{-# OPTIONS -Wno-redundant-constraints #-} +-- {-# OPTIONS -Wno-redundant-constraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} @@ -15,7 +15,6 @@ {-# LANGUAGE NoOverloadedLists #-} -- overloaded lists breaks some predicates {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} @@ -24,6 +23,7 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck + import Predicate import TestRefined hiding (namedTests,unnamedTests,allProps) import Predicate.Refined @@ -41,9 +41,9 @@ import Control.Monad.Cont import Text.Show.Functions () import Data.Tree -import Test.QuickCheck ((===)) import qualified Data.Semigroup as SG import GHC.TypeLits (Nat) +import Data.Semigroup (Semigroup(..)) suite :: IO () suite = defaultMain $ testGroup "TestRefined3" (namedTests <> orderTests unnamedTests <> allProps) @@ -100,12 +100,12 @@ , expect3 (Left $ XTFalse (-6.3)) $ eval3 @(ReadP Double Id) - @(Cmp 'Cgt (ToRational Id) (7 %- 3)) + @(ToRational Id > 7 %- 3) @(PrintF "%5.3f" Id) ol "-6.3" , expect3 (Right $ unsafeRefined3 4.123 "") - $ eval3 @(ReadP Double Id) @(Cmp 'Cgt (ToRational Id) (7 %- 3)) @"" + $ eval3 @(ReadP Double Id) @(ToRational Id > 7 %- 3) @"" ol "4.123" , expect3 (Right $ unsafeRefined3 4.123 (4123 % 1000))