{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
-- | Template Haskell methods for creating Refined* refinement types

module Predicate.Util_TH (
  -- ** Refined

    refinedTH
  , refinedTHIO

  -- ** Refined2

  , refined2TH
  , refined2THIO

  -- ** Refined3

  , refined3TH
  , refined3THIO

  -- ** Refined5

  , refined5TH
  , refined5THIO

 ) where
import Predicate.Util
import Predicate.Misc
import Predicate.Core
import Predicate.Refined
import Predicate.Refined2
import Predicate.Refined3
import Predicate.Refined5

import qualified Language.Haskell.TH.Syntax as TH

-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XTemplateHaskell

-- >>> :m + Predicate


-- | creates a 'Refined.Refined' refinement type

--

-- >>> $$(refinedTH 123) :: Refined OL (Between 100 125 Id) Int

-- Refined 123

--

-- @

-- >$$(refinedTH 99) :: Refined OL (Between 100 125 Id) Int

--

-- <interactive>:8:4: error:

--     * refinedTH: predicate failed with False (100 <= 99)

--     * In the Template Haskell splice $$(refinedTH 99)

--       In the expression:

--           $$(refinedTH 99) :: Refined OL (Between 100 125 Id) Int

-- @

--

-- >>> $$(refinedTH 123) :: Refined OAN (Between 100 125 Id) Int

-- Refined 123

--

refinedTH :: forall opts p i
  . (TH.Lift i, RefinedC opts p i)
  => i
  -> TH.Q (TH.TExp (Refined opts p i))
refinedTH :: i -> Q (TExp (Refined opts p i))
refinedTH i
i =
  let msg0 :: String
msg0 = String
"refinedTH"
  in case i -> Either Msg0 (Refined opts p i)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p i
i of
       Left Msg0
m -> String -> Q (TExp (Refined opts p i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined opts p i)))
-> String -> Q (TExp (Refined opts p i))
forall a b. (a -> b) -> a -> b
$ String -> Msg0 -> String
forall (opts :: Opt). OptC opts => String -> Msg0 -> String
refinedFailMsg @opts String
msg0 Msg0
m
       Right Refined opts p i
r -> [||r||]

-- | creates a 'Refined.Refined' refinement type running in IO

refinedTHIO :: forall opts p i
  . (TH.Lift i, RefinedC opts p i)
  => i
  -> TH.Q (TH.TExp (Refined opts p i))
refinedTHIO :: i -> Q (TExp (Refined opts p i))
refinedTHIO i
i = do
  let msg0 :: String
msg0 = String
"refinedTHIO"
  Either Msg0 (Refined opts p i)
lr <- IO (Either Msg0 (Refined opts p i))
-> Q (Either Msg0 (Refined opts p i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg0 (Refined opts p i))
forall k (opts :: Opt) (p :: k) a (m :: Type -> Type).
(MonadEval m, RefinedC opts p a) =>
a -> m (Either Msg0 (Refined opts p a))
newRefined' i
i)
  case Either Msg0 (Refined opts p i)
lr of
    Left Msg0
m -> String -> Q (TExp (Refined opts p i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined opts p i)))
-> String -> Q (TExp (Refined opts p i))
forall a b. (a -> b) -> a -> b
$ String -> Msg0 -> String
forall (opts :: Opt). OptC opts => String -> Msg0 -> String
refinedFailMsg @opts String
msg0 Msg0
m
    Right Refined opts p i
r -> [||r||]

refinedFailMsg :: forall opts . OptC opts => String -> Msg0 -> String
refinedFailMsg :: String -> Msg0 -> String
refinedFailMsg String
msg Msg0
m =
  let msg1 :: String
