Predicate.Examples.Refined3

Contains prepackaged 5-tuples and proxies to use with Refined3

date time checkers

datetime1 :: Proxy (DateTime1 opts t)

read in a valid datetime

>>> newRefined3P (datetime1 @OL @LocalTime) "2018-09-14 02:57:04"
Right (Refined3 {r3In = 2018-09-14 02:57:04, r3Out = "2018-09-14 02:57:04"})

>>> newRefined3P (datetime1 @OL @LocalTime) "2018-09-99 12:12:12"
Left "Step 1. Initial Conversion(ip) Failed | ParseTimeP LocalTime (%F %T) failed to parse"

type DateTime1 (opts :: OptT) (t :: Type) = '(opts, Dtip t, True, Dtfmt, String)

daten :: OptTC opts => Proxy (DateN opts)

type DateN (opts :: OptT) = '(opts, ParseTimes Day DateFmts Id, True, FormatTimeP "%Y-%m-%d" Id, String)

datetimen :: OptTC opts => Proxy (DateTimeN opts)

type DateTimeN (opts :: OptT) = '(opts, ParseTimes UTCTime DateTimeFmts Id, True, FormatTimeP "%Y-%m-%d %H:%M:%S" Id, String)

type DateTimeNR (opts :: OptT) = MakeR3 (DateTimeN opts)

time checkers

hms :: OptTC opts => Proxy (Hms opts)

read in a time and validate it

>>> newRefined3P (hms @OL) "23:13:59"
Right (Refined3 {r3In = [23,13,59], r3Out = "23:13:59"})

>>> newRefined3P (hms @OL) "23:13:60"
Left "Step 2. Failed Boolean Check(op) | seconds invalid: found 60"

>>> newRefined3P (hms @OL) "26:13:59"
Left "Step 2. Failed Boolean Check(op) | hours invalid: found 26"

type Hms (opts :: OptT) = '(opts, Hmsip, Hmsop >> True, Hmsfmt, String)

type HmsR (opts :: OptT) = MakeR3 (Hms opts)

type Hms' (opts :: OptT) = '(opts, Hmsip, Hmsop', Hmsfmt, String)

type HmsR' (opts :: OptT) = MakeR3 (Hms' opts)

credit cards

ccn :: Proxy (Ccn opts ns)

ccn' :: (OptTC opts, PP ns String ~ [Integer], KnownNat (SumT ns), P ns String) => Proxy (Ccn opts ns)

type Ccn (opts :: OptT) (ns :: [Nat]) = '(opts, Ccip, Ccop (SumT ns), Ccfmt ns, String)

credit card with luhn algorithm

>>> newRefined3P (cc11 @OZ) "1234-5678-901"
Left "Step 2. False Boolean Check(op) | FalseP"

>>> newRefined3P (cc11 @OZ) "1234-5678-903"
Right (Refined3 {r3In = [1,2,3,4,5,6,7,8,9,0,3], r3Out = "1234-5678-903"})

>>> pz @(Ccip >> Ccop 11) "79927398713"
TrueT

>>> pz @(Ccip >> Ccop 10) "79927398713"
FailT "expected 10 digits but found 11"

