{-# 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 #-}
{- |
     Refinement type allowing the external type to differ from the internal type
     see 'Refined2'
-}
module Predicate.Refined2 (

  -- ** Refined2
    Refined2(r2In,r2Out)
  , Refined2C

 -- ** display results
  , prtEval2
  , prtEval2P
  , prtEval2IO
  , prtEval2PIO
  , prt2IO
  , prt2Impl
  , Msg2 (..)
  , RResults2 (..)

  -- ** evaluation methods
  , eval2
  , eval2P
  , eval2M
  , newRefined2
  , newRefined2P

  -- ** create a wrapped Refined2 value
  , newRefined2T
  , newRefined2TP
  , newRefined2TIO
  , withRefined2T
  , withRefined2TP
  , withRefined2TIO

  -- ** proxy methods
  , MakeR2
  , mkProxy2
  , mkProxy2'

  -- ** unsafe methods for creating Refined2
  , 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.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 ((^.))
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String
import Data.Hashable (Hashable(..))
import GHC.Stack

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> :set -XOverloadedStrings
-- >>> :m + Predicate.Prelude
-- >>> :m + Data.Time

-- | Refinement type for specifying an input type that is different from the output type
--
--   * @opts@ are the display options
--   * @ip@ converts @i@ to @PP ip i@ which is the internal type in 'r2In'
--   * @op@ validates that internal type using @PP op (PP ip i) ~ Bool@
--   * @i@ is the input type which is stored in 'r2Out'
--
-- Although a common scenario is String as input, you are free to choose any input type you like
--
-- >>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 255) "00fe"
-- Right (Refined2 {r2In = 254, r2Out = "00fe"})
--
-- >>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 253) "00fe"
-- Left "Step 2. False Boolean Check(op) | FalseP"
--
-- >>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 255) "00fg"
-- Left "Step 1. Initial Conversion(ip) Failed | invalid base 16"
--
-- >>> newRefined2 @'OL @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) "198.162.3.1.5"
-- Left "Step 2. False Boolean Check(op) | {length invalid:5 == 4}"
--
-- >>> newRefined2 @'OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) "198.162.3.1.5"
-- Left "Step 2. Failed Boolean Check(op) | found length=5"
--
-- >>> newRefined2 @'OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) "198.162.3.1"
-- Right (Refined2 {r2In = [198,162,3,1], r2Out = "198.162.3.1"})
--
-- >>> :m + Data.Time.Calendar.WeekDate
-- >>> newRefined2 @'OZ @(MkDayExtra Id >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) (2019,10,13)
-- Right (Refined2 {r2In = (2019-10-13,41,7), r2Out = (2019,10,13)})
--
-- >>> newRefined2 @'OL @(MkDayExtra Id >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) (2019,10,12)
-- Left "Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7}"
--
-- >>> newRefined2 @'OZ @(MkDayExtra' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) (2019,10,12)
-- Left "Step 2. Failed Boolean Check(op) | expected a Sunday"
--
data Refined2 (opts :: OptT) ip op i = Refined2 { r2In :: !(PP ip i), r2Out :: !i }

type role Refined2 nominal nominal nominal nominal

-- | directly load values into 'Refined2'. It still checks to see that those values are valid
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

-- | directly load values into 'Refined2' without any checking
unsafeRefined2 :: forall opts ip op i . PP ip i -> i -> Refined2 opts ip op i
unsafeRefined2 = Refined2

-- | Provides the constraints on Refined2
type Refined2C opts ip op i =
       ( OptTC opts
       , P ip i
       , P op (PP ip i)
       , PP op (PP ip i) ~ Bool   -- the internal value needs to pass the predicate check
       )

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

