{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.Constraints where

import Prelude hiding (null)

import Control.DeepSeq (NFData)

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

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

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.InstanceArguments
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.LevelConstraints
import Mikan.TypeChecking.Sort

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

import Mikan.Utils.CallStack ( withCurrentCallStack )
import Mikan.Utils.List
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null (unlessNullM)
import Mikan.Interaction.Options.ProfileOptions qualified as Profile

import Mikan.Utils.Impossible
import Mikan.Utils.Function (applyUnless)

instance MonadConstraint TCM where
  addConstraint :: Blocker -> Constraint -> TCM ()
addConstraint Blocker
u Constraint
c = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Blocker -> Constraint -> TCM ()
addConstraintTCM Blocker
u Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  addAwakeConstraint :: Blocker -> Constraint -> TCM ()
addAwakeConstraint Blocker
u Constraint
c  = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Blocker -> Constraint -> TCM ()
addAwakeConstraint' Blocker
u Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u

  solveConstraint :: Constraint -> TCM ()
solveConstraint Constraint
c = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Constraint -> TCM ()
solveConstraintTCM Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock -- TODO: does this happen?

  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
s Bool
f = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ((ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM ProblemConstraint -> Bool
s Bool
f) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE wakeConstraints #-}
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraints ProblemConstraint -> WakeUp
w             = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ((ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
w)  (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE stealConstraints #-}
  stealConstraints :: ProblemId -> TCM ()
stealConstraints ProblemId
w            = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (ProblemId -> TCM ()
stealConstraintsTCM ProblemId
w) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE modifyConstraints #-}
  modifyConstraints :: (Constraints -> Constraints)
-> (Constraints -> Constraints) -> TCM ()
modifyConstraints Constraints -> Constraints
f Constraints -> Constraints
g = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv
    ((TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints Constraints -> Constraints
f (TCState -> TCState) -> (TCState -> TCState) -> TCState -> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints Constraints -> Constraints
g))
    (Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock) -- TODO: does this happen?


addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM Blocker
unblock Constraint
c = do
  pids <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  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 (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

{-# INLINE wakeConstraintsTCM #-}
wakeConstraintsTCM :: (ProblemConstraint-> WakeUp) -> TCM ()
wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
wake = do
  tc <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  let c = TCState
tc TCState -> Getting Constraints TCState Constraints -> Constraints
forall s a. s -> Getting a s a -> a
^. Getting Constraints TCState Constraints
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)
  putTC $!
    mapAwakeConstraints (++! wakeup) $ -- TODO: quadratic append!!
      mapSleepingConstraints (const sleepin) tc
  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 <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  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 <$> viewTC eActiveProblems) __IMPOSSIBLE__
  modifyTC $   mapAwakeConstraints    (map' rename)
             . mapSleepingConstraints (map' rename)

{-# SPECIALIZE noConstraints :: TCM a -> TCM a #-}
-- | Error out with @'NonFatalErrors' 'UnsolvedConstraints'@
-- if the computation produced 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, MonadFresh ProblemId m)
  => m a -> m a
noConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadFresh ProblemId m) =>
m a -> m a
noConstraints = Bool -> m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadFresh ProblemId m) =>
Bool -> m a -> m a
noConstraints' Bool
False

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

-- | Error out with @'NonFatalErrors' 'UnsolvedConstraints'@
--   when given computation produced constraints ('True') or blocking constraints ('False').
noConstraints' ::
     (MonadConstraint m, MonadFresh ProblemId m)
  => Bool -> m a -> m a
noConstraints' :: forall (m :: * -> *) a.
(MonadConstraint 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
  -- Consider only blocking constraints unless @includingNonBlocking@.
  let isBlocking = 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 <- applyUnless includingNonBlocking (List.filter isBlocking) <$> getConstraintsForProblem pid
  List1.unlessNull cs \ List1 ProblemConstraint
cs -> (CallStack -> m ()) -> m ()
forall b. HasCallStack => (CallStack -> b) -> b
withCurrentCallStack \ CallStack
loc -> do
    CallStack -> NoConstraintsError -> m ()
forall (m :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> m a
typeError' CallStack
loc (NoConstraintsError -> m ()) -> NoConstraintsError -> m ()
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> NoConstraintsError
NoConstraintsError List1 ProblemConstraint
cs
  return x

newtype NoConstraintsError
  = NoConstraintsError { NoConstraintsError -> List1 ProblemConstraint
nceConstraints :: List1.List1 ProblemConstraint }
  deriving (Int -> NoConstraintsError -> [Char] -> [Char]
[NoConstraintsError] -> [Char] -> [Char]
NoConstraintsError -> [Char]
(Int -> NoConstraintsError -> [Char] -> [Char])
-> (NoConstraintsError -> [Char])
-> ([NoConstraintsError] -> [Char] -> [Char])
-> Show NoConstraintsError
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> NoConstraintsError -> [Char] -> [Char]
showsPrec :: Int -> NoConstraintsError -> [Char] -> [Char]
$cshow :: NoConstraintsError -> [Char]
show :: NoConstraintsError -> [Char]
$cshowList :: [NoConstraintsError] -> [Char] -> [Char]
showList :: [NoConstraintsError] -> [Char] -> [Char]
Show, NoConstraintsError -> ()
(NoConstraintsError -> ()) -> NFData NoConstraintsError
forall a. (a -> ()) -> NFData a
$crnf :: NoConstraintsError -> ()
rnf :: NoConstraintsError -> ()
NFData)

instance PrettyTCM NoConstraintsError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NoConstraintsError -> m Doc
prettyTCM (NoConstraintsError List1 ProblemConstraint
cs) = UnsolvedWarning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnsolvedWarning -> m Doc
prettyTCM (UnsolvedWarning -> m Doc) -> UnsolvedWarning -> m Doc
forall a b. (a -> b) -> a -> b
$ List1 ProblemConstraint -> UnsolvedWarning
UnsolvedConstraints List1 ProblemConstraint
cs

instance Diagnostic NoConstraintsError where
  diagnosticReason :: NoConstraintsError -> DiagnosticReason
diagnosticReason NoConstraintsError
_ = DiagnosticReason
DiagError
  diagnosticString :: NoConstraintsError -> [Char]
diagnosticString NoConstraintsError
_ = [Char]
"UnsolvedConstraints"

-- | Run a computation that should succeed without constraining the
-- solution space, i.e., not add any information about meta-variables.
nonConstraining ::
  ( MonadFresh ProblemId m
  , MonadMetaSolver m
  , MonadTCM m
  ) => m a -> m a
nonConstraining :: forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadMetaSolver m, MonadTCM m) =>
m a -> m a
nonConstraining = [Char] -> Int -> [Char] -> m a -> m a
forall a. [Char] -> Int -> [Char] -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.constr.nonconstraining" Int
30 [Char]
"nonConstraining" (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, MonadFresh ProblemId m) =>
m a -> m a
noConstraints (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.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas

{-# INLINE newProblem #-}
-- | 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)

{-# INLINE newProblem_ #-}
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

{-# INLINE newProblemDontWake_ #-}
-- | Create a fresh problem for the given action. Don't wake problems after the action finishes.
newProblemDontWake_
  :: (MonadFresh ProblemId m, MonadConstraint m)
  => m a -> m ProblemId
newProblemDontWake_ :: forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblemDontWake_ 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
  _ <- nowSolvingConstraints $
         verboseBracket "tc.constr.solve" 50 ("working on problem " ++ show pid) $
           localTC (over eActiveProblems (Set.insert pid)) action
  pure pid

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
  let
    solveLoop :: TCM ()
solveLoop = do
      [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.constr.solve" Int
10 do
        TCMT IO Constraints -> (Constraints -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints \ Constraints
cs ->
          [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) -> (Int -> [Char]) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> TCMT IO Doc) -> Int -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Constraints -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Constraints
cs, 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
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 ()
solveLoop

  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] -> Word64 -> TCM ()
forall (m :: * -> *). MonadStatistics m => [Char] -> Word64 -> m ()
tickMax [Char]
"max-open-constraints" (Word64 -> TCM ())
-> (Constraints -> Word64) -> Constraints -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> Word64
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
$
    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 () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM ()
solveLoop

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 <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
      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 ()
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 ()
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 ()
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 ()
compareSort Comparison
cmp Sort
s1 Sort
s2
solveConstraint_ (LevelCmp Comparison
cmp Level
a Level
b)         = Comparison -> Level -> Level -> TCM ()
compareLevel Comparison
cmp Level
a Level
b
solveConstraint_ (IsEmpty Range
r Type
t)              = Range -> Type -> TCM ()
ensureEmptyType Range
r Type
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
<$> Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas)) (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 ShortText] -> Term -> TCM ()
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

      InstV{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      OpenMeta{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

solveConstraint_ (FindInstance Range
_ MetaId
m Maybe [Candidate]
cands) = MetaId -> Maybe [Candidate] -> TCM ()
findInstance MetaId
m Maybe [Candidate]
cands
solveConstraint_ (ResolveInstanceHead KwRange
kwr QName
q) = KwRange -> QName -> TCM ()
resolveInstanceHead KwRange
kwr 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_ (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 ()
checkType Type
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
  CheckWithApp     Comparison
cmp Type
t WithAppHead
hd QName
f [Elim]
es List1 Expr
as -> Comparison
-> Type -> WithAppHead -> QName -> [Elim] -> List1 Expr -> TCM Term
checkWithApplication Comparison
cmp Type
t WithAppHead
hd QName
f [Elim]
es List1 Expr
as
  CheckWithAppHead Comparison
cmp Type
t Expr
hd Term
tm List1 Expr
as   -> Comparison -> Type -> Expr -> Term -> List1 Expr -> TCM Term
checkWithAppHead Comparison
cmp Type
t Expr
hd Term
tm List1 Expr
as
  DoQuoteTerm Comparison
cmp Term
et Type
t              -> Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t
  DisambiguateConstructor ConstructorDisambiguationData
bcd ConHead -> TCM Term
k     -> ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
disambiguateConstructor' ConstructorDisambiguationData
bcd ConHead -> TCM Term
k
  CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm ->
    Comparison
-> Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> Type
-> Int
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm

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    <- Getter TCState Constraints -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Constraints -> f Constraints) -> TCState -> f TCState
Lens' TCState Constraints
Getter 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
u' -> do
    u <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
u
    patternViolation (unblockOnBoth u u')
{-# INLINE addAndUnblocker #-}

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
u' -> do
    u <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
u
    patternViolation (unblockOnEither u u')
{-# INLINE addOrUnblocker #-}

-- 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')