{-# 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.Refined1 (
Refined1
, unRefined1
, Refined1C
, prtEval1
, prtEval1P
, prtEval1IO
, prtEval1PIO
, prt1IO
, prt1Impl
, Msg1 (..)
, RResults1 (..)
, eval1
, eval1P
, eval1M
, newRefined1
, newRefined1P
, newRefined1T
, newRefined1TP
, newRefined1TPIO
, withRefined1T
, withRefined1TIO
, withRefined1TP
, mkProxy1
, mkProxy1'
, MakeR1
, unsafeRefined1
, unsafeRefined1'
, convertRefined1TP
, rapply1
, rapply1P
, genRefined1
, genRefined1P
, RefinedEmulate
, eval1PX
, eval1X
, type ReplaceOptT1
, type AppendOptT1
) 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 Data.Maybe (fromMaybe)
import Control.Lens ((^.))
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String
import Data.Hashable (Hashable(..))
import GHC.Stack
newtype Refined1 (opts :: OptT) ip op fmt i = Refined1 (PP ip i)
unRefined1 :: forall (opts :: OptT) ip op fmt i. Refined1 opts ip op fmt i -> PP ip i
unRefined1 (Refined1 a) = a
type role Refined1 nominal nominal nominal nominal nominal
unsafeRefined1' :: forall opts ip op fmt i
. ( HasCallStack
, Show i
, Show (PP ip i)
, Refined1C opts ip op fmt i
)
=> i
-> Refined1 opts ip op fmt i
unsafeRefined1' i =
let (ret,mr) = eval1 @opts @ip @op @fmt i
in fromMaybe (error $ show (prt1Impl (getOptT @opts) ret)) mr
unsafeRefined1 :: forall opts ip op fmt i . PP ip i -> Refined1 opts ip op fmt i
unsafeRefined1 = Refined1
type Refined1C 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 (Refined1 opts ip op fmt i)
deriving instance ( Eq i
, Eq (PP ip i)
, Eq (PP fmt (PP ip i))
) => Eq (Refined1 opts ip op fmt i)
deriving instance ( TH.Lift (PP ip i)
, TH.Lift (PP fmt (PP ip i))
) => TH.Lift (Refined1 opts ip op fmt i)
instance (Refined1C opts ip op fmt String, Show (PP ip String)) => IsString (Refined1 opts ip op fmt String) where
fromString s =
let (ret,mr) = eval1 @opts @ip @op @fmt s
in fromMaybe (error $ "Refined1(fromString):" ++ show (prt1Impl (getOptT @opts) ret)) mr
instance ( Eq i
, Show i
, Eq (PP ip i)
, Show (PP ip i)
, Refined1C opts ip op fmt i
, Read (PP ip i)
, Read (PP fmt (PP ip i))
) => Read (Refined1 opts ip op fmt i) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined1")
fld1 <- PCR.reset GR.readPrec
let (_ret,mr) = runIdentity $ eval1MSkip @opts @ip @op @fmt fld1
case mr of
Nothing -> fail ""
Just (Refined1 r1)
| r1 == fld1 -> pure (Refined1 r1)
| otherwise -> fail ""
))
readList = GR.readListDefault
readListPrec = GR.readListPrecDefault
instance ( OptTC opts
, Show (PP fmt (PP ip i))
, ToJSON (PP fmt (PP ip i))
, P fmt (PP ip i)
) => ToJSON (Refined1 opts ip op fmt i) where
toJSON (Refined1 x) =
let ss = runIdentity $ eval (Proxy @fmt) (getOptT @opts) 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 opts ip op fmt i
, FromJSON i
) => FromJSON (Refined1 opts ip op fmt i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval1 @opts @ip @op @fmt i
case mr of
Nothing -> fail $ "Refined1:" ++ show (prt1Impl (getOptT @opts) ret)
Just r -> return r
instance (Arbitrary (PP ip i)
, Refined1C opts ip op fmt i
) => Arbitrary (Refined1 opts ip op fmt i) where
arbitrary = genRefined1 arbitrary
genRefined1 ::
forall opts ip op fmt i
. Refined1C opts ip op fmt i
=> Gen (PP ip i)
-> Gen (Refined1 opts ip op fmt i)
genRefined1 = genRefined1P Proxy
genRefined1P ::
forall opts ip op fmt i
. Refined1C opts ip op fmt i
=> Proxy '(opts,ip,op,fmt,i)
-> Gen (PP ip i)
-> Gen (Refined1 opts ip op fmt i)
genRefined1P _ 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 ("genRefined1 recursion exceeded(" ++ show (oRecursion o) ++ ")")
else f (cnt+1)
Just ppi ->
pure $ unsafeRefined1 ppi
in f 0
instance ( Show (PP fmt (PP ip i))
, Show (PP ip i)
, Refined1C opts ip op fmt i
, Binary i
) => Binary (Refined1 opts ip op fmt i) where
get = do
i <- B.get @i
let (ret,mr) = eval1 @opts @ip @op @fmt i
case mr of
Nothing -> fail $ "Refined1:" ++ show (prt1Impl (getOptT @opts) ret)
Just r -> return r
put (Refined1 x) =
let ss = runIdentity $ eval (Proxy @fmt) (getOptT @opts) 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 opts ip op fmt i
, Hashable (PP ip i)
) => Hashable (Refined1 opts ip op fmt i) where
hashWithSalt s (Refined1 a) = s + hash a
mkProxy1 ::
forall z opts ip op fmt i
. z ~ '(opts,ip,op,fmt,i)
=> Proxy '(opts,ip,op,fmt,i)
mkProxy1 = Proxy
mkProxy1' :: forall z opts ip op fmt i
. ( z ~ '(opts,ip,op,fmt,i)
, Refined1C opts ip op fmt i
) => Proxy '(opts,ip,op,fmt,i)
mkProxy1' = Proxy
type family MakeR1 p where
MakeR1 '(opts,ip,op,fmt,i) = Refined1 opts ip op fmt i
withRefined1TIO :: forall opts ip op fmt i m b
. ( MonadIO m
, Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> i
-> (Refined1 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1TIO = (>>=) . newRefined1TPIO (Proxy @'(opts,ip,op,fmt,i))
withRefined1T :: forall opts ip op fmt i m b
. ( Monad m
, Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> i
-> (Refined1 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1T = (>>=) . newRefined1TP (Proxy @'(opts,ip,op,fmt,i))
withRefined1TP :: forall opts ip op fmt i b proxy m
. ( Monad m
, Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (Refined1 opts ip op fmt i -> RefinedT m b)
-> RefinedT m b
withRefined1TP p = (>>=) . newRefined1TP p
newRefined1 :: forall opts ip op fmt i
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> i
-> Either String (Refined1 opts ip op fmt i)
newRefined1 = newRefined1P Proxy
newRefined1P :: forall opts ip op fmt i proxy
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> Either String (Refined1 opts ip op fmt i)
newRefined1P _ x =
let (lr,xs) = runIdentity $ unRavelT $ newRefined1T @opts @ip @op @fmt x
in left (\e -> e ++ (if all null xs then "" else "\n" ++ unlines xs)) lr
newRefined1T :: forall opts ip op fmt i m
. ( Refined1C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i
)
=> i
-> RefinedT m (Refined1 opts ip op fmt i)
newRefined1T = newRefined1TP (Proxy @'(opts,ip,op,fmt,i))
newRefined1TP :: forall opts ip op fmt i proxy m
. ( Refined1C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i
)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> RefinedT m (Refined1 opts ip op fmt i)
newRefined1TP = newRefined1TPImpl (return . runIdentity)
newRefined1TPIO :: forall opts ip op fmt i proxy m
. ( Refined1C opts ip op fmt i
, MonadIO m
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> RefinedT m (Refined1 opts ip op fmt i)
newRefined1TPIO = newRefined1TPImpl liftIO
newRefined1TPImpl :: forall n m opts ip op fmt i proxy
. ( Refined1C 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 (Refined1 opts ip op fmt i)
newRefined1TPImpl f _ i = do
(ret,mr) <- f $ eval1M i
let m1 = prt1Impl (getOptT @opts) ret
tell [m1Long m1]
case mr of
Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1
Just r -> return r
newRefined1TPSkipIPImpl :: forall n m opts ip op fmt i proxy
. ( Refined1C 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 (Refined1 opts ip op fmt i)
newRefined1TPSkipIPImpl f _ a = do
(ret,mr) <- f $ eval1MSkip a
let m1 = prt1Impl (getOptT @opts) ret
tell [m1Long m1]
case mr of
Nothing -> throwError $ m1Desc m1 <> " | " <> m1Short m1
Just r -> return r
convertRefined1TP :: forall opts ip op fmt i ip1 op1 fmt1 i1 m .
( Refined1C 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 (Refined1 opts ip op fmt i)
-> RefinedT m (Refined1 opts ip1 op1 fmt1 i1)
convertRefined1TP _ _ ma = do
Refined1 x <- ma
Refined1 a <- newRefined1TPSkipIPImpl (return . runIdentity) (Proxy @'(opts, ip1, op1, fmt1, i1)) x
return (Refined1 a)
rapply1 :: forall opts ip op fmt i m .
( Refined1C opts ip op fmt i
, Monad m
, Show (PP ip i)
, Show i)
=> (PP ip i -> PP ip i -> PP ip i)
-> RefinedT m (Refined1 opts ip op fmt i)
-> RefinedT m (Refined1 opts ip op fmt i)
-> RefinedT m (Refined1 opts ip op fmt i)
rapply1 = rapply1P (Proxy @'(opts,ip,op,fmt,i))
rapply1P :: forall opts ip op fmt i proxy m .
( Refined1C 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 (Refined1 opts ip op fmt i)
-> RefinedT m (Refined1 opts ip op fmt i)
-> RefinedT m (Refined1 opts ip op fmt i)
rapply1P p f ma mb = do
let opts = getOptT @opts
tell [setOtherEffects opts "=== a ==="]
Refined1 x <- ma
tell [setOtherEffects opts "=== b ==="]
Refined1 y <- mb
tell [setOtherEffects opts "=== a `op` b ==="]
newRefined1TPSkipIPImpl (return . runIdentity) p (f x y)
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
prtEval1IO :: forall opts ip op fmt i
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> i
-> IO (Either String (Refined1 opts ip op fmt i))
prtEval1IO = prtEval1PIO Proxy
prtEval1PIO :: forall opts ip op fmt i proxy
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> IO (Either String (Refined1 opts ip op fmt i))
prtEval1PIO _ i = do
x <- eval1M i
prt1IO @opts x
prtEval1 :: forall opts ip op fmt i
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> i
-> Either Msg1 (Refined1 opts ip op fmt i)
prtEval1 = prtEval1P Proxy
prtEval1P :: forall opts ip op fmt i proxy
. ( Refined1C opts ip op fmt i
, Show (PP ip i)
, Show i)
=> proxy '(opts,ip,op,fmt,i)
-> i
-> Either Msg1 (Refined1 opts ip op fmt i)
prtEval1P _ i =
let (ret,mr) = eval1 i
in maybe (Left $ prt1Impl (getOptT @opts) ret) Right mr
eval1P :: forall opts ip op fmt i proxy . Refined1C opts ip op fmt i
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
eval1P _ = runIdentity . eval1M
eval1 :: forall opts ip op fmt i . Refined1C opts ip op fmt i
=> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
eval1 = eval1P Proxy
eval1M :: forall opts ip op fmt i m . (MonadEval m, Refined1C opts ip op fmt i)
=> i
-> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
eval1M 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 (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 opts ip op fmt i m . (MonadEval m, Refined1C opts ip op fmt i)
=> PP ip i
-> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
eval1MSkip 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 (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)
prt1IO :: forall opts a b r . (OptTC opts, Show a, Show b) => (RResults1 a b, Maybe r) -> IO (Either String r)
prt1IO (ret,mr) = do
let o = getOptT @opts
let m1 = prt1Impl o ret
unless (hasNoTree o) $ putStrLn $ m1Long m1
return $ maybe (Left (m1Desc m1 <> " | " <> m1Short m1)) 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 :: forall a b . (Show a, Show b)
=> POpts
-> RResults1 a b
-> Msg1
prt1Impl opts v =
let outmsg msg = "\n*** " <> formatOMsg opts " " <> 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 = 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 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 opts ip op fmt i proxy . Refined1C opts ip op fmt i
=> proxy '(opts,ip,op,fmt,i)
-> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
eval1PX _ 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)
eval1X :: forall opts ip op fmt i . Refined1C opts ip op fmt i
=> i
-> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
eval1X = eval1PX (Proxy @'(opts,ip,op,fmt,i))
type RefinedEmulate (opts :: OptT) p a = Refined1 opts Id p Id a
type family ReplaceOptT1 (o :: OptT) t where
ReplaceOptT1 o (Refined1 _ ip op fmt i) = Refined1 o ip op fmt i
type family AppendOptT1 (o :: OptT) t where
AppendOptT1 o (Refined1 o' ip op fmt i) = Refined1 (o' ':# o) ip op fmt i