-- read instance from -ddump-deriv
-- | 'Read' instance for 'Refined2'
--
-- >>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Between 0 255 Id) String) "Refined2 {r2In = 254, r2Out = \"fe\"}"
-- [(Refined2 {r2In = 254, r2Out = "fe"},"")]
--
-- >>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Between 0 255 Id) String) "Refined2 {r2In = 300, r2Out = \"12c\"}"
-- []
--
-- >>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Id < 0) String) "Refined2 {r2In = -1234, r2Out = \"-4d2\"}"
-- [(Refined2 {r2In = -1234, r2Out = "-4d2"},"")]
--
-- >>> reads @(Refined2 'OZ (Map (ReadP Int Id) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) String) "Refined2 {r2In = [192,168,0,1], r2Out = \"192.168.0.1\"}"
-- [(Refined2 {r2In = [192,168,0,1], r2Out = "192.168.0.1"},"")]
--
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

-- | 'ToJSON' instance for 'Refined2'
--
-- >>> import qualified Data.Aeson as A
-- >>> A.encode (unsafeRefined2 @'OZ @(ReadBase Int 16 Id) @(Between 0 255 Id) 254 "fe")
-- "\"fe\""
--
-- >>> A.encode (unsafeRefined2 @'OZ @Id @'True @Int 123 123)
-- "123"
--
instance ToJSON i => ToJSON (Refined2 opts ip op i) where
  toJSON = toJSON . r2Out


-- | 'FromJSON' instance for 'Refined2'
--
-- >>> import qualified Data.Aeson as A
-- >>> A.eitherDecode' @(Refined2 'OZ (ReadBase Int 16 Id) (Id > 10 && Id < 256) String) "\"00fe\""
-- Right (Refined2 {r2In = 254, r2Out = "00fe"})
--
-- >>> removeAnsi $ A.eitherDecode' @(Refined2 'OAN (ReadBase Int 16 Id) (Id > 10 && Id < 256) String) "\"00fe443a\""
-- Error in $: Refined2:Step 2. False Boolean Check(op) | {True && False | (16663610 < 256)}
-- <BLANKLINE>
-- *** Step 1. Success Initial Conversion(ip) [16663610] ***
-- <BLANKLINE>
-- P ReadBase(Int,16) 16663610 | "00fe443a"
-- |
-- `- P Id "00fe443a"
-- <BLANKLINE>
-- *** Step 2. False Boolean Check(op) ***
-- <BLANKLINE>
-- False True && False | (16663610 < 256)
-- |
-- +- True 16663610 > 10
-- |  |
-- |  +- P Id 16663610
-- |  |
-- |  `- P '10
-- |
-- `- False 16663610 < 256
--    |
--    +- P Id 16663610
--    |
--    `- P '256
-- <BLANKLINE>
--
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


-- | 'Binary' instance for 'Refined2'
--
-- >>> import Control.Arrow ((+++))
-- >>> import Control.Lens
-- >>> import Data.Time
-- >>> type K1 = Refined2 'OAN (ReadP Day Id) 'True String
-- >>> type K2 = Refined2 'OAN (ReadP Day Id) (Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id) String
-- >>> r = unsafeRefined2' "2019-04-23" :: K1
-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
-- Refined2 {r2In = 2019-04-23, r2Out = "2019-04-23"}
--
-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
-- Refined2:Step 2. False Boolean Check(op) | {2019-05-30 <= 2019-04-23}
-- <BLANKLINE>
-- *** Step 1. Success Initial Conversion(ip) [2019-04-23] ***
-- <BLANKLINE>
-- P ReadP Day 2019-04-23
-- |
-- `- P Id "2019-04-23"
-- <BLANKLINE>
-- *** Step 2. False Boolean Check(op) ***
-- <BLANKLINE>
-- False 2019-05-30 <= 2019-04-23
-- |
-- +- P Id 2019-04-23
-- |
-- +- P ReadP Day 2019-05-30
-- |  |
-- |  `- P '2019-05-30
-- |
-- `- P ReadP Day 2019-06-01
--    |
--    `- P '2019-06-01
-- <BLANKLINE>
--
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

-- | 'Hashable' instance for 'Refined2'
instance (Refined2C opts ip op i
        , Hashable i
        ) => Hashable (Refined2 opts ip op i) where
  hashWithSalt s (Refined2 _ b) = s + hash b

-- | same as 'withRefined2T' for IO
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

