{-# OPTIONS -Wno-unused-imports #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
-- | Contains prepackaged 4-tuples to use with 'Refined2'

module Predicate.Examples.Refined2 (
 -- ** datetime

    DateTime1
  , datetime1
  , daten
  , DateN
  , datetimen
  , DateTimeN
  , DateTimeNR

  -- ** time

  , hms
  , Hms
  , HmsR
  , Hms'
  , HmsR'

  -- ** credit cards

  , Luhn
  , luhn11

  -- ** ssn

  , ssn
  , Ssn
  , SsnR

  -- ** ipv4

  , ip4
  , Ip4
  , Ip4R

  , ip4'
  , Ip4'
  , Ip4R'

  -- ** ipv6

  , ip6
  , Ip6
  , Ip6R

  -- ** isbn10

  , isbn10
  , Isbn10
  , Isbn10R

  -- ** isbn13

  , isbn13
  , Isbn13
  , Isbn13R

 -- ** base n

  , BaseN
  , BaseN'
  , BaseIJ
  , BaseIJ'
  , BaseIJip
   ) where
import Predicate.Refined2
import Predicate.Examples.Common
import Predicate
import GHC.TypeLits (Nat)
import Data.Time (Day, UTCTime)
import Data.Kind (Type)
import Data.Proxy (Proxy(..))

-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XTemplateHaskell

-- >>> :set -XTypeApplications

-- >>> :m + Data.Time

-- >>> :m + Control.Lens

-- >>> :m + Text.Show.Functions


-- | 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"

--

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

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

--

datetime1 :: Proxy (DateTime1 opts t)
datetime1 :: Proxy (DateTime1 opts t)
datetime1 = Proxy (DateTime1 opts t)
forall k1 k2 k3 k4 (z :: (k1, k2, k3, k4)) (opts :: k1) (ip :: k2)
       (op :: k3) (i :: k4).
(z ~ '(opts, ip, op, i)) =>
Proxy '(opts, ip, op, i)
mkProxy2

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

datetimen :: OptC opts => Proxy (DateTimeN opts)
datetimen :: Proxy (DateTimeN opts)
datetimen = Proxy (DateTimeN opts)
forall k1 k2 (z :: (k1, k2, Type)) (opts :: Opt) (ip :: k1)
       (op :: k2) i.
(z ~ '(ip, op, i), Refined2C opts ip op i) =>
Proxy '(opts, ip, op, i)
mkProxy2'

-- valid dates for for DateFmts are "2001-01-01" "Jan 24 2009" and "03/29/07"

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

daten :: OptC opts => Proxy (DateN opts)
daten :: Proxy (DateN opts)
daten = Proxy (DateN opts)
forall k1 k2 (z :: (k1, k2, Type)) (opts :: Opt) (ip :: k1)
       (op :: k2) i.
(z ~ '(ip, op, i), Refined2C opts ip op i) =>
Proxy '(opts, ip, op, i)
mkProxy2'

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

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

--


ssn :: OptC opts => Proxy (Ssn opts)
ssn :: Proxy (Ssn opts)
ssn = Proxy (Ssn opts)
forall k1 k2 (z :: (k1, k2, Type)) (opts :: Opt) (ip :: k1)
       (op :: k2) i.
(z ~ '(ip, op, i), Refined2C opts ip op i) =>
Proxy '(opts, ip, op, i)
mkProxy2'

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


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

--

hms :: OptC opts => Proxy (Hms opts)
hms :: Proxy (Hms opts)
hms = Proxy (Hms opts)
forall k1 k2 (z :: (k1, k2, Type)) (opts :: Opt) (ip :: k1)
       (op :: k2) i.
(z ~ '(ip, op, i), Refined2C opts ip op i) =>
Proxy '(opts, ip, op, i)
mkProxy2'

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

--hms' :: Proxy (Hms' OZ)

--hms' = mkProxy2'


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

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

--

type Ip4R (opts :: Opt) = MakeR2 (Ip4 opts)
type Ip4 (opts :: Opt) = '(opts, Ip4ip, Ip4op, String) -- guards


ip4 :: Proxy (Ip4 opts)
ip4 :: Proxy (Ip4 opts)
ip4 = Proxy (Ip4 opts)
forall k (t :: k). Proxy t
Proxy

type Ip4R' (opts :: Opt) = MakeR2 (Ip4' opts)
type Ip4' (opts :: Opt) = '(opts, Ip4ip, Ip4op', String) -- boolean predicates


ip4' :: Proxy (Ip4' opts)
ip4' :: Proxy (Ip4' opts)
ip4' = Proxy (Ip4' opts)
forall k (t :: k). Proxy t
Proxy

type Ip6R (opts :: Opt) = MakeR2 (Ip6 opts)
type Ip6 (opts :: Opt) = '(opts, Ip6ip, Ip6op, String) -- guards


ip6 :: Proxy (Ip6 opts)
ip6 :: Proxy (Ip6 opts)
ip6 = Proxy (Ip6 opts)
forall k (t :: k). Proxy t
Proxy

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

--

type Isbn10R (opts :: Opt) = MakeR2 (Isbn10 opts)
type Isbn10 (opts :: Opt) = '(opts, Isbn10ip, Isbn10op, String) -- guards


isbn10 :: Proxy (Isbn10 opts)
isbn10 :: Proxy (Isbn10 opts)
isbn10 = Proxy (Isbn10 opts)
forall k (t :: k). Proxy t
Proxy

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

--

type Isbn13R (opts :: Opt) = MakeR2 (Isbn13 opts)
type Isbn13 (opts :: Opt) = '(opts, Isbn13ip, Isbn13op, String) -- guards


isbn13 :: Proxy (Isbn13 opts)
isbn13 :: Proxy (Isbn13 opts)
isbn13 = Proxy (Isbn13 opts)
forall k (t :: k). Proxy t
Proxy



luhn11 :: Proxy (Luhn opts 11)
luhn11 :: Proxy (Luhn opts 11)
luhn11 = Proxy (Luhn opts 11)
forall k (t :: k). Proxy t
Proxy

-- | 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) = BaseN' opts n 'True
type BaseN' (opts :: Opt) (n :: Nat) p = '(opts,ReadBase Int n, p, String)


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

--

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

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

-- | take any valid Read/Show instance and turn it into a valid 'Predicate.Refined2.Refined2'

--

-- >>> :m + Data.Ratio

-- >>> newRefined2 @OZ @(ReadP Rational Id) @'True "13 % 3"

-- Right (Refined2 (13 % 3) "13 % 3")

--

-- >>> newRefined2 @OZ @(ReadP Rational Id) @'True "13x % 3"

-- Left Step 1. Failed Initial Conversion(ip) | ReadP Ratio Integer (13x % 3)

--

-- >>> newRefined2 @OZ @(ReadP Rational Id) @(3 % 1 <..> 5 % 1) "13 % 3"

-- Right (Refined2 (13 % 3) "13 % 3")

--

-- >>> newRefined2 @OZ @(ReadP Rational Id) @(11 -% 2 <..> 3 -% 1) "-13 % 3"

-- Right (Refined2 ((-13) % 3) "-13 % 3")

--

-- >>> newRefined2 @OZ @(ReadP Rational Id) @(Id > (15 % 1)) "13 % 3"

-- Left Step 2. False Boolean Check(op) | FalseP

--

-- >>> newRefined2 @OL @(ReadP Rational Id) @(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}

--

-- >>> newRefined2 @OZ @(ReadP Rational Id) @(Id > (11 % 1)) "13 % 3"

-- Left Step 2. False Boolean Check(op) | FalseP

--

-- >>> newRefined2 @OZ @(ReadP UTCTime Id) @'True "2018-10-19 14:53:11.5121359 UTC"

-- Right (Refined2 2018-10-19 14:53:11.5121359 UTC "2018-10-19 14:53:11.5121359 UTC")

--

-- >>> :m + Data.Aeson

-- >>> newRefined2 @OZ @(ReadP Value Id) @'True "String \"jsonstring\""

-- Right (Refined2 (String "jsonstring") "String \"jsonstring\"")

--

-- >>> newRefined2 @OZ @(ReadP Value Id) @'True "Number 123.4"

-- Right (Refined2 (Number 123.4) "Number 123.4")

--

-- >>> newRefined @OU @((Id $$ 13) > 100) (\x -> x * 14)

-- Right (Refined <function>)

--

-- >>> newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to r2Out

-- Just <function>

--

-- >>> newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to r2In

-- Just 182

--

-- >>> newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to (($ 13) . r2Out)

-- Just 182

--

-- >>> newRefined2 @OZ @(Pop0 Fst Id) @(Len > 1) (Proxy @Snd,"Abcdef") ^? _Right . to r2In

-- Just "Abcdef"

--

-- >>> newRefined2 @OZ @(Pop0 Fst Id >> Len) @(Id > 1) (Proxy @Snd,"Abcdef") ^? _Right . to r2In

-- Just 6

--