{-# 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 TupleSections #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
module Predicate.Util (
TT(..)
, tBool
, tStrings
, tForest
, fixBoolT
, BoolT(..)
, _FailT
, _PresentT
, _FalseT
, _TrueT
, boolT2P
, BoolP
, PE(PE)
, mkNode
, mkNodeB
, mkNodeSkipP
, getValLRFromTT
, getValLR
, fromTT
, getValueLR
, getValueLRHide
, fixLite
, fixit
, prefixMsg
, splitAndAlign
, POpts(..)
, defOpts
, ol
, olc
, o0
, o2
, o2n
, o3
, ou
, oun
, setw
, setd
, setu
, setc
, color0
, color1
, color2
, color3
, color4
, colorMe
, lite
, unicode
, normal
, show01
, lit01
, show01'
, lit01'
, showLit0
, showLit1
, show0
, show3
, show1
, ROpt(..)
, compileRegex
, GetROpts(..)
, RR(..)
, BetweenT
, NullT
, FailIfT
, AndT
, OrT
, NotT
, RepeatT
, IntersperseT
, LenT
, ReverseTupleC(..)
, TupleListT
, TupleListD(..)
, TupleLenT
, FlipT
, IfT
, SumT
, MapT
, ConsT
, type (%%)
, type (%&)
, nat
, symb
, GetNats(..)
, GetSymbs(..)
, getLen
, GetLen(..)
, showThese
, GetThese(..)
, GetOrdering(..)
, GetBool(..)
, ToN
, OrderingP(..)
, GetOrd(..)
, prtTTIO
, prtTT
, prtTree
, prtImpl
, prtTreePure
, prettyRational
, imply
, evalBinStrict
, hh
, showT
, prettyOrd
, removeAnsi
, MonadEval(..)
) 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.Char
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.ByteString.Char8 as B8
import qualified Data.Text as T
import Data.ByteString (ByteString)
import GHC.Word (Word8)
import Data.Sequence (Seq)
import Control.Applicative (ZipList)
import Data.Kind (Type)
import Data.These
import Data.These.Combinators
import qualified Control.Exception as E
import Control.DeepSeq
import System.IO.Unsafe (unsafePerformIO)
import Data.Bool
import Data.Foldable
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as N
data TT a = TT { _tBool :: BoolT a
, _tStrings :: [String]
, _tForest :: Forest PE }
deriving Show
data BoolT a where
FailT :: String -> BoolT a
FalseT :: BoolT Bool
TrueT :: BoolT Bool
PresentT :: a -> BoolT a
deriving instance Show a => Show (BoolT a)
deriving instance Eq a => Eq (BoolT a)
tBool :: Lens (TT a) (TT b) (BoolT a) (BoolT b)
tBool afb s = (\b -> s { _tBool = b }) <$> afb (_tBool s)
tStrings :: Lens' (TT a) [String]
tStrings afb s = (\b -> s { _tStrings = b }) <$> afb (_tStrings 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
, _pStrings :: [String]
} deriving Show
pBool :: Lens' PE BoolP
pBool afb (PE x y) = flip PE y <$> afb x
mkNode :: POpts -> BoolT a -> [String] -> [Holder] -> TT a
mkNode opts bt ss hs
| oLite opts = TT bt [] []
| otherwise = 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"]) []
partitionTTExtended :: (w, TT a) -> ([((w, TT x), String)], [(w, TT a)])
partitionTTExtended z@(_, t) =
case _tBool t of
FailT e -> ([(z & _2 . tBool .~ FailT e, e)], [])
_ -> ([], [z])
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 then (if null msg0 then "" else " ") <> "[" <> e <> "]"
else ""]
tt'
)
(getValLRFromTT tt)
newtype PColor = PColor (BoolP -> String -> String)
data POpts = POpts { oWidth :: Int
, oDebug :: !Int
, oDisp :: Disp
, oHide :: !Int
, oColor :: !(String, PColor)
, oLite :: !Bool
}
data Disp = NormalDisp
| Unicode
deriving (Show, Eq)
instance Show POpts where
show opts =
"POpts: showA=" <> show (oWidth opts)
<> " debug=" <> show (oDebug opts)
<> " disp=" <> show (oDisp opts)
<> " hide=" <> show (oHide opts)
<> " color=" <> show (fst (oColor opts))
<> " lite=" <> show (oLite opts)
defOpts :: POpts
defOpts = POpts
{ oWidth = 200
, oDebug = 2
, oDisp = NormalDisp
, oHide = 0
, oColor = color1
, oLite = False
}
ol :: POpts
ol = defOpts { oColor = color0, oLite = True }
olc :: POpts
olc = ol { oColor = color1 }
o0 :: POpts
o0 = defOpts { oColor = color0 }
o2 :: POpts
o2 = defOpts { oDebug = 2 }
o2n :: POpts
o2n = o2 { oWidth = 120 }
o3 :: POpts
o3 = defOpts { oDebug = 3, oWidth = 400 }
ou :: POpts
ou = defOpts { oDisp = Unicode }
oun :: POpts
oun = ou { oWidth = 120 }
setw :: Int -> POpts -> POpts
setw w o = o { oWidth = w }
setd :: Int -> POpts -> POpts
setd v o = o { oDebug = v }
setu :: POpts -> POpts
setu o = o { oDisp = Unicode }
setc :: (String, PColor) -> POpts -> POpts
setc pc o = o { oColor = pc }
color0, color1, color2, color3, color4 :: (String, PColor)
color0 = ("color0", PColor $ flip const)
color1 =
("color1",) $ PColor $ \case
FailP {} -> bgColor Magenta
FalseP -> bgColor Red
TrueP -> bgColor Green
PresentP -> bgColor Yellow
color2 =
("color2",) $ PColor $ \case
FailP {} -> bgColor Magenta
FalseP -> bgColor Red
TrueP -> bgColor White
PresentP -> bgColor Yellow
color3 =
("color3",) $ PColor $ \case
FailP {} -> bgColor Blue
FalseP -> color Red
TrueP -> color White
PresentP -> bgColor Yellow
color4 =
("color4",) $ PColor $ \case
FailP {} -> bgColor Cyan
FalseP -> color Red
TrueP -> color Green
PresentP -> bgColor Yellow
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 as = lit01 opts msg0 ret (show as)
lit01 :: Show a1 => POpts -> String -> a1 -> String -> String
lit01 opts msg0 ret as = lit01' opts msg0 ret "" as
show01' :: (Show a1, Show a2) => POpts -> String -> a1 -> String -> a2 -> String
show01' opts msg0 ret fmt as = lit01' opts msg0 ret fmt (show as)
lit01' :: Show a1 => POpts -> String -> a1 -> String -> String -> String
lit01' opts msg0 ret fmt as = msg0 <> show0 opts " " ret <> showLit1 opts (" | " ++ fmt) as
showLit0 :: POpts -> String -> String -> String
showLit0 o s a = showLitImpl o 0 s a
showLit1 :: POpts -> String -> String -> String
showLit1 o s a = showLitImpl o 1 s a
showLitImpl :: POpts -> Int -> String -> String -> String
showLitImpl o i s a =
if oDebug o >= i then
let f n = let ss = take n a
in ss <> (if length ss==n then " ..." else "")
in s <> f (oWidth o)
else ""
show0 :: Show a => POpts -> String -> a -> String
show0 o s a = showAImpl o 0 s a
show3 :: Show a => POpts -> String -> a -> String
show3 o s a = showAImpl o 3 s a
show1 :: Show a => POpts -> String -> a -> String
show1 o s a = showAImpl o 1 s a
showAImpl :: Show a => POpts -> Int -> String -> a -> String
showAImpl o i s a = showLitImpl o i s (show a)
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 =
let rs = getROpts @rs
mm = nm <> " " <> show rs
in flip left (RH.compileM (B8.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 RR =
RR String
| RR1 (String -> [String] -> String)
| RR2 (String -> String)
| RR3 ([String] -> String)
instance Show RR where
show = \case
RR s -> "RR " ++ s
RR1 {} -> "RR1 <fn>"
RR2 {} -> "RR2 <fn>"
RR3 {} -> "RR3 <fn>"
splitAndAlign :: Show x =>
POpts
-> [String]
-> [((Int, x), TT a)]
-> Either (TT w)
([a]
,[((Int, x), TT a)]
)
splitAndAlign opts msgs ts =
case mconcat $ map partitionTTExtended ts of
(excs@(e:_), _) ->
Left $ mkNode opts
(FailT (groupErrors (map snd excs)))
(msgs <> ["excs=" <> show (length excs) <> " " <> formatList opts [fst e]])
(map (hh . snd) ts)
([], tfs) -> Right (valsFromTTs (map snd ts), tfs)
formatList :: forall x z . Show x => POpts -> [((Int, x), z)] -> String
formatList opts = unwords . map (\((i, a), _) -> "(i=" <> show i <> showAImpl opts 0 ", a=" a <> ")")
valsFromTTs :: [TT a] -> [a]
valsFromTTs = concatMap toList
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
groupErrors :: [String] -> String
groupErrors =
intercalate " | "
. map (\xs@(x :| _) -> x <> (if length xs > 1 then "(" <> show (length xs) <> ")" else ""))
. N.group
_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
imply :: Bool -> Bool -> Bool
imply p q = not p || q
evalBinStrict :: POpts
-> String
-> (Bool -> Bool -> Bool)
-> TT Bool
-> TT Bool
-> TT Bool
evalBinStrict opts s fn ll rr =
case getValueLR opts (s <> " p") ll [Holder rr] of
Left e -> e
Right a ->
case getValueLR opts (s <> " q") rr [hh ll] of
Left e -> e
Right b ->
let z = fn a b
in mkNodeB opts z [show a <> " " <> s <> " " <> show b] [hh ll, hh rr]
type family BetweenT (a :: Nat) (b :: Nat) (v :: Nat) :: Constraint where
BetweenT m n v =
FailIfT (NotT (AndT (m GL.<=? v) (v GL.<=? n)))
((m GL.<=? v) ~ 'True, (v GL.<=? n) ~ 'True)
('GL.Text "BetweenT failure"
':$$: 'GL.ShowType v
':$$: 'GL.Text " is outside of "
':$$: 'GL.ShowType m
':<>: 'GL.Text " and "
':<>: 'GL.ShowType n)
type family NullT (x :: Symbol) :: Bool where
NullT ("" :: Symbol) = 'True
NullT _ = 'False
type family FailIfT (b :: Bool) (c :: Constraint) (msg :: GL.ErrorMessage) :: Constraint where
FailIfT 'False c _ = c
FailIfT 'True _ 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
getLen :: forall xs . GetLen xs => Int
getLen = getLenP (Proxy @xs)
class GetLen (xs :: [k]) where
getLenP :: Proxy (xs :: [k]) -> Int
instance GetLen '[] where
getLenP _ = 0
instance GetLen xs => GetLen (x ': xs) where
getLenP _ = 1 + getLenP (Proxy @xs)
showThese :: These a b -> String
showThese = these (const "This") (const "That") (const (const "These"))
class GetThese (th :: These x y) where
getThese :: Proxy th -> (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
data N = S N | Z
type family ToN (n :: Nat) :: N where
ToN 0 = 'Z
ToN n = 'S (ToN (n GL.- 1))
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
| oLite opts = error $ "shouldnt be calling this if we are going lite: toNodeString oLite " ++ show bpe
| otherwise = showBoolP opts (_pBool bpe) <> " " <> displayMessages (_pStrings bpe)
nullSpace :: String -> String
nullSpace s | null s = ""
| otherwise = " " <> s
showBoolP :: POpts -> BoolP -> String
showBoolP 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"
displayMessages :: [String] -> String
displayMessages es =
case filter (not . all isSpace) es of
[] -> ""
z -> intercalate " | " z
colorMe :: POpts -> BoolP -> String -> String
colorMe o b s =
let (_, PColor f) = oColor o
in f b s
prtTTIO :: POpts -> IO (TT a) -> IO ()
prtTTIO = prtTT'
prtTT :: POpts -> Identity (TT a) -> IO ()
prtTT = prtTT'
prtTT' :: MonadEval m => POpts -> m (TT a) -> IO ()
prtTT' o y = liftEval y >>= prtTree o . fromTT
prtTree :: POpts -> Tree PE -> IO ()
prtTree o = prtImpl o . fmap (toNodeString o)
prtImpl :: POpts -> Tree String -> IO ()
prtImpl = (putStr .) . showImpl
fixLite :: forall a . Show a => POpts -> a -> Tree PE -> String
fixLite opts a t
| oLite 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
_ -> showBoolP opts bp
prtTreePure :: POpts -> Tree PE -> String
prtTreePure opts t
| oLite opts = showBoolP opts (t ^. root . pBool)
| otherwise = showImpl opts $ fmap (toNodeString opts) t
showImpl :: POpts -> Tree String -> String
showImpl o =
case oDisp o of
Unicode -> TV.showTree
NormalDisp -> drawTree
lite :: POpts -> POpts
lite o = o { oLite = True }
unicode :: POpts -> POpts
unicode o = o { oDisp = Unicode }
normal :: POpts -> POpts
normal o = o { oDisp = NormalDisp }
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 & tStrings . ix 0 %~ (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 family IntersperseT (s :: Symbol) (xs :: [Symbol]) :: Symbol where
IntersperseT s '[] = ""
IntersperseT s '[x] = x
IntersperseT s (x ': y ': xs) = x `GL.AppendSymbol` s `GL.AppendSymbol` IntersperseT s (y ': xs)
type family LenT (xs :: [k]) :: Nat where
LenT '[] = 0
LenT (x ': xs) = 1 GN.+ LenT xs
type family TupleListT (n :: N) a where
TupleListT 'Z a = ()
TupleListT ('S n) a = (a, TupleListT n a)
class TupleListD (n :: N) a where
tupleListD :: Bool -> [a] -> Either String (TupleListT n a)
instance TupleListD 'Z a where
tupleListD isStrict = \case
z@(_:_) | isStrict ->
let len = length z
in Left $ "is strict and has " <> show len <> " extra element" <> (if len == 1 then "" else "s")
_ -> Right ()
instance (TupleListD n a) => TupleListD ('S n) a where
tupleListD isStrict = \case
[] -> Left "no data left"
a:as -> (a,) <$> tupleListD @n @a isStrict as
class ReverseTupleC x where
type ReverseTupleP x
reverseTupleC :: x -> ReverseTupleP x
instance (GL.TypeError ('GL.Text "ReverseTupleC: inductive tuple cannot be empty")) => ReverseTupleC () where
type ReverseTupleP () = ()
reverseTupleC () = ()
instance ReverseTupleC (a,()) where
type ReverseTupleP (a,()) = (a,())
reverseTupleC (a,()) = (a,())
instance ReverseTupleC (a,(b,())) where
type ReverseTupleP (a,(b,())) = (b,(a,()))
reverseTupleC (a,(b,())) = (b,(a,()))
instance ReverseTupleC (a,(b,(c,()))) where
type ReverseTupleP (a,(b,(c,()))) = (c,(b,(a,())))
reverseTupleC (a,(b,(c,()))) = (c,(b,(a,())))
instance ReverseTupleC (a,(b,(c,(d,())))) where
type ReverseTupleP (a,(b,(c,(d,())))) = (d,(c,(b,(a,()))))
reverseTupleC (a,(b,(c,(d,())))) = (d,(c,(b,(a,()))))
instance ReverseTupleC (a,(b,(c,(d,(e,()))))) where
type ReverseTupleP (a,(b,(c,(d,(e,()))))) = (e,(d,(c,(b,(a,())))))
reverseTupleC (a,(b,(c,(d,(e,()))))) = (e,(d,(c,(b,(a,())))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,())))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,())))))) = (f,(e,(d,(c,(b,(a,()))))))
reverseTupleC (a,(b,(c,(d,(e,(f,())))))) = (f,(e,(d,(c,(b,(a,()))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,()))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,()))))))) = (g,(f,(e,(d,(c,(b,(a,())))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,()))))))) = (g,(f,(e,(d,(c,(b,(a,())))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,())))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,(h,())))))))) = (h,(g,(f,(e,(d,(c,(b,(a,()))))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,())))))))) = (h,(g,(f,(e,(d,(c,(b,(a,()))))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,()))))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,(h,(i,()))))))))) = (i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,()))))))))) = (i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,())))))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,())))))))))) = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,())))))))))) = (j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,()))))))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,()))))))))))) = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,()))))))))))) = (k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,())))))))))))
instance ReverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,(l,())))))))))))) where
type ReverseTupleP (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,(l,())))))))))))) = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))))
reverseTupleC (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,(l,())))))))))))) = (l,(k,(j,(i,(h,(g,(f,(e,(d,(c,(b,(a,()))))))))))))
type family TupleLenT (t :: Type) :: Nat where
TupleLenT () = 0
TupleLenT (_,ts) = 1 GN.+ TupleLenT ts
TupleLenT t = GL.TypeError (
'GL.Text "TupleLenT: expected a valid inductive tuple"
':$$: 'GL.Text "t = "
':<>: 'GL.ShowType t)
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 =
\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 putStrLn $ concat $ unfoldr f e
Right a -> print a