{-# 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 TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE NoOverloadedLists #-}
module Predicate.Prelude (
type (&&)
, type (||)
, type (~>)
, Not
, Ands
, Ors
, Asc
, Asc'
, Desc
, Desc'
, Between
, type (<..>)
, Between'
, All
, Any
, AllPositive
, Positive
, AllNegative
, Negative
, Re
, Re'
, Rescan
, Rescan'
, RescanRanges
, RescanRanges'
, Resplit
, Resplit'
, ReplaceAll
, ReplaceAll'
, ReplaceOne
, ReplaceOne'
, ReplaceAllString
, ReplaceAllString'
, ReplaceOneString
, ReplaceOneString'
, MakeRR
, MakeRR1
, MakeRR2
, MakeRR3
, Fst
, Snd
, Thd
, L1
, L2
, L3
, L4
, L5
, L6
, Dup
, Swap
, Assoc
, Unassoc
, Pairs
, IsLower
, IsUpper
, IsNumber
, IsSpace
, IsPunctuation
, IsControl
, IsHexDigit
, IsOctDigit
, IsSeparator
, IsLatin1
, FormatTimeP
, ParseTimeP
, ParseTimeP'
, ParseTimes
, ParseTimes'
, MkDay
, MkDay'
, UnMkDay
, type (+)
, type (-)
, type (*)
, type (/)
, Negate
, Abs
, Signum
, FromInteger
, FromInteger'
, FromIntegral
, FromIntegral'
, Truncate
, Truncate'
, Ceiling
, Ceiling'
, Floor
, Floor'
, Even
, Odd
, Div
, Mod
, DivMod
, QuotRem
, Quot
, Rem
, type (%)
, type (%-)
, type (-%)
, ToRational
, FromRational
, FromRational'
, MkProxy
, ProxyT
, ProxyT'
, Unproxy
, ShowP
, ReadP
, ReadP'
, ReadQ
, ReadQ'
, ReadMaybe
, ReadMaybe'
, ReadBase
, ReadBase'
, ReadBaseInt
, ShowBase
, type (&&&)
, type (***)
, First
, Second
, type (|||)
, type (+++)
, type (>)
, type (>=)
, type (==)
, type (/=)
, type (<=)
, type (<)
, type (>~)
, type (>=~)
, type (==~)
, type (/=~)
, type (<=~)
, type (<~)
, Gt
, Ge
, Same
, Le
, Lt
, Ne
, OrdP
, type (==!)
, OrdA'
, OrdA
, OrdI
, type (===~)
, Cmp
, CmpI
, Succ
, Pred
, FromEnum
, ToEnum
, ToEnum'
, EnumFromTo
, SuccB
, SuccB'
, PredB
, PredB'
, ToEnumBDef
, ToEnumBDef'
, ToEnumBFail
, Unwrap
, Wrap
, Wrap'
, Coerce
, Coerce2
, Map
, Concat
, ConcatMap
, Partition
, Filter
, Break
, Span
, Intercalate
, Elem
, Inits
, Tails
, Ones
, OneP
, Len
, Length
, PadL
, PadR
, Cycle
, SplitAts
, SplitAt
, Take
, Drop
, Min
, Max
, Sum
, IsEmpty
, Null
, ToList
, ToList'
, IToList
, IToList'
, FromList
, EmptyList
, EmptyList'
, Singleton
, Reverse
, ReverseL
, SortBy
, SortOn
, SortOnDesc
, Remove
, Keep
, ToListExt
, FromListExt
, MkNothing
, MkNothing'
, MkJust
, IsNothing
, IsJust
, MapMaybe
, CatMaybes
, Just
, JustDef
, JustFail
, MaybeIn
, MaybeBool
, PartitionEithers
, IsLeft
, IsRight
, MkLeft
, MkLeft'
, MkRight
, MkRight'
, Left'
, Right'
, LeftDef
, LeftFail
, RightDef
, RightFail
, EitherBool
, MkRightAlt
, MkLeftAlt
, EitherIn
, type (<>)
, MConcat
, STimes
, Sapa
, Sapa'
, MEmptyT
, MEmptyT'
, MEmptyP
, MEmptyT2
, MEmptyT2'
, Ix
, Ix'
, IxL
, type (!!)
, Lookup
, LookupDef
, LookupDef'
, LookupFail
, LookupFail'
, type (:+)
, type (+:)
, Uncons
, Unsnoc
, Head
, Tail
, Init
, Last
, HeadDef
, HeadFail
, TailDef
, TailFail
, LastDef
, LastFail
, InitDef
, InitFail
, PartitionThese
, Thiss
, Thats
, Theses
, This'
, That'
, These'
, IsThis
, IsThat
, IsThese
, MkThis
, MkThis'
, MkThat
, MkThat'
, MkThese
, ThisDef
, ThisFail
, ThatDef
, ThatFail
, TheseDef
, TheseFail
, TheseIn
, TheseId
, TheseX
, Scanl
, ScanN
, ScanNA
, FoldN
, Foldl
, Unfoldr
, IterateN
, IterateUntil
, IterateWhile
, IterateNWhile
, IterateNUntil
, Fail
, Failp
, Failt
, FailS
, Catch
, Catch'
, ZipThese
, ZipL
, ZipR
, Zip
, Unzip
, Unzip3
, If
, Case
, Case'
, Case''
, Guards
, GuardsQuick
, Guard
, ExitWhen
, GuardSimple
, GuardsN
, GuardsDetail
, Bools
, BoolsQuick
, BoolsN
, ReadFile
, FileExists
, ReadDir
, DirExists
, ReadEnv
, ReadEnvAll
, TimeUtc
, TimeZt
, AppendFile
, WriteFile
, WriteFile'
, Stdout
, Stderr
, Stdin
, ToLower
, ToUpper
, Trim
, TrimStart
, TrimEnd
, StripLR
, StripRight
, StripLeft
, IsPrefix
, IsInfix
, IsSuffix
, IsPrefixI
, IsInfixI
, IsSuffixI
, FromStringP
, FromStringP'
, PrintF
, PrintL
, PrintT
, Pure
, Pure2
, FoldMap
, type (<$)
, type (<*)
, type (*>)
, FMapFst
, FMapSnd
, Sequence
, Traverse
, Join
, EmptyT
, type (<|>)
, Extract
, Duplicate
, type ($)
, type (&)
, Do
, type (>>)
, type (<<)
, type (>>>)
, DoN
, Para
, ParaN
, Repeat
, Prime
, Luhn
, Char1
, Hide
, Hole
, Skip
, type (|>)
, type (>|)
, type (>|>)
) where
import Predicate.Core
import Predicate.Util
import Safe (succMay, predMay, toEnumMay)
import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat,ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Control.Lens hiding (iall)
import Data.List
import qualified Data.Text.Lens as TL
import Data.Proxy
import Control.Applicative
import Data.Typeable
import Control.Monad.Except
import qualified Control.Exception as E
import Data.Kind (Type)
import qualified Text.Regex.PCRE.Heavy as RH
import Data.String
import Data.Foldable
import Data.Maybe
import Control.Arrow
import qualified Data.Semigroup as SG
import Numeric
import Data.Char
import Data.Function
import Data.These (These(..), partitionThese)
import qualified Data.Bifunctor.Swap as SW (Swap(..))
import qualified Data.Bifunctor.Assoc as AS (Assoc(..))
import Data.Ratio
import Data.Time
import Data.Coerce
import Data.Void
import qualified Data.Sequence as Seq
import Text.Printf
import System.Directory
import Control.Comonad
import System.IO
import System.Environment
import qualified GHC.Exts as GE
import Data.Bool
import Data.Either
import qualified Data.Type.Equality as DE
import Data.Time.Calendar.WeekDate
type Asc = All (Fst Id <= Snd Id) Pairs
type Asc' = All (Fst Id < Snd Id) Pairs
type Desc = All (Fst Id >= Snd Id) Pairs
type Desc' = All (Fst Id > Snd Id) Pairs
data Between' p q r
type Between p q = Between' p q Id
type p <..> q = Between p q
infix 4 <..>
instance (Ord (PP p x)
, Show (PP p x)
, PP r x ~ PP p x
, PP r x ~ PP q x
, P p x
, P q x
, P r x
) => P (Between' p q r) x where
type PP (Between' p q r) x = Bool
eval _ opts x = do
let msg0 = "Between"
rr <- eval (Proxy @r) opts x
case getValueLR opts msg0 rr [] of
Left e -> pure e
Right r -> do
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x [hh rr]
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh rr, hh pp, hh qq]
in if p <= r && r <= q then mkNodeB opts True [show p <> " <= " <> show r <> " <= " <> show q] hhs
else if p > r then mkNodeB opts False [show p <> " <= " <> show r] hhs
else mkNodeB opts False [show r <> " <= " <> show q] hhs
data All p q
instance (P p a
, PP p a ~ Bool
, PP q x ~ f a
, P q x
, Show a
, Foldable f
) => P (All p q) x where
type PP (All p q) x = Bool
eval _ opts x = do
let msg0 = "All"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts [msg0] ts of
Left e -> e
Right (vals, ixtts) ->
let hhs = hh qq : map (hh . fixit) ts
in case filter (not . snd) (zip [0..] vals) of
[] -> mkNodeB opts True [msg0 ++ "(" ++ show (length q) ++ ")"] hhs
(i,_):fs -> let (_,tt) = ixtts !! i
in mkNodeB opts False [msg0 <> " i=" ++ showIndex i ++ " " <> topMessage tt ++ " " ++ show (length fs+1) ++ " false"] hhs
chkSize :: Foldable t => POpts -> String -> t a -> [Holder] -> Either (TT x) ()
chkSize opts msg0 xs hhs =
case splitAt _MX (toList xs) of
(_,[]) -> Right ()
(_,_:_) -> Left $ mkNode opts (FailT (msg0 <> " list size exceeded")) [msg0 <> " list size exceeded: max is " ++ show _MX] hhs
showIndex :: (Show i, Num i) => i -> String
showIndex i = show (i+0)
data Any p q
instance (P p a
, PP p a ~ Bool
, PP q x ~ f a
, P q x
, Show a
, Foldable f
) => P (Any p q) x where
type PP (Any p q) x = Bool
eval _ opts x = do
let msg0 = "Any"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts [msg0] ts of
Left e -> e
Right (vals, ixtts) ->
let hhs = hh qq : map (hh . fixit) ts
in case filter snd (zip [0..] vals) of
[] -> mkNodeB opts False [msg0 ++ "(" ++ show (length q) ++ ")"] hhs
(i,_):fs -> let (_,tt) = ixtts !! i
in mkNodeB opts True [msg0 <> " i=" ++ showIndex i ++ " " <> topMessage tt ++ " " ++ show (length fs+1) ++ " false"] hhs
type AllPositive = All Positive Id
type AllNegative = All Negative Id
type Positive = Gt 0
type Negative = Lt 0
type Unzip = '(Map (Fst Id) Id, Map (Snd Id) Id)
type Unzip3 = '(Map (Fst Id) Id, Map (Snd Id) Id, Map (Thd Id) Id)
data Re' (rs :: [ROpt]) p q
type Re p q = Re' '[] p q
instance (GetROpts rs
, PP p x ~ String
, PP q x ~ String
, P p x
, P q x
) => P (Re' rs p q) x where
type PP (Re' rs p q) x = Bool
eval _ opts x = do
let msg0 = "Re" <> (if null rs then "' " <> show rs else "")
rs = getROpts @rs
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case compileRegex @rs opts msg1 p hhs of
Left tta -> tta
Right regex ->
let b = q RH.=~ regex
in mkNodeB opts b [msg1 <> showLit1 opts " | " q] hhs
data Rescan' (rs :: [ROpt]) p q
type Rescan p q = Rescan' '[] p q
instance (GetROpts rs
, PP p x ~ String
, PP q x ~ String
, P p x
, P q x
) => P (Rescan' rs p q) x where
type PP (Rescan' rs p q) x = [(String, [String])]
eval _ opts x = do
let msg0 = "Rescan" <> (if null rs then "' " <> show rs else "")
rs = getROpts @rs
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case compileRegex @rs opts msg1 p hhs of
Left tta -> tta
Right regex ->
case splitAt _MX $ RH.scan regex q of
(b, _:_) -> mkNode opts (FailT "Regex looping") [msg1 <> " Looping? " <> show (take 10 b) <> "..." <> show1 opts " | " q] hhs
([], _) ->
mkNode opts (FailT "Regex no results") [msg1 <> " no match" <> show1 opts " | " q] [hh pp, hh qq]
(b, _) -> mkNode opts (PresentT b) [lit01 opts msg1 b q] [hh pp, hh qq]
data RescanRanges' (rs :: [ROpt]) p q
type RescanRanges p q = RescanRanges' '[] p q
instance (GetROpts rs
, PP p x ~ String
, PP q x ~ String
, P p x
, P q x
) => P (RescanRanges' rs p q) x where
type PP (RescanRanges' rs p q) x = [((Int,Int), [(Int,Int)])]
eval _ opts x = do
let msg0 = "RescanRanges" <> (if null rs then "' " <> show rs else "")
rs = getROpts @rs
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case compileRegex @rs opts msg1 p hhs of
Left tta -> tta
Right regex ->
case splitAt _MX $ RH.scanRanges regex q of
(b, _:_) -> mkNode opts (FailT "Regex looping") [msg1 <> " Looping? " <> show (take 10 b) <> "..." <> show1 opts " | " q] hhs
([], _) ->
mkNode opts (FailT "Regex no results") [msg1 <> " no match" <> show1 opts " | " q] hhs
(b, _) -> mkNode opts (PresentT b) [lit01 opts msg1 b q] hhs
data Resplit' (rs :: [ROpt]) p q
type Resplit p q = Resplit' '[] p q
instance (GetROpts rs
, PP p x ~ String
, PP q x ~ String
, P p x
, P q x
) => P (Resplit' rs p q) x where
type PP (Resplit' rs p q) x = [String]
eval _ opts x = do
let msg0 = "Resplit" <> (if null rs then "' " <> show rs else "")
rs = getROpts @rs
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case compileRegex @rs opts msg1 p hhs of
Left tta -> tta
Right regex ->
case splitAt _MX $ RH.split regex q of
(b, _:_) -> mkNode opts (FailT "Regex looping") [msg1 <> " Looping? " <> show (take 10 b) <> "..." <> show1 opts " | " q] hhs
([], _) ->
mkNode opts (FailT "Regex no results") [msg1 <> " no match" <> show1 opts " | " q] hhs
(b, _) -> mkNode opts (PresentT b) [lit01 opts msg1 b q] hhs
_MX :: Int
_MX = 100
data ReplaceImpl (alle :: Bool) (rs :: [ROpt]) p q r
type ReplaceAll' (rs :: [ROpt]) p q r = ReplaceImpl 'True rs p q r
type ReplaceAll p q r = ReplaceAll' '[] p q r
type ReplaceOne' (rs :: [ROpt]) p q r = ReplaceImpl 'False rs p q r
type ReplaceOne p q r = ReplaceOne' '[] p q r
type ReplaceAllString' (rs :: [ROpt]) p q r = ReplaceAll' rs p (MakeRR q) r
type ReplaceAllString p q r = ReplaceAllString' '[] p q r
type ReplaceOneString' (rs :: [ROpt]) p q r = ReplaceOne' rs p (MakeRR q) r
type ReplaceOneString p q r = ReplaceOneString' '[] p q r
data MakeRR p
instance (PP p x ~ String
, P p x) => P (MakeRR p) x where
type PP (MakeRR p) x = RR
eval _ opts x = do
let msg0 = "MakeRR"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = RR p
in mkNode opts (PresentT b) [msg0 <> show1 opts " | " p] [hh pp]
data MakeRR1 p
instance (PP p x ~ (String -> [String] -> String)
, P p x) => P (MakeRR1 p) x where
type PP (MakeRR1 p) x = RR
eval _ opts x = do
let msg0 = "MakeRR1 (String -> [String] -> String)"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right f -> mkNode opts (PresentT (RR1 f)) [msg0] [hh pp]
data MakeRR2 p
instance (PP p x ~ (String -> String)
, P p x) => P (MakeRR2 p) x where
type PP (MakeRR2 p) x = RR
eval _ opts x = do
let msg0 = "MakeRR2 (String -> String)"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right f -> mkNode opts (PresentT (RR2 f)) [msg0] [hh pp]
data MakeRR3 p
instance (PP p x ~ ([String] -> String)
, P p x) => P (MakeRR3 p) x where
type PP (MakeRR3 p) x = RR
eval _ opts x = do
let msg0 = "MakeRR3 ([String] -> String)"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right f -> mkNode opts (PresentT (RR3 f)) [msg0] [hh pp]
instance (GetBool b
, GetROpts rs
, PP p x ~ String
, PP q x ~ RR
, PP r x ~ String
, P p x
, P q x
, P r x
) => P (ReplaceImpl b rs p q r) x where
type PP (ReplaceImpl b rs p q r) x = String
eval _ opts x = do
let msg0 = "Replace" <> (if alle then "All" else "One") <> (if null rs then "' " <> show rs else "")
rs = getROpts @rs
alle = getBool @b
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
case lr of
Left e -> pure e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case compileRegex @rs opts msg1 p hhs of
Left tta -> pure tta
Right regex -> do
rr <- eval (Proxy @r) opts x
pure $ case getValueLR opts msg0 rr hhs of
Left e -> e
Right r ->
let ret :: String
ret = case q of
RR s -> (if alle then RH.gsub else RH.sub) regex s r
RR1 s -> (if alle then RH.gsub else RH.sub) regex s r
RR2 s -> (if alle then RH.gsub else RH.sub) regex s r
RR3 s -> (if alle then RH.gsub else RH.sub) regex s r
in mkNode opts (PresentT ret) [msg1 <> showLit0 opts " " r <> showLit1 opts " | " ret] (hhs <> [hh rr])
data IsCharSet (cs :: CharSet)
data CharSet = CLower
| CUpper
| CNumber
| CSpace
| CPunctuation
| CControl
| CHexDigit
| COctDigit
| CSeparator
| CLatin1
deriving Show
class GetCharSet (cs :: CharSet) where
getCharSet :: (CharSet, Char -> Bool)
instance GetCharSet 'CLower where
getCharSet = (CLower, isLower)
instance GetCharSet 'CUpper where
getCharSet = (CUpper, isUpper)
instance GetCharSet 'CNumber where
getCharSet = (CNumber, isNumber)
instance GetCharSet 'CPunctuation where
getCharSet = (CPunctuation, isPunctuation)
instance GetCharSet 'CControl where
getCharSet = (CControl, isControl)
instance GetCharSet 'CHexDigit where
getCharSet = (CHexDigit, isHexDigit)
instance GetCharSet 'COctDigit where
getCharSet = (COctDigit, isOctDigit)
instance GetCharSet 'CSeparator where
getCharSet = (CSeparator, isSeparator)
instance GetCharSet 'CLatin1 where
getCharSet = (CLatin1, isLatin1)
type IsLower = IsCharSet 'CLower
type IsUpper = IsCharSet 'CUpper
type IsNumber = IsCharSet 'CNumber
type IsSpace = IsCharSet 'CSpace
type IsPunctuation = IsCharSet 'CPunctuation
type IsControl = IsCharSet 'CControl
type IsHexDigit = IsCharSet 'CHexDigit
type IsOctDigit = IsCharSet 'COctDigit
type IsSeparator = IsCharSet 'CSeparator
type IsLatin1 = IsCharSet 'CLatin1
instance (GetCharSet cs
, Show a
, TL.IsText a
) => P (IsCharSet cs) a where
type PP (IsCharSet cs) a = Bool
eval _ opts as =
let b = allOf TL.text f as
msg0 = "IsCharSet " ++ show cs
(cs,f) = getCharSet @cs
in pure $ mkNodeB opts b [msg0 <> show1 opts " | " as] []
data ToLower
instance (Show a, TL.IsText a) => P ToLower a where
type PP ToLower a = a
eval _ opts as =
let msg0 = "ToLower"
xs = as & TL.text %~ toLower
in pure $ mkNode opts (PresentT xs) [show01 opts msg0 xs as] []
data ToUpper
instance (Show a, TL.IsText a) => P ToUpper a where
type PP ToUpper a = a
eval _ opts as =
let msg0 = "ToUpper"
xs = as & TL.text %~ toUpper
in pure $ mkNode opts (PresentT xs) [show01 opts msg0 xs as] []
data Inits
instance Show a => P Inits [a] where
type PP Inits [a] = [[a]]
eval _ opts as =
let msg0 = "Inits"
xs = inits as
in pure $ mkNode opts (PresentT xs) [show01 opts msg0 xs as] []
data Tails
instance Show a => P Tails [a] where
type PP Tails [a] = [[a]]
eval _ opts as =
let msg0 = "Tails"
xs = tails as
in pure $ mkNode opts (PresentT xs) [show01 opts msg0 xs as] []
data Ones p
instance ( PP p x ~ [a]
, P p x
, Show a
) => P (Ones p) x where
type PP (Ones p) x = [PP p x]
eval _ opts x = do
let msg0 = "Ones"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = map (:[]) p
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data ShowP p
instance (Show (PP p x), P p x) => P (ShowP p) x where
type PP (ShowP p) x = String
eval _ opts x = do
let msg0 = "ShowP"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = show p
in mkNode opts (PresentT d) [msg0 <> showLit0 opts " " d <> show1 opts " | " p] [hh pp]
data FormatTimeP p q
instance (PP p x ~ String
, FormatTime (PP q x)
, P p x
, Show (PP q x)
, P q x
) => P (FormatTimeP p q) x where
type PP (FormatTimeP p q) x = String
eval _ opts x = do
let msg0 = "FormatTimeP"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
b = formatTime defaultTimeLocale p q
in mkNode opts (PresentT b) [msg1 <> showLit0 opts " " b <> show1 opts " | " q] [hh pp, hh qq]
data ParseTimeP' t p q
type ParseTimeP (t :: Type) p q = ParseTimeP' (Hole t) p q
instance (ParseTime (PP t a)
, Typeable (PP t a)
, Show (PP t a)
, P p a
, P q a
, PP p a ~ String
, PP q a ~ String
) => P (ParseTimeP' t p q) a where
type PP (ParseTimeP' t p q) a = PP t a
eval _ opts a = do
let msg0 = "ParseTimeP " <> t
t = showT @(PP t a)
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> " (" <> p <> ")"
hhs = [hh pp, hh qq]
in case parseTimeM @Maybe @(PP t a) True defaultTimeLocale p q of
Just b -> mkNode opts (PresentT b) [lit01' opts msg1 b "fmt=" p <> show1 opts " | " q] hhs
Nothing -> mkNode opts (FailT (msg1 <> " failed to parse")) [msg1 <> " failed"] hhs
data ParseTimes' t p q
type ParseTimes (t :: Type) p q = ParseTimes' (Hole t) p q
instance (ParseTime (PP t a)
, Typeable (PP t a)
, Show (PP t a)
, P p a
, P q a
, PP p a ~ [String]
, PP q a ~ String
) => P (ParseTimes' t p q) a where
type PP (ParseTimes' t p q) a = PP t a
eval _ opts a = do
let msg0 = "ParseTimes " <> t
t = showT @(PP t a)
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0
hhs = [hh pp, hh qq]
zs = map (\d -> (d,) <$> parseTimeM @Maybe @(PP t a) True defaultTimeLocale d q) p
in case catMaybes zs of
[] -> mkNode opts (FailT ("no match on [" ++ q ++ "]")) [msg1 <> " no match"] hhs
(d,b):_ -> mkNode opts (PresentT b) [lit01' opts msg1 b "fmt=" d <> show1 opts " | " q] hhs
data MkDay' p q r
type MkDay = MkDay' (Fst Id) (Snd Id) (Thd Id)
instance (P p x
, P q x
, P r x
, PP p x ~ Int
, PP q x ~ Int
, PP r x ~ Int
) => P (MkDay' p q r) x where
type PP (MkDay' p q r) x = Maybe (Day, Int, Int)
eval _ opts x = do
let msg0 = "MkDay"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs = [hh pp, hh qq]
rr <- eval (Proxy @r) opts x
pure $ case getValueLR opts msg0 rr hhs of
Left e -> e
Right r ->
let mday = fromGregorianValid (fromIntegral p) q r
b = mday <&> \day ->
let (_, week, dow) = toWeekDate day
in (day, week, dow)
in mkNode opts (PresentT b) [show01' opts msg0 b "(y,m,d)=" (p,q,r)] (hhs <> [hh rr])
data UnMkDay p
instance (PP p x ~ Day, P p x) => P (UnMkDay p) x where
type PP (UnMkDay p) x = (Int, Int, Int)
eval _ opts x = do
let msg0 = "UnMkDay"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (fromIntegral -> y, m, d) = toGregorian p
b = (y, m, d)
in mkNode opts (PresentT b) [show01 opts msg0 b p] []
data ReadP' t p
type ReadP (t :: Type) p = ReadP' (Hole t) p
instance (P p x
, PP p x ~ String
, Typeable (PP t x)
, Show (PP t x)
, Read (PP t x)
) => P (ReadP' t p) x where
type PP (ReadP' t p) x = PP t x
eval _ opts x = do
let msg0 = "ReadP " <> t
t = showT @(PP t x)
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right s ->
let msg1 = msg0 <> " (" <> s <> ")"
hhs = [hh pp]
in case reads @(PP t x) s of
[(b,"")] -> mkNode opts (PresentT b) [lit01 opts msg1 b s] hhs
o -> mkNode opts (FailT (msg1 <> " failed")) [msg1 <> " failed " <> show o] hhs
data ReadMaybe' t p
type ReadMaybe (t :: Type) p = ReadMaybe' (Hole t) p
type ReadQ' t p = ReadMaybe' t p >> MaybeIn (Failp "read failed") (Guard "oops" (Snd Id >> Null) >> Fst Id)
type ReadQ (t :: Type) p = ReadQ' (Hole t) p
instance (P p x
, PP p x ~ String
, Typeable (PP t x)
, Show (PP t x)
, Read (PP t x)
) => P (ReadMaybe' t p) x where
type PP (ReadMaybe' t p) x = Maybe (PP t x, String)
eval _ opts x = do
let msg0 = "ReadMaybe " <> t
t = showT @(PP t x)
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right s ->
let msg1 = msg0 <> " (" <> s <> ")"
hhs = [hh pp]
in case reads @(PP t x) s of
[(b,rest)] -> mkNode opts (PresentT (Just (b,rest))) [lit01 opts msg1 b s] hhs
o -> mkNode opts (PresentT Nothing) [msg1 <> " failed " <> show o] hhs
data Sum
instance (Num a, Show a) => P Sum [a] where
type PP Sum [a] = a
eval _ opts as =
let msg0 = "Sum"
v = sum as
in pure $ mkNode opts (PresentT v) [show01 opts msg0 v as] []
data Min
instance (Ord a, Show a) => P Min [a] where
type PP Min [a] = a
eval _ opts as' = do
let msg0 = "Min"
pure $ case as' of
[] -> mkNode opts (FailT "empty list") [msg0 <> "(empty list)"] []
as@(_:_) ->
let v = minimum as
in mkNode opts (PresentT v) [show01 opts msg0 v as] []
data Max
instance (Ord a, Show a) => P Max [a] where
type PP Max [a] = a
eval _ opts as' = do
let msg0 = "Max"
pure $ case as' of
[] -> mkNode opts (FailT "empty list") [msg0 <> "(empty list)"] []
as@(_:_) ->
let v = maximum as
in mkNode opts (PresentT v) [show01 opts msg0 v as] []
data SortBy p q
type SortOn p q = SortBy (OrdA p) q
type SortOnDesc p q = SortBy (Swap >> OrdA p) q
type SortByHelper p = Partition (p == 'GT) Id
instance (P p (a,a)
, P q x
, Show a
, PP q x ~ [a]
, PP p (a,a) ~ Ordering
) => P (SortBy p q) x where
type PP (SortBy p q) x = PP q x
eval _ opts x = do
let msg0 = "SortBy"
qq <- eval (Proxy @q) opts x
case getValueLR opts (msg0 <> " q failed") qq [] of
Left e -> pure e
Right as -> do
let ff :: MonadEval m => [a] -> m (TT [a])
ff = \case
[] -> pure $ mkNode opts (PresentT mempty) [msg0 <> " empty"] []
[w] -> pure $ mkNode opts (PresentT [w]) [msg0 <> " one element " <> show w] []
w:ys@(_:_) -> do
pp <- (if isVerbose opts then
eval (Proxy @(SortByHelper p))
else eval (Proxy @(Hide (SortByHelper p)))) opts (map (w,) ys)
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right (ll', rr') -> do
lhs <- ff (map snd ll')
case getValueLR opts msg0 lhs [] of
Left _ -> pure lhs
Right ll -> do
rhs <- ff (map snd rr')
case getValueLR opts msg0 rhs [] of
Left _ -> pure rhs
Right rr -> do
pure $ mkNode opts (PresentT (ll ++ w : rr))
[msg0 <> show0 opts " lhs=" ll <> " pivot " <> show w <> show0 opts " rhs=" rr]
(hh pp : [hh lhs | length ll > 1] ++ [hh rhs | length rr > 1])
ret <- ff as
pure $ case getValueLR opts msg0 ret [hh qq] of
Left _e -> ret
Right xs -> mkNode opts (_tBool ret) [msg0 <> show0 opts " " xs] [hh qq, hh ret]
data Len
instance (Show a, as ~ [a]) => P Len as where
type PP Len as = Int
eval _ opts as =
let msg0 = "Len"
n = length as
in pure $ mkNode opts (PresentT n) [show01 opts msg0 n as] []
data Length p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t) => P (Length p) x where
type PP (Length p) x = Int
eval _ opts x = do
let msg0 = "Length"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let n = length p
in mkNode opts (PresentT n) [show01 opts msg0 n p] []
data Fst p
type L1 p = Fst p
instance (Show (ExtractL1T (PP p x))
, ExtractL1C (PP p x)
, P p x
, Show (PP p x)
) => P (Fst p) x where
type PP (Fst p) x = ExtractL1T (PP p x)
eval _ opts x = do
let msg0 = "Fst"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL1C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL1C tp where
type ExtractL1T tp
extractL1C :: tp -> ExtractL1T tp
instance ExtractL1C (a,b) where
type ExtractL1T (a,b) = a
extractL1C (a,_) = a
instance ExtractL1C (a,b,c) where
type ExtractL1T (a,b,c) = a
extractL1C (a,_,_) = a
instance ExtractL1C (a,b,c,d) where
type ExtractL1T (a,b,c,d) = a
extractL1C (a,_,_,_) = a
instance ExtractL1C (a,b,c,d,e) where
type ExtractL1T (a,b,c,d,e) = a
extractL1C (a,_,_,_,_) = a
instance ExtractL1C (a,b,c,d,e,f) where
type ExtractL1T (a,b,c,d,e,f) = a
extractL1C (a,_,_,_,_,_) = a
data Snd p
type L2 p = Snd p
instance (Show (ExtractL2T (PP p x))
, ExtractL2C (PP p x)
, P p x
, Show (PP p x)
) => P (Snd p) x where
type PP (Snd p) x = ExtractL2T (PP p x)
eval _ opts x = do
let msg0 = "Snd"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL2C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL2C tp where
type ExtractL2T tp
extractL2C :: tp -> ExtractL2T tp
instance ExtractL2C (a,b) where
type ExtractL2T (a,b) = b
extractL2C (_,b) = b
instance ExtractL2C (a,b,c) where
type ExtractL2T (a,b,c) = b
extractL2C (_,b,_) = b
instance ExtractL2C (a,b,c,d) where
type ExtractL2T (a,b,c,d) = b
extractL2C (_,b,_,_) = b
instance ExtractL2C (a,b,c,d,e) where
type ExtractL2T (a,b,c,d,e) = b
extractL2C (_,b,_,_,_) = b
instance ExtractL2C (a,b,c,d,e,f) where
type ExtractL2T (a,b,c,d,e,f) = b
extractL2C (_,b,_,_,_,_) = b
data Thd p
type L3 p = Thd p
instance (Show (ExtractL3T (PP p x))
, ExtractL3C (PP p x)
, P p x
, Show (PP p x)
) => P (Thd p) x where
type PP (Thd p) x = ExtractL3T (PP p x)
eval _ opts x = do
let msg0 = "Thd"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL3C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL3C tp where
type ExtractL3T tp
extractL3C :: tp -> ExtractL3T tp
instance ExtractL3C (a,b) where
type ExtractL3T (a,b) = GL.TypeError ('GL.Text "Thd doesn't work for 2-tuples")
extractL3C _ = error "Thd doesn't work for 2-tuples"
instance ExtractL3C (a,b,c) where
type ExtractL3T (a,b,c) = c
extractL3C (_,_,c) = c
instance ExtractL3C (a,b,c,d) where
type ExtractL3T (a,b,c,d) = c
extractL3C (_,_,c,_) = c
instance ExtractL3C (a,b,c,d,e) where
type ExtractL3T (a,b,c,d,e) = c
extractL3C (_,_,c,_,_) = c
instance ExtractL3C (a,b,c,d,e,f) where
type ExtractL3T (a,b,c,d,e,f) = c
extractL3C (_,_,c,_,_,_) = c
data L4 p
instance (Show (ExtractL4T (PP p x))
, ExtractL4C (PP p x)
, P p x
, Show (PP p x)
) => P (L4 p) x where
type PP (L4 p) x = ExtractL4T (PP p x)
eval _ opts x = do
let msg0 = "L4"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL4C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL4C tp where
type ExtractL4T tp
extractL4C :: tp -> ExtractL4T tp
instance ExtractL4C (a,b) where
type ExtractL4T (a,b) = GL.TypeError ('GL.Text "L4 doesn't work for 2-tuples")
extractL4C _ = error "L4 doesn't work for 2-tuples"
instance ExtractL4C (a,b,c) where
type ExtractL4T (a,b,c) = GL.TypeError ('GL.Text "L4 doesn't work for 3-tuples")
extractL4C _ = error "L4 doesn't work for 3-tuples"
instance ExtractL4C (a,b,c,d) where
type ExtractL4T (a,b,c,d) = d
extractL4C (_,_,_,d) = d
instance ExtractL4C (a,b,c,d,e) where
type ExtractL4T (a,b,c,d,e) = d
extractL4C (_,_,_,d,_) = d
instance ExtractL4C (a,b,c,d,e,f) where
type ExtractL4T (a,b,c,d,e,f) = d
extractL4C (_,_,_,d,_,_) = d
data L5 p
instance (Show (ExtractL5T (PP p x))
, ExtractL5C (PP p x)
, P p x
, Show (PP p x)
) => P (L5 p) x where
type PP (L5 p) x = ExtractL5T (PP p x)
eval _ opts x = do
let msg0 = "L5"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL5C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL5C tp where
type ExtractL5T tp
extractL5C :: tp -> ExtractL5T tp
instance ExtractL5C (a,b) where
type ExtractL5T (a,b) = GL.TypeError ('GL.Text "L5 doesn't work for 2-tuples")
extractL5C _ = error "L5 doesn't work for 2-tuples"
instance ExtractL5C (a,b,c) where
type ExtractL5T (a,b,c) = GL.TypeError ('GL.Text "L5 doesn't work for 3-tuples")
extractL5C _ = error "L5 doesn't work for 3-tuples"
instance ExtractL5C (a,b,c,d) where
type ExtractL5T (a,b,c,d) = GL.TypeError ('GL.Text "L5 doesn't work for 4-tuples")
extractL5C _ = error "L5 doesn't work for 4-tuples"
instance ExtractL5C (a,b,c,d,e) where
type ExtractL5T (a,b,c,d,e) = e
extractL5C (_,_,_,_,e) = e
instance ExtractL5C (a,b,c,d,e,f) where
type ExtractL5T (a,b,c,d,e,f) = e
extractL5C (_,_,_,_,e,_) = e
data L6 p
instance (Show (ExtractL6T (PP p x))
, ExtractL6C (PP p x)
, P p x
, Show (PP p x)
) => P (L6 p) x where
type PP (L6 p) x = ExtractL6T (PP p x)
eval _ opts x = do
let msg0 = "L6"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL6C p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
class ExtractL6C tp where
type ExtractL6T tp
extractL6C :: tp -> ExtractL6T tp
instance ExtractL6C (a,b) where
type ExtractL6T (a,b) = GL.TypeError ('GL.Text "L6 doesn't work for 2-tuples")
extractL6C _ = error "L6 doesn't work for 2-tuples"
instance ExtractL6C (a,b,c) where
type ExtractL6T (a,b,c) = GL.TypeError ('GL.Text "L6 doesn't work for 3-tuples")
extractL6C _ = error "L6 doesn't work for 3-tuples"
instance ExtractL6C (a,b,c,d) where
type ExtractL6T (a,b,c,d) = GL.TypeError ('GL.Text "L6 doesn't work for 4-tuples")
extractL6C _ = error "L6 doesn't work for 4-tuples"
instance ExtractL6C (a,b,c,d,e) where
type ExtractL6T (a,b,c,d,e) = GL.TypeError ('GL.Text "L6 doesn't work for 5-tuples")
extractL6C _ = error "L6 doesn't work for 5-tuples"
instance ExtractL6C (a,b,c,d,e,f) where
type ExtractL6T (a,b,c,d,e,f) = f
extractL6C (_,_,_,_,_,f) = f
data FromStringP' t s
type FromStringP (t :: Type) p = FromStringP' (Hole t) p
instance (P s a
, PP s a ~ String
, Show (PP t a)
, IsString (PP t a)
) => P (FromStringP' t s) a where
type PP (FromStringP' t s) a = PP t a
eval _ opts a = do
let msg0 = "FromStringP"
ss <- eval (Proxy @s) opts a
pure $ case getValueLR opts msg0 ss [] of
Left e -> e
Right s ->
let b = fromString @(PP t a) s
in mkNode opts (PresentT b) [msg0 <> show0 opts " " b] [hh ss]
data FromInteger' t n
type FromInteger (t :: Type) p = FromInteger' (Hole t) p
instance (Num (PP t a)
, Integral (PP n a)
, P n a
, Show (PP t a)
) => P (FromInteger' t n) a where
type PP (FromInteger' t n) a = PP t a
eval _ opts a = do
let msg0 = "FromInteger"
nn <- eval (Proxy @n) opts a
pure $ case getValueLR opts msg0 nn [] of
Left e -> e
Right n ->
let b = fromInteger (fromIntegral n)
in mkNode opts (PresentT b) [msg0 <> show0 opts " " b] [hh nn]
data FromIntegral' t n
type FromIntegral (t :: Type) p = FromIntegral' (Hole t) p
instance (Num (PP t a)
, Integral (PP n a)
, P n a
, Show (PP t a)
, Show (PP n a)
) => P (FromIntegral' t n) a where
type PP (FromIntegral' t n) a = PP t a
eval _ opts a = do
let msg0 = "FromIntegral"
nn <- eval (Proxy @n) opts a
pure $ case getValueLR opts msg0 nn [] of
Left e -> e
Right n ->
let b = fromIntegral n
in mkNode opts (PresentT b) [show01 opts msg0 b n] [hh nn]
data ToRational p
instance (a ~ PP p x
, Show a
, Real a
, P p x)
=> P (ToRational p) x where
type PP (ToRational p) x = Rational
eval _ opts x = do
let msg0 = "ToRational"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a ->
let r = (toRational a)
in mkNode opts (PresentT r) [show01 opts msg0 r a] [hh pp]
data FromRational' t r
type FromRational (t :: Type) p = FromRational' (Hole t) p
instance (P r a
, PP r a ~ Rational
, Show (PP t a)
, Fractional (PP t a)
) => P (FromRational' t r) a where
type PP (FromRational' t r) a = PP t a
eval _ opts a = do
let msg0 = "FromRational"
rr <- eval (Proxy @r) opts a
pure $ case getValueLR opts msg0 rr [] of
Left e -> e
Right r ->
let b = fromRational @(PP t a) r
in mkNode opts (PresentT b) [show01 opts msg0 b r] [hh rr]
data Truncate' t p
type Truncate (t :: Type) p = Truncate' (Hole t) p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Truncate' t p) x where
type PP (Truncate' t p) x = PP t x
eval _ opts x = do
let msg0 = "Truncate"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = truncate p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data Ceiling' t p
type Ceiling (t :: Type) p = Ceiling' (Hole t) p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Ceiling' t p) x where
type PP (Ceiling' t p) x = PP t x
eval _ opts x = do
let msg0 = "Ceiling"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = ceiling p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data Floor' t p
type Floor (t :: Type) p = Floor' (Hole t) p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Floor' t p) x where
type PP (Floor' t p) x = PP t x
eval _ opts x = do
let msg0 = "Floor"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = floor p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data MkProxy
instance Show a => P MkProxy a where
type PP MkProxy a = Proxy a
eval _ opts a =
let msg0 = "MkProxy"
b = Proxy @a
in pure $ mkNode opts (PresentT b) [msg0 <> show1 opts " | " a] []
type family DoExpandT (ps :: [k]) :: Type where
DoExpandT '[] = GL.TypeError ('GL.Text "'[] invalid: requires at least one predicate in the list")
DoExpandT '[p] = Id >> p
DoExpandT (p ': p1 ': ps) = p >> DoExpandT (p1 ': ps)
data Do (ps :: [k])
instance (P (DoExpandT ps) a) => P (Do ps) a where
type PP (Do ps) a = PP (DoExpandT ps) a
eval _ = eval (Proxy @(DoExpandT ps))
data MaybeBool b p
instance (Show (PP p a)
, P b a
, P p a
, PP b a ~ Bool
) => P (MaybeBool b p) a where
type PP (MaybeBool b p) a = Maybe (PP p a)
eval _ opts z = do
let msg0 = "MaybeBool"
bb <- evalBool (Proxy @b) opts z
case getValueLR opts (msg0 <> " b failed") bb [] of
Left e -> pure e
Right True -> do
pp <- eval (Proxy @p) opts z
pure $ case getValueLR opts (msg0 <> " p failed") pp [hh bb] of
Left e -> e
Right p -> mkNode opts (PresentT (Just p)) [msg0 <> "(False)" <> show0 opts " Just " p] [hh bb, hh pp]
Right False -> pure $ mkNode opts (PresentT Nothing) [msg0 <> "(True)"] [hh bb]
data EitherBool b p q
instance (Show (PP p a)
, P p a
, Show (PP q a)
, P q a
, P b a
, PP b a ~ Bool
) => P (EitherBool b p q) a where
type PP (EitherBool b p q) a = Either (PP p a) (PP q a)
eval _ opts z = do
let msg0 = "EitherBool"
bb <- evalBool (Proxy @b) opts z
case getValueLR opts (msg0 <> " b failed") bb [] of
Left e -> pure e
Right False -> do
pp <- eval (Proxy @p) opts z
pure $ case getValueLR opts (msg0 <> " p failed") pp [hh bb] of
Left e -> e
Right p -> mkNode opts (PresentT (Left p)) [msg0 <> "(False)" <> show0 opts " Left " p] [hh bb, hh pp]
Right True -> do
qq <- eval (Proxy @q) opts z
pure $ case getValueLR opts (msg0 <> " q failed") qq [hh bb] of
Left e -> e
Right q -> mkNode opts (PresentT (Right q)) [msg0 <> "(True)" <> show0 opts " Right " q] [hh bb, hh qq]
data Pad (left :: Bool) n p q
type PadL n p q = Pad 'True n p q
type PadR n p q = Pad 'False n p q
instance (P n a
, GetBool left
, Integral (PP n a)
, [PP p a] ~ PP q a
, P p a
, P q a
, Show (PP p a)
) => P (Pad left n p q) a where
type PP (Pad left n p q) a = PP q a
eval _ opts a = do
let msg0 = "Pad" <> (if lft then "L" else "R")
lft = getBool @left
lr <- runPQ msg0 (Proxy @n) (Proxy @p) opts a []
case lr of
Left e -> pure e
Right (fromIntegral -> n,p,nn,pp) -> do
let msg1 = msg0 <> show0 opts " " n <> " pad=" <> show p
hhs = [hh nn, hh pp]
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts (msg1 <> " q failed") qq hhs of
Left e -> e
Right q ->
let l = length q
diff = if n<=l then 0 else n-l
bs = if lft
then (replicate diff p) <> q
else q <> (replicate diff p)
in mkNode opts (PresentT bs) [show01 opts msg1 bs q] (hhs <> [hh qq])
data SplitAts ns p
instance (P ns x
, P p x
, PP p x ~ [a]
, Show n
, Show a
, PP ns x ~ [n]
, Integral n
) => P (SplitAts ns p) x where
type PP (SplitAts ns p) x = [PP p x]
eval _ opts x = do
let msg0 = "SplitAts"
lr <- runPQ msg0 (Proxy @ns) (Proxy @p) opts x []
pure $ case lr of
Left e -> e
Right (ns,p,nn,pp) ->
let zs = foldr (\n k s -> let (a,b) = splitAt (fromIntegral n) s
in a:k b
) (\as -> if null as then [] else [as]) ns p
in mkNode opts (PresentT zs) [show01' opts msg0 zs "ns=" ns <> show1 opts " | " p] [hh nn, hh pp]
data SplitAt n p
type Take n p = Fst (SplitAt n p)
type Drop n p = Snd (SplitAt n p)
instance (PP p a ~ [b]
, P n a
, P p a
, Show b
, Integral (PP n a)
) => P (SplitAt n p) a where
type PP (SplitAt n p) a = (PP p a, PP p a)
eval _ opts a = do
let msg0 = "SplitAt"
lr <- runPQ msg0 (Proxy @n) (Proxy @p) opts a []
pure $ case lr of
Left e -> e
Right (fromIntegral -> n,p,pp,qq) ->
let msg1 = msg0 <> show0 opts " " n <> show0 opts " " p
(x,y) = splitAt n p
ret = (x,y)
in mkNode opts (PresentT ret) [show01' opts msg1 ret "n=" n <> show1 opts " | " p] [hh pp, hh qq]
type p &&& q = W '(p, q)
infixr 3 &&&
data p *** q
infixr 3 ***
type First p = p *** I
type Second q = I *** q
instance (Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p *** q) (a,b) where
type PP (p *** q) (a,b) = (PP p a, PP q b)
eval _ opts (a,b) = do
let msg0 = "(***)"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right a1 -> do
qq <- eval (Proxy @q) opts b
pure $ case getValueLR opts msg0 qq [hh pp] of
Left e -> e
Right b1 -> mkNode opts (PresentT (a1,b1)) [msg0 <> show0 opts " " (a1,b1) <> show1 opts " | " (a,b)] [hh pp, hh qq]
data p ||| q
infixr 2 |||
type EitherIn p q = p ||| q
type IsLeft = 'True ||| 'False
type IsRight = 'False ||| 'True
instance (Show (PP p a)
, P p a
, P q b
, PP p a ~ PP q b
, Show a
, Show b
) => P (p ||| q) (Either a b) where
type PP (p ||| q) (Either a b) = PP p a
eval _ opts lr = do
let msg0 = "(|||)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a1 -> let msg1 = msg0 ++ " Left"
in mkNode opts (_tBool pp) [show01 opts msg1 a1 a] [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNode opts (_tBool qq) [show01 opts msg1 a1 a] [hh qq]
data p +++ q
infixr 2 +++
instance (Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p +++ q) (Either a b) where
type PP (p +++ q) (Either a b) = Either (PP p a) (PP q b)
eval _ opts lr = do
let msg0 = "(+++)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Left"
in mkNode opts (PresentT (Left a1)) [msg1 <> show0 opts " " a1 <> show1 opts " | " a] [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNode opts (PresentT (Right a1)) [msg1 <> show0 opts " " a1 <> show1 opts " | " a] [hh qq]
type Dup = '(Id, Id)
data BinOp = BMult | BSub | BAdd deriving (Show,Eq)
type Mult p q = Bin 'BMult p q
type Add p q = Bin 'BAdd p q
type Sub p q = Bin 'BSub p q
type p + q = Add p q
infixl 6 +
type p - q = Sub p q
infixl 6 -
type p * q = Mult p q
infixl 7 *
type p > q = Cmp 'Cgt p q
infix 4 >
type p >= q = Cmp 'Cge p q
infix 4 >=
type p == q = Cmp 'Ceq p q
infix 4 ==
type p /= q = Cmp 'Cne p q
infix 4 /=
type p <= q = Cmp 'Cle p q
infix 4 <=
type p < q = Cmp 'Clt p q
infix 4 <
type Gt n = Cmp 'Cgt I n
type Ge n = Cmp 'Cge I n
type Same n = Cmp 'Ceq I n
type Le n = Cmp 'Cle I n
type Lt n = Cmp 'Clt I n
type Ne n = Cmp 'Cne I n
type p >~ q = CmpI 'Cgt p q
infix 4 >~
type p >=~ q = CmpI 'Cge p q
infix 4 >=~
type p ==~ q = CmpI 'Ceq p q
infix 4 ==~
type p /=~ q = CmpI 'Cne p q
infix 4 /=~
type p <=~ q = CmpI 'Cle p q
infix 4 <=~
type p <~ q = CmpI 'Clt p q
infix 4 <~
class GetBinOp (k :: BinOp) where
getBinOp :: (Num a, a ~ b) => (String, a -> b -> a)
instance GetBinOp 'BMult where
getBinOp = ("*",(*))
instance GetBinOp 'BSub where
getBinOp = ("-",(-))
instance GetBinOp 'BAdd where
getBinOp = ("+",(+))
data Bin (op :: BinOp) p q
instance (GetBinOp op
, PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Num (PP p a)
) => P (Bin op p q) a where
type PP (Bin op p q) a = PP p a
eval _ opts a = do
let (s,f) = getBinOp @op
lr <- runPQ s (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p `f` q
in mkNode opts (PresentT d) [show p <> " " <> s <> " " <> show q <> " = " <> show d] [hh pp, hh qq]
data p / q
infixl 7 /
instance (PP p a ~ PP q a
, Eq (PP q a)
, P p a
, P q a
, Show (PP p a)
, Fractional (PP p a)
) => P (p / q) a where
type PP (p / q) a = PP p a
eval _ opts a = do
let msg0 = "(/)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq)
| q == 0 -> let msg1 = msg0 <> " zero denominator"
in mkNode opts (FailT msg1) [msg1] [hh pp, hh qq]
| otherwise ->
let d = p / q
in mkNode opts (PresentT d) [show p <> " / " <> show q <> " = " <> show d] [hh pp, hh qq]
data p % q
infixl 8 %
type p %- q = Negate (p % q)
infixl 8 %-
type p -% q = Negate (p % q)
infixl 8 -%
instance (Integral (PP p x)
, Integral (PP q x)
, Eq (PP q x)
, P p x
, P q x
, Show (PP p x)
, Show (PP q x)
) => P (p % q) x where
type PP (p % q) x = Rational
eval _ opts x = do
let msg0 = "MkRatio"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq)
| q == 0 -> let msg1 = msg0 <> " zero denominator"
in mkNode opts (FailT msg1) [msg1] [hh pp, hh qq]
| otherwise ->
let d = fromIntegral p % fromIntegral q
in mkNode opts (PresentT d) [show p <> " % " <> show q <> " = " <> show d] [hh pp, hh qq]
data Negate p
instance (Show (PP p x), Num (PP p x), P p x) => P (Negate p) x where
type PP (Negate p) x = PP p x
eval _ opts x = do
let msg0 = "Negate"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = negate p
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data Abs p
instance (Show (PP p x), Num (PP p x), P p x) => P (Abs p) x where
type PP (Abs p) x = PP p x
eval _ opts x = do
let msg0 = "Abs"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = abs p
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data Signum p
instance (Show (PP p x), Num (PP p x), P p x) => P (Signum p) x where
type PP (Signum p) x = PP p x
eval _ opts x = do
let msg0 = "Signum"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = signum p
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data Unwrap p
instance (PP p x ~ s
, P p x
, Show s
, Show (Unwrapped s)
, Wrapped s
) => P (Unwrap p) x where
type PP (Unwrap p) x = Unwrapped (PP p x)
eval _ opts x = do
let msg0 = "Unwrap"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = p ^. _Wrapped'
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data Wrap' t p
type Wrap (t :: Type) p = Wrap' (Hole t) p
instance (Show (PP p x)
, P p x
, Unwrapped (PP s x) ~ PP p x
, Wrapped (PP s x)
, Show (PP s x)
) => P (Wrap' s p) x where
type PP (Wrap' s p) x = PP s x
eval _ opts x = do
let msg0 = "Wrap"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = p ^. _Unwrapped'
in mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]
data Coerce (t :: k)
instance (Show a
, Show t
, Coercible t a
) => P (Coerce t) a where
type PP (Coerce t) a = t
eval _ opts a =
let msg0 = "Coerce"
d = a ^. coerced
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d a] []
data Coerce2 (t :: k)
instance (Show (f a)
, Show (f t)
, Coercible t a
, Functor f
) => P (Coerce2 t) (f a) where
type PP (Coerce2 t) (f a) = f t
eval _ opts fa =
let msg0 = "Coerce2"
d = view coerced <$> fa
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d fa] []
data MEmptyT2' t
type MEmptyT2 t = MEmptyT2' (Hole t)
instance (Show (f a)
, Show (f (PP t (f a)))
, Functor f
, Monoid (PP t (f a))
) => P (MEmptyT2' t) (f a) where
type PP (MEmptyT2' t) (f a) = f (PP t (f a))
eval _ opts fa =
let msg0 = "MEmptyT2"
b = mempty <$> fa
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b fa] []
data Pure2 (t :: Type -> Type)
type MkRightAlt t p = Pure (Either t) p
type MkLeftAlt t p = MkRightAlt t p >> Swap
instance (Show (f (t a))
, Show (f a)
, Applicative t
, Functor f
) => P (Pure2 t) (f a) where
type PP (Pure2 t) (f a) = f (t a)
eval _ opts fa =
let msg0 = "Pure2"
b = fmap pure fa
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b fa] []
data Reverse
instance (Show a, as ~ [a]) => P Reverse as where
type PP Reverse as = as
eval _ opts as =
let msg0 = "Reverse"
d = reverse as
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d as] []
data ReverseL
instance (Show t, Reversing t) => P ReverseL t where
type PP ReverseL t = t
eval _ opts as =
let msg0 = "ReverseL"
d = as ^. reversed
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d as] []
data Swap
instance (Show (p a b)
, SW.Swap p
, Show (p b a)
) => P Swap (p a b) where
type PP Swap (p a b) = p b a
eval _ opts pab =
let msg0 = "Swap"
d = SW.swap pab
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pab] []
data Assoc
instance (Show (p (p a b) c)
, Show (p a (p b c))
, AS.Assoc p
) => P Assoc (p (p a b) c) where
type PP Assoc (p (p a b) c) = p a (p b c)
eval _ opts pabc =
let msg0 = "Assoc"
d = AS.assoc pabc
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pabc] []
data Unassoc
instance (Show (p (p a b) c)
, Show (p a (p b c))
, AS.Assoc p
) => P Unassoc (p a (p b c)) where
type PP Unassoc (p a (p b c)) = p (p a b) c
eval _ opts pabc =
let msg0 = "Unassoc"
d = AS.unassoc pabc
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d pabc] []
data SuccB p q
type SuccB' q = SuccB (Failp "Succ bounded failed") q
instance (PP q x ~ a
, P q x
, P p (Proxy a)
, PP p (Proxy a) ~ a
, Show a
, Eq a
, Bounded a
, Enum a
) => P (SuccB p q) x where
type PP (SuccB p q) x = PP q x
eval _ opts x = do
let msg0 = "SuccB"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case succMay q of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @p) opts (Proxy @a)
pure $ case getValueLR opts msg1 pp [hh qq] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh qq, hh pp]
Just n -> pure $ mkNode opts (PresentT n) [show01 opts msg0 n q] [hh qq]
data PredB p q
type PredB' q = PredB (Failp "Pred bounded failed") q
instance (PP q x ~ a
, P q x
, P p (Proxy a)
, PP p (Proxy a) ~ a
, Show a
, Eq a
, Bounded a
, Enum a
) => P (PredB p q) x where
type PP (PredB p q) x = PP q x
eval _ opts x = do
let msg0 = "PredB"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case predMay q of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @p) opts (Proxy @a)
pure $ case getValueLR opts msg1 pp [hh qq] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh qq, hh pp]
Just n -> pure $ mkNode opts (PresentT n) [show01 opts msg0 n q] [hh qq]
data Succ p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (Succ p) x where
type PP (Succ p) x = PP p x
eval _ opts x = do
let msg0 = "Succ"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (succ p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) [msg0 <> show0 opts " " p] [hh pp]
Right n -> mkNode opts (PresentT n) [show01 opts msg0 n p] [hh pp]
data Pred p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (Pred p) x where
type PP (Pred p) x = PP p x
eval _ opts x = do
let msg0 = "Pred"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (pred p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) [msg0 <> show0 opts " " p] [hh pp]
Right n -> mkNode opts (PresentT n) [show01 opts msg0 n p] [hh pp]
data FromEnum p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (FromEnum p) x where
type PP (FromEnum p) x = Int
eval _ opts x = do
let msg0 = "FromEnum"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let n = fromEnum p
in mkNode opts (PresentT n) [show01 opts msg0 n p] [hh pp]
data ToEnum' t p
type ToEnum (t :: Type) p = ToEnum' (Hole t) p
instance (PP p x ~ a
, P p x
, Show a
, Enum (PP t x)
, Show (PP t x)
, Integral a
) => P (ToEnum' t p) x where
type PP (ToEnum' t p) x = PP t x
eval _ opts x = do
let msg0 = "ToEnum"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (toEnum $! fromIntegral p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) [msg0 <> show0 opts " " p] [hh pp]
Right n -> mkNode opts (PresentT n) [show01 opts msg0 n p] [hh pp]
data ToEnumBDef' t def
type ToEnumBDef (t :: Type) def = ToEnumBDef' (Hole t) def
type ToEnumBFail (t :: Type) = ToEnumBDef' (Hole t) (Failp "ToEnum bounded failed")
instance (P def (Proxy (PP t a))
, PP def (Proxy (PP t a)) ~ (PP t a)
, Show a
, Show (PP t a)
, Bounded (PP t a)
, Enum (PP t a)
, Integral a
) => P (ToEnumBDef' t def) a where
type PP (ToEnumBDef' t def) a = PP t a
eval _ opts a = do
let msg0 = "ToEnumBDef"
case toEnumMay $ fromIntegral a of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @def) opts (Proxy @(PP t a))
pure $ case getValueLR opts msg1 pp [] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh pp]
Just n -> pure $ mkNode opts (PresentT n) [show01 opts msg0 n a] []
data Prime p
instance (PP p x ~ a
, P p x
, Show a
, Integral a
) => P (Prime p) x where
type PP (Prime p) x = Bool
eval _ opts x = do
let msg0 = "Prime"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = isPrime $ fromIntegral p
in mkNodeB opts b [msg0 <> show1 opts " | " p] []
isPrime :: Integer -> Bool
isPrime n = n==2 || n>2 && all ((> 0).rem n) (2:[3,5 .. floor . sqrt @Double . fromIntegral $ n+1])
data KeepImpl (keep :: Bool) p q
type Remove p q = KeepImpl 'False p q
type Keep p q = KeepImpl 'True p q
instance (GetBool keep
, Eq a
, Show a
, P p x
, P q x
, PP p x ~ PP q x
, PP q x ~ [a]
) => P (KeepImpl keep p q) x where
type PP (KeepImpl keep p q) x = PP q x
eval _ opts x = do
let msg0 = if keep then "Keep" else "Remove"
keep = getBool @keep
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let ret = filter (bool not id keep . (`elem` p)) q
in mkNode opts (PresentT ret) [show01' opts msg0 ret "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data Elem p q
instance ([PP p a] ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Eq (PP p a)
) => P (Elem p q) a where
type PP (Elem p q) a = Bool
eval _ opts a = do
let msg0 = "Elem"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = p `elem` q
in mkNodeB opts b [show p <> " `elem` " <> show q] [hh pp, hh qq]
data FMapFst
instance Functor f => P FMapFst (f (a,x)) where
type PP FMapFst (f (a,x)) = f a
eval _ opts mb = pure $ mkNode opts (PresentT (fst <$> mb)) ["FMapFst"] []
data FMapSnd
instance Functor f => P FMapSnd (f (x,a)) where
type PP FMapSnd (f (x,a)) = f a
eval _ opts mb = pure $ mkNode opts (PresentT (snd <$> mb)) ["FMapSnd"] []
type HeadDef p q = JustDef p (q >> Uncons >> FMapFst)
type HeadFail msg q = JustFail msg (q >> Uncons >> FMapFst)
type TailDef p q = JustDef p (q >> Uncons >> FMapSnd)
type TailFail msg q = JustFail msg (q >> Uncons >> FMapSnd)
type LastDef p q = JustDef p (q >> Unsnoc >> FMapSnd)
type LastFail msg q = JustFail msg (q >> Unsnoc >> FMapSnd)
type InitDef p q = JustDef p (q >> Unsnoc >> FMapFst)
type InitFail msg q = JustFail msg (q >> Unsnoc >> FMapFst)
type LookupDef' x y p q = JustDef p (q >> Lookup x y)
type LookupFail' msg x y q = JustFail msg (q >> Lookup x y)
type LookupDef x y p = LookupDef' x y p I
type LookupFail msg x y = LookupFail' msg x y I
type Left' p = LeftFail "expected Left" p
type Right' p = RightFail "expected Right" p
type This' p = ThisFail "expected This" p
type That' p = ThatFail "expected That" p
type These' p = TheseFail "expected These" p
data EitherX p q r
instance (P r x
, P p (x,a)
, P q (x,b)
, PP r x ~ Either a b
, PP p (x,a) ~ c
, PP q (x,b) ~ c
) => P (EitherX p q r) x where
type PP (EitherX p q r) x = EitherXT (PP r x) x p
eval _ opts x = do
let msg0 = "EitherX"
rr <- eval (Proxy @r) opts x
case getValueLR opts msg0 rr [] of
Left e -> pure e
Right (Left a) -> do
let msg1 = msg0 <> "(Left)"
pp <- eval (Proxy @p) opts (x,a)
pure $ case getValueLR opts msg1 pp [hh rr] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh rr, hh pp]
Right (Right b) -> do
let msg1 = msg0 <> "(Right)"
qq <- eval (Proxy @q) opts (x,b)
pure $ case getValueLR opts msg1 qq [hh rr] of
Left e -> e
Right _ -> mkNode opts (_tBool qq) [msg1] [hh rr, hh qq]
type family EitherXT lr x p where
EitherXT (Either a b) x p = PP p (x,a)
EitherXT o _ _ = GL.TypeError (
'GL.Text "EitherXT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data TheseX p q r s
instance (P s x
, P p (x,a)
, P q (x,b)
, P r (x,(a,b))
, PP s x ~ These a b
, PP p (x,a) ~ c
, PP q (x,b) ~ c
, PP r (x,(a,b)) ~ c
) => P (TheseX p q r s) x where
type PP (TheseX p q r s) x = TheseXT (PP s x) x p
eval _ opts x = do
let msg0 = "TheseX"
ss <- eval (Proxy @s) opts x
case getValueLR opts msg0 ss [] of
Left e -> pure e
Right (This a) -> do
let msg1 = msg0 <> "(This)"
pp <- eval (Proxy @p) opts (x,a)
pure $ case getValueLR opts msg1 pp [hh ss] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh ss, hh pp]
Right (That b) -> do
let msg1 = msg0 <> "(That)"
qq <- eval (Proxy @q) opts (x,b)
pure $ case getValueLR opts msg1 qq [hh ss] of
Left e -> e
Right _ -> mkNode opts (_tBool qq) [msg1] [hh ss, hh qq]
Right (These a b) -> do
let msg1 = msg0 <> "(These)"
rr <- eval (Proxy @r) opts (x,(a,b))
pure $ case getValueLR opts msg1 rr [hh ss] of
Left e -> e
Right _ -> mkNode opts (_tBool rr) [msg1] [hh ss, hh rr]
type family TheseXT lr x p where
TheseXT (These a b) x p = PP p (x,a)
data MaybeIn p q
type IsNothing = MaybeIn 'True 'False
type IsJust = MaybeIn 'False 'True
instance (P q a
, Show a
, Show (PP q a)
, PP p (Proxy (PP q a)) ~ PP q a
, P p (Proxy (PP q a))
) => P (MaybeIn p q) (Maybe a) where
type PP (MaybeIn p q) (Maybe a) = PP q a
eval _ opts ma = do
let msg0 = "MaybeIn"
case ma of
Nothing -> do
let msg1 = msg0 <> "(Nothing)"
pp <- eval (Proxy @p) opts (Proxy @(PP q a))
pure $ case getValueLR opts msg1 pp [] of
Left e -> e
Right b -> mkNode opts (_tBool pp) [msg1 <> show0 opts " " b <> " | Proxy"] [hh pp]
Just a -> do
let msg1 = msg0 <> "(Nothing)"
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg1 qq [] of
Left e -> e
Right b -> mkNode opts (_tBool qq) [show01 opts msg1 b a] [hh qq]
data STimes n p
instance (P n a
, Integral (PP n a)
, Semigroup (PP p a)
, P p a
, Show (PP p a)
) => P (STimes n p) a where
type PP (STimes n p) a = PP p a
eval _ opts a = do
let msg0 = "STimes"
lr <- runPQ msg0 (Proxy @n) (Proxy @p) opts a []
pure $ case lr of
Left e -> e
Right (fromIntegral -> (n::Int),p,pp,qq) ->
let msg1 = msg0 <> show0 opts " " n <> " p=" <> show p
b = SG.stimes n p
in mkNode opts (PresentT b) [show01' opts msg1 b "n=" n <> show1 opts " | " p] [hh pp, hh qq]
data Pure (t :: Type -> Type) p
instance (P p x
, Show (PP p x)
, Show (t (PP p x))
, Applicative t
) => P (Pure t p) x where
type PP (Pure t p) x = t (PP p x)
eval _ opts x = do
let msg0 = "Pure"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a ->
let b = pure a
in mkNode opts (PresentT b) [show01 opts msg0 b a] [hh pp]
data MEmptyT' t
type MEmptyT (t :: Type) = MEmptyT' (Hole t)
type MEmptyP = MEmptyT' Unproxy
instance (Show (PP t a), Monoid (PP t a)) => P (MEmptyT' t) a where
type PP (MEmptyT' t) a = PP t a
eval _ opts _ =
let msg0 = "MEmptyT"
b = mempty @(PP t a)
in pure $ mkNode opts (PresentT b) [msg0 <> show0 opts " " b] []
data EmptyT (t :: Type -> Type) p
instance (P p x
, PP p x ~ a
, Show (t a)
, Show a
, Alternative t
) => P (EmptyT t p) x where
type PP (EmptyT t p) x = t (PP p x)
eval _ opts x = do
let msg0 = "EmptyT"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = empty @t
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data MkNothing' t
type MkNothing (t :: Type) = MkNothing' (Hole t)
instance P (MkNothing' t) a where
type PP (MkNothing' t) a = Maybe (PP t a)
eval _ opts _ =
let msg0 = "MkNothing"
in pure $ mkNode opts (PresentT Nothing) [msg0] []
data MkJust p
instance (PP p x ~ a, P p x, Show a) => P (MkJust p) x where
type PP (MkJust p) x = Maybe (PP p x)
eval _ opts x = do
let msg0 = "MkJust"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = Just p
in mkNode opts (PresentT d) [msg0 <> show0 opts " Just " p] [hh pp]
data MkLeft' t p
type MkLeft (t :: Type) p = MkLeft' (Hole t) p
instance (Show (PP p x), P p x) => P (MkLeft' t p) x where
type PP (MkLeft' t p) x = Either (PP p x) (PP t x)
eval _ opts x = do
let msg0 = "MkLeft"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = Left p
in mkNode opts (PresentT d) [msg0 <> show0 opts " Left " p] [hh pp]
data MkRight' t p
type MkRight (t :: Type) p = MkRight' (Hole t) p
instance (Show (PP p x), P p x) => P (MkRight' t p) x where
type PP (MkRight' t p) x = Either (PP t x) (PP p x)
eval _ opts x = do
let msg0 = "MkRight"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = Right p
in mkNode opts (PresentT d) [msg0 <> show0 opts " Right " p] [hh pp]
data MkThis' t p
type MkThis (t :: Type) p = MkThis' (Hole t) p
instance (Show (PP p x), P p x) => P (MkThis' t p) x where
type PP (MkThis' t p) x = These (PP p x) (PP t x)
eval _ opts x = do
let msg0 = "MkThis"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = This p
in mkNode opts (PresentT d) [msg0 <> show0 opts " This " p] [hh pp]
data MkThat' t p
type MkThat (t :: Type) p = MkThat' (Hole t) p
instance (Show (PP p x), P p x) => P (MkThat' t p) x where
type PP (MkThat' t p) x = These (PP t x) (PP p x)
eval _ opts x = do
let msg0 = "MkThat"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = That p
in mkNode opts (PresentT d) [msg0 <> show0 opts " That " p] [hh pp]
data MkThese p q
instance (P p a
, P q a
, Show (PP p a)
, Show (PP q a)
) => P (MkThese p q) a where
type PP (MkThese p q) a = These (PP p a) (PP q a)
eval _ opts a = do
let msg0 = "MkThese"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = These p q
in mkNode opts (PresentT d) [msg0 <> show0 opts " " d] [hh pp, hh qq]
data MConcat p
type FoldMap (t :: Type) p = Map (Wrap t Id) p >> Unwrap (MConcat Id)
instance (PP p x ~ [a]
, P p x
, Show a
, Monoid a
) => P (MConcat p) x where
type PP (MConcat p) x = ExtractAFromTA (PP p x)
eval _ opts x = do
let msg0 = "MConcat"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = mconcat p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data Concat p
instance (Show a
, Show (t [a])
, PP p x ~ (t [a])
, P p x
, Foldable t
) => P (Concat p) x where
type PP (Concat p) x = ExtractAFromTA (PP p x)
eval _ opts x = do
let msg0 = "Concat"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = concat p
in mkNode opts (PresentT b) [show01 opts msg0 b p] [hh pp]
data Cycle n p
instance (Show a
, Show (t a)
, PP p x ~ (t a)
, P p x
, Integral (PP n x)
, P n x
, Foldable t
) => P (Cycle n p) x where
type PP (Cycle n p) x = [ExtractAFromTA (PP p x)]
eval _ opts x = do
let msg0 = "Cycle"
lr <- runPQ msg0 (Proxy @n) (Proxy @p) opts x []
pure $ case lr of
Left e -> e
Right (fromIntegral -> n,p,nn,pp) ->
let hhs = [hh nn, hh pp]
in case chkSize opts msg0 p hhs of
Left e -> e
Right () ->
let msg1 = msg0 <> "("<> show n <> ")"
d = take n (cycle (toList p))
in mkNode opts (PresentT d) [show01 opts msg1 d p] hhs
data ProxyT' t
type ProxyT (t :: Type) = ProxyT' (Hole t)
instance Typeable t => P (ProxyT' (t :: Type)) a where
type PP (ProxyT' t) a = Proxy (PP t a)
eval _ opts _ =
let t = showT @t
in pure $ mkNode opts (PresentT Proxy) ["ProxyT(" <> show t ++ ")"] []
data Ix (n :: Nat) def
type Ix' (n :: Nat) = Ix n (Failp "Ix index not found")
instance (P def (Proxy a)
, PP def (Proxy a) ~ a
, KnownNat n
, Show a
) => P (Ix n def) [a] where
type PP (Ix n def) [a] = a
eval _ opts as = do
let n = nat @n
msg0 = "Ix " <> show n
case as ^? ix n of
Nothing -> do
let msg1 = msg0 <> " not found"
pp <- eval (Proxy @def) opts (Proxy @a)
pure $ case getValueLR opts msg1 pp [] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) [msg1] [hh pp]
Just a -> pure $ mkNode opts (PresentT a) [msg0 <> show0 opts " " a] []
data IxL p q def
type p !! q = IxL p q (Failp "(!!) index not found")
instance (P q a
, P p a
, Show (PP p a)
, Ixed (PP p a)
, PP q a ~ Index (PP p a)
, Show (Index (PP p a))
, Show (IxValue (PP p a))
, P r (Proxy (IxValue (PP p a)))
, PP r (Proxy (IxValue (PP p a))) ~ IxValue (PP p a)
)
=> P (IxL p q r) a where
type PP (IxL p q r) a = IxValue (PP p a)
eval _ opts a = do
let msg0 = "IxL"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> "(" <> show q <> ")"
in case p ^? ix q of
Nothing -> do
rr <- eval (Proxy @r) opts (Proxy @(IxValue (PP p a)))
pure $ case getValueLR opts msg1 rr [hh pp, hh qq] of
Left e -> e
Right _ -> mkNode opts (_tBool rr) [msg1 <> " index not found"] [hh pp, hh qq]
Just ret -> pure $ mkNode opts (PresentT ret) [show01' opts msg1 ret "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data Lookup p q
instance (P q a
, P p a
, Show (PP p a)
, Ixed (PP p a)
, PP q a ~ Index (PP p a)
, Show (Index (PP p a))
, Show (IxValue (PP p a))
)
=> P (Lookup p q) a where
type PP (Lookup p q) a = Maybe (IxValue (PP p a))
eval _ opts a = do
let msg0 = "Lookup"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let msg1 = msg0 <> "(" <> show q <> ")"
hhs = [hh pp, hh qq]
in case p ^? ix q of
Nothing -> mkNode opts (PresentT Nothing) [msg1 <> " not found"] hhs
Just ret -> mkNode opts (PresentT (Just ret)) [show01' opts msg1 ret "p=" p <> show1 opts " | q=" q] hhs
data Ands p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t
, a ~ Bool
) => P (Ands p) x where
type PP (Ands p) x = Bool
eval _ opts x = do
let msg0 = "Ands"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let msg1 = msg0 ++ "(" ++ show (length p) ++ ")"
w = case findIndex not (toList p) of
Nothing -> ""
Just i -> " i="++show i
in mkNodeB opts (and p) [msg1 <> w <> show1 opts " | " p] [hh pp]
data Ors p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t
, a ~ Bool
) => P (Ors p) x where
type PP (Ors p) x = Bool
eval _ opts x = do
let msg0 = "Ors"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let msg1 = msg0 ++ "(" ++ show (length p) ++ ")"
w = case findIndex id (toList p) of
Nothing -> ""
Just i -> " i="++show i
in mkNodeB opts (or p) [msg1 <> w <> show1 opts " | " p] [hh pp]
data p :+ q
infixr 5 :+
instance (P p x
, P q x
, Show (PP p x)
, Show (PP q x)
, Cons (PP q x) (PP q x) (PP p x) (PP p x)
) => P (p :+ q) x where
type PP (p :+ q) x = PP q x
eval _ opts z = do
let msg0 = "(:+)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = p `cons` q
in mkNode opts (PresentT b) [show01' opts msg0 b "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data p +: q
infixl 5 +:
instance (P p x
, P q x
, Show (PP q x)
, Show (PP p x)
, Snoc (PP p x) (PP p x) (PP q x) (PP q x)
) => P (p +: q) x where
type PP (p +: q) x = PP p x
eval _ opts z = do
let msg0 = "(+:)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = p `snoc` q
in mkNode opts (PresentT b) [show01' opts msg0 b "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data Uncons
instance (Show (ConsT s)
, Show s
, Cons s s (ConsT s) (ConsT s)
) => P Uncons s where
type PP Uncons s = Maybe (ConsT s,s)
eval _ opts as =
let msg0 = "Uncons"
b = as ^? _Cons
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b as] []
data Unsnoc
instance (Show (ConsT s)
, Show s
, Snoc s s (ConsT s) (ConsT s)
) => P Unsnoc s where
type PP Unsnoc s = Maybe (s,ConsT s)
eval _ opts as =
let msg0 = "Unsnoc"
b = as ^? _Snoc
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b as] []
data IsEmpty
instance (Show as, AsEmpty as) => P IsEmpty as where
type PP IsEmpty as = Bool
eval _ opts as =
let b = has _Empty as
in pure $ mkNodeB opts b ["IsEmpty" <> show1 opts " | " as] []
data Null
instance (Show (t a)
, Foldable t
, t a ~ as
) => P Null as where
type PP Null as = Bool
eval _ opts as =
let b = null as
in pure $ mkNodeB opts b ["Null" <> show1 opts " | " as] []
data EnumFromTo p q
instance (P p x
, P q x
, PP p x ~ a
, Show a
, PP q x ~ a
, Enum a
) => P (EnumFromTo p q) x where
type PP (EnumFromTo p q) x = [PP p x]
eval _ opts z = do
let msg0 = "EnumFromTo"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) -> mkNode opts (PresentT (enumFromTo p q)) [msg0 <> " [" <> show p <> " .. " <> show q <> "]"] [hh pp, hh qq]
type MapMaybe p q = ConcatMap (p >> MaybeIn MEmptyP '[Id]) q
type CatMaybes q = MapMaybe Id q
data PartitionEithers
instance (Show a, Show b) => P PartitionEithers [Either a b] where
type PP PartitionEithers [Either a b] = ([a], [b])
eval _ opts as =
let msg0 = "PartitionEithers"
b = partitionEithers as
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b as] []
data PartitionThese
instance (Show a, Show b) => P PartitionThese [These a b] where
type PP PartitionThese [These a b] = ([a], [b], [(a, b)])
eval _ opts as =
let msg0 = "PartitionThese"
b = partitionThese as
in pure $ mkNode opts (PresentT b) [show01 opts msg0 b as] []
type Thiss = Fst PartitionThese
type Thats = Snd PartitionThese
type Theses = Thd PartitionThese
data Scanl p q r
type ScanN n p q = Scanl (Fst Id >> q) p (EnumFromTo 1 n)
type ScanNA q = ScanN (Fst Id) (Snd Id) q
type FoldN n p q = Last (ScanN n p q)
type Foldl p q r = Last (Scanl p q r)
instance (PP p (b,a) ~ b
, PP q x ~ b
, PP r x ~ [a]
, P p (b,a)
, P q x
, P r x
, Show b
, Show a
)
=> P (Scanl p q r) x where
type PP (Scanl p q r) x = [PP q x]
eval _ opts z = do
let msg0 = "Scanl"
lr <- runPQ msg0 (Proxy @q) (Proxy @r) opts z []
case lr of
Left e -> pure e
Right (q,r,qq,rr) -> do
let msg1 = msg0
ff i b as' rs
| i >= _MX = pure (rs, Left $ mkNode opts (FailT (msg1 <> ":failed at i=" <> showIndex i)) [msg1 <> " i=" <> showIndex i <> " (b,as')=" <> show (b,as')] [])
| otherwise =
case as' of
[] -> pure (rs, Right ())
a:as -> do
pp :: TT b <- eval (Proxy @p) opts (b,a)
case getValueLR opts (msg1 <> " i=" <> showIndex i <> " a=" <> show a) pp [] of
Left e -> pure (rs,Left e)
Right b' -> ff (i+1) b' as (rs ++ [((i,b), pp)])
(ts,lrx) :: ([((Int, b), TT b)], Either (TT [b]) ()) <- ff 1 q r []
pure $ case splitAndAlign opts [msg1] (((0,q), mkNode opts (PresentT q) [msg1 <> "(initial)"] []) : ts) of
Left _e -> error "cant happen!"
Right (vals,itts) ->
case lrx of
Left e -> mkNode opts (_tBool e) [msg1] (hh qq : hh rr : map (hh . fixit) itts ++ [hh e])
Right () -> mkNode opts (PresentT vals) [show01' opts msg1 vals "b=" q <> show1 opts " | as=" r] (hh qq : hh rr : map (hh . fixit) itts)
type family UnfoldT mbs where
UnfoldT (Maybe (b,s)) = b
data Unfoldr p q
type IterateN n f = Unfoldr (MaybeBool (Fst Id > 0) '(Snd Id, Pred Id *** f)) '(n, Id)
type IterateUntil p f = IterateWhile (Not p) f
type IterateWhile p f = Unfoldr (MaybeBool p '(Id, f)) Id
type IterateNWhile n p f = '(n, Id) >> IterateWhile (Fst Id > 0 && (Snd Id >> p)) (Pred Id *** f) >> Map (Snd Id) Id
type IterateNUntil n p f = IterateNWhile n (Not p) f
instance (PP q a ~ s
, PP p s ~ Maybe (b,s)
, P q a
, P p s
, Show s
, Show b
)
=> P (Unfoldr p q) a where
type PP (Unfoldr p q) a = [UnfoldT (PP p (PP q a))]
eval _ opts z = do
let msg0 = "Unfoldr"
qq <- eval (Proxy @q) opts z
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
let msg1 = msg0 <> show0 opts " " q
ff i s rs | i >= _MX = pure (rs, Left $ mkNode opts (FailT (msg1 <> ":failed at i=" <> showIndex i)) [msg1 <> " i=" <> showIndex i <> " s=" <> show s] [])
| otherwise = do
pp :: TT (PP p s) <- eval (Proxy @p) opts s
case getValueLR opts (msg1 <> " i=" <> showIndex i <> " s=" <> show s) pp [] of
Left e -> pure (rs, Left e)
Right Nothing -> pure (rs, Right ())
Right w@(Just (_b,s')) -> ff (i+1) s' (rs ++ [((i,w), pp)])
(ts,lr) :: ([((Int, PP p s), TT (PP p s))], Either (TT [b]) ()) <- ff 1 q []
pure $ case splitAndAlign opts [msg1] ts of
Left _e -> error "cant happen"
Right (vals, itts) ->
case lr of
Left e -> mkNode opts (_tBool e) [msg1] (hh qq : map (hh . fixit) itts ++ [hh e])
Right () ->
let ret = fst <$> catMaybes vals
in mkNode opts (PresentT ret) [show01' opts msg1 ret "s=" q ] (hh qq : map (hh . fixit) itts)
data Map p q
type ConcatMap p q = Concat (Map p q)
instance (Show (PP p a)
, P p a
, PP q x ~ f a
, P q x
, Show a
, Show (f a)
, Foldable f
) => P (Map p q) x where
type PP (Map p q) x = [PP p (ExtractAFromTA (PP q x))]
eval _ opts x = do
let msg0 = "Map"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
ts <- zipWithM (\i a -> ((i, a),) <$> eval (Proxy @p) opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts [msg0] ts of
Left e -> e
Right (vals, _) -> mkNode opts (PresentT vals) [show01 opts msg0 vals q] (hh qq : map (hh . fixit) ts)
data If p q r
instance (Show (PP r a)
, P p a
, PP p a ~ Bool
, P q a
, P r a
, PP q a ~ PP r a
) => P (If p q r) a where
type PP (If p q r) a = PP q a
eval _ opts a = do
let msg0 = "If"
pp <- evalBool (Proxy @p) opts a
case getValueLR opts (msg0 <> " condition failed") pp [] of
Left e -> pure e
Right b -> do
qqrr <- if b
then eval (Proxy @q) opts a
else eval (Proxy @r) opts a
pure $ case getValueLR opts (msg0 <> " [" <> show b <> "]") qqrr [hh pp, hh qqrr] of
Left e -> e
Right ret -> mkNode opts (_tBool qqrr) [msg0 <> " " <> if b then "(true cond)" else "(false cond)" <> show0 opts " " ret] [hh pp, hh qqrr]
data Pairs
instance Show a => P Pairs [a] where
type PP Pairs [a] = [(a,a)]
eval _ opts as =
let msg0 = "Pairs"
lr = case as of
[] -> Left (msg0 <> " no data found")
[_] -> Left (msg0 <> " only one element found")
_:bs@(_:_) -> Right (zip as bs)
in pure $ case lr of
Left e -> mkNode opts (FailT e) [e] []
Right zs -> mkNode opts (PresentT zs) [show01 opts msg0 zs as ] []
data Partition p q
type Filter p q = Partition p q >> Fst Id
instance (P p x
, Show x
, PP q a ~ [x]
, PP p x ~ Bool
, P q a
) => P (Partition p q) a where
type PP (Partition p q) a = (PP q a, PP q a)
eval _ opts a' = do
let msg0 = "Partition"
qq <- eval (Proxy @q) opts a'
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalBool (Proxy @p) opts a) [0::Int ..] q
pure $ case splitAndAlign opts [msg0] ts of
Left e -> e
Right (vals, tfs) ->
let w0 = partition fst $ zip vals tfs
zz1 = (map (snd . fst . snd) *** map (snd . fst . snd)) w0
in mkNode opts (PresentT zz1) [show01' opts msg0 zz1 "s=" q] (hh qq : map (hh . fixit) tfs)
data Break p q
type Span p q = Break (Not p) q
instance (P p x
, PP q a ~ [x]
, PP p x ~ Bool
, P q a
) => P (Break p q) a where
type PP (Break p q) a = (PP q a, PP q a)
eval _ opts a' = do
let msg0 = "Break"
qq <- eval (Proxy @q) opts a'
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
let ff [] zs = pure (zs, [], Nothing)
ff ((i,a):ias) zs = do
pp <- evalBool (Proxy @p) opts a
let v = ((i,a), pp)
case getValueLR opts msg0 pp [hh qq] of
Right False -> ff ias (zs Seq.|> v)
Right True -> pure (zs,map snd ias,Just v)
Left _ -> pure (zs,map snd ias,Just v)
(ialls,rhs,mpivot) <- ff (zip [0::Int ..] q) Seq.empty
pure $ case mpivot of
Nothing ->
mkNode opts (PresentT (map (snd . fst) (toList ialls), rhs))
([msg0] <> ["cnt=" <> show (length ialls, length rhs)])
(map (hh . fixit) (toList ialls))
Just iall@(ia, tt) ->
case getValueLR opts (msg0 <> " predicate failed") tt (hh qq : map (hh . fixit) (toList (ialls Seq.|> iall))) of
Right True ->
mkNode opts (PresentT (map (snd . fst) (toList ialls), snd ia : rhs))
([msg0] <> ["cnt=" <> show (length ialls, 1+length rhs)])
(hh qq : hh tt : map (hh . fixit) (toList (ialls Seq.|> iall)))
Right False -> error "shouldnt happen"
Left e -> e
data Fail t prt
type Failp s = Fail Unproxy s
type Failt (t :: Type) prt = Fail (Hole t) prt
type FailS s = Fail I s
instance (P prt a
, PP prt a ~ String
) => P (Fail t prt) a where
type PP (Fail t prt) a = PP t a
eval _ opts a = do
let msg0 = "Fail"
pp <- eval (Proxy @prt) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right s -> mkNode opts (FailT s) [msg0 <> " " <> s] (if isVerbose opts then [hh pp] else [])
data Hole (t :: Type)
instance Typeable t => P (Hole t) a where
type PP (Hole t) a = t
eval _ opts _a =
let msg0 = "Hole(" <> showT @t <> ")"
in pure $ mkNode opts (FailT msg0) [msg0 <> " you probably meant to get access to the type of PP only and not evaluate"] []
data Unproxy
instance Typeable a => P Unproxy (Proxy (a :: Type)) where
type PP Unproxy (Proxy a) = a
eval _ opts _a =
let msg0 = "Unproxy(" <> showT @a <> ")"
in pure $ mkNode opts (FailT msg0) [msg0 <> " you probably meant to get access to the type of PP only and not evaluate"] []
data Catch p q
type Catch' p s = Catch p (FailCatch s)
type FailCatch s = Fail (Snd Id >> Unproxy) (Fst Id >> s)
instance (P p x
, P q ((String, x)
, Proxy (PP p x))
, PP p x ~ PP q ((String, x), Proxy (PP p x))
) => P (Catch p q) x where
type PP (Catch p q) x = PP p x
eval _ opts x = do
let msg0 = "Catch"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> do
let emsg = e ^?! tBool . _FailT
qq <- eval (Proxy @q) opts ((emsg, x), Proxy @(PP p x))
pure $ case getValueLR opts (msg0 <> " default condition failed") qq [hh pp] of
Left e1 -> e1
Right _ -> mkNode opts (_tBool qq) [msg0 <> " caught exception[" <> emsg <> "]"] [hh pp, hh qq]
Right _ -> pure $ mkNode opts (_tBool pp) [msg0 <> " did not fire"] [hh pp]
type Even = Mod I 2 == 0
type Odd = Mod I 2 == 1
data Div p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (Div p q) a where
type PP (Div p q) a = PP p a
eval _ opts a = do
let msg0 = "Div"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) [msg0 <> " zero denominator"] hhs
_ -> let d = p `div` q
in mkNode opts (PresentT d) [show p <> " `div` " <> show q <> " = " <> show d] hhs
data Mod p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (Mod p q) a where
type PP (Mod p q) a = PP p a
eval _ opts a = do
let msg0 = "Mod"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) [msg0 <> " zero denominator"] hhs
_ -> let d = p `mod` q
in mkNode opts (PresentT d) [show p <> " `mod` " <> show q <> " = " <> show d] hhs
data DivMod p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (DivMod p q) a where
type PP (DivMod p q) a = (PP p a, PP p a)
eval _ opts a = do
let msg0 = "DivMod"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) [msg0 <> " zero denominator"] hhs
_ -> let d = p `divMod` q
in mkNode opts (PresentT d) [show p <> " `divMod` " <> show q <> " = " <> show d] hhs
data QuotRem p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (QuotRem p q) a where
type PP (QuotRem p q) a = (PP p a, PP p a)
eval _ opts a = do
let msg0 = "QuotRem"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) [msg0 <> " zero denominator"] hhs
_ -> let d = p `quotRem` q
in mkNode opts (PresentT d) [show p <> " `quotRem` " <> show q <> " = " <> show d] hhs
type Quot p q = Fst (QuotRem p q)
type Rem p q = Snd (QuotRem p q)
type OneP = Guard (PrintF "expected list of length 1 but found length=%d" Len) (Len == 1) >> Head Id
data GuardsImpl (n :: Nat) (os :: [(k,k1)])
type GuardsQuick (prt :: k) (os :: [k1]) = Guards (ToGuardsT prt os)
data Guards (ps :: [(k,k1)])
instance (GetLen ps, P (GuardsImpl (LenT ps) ps) [a]) => P (Guards ps) [a] where
type PP (Guards ps) [a] = PP (GuardsImpl (LenT ps) ps) [a]
eval _ opts as = do
let msgbase0 = "Guards"
n = getLen @ps
if n /= length as then
let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")"
in pure $ mkNode opts (FailT xx) [xx] []
else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
instance (KnownNat n
, Show a
) => P (GuardsImpl n ('[] :: [(k,k1)])) [a] where
type PP (GuardsImpl n ('[] :: [(k,k1)])) [a] = [a]
eval _ opts as =
let msg0 = "Guards" <> "(" <> show n <> ")"
n :: Int = nat @n
in if not (null as) then error $ "programmer error: GuardsImpl base case has extra data " ++ show as
else pure $ mkNode opts (PresentT as) [msg0 <> " done!"] []
instance (PP prt (Int, a) ~ String
, P prt (Int, a)
, KnownNat n
, GetLen ps
, P p a
, PP p a ~ Bool
, P (GuardsImpl n ps) [a]
, PP (GuardsImpl n ps) [a] ~ [a]
, Show a
) => P (GuardsImpl n ('(prt,p) ': ps)) [a] where
type PP (GuardsImpl n ('(prt,p) ': ps)) [a] = [a]
eval _ opts as' = do
let msgbase1 = "Guard" <> "(" <> show (n-pos) <> ")"
msgbase2 = "Guards"
n :: Int = nat @n
pos = getLen @ps
case as' of
a:as -> do
pp <- evalBool (Proxy @p) opts a
case getValueLR opts (msgbase1 <> " p failed") pp [] of
Left e -> pure e
Right False -> do
qq <- eval (Proxy @prt) opts (n-pos,a)
pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
Left e -> e
Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else [])
Right True -> do
ss <- eval (Proxy @(GuardsImpl n ps)) opts as
pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
Left e -> e
Right zs -> mkNode opts (PresentT (a:zs)) [msgbase1 <> show0 opts " " a] [hh pp, hh ss]
_ -> error $ "programmer error: GuardsImpl n+1 case has no data"
data Bools (ps :: [(k,k1)])
type BoolsQuick (prt :: k) (ps :: [k1]) = Bools (ToGuardsT prt ps)
instance (GetLen ps
, P (BoolsImpl (LenT ps) ps) [a]
, PP (BoolsImpl (LenT ps) ps) [a] ~ Bool
) => P (Bools ps) [a] where
type PP (Bools ps) [a] = Bool
eval _ opts as = do
let msgbase0 = "Bools("++show n++")"
n = getLen @ps
if n /= length as then
let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")"
in pure $ mkNode opts (FailT xx) [xx] []
else evalBool (Proxy @(BoolsImpl (LenT ps) ps)) opts as
data BoolsImpl (n :: Nat) (os :: [(k,k1)])
instance (KnownNat n
, Show a
) => P (BoolsImpl n ('[] :: [(k,k1)])) [a] where
type PP (BoolsImpl n ('[] :: [(k,k1)])) [a] = Bool
eval _ opts as =
let msg0 = "Bools" <> "(" <> show n <> ")"
n :: Int = nat @n
in if not (null as) then error $ "programmer error: BoolsImpl base case has extra data " ++ show as
else pure $ mkNodeB opts True [msg0 <> " done!"] []
instance (PP prt (Int, a) ~ String
, P prt (Int, a)
, KnownNat n
, GetLen ps
, P p a
, PP p a ~ Bool
, P (BoolsImpl n ps) [a]
, PP (BoolsImpl n ps) [a] ~ Bool
, Show a
) => P (BoolsImpl n ('(prt,p) ': ps)) [a] where
type PP (BoolsImpl n ('(prt,p) ': ps)) [a] = Bool
eval _ opts as' = do
let cpos = n-pos-1
msgbase1 = "GuardBool" <> "(" <> showIndex cpos <> ")"
msgbase2 = "Bools"
n :: Int = nat @n
pos = getLen @ps
case as' of
a:as -> do
pp <- evalBool (Proxy @p) opts a
case getValueLR opts (msgbase1 <> " p failed") pp [] of
Left e -> pure e
Right False -> do
qq <- eval (Proxy @prt) opts (cpos,a)
pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
Left e -> e
Right msgx -> mkNodeB opts False [msgbase1 <> " [" <> msgx <> "] " <> topMessage pp] (hh pp : if isVerbose opts then [hh qq] else [])
Right True -> do
ss <- evalBool (Proxy @(BoolsImpl n ps)) opts as
pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
Left e -> e
Right True -> mkNodeB opts True [msgbase1 <> show0 opts " " a] [hh pp, hh ss]
Right False -> ss & tForest %~ \x -> fromTT pp : x
_ -> error $ "programmer error: BoolsImpl n+1 case has no data"
data BoolsN prt (n :: Nat) p
instance ( GetLen (ToGuardsT prt (RepeatT n p))
, PP (BoolsImpl (LenT (ToGuardsT prt (RepeatT n p))) (ToGuardsT prt (RepeatT n p))) [a] ~ Bool
, P (BoolsImpl (LenT (ToGuardsT prt (RepeatT n p))) (ToGuardsT prt (RepeatT n p))) [a]
) => P (BoolsN prt n p) [a] where
type PP (BoolsN prt n p) [a] = PP (Bools (ToGuardsT prt (RepeatT n p))) [a]
eval _ opts as =
eval (Proxy @(Bools (ToGuardsT prt (RepeatT n p)))) opts as
data GuardsImplX (n :: Nat) (os :: [(k,k1)])
type GuardsDetail (prt :: Symbol) (os :: [(k0,k1)]) = GuardsImplXX (ToGuardsDetailT prt os)
type family ToGuardsDetailT (prt :: k1) (os :: [(k2,k3)]) :: [(Type,k3)] where
ToGuardsDetailT prt '[ '(s,p) ] = '(PrintT prt '(s,Id), p) : '[]
ToGuardsDetailT prt ( '(s,p) ': ps) = '(PrintT prt '(s,Id), p) ': ToGuardsDetailT prt ps
ToGuardsDetailT prt '[] = GL.TypeError ('GL.Text "ToGuardsDetailT cannot be empty")
data GuardsImplXX (ps :: [(k,k1)])
instance (GetLen ps
, P (GuardsImplX (LenT ps) ps) [a]
) => P (GuardsImplXX ps) [a] where
type PP (GuardsImplXX ps) [a] = PP (GuardsImplX (LenT ps) ps) [a]
eval _ opts as = do
let msgbase0 = "Guards"
n = getLen @ps
if n /= length as then
let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")"
in pure $ mkNode opts (FailT xx) [xx] []
else eval (Proxy @(GuardsImplX (LenT ps) ps)) opts as
instance (KnownNat n
, Show a
) => P (GuardsImplX n ('[] :: [(k,k1)])) [a] where
type PP (GuardsImplX n ('[] :: [(k,k1)])) [a] = [a]
eval _ opts as =
let msg0 = "Guards" <> "(" <> show n <> ")"
n :: Int = nat @n
in if not (null as) then error $ "programmer error: GuardsImplX base case has extra data " ++ show as
else pure $ mkNode opts (PresentT as) [msg0 <> " done!"] []
instance (PP prt a ~ String
, P prt a
, KnownNat n
, GetLen ps
, P p a
, PP p a ~ Bool
, P (GuardsImplX n ps) [a]
, PP (GuardsImplX n ps) [a] ~ [a]
, Show a
) => P (GuardsImplX n ('(prt,p) ': ps)) [a] where
type PP (GuardsImplX n ('(prt,p) ': ps)) [a] = [a]
eval _ opts as' = do
let cpos = n-pos-1
msgbase1 = "Guard" <> "(" <> showIndex cpos <> ")"
msgbase2 = "Guards"
n :: Int = nat @n
pos = getLen @ps
case as' of
a:as -> do
pp <- evalBool (Proxy @p) opts a
case getValueLR opts (msgbase1 <> " p failed") pp [] of
Left e -> pure e
Right False -> do
qq <- eval (Proxy @prt) opts a
pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
Left e -> e
Right msgx -> mkNode opts (FailT msgx) [msgbase1 <> " failed [" <> msgx <> "]" <> show0 opts " " a] (hh pp : if isVerbose opts then [hh qq] else [])
Right True -> do
ss <- eval (Proxy @(GuardsImplX n ps)) opts as
pure $ case getValueLRHide opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
Left e -> e
Right zs -> mkNode opts (PresentT (a:zs)) [msgbase1 <> show0 opts " " a] [hh pp, hh ss]
_ -> error $ "programmer error: GuardsImplX n+1 case has no data"
data GuardsN prt (n :: Nat) p
instance ( GetLen (ToGuardsT prt (RepeatT n p))
, P (GuardsImpl
(LenT (ToGuardsT prt (RepeatT n p)))
(ToGuardsT prt (RepeatT n p)))
[a]
) => P (GuardsN prt n p) [a] where
type PP (GuardsN prt n p) [a] = PP (Guards (ToGuardsT prt (RepeatT n p))) [a]
eval _ opts as =
eval (Proxy @(Guards (ToGuardsT prt (RepeatT n p)))) opts as
data Guard prt p
type ExitWhen prt p = Guard prt (Not p)
instance (Show a
, P prt a
, PP prt a ~ String
, P p a
, PP p a ~ Bool
) => P (Guard prt p) a where
type PP (Guard prt p) a = a
eval _ opts a = do
let msg0 = "Guard"
pp <- evalBool (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right False -> do
qq <- eval (Proxy @prt) opts a
pure $ case getValueLR opts (msg0 <> " Msg") qq [hh pp] of
Left e -> e
Right msgx -> mkNode opts (FailT msgx) [msg0 <> "(failed) [" <> msgx <> "]" <> show0 opts " | " a] (hh pp : if isVerbose opts then [hh qq] else [])
Right True -> pure $ mkNode opts (PresentT a) [msg0 <> "(ok)" <> show0 opts " | " a] [hh pp]
data GuardSimple p
instance (Show a
, P p a
, PP p a ~ Bool
) => P (GuardSimple p) a where
type PP (GuardSimple p) a = a
eval _ opts a = do
let msg0 = "GuardSimple"
pp <- evalBool (Proxy @p) (if hasNoTree opts then o0 else opts) a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right False ->
let msgx = topMessage pp
in mkNode opts (FailT msgx) [msg0 <> "(failed) " <> msgx <> show0 opts " | " a] [hh pp]
Right True ->
mkNode opts (PresentT a) [msg0 <> "(ok)" <> show0 opts " | " a] [hh pp]
data Skip p
type p |> q = Skip p >> q
infixr 1 |>
type p >| q = p >> Skip q
infixr 1 >|
type p >|> q = Skip p >> Skip q
infixr 1 >|>
instance (Show (PP p a), P p a) => P (Skip p) a where
type PP (Skip p) a = a
eval _ opts a = do
let msg0 = "Skip"
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p -> mkNode opts (PresentT a) [msg0 <> show0 opts " " p] [hh pp]
data p >> q
infixr 1 >>
type (<<) p q = q >> p
infixr 1 <<
type p >>> q = p >> q
infixl 1 >>>
instance (Show (PP p a)
, Show (PP q (PP p a))
, P p a
, P q (PP p a)
) => P (p >> q) a where
type PP (p >> q) a = PP q (PP p a)
eval _ opts a = do
let msg0 = "(>>)"
pp <- eval (Proxy @p) opts a
case getValueLRHide opts ("(>>) lhs failed") pp [] of
Left e -> pure e
Right p -> do
qq <- eval (Proxy @q) opts p
pure $ case getValueLRHide opts (show p <> " (>>) rhs failed") qq [hh pp] of
Left e -> e
Right q -> mkNode opts (_tBool qq) [lit01 opts msg0 q (topMessage' qq)] [hh pp, hh qq]
data p && q
infixr 3 &&
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p && q) a where
type PP (p && q) a = Bool
eval _ opts a = do
let msg0 = "&&"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(True,True) -> ""
(False,True) -> topMessage pp
(True,False) -> topMessage qq
(False,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
in mkNodeB opts (p&&q) [show p <> " " <> msg0 <> " " <> show q <> (if null zz then zz else " | " <> zz)] [hh pp, hh qq]
data p || q
infixr 2 ||
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p || q) a where
type PP (p || q) a = Bool
eval _ opts a = do
let msg0 = "||"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(False,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
_ -> ""
in mkNodeB opts (p||q) [show p <> " " <> msg0 <> " " <> show q <> (if null zz then zz else " | " <> zz)] [hh pp, hh qq]
data p ~> q
infixr 1 ~>
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p ~> q) a where
type PP (p ~> q) a = Bool
eval _ opts a = do
let msg0 = "~>"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(True,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
_ -> ""
in mkNodeB opts (p~>q) [show p <> " " <> msg0 <> " " <> show q <> (if null zz then zz else " | " <> zz)] [hh pp, hh qq]
data Not p
instance (PP p x ~ Bool, P p x) => P (Not p) x where
type PP (Not p) x = Bool
eval _ opts x = do
let msg0 = "Not"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = not p
in mkNodeB opts b [msg0 <> " " <> topMessage pp] [hh pp]
data OrdP p q
type p ==! q = OrdP p q
infix 4 ==!
type OrdA' p q = OrdP (Fst Id >> p) (Snd Id >> q)
type OrdA p = OrdA' p p
instance (Ord (PP p a)
, PP p a ~ PP q a
, P p a
, Show (PP q a)
, P q a
) => P (OrdP p q) a where
type PP (OrdP p q) a = Ordering
eval _ opts a = do
let msg0 = "OrdP"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = compare p q
in mkNode opts (PresentT d) [msg0 <> " " <> show p <> " " <> prettyOrd d <> show0 opts " " q] [hh pp, hh qq]
data OrdI p q
type p ===~ q = OrdI p q
infix 4 ===~
instance (PP p a ~ String
, PP p a ~ PP q a
, P p a
, P q a
) => P (OrdI p q) a where
type PP (OrdI p q) a = Ordering
eval _ opts a = do
let msg0 = "OrdI"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = on compare (map toLower) p q
in mkNode opts (PresentT d) [msg0 <> " " <> p <> " " <> prettyOrd d <> " " <> q] [hh pp, hh qq]
data Cmp (o :: OrderingP) p q
instance (GetOrd o
, Ord (PP p a)
, Show (PP p a)
, PP p a ~ PP q a
, P p a
, P q a
) => P (Cmp o p q) a where
type PP (Cmp o p q) a = Bool
eval _ opts a = do
let (sfn, fn) = getOrd @o
lr <- runPQ sfn (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = fn p q
in mkNodeB opts b [show p <> " " <> sfn <> show0 opts " " q] [hh pp, hh qq]
data CmpI (o :: OrderingP) p q
instance (PP p a ~ String
, GetOrd o
, PP p a ~ PP q a
, P p a
, P q a
) => P (CmpI o p q) a where
type PP (CmpI o p q) a = Bool
eval _ opts a = do
let (sfn, fn) = getOrd @o
lr <- runPQ sfn (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = on fn (map toLower) p q
in mkNodeB opts b ["CmpI " <> p <> " " <> sfn <> " " <> q] [hh pp, hh qq]
data IToList' t p
type IToList (t :: Type) = IToList' (Hole t) Id
instance (Show x
, P p x
, Typeable (PP t (PP p x))
, Show (PP t (PP p x))
, FoldableWithIndex (PP t (PP p x)) f
, PP p x ~ f a
, Show a
) => P (IToList' t p) x where
type PP (IToList' t p) x = [(PP t (PP p x), ExtractAFromTA (PP p x))]
eval _ opts x = do
let msg0 = "IToList"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = itoList p
t = showT @(PP t (PP p x))
in mkNode opts (PresentT b) [msg0 <> "(" <> t <> ")" <> show0 opts " " b <> show1 opts " | " x] [hh pp]
data ToList
instance (Show (t a)
, Foldable t
, Show a
) => P ToList (t a) where
type PP ToList (t a) = [a]
eval _ opts as =
let msg0 = "ToList"
z = toList as
in pure $ mkNode opts (PresentT z) [show01 opts msg0 z as] []
data ToList' p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t
, Show a
) => P (ToList' p) x where
type PP (ToList' p) x = [ExtractAFromTA (PP p x)]
eval _ opts x = do
let msg0 = "ToList'"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let hhs = [hh pp]
b = toList p
in mkNode opts (PresentT b) [show01 opts msg0 b p] hhs
data ToListExt
instance (Show l
, GE.IsList l
, Show (GE.Item l)
) => P ToListExt l where
type PP ToListExt l = [GE.Item l]
eval _ opts as =
let msg0 = "ToListExt"
z = GE.toList as
in pure $ mkNode opts (PresentT z) [show01 opts msg0 z as] []
data FromList (t :: Type)
instance (a ~ GE.Item t
, Show t
, GE.IsList t
) => P (FromList t) [a] where
type PP (FromList t) [a] = t
eval _ opts as =
let msg0 = "FromList"
z = GE.fromList (as :: [GE.Item t]) :: t
in pure $ mkNode opts (PresentT z) [msg0 <> show0 opts " " z] []
data FromListExt (t :: Type)
instance (Show l
, GE.IsList l
, l ~ l'
) => P (FromListExt l') l where
type PP (FromListExt l') l = l'
eval _ opts as =
let msg0 = "FromListExt"
z = GE.fromList (GE.toList @l as)
in pure $ mkNode opts (PresentT z) [msg0 <> show0 opts " " z] []
data IsTh (th :: These x y) p
type IsThis p = IsTh ('This '()) p
type IsThat p = IsTh ('That '()) p
type IsThese p = IsTh ('These '() '()) p
instance (PP p x ~ These a b
, P p x
, Show a
, Show b
, GetThese th
) => P (IsTh (th :: These x1 x2) p) x where
type PP (IsTh th p) x = Bool
eval _ opts x = do
let msg0 = "IsTh"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (t,f) = getThese (Proxy @th)
b = f p
in mkNodeB opts b [msg0 <> " " <> t <> show1 opts " | " p] []
data TheseIn p q r
type TheseId p q = TheseIn '(I, p) '(q, I) I
instance (Show a
, Show b
, Show (PP p a)
, P p a
, P q b
, P r (a,b)
, PP p a ~ PP q b
, PP p a ~ PP r (a,b)
, PP q b ~ PP r (a,b)
) => P (TheseIn p q r) (These a b) where
type PP (TheseIn p q r) (These a b) = PP p a
eval _ opts =
\case
This a -> do
let msg0 = "This"
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts (msg0 <> " p failed") pp [] of
Left e -> e
Right c -> mkNode opts (PresentT c) [show01' opts msg0 c "This " a] [hh pp]
That b -> do
let msg0 = "That"
qq <- eval (Proxy @q) opts b
pure $ case getValueLR opts (msg0 <> " q failed") qq [] of
Left e -> e
Right c -> mkNode opts (PresentT c) [show01' opts msg0 c "That " b] [hh qq]
These a b -> do
let msg0 = "TheseIn"
rr <- eval (Proxy @r) opts (a,b)
pure $ case getValueLR opts (msg0 <> " r failed") rr [] of
Left e -> e
Right c -> mkNode opts (PresentT c) [show01 opts msg0 c (These a b)] [hh rr]
data EmptyList' t
type EmptyList (t :: Type) = EmptyList' (Hole t)
instance P (EmptyList' t) x where
type PP (EmptyList' t) x = [PP t x]
eval _ opts _ =
pure $ mkNode opts (PresentT []) ["EmptyList"] []
type Singleton p = p :+ EmptyT [] p
data Char1 (s :: Symbol)
instance (KnownSymbol s, NullT s ~ 'False) => P (Char1 s) a where
type PP (Char1 s) a = Char
eval _ opts _ =
let c = head $ symb @s
in pure $ mkNode opts (PresentT c) ["Char1" <> show0 opts " " c] []
data ZipThese p q
instance (PP p a ~ [x]
, PP q a ~ [y]
, P p a
, P q a
, Show x
, Show y
) => P (ZipThese p q) a where
type PP (ZipThese p q) a = [These (ExtractAFromList (PP p a)) (ExtractAFromList (PP q a))]
eval _ opts a = do
let msg0 = "ZipThese"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = simpleAlign p q
in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
simpleAlign :: [a] -> [b] -> [These a b]
simpleAlign as [] = map This as
simpleAlign [] bs = map That bs
simpleAlign (a:as) (b:bs) = These a b : simpleAlign as bs
type family ExtractAFromTA (ta :: Type) :: Type where
ExtractAFromTA (t a) = a
ExtractAFromTA z = GL.TypeError (
'GL.Text "ExtractAFromTA: expected (t a) but found something else"
':$$: 'GL.Text "t a = "
':<>: 'GL.ShowType z)
type family ExtractAFromList (as :: Type) :: Type where
ExtractAFromList [a] = a
ExtractAFromList z = GL.TypeError (
'GL.Text "ExtractAFromList: expected [a] but found something else"
':$$: 'GL.Text "as = "
':<>: 'GL.ShowType z)
data ZipPad l r p q
instance (PP l a ~ x
, PP r a ~ y
, P l a
, P r a
, PP p a ~ [x]
, PP q a ~ [y]
, P p a
, P q a
, Show x
, Show y
) => P (ZipPad l r p q) a where
type PP (ZipPad l r p q) a = [(PP l a, PP r a)]
eval _ opts a = do
let msg0 = "ZipPad"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs = [hh pp, hh qq]
case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of
Left e -> pure e
Right () -> do
let lls = (length p,length q)
case uncurry compare lls of
LT -> do
ll <- eval (Proxy @l) opts a
pure $ case getValueLR opts (msg0 <> " l failed") ll hhs of
Left e -> e
Right l ->
let d = zip (p ++ repeat l) q
in mkNode opts (PresentT d) [show01' opts (msg0 <> " Left pad") d "p=" p <> show1 opts " | q=" q] (hhs ++ [hh ll])
GT -> do
rr <- eval (Proxy @r) opts a
pure $ case getValueLR opts (msg0 <> " r failed") rr hhs of
Left e -> e
Right r ->
let d =zip p (q ++ repeat r)
in mkNode opts (PresentT d) [show01' opts (msg0 <> " Right pad") d "p=" p <> show1 opts " | q=" q] (hhs ++ [hh rr])
EQ ->
let d = zip p q
in pure $ mkNode opts (PresentT d) [show01' opts (msg0 <> " No pad") d "p=" p <> show1 opts " | q=" q] hhs
data ZipL l p q
instance (PP l a ~ x
, P l a
, PP p a ~ [x]
, PP q a ~ [y]
, P p a
, P q a
, Show x
, Show y
) => P (ZipL l p q) a where
type PP (ZipL l p q) a = [(ExtractAFromList (PP p a), ExtractAFromList (PP q a))]
eval _ opts a = do
let msg0 = "ZipL"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs = [hh pp, hh qq]
case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of
Left e -> pure e
Right () -> do
let lls = (length p,length q)
case uncurry compare lls of
GT -> let msg1 = msg0 ++ show lls
in pure $ mkNode opts (FailT (msg1 ++ " rhs would be truncated")) [msg1 <> "rhs would be truncated " <> show1 opts " | p=" p <> show1 opts " | q=" q] hhs
_ -> do
ll <- eval (Proxy @l) opts a
pure $ case getValueLR opts (msg0 <> " l failed") ll hhs of
Left e -> e
Right l ->
let d = zip (p ++ repeat l) q
in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] (hhs ++ [hh ll])
data ZipR r p q
instance (PP r a ~ y
, P r a
, PP p a ~ [x]
, PP q a ~ [y]
, P p a
, P q a
, Show x
, Show y
) => P (ZipR r p q) a where
type PP (ZipR r p q) a = [(ExtractAFromList (PP p a), ExtractAFromList (PP q a))]
eval _ opts a = do
let msg0 = "ZipR"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs = [hh pp, hh qq]
case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of
Left e -> pure e
Right () -> do
let lls = (length p,length q)
case uncurry compare lls of
LT -> let msg1 = msg0 ++ show lls
in pure $ mkNode opts (FailT (msg1 ++ " rhs would be truncated")) [msg1 <> "rhs would be truncated " <> show1 opts " | p=" p <> show1 opts " | q=" q] hhs
_ -> do
rr <- eval (Proxy @r) opts a
pure $ case getValueLR opts (msg0 <> " l failed") rr hhs of
Left e -> e
Right r ->
let d = zip p (q ++ repeat r)
in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] (hhs ++ [hh rr])
data Zip p q
instance (PP p a ~ [x]
, PP q a ~ [y]
, P p a
, P q a
, Show x
, Show y
) => P (Zip p q) a where
type PP (Zip p q) a = [(ExtractAFromList (PP p a), ExtractAFromList (PP q a))]
eval _ opts a = do
let msg0 = "Zip"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case chkSize opts msg0 p hhs <* chkSize opts msg0 q hhs of
Left e -> e
Right () ->
let lls = (length p, length q)
in case uncurry compare lls of
EQ -> let d = zip p q
in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] hhs
_ -> let msg1 = msg0 ++ show lls
in mkNode opts (FailT (msg1 <> " length mismatch")) [msg1 <> " length mismatch" ++ show1 opts " | p=" p <> show1 opts " | q=" q] hhs
data Luhn p
instance (PP p x ~ [Int]
, P p x
) => P (Luhn p) x where
type PP (Luhn p) x = Bool
eval _ opts x = do
let msg0 = "Luhn"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let xs = zipWith (*) (reverse p) (cycle [1,2])
ys = map (\w -> if w>=10 then w-9 else w) xs
z = sum ys
ret = z `mod` 10
hhs = [hh pp]
in if ret == 0 then mkNodeB opts True [msg0 <> show0 opts " | " p] hhs
else mkNodeB opts False [msg0 <> " map=" <> show ys <> " sum=" <> show z <> " ret=" <> show ret <> show1 opts " | " p] hhs
data ReadBase' t (n :: Nat) p
type ReadBase (t :: Type) (n :: Nat) p = ReadBase' (Hole t) n p
type ReadBaseInt (n :: Nat) p = ReadBase' (Hole Int) n p
instance (Typeable (PP t x)
, BetweenT 2 36 n
, Show (PP t x)
, Num (PP t x)
, KnownNat n
, PP p x ~ String
, P p x
) => P (ReadBase' t n p) x where
type PP (ReadBase' t n p) x = PP t x
eval _ opts x = do
let n = nat @n
xs = getValidBase n
msg0 = "ReadBase(" <> t <> "," <> show n <> ")"
t = showT @(PP t x)
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (ff,p1) = case p of
'-':q -> (negate,q)
_ -> (id,p)
in case readInt (fromIntegral n)
((`elem` xs) . toLower)
(fromJust . (`elemIndex` xs) . toLower)
p1 of
[(b,"")] -> mkNode opts (PresentT (ff b)) [msg0 <> show0 opts " " (ff b) <> show1 opts " | " p] [hh pp]
o -> mkNode opts (FailT ("invalid base " <> show n)) [msg0 <> " as=" <> p <> " err=" <> show o] [hh pp]
getValidBase :: Int -> String
getValidBase n =
let xs = ['0'..'9'] <> ['a'..'z']
len = length xs
in if n > len || n < 2 then error $ "oops invalid base valid is 2 thru " ++ show len ++ " found " ++ show n
else take n xs
data ShowBase (n :: Nat) p
instance (PP p x ~ a
, P p x
, Show a
, 2 GL.<= n
, n GL.<= 36
, KnownNat n
, Integral a
) => P (ShowBase n p) x where
type PP (ShowBase n p) x = String
eval _ opts x = do
let n = nat @n
xs = getValidBase n
msg0 = "ShowBase " <> show n
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (ff,a') = if p < 0 then (('-':), abs p) else (id,p)
b = showIntAtBase (fromIntegral n) (xs !!) a' ""
in mkNode opts (PresentT (ff b)) [msg0 <> showLit0 opts " " (ff b) <> show1 opts " | " p] []
data Intercalate p q
instance (PP p x ~ [a]
, PP q x ~ PP p x
, P p x
, P q x
, Show a
) => P (Intercalate p q) x where
type PP (Intercalate p q) x = PP p x
eval _ opts x = do
let msg0 = "Intercalate"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = intercalate p (map (:[]) q)
in mkNode opts (PresentT d) [show01 opts msg0 d p <> show1 opts " | " q] [hh pp, hh qq]
data PrintF s p
instance (PrintfArg (PP p x)
, Show (PP p x)
, PP s x ~ String
, P s x
, P p x
) => P (PrintF s p) x where
type PP (PrintF s p) x = String
eval _ opts x = do
let msg0 = "PrintF"
lrx <- runPQ msg0 (Proxy @s) (Proxy @p) opts x []
case lrx of
Left e -> pure e
Right (s,p,ss,pp) -> do
let msg1 = msg0
lr <- catchitNF @_ @E.SomeException (printf s p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg1 <> " (" <> e <> ")")) [msg1 <> show0 opts " " p <> " s=" <> s] [hh ss, hh pp]
Right ret -> mkNode opts (PresentT ret) [msg1 <> " [" <> showLit0 opts "" ret <> "]" <> show1 opts " | p=" p <> showLit1 opts " | s=" s] [hh ss, hh pp]
type family GuardsT (ps :: [k]) where
GuardsT '[] = '[]
GuardsT (p ': ps) = Guard "fromGuardsT" p ': GuardsT ps
type family ToGuardsT (prt :: k) (os :: [k1]) :: [(k,k1)] where
ToGuardsT prt '[] = GL.TypeError ('GL.Text "ToGuardsT cannot be empty")
ToGuardsT prt '[p] = '(prt,p) : '[]
ToGuardsT prt (p ': ps) = '(prt,p) ': ToGuardsT prt ps
data ParaImpl (n :: Nat) (os :: [k])
data Para (ps :: [k])
instance (GetLen ps, P (ParaImpl (LenT ps) ps) [a]) => P (Para ps) [a] where
type PP (Para ps) [a] = PP (ParaImpl (LenT ps) ps) [a]
eval _ opts as = do
let msgbase0 = "Para"
n = getLen @ps
if n /= length as then
let xx = msgbase0 <> ": data elements(" <> show (length as) <> ") /= predicates(" <> show n <> ")"
in pure $ mkNode opts (FailT xx) [xx] []
else eval (Proxy @(ParaImpl (LenT ps) ps)) opts as
instance GL.TypeError ('GL.Text "ParaImpl '[] invalid: requires at least one value in the list")
=> P (ParaImpl n ('[] :: [k])) [a] where
type PP (ParaImpl n ('[] :: [k])) [a] = Void
eval _ _ _ = error "should not be called and yet..."
instance (Show (PP p a)
, KnownNat n
, Show a
, P p a
) => P (ParaImpl n '[p]) [a] where
type PP (ParaImpl n '[p]) [a] = [PP p a]
eval _ opts as' = do
let msgbase0 = "Para"
msgbase1 = msgbase0 <> "(" <> show n <> ")"
n :: Int
n = nat @n
case as' of
[a] -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msgbase1 pp [] of
Left e -> e
Right b -> mkNode opts (PresentT [b]) [msgbase1 <> show0 opts " " (b : []) <> show1 opts " | " a] [hh pp]
_ -> error $ "programmer error: ParaImpl base case should have exactly one element but found " ++ show as'
instance (KnownNat n
, GetLen ps
, P p a
, P (ParaImpl n (p1 ': ps)) [a]
, PP (ParaImpl n (p1 ': ps)) [a] ~ [PP p a]
, Show a
, Show (PP p a)
)
=> P (ParaImpl n (p ': p1 ': ps)) [a] where
type PP (ParaImpl n (p ': p1 ': ps)) [a] = [PP p a]
eval _ opts as' = do
let cpos = n-pos-1
msgbase0 = msgbase2 <> "(" <> showIndex cpos <> " of " <> show n <> ")"
msgbase1 = msgbase2 <> "(" <> showIndex cpos <> ")"
msgbase2 = "Para"
n = nat @n
pos = 1 + getLen @ps
case as' of
a:as -> do
pp <- eval (Proxy @p) opts a
case getValueLR opts msgbase0 pp [] of
Left e -> pure e
Right b -> do
qq <- eval (Proxy @(ParaImpl n (p1 ': ps))) opts as
pure $ case getValueLRHide opts (msgbase1 <> " rhs failed " <> show b) qq [hh pp] of
Left e -> e
Right bs -> mkNode opts (PresentT (b:bs)) [msgbase1 <> show0 opts " " (b:bs) <> show1 opts " | " as'] [hh pp, hh qq]
_ -> error $ "programmer error: ParaImpl n+1 case has no data left"
data ParaN (n :: Nat) p
instance ( P (ParaImpl (LenT (RepeatT n p)) (RepeatT n p)) [a]
, GetLen (RepeatT n p)
) => P (ParaN n p) [a] where
type PP (ParaN n p) [a] = PP (Para (RepeatT n p)) [a]
eval _ opts as =
eval (Proxy @(Para (RepeatT n p))) opts as
data CaseImpl (n :: Nat) (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2)
data Case (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2)
type Case' (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (Snd Id >> Failp "Case:no match") ps qs r
type Case'' s (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (FailCase s) ps qs r
type FailCase p = Fail (Snd Id >> Unproxy) (Fst Id >> p)
instance (FailUnlessT (LenT ps DE.== LenT qs)
('GL.Text "lengths are not the same "
':<>: 'GL.ShowType (LenT ps)
':<>: 'GL.Text " vs "
':<>: 'GL.ShowType (LenT qs))
, P (CaseImpl (LenT ps) e ps qs r) x
) => P (Case e ps qs r) x where
type PP (Case e ps qs r) x = PP (CaseImpl (LenT ps) e ps qs r) x
eval _ = eval (Proxy @(CaseImpl (LenT ps) e ps qs r))
instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lhs requires at least one value in the list"))
=> P (CaseImpl n e ('[] :: [k]) (q ': qs) r) x where
type PP (CaseImpl n e ('[] :: [k]) (q ': qs) r) x = Void
eval _ _ _ = error "should not be called and yet..."
instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: rhs requires at least one value in the list"))
=> P (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x where
type PP (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x = Void
eval _ _ _ = error "should not be called and yet..."
instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lists are both empty"))
=> P (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x where
type PP (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x = Void
eval _ _ _ = error "should not be called and yet..."
instance (P r x
, P q (PP r x)
, Show (PP q (PP r x))
, P p (PP r x)
, PP p (PP r x) ~ Bool
, KnownNat n
, Show (PP r x)
, P e (PP r x, Proxy (PP q (PP r x)))
, PP e (PP r x, Proxy (PP q (PP r x))) ~ PP q (PP r x)
) => P (CaseImpl n e '[p] '[q] r) x where
type PP (CaseImpl n e '[p] '[q] r) x = PP q (PP r x)
eval _ opts z = do
let msgbase0 = "Case" <> "(" <> show n <> ")"
n :: Int = nat @n
rr <- eval (Proxy @r) opts z
case getValueLR opts msgbase0 rr [] of
Left e -> pure e
Right a -> do
pp <- evalBool (Proxy @p) opts a
case getValueLR opts msgbase0 pp [hh rr] of
Left e -> pure e
Right True -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msgbase0 qq [hh rr, hh pp] of
Left e -> e
Right b -> mkNode opts (PresentT b) [show01 opts msgbase0 b a] (hh rr : hh pp : if isVerbose opts then [hh qq] else [])
Right False -> do
ee <- eval (Proxy @e) opts (a, Proxy @(PP q (PP r x)))
pure $ case getValueLR opts (msgbase0 <> " otherwise failed") ee [hh rr, hh pp] of
Left e -> e
Right b -> mkNode opts (PresentT b) [show01 opts msgbase0 b a] [hh rr, hh pp, hh ee]
instance (KnownNat n
, GetLen ps
, P r x
, P p (PP r x)
, P q (PP r x)
, PP p (PP r x) ~ Bool
, Show (PP q (PP r x))
, Show (PP r x)
, P (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x
, PP (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x ~ PP q (PP r x)
)
=> P (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x where
type PP (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x = PP q (PP r x)
eval _ opts z = do
let cpos = n-pos-1
msgbase0 = msgbase2 <> "(" <> showIndex cpos <> " of " <> show n <> ")"
msgbase1 = msgbase2 <> "(" <> showIndex cpos <> ")"
msgbase2 = "Case"
n = nat @n
pos = 1 + getLen @ps
rr <- eval (Proxy @r) opts z
case getValueLR opts msgbase0 rr [] of
Left e -> pure e
Right a -> do
pp <- evalBool (Proxy @p) opts a
case getValueLR opts msgbase0 pp [hh rr] of
Left e -> pure e
Right True -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msgbase0 qq [hh pp, hh rr] of
Left e -> e
Right b -> mkNode opts (PresentT b) [show01 opts msgbase0 b a] (hh rr : hh pp : if isVerbose opts then [hh qq] else [])
Right False -> do
ww <- eval (Proxy @(CaseImpl n e (p1 ': ps) (q1 ': qs) r)) opts z
pure $ case getValueLR opts (msgbase1 <> " failed rhs") ww [hh rr, hh pp] of
Left e -> e
Right b -> mkNode opts (PresentT b) [show01 opts msgbase1 b a] [hh rr, hh pp, hh ww]
data Sequence
type Traverse p q = Map p q >> Sequence
instance (Show (f (t a))
, Show (t (f a))
, Traversable t
, Applicative f
) => P Sequence (t (f a)) where
type PP Sequence (t (f a)) = f (t a)
eval _ opts tfa =
let d = sequenceA tfa
in pure $ mkNode opts (PresentT d) ["Sequence" <> show0 opts " " d <> show1 opts " | " tfa] []
data Hide p
instance P p x => P (Hide p) x where
type PP (Hide p) x = PP p x
eval _ opts x = do
tt <- eval (Proxy @(Msg "!" p)) opts x
pure $ tt & tForest .~ []
data ReadFile p
type FileExists p = ReadFile p >> IsJust
instance (PP p x ~ String, P p x) => P (ReadFile p) x where
type PP (ReadFile p) x = Maybe String
eval _ opts x = do
let msg0 = "ReadFile"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
let msg1 = msg0 <> "[" <> p <> "]"
mb <- runIO $ do
b <- doesFileExist p
if b then Just <$> readFile p
else pure Nothing
pure $ case mb of
Nothing -> mkNode opts (FailT (msg1 <> " must run in IO")) [msg1 <> " must run in IO"] []
Just Nothing -> mkNode opts (PresentT Nothing) [msg1 <> " does not exist"] []
Just (Just b) -> mkNode opts (PresentT (Just b)) [msg1 <> " len=" <> show (length b) <> showLit0 opts " Just " b] []
data ReadDir p
type DirExists p = ReadDir p >> IsJust
instance (PP p x ~ String, P p x) => P (ReadDir p) x where
type PP (ReadDir p) x = Maybe [FilePath]
eval _ opts x = do
let msg0 = "ReadDir"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
let msg1 = msg0 <> "[" <> p <> "]"
mb <- runIO $ do
b <- doesDirectoryExist p
if b then Just <$> listDirectory p
else pure Nothing
pure $ case mb of
Nothing -> mkNode opts (FailT (msg1 <> " must run in IO")) [msg1 <> " must run in IO"] []
Just Nothing -> mkNode opts (PresentT Nothing) [msg1 <> " does not exist"] []
Just (Just b) -> mkNode opts (PresentT (Just b)) [msg1 <> " len=" <> show (length b) <> show0 opts " Just " b] []
data ReadEnv p
instance (PP p x ~ String, P p x) => P (ReadEnv p) x where
type PP (ReadEnv p) x = Maybe String
eval _ opts x = do
let msg0 = "ReadEnv"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
let msg1 = msg0 <> "[" <> p <> "]"
mb <- runIO $ lookupEnv p
pure $ case mb of
Nothing -> mkNode opts (FailT (msg1 <> " must run in IO")) [msg1 <> " must run in IO"] []
Just Nothing -> mkNode opts (PresentT Nothing) [msg1 <> " does not exist"] []
Just (Just v) -> mkNode opts (PresentT (Just v)) [msg1 <> showLit0 opts " " v] []
data ReadEnvAll
instance P ReadEnvAll a where
type PP ReadEnvAll a = [(String,String)]
eval _ opts _ = do
let msg0 = "ReadEnvAll"
mb <- runIO $ getEnvironment
pure $ case mb of
Nothing -> mkNode opts (FailT (msg0 <> " must run in IO")) [msg0 <> " must run in IO"] []
Just v -> mkNode opts (PresentT v) [msg0 <> " count=" <> show (length v)] []
data TimeUtc
instance P TimeUtc a where
type PP TimeUtc a = UTCTime
eval _ opts _a = do
let msg0 = "TimeUtc"
mb <- runIO $ getCurrentTime
pure $ case mb of
Nothing -> mkNode opts (FailT (msg0 <> " must run in IO")) [msg0 <> " must run in IO"] []
Just v -> mkNode opts (PresentT v) [msg0 <> show0 opts " " v] []
data TimeZt
instance P TimeZt a where
type PP TimeZt a = ZonedTime
eval _ opts _a = do
let msg0 = "TimeZt"
mb <- runIO $ getZonedTime
pure $ case mb of
Nothing -> mkNode opts (FailT (msg0 <> " must run in IO")) [msg0 <> " must run in IO"] []
Just v -> mkNode opts (PresentT v) [msg0 <> show0 opts " " v] []
data FHandle s = FStdout | FStderr | FOther s WFMode deriving Show
class GetFHandle (x :: FHandle Symbol) where getFHandle :: FHandle String
instance GetFHandle 'FStdout where getFHandle = FStdout
instance GetFHandle 'FStderr where getFHandle = FStderr
instance (GetMode w, KnownSymbol s) => GetFHandle ('FOther s w) where getFHandle = FOther (symb @s) (getMode @w)
data WFMode = WFAppend | WFWrite | WFWriteForce deriving (Show,Eq)
class GetMode (x :: WFMode) where getMode :: WFMode
instance GetMode 'WFAppend where getMode = WFAppend
instance GetMode 'WFWriteForce where getMode = WFWriteForce
instance GetMode 'WFWrite where getMode = WFWrite
data WriteFileImpl (hh :: FHandle Symbol) p
type AppendFile (s :: Symbol) p = WriteFileImpl ('FOther s 'WFAppend) p
type WriteFile' (s :: Symbol) p = WriteFileImpl ('FOther s 'WFWriteForce) p
type WriteFile (s :: Symbol) p = WriteFileImpl ('FOther s 'WFWrite) p
type Stdout p = WriteFileImpl 'FStdout p
type Stderr p = WriteFileImpl 'FStderr p
instance (GetFHandle fh
, P p a
, PP p a ~ String
) => P (WriteFileImpl fh p) a where
type PP (WriteFileImpl fh p) a = ()
eval _ opts a = do
let fh = getFHandle @fh
msg0 = case fh of
FStdout -> "Stdout"
FStderr -> "Stderr"
FOther s w -> (<>("[" <> s <> "]")) $ case w of
WFAppend -> "AppendFile"
WFWrite -> "WriteFile"
WFWriteForce -> "WriteFile'"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right ss -> do
mb <- runIO $ do
case fh of
FStdout -> fmap (left show) $ E.try @E.SomeException $ hPutStr stdout ss
FStderr -> fmap (left show) $ E.try @E.SomeException $ hPutStr stderr ss
FOther s w -> do
b <- doesFileExist s
if b && w == WFWrite then pure $ Left $ "file [" <> s <> "] already exists"
else do
let md = case w of
WFAppend -> AppendMode
_ -> WriteMode
fmap (left show) $ E.try @E.SomeException $ withFile s md (flip hPutStr ss)
pure $ case mb of
Nothing -> mkNode opts (FailT (msg0 <> " must run in IO")) [msg0 <> " must run in IO"] [hh pp]
Just (Left e) -> mkNode opts (FailT e) [msg0 <> " " <> e] [hh pp]
Just (Right ()) -> mkNode opts (PresentT ()) [msg0] [hh pp]
data Stdin
instance P Stdin a where
type PP Stdin a = String
eval _ opts _a = do
let msg0 = "Stdin"
mb <- runIO $ do
lr <- E.try $ hGetContents stdin
pure $ case lr of
Left (e :: E.SomeException) -> Left $ show e
Right ss -> Right ss
pure $ case mb of
Nothing -> mkNode opts (FailT (msg0 <> " must run in IO")) [msg0 <> " must run in IO"] []
Just (Left e) -> mkNode opts (FailT e) [msg0 <> " " <> e] []
Just (Right ss) -> mkNode opts (PresentT ss) [msg0 <> "[" <> showLit1 opts "" ss <> "]"] []
data IsFixImpl (cmp :: Ordering) (ignore :: Bool) p q
type IsPrefix p q = IsFixImpl 'LT 'False p q
type IsInfix p q = IsFixImpl 'EQ 'False p q
type IsSuffix p q = IsFixImpl 'GT 'False p q
type IsPrefixI p q = IsFixImpl 'LT 'True p q
type IsInfixI p q = IsFixImpl 'EQ 'True p q
type IsSuffixI p q = IsFixImpl 'GT 'True p q
instance (GetBool ignore
, P p x
, P q x
, PP p x ~ String
, PP q x ~ String
, GetOrdering cmp
) => P (IsFixImpl cmp ignore p q) x where
type PP (IsFixImpl cmp ignore p q) x = Bool
eval _ opts x = do
let cmp = getOrdering @cmp
ignore = getBool @ignore
lwr = if ignore then map toLower else id
(ff,msg0) = case cmp of
LT -> (isPrefixOf, "IsPrefix")
EQ -> (isInfixOf, "IsInfix")
GT -> (isSuffixOf, "IsSuffix")
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right s0 -> do
let msg1 = msg0 <> (if ignore then "I" else "") <> "(" <> s0 <> ")"
qq <- eval (Proxy @q) opts x
pure $ case getValueLR opts (msg1 <> " q failed") qq [hh pp] of
Left e -> e
Right s1 -> mkNodeB opts (on ff lwr s0 s1) [msg1 <> showLit0 opts " " s1] [hh pp, hh qq]
data p <> q
infixr 6 <>
type Sapa' (t :: Type) = Wrap t (Fst Id) <> Wrap t (Snd Id)
type Sapa = Fst Id <> Snd Id
instance (Semigroup (PP p x)
, PP p x ~ PP q x
, P p x
, Show (PP q x)
,P q x
) => P (p <> q) x where
type PP (p <> q) x = PP p x
eval _ opts x = do
let msg0 = "<>"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p <> q
in mkNode opts (PresentT d) [show p <> " <> " <> show q <> " = " <> show d] [hh pp, hh qq]
class PrintC x where
prtC :: (PrintfArg a, PrintfType r) => String -> (a,x) -> r
instance PrintC () where
prtC s (a,()) = printf s a
instance (PrintfArg a, PrintC rs) => PrintC (a,rs) where
prtC s (a,rs) = prtC s rs a
data PrintT s p
instance (PrintC bs
, (b,bs) ~ InductTupleP y
, InductTupleC y
, PrintfArg b
, PP s x ~ String
, PP p x ~ y
, P s x
, P p x
, CheckT (PP p x) ~ 'True
) => P (PrintT s p) x where
type PP (PrintT s p) x = String
eval _ opts x = do
let msg0 = "PrintT"
lrx <- runPQ msg0 (Proxy @s) (Proxy @p) opts x []
case lrx of
Left e -> pure e
Right (s,y,ss,pp) -> do
let msg1 = msg0
hhs = [hh ss, hh pp]
lr <- catchitNF @_ @E.SomeException (prtC @bs s (inductTupleC y))
pure $ case lr of
Left e -> mkNode opts (FailT (msg1 <> "(" <> e <> ")")) [msg1 <> " s=" <> s] hhs
Right ret -> mkNode opts (PresentT ret) [msg1 <> " [" <> showLit0 opts "" ret <> "]" <> showLit0 opts " | s=" s] hhs
data PrintL (n :: Nat) s p
instance (KnownNat n
, PrintC bs
, (b,bs) ~ InductListP n a
, InductListC n a
, PrintfArg b
, PP s x ~ String
, PP p x ~ [a]
, P s x
, P p x
) => P (PrintL n s p) x where
type PP (PrintL n s p) x = String
eval _ opts x = do
let msg0 = "PrintL(" ++ show n ++ ")"
n = nat @n
lrx <- runPQ msg0 (Proxy @s) (Proxy @p) opts x []
case lrx of
Left e -> pure e
Right (s,p,ss,pp) -> do
let hhs = [hh ss, hh pp]
if length p /= n then pure $ mkNode opts (FailT (msg0 <> " arg count=" ++ show (length p))) [msg0 <> " wrong length " ++ show (length p)] hhs
else do
lr <- catchitNF @_ @E.SomeException (prtC @bs s (inductListC @n @a p))
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> "(" <> e <> ")")) [msg0 <> " s=" <> s] hhs
Right ret -> mkNode opts (PresentT ret) [msg0 <> " [" <> showLit0 opts "" ret <> "]" <> showLit0 opts " | s=" s] hhs
type family CheckT (tp :: Type) :: Bool where
CheckT () = GL.TypeError ('GL.Text "Printfn: inductive tuple cannot be empty")
CheckT o = 'True
type family ApplyConstT (ta :: Type) (b :: Type) :: Type where
ApplyConstT (t a) b = t b
ApplyConstT ta b = GL.TypeError (
'GL.Text "ApplyConstT: (t a) b but found something else"
':$$: 'GL.Text "t a = "
':<>: 'GL.ShowType ta
':$$: 'GL.Text "b = "
':<>: 'GL.ShowType b)
data p <$ q
infixl 4 <$
instance (P p x
, P q x
, Show (PP p x)
, Functor t
, PP q x ~ t c
, ApplyConstT (PP q x) (PP p x) ~ t (PP p x)
) => P (p <$ q) x where
type PP (p <$ q) x = ApplyConstT (PP q x) (PP p x)
eval _ opts x = do
let msg0 = "(<$)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p <$ q
in mkNode opts (PresentT d) [msg0 <> show0 opts " " p] [hh pp, hh qq]
data p <* q
infixl 4 <*
type p *> q = q <* p
infixl 4 *>
instance (Show (t c)
, P p x
, P q x
, Show (t b)
, Applicative t
, t b ~ PP p x
, PP q x ~ t c
) => P (p <* q) x where
type PP (p <* q) x = PP p x
eval _ opts x = do
let msg0 = "(<*)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p <* q
in mkNode opts (PresentT d) [show01' opts msg0 p "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data p <|> q
infixl 3 <|>
instance (P p x
, P q x
, Show (t b)
, Alternative t
, t b ~ PP p x
, PP q x ~ t b
) => P (p <|> q) x where
type PP (p <|> q) x = PP p x
eval _ opts x = do
let msg0 = "(<|>)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p <|> q
in mkNode opts (PresentT d) [show01' opts msg0 d "p=" p <> show1 opts " | q=" q] [hh pp, hh qq]
data Extract
instance (Show (t a)
, Show a
, Comonad t
) => P Extract (t a) where
type PP Extract (t a) = a
eval _ opts ta =
let msg0 = "Extract"
d = extract ta
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d ta] []
data Duplicate
instance (Show (t a)
, Show (t (t a))
, Comonad t
) => P Duplicate (t a) where
type PP Duplicate (t a) = t (t a)
eval _ opts ta =
let msg0 = "Duplicate"
d = duplicate ta
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d ta] []
data Join
instance (Show (t (t a))
, Show (t a)
, Monad t
) => P Join (t (t a)) where
type PP Join (t (t a)) = t a
eval _ opts tta =
let msg0 = "Join"
d = join tta
in pure $ mkNode opts (PresentT d) [show01 opts msg0 d tta] []
data p $ q
infixl 0 $
instance (P p x
, P q x
, PP p x ~ (a -> b)
, FnT (PP p x) ~ b
, PP q x ~ a
, Show a
, Show b
) => P (p $ q) x where
type PP (p $ q) x = FnT (PP p x)
eval _ opts x = do
let msg0 = "($)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p q
in mkNode opts (PresentT d) ["fn $ " <> show q <> " = " <> show d] [hh pp, hh qq]
data q & p
infixr 1 &
instance (P p x
, P q x
, PP p x ~ (a -> b)
, FnT (PP p x) ~ b
, PP q x ~ a
, Show a
, Show b
) => P (q & p) x where
type PP (q & p) x = FnT (PP p x)
eval _ opts x = do
let msg0 = "(&)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p q
in mkNode opts (PresentT d) ["fn & " <> show q <> " = " <> show d] [hh pp, hh qq]
type family FnT ab :: Type where
FnT (a -> b) = b
FnT ab = GL.TypeError (
'GL.Text "FnT: expected Type -> Type but found a simple Type?"
':$$: 'GL.Text "ab = "
':<>: 'GL.ShowType ab)
data Trim' (left :: Bool) (right :: Bool) p
type Trim p = Trim' 'True 'True p
type TrimStart p = Trim' 'True 'False p
type TrimEnd p = Trim' 'False 'True p
instance (FailUnlessT (OrT l r)
('GL.Text "Trim': left and right cannot both be False")
, GetBool l
, GetBool r
, TL.IsText (PP p x)
, P p x
) => P (Trim' l r p) x where
type PP (Trim' l r p) x = PP p x
eval _ opts x = do
let msg0 = "Trim" ++ (if l && r then "" else if l then "Start" else "End")
l = getBool @l
r = getBool @r
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right (view TL.unpacked -> p) ->
let fl = if l then dropWhile isSpace else id
fr = if r then dropWhileEnd isSpace else id
b = (fl . fr) p
in mkNode opts (PresentT (b ^. TL.packed)) [msg0 <> showLit0 opts "" b <> showLit1 opts " | " p] [hh pp]
data StripLR (right :: Bool) p q
type StripRight p q = StripLR 'True p q
type StripLeft p q = StripLR 'False p q
instance (GetBool r
, PP p x ~ String
, P p x
, TL.IsText (PP q x)
, P q x
) => P (StripLR r p q) x where
type PP (StripLR r p q) x = Maybe (PP q x)
eval _ opts x = do
let msg0 = "Strip" ++ (if r then "Right" else "Left")
r = getBool @r
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,view TL.unpacked -> q,pp,qq) ->
let b = if r then
let (before,after) = splitAt (length q - length p) q
in if after == p then Just before else Nothing
else
let (before,after) = splitAt (length p) q
in if before == p then Just after else Nothing
in mkNode opts (PresentT (fmap (view TL.packed) b)) [msg0 <> show0 opts "" b <> showLit1 opts " | p=" p <> showLit1 opts " | q=" q] [hh pp, hh qq]
data Repeat (n :: Nat) p
instance (P (RepeatT n p) a
) => P (Repeat n p) a where
type PP (Repeat n p) a = PP (RepeatT n p) a
eval _ opts a =
eval (Proxy @(RepeatT n p)) opts a
data DoN (n :: Nat) p
instance (P (DoExpandT (RepeatT n p)) a
) => P (DoN n p) a where
type PP (DoN n p) a = PP (Do (RepeatT n p)) a
eval _ opts a =
eval (Proxy @(Do (RepeatT n p))) opts a
data JustDef p q
instance ( PP p x ~ a
, PP q x ~ Maybe a
, P p x
, P q x)
=> P (JustDef p q) x where
type PP (JustDef p q) x = MaybeT (PP q x)
eval _ opts x = do
let msg0 = "JustDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Just b -> pure $ mkNode opts (PresentT b) [msg0 <> " Just"] [hh qq]
Nothing -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right b -> mkNode opts (PresentT b) [msg0 <> " Nothing"] [hh qq, hh pp]
type family MaybeT mb where
MaybeT (Maybe a) = a
MaybeT o = GL.TypeError (
'GL.Text "MaybeT: expected 'Maybe a' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data JustFail p q
instance ( PP p x ~ String
, PP q x ~ Maybe a
, P p x
, P q x)
=> P (JustFail p q) x where
type PP (JustFail p q) x = MaybeT (PP q x)
eval _ opts x = do
let msg0 = "JustFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Just b -> pure $ mkNode opts (PresentT b) [msg0 <> " Just"] [hh qq]
Nothing -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " Nothing"] [hh qq, hh pp]
data LeftDef p q
instance ( PP q x ~ Either a b
, PP p (b,x) ~ a
, P q x
, P p (b,x)
) => P (LeftDef p q) x where
type PP (LeftDef p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Left a -> pure $ mkNode opts (PresentT a) [msg0 <> " Left"] [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) [msg0 <> " Right"] [hh qq, hh pp]
type family LeftT lr where
LeftT (Either a b) = a
LeftT o = GL.TypeError (
'GL.Text "LeftT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
type family RightT lr where
RightT (Either a b) = b
RightT o = GL.TypeError (
'GL.Text "RightT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data RightDef p q
instance ( PP q x ~ Either a b
, PP p (a,x) ~ b
, P q x
, P p (a,x)
) => P (RightDef p q) x where
type PP (RightDef p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Right b -> pure $ mkNode opts (PresentT b) [msg0 <> " Right"] [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) [msg0 <> " Left"] [hh qq, hh pp]
data LeftFail p q
instance ( PP p (b,x) ~ String
, PP q x ~ Either a b
, P p (b,x)
, P q x)
=> P (LeftFail p q) x where
type PP (LeftFail p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Left a -> pure $ mkNode opts (PresentT a) [msg0 <> " Left"] [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " Right"] [hh qq, hh pp]
data RightFail p q
instance ( PP p (a,x) ~ String
, PP q x ~ Either a b
, P p (a,x)
, P q x)
=> P (RightFail p q) x where
type PP (RightFail p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
Right b -> pure $ mkNode opts (PresentT b) [msg0 <> " Right"] [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " Left"] [hh qq, hh pp]
data ThisDef p q
instance ( PP q x ~ These a b
, PP p x ~ a
, P q x
, P p x
) => P (ThisDef p q) x where
type PP (ThisDef p q) x = ThisT (PP q x)
eval _ opts x = do
let msg0 = "ThisDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
This a -> pure $ mkNode opts (PresentT a) [msg0 <> " This"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
type family ThisT lr where
ThisT (These a b) = a
ThisT o = GL.TypeError (
'GL.Text "ThisT: expected 'These a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
type family ThatT lr where
ThatT (These a b) = b
ThatT o = GL.TypeError (
'GL.Text "ThatT: expected 'These a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
type family TheseT lr where
TheseT (These a b) = (a,b)
TheseT o = GL.TypeError (
'GL.Text "TheseT: expected 'These a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data ThatDef p q
instance ( PP q x ~ These a b
, PP p x ~ b
, P q x
, P p x
) => P (ThatDef p q) x where
type PP (ThatDef p q) x = ThatT (PP q x)
eval _ opts x = do
let msg0 = "ThatDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
That a -> pure $ mkNode opts (PresentT a) [msg0 <> " That"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
data TheseDef p q
instance ( PP q x ~ These a b
, PP p x ~ (a,b)
, P q x
, P p x
) => P (TheseDef p q) x where
type PP (TheseDef p q) x = TheseT (PP q x)
eval _ opts x = do
let msg0 = "TheseDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
These a b -> pure $ mkNode opts (PresentT (a,b)) [msg0 <> " These"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
data ThisFail p q
instance ( PP p x ~ String
, PP q x ~ These a b
, P p x
, P q x)
=> P (ThisFail p q) x where
type PP (ThisFail p q) x = ThisT (PP q x)
eval _ opts x = do
let msg0 = "ThisFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
This a -> pure $ mkNode opts (PresentT a) [msg0 <> " This"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
data ThatFail p q
instance ( PP p x ~ String
, PP q x ~ These a b
, P p x
, P q x)
=> P (ThatFail p q) x where
type PP (ThatFail p q) x = ThatT (PP q x)
eval _ opts x = do
let msg0 = "ThatFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
That a -> pure $ mkNode opts (PresentT a) [msg0 <> " That"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
data TheseFail p q
instance ( PP p x ~ String
, PP q x ~ These a b
, P p x
, P q x)
=> P (TheseFail p q) x where
type PP (TheseFail p q) x = TheseT (PP q x)
eval _ opts x = do
let msg0 = "TheseFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
case q of
These a b -> pure $ mkNode opts (PresentT (a,b)) [msg0 <> " These"] [hh qq]
_ -> do
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) [msg0 <> " " <> getTheseType q] [hh qq, hh pp]
getTheseType :: These a b -> String
getTheseType = \case
This {} -> "This"
That {} -> "That"
These {} -> "These"
data Head p
instance (Show (ConsT s)
, Show s
, Cons s s (ConsT s) (ConsT s)
, PP p x ~ s
, P p x
) => P (Head p) x where
type PP (Head p) x = ConsT (PP p x)
eval _ opts x = do
let msg0 = "Head"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p ^? _Cons of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " no data"] [hh pp]
Just (a,_) -> mkNode opts (PresentT a) [show01 opts msg0 a p] [hh pp]
data Tail p
instance (Show s
, Cons s s (ConsT s) (ConsT s)
, PP p x ~ s
, P p x
) => P (Tail p) x where
type PP (Tail p) x = PP p x
eval _ opts x = do
let msg0 = "Tail"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p ^? _Cons of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " no data"] [hh pp]
Just (_,as) -> mkNode opts (PresentT as) [show01 opts msg0 as p] [hh pp]
data Last p
instance (Show (ConsT s)
, Show s
, Snoc s s (ConsT s) (ConsT s)
, PP p x ~ s
, P p x
) => P (Last p) x where
type PP (Last p) x = ConsT (PP p x)
eval _ opts x = do
let msg0 = "Last"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p ^? _Snoc of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " no data"] [hh pp]
Just (_,a) -> mkNode opts (PresentT a) [show01 opts msg0 a p] [hh pp]
data Init p
instance (Show s
, Snoc s s (ConsT s) (ConsT s)
, PP p x ~ s
, P p x
) => P (Init p) x where
type PP (Init p) x = PP p x
eval _ opts x = do
let msg0 = "Init"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p ^? _Snoc of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " no data"] [hh pp]
Just (as,_) -> mkNode opts (PresentT as) [show01 opts msg0 as p] [hh pp]
data Just p
instance (Show a
, PP p x ~ Maybe a
, P p x
) => P (Just p) x where
type PP (Just p) x = MaybeT (PP p x)
eval _ opts x = do
let msg0 = "Just"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) [msg0 <> " found Nothing"] [hh pp]
Just d -> mkNode opts (PresentT d) [show01 opts msg0 d p] [hh pp]