{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Conversion.Pure where

import Control.Monad.Except
import System.IO.Unsafe (unsafeDupablePerformIO)
import Agda.Syntax.Internal

import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.Utils.IORef.Strict qualified as Strict
import Agda.Utils.Impossible

pureConversion ::
       TCM b               -- ^ What to do on `neverUnblock`
    -> (Blocker -> TCM b)  -- ^ What to do on other blockers.
    -> (a -> TCM b)        -- ^ What to do with successful result.
    -> TCM a
    -> TCM b
pureConversion :: forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion TCM b
rigidblock Blocker -> TCM b
flexblock a -> TCM b
nonblocked = \TCM a
m ->
  (TCEnv -> TCEnv) -> TCM b -> TCM b
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
eCompareBlocked Bool
True (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
ePureConversion Bool
True) (TCM b -> TCM b) -> TCM b -> TCM b
forall a b. (a -> b) -> a -> b
$
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM b -> TCM b
forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.pure" VerboseLevel
40 VerboseKey
"runPureConversion" (TCM b -> TCM b) -> TCM b -> TCM b
forall a b. (a -> b) -> a -> b
$ do
    oldState <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    let debugResult TCMT IO Doc
msg =
           VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.conv.pure" VerboseLevel
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"runPureConversion result: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
msg
    res <- (Right <$> m) `catchError` \case
      PatternErr Blocker
block ->
        Either Blocker a -> TCMT IO (Either Blocker a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker a -> TCMT IO (Either Blocker a))
-> Either Blocker a -> TCMT IO (Either Blocker a)
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker a
forall a b. a -> Either a b
Left Blocker
block

      -- András 2024-10-21: we treat this as a rigid blocker. Not sure why,
      -- but the old code did it like this.
      TypeError{} -> do
        TCMT IO Doc -> TCMT IO ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"type error"
        Either Blocker a -> TCMT IO (Either Blocker a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker a -> TCMT IO (Either Blocker a))
-> Either Blocker a -> TCMT IO (Either Blocker a)
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker a
forall a b. a -> Either a b
Left Blocker
neverUnblock

      GenericException{} -> TCMT IO (Either Blocker a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      IOException{}      -> TCMT IO (Either Blocker a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      ParserError{}      -> TCMT IO (Either Blocker a)
forall a. HasCallStack => a
__IMPOSSIBLE__
    putTC oldState
    case res of
      Left Blocker
block | Blocker
block Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> do
        TCMT IO Doc -> TCMT IO ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"stuck"
        TCM b
rigidblock
      Left Blocker
block -> do
        TCMT IO Doc -> TCMT IO ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"blocked on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
block
        Blocker -> TCM b
flexblock Blocker
block
      Right a
a ->
        a -> TCM b
nonblocked a
a
{-# INLINE pureConversion #-}

-- | Run conversion without modifying constraint or meta state. A state
--   modification instead throws a pattern violation.
runPureConversion :: TCM a -> TCM a
runPureConversion :: forall a. TCM a -> TCM a
runPureConversion =
  TCM a -> (Blocker -> TCM a) -> (a -> TCM a) -> TCM a -> TCM a
forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion (Blocker -> TCM a
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock) Blocker -> TCM a
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation a -> TCM a
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Don't catch pattern violation.
pureEqualTerm :: Type -> Term -> Term -> TCM Bool
pureEqualTerm :: Type -> Term -> Term -> TCM Bool
pureEqualTerm Type
a Term
u Term
v =
  TCM Bool
-> (Blocker -> TCM Bool)
-> (() -> TCM Bool)
-> TCMT IO ()
-> TCM Bool
forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion (Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) Blocker -> TCM Bool
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (\()
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) (Type -> Term -> Term -> TCMT IO ()
equalTerm Type
a Term
u Term
v)

-- | Compare terms, catch and return pattern violation.
pureBlockOrEqualTerm :: Type -> Term -> Term -> TCM (Either Blocker Bool)
pureBlockOrEqualTerm :: Type -> Term -> Term -> TCM (Either Blocker Bool)
pureBlockOrEqualTerm Type
a Term
u Term
v =
  TCM (Either Blocker Bool)
-> (Blocker -> TCM (Either Blocker Bool))
-> (() -> TCM (Either Blocker Bool))
-> TCMT IO ()
-> TCM (Either Blocker Bool)
forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion (Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
False) (Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> (Blocker -> Either Blocker Bool)
-> Blocker
-> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Either Blocker Bool
forall a b. a -> Either a b
Left) (\()
_ -> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) (Type -> Term -> Term -> TCMT IO ()
equalTerm Type
a Term
u Term
v)

{-# INLINE pureBlockOrEqualTermPureTCM #-}
pureBlockOrEqualTermPureTCM :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
pureBlockOrEqualTermPureTCM :: forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Either Blocker Bool)
pureBlockOrEqualTermPureTCM Type
a Term
u Term
v = do
  st <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  e  <- askTC
  pure $! unsafeDupablePerformIO $ do
    ref <- Strict.newIORef st
    unTCM (pureBlockOrEqualTerm a u v) ref e

pureBlockOrEqualType :: Type -> Type -> TCM (Either Blocker Bool)
pureBlockOrEqualType :: Type -> Type -> TCM (Either Blocker Bool)
pureBlockOrEqualType Type
a Type
b =
  TCM (Either Blocker Bool)
-> (Blocker -> TCM (Either Blocker Bool))
-> (() -> TCM (Either Blocker Bool))
-> TCMT IO ()
-> TCM (Either Blocker Bool)
forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion (Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
False) (Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> (Blocker -> Either Blocker Bool)
-> Blocker
-> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Either Blocker Bool
forall a b. a -> Either a b
Left) (\()
_ -> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker Bool -> TCM (Either Blocker Bool))
-> Either Blocker Bool -> TCM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) (Type -> Type -> TCMT IO ()
equalType Type
a Type
b)

{-# INLINE pureBlockOrEqualTypePureTCM #-}
pureBlockOrEqualTypePureTCM :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
pureBlockOrEqualTypePureTCM :: forall (m :: * -> *).
PureTCM m =>
Type -> Type -> m (Either Blocker Bool)
pureBlockOrEqualTypePureTCM Type
a Type
a' = do
  st <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  e  <- askTC
  pure $! unsafeDupablePerformIO $ do
    ref <- Strict.newIORef st
    unTCM (pureBlockOrEqualType a a') ref e

pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool
pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool
pureCompareAs Comparison
cmp CompareAs
a Term
u Term
v =
  TCM Bool
-> (Blocker -> TCM Bool)
-> (() -> TCM Bool)
-> TCMT IO ()
-> TCM Bool
forall b a.
TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
pureConversion (Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) Blocker -> TCM Bool
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (\()
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) (Comparison -> CompareAs -> Term -> Term -> TCMT IO ()
compareAs Comparison
cmp CompareAs
a Term
u Term
v)