{-# 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.Refined2 (
Refined2(r2In,r2Out)
, Refined2C
, prtEval2
, prtEval2P
, prtEval2IO
, prtEval2PIO
, prt2IO
, prt2Impl
, Msg2 (..)
, RResults2 (..)
, eval2
, eval2P
, eval2M
, newRefined2
, newRefined2P
, newRefined2T
, newRefined2TP
, newRefined2TIO
, withRefined2T
, withRefined2TP
, withRefined2TIO
, MakeR2
, mkProxy2
, mkProxy2'
, genRefined2
, genRefined2P
, unsafeRefined2
, unsafeRefined2'
, type ReplaceOptT2
, type AppendOptT2
) 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 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, isJust)
import Control.Lens
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String
import Data.Hashable (Hashable(..))
import GHC.Stack
import Test.QuickCheck
data Refined2 (opts :: OptT) ip op i = Refined2 { r2In :: !(PP ip i), r2Out :: !i }
type role Refined2 nominal nominal nominal nominal
unsafeRefined2' :: forall opts ip op i
. ( Show (PP ip i)
, Refined2C opts ip op i
, HasCallStack
)
=> i
-> Refined2 opts ip op i
unsafeRefined2' i =
let (ret,mr) = eval2 @opts @ip @op i
in fromMaybe (error $ show (prt2Impl (getOptT @opts) ret)) mr
unsafeRefined2 :: forall opts ip op i
. PP ip i
-> i
-> Refined2 opts ip op i
unsafeRefined2 = Refined2
type Refined2C opts ip op i =
( OptTC opts
, P ip i
, P op (PP ip i)
, PP op (PP ip i) ~ Bool
)
deriving instance (Show i, Show (PP ip i)) => Show (Refined2 opts ip op i)
deriving instance (Eq i, Eq (PP ip i)) => Eq (Refined2 opts ip op i)
deriving instance (TH.Lift (PP ip i), TH.Lift i) => TH.Lift (Refined2 opts ip op i)
instance ( s ~ String
, Refined2C opts ip op s
, Show (PP ip s)
) => IsString (Refined2 opts ip op s) where
fromString s =
let (ret,mr) = eval2 @opts @ip @op s
in fromMaybe (error $ "Refined2(fromString):" ++ show (prt2Impl (getOptT @opts) ret)) mr
instance ( Eq i
, Show i
, Show (PP ip i)
, Refined2C opts ip op i
, Read (PP ip i)
, Read i
) => Read (Refined2 opts ip op i) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined2")
GR.expectP (RL.Punc "{")
fld1 <- readField
"r2In" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc ",")
fld2 <- readField
"r2Out" (PCR.reset GR.readPrec)
GR.expectP (RL.Punc "}")
let lr = getValLRFromTT $ runIdentity $ evalBool (Proxy @op) (getOptT @opts) fld1
case lr of
Left {} -> fail ""
Right True -> pure (Refined2 fld1 fld2)
Right False -> fail ""
))
readList = GR.readListDefault
readListPrec = GR.readListPrecDefault
instance ToJSON i => ToJSON (Refined2 opts ip op i) where
toJSON = toJSON . r2Out
instance ( Show i
, Show (PP ip i)
, Refined2C opts ip op i
, FromJSON i
) => FromJSON (Refined2 opts ip op i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval2 @opts @ip @op i
case mr of
Nothing -> fail $ "Refined2:" ++ show (prt2Impl (getOptT @opts) ret)
Just r -> return r
instance ( Arbitrary i
, Refined2C opts ip op i
, Show (PP ip i)
) => Arbitrary (Refined2 opts ip op i) where
arbitrary = genRefined2 arbitrary
genRefined2 ::
forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
)
=> Gen i
-> Gen (Refined2 opts ip op i)
genRefined2 = genRefined2P Proxy
genRefined2P ::
forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
)
=> Proxy '(opts,ip,op,i)
-> Gen i
-> Gen (Refined2 opts ip op i)
genRefined2P _ g =
let o = getOptT @opts
f !cnt = do
mi <- suchThatMaybe g (isJust . snd . eval2 @opts @ip @op)
case mi of
Nothing ->
if cnt >= oRecursion o
then error $ setOtherEffects o ("genRefined2P recursion exceeded(" ++ show (oRecursion o) ++ ")")
else f (cnt+1)
Just i -> do
let lr = newRefined2 @opts @ip @op i
case lr of
Left e -> error $ "conversion failed: programming error failed!! " ++ e
Right r -> pure r
in f 0
instance ( Show i
, Show (PP ip i)
, Refined2C opts ip op i
, Binary i
) => Binary (Refined2 opts ip op i) where
get = do
i <- B.get @i
let (ret,mr) = eval2 @opts @ip @op i
case mr of
Nothing -> fail $ "Refined2:" ++ show (prt2Impl (getOptT @opts) ret)
Just r -> return r
put (Refined2 _ r) = B.put @i r
instance (Refined2C opts ip op i
, Hashable i
) => Hashable (Refined2 opts ip op i) where
hashWithSalt s (Refined2 _ b) = s + hash b
withRefined2TIO :: forall opts ip op i m b
. ( MonadIO m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> (Refined2 opts ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2TIO = (>>=) . newRefined2TIO @opts @ip @op @i
withRefined2T :: forall opts ip op i m b
. ( Monad m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> (Refined2 opts ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2T = (>>=) . newRefined2TP (Proxy @'(opts,ip,op,i))
withRefined2TP :: forall opts ip op i b proxy m
. ( Monad m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> proxy '(opts,ip,op,i)
-> i
-> (Refined2 opts ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2TP p = (>>=) . newRefined2TP p
newRefined2 :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => i
-> Either String (Refined2 opts ip op i)
newRefined2 = newRefined2P Proxy
newRefined2P :: forall opts ip op i proxy
. ( Refined2C opts ip op i
, Show (PP ip i)
) => proxy '(opts,ip,op,i)
-> i
-> Either String (Refined2 opts ip op i)
newRefined2P _ x =
let (lr,xs) = runIdentity $ unRavelT $ newRefined2T @opts @ip @op x
in left (\e -> e ++ (if all null xs then "" else "\n" ++ unlines xs)) lr
newRefined2T :: forall opts ip op i m
. ( Refined2C opts ip op i
, Monad m
, Show (PP ip i)
) => i
-> RefinedT m (Refined2 opts ip op i)
newRefined2T = newRefined2TImpl (return . runIdentity)
newRefined2TP :: forall opts ip op i proxy m
. ( Refined2C opts ip op i
, Monad m
, Show (PP ip i)
) => proxy '(opts,ip,op,i)
-> i
-> RefinedT m (Refined2 opts ip op i)
newRefined2TP _ = newRefined2TImpl (return . runIdentity)
newRefined2TIO :: forall opts ip op i m
. ( Refined2C opts ip op i
, MonadIO m
, Show (PP ip i)
) => i
-> RefinedT m (Refined2 opts ip op i)
newRefined2TIO = newRefined2TImpl @IO @m liftIO
newRefined2TImpl :: forall n m opts ip op i
. ( Refined2C opts ip op i
, Monad m
, MonadEval n
, Show (PP ip i)
) => (forall x . n x -> RefinedT m x)
-> i
-> RefinedT m (Refined2 opts ip op i)
newRefined2TImpl f i = do
(ret,mr) <- f $ eval2M i
let m2 = prt2Impl (getOptT @opts) ret
tell [m2Long m2]
case mr of
Nothing -> throwError $ m2Desc m2 <> " | " <> m2Short m2
Just r -> return r
data RResults2 a =
RF !String !(Tree PE)
| RTF !a !(Tree PE) !String !(Tree PE)
| RTFalse !a !(Tree PE) !(Tree PE)
| RTTrue !a !(Tree PE) !(Tree PE)
deriving Show
prtEval2IO :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => i
-> IO (Either String (Refined2 opts ip op i))
prtEval2IO = prtEval2PIO Proxy
prtEval2PIO :: forall opts ip op i proxy
. ( Refined2C opts ip op i
, Show (PP ip i)
) => proxy '(opts,ip,op,i)
-> i
-> IO (Either String (Refined2 opts ip op i))
prtEval2PIO _ i = do
x <- eval2M @opts @ip @op i
prt2IO @opts x
prtEval2 :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => i
-> Either Msg2 (Refined2 opts ip op i)
prtEval2 = prtEval2P Proxy
prtEval2P :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => Proxy '(opts,ip,op,i)
-> i
-> Either Msg2 (Refined2 opts ip op i)
prtEval2P _ i =
let (ret,mr) = eval2 i
in maybe (Left $ prt2Impl (getOptT @opts) ret) Right mr
eval2P :: forall opts ip op i
. ( Refined2C opts ip op i
)
=> Proxy '(opts,ip,op,i)
-> i
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2P _ = runIdentity . eval2M
eval2 :: forall opts ip op i
. ( Refined2C opts ip op i
)
=> i
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2 = runIdentity . eval2M
eval2M :: forall opts ip op i m
. ( MonadEval m
, Refined2C opts ip op i
)
=> i
-> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M 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
pure $ case getValAndPE rr of
(Right True,t2) -> (RTTrue a t1 t2, Just (Refined2 a i))
(Right False,t2) -> (RTFalse a t1 t2, Nothing)
(Left e,t2) -> (RTF a t1 e t2, Nothing)
(Left e,t1) -> pure (RF e t1, Nothing)
prt2IO :: forall opts a r . (OptTC opts, Show a) => (RResults2 a, Maybe r) -> IO (Either String r)
prt2IO (ret,mr) = do
let m2 = prt2Impl o ret
o = getOptT @opts
unless (hasNoTree o) $ putStrLn $ m2Long m2
return $ maybe (Left (m2Desc m2 <> " | " <> m2Short m2)) Right mr
data Msg2 = Msg2 { m2Desc :: !String
, m2Short :: !String
, m2Long :: !String
} deriving Eq
instance Show Msg2 where
show (Msg2 a b c) = a <> " | " <> b <> (if null c then "" else "\n" <> c)
prt2Impl :: forall a . Show a
=> POpts
-> RResults2 a
-> Msg2
prt2Impl opts v =
let outmsg msg = "\n*** " <> formatOMsg opts " " <> msg <> " ***\n\n"
msg1 a = outmsg ("Step 1. Success Initial Conversion(ip) (" ++ show a ++ ")")
mkMsg2 m n r | hasNoTree opts = Msg2 m n ""
| otherwise = Msg2 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 mkMsg2 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 mkMsg2 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 mkMsg2 m n r
RTTrue a t1 t2 ->
let (m,n) = ("Step 2. True Boolean Check(op)", "")
r = msg1 a
<> fixLite opts a t1
<> outmsg m
<> prtTreePure opts t2
in mkMsg2 m n r
mkProxy2 :: forall z opts ip op i
. ( z ~ '(opts,ip,op,i)
) => Proxy '(opts,ip,op,i)
mkProxy2 = Proxy
mkProxy2' :: forall z opts ip op i
. ( z ~ '(ip,op,i)
, Refined2C opts ip op i
) => Proxy '(opts,ip,op,i)
mkProxy2' = Proxy
type family MakeR2 p where
MakeR2 '(opts,ip,op,i) = Refined2 opts ip op i
type family ReplaceOptT2 (o :: OptT) t where
ReplaceOptT2 o (Refined2 _ ip op i) = Refined2 o ip op i
type family AppendOptT2 (o :: OptT) t where
AppendOptT2 o (Refined2 o' ip op i) = Refined2 (o' ':# o) ip op i