Safe Haskell	None
Language	Haskell2010

Predicate.Examples.Refined3

Contents

datetime
time
credit cards
ssn
ipv4
ipv6
isbn10
isbn13
base n
read / show
between
miscellaneous

Description

Contains prepackaged 5-tuples and proxies to use with Refined3

Synopsis

datetime1 :: Proxy (DateTime1 opts t)
type DateTime1 (opts :: Opt) (t :: Type) = '(opts, Dtip t, True, Dtfmt, String)
daten :: OptC opts => Proxy (DateN opts)
type DateN (opts :: Opt) = '(opts, ParseTimes Day DateFmts Id, True, FormatTimeP "%Y-%m-%d", String)
datetimen :: OptC opts => Proxy (DateTimeN opts)
type DateTimeN (opts :: Opt) = '(opts, ParseTimes UTCTime DateTimeFmts Id, True, FormatTimeP "%Y-%m-%d %H:%M:%S", String)
type DateTimeNR (opts :: Opt) = MakeR3 (DateTimeN opts)
hms :: OptC opts => Proxy (Hms opts)
type Hms (opts :: Opt) = '(opts, Hmsip, Hmsop, Hmsfmt, String)
type HmsR (opts :: Opt) = MakeR3 (Hms opts)
type Hms' (opts :: Opt) = '(opts, Hmsip, Hmsop', Hmsfmt, String)
type HmsR' (opts :: Opt) = MakeR3 (Hms' opts)
luhn :: Proxy (Luhn opts ns)
luhn' :: (OptC opts, PP ns String ~ [Integer], KnownNat (SumT ns), P ns String) => Proxy (Luhn opts ns)
type Luhn (opts :: Opt) (ns :: [Nat]) = '(opts, Luhnip, Luhnop (SumT ns), Luhnfmt ns, String)
luhn11 :: OptC opts => Proxy (Luhn opts '[4, 4, 3])
type Luhn11 (opts :: Opt) = Luhn opts '[4, 4, 3]
type LuhnR (opts :: Opt) (n :: Nat) = MakeR3 (LuhnT opts n)
type LuhnT (opts :: Opt) (n :: Nat) = '(opts, Map' (ReadP Int Id) Ones, Msg "incorrect number of digits:" (Len == n) && IsLuhn, ConcatMap (ShowP Id) Id, String)
ssn :: OptC opts => Proxy (Ssn opts)
type Ssn (opts :: Opt) = '(opts, Ssnip, Ssnop, Ssnfmt, String)
type SsnR (opts :: Opt) = MakeR3 (Ssn opts)
ip4 :: OptC opts => Proxy (Ip4 opts)
type Ip4 (opts :: Opt) = '(opts, Ip4ip, Ip4op, Ip4fmt, String)
type Ip4R (opts :: Opt) = MakeR3 (Ip4 opts)
ip4' :: OptC opts => Proxy (Ip4' opts)
type Ip4' (opts :: Opt) = '(opts, Ip4ip, Ip4op', Ip4fmt, String)
type Ip4R' (opts :: Opt) = MakeR3 (Ip4' opts)
ip6 :: Proxy (Ip6 opts)
type Ip6 (opts :: Opt) = '(opts, Ip6ip, Ip6op, Ip6fmt, String)
type Ip6R (opts :: Opt) = MakeR3 (Ip6 opts)
isbn10 :: Proxy (Isbn10 opts)
type Isbn10 (opts :: Opt) = '(opts, Isbn10ip, Isbn10op, Isbn10fmt, String)
type Isbn10R (opts :: Opt) = MakeR3 (Isbn10 opts)
isbn13 :: Proxy (Isbn13 opts)
type Isbn13 (opts :: Opt) = '(opts, Isbn13ip, Isbn13op, Isbn13fmt, String)
type Isbn13R (opts :: Opt) = MakeR3 (Isbn13 opts)
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 :: Opt) (n :: Nat) = BaseN' opts n True
type BaseN' (opts :: Opt) (n :: Nat) p = '(opts, ReadBase Int n, p, ShowBase n, String)
type BaseIJ (opts :: Opt) (i :: Nat) (j :: Nat) = BaseIJ' opts i j True
type BaseIJ' (opts :: Opt) (i :: Nat) (j :: Nat) p = '(opts, ReadBase Int i >> ShowBase j, p, ReadBase Int j >> ShowBase i, String)
readshow :: Proxy (ReadShow opts t)
type ReadShow (opts :: Opt) (t :: Type) = '(opts, ReadP t Id, True, ShowP Id, String)
type ReadShowR (opts :: Opt) (t :: Type) = MakeR3 (ReadShow opts t)
readshow' :: Proxy (ReadShow' opts t p)
type ReadShow' (opts :: Opt) (t :: Type) p = '(opts, ReadP t Id, p, ShowP Id, String)
type ReadShowR' (opts :: Opt) (t :: Type) p = MakeR3 (ReadShow' opts t p)
between :: Proxy (BetweenN opts m n)
type BetweenN (opts :: Opt) m n = '(opts, Id, Between m n Id, Id, Int)
ok :: Proxy (Ok opts t)
type Ok (opts :: Opt) (t :: Type) = '(opts, Id, True, Id, t)
type OkR (opts :: Opt) (t :: Type) = MakeR3 (Ok opts t)
oknot :: Proxy (OkNot t)
type OkNot (t :: Type) = '(OAN, Id, False, Id, t)
type OkNotR (t :: Type) = MakeR3 (OkNot t)

datetime

