{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wno-redundant-constraints #-}
{-# LANGUAGE BangPatterns #-}
{-# 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 RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Refined3 (
Refined3(r3In,r3Out)
, Refined3C
, prtEval3
, prtEval3P
, prtEval3IO
, prtEval3PIO
, prt3IO
, prt3Impl
, Msg3 (..)
, RResults3 (..)
, eval3
, eval3P
, eval3M
, newRefined3
, newRefined3P
, newRefined3T
, newRefined3TP
, newRefined3TPIO
, newRefined3TIO
, withRefined3T
, withRefined3TIO
, withRefined3TP
, mkProxy3
, mkProxy3'
, MakeR3
, MakeR3'
, unsafeRefined3
, unsafeRefined3'
, convertRefined3TP
, rapply3
, rapply3P
, genRefined3
, genRefined3P
, RefinedEmulate
, eval3PX
, eval3X
, type ReplaceOptT3
, type AppendOptT3
) where
import Predicate.Refined
import Predicate.Core
import Predicate.Util
import Data.Functor.Identity (Identity(..))
import Data.Tree
import Data.Proxy
import Control.Arrow (left)
import Control.Monad.Except
import Control.Monad.Writer (tell)
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
import Test.QuickCheck
import qualified GHC.Read as GR
import qualified Text.ParserCombinators.ReadPrec as PCR
import qualified Text.Read.Lex as RL
import qualified Data.Binary as B
import Data.Binary (Binary)
import Control.Lens ((^.))
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String
import Data.Hashable (Hashable(..))
import GHC.Stack
data Refined3 (opts :: OptT) ip op fmt i = Refined3 { r3In :: !(PP ip i), r3Out :: !(PP fmt (PP ip i)) }
type role Refined3 nominal nominal nominal nominal nominal
unsafeRefined3' :: forall opts ip op fmt i
. ( HasCallStack
, Show i
, Show (PP ip i)
, Refined3C opts ip op fmt i)
=> i
-> Refined3 opts ip op fmt i
unsafeRefined3' i =
let (ret,mr) = eval3 @opts @ip @op @fmt i
in case mr of
Nothing -> error $ show (prt3Impl (getOptT @opts) ret)
Just r -> r
unsafeRefined3 ::
forall opts ip op fmt i
. PP ip i
-> PP fmt (PP ip i)
-> Refined3 opts ip op fmt i
unsafeRefined3 = Refined3
type Refined3C opts ip op fmt i =
( OptTC opts
, P ip i
, P op (PP ip i)
, PP op (PP ip i) ~ Bool
, P fmt (PP ip i)
, PP fmt (PP ip i) ~ i
)
deriving instance ( Show i
, Show (PP ip i)
, Show (PP fmt (PP ip i))
) => Show (Refined3 opts ip op fmt i)
deriving instance ( Eq i
, Eq (PP ip i)
, Eq (PP fmt (PP ip i))
) => Eq (Refined3 opts ip op fmt i)
deriving instance ( TH.Lift (PP ip i)
, TH.Lift (PP fmt (PP ip i))
) => TH.Lift (Refined3 opts ip op fmt i)
instance (Refined3C opts ip op fmt String, Show (PP ip String))
=> IsString (Refined3 opts ip op fmt String) where
fromString s =
let (ret,mr) = eval3 @opts @ip @op @fmt s
in case mr of
Nothing -> error $ "Refined3(fromString):" ++ show (prt3Impl (getOptT @opts) ret)
Just r -> r
instance ( Eq i
, Show i
, Show (PP ip i)
, Refined3C opts ip op fmt i
, Read (PP ip i)
, Read (PP fmt (PP ip i))
) => Read (Refined3 opts ip op fmt i) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined3")
GR.expectP (RL.Punc "{")
fld1 <- readField
"r3In" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc ",")
fld2 <- readField
"r3Out" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc "}")
let (_ret,mr) = runIdentity $ eval3MSkip @opts @ip @op @fmt fld1
case mr of
Nothing -> fail ""
Just (Refined3 _r1 r2)
| r2 == fld2 -> pure (Refined3 fld1 fld2)
| otherwise -> fail ""
))
readList = GR.readListDefault
readListPrec = GR.readListPrecDefault
instance ToJSON (PP fmt (PP ip i)) => ToJSON (Refined3 opts ip op fmt i) where
toJSON = toJSON . r3Out
instance (Show (PP fmt (PP ip i))
, Show (PP ip i)
, Refined3C opts ip op fmt i
, FromJSON i
) => FromJSON (Refined3 opts ip op fmt i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval3 @opts @ip @op @fmt i
case mr of
Nothing -> fail $ "Refined3:" ++ show (prt3Impl (getOptT @opts) ret)
Just r -> return r
instance ( Arbitrary (PP ip i)
, Refined3C opts ip op fmt i
) => Arbitrary (Refined3 opts ip op fmt i) where
arbitrary = genRefined3 arbitrary
genRefined3 ::
forall opts ip op fmt i
. Refined3C opts ip op fmt i
=> Gen (PP ip i)
-> Gen (Refined3 opts ip op fmt i)
genRefined3 = genRefined3P Proxy
genRefined3P ::
forall opts ip op fmt i
. Refined3C opts ip op fmt i
=> Proxy '(opts,ip,op,fmt,i)
-> Gen (PP ip i)
-> Gen (Refined3 opts ip op fmt i)
genRefined3P _ g =
let o = getOptT @opts
f !cnt = do
mppi <- suchThatMaybe g (\a -> getValLRFromTT (runIdentity (eval @_ (Proxy @op) o a)) == Right True)
case mppi of
Nothing ->
if cnt >= oRecursion o
then error $ setOtherEffects o ("genRefined3P recursion exceeded(" ++ show (oRecursion o) ++ ")")
else f (cnt+1)
Just ppi -> do
let lr = getValLRFromTT (runIdentity (eval @_ (Proxy @fmt) o ppi))
case lr of
Left e -> error $ "genRefined3P: formatting failed!! " ++ e
Right r -> pure $ unsafeRefined3 ppi r
in f 0
instance ( Show (PP fmt (PP ip i))
, Show (PP ip i)
, Refined3C opts ip op fmt i
, Binary i
) => Binary (Refined3 opts ip op fmt i) where
get = do
i <- B.get @i
let (ret,mr) = eval3 @opts @ip @op @fmt i
case mr of
Nothing -> fail $ "Refined3:" ++ show (prt3Impl (getOptT @opts) ret)
Just r -> return r
put (Refined3 _ r) = B.put @i r
instance (Refined3C opts ip op fmt i
, Hashable (PP ip i)
) => Hashable (Refined3 opts ip op fmt i) where
hashWithSalt s (Refined3 a _) = s + hash a
mkProxy3 ::
forall z opts ip op fmt i
. z ~ '(opts,ip,op,fmt,i)
=> Proxy '(opts,ip,op,fmt,i)
mkProxy3 = Proxy
mkProxy3' :: forall z opts ip op fmt i . (z ~ '(opts,ip,op,fmt,i), Refined3C opts ip op fmt i) => Proxy '(opts,ip,op,fmt,i)
mkProxy3' = Proxy
type family MakeR3 p where
MakeR3 '(opts,ip,op,fmt,i) = Refined3 opts ip op fmt i
type family MakeR3' opts p where
MakeR3' opts '(ip,op,fmt,i) = Refined3 opts ip op fmt i
withRefined3TIO :: forall opts ip op fmt i m b
. ( MonadIO m
, Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> i
-> (Refined3 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3TIO = (>>=) . newRefined3TPIO (Proxy @'(opts,ip,op,fmt,i))
withRefined3T :: forall opts ip op fmt i m b
. ( Monad m
, Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> i
-> (Refined3 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3T = (>>=) . newRefined3TP (Proxy @'(opts,ip,op,fmt,i))
withRefined3TP :: forall opts ip op fmt i b proxy m
. ( Monad m
, Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (Refined3 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3TP p = (>>=) . newRefined3TP p
newRefined3 :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> i
-> Either String (Refined3 opts ip op fmt i)
newRefined3 = newRefined3P Proxy
newRefined3P :: forall opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> Either String (Refined3 opts ip op fmt i)
newRefined3P _ x =
let (lr,xs) = runIdentity $ unRavelT $ newRefined3T @opts @ip @op @fmt x
in left (\e -> e ++ (if all null xs then "" else "\n" ++ unlines xs)) lr
newRefined3T :: forall opts ip op fmt i m
. ( Refined3C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i
)
=> i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3T = newRefined3TP (Proxy @'(opts,ip,op,fmt,i))
newRefined3TP :: forall opts ip op fmt i proxy m
. ( Refined3C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3TP = newRefined3TPImpl (return . runIdentity)
newRefined3TIO :: forall opts ip op fmt i m
. ( Refined3C opts ip op fmt i
, MonadIO m
, Show (PP ip i)
, Show i)
=> i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3TIO = newRefined3TPImpl liftIO Proxy
newRefined3TPIO :: forall opts ip op fmt i proxy m
. ( Refined3C opts ip op fmt i
, MonadIO m
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3TPIO = newRefined3TPImpl liftIO
newRefined3TPImpl :: forall n m opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
, Monad m
, MonadEval n
, Show (PP ip i)
, Show (PP fmt (PP ip i)))
=> (forall x . n x -> RefinedT m x)
-> proxy '(opts,ip,op,fmt,i)
-> i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3TPImpl f _ i = do
(ret,mr) <- f $ eval3M i
let m3 = prt3Impl (getOptT @opts) ret
tell [m3Long m3]
case mr of
Nothing -> throwError $ m3Desc m3 <> " | " <> m3Short m3
Just r -> return r
newRefined3TPSkipIPImpl :: forall n m opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
, Monad m
, MonadEval n
, Show (PP ip i)
, Show (PP fmt (PP ip i))
)
=> (forall x . n x -> RefinedT m x)
-> proxy '(opts,ip,op,fmt,i)
-> PP ip i
-> RefinedT m (Refined3 opts ip op fmt i)
newRefined3TPSkipIPImpl f _ a = do
(ret,mr) <- f $ eval3MSkip a
let m3 = prt3Impl (getOptT @opts) ret
tell [m3Long m3]
case mr of
Nothing -> throwError $ m3Desc m3 <> " | " <> m3Short m3
Just r -> return r
convertRefined3TP :: forall opts ip op fmt i ip1 op1 fmt1 i1 m .
( Refined3C opts ip op fmt i
, Refined3C opts ip1 op1 fmt1 i1
, Monad m
, Show (PP ip i)
, PP ip i ~ PP ip1 i1
, Show i1)
=> Proxy '(opts, ip, op, fmt, i)
-> Proxy '(opts, ip1, op1, fmt1, i1)
-> RefinedT m (Refined3 opts ip op fmt i)
-> RefinedT m (Refined3 opts ip1 op1 fmt1 i1)
convertRefined3TP _ _ ma = do
Refined3 x _ <- ma
Refined3 a b <- newRefined3TPSkipIPImpl (return . runIdentity) (Proxy @'(opts, ip1, op1, fmt1, i1)) x
return (Refined3 a b)
rapply3 :: forall opts ip op fmt i m .
( Refined3C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined3 opts ip op fmt i)
-> RefinedT m (Refined3 opts ip op fmt i)
-> RefinedT m (Refined3 opts ip op fmt i)
rapply3 = rapply3P (Proxy @'(opts,ip,op,fmt,i))
rapply3P :: forall opts ip op fmt i proxy m .
( Refined3C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined3 opts ip op fmt i)
-> RefinedT m (Refined3 opts ip op fmt i)
-> RefinedT m (Refined3 opts ip op fmt i)
rapply3P p f ma mb = do
let opts = getOptT @opts
tell [setOtherEffects opts "=== a ==="]
Refined3 x _ <- ma
tell [setOtherEffects opts "=== b ==="]
Refined3 y _ <- mb
tell [setOtherEffects opts "=== a `op` b ==="]
newRefined3TPSkipIPImpl (return . runIdentity) p (f x y)
data RResults3 a b =
RF !String !(Tree PE)
| RTF !a !(Tree PE) !String !(Tree PE)
| RTFalse !a !(Tree PE) !(Tree PE)
| RTTrueF !a !(Tree PE) !(Tree PE) !String !(Tree PE)
| RTTrueT !a !(Tree PE) !(Tree PE) !b !(Tree PE)
deriving Show
prtEval3IO :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> i
-> IO (Either String (Refined3 opts ip op fmt i))
prtEval3IO = prtEval3PIO Proxy
prtEval3PIO :: forall opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> IO (Either String (Refined3 opts ip op fmt i))
prtEval3PIO _ i = do
x <- eval3M i
prt3IO @opts x
prtEval3 :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> i
-> Either Msg3 (Refined3 opts ip op fmt i)
prtEval3 = prtEval3P Proxy
prtEval3P :: forall opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> Either Msg3 (Refined3 opts ip op fmt i)
prtEval3P _ i =
let (ret,mr) = eval3 i
in maybe (Left $ prt3Impl (getOptT @opts) ret) Right mr
eval3 :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
)
=> i
-> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 opts ip op fmt i))
eval3 = eval3P Proxy
eval3P :: forall opts ip op fmt i proxy
. ( Refined3C opts ip op fmt i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 opts ip op fmt i))
eval3P _ = runIdentity . eval3M
eval3M :: forall opts ip op fmt i m
. ( MonadEval m
, Refined3C opts ip op fmt i
)
=> i
-> m (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 opts ip op fmt i))
eval3M i = do
let o = getOptT @opts
ll <- eval (Proxy @ip) o i
case getValAndPE ll of
(Right a, t1) -> do
rr <- evalBool (Proxy @op) o a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) o a
pure $ case getValAndPE ss of
(Right b,t3) -> (RTTrueT a t1 t2 b t3, Just (Refined3 a b))
(Left e,t3) -> (RTTrueF a t1 t2 e t3, Nothing)
(Right False,t2) -> pure (RTFalse a t1 t2, Nothing)
(Left e,t2) -> pure (RTF a t1 e t2, Nothing)
(Left e,t1) -> pure (RF e t1, Nothing)
eval3MSkip :: forall opts ip op fmt i m
. ( MonadEval m
, Refined3C opts ip op fmt i
)
=> PP ip i
-> m (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 opts ip op fmt i))
eval3MSkip a = do
let o = getOptT @opts
rr <- evalBool (Proxy @op) o a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) o a
pure $ case getValAndPE ss of
(Right b,t3) -> (RTTrueT a mkNodeSkipP t2 b t3, Just (Refined3 a b))
(Left e,t3) -> (RTTrueF a mkNodeSkipP t2 e t3, Nothing)
(Right False,t2) -> pure (RTFalse a mkNodeSkipP t2, Nothing)
(Left e,t2) -> pure (RTF a mkNodeSkipP e t2, Nothing)
prt3IO :: forall opts a b r .
(OptTC opts, Show a, Show b)
=> (RResults3 a b, Maybe r)
-> IO (Either String r)
prt3IO (ret,mr) = do
let m3 = prt3Impl (getOptT @opts) ret
unless (hasNoTree (getOptT @opts)) $ putStrLn $ m3Long m3
return $ maybe (Left (m3Desc m3 <> " | " <> m3Short m3)) Right mr
data Msg3 = Msg3 { m3Desc :: !String
, m3Short :: !String
, m3Long :: !String
} deriving Eq
instance Show Msg3 where
show (Msg3 a b c) = a <> " | " <> b <> (if null c then "" else "\n" <> c)
prt3Impl :: forall a b . (Show a, Show b)
=> POpts
-> RResults3 a b
-> Msg3
prt3Impl opts v =
let outmsg msg = "\n*** " <> formatOMsg opts " " <> msg <> " ***\n\n"
msg1 a = outmsg ("Step 1. Success Initial Conversion(ip) (" ++ show a ++ ")")
mkMsg3 m n r | hasNoTree opts = Msg3 m n ""
| otherwise = Msg3 m n r
in case v of
RF e t1 ->
let (m,n) = ("Step 1. Initial Conversion(ip) Failed", e)
r = outmsg m
<> prtTreePure opts t1
in mkMsg3 m n r
RTF a t1 e t2 ->
let (m,n) = ("Step 2. Failed Boolean Check(op)", e)
r = msg1 a
<> fixLite opts a t1
<> outmsg m
<> prtTreePure opts t2
in mkMsg3 m n r
RTFalse a t1 t2 ->
let (m,n) = ("Step 2. False Boolean Check(op)", z)
z = let w = t2 ^. root . pString
in if all isSpace w then "FalseP" else "{" <> w <> "}"
r = msg1 a
<> fixLite opts a t1
<> outmsg m
<> prtTreePure opts t2
in mkMsg3 m n r
RTTrueF a t1 t2 e t3 ->
let (m,n) = ("Step 3. Failed Output Conversion(fmt)", e)
r = msg1 a
<> fixLite opts a t1
<> outmsg "Step 2. Success Boolean Check(op)"
<> prtTreePure opts t2
<> outmsg m
<> prtTreePure opts t3
in mkMsg3 m n r
RTTrueT a t1 t2 b t3 ->
let (m,n) = ("Step 3. Success Output Conversion(fmt)", show b)
r = msg1 a
<> fixLite opts a t1
<> outmsg "Step 2. Success Boolean Check(op)"
<> prtTreePure opts t2
<> outmsg m
<> fixLite opts b t3
in mkMsg3 m n r
eval3PX :: forall opts ip op fmt i proxy
. Refined3C opts ip op fmt i
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
eval3PX _ i = runIdentity $ do
let o = getOptT @opts
ll <- eval (Proxy @ip) o i
case getValAndPE ll of
(Right a,t1) -> do
rr <- evalBool (Proxy @op) o a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) o a
pure $ case getValAndPE ss of
(Right b,t3) -> (RTTrueT a t1 t2 b t3, Just (unsafeRefined a, b))
(Left e,t3) -> (RTTrueF a t1 t2 e t3, Nothing)
(Right False,t2) -> pure (RTFalse a t1 t2, Nothing)
(Left e,t2) -> pure (RTF a t1 e t2, Nothing)
(Left e,t1) -> pure (RF e t1, Nothing)
eval3X :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
)
=> i
-> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
eval3X = eval3PX (Proxy @'(opts,ip,op,fmt,i))
type RefinedEmulate (opts :: OptT) p a = Refined3 opts Id p Id a
type family ReplaceOptT3 (o :: OptT) t where
ReplaceOptT3 o (Refined3 _ ip op fmt i) = Refined3 o ip op fmt i
type family AppendOptT3 (o :: OptT) t where
AppendOptT3 o (Refined3 o' ip op fmt i) = Refined3 (o' ':# o) ip op fmt i