{-# 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 DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Refined1 (
Refined1(unRefined1)
, Refined1C
, prtEval1
, prtEval1P
, prtEval1PIO
, prt1IO
, prt1
, prt1Impl
, Msg1 (..)
, RResults1 (..)
, eval1
, eval1P
, newRefined1T
, newRefined1TP
, newRefined1TPIO
, withRefined1T
, withRefined1TIO
, withRefined1TP
, mkProxy1
, mkProxy1'
, MakeR1
, unsafeRefined1
, unsafeRefined1'
, convertRefined1TP
, rapply1
, rapply1P
, arbRefined1
, arbRefined1With
, RefinedEmulate
, eval1PX
, eval1X
, T4_1
, T4_2
, T4_3
, T4_4
) 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)
import Data.String
import Data.Hashable (Hashable(..))
import GHC.Stack
newtype Refined1 ip op fmt i = Refined1 { unRefined1 :: PP ip i }
type role Refined1 nominal nominal nominal nominal
unsafeRefined1' :: forall ip op fmt i
. (HasCallStack, Show i, Show (PP ip i), Refined1C ip op fmt i)
=> POpts
-> i
-> Refined1 ip op fmt i
unsafeRefined1' opts i =
let (ret,mr) = eval1 @ip @op @fmt opts i
in fromMaybe (error $ show (prt1Impl opts ret)) mr
unsafeRefined1 :: forall ip op fmt i . PP ip i -> Refined1 ip op fmt i
unsafeRefined1 = Refined1
type Refined1C 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 (Refined1 ip op fmt i)
deriving instance (Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined1 ip op fmt i)
deriving instance (TH.Lift (PP ip i), TH.Lift (PP fmt (PP ip i))) => TH.Lift (Refined1 ip op fmt i)
instance (Refined1C ip op fmt String, Show (PP ip String)) => IsString (Refined1 ip op fmt String) where
fromString s =
let (ret,mr) = eval1 @ip @op @fmt o2 s
in fromMaybe (error $ "Refined1(fromString):" ++ show (prt1Impl o2 ret)) mr
instance ( Eq i
, Show i
, Eq (PP ip i)
, Show (PP ip i)
, Refined1C ip op fmt i
, Read (PP ip i)
, Read (PP fmt (PP ip i))
) => Read (Refined1 ip op fmt i) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined1")
GR.expectP (RL.Punc "{")
fld1 <- readField
"unRefined1" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc "}")
let (_ret,mr) = runIdentity $ eval1MSkip @_ @ip @op @fmt oz fld1
case mr of
Nothing -> fail ""
Just (Refined1 r1)
| r1 == fld1 -> pure (Refined1 r1)
| otherwise -> fail ""
))
readList = GR.readListDefault
readListPrec = GR.readListPrecDefault
instance (Show (PP fmt (PP ip i)), ToJSON (PP fmt (PP ip i)), P fmt (PP ip i)) => ToJSON (Refined1 ip op fmt i) where
toJSON (Refined1 x) =
let ss = runIdentity $ eval (Proxy @fmt) o2 x
in case getValAndPE ss of
(Right b,_) -> toJSON b
(Left e,t3) -> error $ "oops tojson failed " ++ show e ++ " t3=" ++ show t3
instance (Show ( PP fmt (PP ip i))
, Show (PP ip i)
, Refined1C ip op fmt i
, FromJSON i
) => FromJSON (Refined1 ip op fmt i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval1 @ip @op @fmt o2 i
case mr of
Nothing -> fail $ "Refined1:" ++ show (prt1Impl o2 ret)
Just r -> return r
arbRefined1 :: forall ip op fmt i .
( Arbitrary (PP ip i)
, Refined1C ip op fmt i
) => Proxy '(ip,op,fmt,i)
-> Gen (Refined1 ip op fmt i)
arbRefined1 = flip arbRefined1With id
arbRefined1With ::
forall ip op fmt i
. (Arbitrary (PP ip i)
, Refined1C ip op fmt i)
=> Proxy '(ip,op,fmt,i)
-> (PP ip i -> PP ip i)
-> Gen (Refined1 ip op fmt i)
arbRefined1With _ f =
suchThatMap (f <$> arbitrary @(PP ip i)) $ eval1MQuickIdentity @ip @op @fmt
instance ( Show (PP fmt (PP ip i))
, Show (PP ip i)
, Refined1C ip op fmt i
, Binary i
) => Binary (Refined1 ip op fmt i) where
get = do
i <- B.get @i
let (ret,mr) = eval1 @ip @op @fmt o2 i
case mr of
Nothing -> fail $ "Refined1:" ++ show (prt1Impl o2 ret)
Just r -> return r
put (Refined1 x) =
let ss = runIdentity $ eval (Proxy @fmt) o2 x
in case getValAndPE ss of
(Right b,_) -> B.put @i b
(Left e,t3) -> error $ "oops tojson failed " ++ show e ++ " t3=" ++ show t3
instance (Refined1C ip op fmt i
, Hashable (PP ip i)
) => Hashable (Refined1 ip op fmt i) where
hashWithSalt s (Refined1 a) = s + hash a
mkProxy1 :: forall z ip op fmt i . z ~ '(ip,op,fmt,i) => Proxy '(ip,op,fmt,i)
mkProxy1 = Proxy
mkProxy1' :: forall z ip op fmt i . (z ~ '(ip,op,fmt,i), Refined1C ip op fmt i) => Proxy '(ip,op,fmt,i)
mkProxy1' = Proxy
type family MakeR1 p where
MakeR1 '(ip,op,fmt,i) = Refined1 ip op fmt i
withRefined1TIO :: forall ip op fmt i m b
. (MonadIO m, Refined1C ip op fmt i, Show (PP ip i), Show i)
=> POpts
-> i
-> (Refined1 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1TIO opts = (>>=) . newRefined1TPIO (Proxy @'(ip,op,fmt,i)) opts
withRefined1T :: forall ip op fmt i m b
. (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i)
=> POpts
-> i
-> (Refined1 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1T opts = (>>=) . newRefined1TP (Proxy @'(ip,op,fmt,i)) opts
withRefined1TP :: forall m ip op fmt i b proxy
. (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (Refined1 ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1TP p opts = (>>=) . newRefined1TP p opts
newRefined1T :: forall m ip op fmt i . (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i)
=> POpts
-> i
-> RefinedT m (Refined1 ip op fmt i)
newRefined1T = newRefined1TP (Proxy @'(ip,op,fmt,i))
newRefined1TP :: forall m ip op fmt i proxy
. (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> RefinedT m (Refined1 ip op fmt i)
newRefined1TP = newRefined1TPImpl (return . runIdentity)
newRefined1TPIO :: forall m ip op fmt i proxy
. (Refined1C ip op fmt i
, MonadIO m
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> RefinedT m (Refined1 ip op fmt i)
newRefined1TPIO = newRefined1TPImpl liftIO
newRefined1TPImpl :: forall n m ip op fmt i proxy
. (Refined1C 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 (Refined1 ip op fmt i)
newRefined1TPImpl f _ opts i = do
(ret,mr) <- f $ eval1M opts i
let m1 = prt1Impl opts ret
tell [m1Long m1]
case mr of
Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1
Just r -> return r
newRefined1TPSkipIPImpl :: forall n m ip op fmt i proxy
. (Refined1C 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 (Refined1 ip op fmt i)
newRefined1TPSkipIPImpl f _ opts a = do
(ret,mr) <- f $ eval1MSkip opts a
let m1 = prt1Impl opts ret
tell [m1Long m1]
case mr of
Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1
Just r -> return r
convertRefined1TP :: forall m ip op fmt i ip1 op1 fmt1 i1 .
( Refined1C 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 (Refined1 ip op fmt i)
-> RefinedT m (Refined1 ip1 op1 fmt1 i1)
convertRefined1TP _ _ opts ma = do
Refined1 x <- ma
Refined1 a <- newRefined1TPSkipIPImpl (return . runIdentity) (Proxy @'(ip1, op1, fmt1, i1)) opts x
return (Refined1 a)
rapply1 :: forall m ip op fmt i .
( Refined1C ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> POpts
-> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined1 ip op fmt i)
-> RefinedT m (Refined1 ip op fmt i)
-> RefinedT m (Refined1 ip op fmt i)
rapply1 = rapply1P (Proxy @'(ip,op,fmt,i))
rapply1P :: forall m ip op fmt i proxy .
( Refined1C 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 (Refined1 ip op fmt i)
-> RefinedT m (Refined1 ip op fmt i)
-> RefinedT m (Refined1 ip op fmt i)
rapply1P p opts f ma mb = do
tell [bgColor Blue "=== a ==="]
Refined1 x <- ma
tell [bgColor Blue "=== b ==="]
Refined1 y <- mb
tell [bgColor Blue "=== a `op` b ==="]
Refined1 a <- newRefined1TPSkipIPImpl (return . runIdentity) p opts (f x y)
return (Refined1 a)
data RResults1 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
prtEval1PIO :: forall ip op fmt i proxy
. ( Refined1C ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> IO (Either String (Refined1 ip op fmt i))
prtEval1PIO _ opts i = do
x <- eval1M opts i
prt1IO opts x
prtEval1 :: forall ip op fmt i
. ( Refined1C ip op fmt i
, Show (PP ip i)
, Show i)
=> POpts
-> i
-> Either Msg1 (Refined1 ip op fmt i)
prtEval1 = prtEval1P Proxy
prtEval1P :: forall ip op fmt i proxy
. ( Refined1C ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> Either Msg1 (Refined1 ip op fmt i)
prtEval1P _ opts = prt1 opts . eval1 opts
eval1P :: forall ip op fmt i proxy . Refined1C ip op fmt i
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))
eval1P _ opts = runIdentity . eval1M opts
eval1 :: forall ip op fmt i . Refined1C ip op fmt i
=> POpts
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))
eval1 = eval1P Proxy
eval1M :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i)
=> POpts
-> i
-> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))
eval1M opts i = do
ll <- eval (Proxy @ip) opts i
case getValAndPE ll of
(Right a, t1) -> do
rr <- evalBool (Proxy @op) opts a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) opts a
pure $ case getValAndPE ss of
(Right b,t3) -> (RTTrueT a t1 t2 b t3, Just (Refined1 a))
(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)
eval1MSkip :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i)
=> POpts
-> PP ip i
-> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))
eval1MSkip opts a = do
rr <- evalBool (Proxy @op) opts a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) opts a
pure $ case getValAndPE ss of
(Right b,t3) -> (RTTrueT a mkNodeSkipP t2 b t3, Just (Refined1 a))
(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)
eval1MQuickIdentity :: forall ip op fmt i . Refined1C ip op fmt i
=> PP ip i
-> Maybe (Refined1 ip op fmt i)
eval1MQuickIdentity = runIdentity . eval1MQuick
eval1MQuick :: forall m ip op fmt i . (MonadEval m, Refined1C ip op fmt i)
=> PP ip i
-> m (Maybe (Refined1 ip op fmt i))
eval1MQuick a = do
let opts = oz
rr <- evalBool (Proxy @op) opts a
case getValLRFromTT rr of
Right True -> do
ss <- eval (Proxy @fmt) opts a
pure $ case getValLRFromTT ss of
Right _ -> Just (Refined1 a)
_ -> Nothing
_ -> pure Nothing
prt1IO :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> IO (Either String r)
prt1IO opts (ret,mr) = do
let m1 = prt1Impl opts ret
unless (hasNoTree opts) $ putStrLn $ m1Long m1
return $ maybe (Left (m1Desc m1 <> " | " <> m1Short m1)) Right mr
prt1 :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> Either Msg1 r
prt1 opts (ret,mr) = maybe (Left $ prt1Impl opts ret) Right mr
data Msg1 = Msg1 { m1Desc :: !String
, m1Short :: !String
, m1Long :: !String
} deriving Eq
instance Show Msg1 where
show (Msg1 a b c) = a <> " | " <> b <> (if null c then "" else "\n" <> c)
prt1Impl :: (Show a, Show b)
=> POpts
-> RResults1 a b
-> Msg1
prt1Impl opts v =
let outmsg msg = "\n*** " <> msg <> " ***\n\n"
msg1 a = outmsg ("Step 1. Success Initial Conversion(ip) [" ++ show a ++ "]")
mkMsg1 m n r | hasNoTree opts = Msg1 m n ""
| otherwise = Msg1 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 mkMsg1 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 mkMsg1 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 mkMsg1 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 mkMsg1 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 mkMsg1 m n r
eval1PX :: forall ip op fmt i proxy . Refined1C ip op fmt i
=> proxy '(ip,op,fmt,i)
-> POpts
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
eval1PX _ opts i = runIdentity $ do
ll <- eval (Proxy @ip) opts i
case getValAndPE ll of
(Right a,t1) -> do
rr <- evalBool (Proxy @op) opts a
case getValAndPE rr of
(Right True,t2) -> do
ss <- eval (Proxy @fmt) opts 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)
eval1X :: forall ip op fmt i . Refined1C ip op fmt i
=> POpts
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
eval1X = eval1PX (Proxy @'(ip,op,fmt,i))
type RefinedEmulate p a = Refined1 Id p Id a
type family T4_1 x where
T4_1 '(a,b,c,d) = a
type family T4_2 x where
T4_2 '(a,b,c,d) = b
type family T4_3 x where
T4_3 '(a,b,c,d) = c
type family T4_4 x where
T4_4 '(a,b,c,d) = d