datetime1 :: Proxy (DateTime1 opts t) #

read in a valid datetime

>>> newRefined3P (datetime1 @OL @LocalTime) "2018-09-14 02:57:04"
Right (Refined3 2018-09-14 02:57:04 "2018-09-14 02:57:04")

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

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

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

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

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

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

type DateTimeNR (opts :: Opt) = MakeR3 (DateTimeN opts) #

time

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

read in a time and validate it

>>> newRefined3P (hms @OL) "23:13:59"
Right (Refined3 [23,13,59] "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 :: Opt) = '(opts, Hmsip, Hmsop, Hmsfmt, String) #

type HmsR (opts :: Opt) = MakeR3 (Hms opts) #

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

type HmsR' (opts :: Opt) = MakeR3 (Hms' opts) #

credit cards

luhn :: Proxy (Luhn opts ns) #

luhn' :: (OptC opts, PP ns String ~ [Integer], KnownNat (SumT ns), P ns String) => Proxy (Luhn opts ns) #

type Luhn (opts :: Opt) (ns :: [Nat]) = '(opts, Luhnip, Luhnop (SumT ns), Luhnfmt ns, String) #

credit card with luhn algorithm

>>> newRefined3P (luhn11 @OZ) "1234-5678-901"
Left Step 2. Failed Boolean Check(op) | invalid checkdigit

>>> newRefined3P (luhn11 @OZ) "1234-5678-903"
Right (Refined3 [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 :: OptC opts => Proxy (Luhn opts '[4, 4, 3]) #

type Luhn11 (opts :: Opt) = Luhn opts '[4, 4, 3] #

type LuhnR (opts :: Opt) (n :: Nat) = MakeR3 (LuhnT opts n) #

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

Luhn check

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

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

| uses builtin IsLuhn

ssn

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

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

read in an ssn

>>> newRefined3P (ssn @OZ) "134-01-2211"
Right (Refined3 [134,1,2211] "134-01-2211")

>>> newRefined3P (ssn @OL) "666-01-2211"
Left Step 2. Failed 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. Failed Boolean Check(op) | Bool(1) [number for group 1 invalid: found 0] (1 <= 0)

type SsnR (opts :: Opt) = MakeR3 (Ssn opts) #

ipv4

ip4 :: OptC opts => Proxy (Ip4 opts) #

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

type Ip4R (opts :: Opt) = MakeR3 (Ip4 opts) #

read in an ipv4 address and validate it

>>> newRefined3P (ip4 @OZ) "001.223.14.1"
Right (Refined3 [1,223,14,1] "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' :: OptC opts => Proxy (Ip4' opts) #

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

type Ip4R' (opts :: Opt) = MakeR3 (Ip4' opts) #

ipv6

ip6 :: Proxy (Ip6 opts) #

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

type Ip6R (opts :: Opt) = MakeR3 (Ip6 opts) #

isbn10

isbn10 :: Proxy (Isbn10 opts) #

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

type Isbn10R (opts :: Opt) = MakeR3 (Isbn10 opts) #

validate isbn10

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

>>> newRefined3P (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, Isbn13fmt, String) #

type Isbn13R (opts :: Opt) = MakeR3 (Isbn13 opts) #

validate isbn13

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

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

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 :: Opt) (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 254 "fe")

>>> newRefined3P (basen' @OZ @16 @(100 <..> 400)) "00fe"
Right (Refined3 254 "fe")

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

>>> newRefined3P (basen' @OZ @16 @(GuardBool (PrintF "oops bad hex=%d" Id) (Id < 400))) "f0fe"
Left Step 2. Failed Boolean Check(op) | oops bad hex=61694

>>> newRefined3P (basen' @OL @16 @(Id < 400)) "f0fe"
Left Step 2. False Boolean Check(op) | {61694 < 400}

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

type BaseIJ (opts :: Opt) (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 "11111110" "fe")

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

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

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

read / show

readshow :: Proxy (ReadShow opts t) #

type ReadShow (opts :: Opt) (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 (13 % 3) "13 % 3")

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

>>> newRefined3P (readshow' @OZ @Rational @(3 % 1 <..> 5 % 1)) "13 % 3"
Right (Refined3 (13 % 3) "13 % 3")

>>> newRefined3P (Proxy @(ReadShow' OZ Rational (11 -% 2 <..> 3 -% 1))) "-13 % 3"
Right (Refined3 ((-13) % 3) "(-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 > (15 % 1))))) "13 % 3"
Left Step 2. False Boolean Check(op) | {invalid=4.33 13 % 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 2018-10-19 14:53:11.5121359 UTC "2018-10-19 14:53:11.5121359 UTC")

>>> :m + Data.Aeson
>>> newRefined3P (readshow @OZ @Value) "String \"jsonstring\""
Right (Refined3 (String "jsonstring") "String \"jsonstring\"")

>>> newRefined3P (readshow @OZ @Value) "Number 123.4"
Right (Refined3 (Number 123.4) "Number 123.4")

type ReadShowR (opts :: Opt) (t :: Type) = MakeR3 (ReadShow opts t) #

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

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

type ReadShowR' (opts :: Opt) (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 14 14)

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

>>> newRefined3P (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 BetweenN (opts :: Opt) m n = '(opts, Id, Between m n Id, Id, Int) #

miscellaneous

ok :: Proxy (Ok opts t) #

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

noop true

type OkR (opts :: Opt) (t :: Type) = MakeR3 (Ok opts t) #

oknot :: Proxy (OkNot t) #

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

noop false

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