{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Constraints where

import Prelude hiding (null)

import Control.Monad.Except ( MonadError )

import qualified Data.List as List
import qualified Data.Set as Set
import Data.Either

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.LevelConstraints
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Warnings

import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
import {-# SOURCE #-} Agda.TypeChecking.Rules.Data ( checkDataSort )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Empty
import {-# SOURCE #-} Agda.TypeChecking.Lock
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType )

import Agda.Utils.CallStack ( withCurrentCallStack )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null ()
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Singleton

import Agda.Utils.Impossible

instance MonadConstraint TCM where
  addConstraint :: Blocker -> Constraint -> TCM ()
addConstraint             = Blocker -> Constraint -> TCM ()
addConstraintTCM
  addAwakeConstraint :: Blocker -> Constraint -> TCM ()
addAwakeConstraint        = Blocker -> Constraint -> TCM ()
addAwakeConstraint'
  solveConstraint :: Constraint -> TCM ()
solveConstraint           = Constraint -> TCM ()
solveConstraintTCM
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraints = (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraints           = (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM
  stealConstraints :: ProblemId -> TCM ()
stealConstraints          = ProblemId -> TCM ()
stealConstraintsTCM
  modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM ()
modifyAwakeConstraints    = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((Constraints -> Constraints) -> TCState -> TCState)
-> (Constraints -> Constraints)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints
  modifySleepingConstraints :: (Constraints -> Constraints) -> TCM ()
modifySleepingConstraints = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((Constraints -> Constraints) -> TCState -> TCState)
-> (Constraints -> Constraints)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints

addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM Blocker
unblock Constraint
c = do
      pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
      reportSDoc "tc.constr.add" 20 $ hsep
        [ "adding constraint"
        , prettyTCM . PConstr pids unblock =<< buildClosure c
        , "unblocker: " , prettyTCM unblock
        ]
      -- Jesper, 2022-10-22: We should never block on a meta that is
      -- already solved.
      forM_ (allBlockingMetas unblock) $ \ MetaId
m ->
        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCMT IO Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isInstantiatedMeta MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Int
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Attempted to block on solved meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Need to reduce to reveal possibly blocking metas
      c <- reduce =<< instantiateFull c
      caseMaybeM (simpl c) {-no-} (addConstraint' unblock c) $ {-yes-} \ [Constraint]
cs -> do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  simplified:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Constraint -> TCMT IO Doc) -> [Constraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
prettyTCM [Constraint]
cs)
          (Constraint -> TCM ()) -> [Constraint] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Constraint -> TCM ()
solveConstraint_ [Constraint]
cs
      -- The added constraint can cause instance constraints to be solved,
      -- but only the constraints which aren’t blocked on an uninstantiated meta.
      unless (isInstanceConstraint c) $
         wakeConstraints' isWakeableInstanceConstraint
    where
      isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
      isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
isWakeableInstanceConstraint ProblemConstraint
c =
        case Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c of
          FindInstance{}
            | ProblemConstraint -> Blocker
constraintUnblocker ProblemConstraint
c Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock -> WakeUp
WakeUp
          Constraint
_ -> Maybe Blocker -> WakeUp
DontWakeUp Maybe Blocker
forall a. Maybe a
Nothing

      isLvl :: Constraint -> Bool
isLvl LevelCmp{} = Bool
True
      isLvl Constraint
_          = Bool
False

      -- Try to simplify a level constraint
      simpl :: Constraint -> TCM (Maybe [Constraint])
      simpl :: Constraint -> TCMT IO (Maybe [Constraint])
simpl Constraint
c
        | Constraint -> Bool
isLvl Constraint
c = do
          -- Get all level constraints.
          lvlcs <- [Closure Constraint] -> TCMT IO [Closure Constraint]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([Closure Constraint] -> TCMT IO [Closure Constraint])
-> TCMT IO [Closure Constraint] -> TCMT IO [Closure Constraint]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            (Closure Constraint -> Bool)
-> [Closure Constraint] -> [Closure Constraint]
forall a. (a -> Bool) -> [a] -> [a]
List.filter (Constraint -> Bool
isLvl (Constraint -> Bool)
-> (Closure Constraint -> Constraint) -> Closure Constraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue) ([Closure Constraint] -> [Closure Constraint])
-> (Constraints -> [Closure Constraint])
-> Constraints
-> [Closure Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Closure Constraint)
-> Constraints -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint (Constraints -> [Closure Constraint])
-> TCMT IO Constraints -> TCMT IO [Closure Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
          List1.ifNull lvlcs (return Nothing) $ {-else-} \ List1 (Closure Constraint)
lvlcs -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.lvl" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"simplifying level constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
prettyTCM Constraint
c
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"using" Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ List1 (Closure Constraint) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
List1 (Closure Constraint) -> m Doc
prettyTCM List1 (Closure Constraint)
lvlcs
              ]
            -- Try to simplify @c@ using the other constraints.
            Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Constraint] -> TCMT IO (Maybe [Constraint]))
-> Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
forall a b. (a -> b) -> a -> b
$ Constraint -> List1 Constraint -> Maybe [Constraint]
simplifyLevelConstraint Constraint
c (List1 Constraint -> Maybe [Constraint])
-> List1 Constraint -> Maybe [Constraint]
forall a b. (a -> b) -> a -> b
$ (Closure Constraint -> Constraint)
-> List1 (Closure Constraint) -> List1 Constraint
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Closure Constraint -> Constraint
forall a. Closure a -> a
clValue List1 (Closure Constraint)
lvlcs
        | Bool
otherwise = Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Constraint]
forall a. Maybe a
Nothing

wakeConstraintsTCM :: (ProblemConstraint-> WakeUp) -> TCM ()
wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
wake = do
  c <- Lens' TCState Constraints -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Constraints -> f Constraints) -> TCState -> f TCState
Lens' TCState Constraints
stSleepingConstraints
  let (wakeup, sleepin) = partitionEithers $ map checkWakeUp c
  reportSLn "tc.constr.wake" 50 $
    "waking up         " ++ show (List.map (Set.toList . constraintProblems) wakeup) ++ "\n" ++
    "  still sleeping: " ++ show (List.map (Set.toList . constraintProblems) sleepin)
  modifySleepingConstraints $ const sleepin
  modifyAwakeConstraints (++ wakeup)
  where
    checkWakeUp :: ProblemConstraint -> Either ProblemConstraint ProblemConstraint
checkWakeUp ProblemConstraint
c = case ProblemConstraint -> WakeUp
wake ProblemConstraint
c of
      WakeUp
WakeUp              -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
forall a b. a -> Either a b
Left ProblemConstraint
c
      DontWakeUp Maybe Blocker
Nothing  -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
forall a b. b -> Either a b
Right ProblemConstraint
c
      DontWakeUp (Just Blocker
u) -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
forall a b. b -> Either a b
Right ProblemConstraint
c{ constraintUnblocker = u }

-- | Add all constraints belonging to the given problem to the current problem(s).
stealConstraintsTCM :: ProblemId -> TCM ()
stealConstraintsTCM :: ProblemId -> TCM ()
stealConstraintsTCM ProblemId
pid = do
  current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
  reportSLn "tc.constr.steal" 50 $ "problem " ++ show (Set.toList current) ++ " is stealing problem " ++ show pid ++ "'s constraints!"
  -- Add current to any constraint in pid.
  let rename pc :: ProblemConstraint
pc@(PConstr Set ProblemId
pids Blocker
u Closure Constraint
c) | ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid Set ProblemId
pids = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ProblemId
current Set ProblemId
pids) Blocker
u Closure Constraint
c
                                   | Bool