cc11 :: OptTC opts => Proxy (Ccn opts '[4, 4, 3])

type Cc11 (opts :: OptT) = Ccn opts '[4, 4, 3]

type LuhnR (opts :: OptT) (n :: Nat) = MakeR3 (LuhnT opts n)

type LuhnT (opts :: OptT) (n :: Nat) = '(opts, Map (ReadP Int Id) (Ones Id), Msg "incorrect number of digits:" (Len == n) && Luhn Id, ConcatMap (ShowP Id) Id, String)

Luhn check

>>> newRefined3P (Proxy @(LuhnT OZ 4)) "1230"
Right (Refined3 {r3In = [1,2,3,0], r3Out = "1230"})

>>> newRefined3P (Proxy @(LuhnT OL 4)) "1234"
Left "Step 2. False Boolean Check(op) | {True && False | (Luhn map=[4,6,2,2] sum=14 ret=4 | [1,2,3,4])}"

| uses builtin Luhn

ssn

ssn :: OptTC opts => Proxy (Ssn opts)

type Ssn (opts :: OptT) = '(opts, Ssnip, Ssnop, Ssnfmt, String)

read in an ssn

>>> newRefined3P (ssn @OZ) "134-01-2211"
Right (Refined3 {r3In = [134,1,2211], r3Out = "134-01-2211"})

>>> newRefined3P (ssn @OL) "666-01-2211"
Left "Step 2. False Boolean Check(op) | {Bool(0) [number for group 0 invalid: found 666] (True && False | (666 /= 666))}"

>>> newRefined3P (ssn @OL) "667-00-2211"
Left "Step 2. False Boolean Check(op) | {Bool(1) [number for group 1 invalid: found 0] (1 <= 0)}"

type SsnR (opts :: OptT) = MakeR3 (Ssn opts)

ipv4

ip4 :: OptTC opts => Proxy (Ip4 opts)

type Ip4 (opts :: OptT) = '(opts, Ip4ip, Ip4op >> True, Ip4fmt, String)

type Ip4R (opts :: OptT) = MakeR3 (Ip4 opts)

read in an ipv4 address and validate it

>>> newRefined3P (ip4 @OZ) "001.223.14.1"
Right (Refined3 {r3In = [1,223,14,1], r3Out = "001.223.014.001"})

>>> newRefined3P (ip4 @OL) "001.223.14.999"
Left "Step 2. Failed Boolean Check(op) | octet 3 out of range 0-255 found 999"

>>> newRefined3P (ip4 @OZ) "001.223.14.999.1"
Left "Step 2. Failed Boolean Check(op) | Guards:invalid length(5) expected 4"

>>> newRefined3P (ip4 @OL) "001.257.14.1"
Left "Step 2. Failed Boolean Check(op) | octet 1 out of range 0-255 found 257"

ip4' :: OptTC opts => Proxy (Ip4' opts)

type Ip4' (opts :: OptT) = '(opts, Ip4ip, Ip4op', Ip4fmt, String)

type Ip4R' (opts :: OptT) = MakeR3 (Ip4' opts)

ipv6

ip6 :: Proxy (Ip6 opts)

type Ip6 (opts :: OptT) = '(opts, Ip6ip, Ip6op, Ip6fmt, String)

type Ip6R (opts :: OptT) = MakeR3 (Ip6 opts)

base n

basen :: Proxy (BaseN opts n)

base2 :: Proxy (BaseN opts 2)

base16 :: Proxy (BaseN opts 16)

basen' :: Proxy (BaseN' opts n p)

base2' :: Proxy (BaseN' opts 2 p)

base16' :: Proxy (BaseN' opts 16 p)

type BaseN (opts :: OptT) (n :: Nat) = BaseN' opts n True

convert a string from a given base 'i' and store it internally as an base 10 integer

>>> newRefined3P (base16 @OZ) "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})

>>> newRefined3P (basen' @OZ @16 @(100 <..> 400)) "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})

>>> newRefined3P (basen' @OZ @16 @(GuardSimple (Id < 400) >> 'True)) "f0fe"
Left "Step 2. Failed Boolean Check(op) | (61694 < 400)"