-- | create a 'Refined2' value using a continuation
--
-- This first example reads a hex string and makes sure it is between 100 and 200 and then
-- reads a binary string and adds the values together
--
-- >>> :set -XPolyKinds
-- >>> prtRefinedTIO $ withRefined2T @'OZ @(ReadBase Int 16 Id) @(Between 100 200 Id) "a3" $ \x -> withRefined2T @'OZ @(ReadBase Int 2 Id) @'True "1001110111" $ \y -> pure (r2In x + r2In y)
-- 794
--
-- this example fails as the the hex value is out of range
--
-- >>> prtRefinedTIO $ withRefined2T @'OAN @(ReadBase Int 16 Id) @(Between 100 200 Id) "a388" $ \x -> withRefined2T @'OAN @(ReadBase Int 2 Id) @'True "1001110111" $ \y -> pure (x,y)
-- <BLANKLINE>
-- *** Step 1. Success Initial Conversion(ip) [41864] ***
-- <BLANKLINE>
-- P ReadBase(Int,16) 41864 | "a388"
-- |
-- `- P Id "a388"
-- <BLANKLINE>
-- *** Step 2. False Boolean Check(op) ***
-- <BLANKLINE>
-- False 41864 <= 200
-- |
-- +- P Id 41864
-- |
-- +- P '100
-- |
-- `- P '200
-- <BLANKLINE>
-- failure msg[Step 2. False Boolean Check(op) | {41864 <= 200}]
--
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 m opts ip op i b proxy
  . ( 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

-- | pure version for extracting Refined2
--
-- >>> newRefined2 @'OU @Id @'True 22
-- Right (Refined2 {r2In = 22, r2Out = 22})
--
-- >>> newRefined2 @'OU @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust (ToDay Id))) "2020-05-04 12:13:14Z"
-- Right (Refined2 {r2In = 2020-05-04 12:13:14 UTC, r2Out = "2020-05-04 12:13:14Z"})
--
-- >>> newRefined2 @'OU @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust (ToDay Id))) "2020-05-08 12:13:14Z"
-- Left "Step 2. False Boolean Check(op) | {Just 2020-05-08 <= Just 2020-05-07}"
--
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 _ = fst . runIdentity . unRavelT . newRefined2T @_ @opts @ip @op

-- | create a wrapped 'Refined2' type
--
-- >>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Thd Id == 5) (2019,11,1)
-- Refined2 {r2In = (2019-11-01,44,5), r2Out = (2019,11,1)}
--
-- >>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Thd Id == 5) (2019,11,2)
-- failure msg[Step 2. False Boolean Check(op) | {6 == 5}]
--
-- >>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Msg "wrong day:" (Thd Id == 5)) (2019,11,2)
-- failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}]
--
newRefined2T :: forall m opts ip op i
   . ( Refined2C opts ip op i
     , Monad m
     , Show (PP ip i)
    ) => i
      -> RefinedT m (Refined2 opts ip op i)
newRefined2T = newRefined2TImpl (return . runIdentity)

-- | create a wrapped 'Refined2' type with an explicit proxy
newRefined2TP :: forall m opts ip op i proxy
   . ( 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)

-- | create a wrapped 'Refined2' type in IO
newRefined2TIO :: forall m opts ip op i
   . ( Refined2C opts ip op i
     , MonadIO m
     , Show (PP ip i)
    ) => i
      -> RefinedT m (Refined2 opts ip op i)
newRefined2TIO = newRefined2TImpl 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

-- | An ADT that summarises the results of evaluating Refined2 representing all possible states
data RResults2 a =
       RF !String !(Tree PE)        -- fails initial conversion
     | RTF !a !(Tree PE) !String !(Tree PE)    -- op fails
     | RTFalse !a !(Tree PE) !(Tree PE)        -- op false
     | RTTrue !a !(Tree PE) !(Tree PE) -- op true
     deriving Show

-- | same as 'prtEval2PIO' without a proxy for used with TypeApplications
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

-- | same as 'prtEval2P' but runs in IO
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 m opts ip op i
  . ( 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

-- | creates a 4-tuple proxy (see 'withRefined2TP' 'newRefined2TP' 'eval2P' 'prtEval2P')
--
-- use type application to set the 4-tuple or set the individual parameters directly
--
-- set the 4-tuple directly
--
-- >>> eg1 = mkProxy2 @'( 'OL, ReadP Int Id, Gt 10, String)
-- >>> newRefined2P eg1 "24"
-- Right (Refined2 {r2In = 24, r2Out = "24"})
--
-- skip the 4-tuple and set each parameter individually using type application
--
-- >>> eg2 = mkProxy2 @_ @'OL @(ReadP Int Id) @(Gt 10)
-- >>> newRefined2P eg2 "24"
-- Right (Refined2 {r2In = 24, r2Out = "24"})
--
mkProxy2 :: forall z opts ip op i
  . ( z ~ '(opts,ip,op,i)
    ) => Proxy '(opts,ip,op,i)
mkProxy2 = Proxy

-- | same as 'mkProxy2' but checks to make sure the proxy is consistent with the 'Refined2C' constraint
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 for converting from a 4-tuple '(opts,ip,op,i) to a 'Refined2' type
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