otherwise           = ProblemConstraint
pc
  -- We should never steal from an active problem.
  whenM (Set.member pid <$> asksTC envActiveProblems) __IMPOSSIBLE__
  modifyAwakeConstraints    $ List.map rename
  modifySleepingConstraints $ List.map rename


{-# SPECIALIZE noConstraints :: TCM a -> TCM a #-}
-- | Don't allow the argument to produce any blocking constraints.
--
-- WARNING: this does not mean that the given computation cannot
-- constrain the solution space further.
-- It can well do so, by solving metas.
noConstraints
  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
  => m a -> m a
noConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints = Bool -> m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
Bool -> m a -> m a
noConstraints' Bool
False

-- | As noConstraints but also fail for non-blocking constraints.
reallyNoConstraints
  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
  => m a -> m a
reallyNoConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
reallyNoConstraints = Bool -> m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
Bool -> m a -> m a
noConstraints' Bool
True

noConstraints'
  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
  => Bool -> m a -> m a
noConstraints' :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
Bool -> m a -> m a
noConstraints' Bool
includingNonBlocking m a
problem = do
  (pid, x) <- m a -> m (ProblemId, a)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m a
problem
  let counts | Bool
includingNonBlocking = Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True
             | Bool
otherwise            = Constraint -> Bool
isBlockingConstraint (Constraint -> Bool)
-> (ProblemConstraint -> Constraint) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint
  cs <- List.filter counts <$> getConstraintsForProblem pid
  List1.ifNull cs (pure ()) \ List1 ProblemConstraint
cs -> do
    (CallStack -> m ()) -> m ()
forall b. HasCallStack => (CallStack -> b) -> b
withCurrentCallStack \ CallStack
loc -> do
      w <- CallStack -> Warning -> m TCWarning
forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m TCWarning
warning'_ CallStack
loc (Warning -> m TCWarning) -> Warning -> m TCWarning
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> Warning
UnsolvedConstraints List1 ProblemConstraint
cs
      typeError' loc $ NonFatalErrors $ singleton w
  return x

-- | Run a computation that should succeeds without constraining
--   the solution space, i.e., not add any information about meta-variables.
nonConstraining ::
  ( HasOptions m
  , MonadConstraint m
  , MonadDebug m
  , MonadError TCErr m
  , MonadFresh ProblemId m
  , MonadTCEnv m
  , MonadWarning m
  ) => m a -> m a
nonConstraining :: forall (m :: * -> *) a.
(HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m,
 MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) =>
m a -> m a
nonConstraining = m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints

{-# SPECIALIZE newProblem :: TCM a -> TCM (ProblemId, a) #-}
-- | Create a fresh problem for the given action.
newProblem
  :: (MonadFresh ProblemId m, MonadConstraint m)
  => m a -> m (ProblemId, a)
newProblem :: forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m a
action = do
  pid <- m ProblemId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  -- Don't get distracted by other constraints while working on the problem
  x <- nowSolvingConstraints $ solvingProblem pid action
  -- Now we can check any woken constraints
  solveAwakeConstraints
  return (pid, x)

{-# SPECIALIZE newProblem_ :: TCM a -> TCM ProblemId #-}
newProblem_
  :: (MonadFresh ProblemId m, MonadConstraint m)
  => m a -> m ProblemId
newProblem_ :: forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ m a
action = (ProblemId, a) -> ProblemId
forall a b. (a, b) -> a
fst ((ProblemId, a) -> ProblemId) -> m (ProblemId, a) -> m ProblemId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (ProblemId, a)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m a
action

ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints :: forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints TCM a
check a -> TCM b
ifNo ProblemId -> a -> TCM b
ifCs = do
  (pid, x) <- TCM a -> TCMT IO (ProblemId, a)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem TCM a
check
  ifM (isProblemSolved pid) (ifNo x) (ifCs pid x)

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ :: forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
check TCM a
ifNo ProblemId -> TCM a
ifCs = TCM () -> (() -> TCM a) -> (ProblemId -> () -> TCM a) -> TCM a
forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints TCM ()
check (TCM a -> () -> TCM a
forall a b. a -> b -> a
const TCM a
ifNo) (\ProblemId
pid ()
_ -> ProblemId -> TCM a
ifCs ProblemId
pid)

-- | @guardConstraint c blocker@ tries to solve @blocker@ first.
--   If successful without constraints, it moves on to solve @c@, otherwise it
--   adds a @c@ to the constraint pool, blocked by the problem generated by @blocker@.
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint Constraint
c TCM ()
blocker =
  TCM () -> TCM () -> (ProblemId -> TCM ()) -> TCM ()
forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
blocker (Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint Constraint
c) (\ ProblemId
pid -> Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (ProblemId -> Blocker
unblockOnProblem ProblemId
pid) Constraint
c)

whenConstraints :: TCM () -> TCM () -> TCM ()
whenConstraints :: TCM () -> TCM () -> TCM ()
whenConstraints TCM ()
action TCM ()
handler =
  TCM () -> TCM () -> (ProblemId -> TCM ()) -> TCM ()
forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
action (() -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((ProblemId -> TCM ()) -> TCM ())
-> (ProblemId -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ProblemId
pid -> do
    ProblemId -> TCM ()
forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints ProblemId
pid
    TCM ()
handler

{-# SPECIALIZE wakeupConstraints :: MetaId -> TCM () #-}
-- | Wake up the constraints depending on the given meta.
wakeupConstraints :: MonadMetaSolver m => MetaId -> m ()
wakeupConstraints :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
x = do
  (ProblemConstraint -> WakeUp) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' (MetaId -> Blocker -> WakeUp
wakeIfBlockedOnMeta MetaId
x (Blocker -> WakeUp)
-> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker)
  m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

-- | Wake up all constraints not blocked on a problem.
wakeupConstraints_ :: TCM ()
wakeupConstraints_ :: TCM ()
wakeupConstraints_ = do
  (ProblemConstraint -> WakeUp) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' (Blocker -> WakeUp
wakeup (Blocker -> WakeUp)
-> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker)
  TCM ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
  where
    wakeup :: Blocker -> WakeUp
wakeup Blocker
u | Set ProblemId -> Bool
forall a. Set a -> Bool
Set.null (Set ProblemId -> Bool) -> Set ProblemId -> Bool
forall a b. (a -> b) -> a -> b
$ Blocker -> Set ProblemId
allBlockingProblems Blocker
u = WakeUp
WakeUp
             | Bool
otherwise                        = Maybe Blocker -> WakeUp
DontWakeUp Maybe Blocker
forall a. Maybe a
Nothing

-- | Solve awake constraints matching the predicate. If the second argument is
--   True solve constraints even if already 'isSolvingConstraints'.
solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM ProblemConstraint -> Bool
solveThis Bool
force = do
    ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Constraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickMax [Char]
"max-open-constraints" (Integer -> TCM ())
-> (Constraints -> Integer) -> Constraints -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> Integer
forall i a. Num i => [a] -> i
List.genericLength (Constraints -> TCM ()) -> TCMT IO Constraints -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
    TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool
force Bool -> Bool -> Bool
||) (Bool -> Bool) -> (Bool -> Bool) -> Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
     -- solveSizeConstraints -- Andreas, 2012-09-27 attacks size constrs too early
     -- Ulf, 2016-12-06: Don't inherit problems here! Stored constraints
     -- already contain all their dependencies.
     Lens' TCEnv (Set ProblemId)
-> (Set ProblemId -> Set ProblemId) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a b. a -> b -> a
const Set ProblemId
forall a. Set a
Set.empty) TCM ()
solve
  where
    solve :: TCM ()
solve = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.solve" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"Solving awake constraints."
                                             , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Constraints -> [Char]) -> Constraints -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char]) -> (Constraints -> Int) -> Constraints -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Constraints -> TCMT IO Doc) -> TCMT IO Constraints -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints
                                             , TCMT IO Doc
