Predicate.Examples.Refined2

Contains examples to use with Predicate.Refined2

date time checkers

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

read in a valid datetime

>>> prtEval2 @(Dtip LocalTime) @'True ol "2018-09-14 02:57:04"
Right (Refined2 {r2In = 2018-09-14 02:57:04, r2Out = "2018-09-14 02:57:04"})

>>> prtEval2 @(Dtip LocalTime) @'True 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)

daten :: Proxy DateN

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

datetimen :: Proxy DateTimeN

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

type DateTimeNR = MakeR2 DateTimeN

time checkers

hms :: Proxy Hms

read in a time and validate it

>>> prtEval2 @Hmsip @Hmsop' ol "23:13:59"
Right (Refined2 {r2In = [23,13,59], r2Out = "23:13:59"})

>>> prtEval2 @Hmsip @Hmsop' ol "23:13:60"
Left Step 2. False Boolean Check(op) | {Bools(2) [seconds] (60 <= 59)}

>>> prtEval2 @Hmsip @Hmsop' ol "26:13:59"
Left Step 2. False Boolean Check(op) | {Bools(0) [hours] (26 <= 23)}

type Hms = '(Hmsip, Hmsop >> True, String)

type HmsR = MakeR2 Hms

credit cards

type Ccn (n :: Nat) = '(Ccip, Ccop n, String)

credit card with luhn algorithm

>>> prtEval2 @Ccip @(Ccop 11) oz "1234-5678-901"
Left Step 2. False Boolean Check(op) | FalseP

>>> prtEval2 @Ccip @(Ccop 11) oz "1234-5678-903"
Right (Refined2 {r2In = [1,2,3,4,5,6,7,8,9,0,3], r2Out = "1234-5678-903"})

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

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

cc11 :: Proxy (Ccn 11)

ssn

ssn :: Proxy Ssn

read in an ssn

>>> prtEval2 @Ssnip @Ssnop oz "134-01-2211"
Right (Refined2 {r2In = [134,1,2211], r2Out = "134-01-2211"})

>>> prtEval2 @Ssnip @Ssnop ol "666-01-2211"
Left Step 2. False Boolean Check(op) | {Bools(0) [number for group 0 invalid: found 666] (True && False | (666 /= 666))}

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

type Ssn = '(Ssnip, Ssnop, String)

type SsnR = MakeR2 Ssn

ipv4

ip4 :: Proxy Ip4

type Ip4 = '(Ip4ip, Ip4op >> True, String)

type Ip4R = MakeR2 Ip4

read in an ipv4 address and validate it

>>> prtEval2 @Ip4ip @Ip4op' oz "001.223.14.1"
Right (Refined2 {r2In = [1,223,14,1], r2Out = "001.223.14.1"})

>>> prtEval2 @Ip4ip @Ip4op' ol "001.223.14.999"
Left Step 2. False Boolean Check(op) | {Bools(3) [octet 3 out of range 0-255 found 999] (999 <= 255)}

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

>>> prtEval2P ip4 ol "001.223.14.999.1"
Left Step 2. Failed Boolean Check(op) | Guards: invalid length:expected 4 but found 5

>>> prtEval2P 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'

type Ip4' = '(Ip4ip, Ip4op', String)

type Ip4R' = MakeR2 Ip4

ipv6

ip6 :: Proxy Ip6

type Ip6 = '(Ip6ip, Ip6op, String)

type Ip6R = MakeR2 Ip6

base n

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

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

>>> prtEval2 @(ReadBaseInt 16 Id) @'True oz "00fe"
Right (Refined2 {r2In = 254, r2Out = "00fe"})

>>> prtEval2 @(ReadBaseInt 16 Id) @(Between 100 400) oz "00fe"
Right (Refined2 {r2In = 254, r2Out = "00fe"})

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

>>> prtEval2 @(ReadBaseInt 16 Id) @(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, String)

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

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

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

Luhn check

>>> prtEval2 @Luhnip @(Luhnop 4) oz "1230"
Right (Refined2 {r2In = [1,2,3,0], r2Out = "1230"})

>>> prtEval2 @Luhnip @(Luhnop 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

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

>>> prtEval2 @(BaseIJip 16 2) @'True oz "fe"
Right (Refined2 {r2In = "11111110", r2Out = "fe"})

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

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