msg1 | POpts -> Bool
hasNoTree (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Bool -> Bool -> Bool
|| String -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null (Msg0 -> String
m0Long Msg0
m) = String
""
           | Bool
otherwise = String -> String -> String
nullIf String
"\n" (Msg0 -> String
m0Long Msg0
m)
  in String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": predicate failed with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0ValBoolColor Msg0
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0Short Msg0
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg1

-- | creates a 'Refined2.Refined2' refinement type

--

-- >>> $$(refined2TH 100) :: Refined2 OAN Id (Between 100 125 Id) Int

-- Refined2 100 100

--

-- @

-- >$$(refined2TH 99) :: Refined2 OAN Id (Between 100 125 Id) Int

--

-- <interactive>:127:4: error:

--     * Step 2. False Boolean Check(op) | {100 <= 99}

-- *** Step 1. Success Initial Conversion(ip) (99) ***

-- P Id 99

-- *** Step 2. False Boolean Check(op) ***

-- Present False 100 <= 99

-- |

-- +- P Id 99

-- |

-- +- P '100

-- |

-- `- P '125

--

--     * In the Template Haskell splice $$(refined2TH 99)

--       In the expression:

--           $$(refined2TH 99) :: Refined2 OAN Id (Between 100 125 Id) Int

-- @

--

refined2TH :: forall opts ip op i
  . ( Refined2C opts ip op i
    , TH.Lift i
    , TH.Lift (PP ip i)
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined2 opts ip op i))
refined2TH :: i -> Q (TExp (Refined2 opts ip op i))
refined2TH i
i =
  case i -> Either Msg2 (Refined2 opts ip op i)
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 i
i of
    Left Msg2
e -> String -> Q (TExp (Refined2 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined2 opts ip op i)))
-> String -> Q (TExp (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
    Right Refined2 opts ip op i
r -> [||r||]

-- | creates a 'Refined2.Refined2' refinement type using IO

refined2THIO :: forall opts ip op i
  . ( TH.Lift i
    , TH.Lift (PP ip i)
    , Refined2C opts ip op i
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined2 opts ip op i))
refined2THIO :: i -> Q (TExp (Refined2 opts ip op i))
refined2THIO i
i = do
  Either Msg2 (Refined2 opts ip op i)
x <- IO (Either Msg2 (Refined2 opts ip op i))
-> Q (Either Msg2 (Refined2 opts ip op i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg2 (Refined2 opts ip op i))
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i
       (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' i
i)
  case Either Msg2 (Refined2 opts ip op i)
x of
    Left Msg2
e -> String -> Q (TExp (Refined2 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined2 opts ip op i)))
-> String -> Q (TExp (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
    Right Refined2 opts ip op i
r -> [||r||]

-- | creates a 'Refined3.Refined3' refinement type

--

-- >>> $$(refined3TH 100) :: Refined3 OAN Id (Between 100 125 Id) Id Int

-- Refined3 100 100

--

-- @

-- >$$(refined3TH 99) :: Refined3 OAN Id (Between 100 125 Id) Id Int

--

-- <interactive>:127:4: error:

--     * Step 2. False Boolean Check(op) | {100 <= 99}

-- *** Step 1. Success Initial Conversion(ip) (99) ***

-- P Id 99

-- *** Step 2. False Boolean Check(op) ***

-- Present False 100 <= 99

-- |

-- +- P Id 99

-- |

-- +- P '100

-- |

-- `- P '125

--

--     * In the Template Haskell splice $$(refined3TH 99)

--       In the expression:

--           $$(refined3TH 99) :: Refined3 OAN Id (Between 100 125 Id) Id Int

-- @

--

-- >>> $$(refined3TH @OL @(Resplit "\\." >> Map (ReadP Int Id)) @(All (0 <..> 0xff) && Len == 4) @(PrintL 4 "%03d.%03d.%03d.%03d" Id)  "200.2.3.4")

-- Refined3 [200,2,3,4] "200.002.003.004"

--

refined3TH :: forall opts ip op fmt i
  . ( Refined3C opts ip op fmt i
    , TH.Lift i
    , TH.Lift (PP ip i)
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined3 opts ip op fmt i))
refined3TH :: i -> Q (TExp (Refined3 opts ip op fmt i))
refined3TH i
i =
  case i -> Either Msg3 (Refined3 opts ip op fmt i)
