Predicate.Refined3Helper

Contains prepackaged 4-tuples to use with Refined3

date time checkers

datetime1 :: Proxy (DateTime1 t)

read in a valid datetime

>>> prtEval3P (datetime1 @LocalTime) oz "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"})

type DateTime1 (t :: Type) = '(Dtip t, Dtop, Dtfmt, String)

datetime1' :: Proxy (DateTime1' t)

type DateTime1' (t :: Type) = '(Dtip t, Dtop', Dtfmt, String)

daten :: Proxy DateN

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

datetimen :: Proxy DateTimeN

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

type DateTimeNR = MakeR3 DateTimeN

type DateFmts = '["%Y-%m-%d", "%m/%d/%y", "%B %d %Y"]

type DateTimeFmts = '["%Y-%m-%d %H:%M:%S", "%m/%d/%y %H:%M:%S", "%B %d %Y %H:%M:%S", "%Y-%m-%dT%H:%M:%S"]

time checkers

hms :: Proxy Hms

read in a time and validate it

>>> prtEval3P hms ol "23:13:59"
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)}

>>> prtEval3P hms ol "26:13:59"
Left Step 2. False Boolean Check(op) | {GuardBool(0) [hours] (26 <= 23)}

type Hms = '(Hmsip, Hmsop, Hmsfmt, String)

type Hmsip = Map (ReadP Int Id) (Resplit ":" Id)

type Hmsop = Bools '['("hours", Between 0 23), '("minutes", Between 0 59), '("seconds", Between 0 59)]

type Hmsfmt = PrintL 3 "%02d:%02d:%02d" Id

type HmsRE = "^([0-1][0-9]|2[0-3]):([0-5][0-9]):([0-5][0-9])$"

credit cards

ccn :: Proxy (Ccn ns)

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

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

cc11 :: Proxy (Ccn '[4, 4, 3])

type CC11 = Ccn '[4, 4, 3]

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

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

Luhn check

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

>>> prtEval3P (Proxy @(LuhnT 4)) ol "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 :: Proxy Ssn

type Ssn = '(Ssnip, Ssnop, Ssnfmt, String)

read in an ssn

>>> prtEval3P ssn oz "134-01-2211"
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))}

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

ipv4

ip :: Proxy Ip

type Ip = '(Ipip, Ipop, Ipfmt, String)

read in an ipv4 address and validate it

>>> prtEval3P ip oz "001.223.14.1"
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)}

>>> 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)}

type OctetRE = "(25[0-5]|2[0..4][0-9]|1[0-9][0-9]|[1-9][0-9]|[0-9])"

type Ip4StrictRE = ("^" `AppendSymbol` IntersperseT "\\." (RepeatT 4 OctetRE)) `AppendSymbol` "$"

base n

basen :: Proxy (BaseN n)

base2 :: Proxy (BaseN 2)

base16 :: Proxy (BaseN 16)

basen' :: Proxy (BaseN' n p)

base2' :: Proxy (BaseN' 2 p)

base16' :: Proxy (BaseN' 16 p)

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

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

>>> prtEval3P base16 oz "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})

>>> prtEval3P (basen' @16 @(Between 100 400)) oz "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})

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

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

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

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

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

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

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

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

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

read / show

readshow :: Proxy (ReadShow t)

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

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

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

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

>>> prtEval3P (readshow' @Rational @(Between (3 % 1) (5 % 1))) oz "13 % 3"
Right (Refined3 {r3In = 13 % 3, r3Out = "13 % 3"})

>>> prtEval3P (Proxy @(ReadShow' Rational (Between (11 %- 2) (3 %- 1)))) oz "-13 % 3"
Right (Refined3 {r3In = (-13) % 3, r3Out = "(-13) % 3"})

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

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

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

>>> let tmString = "2018-10-19 14:53:11.5121359 UTC"
>>> let tm = read tmString :: UTCTime
>>> prtEval3P (readshow @UTCTime) oz tmString
Right (Refined3 {r3In = 2018-10-19 14:53:11.5121359 UTC, r3Out = "2018-10-19 14:53:11.5121359 UTC"})

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

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

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

readshow' :: Proxy (ReadShow' t p)

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

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

between

between :: Proxy (BetweenN m n)

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

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

>>> prtEval3P (between @10 @16) oz 17
Left Step 2. False Boolean Check(op) | FalseP

>>> prtEval3P (between @10 @16) o0 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 m n = RefinedEmulate (Between m n) Int

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

miscellaneous

ok :: Proxy (Ok t)

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

noop true

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

oknot :: Proxy (OkNot t)

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

noop false

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