{-# 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 #-}
module Predicate.Refined2 (
Refined2(r2In,r2Out)
, Refined2C
, prtEval2
, prtEval2P
, prtEval2PIO
, prt2IO
, prt2
, prt2Impl
, Msg2 (..)
, RResults2 (..)
, eval2
, eval2P
, newRefined2T
, newRefined2TP
, newRefined2TIO
, withRefined2T
, withRefined2TP
, withRefined2TIO
, MakeR2
, mkProxy2
, mkProxy2'
, unsafeRefined2
, unsafeRefined2'
, T3_1
, T3_2
, T3_3
) 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 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.Semigroup ((<>))
import Data.String
import Data.Hashable (Hashable(..))
data Refined2 ip op i = Refined2 { r2In :: PP ip i, r2Out :: i }
type role Refined2 nominal nominal nominal
unsafeRefined2' :: forall ip op i
. (Show (PP ip i), Refined2C ip op i)
=> POpts
-> i
-> Refined2 ip op i
unsafeRefined2' opts i =
let (ret,mr) = eval2 @ip @op opts i
in fromMaybe (error $ show (prt2Impl opts ret)) mr
unsafeRefined2 :: forall ip op i . PP ip i -> i -> Refined2 ip op i
unsafeRefined2 = Refined2
type Refined2C ip op i =
( P ip i
, P op (PP ip i)
, PP op (PP ip i) ~ Bool
)
deriving instance (Show i, Show (PP ip i)) => Show (Refined2 ip op i)
deriving instance (Eq i, Eq (PP ip i)) => Eq (Refined2 ip op i)
deriving instance (TH.Lift (PP ip i), TH.Lift i) => TH.Lift (Refined2 ip op i)
instance (Refined2C ip op String, Show (PP ip String)) => IsString (Refined2 ip op String) where
fromString s =
let (ret,mr) = eval2 @ip @op o2 s
in fromMaybe (error $ "Refined2(fromString):" ++ show (prt2Impl o2 ret)) mr
instance ( Eq i
, Show i
, Show (PP ip i)
, Refined2C ip op i
, Read (PP ip i)
, Read i
) => Read (Refined2 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) oz 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 ip op i) where
toJSON = toJSON . r2Out
instance (Show i
, Show (PP ip i)
, Refined2C ip op i
, FromJSON i
) => FromJSON (Refined2 ip op i) where
parseJSON z = do
i <- parseJSON @i z
let (ret,mr) = eval2 @ip @op o2 i
case mr of
Nothing -> fail $ "Refined2:" ++ show (prt2Impl o2 ret)
Just r -> return r
instance ( Show i
, Show (PP ip i)
, Refined2C ip op i
, Binary i
) => Binary (Refined2 ip op i) where
get = do
i <- B.get @i
let (ret,mr) = eval2 @ip @op o2 i
case mr of
Nothing -> fail $ "Refined2:" ++ show (prt2Impl o2 ret)
Just r -> return r
put (Refined2 _ r) = B.put @i r
instance (Refined2C ip op i
, Hashable i
) => Hashable (Refined2 ip op i) where
hashWithSalt s (Refined2 _ b) = s + hash b
withRefined2TIO :: forall ip op i m b
. (MonadIO m, Refined2C ip op i, Show (PP ip i))
=> POpts
-> i
-> (Refined2 ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2TIO opts = (>>=) . newRefined2TIO @_ @ip @op @i opts
withRefined2T :: forall ip op i m b
. (Monad m, Refined2C ip op i, Show (PP ip i))
=> POpts
-> i
-> (Refined2 ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2T opts = (>>=) . newRefined2TP (Proxy @'(ip,op,i)) opts
withRefined2TP :: forall m ip op i b proxy
. (Monad m, Refined2C ip op i, Show (PP ip i))
=> proxy '(ip,op,i)
-> POpts
-> i
-> (Refined2 ip op i -> RefinedT m b)
-> RefinedT m b
withRefined2TP p opts = (>>=) . newRefined2TP p opts
newRefined2T :: forall m ip op i
. (Refined2C ip op i
, Monad m
, Show (PP ip i)
) => POpts
-> i
-> RefinedT m (Refined2 ip op i)
newRefined2T = newRefined2TImpl (return . runIdentity)
newRefined2TP :: forall m ip op i proxy
. (Refined2C ip op i
, Monad m
, Show (PP ip i)
) => proxy '(ip,op,i)
-> POpts
-> i
-> RefinedT m (Refined2 ip op i)
newRefined2TP _ = newRefined2TImpl (return . runIdentity)
newRefined2TIO :: forall m ip op i
. (Refined2C ip op i
, MonadIO m
, Show (PP ip i)
) => POpts
-> i
-> RefinedT m (Refined2 ip op i)
newRefined2TIO = newRefined2TImpl liftIO
newRefined2TImpl :: forall n m ip op i
. (Refined2C ip op i
, Monad m
, MonadEval n
, Show (PP ip i)
) => (forall x . n x -> RefinedT m x)
-> POpts
-> i
-> RefinedT m (Refined2 ip op i)
newRefined2TImpl f opts i = do
(ret,mr) <- f $ eval2M opts i
let m2 = prt2Impl 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
prtEval2PIO :: forall ip op i proxy
. ( Refined2C ip op i
, Show (PP ip i)
) => proxy '(ip,op,i)
-> POpts
-> i
-> IO (Either String (Refined2 ip op i))
prtEval2PIO _ opts i = do
x <- eval2M opts i
prt2IO opts x
prtEval2 :: forall ip op i
. ( Refined2C ip op i
, Show (PP ip i)
) => POpts
-> i
-> Either Msg2 (Refined2 ip op i)
prtEval2 opts = prt2 opts . eval2 opts
prtEval2P :: forall ip op i
. ( Refined2C ip op i
, Show (PP ip i)
) => Proxy '(ip,op,i)
-> POpts
-> i
-> Either Msg2 (Refined2 ip op i)
prtEval2P _ opts = prt2 opts . eval2 opts
eval2P :: forall ip op i . Refined2C ip op i
=> Proxy '(ip,op,i)
-> POpts
-> i
-> (RResults2 (PP ip i), Maybe (Refined2 ip op i))
eval2P _ opts = runIdentity . eval2M opts
eval2 :: forall ip op i . Refined2C ip op i
=> POpts
-> i
-> (RResults2 (PP ip i), Maybe (Refined2 ip op i))
eval2 opts = runIdentity . eval2M opts
eval2M :: forall m ip op i . (MonadEval m, Refined2C ip op i)
=> POpts
-> i
-> m (RResults2 (PP ip i), Maybe (Refined2 ip op i))
eval2M opts i = do
ll <- eval (Proxy @ip) opts i
case getValAndPE ll of
(Right a, t1) -> do
rr <- evalBool (Proxy @op) opts 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 :: Show a => POpts -> (RResults2 a, Maybe r) -> IO (Either String r)
prt2IO opts (ret,mr) = do
let m2 = prt2Impl opts ret
unless (hasNoTree opts) $ putStrLn $ m2Long m2
return $ maybe (Left (m2Desc m2 <> " | " <> m2Short m2)) Right mr
prt2 :: Show a => POpts -> (RResults2 a, Maybe r) -> Either Msg2 r
prt2 opts (ret,mr) = maybe (Left $ prt2Impl opts ret) 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 :: Show a
=> POpts
-> RResults2 a
-> Msg2
prt2Impl opts v =
let outmsg msg = "\n*** " <> 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 = 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 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 ip op i . z ~ '(ip,op,i) => Proxy '(ip,op,i)
mkProxy2 = Proxy
mkProxy2' :: forall z ip op i . (z ~ '(ip,op,i), Refined2C ip op i) => Proxy '(ip,op,i)
mkProxy2' = Proxy
type family MakeR2 p where
MakeR2 '(ip,op,i) = Refined2 ip op i
type family T3_1 x where
T3_1 '(a,b,c) = a
type family T3_2 x where
T3_2 '(a,b,c) = b
type family T3_3 x where
T3_3 '(a,b,c) = c