{-# 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 #-}
module Predicate.Examples.Refined3 (
datetime1
, DateTime1
, daten
, DateN
, datetimen
, DateTimeN
, DateTimeNR
, hms
, Hms
, HmsR
, Hms'
, HmsR'
, luhn
, luhn'
, Luhn
, luhn11
, Luhn11
, LuhnR
, LuhnT
, ssn
, Ssn
, SsnR
, ip4
, Ip4
, Ip4R
, ip4'
, Ip4'
, Ip4R'
, ip6
, Ip6
, Ip6R
, isbn10
, Isbn10
, Isbn10R
, isbn13
, Isbn13
, Isbn13R
, basen
, base2
, base16
, basen'
, base2'
, base16'
, BaseN
, BaseN'
, BaseIJ
, BaseIJ'
, readshow
, ReadShow
, ReadShowR
, readshow'
, ReadShow'
, ReadShowR'
, between
, BetweenN
, ok
, Ok
, OkR
, oknot
, OkNot
, OkNotR
) where
import Predicate.Examples.Common
import Predicate.Refined3
import Predicate
import Data.Proxy (Proxy(..))
import GHC.TypeLits (KnownNat, Nat)
import Data.Kind (Type)
import Data.Time (Day, UTCTime)
type Luhn (opts :: Opt) (ns :: [Nat]) = '(opts, Luhnip, Luhnop (SumT ns), Luhnfmt ns, String)
type Luhn11 (opts :: Opt) = Luhn opts '[4,4,3]
luhn :: Proxy (Luhn opts ns)
luhn :: Proxy (Luhn opts ns)
luhn = Proxy (Luhn opts ns)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
luhn' :: ( OptC opts
, PP ns String ~ [Integer]
, KnownNat (SumT ns)
, P ns String
) => Proxy (Luhn opts ns)
luhn' :: Proxy (Luhn opts ns)
luhn' = Proxy (Luhn opts ns)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
luhn11 :: OptC opts => Proxy (Luhn opts '[4,4,3])
luhn11 :: Proxy (Luhn opts '[4, 4, 3])
luhn11 = Proxy (Luhn opts '[4, 4, 3])
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
datetime1 :: Proxy (DateTime1 opts t)
datetime1 :: Proxy (DateTime1 opts t)
datetime1 = Proxy (DateTime1 opts t)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
type DateTime1 (opts :: Opt) (t :: Type) = '(opts, Dtip t, 'True, Dtfmt, String)
type DateN (opts :: Opt) = '(opts, ParseTimes Day DateFmts Id, 'True, FormatTimeP "%Y-%m-%d", String)
type DateTimeNR (opts :: Opt) = MakeR3 (DateTimeN opts)
type DateTimeN (opts :: Opt) = '(opts, ParseTimes UTCTime DateTimeFmts Id, 'True, FormatTimeP "%Y-%m-%d %H:%M:%S" , String)
ssn :: OptC opts => Proxy (Ssn opts)
ssn :: Proxy (Ssn opts)
ssn = Proxy (Ssn opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
type Ssn (opts :: Opt) = '(opts, Ssnip, Ssnop, Ssnfmt, String)
type SsnR (opts :: Opt) = MakeR3 (Ssn opts)
hms :: OptC opts => Proxy (Hms opts)
hms :: Proxy (Hms opts)
hms = Proxy (Hms opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
type HmsR (opts :: Opt) = MakeR3 (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 Ip4R (opts :: Opt) = MakeR3 (Ip4 opts)
type Ip4 (opts :: Opt) = '(opts, Ip4ip, Ip4op, Ip4fmt, String)
ip4 :: OptC opts => Proxy (Ip4 opts)
ip4 :: Proxy (Ip4 opts)
ip4 = Proxy (Ip4 opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
type Ip4R' (opts :: Opt) = MakeR3 (Ip4' opts)
type Ip4' (opts :: Opt) = '(opts, Ip4ip, Ip4op', Ip4fmt, String)
ip4' :: OptC opts => Proxy (Ip4' opts)
ip4' :: Proxy (Ip4' opts)
ip4' = Proxy (Ip4' opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
type Ip6R (opts :: Opt) = MakeR3 (Ip6 opts)
type Ip6 (opts :: Opt) = '(opts, Ip6ip, Ip6op, Ip6fmt, String)
ip6 :: Proxy (Ip6 opts)
ip6 :: Proxy (Ip6 opts)
ip6 = Proxy (Ip6 opts)
forall k (t :: k). Proxy t
Proxy
type Isbn10R (opts :: Opt) = MakeR3 (Isbn10 opts)
type Isbn10 (opts :: Opt) = '(opts, Isbn10ip, Isbn10op, Isbn10fmt, String)
isbn10 :: Proxy (Isbn10 opts)
isbn10 :: Proxy (Isbn10 opts)
isbn10 = Proxy (Isbn10 opts)
forall k (t :: k). Proxy t
Proxy
type Isbn13R (opts :: Opt) = MakeR3 (Isbn13 opts)
type Isbn13 (opts :: Opt) = '(opts, Isbn13ip, Isbn13op, Isbn13fmt, String)
isbn13 :: Proxy (Isbn13 opts)
isbn13 :: Proxy (Isbn13 opts)
isbn13 = Proxy (Isbn13 opts)
forall k (t :: k). Proxy t
Proxy
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)
base16 :: Proxy (BaseN opts 16)
base16 :: Proxy (BaseN opts 16)
base16 = Proxy (BaseN opts 16)
forall (opts :: Opt) (n :: Nat). Proxy (BaseN opts n)
basen
base16' :: Proxy (BaseN' opts 16 p)
base16' :: Proxy (BaseN' opts 16 p)
base16' = Proxy (BaseN' opts 16 p)
forall k (opts :: Opt) (n :: Nat) (p :: k). Proxy (BaseN' opts n p)
basen'
base2 :: Proxy (BaseN opts 2)
base2 :: Proxy (BaseN opts 2)
base2 = Proxy (BaseN opts 2)
forall (opts :: Opt) (n :: Nat). Proxy (BaseN opts n)
basen
base2' :: Proxy (BaseN' opts 2 p)
base2' :: Proxy (BaseN' opts 2 p)
base2' = Proxy (BaseN' opts 2 p)
forall k (opts :: Opt) (n :: Nat) (p :: k). Proxy (BaseN' opts n p)
basen'
basen :: Proxy (BaseN opts n)
basen :: Proxy (BaseN opts n)
basen = Proxy (BaseN opts n)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
basen' :: Proxy (BaseN' opts n p)
basen' :: Proxy (BaseN' opts n p)
basen' = Proxy (BaseN' opts n p)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
daten :: OptC opts => Proxy (DateN opts)
daten :: Proxy (DateN opts)
daten = Proxy (DateN opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
datetimen :: OptC opts => Proxy (DateTimeN opts)
datetimen :: Proxy (DateTimeN opts)
datetimen = Proxy (DateTimeN opts)
forall k1 k2 k3 (z :: (Opt, k1, k2, k3, Type)) (opts :: Opt)
(ip :: k1) (op :: k2) (fmt :: k3) i.
(z ~ '(opts, ip, op, fmt, i), Refined3C opts ip op fmt i) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3'
between :: Proxy (BetweenN opts m n)
between :: Proxy (BetweenN opts m n)
between = Proxy (BetweenN opts m n)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
type BetweenN (opts :: Opt) m n = '(opts, Id, Between m n Id, Id, Int)
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)
type Ok (opts :: Opt) (t :: Type) = '(opts, Id, 'True, Id, t)
type OkR (opts :: Opt) (t :: Type) = MakeR3 (Ok opts t)
ok :: Proxy (Ok opts t)
ok :: Proxy (Ok opts t)
ok = Proxy (Ok opts t)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
type OkNot (t :: Type) = '(OAN, Id, 'False, Id, t)
type OkNotR (t :: Type) = MakeR3 (OkNot t)
oknot :: Proxy (OkNot t)
oknot :: Proxy (OkNot t)
oknot = Proxy (OkNot t)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
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)
type ReadShow (opts :: Opt) (t :: Type) = '(opts, ReadP t Id, 'True, ShowP Id, String)
type ReadShowR (opts :: Opt) (t :: Type) = MakeR3 (ReadShow opts t)
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)
readshow :: Proxy (ReadShow opts t)
readshow :: Proxy (ReadShow opts t)
readshow = Proxy (ReadShow opts t)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3
readshow' :: Proxy (ReadShow' opts t p)
readshow' :: Proxy (ReadShow' opts t p)
readshow' = Proxy (ReadShow' opts t p)
forall k1 k2 k3 k4 k5 (z :: (k1, k2, k3, k4, k5)) (opts :: k1)
(ip :: k2) (op :: k3) (fmt :: k4) (i :: k5).
(z ~ '(opts, ip, op, fmt, i)) =>
Proxy '(opts, ip, op, fmt, i)
mkProxy3