{-# OPTIONS -Wall #-}
{-# OPTIONS -Wno-compat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE FunctionalDependencies #-}
module Predicate.Util (
TT(..)
, tBool
, tString
, tForest
, fixBoolT
, topMessage
, hasNoTree
, BoolT(..)
, GetBoolT(..)
, _FailT
, _PresentT
, _FalseT
, _TrueT
, PE
, pString
, mkNode
, mkNodeB
, mkNodeSkipP
, getValAndPE
, getValLRFromTT
, fromTT
, getValueLR
, getValueLRHide
, fixLite
, fixit
, prefixMsg
, splitAndAlign
, POptsL
, POpts
, Debug(..)
, Disp(..)
, Color(..)
, colorMe
, isVerbose
, colorBoolT
, colorBoolT'
, setOtherEffects
, type Color1
, type Color2
, type Color3
, type Color4
, type Color5
, type Other1
, type Other2
, HOpts(..)
, OptT(..)
, OptTC()
, getOptT
, subopts
, show01
, lit01
, show01'
, lit01'
, showLit0
, showLit1
, show0
, show3
, show1
, showL
, litL
, litBL
, litBS
, ROpt(..)
, compileRegex
, GetROpts(..)
, RReplace(..)
, GetReplaceFnSub(..)
, ReplaceFnSub(..)
, ZwischenT
, FailWhenT
, FailUnlessT
, AndT
, OrT
, NotT
, RepeatT
, IntersperseT
, LenT
, InductTupleC(..)
, InductListC(..)
, FlipT
, IfT
, SumT
, MapT
, ConsT
, type (%%)
, type (%&)
, type (<%>)
, AnyT
, nat
, symb
, GetNats(..)
, GetSymbs(..)
, GetLen(..)
, GetThese(..)
, GetOrdering(..)
, GetBool(..)
, OrderingP(..)
, GetOrd(..)
, prtTreePure
, prettyRational
, formatOMsg
, (~>)
, T4_1
, T4_2
, T4_3
, T4_4
, T5_1
, T5_2
, T5_3
, T5_4
, T5_5
, Holder
, hh
, showT
, prettyOrd
, removeAnsi
, MonadEval(..)
, errorInProgram
, readField
, showThese
, chkSize
, pureTryTest
, pureTryTestPred
, isPrime
) where
import qualified GHC.TypeNats as GN
import Data.Ratio
import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat,ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Control.Lens
import Control.Arrow
import Data.List
import qualified Data.Tree.View as TV
import Data.Tree
import Data.Tree.Lens
import Data.Proxy
import Data.Data
import System.Console.Pretty
import GHC.Exts (Constraint)
import qualified Text.Regex.PCRE.Heavy as RH
import qualified Text.Regex.PCRE.Light as RL
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
import GHC.Word (Word8)
import Data.Sequence (Seq)
import Control.Applicative (ZipList)
import Data.Kind (Type)
import Data.These (These(..))
import Data.These.Combinators (isThis, isThat, isThese)
import qualified Control.Exception as E
import Control.DeepSeq
import System.IO.Unsafe (unsafePerformIO)
import Data.Bool
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as N
import Data.Either
import qualified Text.Read.Lex as L
import Text.ParserCombinators.ReadPrec
import qualified GHC.Read as GR
import Data.ByteString (ByteString)
import qualified Data.ByteString.Lazy.Char8 as BL8
import qualified Data.ByteString.Char8 as BS8
import GHC.Stack
import Data.Monoid (Last (..))
import Data.Maybe
import Data.Coerce
import Data.Foldable (toList)
data TT a = TT { _tBool :: !(BoolT a)
, _tString :: !String
, _tForest :: !(Forest PE)
} deriving Show
data BoolT a where
FailT :: !String -> BoolT a
FalseT :: BoolT Bool
TrueT :: BoolT Bool
PresentT :: !a -> BoolT a
instance Semigroup (BoolT a) where
FailT s <> FailT s1 = FailT (s <> s1)
FailT s <> _ = FailT s
_ <> FailT s = FailT s
FalseT <> _ = FalseT
_ <> FalseT = FalseT
TrueT <> TrueT = TrueT
TrueT <> PresentT a = PresentT a
PresentT a <> TrueT = PresentT a
PresentT a <> PresentT _ = PresentT a
deriving instance Show a => Show (BoolT a)
deriving instance Eq a => Eq (BoolT a)
class GetBoolT a (x :: BoolT a) | x -> a where
getBoolT :: Either Bool Bool
instance GetBoolT Bool 'TrueT where
getBoolT = Left True
instance GetBoolT Bool 'FalseT where
getBoolT = Left False
instance GetBoolT a ('PresentT b) where
getBoolT = Right True
instance GetBoolT a ('FailT s) where
getBoolT = Right False
tBool :: Lens (TT a) (TT b) (BoolT a) (BoolT b)
tBool afb s = (\b -> s { _tBool = b }) <$> afb (_tBool s)
tString :: Lens' (TT a) String
tString afb s = (\b -> s { _tString = b }) <$> afb (_tString s)
tForest :: Lens' (TT a) (Forest PE)
tForest afb s = (\b -> s { _tForest = b }) <$> afb (_tForest s)
boolT2P :: Lens' (BoolT a) BoolP
boolT2P afb = \case
FailT e -> FailT e <$ afb (FailP e)
TrueT -> TrueT <$ afb TrueP
FalseT -> FalseT <$ afb FalseP
PresentT a -> PresentT a <$ afb PresentP
data BoolP =
FailP !String
| FalseP
| TrueP
| PresentP
deriving (Show, Eq)
data PE = PE { _pBool :: !BoolP
, _pString :: !String
} deriving Show
pBool :: Lens' PE BoolP
pBool afb (PE x y) = flip PE y <$> afb x
pString :: Lens' PE String
pString afb s = (\b -> s { _pString = b }) <$> afb (_pString s)
mkNode :: POpts -> BoolT a -> String -> [Holder] -> TT a
mkNode opts bt ss hs =
case oDebug opts of
DZero -> TT bt [] []
DLite -> TT bt ss []
_ -> TT bt ss (map fromTTH hs)
mkNodeB :: POpts -> Bool -> String -> [Holder] -> TT Bool
mkNodeB opts b = mkNode opts (bool FalseT TrueT b)
mkNodeSkipP :: Tree PE
mkNodeSkipP = Node (PE TrueP "skipped PP ip i = Id") []
getValAndPE :: TT a -> (Either String a, Tree PE)
getValAndPE tt = (getValLRFromTT tt, fromTT tt)
getValLRFromTT :: TT a -> Either String a
getValLRFromTT = getValLR . _tBool
getValLR :: BoolT a -> Either String a
getValLR = \case
FailT e -> Left e
TrueT -> Right True
FalseT -> Right False
PresentT a -> Right a
fromTT :: TT a -> Tree PE
fromTT (TT bt ss tt) = Node (PE (bt ^. boolT2P) ss) tt
data Holder = forall w . Holder !(TT w)
fromTTH :: Holder -> Tree PE
fromTTH (Holder x) = fromTT x
hh :: TT w -> Holder
hh = Holder
getValueLR :: POpts -> String -> TT a -> [Holder] -> Either (TT x) a
getValueLR = getValueLRImpl True
getValueLRHide :: POpts -> String -> TT a -> [Holder] -> Either (TT x) a
getValueLRHide = getValueLRImpl False
getValueLRImpl :: Bool -> POpts -> String -> TT a -> [Holder] -> Either (TT x) a
getValueLRImpl showError opts msg0 tt hs =
let tt' = hs ++ [hh tt]
in left (\e -> mkNode
opts
(FailT e)
(msg0 <> if showError || isVerbose opts then (if null msg0 then "" else " ") <> "[" <> e <> "]"
else "")
tt'
)
(getValLRFromTT tt)
newtype SColor = SColor Color
instance Show SColor where
show (SColor c) =
case c of
Black-> "Black"
Red-> "Red"
Green-> "Green"
Yellow-> "Yellow"
Blue-> "Blue"
Magenta-> "Magenta"
Cyan-> "Cyan"
White-> "White"
Default -> "Default"
newtype PColor = PColor (BoolP -> String -> String)
instance Show PColor where
show PColor {} = "PColor <fn>"
type family HKD f a where
HKD Identity a = a
HKD f a = f a
type POpts = HOpts Identity
data HOpts f =
HOpts { oWidth :: !(HKD f Int)
, oDebug :: !(HKD f Debug)
, oDisp :: !(HKD f Disp)
, oColor :: !(HKD f (String, PColor))
, oMsg :: ![String]
, oRecursion :: !(HKD f Int)
, oOther :: !(HKD f (Bool, SColor, SColor))
, oNoColor :: !(HKD f Bool)
}
deriving instance
( Show (HKD f Int)
, Show (HKD f Debug)
, Show (HKD f Disp)
, Show (HKD f (String, PColor))
, Show (HKD f Bool)
, Show (HKD f (Bool, SColor, SColor))
) => Show (HOpts f)
reifyOpts :: HOpts Last -> HOpts Identity
reifyOpts h =
HOpts (fromMaybe (oWidth defOpts) (getLast (oWidth h)))
(fromMaybe (oDebug defOpts) (getLast (oDebug h)))
(fromMaybe (oDisp defOpts) (getLast (oDisp h)))
(if fromMaybe (oNoColor defOpts) (getLast (oNoColor h)) then nocolor
else fromMaybe (oColor defOpts) (getLast (oColor h)))
(oMsg defOpts <> oMsg h)
(fromMaybe (oRecursion defOpts) (getLast (oRecursion h)))
(if fromMaybe (oNoColor defOpts) (getLast (oNoColor h)) then otherDef
else fromMaybe (oOther defOpts) (getLast (oOther h)))
(fromMaybe (oNoColor defOpts) (getLast (oNoColor h)))
setWidth :: Int -> POptsL
setWidth i = mempty { oWidth = pure i }
setMessage :: String -> POptsL
setMessage s = mempty { oMsg = pure s }
setRecursion :: Int -> POptsL
setRecursion i = mempty { oRecursion = pure i }
setOther :: Bool -> Color -> Color -> POptsL
setOther b c1 c2 = mempty { oOther = pure $ coerce (b, c1, c2) }
setNoColor :: Bool -> POptsL
setNoColor b = mempty { oNoColor = pure b }
setDisp :: Disp -> POptsL
setDisp d = mempty { oDisp = pure d }
setCreateColor :: String
-> Color
-> Color
-> Color
-> Color
-> Color
-> Color
-> Color
-> Color
-> POptsL
setCreateColor s c1 c2 c3 c4 c5 c6 c7 c8 =
let pc = \case
FailP {} -> color c1 . bgColor c2
FalseP -> color c3 . bgColor c4
TrueP -> color c5 . bgColor c6
PresentP -> color c7 . bgColor c8
in mempty { oColor = pure (s,PColor pc) }
setDebug :: Debug -> POptsL
setDebug d =
mempty { oDebug = pure d }
type POptsL = HOpts Last
instance Monoid (HOpts Last) where
mempty = HOpts mempty mempty mempty mempty mempty mempty mempty mempty
instance Semigroup (HOpts Last) where
HOpts a b c d e f g h <> HOpts a' b' c' d' e' f' g' h'
= HOpts (a <> a')
(b <> b')
(c <> c')
(d <> d')
(e <> e')
(f <> f')
(g <> g')
(h <> h')
data Disp = Ansi
| Unicode
deriving (Show, Eq)
defOpts :: POpts
defOpts = HOpts
{ oWidth = 200
, oDebug = DNormal
, oDisp = Ansi
, oColor = colorDef
, oMsg = mempty
, oRecursion = 100
, oOther = otherDef
, oNoColor = False
}
otherDef :: (Bool, SColor, SColor)
otherDef = coerce (True, Default, Default)
nocolor, colorDef :: (String, PColor)
nocolor = ("nocolor", PColor $ flip const)
colorDef = fromJust $ getLast $ oColor $ getOptT' @Color5
data Debug =
DZero
| DLite
| DSubNormal
| DNormal
| DVerbose
deriving (Ord, Show, Eq, Enum, Bounded)
isVerbose :: POpts -> Bool
isVerbose = (DVerbose==) . oDebug
type Color1 = 'OColor "color1" 'Default 'Blue 'Default 'Red 'Black 'Cyan 'Black 'Yellow
type Color2 = 'OColor "color2" 'Default 'Magenta 'Default 'Red 'Black 'White 'Black 'Yellow
type Color3 = 'OColor "color3" 'Default 'Blue 'Red 'Default 'White 'Default 'Black 'Yellow
type Color4 = 'OColor "color4" 'Default 'Red 'Red 'Default 'Green 'Default 'Black 'Yellow
type Color5 = 'OColor "color5" 'Blue 'Default 'Red 'Default 'Cyan 'Default 'Yellow 'Default
type Other1 = 'OOther 'True 'Yellow 'Default
type Other2 = 'OOther 'True 'Default 'Default
fixBoolT :: TT Bool -> TT Bool
fixBoolT t =
case t ^? tBool . _PresentT of
Nothing -> t
Just b -> t & tBool .~ _boolT # b
show01 :: (Show a1, Show a2) => POpts -> String -> a1 -> a2 -> String
show01 opts msg0 ret = lit01 opts msg0 ret . show
lit01 :: Show a1 => POpts -> String -> a1 -> String -> String
lit01 opts msg0 ret = lit01' opts msg0 ret ""
show01' :: (Show a1, Show a2) => POpts -> String -> a1 -> String -> a2 -> String
show01' opts msg0 ret fmt = lit01' opts msg0 ret fmt . show
lit01' :: Show a1 => POpts -> String -> a1 -> String -> String -> String
lit01' opts msg0 ret fmt as
| null fmt && null as = msg0
| otherwise =
msg0
<> show0 opts " " ret
<> showLit1 opts (" | " ++ fmt) as
showLit0 :: POpts -> String -> String -> String
showLit0 o = showLitImpl o DLite
showLit1 :: POpts -> String -> String -> String
showLit1 o = showLitImpl o DLite
showLitImpl :: POpts -> Debug -> String -> String -> String
showLitImpl o i s a =
if oDebug o >= i then s <> litL (oWidth o) a
else ""
show0 :: Show a => POpts -> String -> a -> String
show0 o = showAImpl o DLite
show3 :: Show a => POpts -> String -> a -> String
show3 o = showAImpl o DVerbose
show1 :: Show a => POpts -> String -> a -> String
show1 o = showAImpl o DLite
showAImpl :: Show a => POpts -> Debug -> String -> a -> String
showAImpl o i s a = showLitImpl o i s (show a)
showL :: Show a => Int -> a -> String
showL i = litL i . show
litL :: Int -> String -> String
litL i s = take i s <> if length s > i then "..." else ""
litBL :: Int -> BL8.ByteString -> String
litBL i s = litL i (BL8.unpack (BL8.take (fromIntegral i+1) s))
litBS :: Int -> BS8.ByteString -> String
litBS i s = litL i (BS8.unpack (BS8.take (i+1) s))
data ROpt =
Anchored
| Auto_callout
| Caseless
| Dollar_endonly
| Dotall
| Dupnames
| Extended
| Extra
| Firstline
| Multiline
| Newline_cr
| Newline_crlf
| Newline_lf
| No_auto_capture
| Ungreedy
| Utf8
| No_utf8_check
deriving (Show,Eq,Ord,Enum,Bounded)
compileRegex :: forall rs a . GetROpts rs
=> POpts -> String -> String -> [Holder] -> Either (TT a) RH.Regex
compileRegex opts nm s hhs
| null s = Left (mkNode opts (FailT "Regex cannot be empty") nm hhs)
| otherwise =
let rs = getROpts @rs
mm = nm <> " " <> show rs
in flip left (RH.compileM (TE.encodeUtf8 (T.pack s)) rs)
$ \e -> mkNode opts (FailT "Regex failed to compile") (mm <> " compile failed with regex msg[" <> e <> "]") hhs
class GetROpts (os :: [ROpt]) where
getROpts :: [RL.PCREOption]
instance GetROpts '[] where
getROpts = []
instance (GetROpt r, GetROpts rs) => GetROpts (r ': rs) where
getROpts = getROpt @r : getROpts @rs
class GetROpt (o :: ROpt) where
getROpt :: RL.PCREOption
instance GetROpt 'Anchored where getROpt = RL.anchored
instance GetROpt 'Auto_callout where getROpt = RL.auto_callout
instance GetROpt 'Caseless where getROpt = RL.caseless
instance GetROpt 'Dollar_endonly where getROpt = RL.dollar_endonly
instance GetROpt 'Dotall where getROpt = RL.dotall
instance GetROpt 'Dupnames where getROpt = RL.dupnames
instance GetROpt 'Extended where getROpt = RL.extended
instance GetROpt 'Extra where getROpt = RL.extra
instance GetROpt 'Firstline where getROpt = RL.firstline
instance GetROpt 'Multiline where getROpt = RL.multiline
instance GetROpt 'Newline_cr where getROpt = RL.newline_cr
instance GetROpt 'Newline_crlf where getROpt = RL.newline_crlf
instance GetROpt 'Newline_lf where getROpt = RL.newline_lf
instance GetROpt 'No_auto_capture where getROpt = RL.no_auto_capture
instance GetROpt 'Ungreedy where getROpt = RL.ungreedy
instance GetROpt 'Utf8 where getROpt = RL.utf8
instance GetROpt 'No_utf8_check where getROpt = RL.no_utf8_check
data ReplaceFnSub = RPrepend | ROverWrite | RAppend deriving (Show,Eq)
class GetReplaceFnSub (k :: ReplaceFnSub) where
getReplaceFnSub :: ReplaceFnSub
instance GetReplaceFnSub 'RPrepend where getReplaceFnSub = RPrepend
instance GetReplaceFnSub 'ROverWrite where getReplaceFnSub = ROverWrite
instance GetReplaceFnSub 'RAppend where getReplaceFnSub = RAppend
data RReplace =
RReplace !ReplaceFnSub !String
| RReplace1 !(String -> [String] -> String)
| RReplace2 !(String -> String)
| RReplace3 !([String] -> String)
instance Show RReplace where
show = \case
RReplace o s -> "RReplace " ++ show o ++ " " ++ s
RReplace1 {} -> "RReplace1 <fn>"
RReplace2 {} -> "RReplace2 <fn>"
RReplace3 {} -> "RReplace3 <fn>"
splitAndAlign :: Show x =>
POpts
-> String
-> [((Int, x), TT a)]
-> Either (TT w) [(a, (Int, x), TT a)]
splitAndAlign opts msgs ts =
case partitionEithers (map partitionTTExtended ts) of
(excs@(e:_), _) ->
Left $ mkNode opts
(FailT (groupErrors (map snd excs)))
(msgs <> (formatList opts [fst e] <> " excnt=" <> show (length excs)))
(map (hh . snd) ts)
([], tfs) -> Right tfs
groupErrors :: [String] -> String
groupErrors =
intercalate " | "
. map (\xs@(x :| _) -> x <> (if length xs > 1 then "(" <> show (length xs) <> ")" else ""))
. N.group
partitionTTExtended :: (w, TT a) -> Either ((w, TT x), String) (a, w, TT a)
partitionTTExtended (s, t) =
case _tBool t of
FailT e -> Left ((s, t & tBool .~ FailT e), e)
PresentT a -> Right (a,s,t)
TrueT -> Right (True,s,t)
FalseT -> Right (False,s,t)
formatList :: forall x z . Show x => POpts -> [((Int, x), z)] -> String
formatList opts = unwords . map (\((i, a), _) -> "(i=" <> show i <> showAImpl opts DLite ", a=" a <> ")")
instance Foldable TT where
foldMap am = foldMap am . _tBool
instance Foldable BoolT where
foldMap am = either (const mempty) am . getValLR
_boolT :: Prism' (BoolT Bool) Bool
_boolT = prism' (bool FalseT TrueT)
$ \case
PresentT a -> Just a
TrueT -> Just True
FalseT -> Just False
FailT {} -> Nothing
_FailT :: Prism' (BoolT a) String
_FailT = prism' FailT $ \case
FailT s -> Just s
_ -> Nothing
_PresentT :: Prism' (BoolT a) a
_PresentT = prism' PresentT $ \case
PresentT a -> Just a
_ -> Nothing
_FalseT :: Prism' (BoolT Bool) ()
_FalseT = prism' (const FalseT) $
\case
FalseT -> Just ()
_ -> Nothing
_TrueT :: Prism' (BoolT Bool) ()
_TrueT = prism' (const TrueT) $
\case
TrueT -> Just ()
_ -> Nothing
(~>) :: Bool -> Bool -> Bool
p ~> q = not p || q
infixr 1 ~>
type family ZwischenT (a :: Nat) (b :: Nat) (v :: Nat) :: Constraint where
ZwischenT m n v =
FailUnlessT (AndT (m GL.<=? v) (v GL.<=? n))
('GL.Text "ZwischenT failure"
':$$: 'GL.ShowType v
':$$: 'GL.Text " is outside of "
':$$: 'GL.ShowType m
':<>: 'GL.Text " and "
':<>: 'GL.ShowType n)
type family FailWhenT (b :: Bool) (msg :: GL.ErrorMessage) :: Constraint where
FailWhenT 'False _ = ()
FailWhenT 'True e = GL.TypeError e
type family FailUnlessT (b :: Bool) (msg :: GL.ErrorMessage) :: Constraint where
FailUnlessT 'True _ = ()
FailUnlessT 'False e = GL.TypeError e
type family AndT (b :: Bool) (b1 :: Bool) :: Bool where
AndT 'False _ = 'False
AndT 'True b1 = b1
type family OrT (b :: Bool) (b1 :: Bool) :: Bool where
OrT 'True _ = 'True
OrT 'False b1 = b1
type family NotT (b :: Bool) :: Bool where
NotT 'True = 'False
NotT 'False = 'True
nat :: forall n a . (KnownNat n, Num a) => a
nat = fromIntegral (GL.natVal (Proxy @n))
symb :: forall s . KnownSymbol s => String
symb = GL.symbolVal (Proxy @s)
class GetNats as where
getNats :: [Int]
instance GetNats '[] where
getNats = []
instance (KnownNat n, GetNats ns) => GetNats (n ': ns) where
getNats = nat @n : getNats @ns
class GetSymbs ns where
getSymbs :: [String]
instance GetSymbs '[] where
getSymbs = []
instance (KnownSymbol s, GetSymbs ss) => GetSymbs (s ': ss) where
getSymbs = symb @s : getSymbs @ss
class GetLen xs where
getLen :: Int
instance GetLen '[] where
getLen = 0
instance GetLen xs => GetLen (x ': xs) where
getLen = 1 + getLen @xs
instance GetLen ('Just a) where
getLen = 1
instance GetLen 'Nothing where
getLen = 0
instance GetLen ('Left a) where
getLen = 0
instance GetLen ('Right a) where
getLen = 1
instance GetLen ('This a) where
getLen = 0
instance GetLen ('That a) where
getLen = 1
instance GetLen ('These a b) where
getLen = 1
instance GetLen xs => GetLen (x ':| xs) where
getLen = 1 + getLen @xs
showThese :: These a b -> String
showThese = \case
This {} -> "This"
That {} -> "That"
These {} -> "These"
class GetThese th where
getThese :: (String, These w v -> Bool)
instance GetThese ('This x) where
getThese = ("This", isThis)
instance GetThese ('That y) where
getThese = ("That", isThat)
instance GetThese ('These x y) where
getThese = ("These", isThese)
class GetOrdering (cmp :: Ordering) where
getOrdering :: Ordering
instance GetOrdering 'LT where
getOrdering = LT
instance GetOrdering 'EQ where
getOrdering = EQ
instance GetOrdering 'GT where
getOrdering = GT
class GetBool (a :: Bool) where
getBool :: Bool
instance GetBool 'True where
getBool = True
instance GetBool 'False where
getBool = False
class GetDisp (a :: Disp) where
getDisp :: Disp
instance GetDisp 'Ansi where
getDisp = Ansi
instance GetDisp 'Unicode where
getDisp = Unicode
class GetDebug (a :: Debug) where
getDebug :: Debug
instance GetDebug 'DZero where
getDebug = DZero
instance GetDebug 'DLite where
getDebug = DLite
instance GetDebug 'DSubNormal where
getDebug = DSubNormal
instance GetDebug 'DNormal where
getDebug = DNormal
instance GetDebug 'DVerbose where
getDebug = DVerbose
class GetColor (a :: Color) where
getColor :: Color
instance GetColor 'Black where
getColor = Black
instance GetColor 'Red where
getColor = Red
instance GetColor 'Green where
getColor = Green
instance GetColor 'Yellow where
getColor = Yellow
instance GetColor 'Blue where
getColor = Blue
instance GetColor 'Magenta where
getColor = Magenta
instance GetColor 'Cyan where
getColor = Cyan
instance GetColor 'White where
getColor = White
instance GetColor 'Default where
getColor = Default
data OrderingP = CGt | CGe | CEq | CLe | CLt | CNe deriving (Show, Eq, Enum, Bounded)
class GetOrd (k :: OrderingP) where
getOrd :: Ord a => (String, a -> a -> Bool)
instance GetOrd 'CGt where getOrd = (">", (>))
instance GetOrd 'CGe where getOrd = (">=",(>=))
instance GetOrd 'CEq where getOrd = ("==",(==))
instance GetOrd 'CLe where getOrd = ("<=",(<=))
instance GetOrd 'CLt where getOrd = ("<", (<))
instance GetOrd 'CNe where getOrd = ("/=",(/=))
toNodeString :: POpts -> PE -> String
toNodeString opts bpe =
if hasNoTree opts
then errorInProgram $ "shouldnt be calling this if we are dropping details: toNodeString " <> show (oDebug opts) <> " " <> show bpe
else colorBoolP opts (_pBool bpe) <> " " <> _pString bpe
hasNoTree :: POpts -> Bool
hasNoTree opts =
case oDebug opts of
DZero -> True
DLite -> True
DSubNormal -> False
DNormal -> False
DVerbose -> False
nullSpace :: String -> String
nullSpace s | null s = ""
| otherwise = " " <> s
colorBoolP :: POpts -> BoolP -> String
colorBoolP o =
\case
b@(FailP e) -> "[" <> colorMe o b "Error" <> nullSpace e <> "]"
b@PresentP -> colorMe o b "P"
b@TrueP -> colorMe o b "True"
b@FalseP -> colorMe o b "False"
colorBoolT :: Show a => POpts -> BoolT a -> String
colorBoolT o r =
let f = colorMe o (r ^. boolT2P)
in case r of
FailT e -> f "Error" <> " " <> e
TrueT -> f "True"
FalseT -> f "False"
PresentT x -> f "Present" <> " " <> show x
colorBoolT' :: Show a => POpts -> BoolT a -> String
colorBoolT' o r =
let f = colorMe o (r ^. boolT2P)
in case r of
FailT e -> f "FailT" <> " " <> e
TrueT -> f "TrueT"
FalseT -> f "FalseT"
PresentT x -> f "PresentT" <> " " <> show x
colorMe :: POpts -> BoolP -> String -> String
colorMe o b s =
let (_, PColor f) = if oNoColor o then nocolor else oColor o
in f b s
fixLite :: forall a . Show a => POpts -> a -> Tree PE -> String
fixLite opts a t
| hasNoTree opts = fixPresentP opts (t ^. root . pBool) a <> "\n"
| otherwise = prtTreePure opts t
fixPresentP :: Show a => POpts -> BoolP -> a -> String
fixPresentP opts bp a =
case bp of
PresentP -> colorMe opts PresentP "Present" <> " " <> show a
_ -> colorBoolP opts bp
prtTreePure :: POpts -> Tree PE -> String
prtTreePure opts t
| hasNoTree opts = colorBoolP opts (t ^. root . pBool)
| otherwise = showImpl opts $ fmap (toNodeString opts) t
topMessage :: TT a -> String
topMessage pp =
let s = pp ^. tString
in if null s then "" else "(" <> s <> ")"
showImpl :: POpts -> Tree String -> String
showImpl o =
case oDisp o of
Unicode -> TV.showTree
Ansi -> drawTree
prettyRational :: Rational -> String
prettyRational (numerator &&& denominator -> (n,d)) =
if | n == 0 -> "0"
| d == 1 -> show n
| otherwise -> show n <> " / " <> show d
fixit :: ((Int, x), TT a) -> TT a
fixit ((i, _), t) = prefixMsg ("i=" <> show i <> ":") t
prefixMsg :: String -> TT a -> TT a
prefixMsg msg t =
t & tString %~ (msg <>)
showT :: forall (t :: Type) . Typeable t => String
showT = show (typeRep (Proxy @t))
prettyOrd :: Ordering -> String
prettyOrd = \case
LT -> "<"
EQ -> "="
GT -> ">"
type family RepeatT (n :: Nat) (p :: k) :: [k] where
RepeatT 0 p = GL.TypeError ('GL.Text "RepeatT is not defined for zero")
RepeatT 1 p = p ': '[]
RepeatT n p = p ': RepeatT (n GN.- 1) p
type s <%> t = GL.AppendSymbol s t
infixr 7 <%>
type family IntersperseT (s :: Symbol) (xs :: [Symbol]) :: Symbol where
IntersperseT s '[] = ""
IntersperseT s '[x] = x
IntersperseT s (x ': y ': xs) = x <%> s <%> IntersperseT s (y ': xs)
type family LenT (xs :: [k]) :: Nat where
LenT '[] = 0
LenT (x ': xs) = 1 GN.+ LenT xs
class InductTupleC x where
type InductTupleP x
inductTupleC :: x -> InductTupleP x
instance (GL.TypeError ('GL.Text "InductTupleC: inductive tuple cannot be empty")) => InductTupleC () where
type InductTupleP () = ()
inductTupleC () = ()
instance InductTupleC (a,b) where
type InductTupleP (a,b) = (b,(a,()))
inductTupleC (a,b) = (b,(a,()))
instance InductTupleC (a,b,c) where
type InductTupleP (a,b,c) = (c,(b,(a,())))
inductTupleC (a,b,c) = (c,(b,(a,())))
instance InductTupleC (a,b,c,d) where
type InductTupleP (a,b,c,d) = (d,(c,(b,(a,()))))
inductTupleC (a,b,c,d) = (d,(c,(b,(a,()))))
instance InductTupleC (a,b,c,d,e) where
type InductTupleP (a,b,c,d,e) = (e,(d,(c,(b,(a,())))))
inductTupleC (a,b,c,d,e) = (e,(d,(c,(b,(a,())))))
instance InductTupleC (a,b,c,d,e,f) where
type InductTupleP (a,b,c,d,e,f) = (f,(e,(d,(c,(b,(a,()))))))
inductTupleC (a,b,c,d,e,f) = (f,(e,(d,(c,(b,(a,()))))))
instance InductTupleC (a,b,c,d,e,f,g) where
type InductTupleP (a,b,c,d,e,f,g) = (g,(f,(e,(d,(c,(b,(a,())))))))
inductTupleC (a,b,c,d,e,f,g) = (g,(f,(e,(d,(c,(b,(a,())))))))
instance InductTupleC (a,b,c,d,e,f,g,h) where
type InductTupleP (a,b,c,d,e,f,g,h) = (h,(g,(f,(e,(d,(c,(b,(a,()))))))))
inductTupleC (a,b,c,d,e,f,g,h) = (h,(g,(f,(e,(d,(c,(b,(a,()))))))))
instance InductTupleC (a,b,c,d,e,f,g,h,i) where
type InductTupleP (a,b,c,d,e,f,g,h,i) = (i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))
inductTupleC (a,b,c,d,e,f,g,h,i) = (i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))
instance InductTupleC (a,b,c,d,e,f,g,h,i,j) where
type InductTupleP (a,b,c,d,e,f,g,h,i,j) = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))
inductTupleC (a,b,c,d,e,f,g,h,i,j) = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))
instance InductTupleC (a,b,c,d,e,f,g,h,i,j,k) where
type InductTupleP (a,b,c,d,e,f,g,h,i,j,k) = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))
inductTupleC (a,b,c,d,e,f,g,h,i,j,k) = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))
instance InductTupleC (a,b,c,d,e,f,g,h,i,j,k,l) where
type InductTupleP (a,b,c,d,e,f,g,h,i,j,k,l) = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))))
inductTupleC (a,b,c,d,e,f,g,h,i,j,k,l) = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))))
class InductListC (n :: Nat) a where
type InductListP n a
inductListC :: [a] -> InductListP n a
instance (GL.TypeError ('GL.Text "InductListC: inductive tuple cannot be empty")) => InductListC 0 a where
type InductListP 0 a = ()
inductListC _ = errorInProgram "InductListC 0: shouldnt be called"
instance InductListC 1 a where
type InductListP 1 a = (a,())
inductListC [a] = (a,())
inductListC _ = errorInProgram "inductListC: expected 1 value"
instance InductListC 2 a where
type InductListP 2 a = (a,(a,()))
inductListC [a,b] = (b,(a,()))
inductListC _ = errorInProgram "inductListC: expected 2 values"
instance InductListC 3 a where
type InductListP 3 a = (a,(a,(a,())))
inductListC [a,b,c] = (c,(b,(a,())))
inductListC _ = errorInProgram "inductListC: expected 3 values"
instance InductListC 4 a where
type InductListP 4 a = (a,(a,(a,(a,()))))
inductListC [a,b,c,d] = (d,(c,(b,(a,()))))
inductListC _ = errorInProgram "inductListC: expected 4 values"
instance InductListC 5 a where
type InductListP 5 a = (a,(a,(a,(a,(a,())))))
inductListC [a,b,c,d,e] = (e,(d,(c,(b,(a,())))))
inductListC _ = errorInProgram "inductListC: expected 5 values"
instance InductListC 6 a where
type InductListP 6 a = (a,(a,(a,(a,(a,(a,()))))))
inductListC [a,b,c,d,e,f] = (f,(e,(d,(c,(b,(a,()))))))
inductListC _ = errorInProgram "inductListC: expected 6 values"
instance InductListC 7 a where
type InductListP 7 a = (a,(a,(a,(a,(a,(a,(a,())))))))
inductListC [a,b,c,d,e,f,g] = (g,(f,(e,(d,(c,(b,(a,())))))))
inductListC _ = errorInProgram "inductListC: expected 7 values"
instance InductListC 8 a where
type InductListP 8 a = (a,(a,(a,(a,(a,(a,(a,(a,()))))))))
inductListC [a,b,c,d,e,f,g,h] = (h,(g,(f,(e,(d,(c,(b,(a,()))))))))
inductListC _ = errorInProgram "inductListC: expected 8 values"
instance InductListC 9 a where
type InductListP 9 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,())))))))))
inductListC [a,b,c,d,e,f,g,h,i] = (i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))
inductListC _ = errorInProgram "inductListC: expected 9 values"
instance InductListC 10 a where
type InductListP 10 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,()))))))))))
inductListC [a,b,c,d,e,f,g,h,i,j] = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))
inductListC _ = errorInProgram "inductListC: expected 10 values"
instance InductListC 11 a where
type InductListP 11 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,())))))))))))
inductListC [a,b,c,d,e,f,g,h,i,j,k] = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))
inductListC _ = errorInProgram "inductListC: expected 11 values"
instance InductListC 12 a where
type InductListP 12 a = (a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,(a,()))))))))))))
inductListC [a,b,c,d,e,f,g,h,i,j,k,l] = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))))
inductListC _ = errorInProgram "inductListC: expected 12 values"
type family (p :: k -> k1) %% (q :: k) :: k1 where
p %% q = p q
infixl 9 %%
type family (p :: k) %& (q :: k -> k1) :: k1 where
p %& q = q p
infixr 9 %&
type family FlipT (d :: k1 -> k -> k2) (p :: k) (q :: k1) :: k2 where
FlipT d p q = d q p
type family IfT (b :: Bool) (t :: k) (f :: k) :: k where
IfT 'True t f = t
IfT 'False t f = f
type family SumT (ns :: [Nat]) :: Nat where
SumT '[] = 0
SumT (n ': ns) = n GL.+ SumT ns
type family MapT (f :: k -> k1) (xs :: [k]) :: [k1] where
MapT f '[] = '[]
MapT f (x ': xs) = f x ': MapT f xs
type family ConsT s where
ConsT [a] = a
ConsT (ZipList a) = a
ConsT T.Text = Char
ConsT ByteString = Word8
ConsT (Seq a) = a
ConsT s = GL.TypeError (
'GL.Text "invalid ConsT instance"
':$$: 'GL.Text "s = "
':<>: 'GL.ShowType s)
class Monad m => MonadEval m where
runIO :: IO a -> m (Maybe a)
catchit :: E.Exception e => a -> m (Either String a)
catchitNF :: (E.Exception e, NFData a) => a -> m (Either String a)
liftEval :: m a -> IO a
instance MonadEval Identity where
runIO _ = Identity Nothing
catchit v = Identity $ unsafePerformIO $ catchit @IO @E.SomeException v
catchitNF v = Identity $ unsafePerformIO $ catchitNF @IO @E.SomeException v
liftEval = return . runIdentity
instance MonadEval IO where
runIO ioa = Just <$> ioa
catchit v = E.evaluate (Right $! v) `E.catch` (\(E.SomeException e) -> pure $ Left ("IO e=" <> show e))
catchitNF v = E.evaluate (Right $!! v) `E.catch` (\(E.SomeException e) -> pure $ Left ("IO e=" <> show e))
liftEval = id
removeAnsi :: Show a => Either String a -> IO ()
removeAnsi = putStrLn . removeAnsiImpl
removeAnsiImpl :: Show a => Either String a -> String
removeAnsiImpl =
\case
Left e -> let esc = '\x1b'
f :: String -> Maybe (String, String)
f = \case
[] -> Nothing
c:cs | c == esc -> case break (=='m') cs of
(_,'m':s) -> Just ("",s)
_ -> Nothing
| otherwise -> Just $ break (==esc) (c:cs)
in concat $ unfoldr f e
Right a -> show a
errorInProgram :: HasCallStack => String -> x
errorInProgram s = error $ "programmer error:" <> s
readField :: String -> ReadPrec a -> ReadPrec a
readField fieldName readVal = do
GR.expectP (L.Ident fieldName)
GR.expectP (L.Punc "=")
readVal
data OptT =
ODebug !Debug
| OWidth !Nat
| OMsg !Symbol
| ORecursion !Nat
| OOther
!Bool
!Color
!Color
| OEmpty
| !OptT :# !OptT
| OColor
!Symbol
!Color
!Color
!Color
!Color
!Color
!Color
!Color
!Color
| ONoColor !Bool
| ODisp !Disp
| OZ
| OL
| OAN
| OA
| OAB
| OU
| OUB
instance Show OptT where
show = \case
ODebug _n -> "ODebug"
OWidth _n -> "OWidth"
OMsg _s -> "OMsg"
ORecursion _n -> "ORecursion"
OOther _b _c1 _c2 -> "OOther"
OEmpty -> "OEmpty"
a :# b -> show a ++ " ':# " ++ show b
OColor _s _c1 _c2 _c3 _c4 _c5 _c6 _c7 _c8 -> "OColor"
ONoColor b -> "ONoColor " ++ show b
ODisp b -> "ODisp " ++ show b
OZ -> "OZ"
OL -> "OL"
OAN -> "OAN"
OA -> "OA"
OAB -> "OAB"
OU -> "OU"
OUB -> "OUB"
infixr 6 :#
class OptTC (k :: OptT) where
getOptT' :: POptsL
instance GetDebug n => OptTC ('ODebug n) where
getOptT' = setDebug (getDebug @n)
instance KnownNat n => OptTC ('OWidth n) where
getOptT' = setWidth (nat @n)
instance KnownSymbol s => OptTC ('OMsg s) where
getOptT' = setMessage (symb @s)
instance KnownNat n => OptTC ('ORecursion n) where
getOptT' = setRecursion (nat @n)
instance (GetBool b, GetColor c1, GetColor c2) => OptTC ('OOther b c1 c2) where
getOptT' = setOther (getBool @b) (getColor @c1) (getColor @c2)
instance OptTC 'OEmpty where
getOptT' = mempty
instance (OptTC a, OptTC b) => OptTC (a ':# b) where
getOptT' = getOptT' @a <> getOptT' @b
instance ( KnownSymbol s
, GetColor c1
, GetColor c2
, GetColor c3
, GetColor c4
, GetColor c5
, GetColor c6
, GetColor c7
, GetColor c8)
=> OptTC ('OColor s c1 c2 c3 c4 c5 c6 c7 c8) where
getOptT' = setCreateColor
(symb @s)
(getColor @c1)
(getColor @c2)
(getColor @c3)
(getColor @c4)
(getColor @c5)
(getColor @c6)
(getColor @c7)
(getColor @c8)
instance GetBool b => OptTC ('ONoColor b) where
getOptT' = setNoColor (getBool @b)
instance GetDisp b => OptTC ('ODisp b) where
getOptT' = setDisp (getDisp @b)
instance OptTC 'OZ where
getOptT' = setDisp Ansi <> setNoColor True <> setDebug DZero
instance OptTC 'OL where
getOptT' = setDisp Ansi <> setNoColor True <> setDebug DLite
instance OptTC 'OAN where
getOptT' = setDisp Ansi <> setNoColor True <> setDebug DNormal
instance OptTC 'OA where
getOptT' = setDisp Ansi <> getOptT' @Color5 <> setDebug DNormal <> getOptT' @Other2
instance OptTC 'OAB where
getOptT' = setDisp Ansi <> getOptT' @Color1 <> setDebug DNormal <> getOptT' @Other1
instance OptTC 'OU where
getOptT' = setDisp Unicode <> getOptT' @Color5 <> setDebug DNormal <> getOptT' @Other2
instance OptTC 'OUB where
getOptT' = setDisp Unicode <> getOptT' @Color1 <> setDebug DNormal <> getOptT' @Other1
getOptT :: forall o . OptTC o => POpts
getOptT = reifyOpts (getOptT' @o)
type family T4_1 x where
T4_1 '(a,_,_,_) = a
type family T4_2 x where
T4_2 '(_,b,_,_) = b
type family T4_3 x where
T4_3 '(_,_,c,_) = c
type family T4_4 x where
T4_4 '(_,_,_,d) = d
type family T5_1 x where
T5_1 '(a,_,_,_,_) = a
type family T5_2 x where
T5_2 '(_,b,_,_,_) = b
type family T5_3 x where
T5_3 '(_,_,c,_,_) = c
type family T5_4 x where
T5_4 '(_,_,_,d,_) = d
type family T5_5 x where
T5_5 '(_,_,_,_,e) = e
chkSize :: Foldable t => POpts -> String -> t a -> [Holder] -> Either (TT x) ()
chkSize opts msg0 xs hhs =
let mx = oRecursion opts
in case splitAt mx (toList xs) of
(_,[]) -> Right ()
(_,_:_) -> Left $ mkNode opts (FailT (msg0 <> " list size exceeded")) (msg0 <> " list size exceeded: max is " ++ show mx) hhs
formatOMsg :: POpts -> String -> String
formatOMsg o suffix =
case oMsg o of
[] -> mempty
s@(_:_) -> intercalate " | " (map (setOtherEffects o) s) <> suffix
subopts :: POpts -> POpts
subopts opts =
case oDebug opts of
DZero -> opts { oDebug = DLite }
_ -> opts
setOtherEffects :: POpts -> String -> String
setOtherEffects o =
if oNoColor o then id
else case coerce (oOther o) of
(False, Default, Default) -> id
(b, c1, c2) -> (if b then style Underline else id) . color c1 . bgColor c2
type family AnyT :: k where {}
pureTryTest :: a -> IO (Either () a)
pureTryTest = fmap (left (const ())) . E.try @E.SomeException . E.evaluate
pureTryTestPred :: (String -> Bool) -> a -> IO (Either String (Either () a))
pureTryTestPred p a = do
lr <- left E.displayException <$> E.try @E.SomeException (E.evaluate a)
return $ case lr of
Left e | p e -> Right (Left ())
| otherwise -> Left ("no match found: e=" ++ e)
Right r -> Right (Right r)
isPrime :: Int -> Bool
isPrime n = n==2 || n>2 && all ((> 0).rem n) (2:[3,5 .. floor . sqrt @Double . fromIntegral $ n+1])