"remaining." ]
      TCMT IO (Maybe ProblemConstraint)
-> (ProblemConstraint -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM ((ProblemConstraint -> Bool) -> TCMT IO (Maybe ProblemConstraint)
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' ProblemConstraint -> Bool
solveThis) ((ProblemConstraint -> TCM ()) -> TCM ())
-> (ProblemConstraint -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
c -> do
        (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
forall (m :: * -> *) a.
MonadConstraint m =>
(Constraint -> m a) -> ProblemConstraint -> m a
withConstraint Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint ProblemConstraint
c
        TCM ()
solve

solveConstraintTCM :: Constraint -> TCM ()
solveConstraintTCM :: Constraint -> TCM ()
solveConstraintTCM Constraint
c = do
    ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Constraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCM ()
forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"attempted-constraints"
    [Char] -> Int -> [Char] -> TCM () -> TCM ()
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.constr.solve" Int
20 [Char]
"solving constraint" (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
      reportSDoc "tc.constr.solve.constr" 20 $ text (show $ Set.toList pids) <+> prettyTCM c
      solveConstraint_ c

solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ (ValueCmp Comparison
cmp CompareAs
a Term
u Term
v)       = Comparison -> CompareAs -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
a Term
u Term
v
solveConstraint_ (ValueCmpOnFace Comparison
cmp Term
p Type
a Term
u Term
v) = Comparison -> Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace Comparison
cmp Term
p Type
a Term
u Term
v
solveConstraint_ (ElimCmp [Polarity]
cmp [IsForced]
fs Type
a Term
e [Elim]
u [Elim]
v)   = [Polarity]
-> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity]
-> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m ()
compareElims [Polarity]
cmp [IsForced]
fs Type
a Term
e [Elim]
u [Elim]
v
solveConstraint_ (SortCmp Comparison
cmp Sort
s1 Sort
s2)        = Comparison -> Sort -> Sort -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s1 Sort
s2
solveConstraint_ (LevelCmp Comparison
cmp Level
a Level
b)         = Comparison -> Level -> Level -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Level -> Level -> m ()
compareLevel Comparison
cmp Level
a Level
b
solveConstraint_ (IsEmpty Range
r Type
t)              = Range -> Type -> TCM ()
ensureEmptyType Range
r Type
t
solveConstraint_ (CheckSizeLtSat Term
t)         = Term -> TCM ()
checkSizeLtSat Term
t
solveConstraint_ (UnquoteTactic Term
tac Term
hole Type
goal) = Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
hole Type
goal
solveConstraint_ (UnBlock MetaId
m)                =   -- alwaysUnblock since these have their own unblocking logic (for now)
  TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)) (do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.unblock" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"not unblocking", MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m, TCMT IO Doc
"because",
                                                  TCMT IO Bool -> TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) TCMT IO Doc
"it's frozen" TCMT IO Doc
"meta assignments are turned off"]
        Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
