Predicate.Examples.Refined2

Contains prepackaged 4-tuples to use with Refined2

datetime

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

datetime1 :: Proxy (DateTime1 opts t)

read in a valid datetime

>>> newRefined2 @OL @(Dtip LocalTime) @'True "2018-09-14 02:57:04"
Right (Refined2 2018-09-14 02:57:04 "2018-09-14 02:57:04")

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

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

type DateN (opts :: Opt) = '(opts, ParseTimes Day DateFmts Id, 'True, String)

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

type DateTimeN (opts :: Opt) = '(opts, ParseTimes UTCTime DateTimeFmts Id, 'True, String)

type DateTimeNR (opts :: Opt) = MakeR2 (DateTimeN opts)

time

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

read in a time and validate it

>>> newRefined2 @OL @Hmsip @Hmsop' "23:13:59"
Right (Refined2 [23,13,59] "23:13:59")

>>> newRefined2 @OL @Hmsip @Hmsop' "23:13:60"
Left Step 2. Failed Boolean Check(op) | Bool(2) [seconds] (60 <= 59)

>>> newRefined2 @OL @Hmsip @Hmsop' "26:13:59"
Left Step 2. Failed Boolean Check(op) | Bool(0) [hours] (26 <= 23)

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

type HmsR (opts :: Opt) = MakeR2 (Hms opts)

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

type HmsR' (opts :: Opt) = MakeR2 (Hms' opts)

credit cards

type Luhn (opts :: Opt) (n :: Nat) = '(opts, Luhnip, Luhnop n, String)

credit card with luhn algorithm

>>> newRefined2 @OZ @Luhnip @(Luhnop 11) "1234-5678-901"
Left Step 2. Failed Boolean Check(op) | invalid checkdigit

>>> newRefined2 @OZ @Luhnip @(Luhnop 11) "1234-5678-903"
Right (Refined2 [1,2,3,4,5,6,7,8,9,0,3] "1234-5678-903")

>>> pz @(Luhnip >> Luhnop 11) "79927398713"
Val True

>>> pz @(Luhnip >> Luhnop 10) "79927398713"
Fail "expected 10 digits but found 11"

luhn11 :: Proxy (Luhn opts 11)

ssn

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

read in an ssn

>>> newRefined2 @OZ @Ssnip @Ssnop "134-01-2211"
Right (Refined2 [134,1,2211] "134-01-2211")

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

>>> newRefined2 @OL @Ssnip @Ssnop "667-00-2211"
Left Step 2. Failed Boolean Check(op) | Bool(1) [number for group 1 invalid: found 0] (1 <= 0)

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

type SsnR (opts :: Opt) = MakeR2 (Ssn opts)

ipv4

ip4 :: Proxy (Ip4 opts)

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

type Ip4R (opts :: Opt) = MakeR2 (Ip4 opts)

read in an ipv4 address and validate it

>>> newRefined2 @OZ @Ip4ip @Ip4op' "001.223.14.1"
Right (Refined2 [1,223,14,1] "001.223.14.1")

>>> newRefined2 @OL @Ip4ip @Ip4op' "001.223.14.999"
Left Step 2. Failed Boolean Check(op) | Bool(3) [octet 3 out of range 0-255 found 999] (999 <= 255)

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

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

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

ip4' :: Proxy (Ip4' opts)

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

type Ip4R' (opts :: Opt) = MakeR2 (Ip4' opts)

ipv6

ip6 :: Proxy (Ip6 opts)

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

type Ip6R (opts :: Opt) = MakeR2 (Ip6 opts)

isbn10

isbn10 :: Proxy (Isbn10 opts)

type Isbn10 (opts :: Opt) = '(opts, Isbn10ip, Isbn10op, String)

type Isbn10R (opts :: Opt) = MakeR2 (Isbn10 opts)

validate isbn10

>>> newRefined2P (isbn10 @OZ) "0-306-40611-X"
Right (Refined2 ([0,3,0,6,4,0,6,1,1],10) "0-306-40611-X")

>>> newRefined2P (isbn10 @OZ) "0-306-40611-9"
Left Step 2. Failed Boolean Check(op) | mod 0 oops

isbn13

isbn13 :: Proxy (Isbn13 opts)

type Isbn13 (opts :: Opt) = '(opts, Isbn13ip, Isbn13op, String)

type Isbn13R (opts :: Opt) = MakeR2 (Isbn13 opts)

validate isbn13

>>> newRefined2P (isbn13 @OZ) "978-0-306-40615-7"
Right (Refined2 [9,7,8,0,3,0,6,4,0,6,1,5,7] "978-0-306-40615-7")

>>> newRefined2P (isbn13 @OZ) "978-0-306-40615-8"
Left Step 2. Failed Boolean Check(op) | sum=101 mod 10=1

base n

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

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

>>> newRefined2 @OZ @(ReadBase Int 16) @'True "00fe"
Right (Refined2 254 "00fe")

>>> newRefined2 @OZ @(ReadBase Int 16) @(Between 100 400 Id) "00fe"
Right (Refined2 254 "00fe")

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

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

type BaseN' (opts :: Opt) (n :: Nat) p = '(opts, ReadBase Int n, p, String)

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

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

type BaseIJip (i :: Nat) (j :: Nat) = ReadBase Int i >> ShowBase j

Luhn check

>>> newRefined2 @OZ @Luhnip @(Luhnop 4) "1230"
Right (Refined2 [1,2,3,0] "1230")

>>> newRefined2 @OL @Luhnip @(Luhnop 4) "1234"
Left Step 2. Failed Boolean Check(op) | invalid checkdigit

| uses builtin IsLuhn

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

>>> newRefined2 @OZ @(BaseIJip 16 2) @'True "fe"
Right (Refined2 "11111110" "fe")

>>> newRefined2 @OZ @(BaseIJip 16 2) @'True "fge"
Left Step 1. Failed Initial Conversion(ip) | invalid base 16

>>> newRefined2 @OL @(BaseIJip 16 2) @(ReadBase Int 2 < 1000) "ffe"
Left Step 2. False Boolean Check(op) | {4094 < 1000}