{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wno-redundant-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 RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE DeriveLift #-}
module Predicate.Refined3 (
Refined3(r3In,r3Out)
, Refined3C
, prtEval3P
, prtEval3PIO
, prtEval3
, prt3IO
, prt3
, prt3Impl
, Msg3 (..)
, Results (..)
, RResults (..)
, mkProxy3
, mkProxy3'
, MakeR3
, eval3P
, eval3
, withRefined3TIO
, withRefined3T
, withRefined3TP
, newRefined3T
, newRefined3TP
, newRefined3TPIO
, convertRefined3TP
, rapply3
, rapply3P
, arbRefined3
, arbRefined3With
, unsafeRefined3
, unsafeRefined3'
, RefinedEmulate
, eval3PX
, eval3X
) where
import Predicate.Refined
import Predicate.Core
import Predicate.Util
import Data.Functor.Identity (Identity(..))
import Data.Tree
import Data.Proxy
import Control.Monad.Except
import Control.Monad.Writer (tell)
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
import System.Console.Pretty
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 Data.Maybe (fromMaybe)
import Control.Lens ((^?),ix)
import Data.Tree.Lens (root)
import Data.Char (isSpace)
data Refined3 ip op fmt i = Refined3 { r3In :: PP ip i, r3Out :: PP fmt (PP ip i) }
unsafeRefined3' :: forall ip op fmt i
. (Show i, Show (PP ip i), Refined3C ip op fmt i)
=> POpts
-> i
-> Refined3 ip op fmt i
unsafeRefined3' opts i =
let (ret,mr) = eval3 @ip @op @fmt opts i
in fromMaybe (error $ show (prt3Impl opts ret)) mr
unsafeRefined3 :: forall ip op fmt i . PP ip i -> PP fmt (PP ip i) -> Refined3 ip op fmt i
unsafeRefined3 = Refined3
type Refined3C ip op fmt i =
( 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 ip op fmt i)
deriving instance (Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined3 ip op fmt i)
deriving instance (TH.Lift (PP ip i), TH.Lift (PP fmt (PP ip i))) => TH.Lift (Refined3 ip op fmt i)
instance ( Eq i
, Show i
, Show (PP ip i)
, Refined3C ip op fmt i
, Read (PP ip i)
, Read (PP fmt (PP ip i))
) => Read (Refined3 ip op fmt i) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined3")
GR.expectP (RL.Punc "{")
fld1 <- GR.readField
"r3In" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc ",")
fld2 <- GR.readField
"r3Out" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc "}")
let (_ret,mr) = runIdentity $ eval3MSkip @_ @ip @op @fmt oz 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 ip op fmt i) where
toJSON = toJSON . r3Out
instance (Show ( PP fmt (PP ip i))
, Show (PP ip i)
, Refined3C ip op fmt i
, FromJSON i
) => FromJSON (Refined3 ip op fmt i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval3 @ip @op @fmt o2 i
case mr of
Nothing -> fail $ "Refined3:" ++ show (prt3Impl o2 ret)
Just r -> return r
arbRefined3 :: forall ip op fmt i .
( Arbitrary (PP ip i)
, Refined3C ip op fmt i
) => Proxy '(ip,op,fmt,i)
-> Gen (Refined3 ip op fmt i)
arbRefined3 _ = suchThatMap (arbitrary @(PP ip i)) $ eval3MQuickIdentity @ip @op @fmt
arbRefined3With ::
forall ip op fmt i
. (Arbitrary (PP ip i)
, Refined3C ip op fmt i)
=> Proxy '(ip,op,fmt,i)
-> (PP ip i -> PP ip i)
-> Gen (Refined3 ip op fmt i)
arbRefined3With _ f =
suchThatMap (f <$> arbitrary @(PP ip i)) $ eval3MQuickIdentity @ip @op @fmt
instance ( Show (PP fmt (PP ip i))
, Show (PP ip i)
, Refined3C ip op fmt i
, Binary i
) => Binary (Refined3 ip op fmt i) where
get = do
i <- B.get @i
let (ret,mr) = eval3 @ip @op @fmt o2 i
case mr of
Nothing -> fail $ "Refined3:" ++ show (prt3Impl o2 ret)
Just r -> return r
put (Refined3 _ r) = B.put @i r
mkProxy3 :: forall z ip op fmt i . z ~ '(ip,op,fmt,i) => Proxy '(ip,op,fmt,i)
mkProxy3 = Proxy
mkProxy3' :: forall z ip op fmt i . (z ~ '(ip,op,fmt,i), Refined3C ip op fmt i) => Proxy '(ip,op,fmt,i)
mkProxy3' = Proxy
type family MakeR3 p where
MakeR3 '(ip,op,fmt,i) = Refined3 ip op fmt i
withRefined3TIO :: forall ip op fmt i m b
. (MonadIO m, Refined3C ip op fmt i, Show (PP ip i), Show i)
=> POpts
-> i
-> (Refined3 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3TIO opts = (>>=) . newRefined3TPIO (Proxy @'(ip,op,fmt,i)) opts
withRefined3T :: forall ip op fmt i m b
. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i)
=> POpts
-> i
-> (Refined3 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3T opts = (>>=) . newRefined3TP (Proxy @'(ip,op,fmt,i)) opts
withRefined3TP :: forall m ip op fmt i b proxy
. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (Refined3 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined3TP p opts = (>>=) . newRefined3TP p opts
newRefined3T :: forall m ip op fmt i . (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i)
=> POpts
-> i
-> RefinedT m (Refined3 ip op fmt i)
newRefined3T = newRefined3TP (Proxy @'(ip,op,fmt,i))
newRefined3TP :: forall m ip op fmt i proxy
. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> RefinedT m (Refined3 ip op fmt i)
newRefined3TP = newRefined3TPImpl (return . runIdentity)
newRefined3TPIO :: forall m ip op fmt i proxy
. (Refined3C ip op fmt i
, MonadIO m
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> RefinedT m (Refined3 ip op fmt i)
newRefined3TPIO = newRefined3TPImpl liftIO
newRefined3TPImpl :: forall n m ip op fmt i proxy
. (Refined3C 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 '(ip,op,fmt,i)
-> POpts
-> i
-> RefinedT m (Refined3 ip op fmt i)
newRefined3TPImpl f _ opts i = do
(ret,mr) <- f $ eval3M opts i
let m3 = prt3Impl opts ret
tell [m3Long m3]
case mr of
Nothing -> throwError $ m3Desc m3 <> " | " <> m3Short m3
Just r -> return r
newRefined3TPSkipIPImpl :: forall n m ip op fmt i proxy
. (Refined3C 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 '(ip,op,fmt,i)
-> POpts
-> PP ip i
-> RefinedT m (Refined3 ip op fmt i)
newRefined3TPSkipIPImpl f _ opts a = do
(ret,mr) <- f $ eval3MSkip opts a
let m3 = prt3Impl opts ret
tell [m3Long m3]
case mr of
Nothing -> throwError $ m3Desc m3 <> " | " <> m3Short m3
Just r -> return r
convertRefined3TP :: forall m ip op fmt i ip1 op1 fmt1 i1 .
( Refined3C ip1 op1 fmt1 i1
, Monad m
, Show (PP ip i)
, PP ip i ~ PP ip1 i1
, Show i1)
=> Proxy '(ip, op, fmt, i)
-> Proxy '(ip1, op1, fmt1, i1)
-> POpts
-> RefinedT m (Refined3 ip op fmt i)
-> RefinedT m (Refined3 ip1 op1 fmt1 i1)
convertRefined3TP _ _ opts ma = do
Refined3 x _ <- ma
Refined3 a b <- newRefined3TPSkipIPImpl (return . runIdentity) (Proxy @'(ip1, op1, fmt1, i1)) opts x
return (Refined3 a b)
rapply3 :: forall m ip op fmt i .
( Refined3C ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> POpts
-> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined3 ip op fmt i)
-> RefinedT m (Refined3 ip op fmt i)
-> RefinedT m (Refined3 ip op fmt i)
rapply3 = rapply3P (Proxy @'(ip,op,fmt,i))
rapply3P :: forall m ip op fmt i proxy .
( Refined3C ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined3 ip op fmt i)
-> RefinedT m (Refined3 ip op fmt i)
-> RefinedT m (Refined3 ip op fmt i)
rapply3P p opts f ma mb = do
tell [bgColor Blue "=== a ==="]
Refined3 x _ <- ma
tell [bgColor Blue "=== b ==="]
Refined3 y _ <- mb
tell [bgColor Blue "=== a `op` b ==="]
Refined3 a b <- newRefined3TPSkipIPImpl (return . runIdentity) p opts (f x y)
return (Refined3 a b)
data Results a b =
XF String
| XTF a String
| XTFalse a
| XTTrueF a String
| XTTrueT a b
deriving (Show,Eq)
data RResults 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
prtEval3PIO :: forall ip op fmt i proxy
. ( Refined3C ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> IO (Either String (Refined3 ip op fmt i))
prtEval3PIO _ opts i = do
x <- eval3M opts i
prt3IO opts x
prtEval3 :: forall ip op fmt i
. ( Refined3C ip op fmt i
, Show (PP ip i)
, Show i)
=> POpts
-> i
-> Either Msg3 (Refined3 ip op fmt i)
prtEval3 = prtEval3P Proxy
prtEval3P :: forall ip op fmt i proxy
. ( Refined3C ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> Either Msg3 (Refined3 ip op fmt i)
prtEval3P _ opts = prt3 opts . eval3 opts
eval3P :: forall ip op fmt i proxy . Refined3C ip op fmt i
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
eval3P _ opts = runIdentity . eval3M opts
eval3 :: forall ip op fmt i . Refined3C ip op fmt i
=> POpts
-> i
-> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
eval3 = eval3P Proxy
eval3M :: forall m ip op fmt i . (MonadEval m, Refined3C ip op fmt i)
=> POpts
-> i
-> m (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
eval3M opts i = do
ll@(fromTT -> t1) <- eval (Proxy @ip) opts i
case getValLR (_tBool ll) of
Right a -> do
rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a
case getValLR (_tBool rr) of
Right True -> do
ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a
pure $ case getValLR (_tBool ss) of
Right b -> (RTTrueT a t1 t2 b t3, Just (Refined3 a b))
Left e -> (RTTrueF a t1 t2 e t3, Nothing)
Right False -> pure (RTFalse a t1 t2, Nothing)
Left e -> pure (RTF a t1 e t2, Nothing)
Left e -> pure (RF e t1, Nothing)
eval3MSkip :: forall m ip op fmt i . (MonadEval m, Refined3C ip op fmt i)
=> POpts
-> PP ip i
-> m (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
eval3MSkip opts a = do
rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a
case getValLR (_tBool rr) of
Right True -> do
ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a
pure $ case getValLR (_tBool ss) of
Right b -> (RTTrueT a mkNodeSkipP t2 b t3, Just (Refined3 a b))
Left e -> (RTTrueF a mkNodeSkipP t2 e t3, Nothing)
Right False -> pure (RTFalse a mkNodeSkipP t2, Nothing)
Left e -> pure (RTF a mkNodeSkipP e t2, Nothing)
eval3MQuickIdentity :: forall ip op fmt i . Refined3C ip op fmt i
=> PP ip i
-> Maybe (Refined3 ip op fmt i)
eval3MQuickIdentity = runIdentity . eval3MQuick
eval3MQuick :: forall m ip op fmt i . (MonadEval m, Refined3C ip op fmt i)
=> PP ip i
-> m (Maybe (Refined3 ip op fmt i))
eval3MQuick a = do
let opts = oz
rr <- evalBool (Proxy @op) opts a
case getValLR (_tBool rr) of
Right True -> do
ss <- eval (Proxy @fmt) opts a
pure $ case getValLR (_tBool ss) of
Right b -> Just (Refined3 a b)
_ -> Nothing
_ -> pure Nothing
prt3IO :: (Show a, Show b) => POpts -> (RResults a b, Maybe r) -> IO (Either String r)
prt3IO opts (ret,mr) = do
let m3 = prt3Impl opts ret
unless (hasNoTree opts) $ putStrLn $ m3Long m3
return $ maybe (Left (m3Desc m3 <> " | " <> m3Short m3)) Right mr
prt3 :: (Show a, Show b) => POpts -> (RResults a b, Maybe r) -> Either Msg3 r
prt3 opts (ret,mr) = maybe (Left $ prt3Impl opts ret) 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 :: (Show a, Show b)
=> POpts
-> RResults a b
-> Msg3
prt3Impl opts v =
let outmsg msg = "\n*** " <> 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 = case t2 ^? root . pStrings . ix 0 of
Just w -> if null (dropWhile isSpace w) then "FalseP" else "{" <> w <> "}"
Nothing -> "FalseP"
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 ip op fmt i proxy . Refined3C ip op fmt i
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
eval3PX _ opts i = runIdentity $ do
ll@(fromTT -> t1) <- eval (Proxy @ip) opts i
case getValLR (_tBool ll) of
Right a -> do
rr@(fromTT -> t2) <- evalBool (Proxy @op) opts a
case getValLR (_tBool rr) of
Right True -> do
ss@(fromTT -> t3) <- eval (Proxy @fmt) opts a
pure $ case getValLR (_tBool ss) of
Right b -> (RTTrueT a t1 t2 b t3, Just (unsafeRefined a, b))
Left e -> (RTTrueF a t1 t2 e t3, Nothing)
Right False -> pure (RTFalse a t1 t2, Nothing)
Left e -> pure (RTF a t1 e t2, Nothing)
Left e -> pure (RF e t1, Nothing)
eval3X :: forall ip op fmt i . Refined3C ip op fmt i
=> POpts
-> i
-> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
eval3X = eval3PX (Proxy @'(ip,op,fmt,i))
type RefinedEmulate p a = Refined3 Id p Id a