forall k1 k2 k3 (opts :: Opt) (ip :: k1) (op :: k2) (fmt :: k3) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 i
i of
    Left Msg3
e -> String -> Q (TExp (Refined3 opts ip op fmt i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined3 opts ip op fmt i)))
-> String -> Q (TExp (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
    Right Refined3 opts ip op fmt i
r -> [||r||]

-- | creates a 'Refined3.Refined3' refinement type using IO

refined3THIO :: forall opts ip op fmt i
  . ( TH.Lift i
    , TH.Lift (PP ip i)
    , Refined3C opts ip op fmt i
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined3 opts ip op fmt i))
refined3THIO :: i -> Q (TExp (Refined3 opts ip op fmt i))
refined3THIO i
i = do
  Either Msg3 (Refined3 opts ip op fmt i)
x <- IO (Either Msg3 (Refined3 opts ip op fmt i))
-> Q (Either Msg3 (Refined3 opts ip op fmt i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg3 (Refined3 opts ip op fmt i))
forall k1 k2 k3 (opts :: Opt) (ip :: k1) (op :: k2) (fmt :: k3) i
       (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3' i
i)
  case Either Msg3 (Refined3 opts ip op fmt i)
x of
    Left Msg3
e -> String -> Q (TExp (Refined3 opts ip op fmt i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined3 opts ip op fmt i)))
-> String -> Q (TExp (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
    Right Refined3 opts ip op fmt i
r -> [||r||]

-- | creates a 'Refined5.Refined5' refinement type

--

-- >>> $$(refined5TH 100) :: Refined5 OAN Id (Between 100 125 Id) Int

-- Refined5 100

--

-- @

-- >$$(refined5TH 99) :: Refined5 OAN Id (Between 100 125 Id) Int

--

-- <interactive>:127:4: error:

--     * Step 2. False Boolean Check(op) | {100 <= 99}

-- *** Step 1. Success Initial Conversion(ip) (99) ***

-- P Id 99

-- *** Step 2. False Boolean Check(op) ***

-- Present False 100 <= 99

-- |

-- +- P Id 99

-- |

-- +- P '100

-- |

-- `- P '125

--

--     * In the Template Haskell splice $$(refined5TH 99)

--       In the expression:

--           $$(refined5TH 99) :: Refined5 OAN Id (Between 100 125 Id) Int

-- @

--

refined5TH :: forall opts ip op i
  . ( Refined2C opts ip op i
    , TH.Lift (PP ip i)
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined5 opts ip op i))
refined5TH :: i -> Q (TExp (Refined5 opts ip op i))
refined5TH i
i =
  case i -> Either Msg2 (Refined5 opts ip op i)
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 i
i of
    Left Msg2
e -> String -> Q (TExp (Refined5 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined5 opts ip op i)))
-> String -> Q (TExp (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
    Right Refined5 opts ip op i
r -> [||r||]

-- | creates a 'Refined5.Refined5' refinement type using IO

refined5THIO :: forall opts ip op i
  . ( TH.Lift (PP ip i)
    , Refined2C opts ip op i
    , Show (PP ip i)
    )
  => i
  -> TH.Q (TH.TExp (Refined5 opts ip op i))
refined5THIO :: i -> Q (TExp (Refined5 opts ip op i))
refined5THIO i
i = do
  Either Msg2 (Refined5 opts ip op i)
x <- IO (Either Msg2 (Refined5 opts ip op i))
-> Q (Either Msg2 (Refined5 opts ip op i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg2 (Refined5 opts ip op i))
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i
       (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' i
i)
  case Either Msg2 (Refined5 opts ip op i)
x of
    Left Msg2
e -> String -> Q (TExp (Refined5 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined5 opts ip op i)))
-> String -> Q (TExp (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
    Right Refined5 opts ip op i
r -> [||r||]