{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveLift #-}
module Refined3Helper where
import Refined3
import Predicate
import UtilP
import Data.Proxy
import GHC.TypeLits (AppendSymbol,Nat,KnownNat)
import Data.Kind (Type)
import Data.Time
import qualified Data.Semigroup as SG
type Ccip = Map (ReadP Int) (Remove "-" Id >> Ones)
type Ccop (n :: Nat) = Guard ('(n,Len) >> Printf2 "expected %d digits but found %d") (Len >> Same n) >> Luhn
type Ccfmt (ns :: [Nat]) = ConcatMap ShowP Id >> SplitAts ns Id >> Concat (Intercalate '["-"] Id)
type Ccn (ns :: [Nat]) = '(Ccip, Ccop (SumT ns), Ccfmt ns, String)
type CC11 = Ccn '[4,4,3]
ccn :: forall (ns :: [Nat]) . (KnownNat (SumT ns), P ns String, PP ns String ~ [Integer]) => Proxy (Ccn ns)
ccn = mkProxy3
cc11 :: Proxy (Ccn '[4,4,3])
cc11 = mkProxy3P
type DateTime1 (t :: Type) = '(Dtip1 t, Dtop1, Dtfmt1, String)
type Dtip1 t = ParseTimeP t "%F %T" Id
type Dtop1 =
Map (ReadP Int) (FormatTimeP "%H %M %S" Id >> Resplit "\\s+" Id)
>> Guards '[ '(Printf2 "guard %d invalid hours %d", Between 0 23)
, '(Printf2 "guard %d invalid minutes %d", Between 0 59)
, '(Printf2 "guard %d invalid seconds %d", Between 0 59)
] >> 'True
type Dtfmt1 = FormatTimeP "%F %T" Id
ssn :: Proxy Ssn
ssn = mkProxy3
type Ssn = '(Ssnip, Ssnop, Ssnfmt, String)
type Ssnip = Map (ReadP Int) (Rescan "^(\\d{3})-(\\d{2})-(\\d{4})$" Id >> OneP >> Snd)
type Ssnop = GuardsQuick (Printf2 "number for group %d invalid: found %d")
'[Between 1 899 && Id /= 666, Between 1 99, Between 1 9999]
>> 'True
type Ssnop' = Guards '[ '(Printf2 "guard %d invalid: found %d", Between 1 899 && Id /= 666)
, '(Printf2 "group %d invalid: found %d", Between 1 99)
, '(Printf2 "group %d invalid: found %d", Between 1 9999)
] >> 'True
type Ssnfmt = Printfnt 3 "%03d-%02d-%04d"
hms :: Proxy Hms
hms = mkProxy3
type Hms = '(Hmsip, Hmsop >> 'True, Hmsfmt, String)
type Hmsip = Map (ReadP Int) (Resplit ":" Id)
type Hmsop = Guard (Printf "expected len 3 but found %d" Len) (Len >> Same 3)
>> Guards '[ '(Printf2 "guard(%d) %d hours is out of range", Between 0 23)
, '(Printf2 "guard(%d) %d mins is out of range", Between 0 59)
, '(Printf2 "guard(%d) %d secs is out of range", Between 0 59)]
type Hmsfmt = Printfnt 3 "%02d:%02d:%02d"
type Ip = '(Ipip, Ipop, Ipfmt, String)
type Ip1 = '(Ipip, Ipop', Ipfmt, String)
ip :: Proxy Ip
ip = mkProxy3
ip1 :: Proxy Ip1
ip1 = mkProxy3
type Ipip = Map (ReadP Int) (Rescan "^(\\d{1,3}).(\\d{1,3}).(\\d{1,3}).(\\d{1,3})$" Id >> OneP >> Snd)
type Ipop = GuardsQuick (Printf2 "guard(%d) octet out of range 0-255 found %d") (RepeatT 4 (Between 0 255)) >> 'True
type Ipop' = Guards '[
'(Printf2 "octet %d out of range 0-255 found %d", Between 0 255)
, '(Printf2 "octet %d out of range 0-255 found %d", Between 0 255)
, '(Printf2 "octet %d out of range 0-255 found %d", Between 0 255)
, '(Printf2 "octet %d out of range 0-255 found %d", Between 0 255)
] >> 'True
type Ipfmt = Printfnt 4 "%03d.%03d.%03d.%03d"
type HmsRE = "^([0-1][0-9]|2[0-3]):([0-5][0-9]):([0-5][0-9])$"
type Hmsconv = Do '[Rescan HmsRE Id, Head, Snd, Map (ReadBaseInt 10) Id]
type Hmsval = GuardsQuick (Printf2 "guard(%d) %d is out of range") '[Between 0 23, Between 0 59, Between 0 59]
type Hms4 = '(Hmsconv, Hmsval >> 'True, Hmsfmt, String)
hms4 :: Proxy Hms4
hms4 = mkProxy3
type OctetRE = "(25[0-5]|2[0..4][0-9]|1[0-9][0-9]|[1-9][0-9]|[0-9])"
type Ip4strictRE = "^" `AppendSymbol` IntersperseT "\\." (RepeatT 4 OctetRE) `AppendSymbol` "$"
type DateFmts = '["%Y-%m-%d", "%m/%d/%y", "%B %d %Y"]
type DateN = '(ParseTimes Day DateFmts Id, 'True, FormatTimeP "%Y-%m-%d" Id, String)
type DateTimeFmts = '["%Y-%m-%d %H:%M:%S", "%m/%d/%y %H:%M:%S", "%B %d %Y %H:%M:%S", "%Y-%m-%dT%H:%M:%S"]
type DateTimeN = '(ParseTimes UTCTime DateTimeFmts Id, 'True, FormatTimeP "%Y-%m-%d %H:%M:%S" Id, String)
type BaseN (n :: Nat) = '(ReadBase Integer n, 'True, ShowBase n, String)
base16 :: Proxy (BaseN 16)
base16 = mkProxy3
daten :: Proxy DateN
daten = mkProxy3
datetimen :: Proxy DateTimeN
datetimen = mkProxy3
type BetweenR m n = Refined3 Id (Between m n) Id Int
type LuhnR (n :: Nat) = MakeR3 (LuhnY n)
type LuhnR' (n :: Nat) = MakeR3 (LuhnX n)
type LuhnY (n :: Nat) =
'(Map (ReadP Int) Ones
, Guard (Printfn "incorrect number of digits found %d but expected %d in [%s]" (TupleI '[Len, W n, ShowP]))
(Len >> Same n)
>> Guard ("luhn check failed") Luhn >> 'True
, ConcatMap ShowP Id
, String)
type LuhnX (n :: Nat) =
'(Map (ReadP Int) Ones
, Luhn'' n >> 'True
, ConcatMap ShowP Id
, String)
type Luhn'' (n :: Nat) =
Guard (Printfn "incorrect number of digits found %d but expected %d in [%s]" (TupleI '[Len, W n, ShowP])) (Len >> Same n)
>> Do '[
Reverse
,Ziplc [1,2] Id
,Map (Fst * Snd >> If (Id >= 10) (Id - 9) Id) Id
,FoldMap (SG.Sum Int) Id
]
>> Guard (Printfn "expected %d mod 10 = 0 but found %d" (TupleI '[Id, Id `Mod` 10])) (Mod Id 10 >> Same 0)
type Luhn' (n :: Nat) =
Msg "Luhn'" (Do
'[Guard (Printfn "incorrect number of digits found %d but expected %d in [%s]" (TupleI '[Len, W n, Id])) (Len >> Same n)
,Do
'[Ones
,Map (ReadP Int) Id
,Reverse
,Ziplc [1,2] Id
,Map (Fst * Snd >> If (Id >= 10) (Id - 9) Id) Id
,FoldMap (SG.Sum Int) Id
]
,Guard (Printfn "expected %d mod 10 = 0 but found %d" (TupleI '[Id, Id `Mod` 10])) (Mod Id 10 >> Same 0)
])
type Ok (t :: Type) = '(Id, 'True, Id, t)
type OkR (t :: Type) = MakeR3 (Ok t)
type OkNot (t :: Type) = '(Id, 'False, Id, t)
type OkNotR (t :: Type) = MakeR3 (OkNot t)
type BaseIJ (i :: Nat) (j :: Nat) = BaseIJ' i j 'True
type BaseIJ' (i :: Nat) (j :: Nat) p = '(ReadBase Int i >> ShowBase j, p, ReadBase Int j >> ShowBase i, String)
type ReadShow (t :: Type) = '(ReadP t, 'True, ShowP, String)
type ReadShowR (t :: Type) = MakeR3 (ReadShow t)
type ReadShow' (t :: Type) p = '(ReadP t, p, ShowP, String)
type ReadShowR' (t :: Type) p = MakeR3 (ReadShow' t p)