{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
module Predicate.Refined (
Refined
, unRefined
, RefinedC
, RefinedT(..)
, prtRefinedIO
, prtRefinedTIO
, newRefined
, newRefinedM
, withRefinedT
, withRefinedTIO
, newRefinedT
, newRefinedTIO
, genRefined
, convertRefinedT
, unRavelT
, rapply
, rapply0
, rapplyLift
, unsafeRefined
, unsafeRefined'
, type ReplaceOptT
, type AppendOptT
) where
import Predicate.Core
import Predicate.Util
import Control.Lens
import Data.Functor.Identity (Identity(..))
import Data.Proxy
import Control.Monad.Except
import Control.Monad.Writer (WriterT(..), runWriterT, MonadWriter, tell)
import Control.Monad.Cont
import Data.Aeson (ToJSON(..), FromJSON(..))
import GHC.Generics (Generic)
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.String
import Data.Hashable (Hashable(..))
import GHC.Stack
import Data.Maybe (fromMaybe)
newtype Refined (opts :: OptT) p a = Refined a deriving (Show, Eq, Generic, TH.Lift)
unRefined :: forall k (opts :: OptT) (p :: k) a. Refined opts p a -> a
unRefined (Refined a) = a
type role Refined nominal nominal nominal
instance RefinedC opts p String => IsString (Refined opts p String) where
fromString s =
let (w,mr) = runIdentity $ newRefinedM @opts @p s
in fromMaybe (error $ "Refined(fromString):" ++ errorDisplay (getOptT @opts) w) mr
errorDisplay :: POpts -> (String,(String,String)) -> String
errorDisplay o (bp,(top,e)) =
bp
++ (if null top then "" else " " ++ top)
++ (if null e || hasNoTree o then "" else "\n" ++ e)
instance (RefinedC opts p a, Read a) => Read (Refined opts p a) where
readPrec
= GR.parens
(PCR.prec
11
(do GR.expectP (RL.Ident "Refined")
fld0 <- PCR.reset GR.readPrec
case newRefined @opts @p fld0 of
Left _e -> fail ""
Right _r -> pure (Refined fld0)
))
readList = GR.readListDefault
readListPrec = GR.readListPrecDefault
type RefinedC opts p a = (OptTC opts, PP p a ~ Bool, P p a)
instance ToJSON a => ToJSON (Refined opts p a) where
toJSON = toJSON . unRefined
instance (RefinedC opts p a, FromJSON a) => FromJSON (Refined opts p a) where
parseJSON z = do
a <- parseJSON z
let (w,mr) = runIdentity $ newRefinedM @opts @p a
case mr of
Nothing -> fail $ "Refined(FromJSON:parseJSON):" ++ errorDisplay (getOptT @opts) w
Just r -> return r
instance (RefinedC opts p a, Binary a) => Binary (Refined opts p a) where
get = do
fld0 <- B.get @a
let (w,mr) = runIdentity $ newRefinedM @opts @p fld0
case mr of
Nothing -> fail $ "Refined(Binary:get):" ++ errorDisplay (getOptT @opts) w
Just r -> return r
put (Refined r) = B.put @a r
instance ( RefinedC opts p a
, Hashable a
) => Hashable (Refined opts p a) where
hashWithSalt s (Refined a) = s + hash a
instance ( Arbitrary a
, RefinedC opts p a
, Show a
) => Arbitrary (Refined opts p a) where
arbitrary = genRefined arbitrary
genRefined :: forall opts p a .
RefinedC opts p a
=> Gen a
-> Gen (Refined opts p a)
genRefined g =
let o = getOptT @opts
f !cnt = do
ma <- suchThatMaybe g (\a -> getValLRFromTT (runIdentity (eval @_ (Proxy @p) o a)) == Right True)
case ma of
Nothing ->
if cnt >= oRecursion o
then error $ setOtherEffects o ("genRefined recursion exceeded(" ++ show (oRecursion o) ++ ")")
else f (cnt+1)
Just a -> pure $ unsafeRefined a
in f 0
rapply :: forall m opts p a . (RefinedC opts p a, Monad m)
=> (a -> a -> a)
-> RefinedT m (Refined opts p a)
-> RefinedT m (Refined opts p a)
-> RefinedT m (Refined opts p a)
rapply f ma mb = do
let opts = getOptT @opts
tell [setOtherEffects opts "=== a ==="]
Refined x <- ma
tell [setOtherEffects opts "=== b ==="]
Refined y <- mb
tell [setOtherEffects opts "=== a `op` b ==="]
newRefinedT @m @opts @p (f x y)
rapply0 :: forall opts p a m . (RefinedC opts p a, Monad m)
=> (a -> a -> a)
-> a
-> a
-> RefinedT m (Refined opts p a)
rapply0 f a b = rapply f (newRefinedT a) (newRefinedT b)
rapplyLift :: forall m opts p a . (RefinedC opts p a, Monad m)
=> (a -> a -> a)
-> Refined opts p a
-> Refined opts p a
-> RefinedT m (Refined opts p a)
rapplyLift f (Refined a) (Refined b) = newRefinedT (f a b)
convertRefinedT :: forall m opts p a p1 a1
. ( RefinedC opts p1 a1
, Monad m)
=> (a -> a1)
-> RefinedT m (Refined opts p a)
-> RefinedT m (Refined opts p1 a1)
convertRefinedT f ma = do
Refined a <- ma
newRefinedT @m @opts @p1 (f a)
withRefinedT :: forall opts p m a b
. ( Monad m
, RefinedC opts p a
)
=> a
-> (Refined opts p a -> RefinedT m b)
-> RefinedT m b
withRefinedT a k = newRefinedT @m @opts @p a >>= k
withRefinedTIO :: forall opts p m a b
. ( MonadIO m
, RefinedC opts p a
)
=> a
-> (Refined opts p a -> RefinedT m b)
-> RefinedT m b
withRefinedTIO a k = newRefinedTIO @opts @p a >>= k
prtRefinedIO :: forall opts p a
. RefinedC opts p a
=> a
-> IO (Either (BoolT Bool) (Refined opts p a))
prtRefinedIO a = do
let o = getOptT @opts
tt <- evalBool (Proxy @p) o a
let r = _tBool tt
case oDebug o of
DZero -> pure ()
DLite -> putStrLn $ colorBoolT o r <> " " <> topMessage tt
_ -> putStrLn $ prtTree o tt
pure $ case getValueLR o "" tt [] of
Right True -> Right (Refined a)
_ -> Left r
newRefined :: forall opts p a
. RefinedC opts p a
=> a
-> Either String (Refined opts p a)
newRefined a =
let ((bp,(top,e)),mr) = runIdentity $ newRefinedM @opts @p a
in case mr of
Nothing -> case oDebug (getOptT @opts) of
DZero -> Left bp
DLite -> Left (bp <> (if null top then "" else " " <> top))
_ -> Left e
Just r -> Right r
newRefinedM :: forall opts p a m
. ( MonadEval m
, RefinedC opts p a
)
=> a
-> m ((String, (String, String)), Maybe (Refined opts p a))
newRefinedM a = do
let o = getOptT @opts
pp <- evalBool (Proxy @p) o a
let r = colorBoolT' o (_tBool pp)
s = prtTree o pp
pure $ ((r,(topMessage pp, s)),) $ case getValueLR o "" pp [] of
Right True -> Just (Refined a)
_ -> Nothing
newRefinedTImpl :: forall opts p a n m
. ( RefinedC opts p a
, Monad m
, MonadEval n
)
=> (forall x . n x -> RefinedT m x)
-> a
-> RefinedT m (Refined opts p a)
newRefinedTImpl f a = do
let o = getOptT @opts
tt <- f $ evalBool (Proxy @p) o a
let msg = prtTree o tt
tell [msg]
case getValueLR o "" tt [] of
Right True -> return (Refined a)
_ -> throwError $ colorBoolT' o (_tBool tt)
newRefinedT :: forall m opts p a
. ( RefinedC opts p a
, Monad m)
=> a
-> RefinedT m (Refined opts p a)
newRefinedT = newRefinedTImpl (return . runIdentity)
newRefinedTIO :: forall opts p a m
. ( RefinedC opts p a
, MonadIO m)
=> a
-> RefinedT m (Refined opts p a)
newRefinedTIO = newRefinedTImpl liftIO
newtype RefinedT m a = RefinedT { unRefinedT :: ExceptT String (WriterT [String] m) a }
deriving (Functor, Applicative, Monad, MonadCont, MonadWriter [String], Show, MonadIO)
instance MonadTrans RefinedT where
lift ma = RefinedT $ ExceptT $ WriterT $ do
a <- ma
return (Right a, [])
instance Monad m => MonadError String (RefinedT m) where
throwError e = RefinedT $ ExceptT $ WriterT $ return (Left e,[])
catchError (RefinedT (ExceptT (WriterT ma))) ema =
RefinedT $ ExceptT $ WriterT $ do
(lr,ss) <- ma
case lr of
Left e -> unRavelT (tell ss >> ema e)
Right _ -> ma
unRavelT :: RefinedT m a -> m (Either String a, [String])
unRavelT = runWriterT . runExceptT . unRefinedT
prtRefinedTImpl :: forall n m a . (MonadIO n, Show a) => (forall x . m x -> n x) -> RefinedT m a -> n ()
prtRefinedTImpl f rt = do
(lr,ws) <- f $ unRavelT rt
liftIO $ do
forM_ (zip [1::Int ..] ws) $ \(_,y) -> unless (null y) $ putStrLn y
case lr of
Left e -> putStrLn $ "failure msg[" <> e <> "]"
Right a -> print a
prtRefinedTIO :: (MonadIO m, Show a) => RefinedT m a -> m ()
prtRefinedTIO = prtRefinedTImpl id
unsafeRefined :: forall opts p a . a -> Refined opts p a
unsafeRefined = Refined
unsafeRefined' :: forall opts p a
. ( RefinedC opts p a
, HasCallStack
) => a -> Refined opts p a
unsafeRefined' a =
let o = getOptT @opts
tt = runIdentity $ evalBool (Proxy @p) o a
in case getValueLR o "" tt [] of
Right True -> Refined a
_ -> let s = prtTree o tt
bp = colorBoolT' o (view tBool tt)
in case oDebug o of
DZero -> error bp
DLite -> error $ bp ++ "\n" ++ s
_ -> error $ bp ++ "\n" ++ s
type family ReplaceOptT (o :: OptT) t where
ReplaceOptT o (Refined _ p a) = Refined o p a
type family AppendOptT (o :: OptT) t where
AppendOptT o (Refined o' p a) = Refined (o' ':# o) p a