alwaysUnblock (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
UnBlock MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    inst <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
    reportSDoc "tc.constr.unblock" 65 $ "unblocking a metavar yields the constraint:" <+> pretty inst
    case inst of
      BlockedConst Term
t -> do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.blocked" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"blocked const " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :=") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
        MetaId -> [Arg [Char]] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m [] Term
t
      PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> Closure TypeCheckingProblem
-> (TypeCheckingProblem -> TCM ()) -> TCM ()
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> TCM ()) -> TCM ())
-> (TypeCheckingProblem -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
prob -> do
          tel <- TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
          v   <- liftTCM $ checkTypeCheckingProblem prob
          assignTerm m (telToArgs tel) v
      -- Andreas, 2009-02-09, the following were IMPOSSIBLE cases
      -- somehow they pop up in the context of sized types
      --
      -- already solved metavariables: should only happen for size
      -- metas (not sure why it does, Andreas?)
      -- Andreas, 2017-07-11:
      -- I think this is because the size solver instantiates
      -- some metas with infinity but does not clean up the UnBlock constraints.
      -- See also issue #2637.
      -- Ulf, 2018-04-30: The size solver shouldn't touch blocked terms! They have
      -- a twin meta that it's safe to solve.
      InstV{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      OpenMeta{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
solveConstraint_ (FindInstance MetaId
m Maybe [Candidate]
cands) = MetaId -> Maybe [Candidate] -> TCM ()
findInstance MetaId
m Maybe [Candidate]
cands
solveConstraint_ (ResolveInstanceHead QName
q) = QName -> TCM ()
resolveInstanceHead QName
q
solveConstraint_ (CheckFunDef DefInfo
i QName
q [Clause]
cs TCErr
_err) = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
  -- re #3498: checking a fundef would normally be cached, but here it's
  -- happening out of order so it would only corrupt the caching log.
  DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef DefInfo
i QName
q [Clause]
cs
solveConstraint_ (CheckLockedVars Term
a Type
b Arg Term
c Type
d)   = Term -> Type -> Arg Term -> Type -> TCM ()
checkLockedVars Term
a Type
b Arg Term
c Type
d
solveConstraint_ (HasBiggerSort Sort
a)      = Sort -> TCM ()
hasBiggerSort Sort
a
solveConstraint_ (HasPTSRule Dom Type
a Abs Sort
b)       = Dom Type -> Abs Sort -> TCM ()
hasPTSRule Dom Type
a Abs Sort
b
solveConstraint_ (CheckDataSort QName
q Sort
s)    = QName -> Sort -> TCM ()
checkDataSort QName
q Sort
s
solveConstraint_ (CheckMetaInst MetaId
m)      = MetaId -> TCM ()
checkMetaInst MetaId
m
solveConstraint_ (CheckType Type
t)          = Type -> TCM ()
forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
t
solveConstraint_ (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
MonadConstraint (TCMT IO) =>
Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' Maybe Sort
ms WhyCheckModality
cc Modality
mod Term
t

checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem = \case
  CheckExpr Comparison
cmp Expr
e Type
t              -> Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
  CheckArgs Comparison
cmp ExpandHidden
eh Expr
hd [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
k -> Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
eh Expr
hd [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
k
  CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds Expr
hd [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm ->
    Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> Expr
-> [NamedArg Expr]
-> Type
-> Int
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds Expr
hd [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm
  CheckLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe Type)
args Expr
body Type
target -> Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TCM Term
checkPostponedLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe Type)
args Expr
body Type
target
  DoQuoteTerm Comparison
cmp Term
et Type
t           -> Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t

debugConstraints :: TCM ()
debugConstraints :: TCM ()
debugConstraints = [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.constr" Int
50 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  awake    <- Lens' TCState Constraints -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Constraints -> f Constraints) -> TCState -> f TCState
Lens' TCState Constraints
stAwakeConstraints
  sleeping <- useTC stSleepingConstraints
  reportSDoc "tc.constr" 50 $ vcat
    [ "Current constraints"
    , nest 2 $ vcat [ "awake " <+> vcat (map prettyTCM awake)
                    , "asleep" <+> vcat (map prettyTCM sleeping) ] ]

-- Update the blocker after some instantiation or pruning might have happened.
updateBlocker :: (PureTCM m) => Blocker -> m Blocker
updateBlocker :: forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker = Blocker -> m Blocker
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate

addAndUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a
addAndUnblocker :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addAndUnblocker Blocker
u
  | Blocker
u Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = m a -> m a
forall a. a -> a
id
  | Bool
otherwise          = (Blocker -> m a) -> m a -> m a
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m a) -> m a -> m a) -> (Blocker -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ Blocker
u' -> do
      u <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
u
      patternViolation (unblockOnBoth u u')

addOrUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a
addOrUnblocker :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
u
  | Blocker
u Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock = m a -> m a
forall a. a -> a
id
  | Bool
otherwise         = (Blocker -> m a) -> m a -> m a
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m a) -> m a -> m a) -> (Blocker -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ Blocker
u' -> do
      u <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
u
      patternViolation (unblockOnEither u u')

-- Reduce a term and call the continuation. If the continuation is
-- blocked, the whole call is blocked either on what blocked the reduction
-- or on what blocked the continuation (using `blockedOnEither`).
withReduced
  :: (Reduce a, IsMeta a, PureTCM m, MonadBlock m)
  => a -> (a -> m b) -> m b
withReduced :: forall a (m :: * -> *) b.
(Reduce a, IsMeta a, PureTCM m, MonadBlock m) =>
a -> (a -> m b) -> m b
withReduced a
a a -> m b
cont = a -> (Blocker -> a -> m b) -> (NotBlocked -> a -> m b) -> m b
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked a
a (\Blocker
b a
a' -> Blocker -> m b -> m b
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
b (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ a -> m b
cont a
a') (\NotBlocked
_ a
a' -> a -> m b
cont a
a')