>>> newRefined3P (basen' @OL @16 @(Id < 400)) "f0fe" -- todo: why different parens vs braces
Left "Step 2. False Boolean Check(op) | {61694 < 400}"

type BaseN' (opts :: OptT) (n :: Nat) p = '(opts, ReadBase Int n Id, p, ShowBase n Id, String)

type BaseIJ (opts :: OptT) (i :: Nat) (j :: Nat) = BaseIJ' opts i j True

convert a string from a given base 'i' and store it internally as a base 'j' string

>>> newRefined3P (Proxy @(BaseIJ OZ 16 2)) "fe"
Right (Refined3 {r3In = "11111110", r3Out = "fe"})

>>> newRefined3P (Proxy @(BaseIJ OZ 16 2)) "fge"
Left "Step 1. Initial Conversion(ip) Failed | invalid base 16"

>>> newRefined3P (Proxy @(BaseIJ' OL 16 2 (ReadBase Int 2 Id < 1000))) "ffe"
Left "Step 2. False Boolean Check(op) | {4094 < 1000}"

type BaseIJ' (opts :: OptT) (i :: Nat) (j :: Nat) p = '(opts, ReadBase Int i Id >> ShowBase j Id, p, ReadBase Int j Id >> ShowBase i Id, String)

read / show

readshow :: Proxy (ReadShow opts t)

type ReadShow (opts :: OptT) (t :: Type) = '(opts, ReadP t Id, True, ShowP Id, String)

take any valid Read/Show instance and turn it into a valid Refined3

>>> :m + Data.Ratio
>>> newRefined3P (readshow @OZ @Rational) "13 % 3"
Right (Refined3 {r3In = 13 % 3, r3Out = "13 % 3"})

>>> newRefined3P (readshow @OZ @Rational) "13x % 3"
Left "Step 1. Initial Conversion(ip) Failed | ReadP Ratio Integer (13x % 3)"

>>> newRefined3P (readshow' @OZ @Rational @(3 % 1 <..> 5 % 1)) "13 % 3"
Right (Refined3 {r3In = 13 % 3, r3Out = "13 % 3"})

>>> newRefined3P (Proxy @(ReadShow' OZ Rational (11 -% 2 <..> 3 -% 1))) "-13 % 3"
Right (Refined3 {r3In = (-13) % 3, r3Out = "(-13) % 3"})

>>> newRefined3P (Proxy @(ReadShow' OZ Rational (Id > (15 % 1)))) "13 % 3"
Left "Step 2. False Boolean Check(op) | FalseP"

>>> newRefined3P (Proxy @(ReadShow' OL Rational (Msg (PrintF "invalid=%3.2f" (FromRational Double Id)) (Id > (15 % 1))))) "13 % 3"
Left "Step 2. False Boolean Check(op) | {invalid=4.3313 % 3 > 15 % 1}"

>>> newRefined3P (Proxy @(ReadShow' OZ Rational (Id > (11 % 1)))) "13 % 3"
Left "Step 2. False Boolean Check(op) | FalseP"

>>> newRefined3P (readshow @OZ @UTCTime) "2018-10-19 14:53:11.5121359 UTC"
Right (Refined3 {r3In = 2018-10-19 14:53:11.5121359 UTC, r3Out = "2018-10-19 14:53:11.5121359 UTC"})

>>> :m + Data.Aeson
>>> newRefined3P (readshow @OZ @Value) "String \"jsonstring\""
Right (Refined3 {r3In = String "jsonstring", r3Out = "String \"jsonstring\""})

>>> newRefined3P (readshow @OZ @Value) "Number 123.4"
Right (Refined3 {r3In = Number 123.4, r3Out = "Number 123.4"})

type ReadShowR (opts :: OptT) (t :: Type) = MakeR3 (ReadShow opts t)

readshow' :: Proxy (ReadShow' opts t p)

type ReadShow' (opts :: OptT) (t :: Type) p = '(opts, ReadP t Id, p, ShowP Id, String)

type ReadShowR' (opts :: OptT) (t :: Type) p = MakeR3 (ReadShow' opts t p)

between

between :: Proxy (BetweenN opts m n)

ensures that two numbers are in a given range (emulates Refined)

>>> newRefined3P (between @OZ @10 @16) 14
Right (Refined3 {r3In = 14, r3Out = 14})

>>> newRefined3P (between @OZ @10 @16) 17
Left "Step 2. False Boolean Check(op) | FalseP"

>>> prtEval3P (between @OAN @10 @16) 17
Left Step 2. False Boolean Check(op) | {17 <= 16}

*** Step 1. Success Initial Conversion(ip) (17) ***

P Id 17

*** Step 2. False Boolean Check(op) ***

False 17 <= 16
|
+- P Id 17
|
+- P '10
|
`- P '16

type BetweenR (opts :: OptT) m n = RefinedEmulate opts (Between m n Id) Int

type BetweenN (opts :: OptT) m n = '(opts, Id, Between m n Id, Id, Int)

miscellaneous

ok :: Proxy (Ok opts t)

type Ok (opts :: OptT) (t :: Type) = '(opts, Id, True, Id, t)

noop true

type OkR (opts :: OptT) (t :: Type) = MakeR3 (Ok opts t)

oknot :: Proxy (OkNot t)

type OkNot (t :: Type) = '(OA, Id, False, Id, t)

noop false

type OkNotR (t :: Type) = MakeR3 (OkNot t)