{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Constraints where
import Prelude hiding (null)
import Control.Monad
import qualified Data.List as List
import qualified Data.Set as Set
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.MetaVars.Mention
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
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 Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Impossible
instance MonadConstraint TCM where
catchPatternErr :: TCM a -> TCM a -> TCM a
catchPatternErr = TCM a -> TCM a -> TCM a
forall a. TCM a -> TCM a -> TCM a
catchPatternErrTCM
addConstraint :: Constraint -> TCM ()
addConstraint = Constraint -> TCM ()
addConstraintTCM
addAwakeConstraint :: Constraint -> TCM ()
addAwakeConstraint = Constraint -> TCM ()
addAwakeConstraint'
solveConstraint :: Constraint -> TCM ()
solveConstraint = Constraint -> TCM ()
solveConstraintTCM
solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraints = (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM
wakeConstraints :: (ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints = (ProblemConstraint -> TCM Bool) -> 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
catchPatternErrTCM :: TCM a -> TCM a -> TCM a
catchPatternErrTCM :: TCM a -> TCM a -> TCM a
catchPatternErrTCM handle :: TCM a
handle v :: TCM a
v =
TCM a -> (TCErr -> TCM a) -> TCM a
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ TCM a
v ((TCErr -> TCM a) -> TCM a) -> (TCErr -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \err :: TCErr
err ->
case TCErr
err of
PatternErr{} -> TCM a
handle
_ -> TCErr -> TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
addConstraintTCM :: Constraint -> TCM ()
addConstraintTCM :: Constraint -> TCM ()
addConstraintTCM c :: Constraint
c = do
Set ProblemId
pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.add" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep
[ "adding constraint"
, VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ([ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([ProblemId] -> VerboseKey) -> [ProblemId] -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids)
, Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c ]
Constraint
c <- Constraint -> TCMT IO Constraint
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Constraint -> TCMT IO Constraint)
-> TCMT IO Constraint -> TCMT IO Constraint
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> TCMT IO Constraint
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Constraint
c
TCMT IO (Maybe [Constraint])
-> TCM () -> ([Constraint] -> TCM ()) -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Constraint -> TCMT IO (Maybe [Constraint])
simpl Constraint
c) (Constraint -> TCM ()
addConstraint' Constraint
c) (([Constraint] -> TCM ()) -> TCM ())
-> ([Constraint] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ cs :: [Constraint]
cs -> do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.add" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ " simplified:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ((Constraint -> TCM Doc) -> [Constraint] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constraint -> Bool
isInstanceConstraint Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
(ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' (Constraint -> TCM Bool
isWakeableInstanceConstraint (Constraint -> TCM Bool)
-> (ProblemConstraint -> Constraint)
-> ProblemConstraint
-> TCM 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)
where
isWakeableInstanceConstraint :: Constraint -> TCM Bool
isWakeableInstanceConstraint :: Constraint -> TCM Bool
isWakeableInstanceConstraint = \case
FindInstance _ b :: Maybe MetaId
b _ -> TCM Bool -> (MetaId -> TCM Bool) -> Maybe MetaId -> TCM Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) MetaId -> TCM Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Maybe MetaId
b
_ -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isLvl :: Constraint -> Bool
isLvl LevelCmp{} = Bool
True
isLvl _ = Bool
False
simpl :: Constraint -> TCM (Maybe [Constraint])
simpl :: Constraint -> TCMT IO (Maybe [Constraint])
simpl c :: Constraint
c
| Constraint -> Bool
isLvl Constraint
c = do
[Closure Constraint]
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
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Closure Constraint] -> Bool
forall a. Null a => a -> Bool
null [Closure Constraint]
lvlcs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.lvl" 40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "simplifying level constraint" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> VerboseLevel -> m Doc -> m Doc
hang "using" 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Closure Constraint] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Closure Constraint]
lvlcs
]
Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
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 -> [Constraint] -> Maybe [Constraint]
simplifyLevelConstraint Constraint
c ([Constraint] -> Maybe [Constraint])
-> [Constraint] -> Maybe [Constraint]
forall a b. (a -> b) -> a -> b
$ (Closure Constraint -> Constraint)
-> [Closure Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map Closure Constraint -> Constraint
forall a. Closure a -> a
clValue [Closure Constraint]
lvlcs
| Bool
otherwise = Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Constraint]
forall a. Maybe a
Nothing
wakeConstraintsTCM :: (ProblemConstraint-> TCM Bool) -> TCM ()
wakeConstraintsTCM :: (ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraintsTCM wake :: ProblemConstraint -> TCM Bool
wake = do
Constraints
c <- Lens' Constraints TCState -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Constraints TCState
stSleepingConstraints
(wakeup :: Constraints
wakeup, sleepin :: Constraints
sleepin) <- (ProblemConstraint -> TCM Bool)
-> Constraints -> TCMT IO (Constraints, Constraints)
forall (m :: * -> *) a.
(Functor m, Applicative m) =>
(a -> m Bool) -> [a] -> m ([a], [a])
partitionM ProblemConstraint -> TCM Bool
wake Constraints
c
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.constr.wake" 50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
"waking up " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[ProblemId]] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ((ProblemConstraint -> [ProblemId]) -> Constraints -> [[ProblemId]]
forall a b. (a -> b) -> [a] -> [b]
List.map (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList (Set ProblemId -> [ProblemId])
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) Constraints
wakeup) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ "\n" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
" still sleeping: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[ProblemId]] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ((ProblemConstraint -> [ProblemId]) -> Constraints -> [[ProblemId]]
forall a b. (a -> b) -> [a] -> [b]
List.map (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList (Set ProblemId -> [ProblemId])
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) Constraints
sleepin)
(Constraints -> Constraints) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifySleepingConstraints ((Constraints -> Constraints) -> TCM ())
-> (Constraints -> Constraints) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Constraints -> Constraints -> Constraints
forall a b. a -> b -> a
const Constraints
sleepin
(Constraints -> Constraints) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (Constraints -> Constraints -> Constraints
forall a. [a] -> [a] -> [a]
++ Constraints
wakeup)
stealConstraintsTCM :: ProblemId -> TCM ()
stealConstraintsTCM :: ProblemId -> TCM ()
stealConstraintsTCM pid :: ProblemId
pid = do
Set ProblemId
current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.constr.steal" 50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
current) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " is stealing problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ "'s constraints!"
let rename :: ProblemConstraint -> ProblemConstraint
rename pc :: ProblemConstraint
pc@(PConstr pids :: Set ProblemId
pids c :: Closure Constraint
c) | ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid Set ProblemId
pids = Set ProblemId -> 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) Closure Constraint
c
| Bool
otherwise = ProblemConstraint
pc
TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid (Set ProblemId -> Bool) -> TCMT IO (Set ProblemId) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
(Constraints -> Constraints) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints ((Constraints -> Constraints) -> TCM ())
-> (Constraints -> Constraints) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint)
-> Constraints -> Constraints
forall a b. (a -> b) -> [a] -> [b]
List.map ProblemConstraint -> ProblemConstraint
rename
(Constraints -> Constraints) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifySleepingConstraints ((Constraints -> Constraints) -> TCM ())
-> (Constraints -> Constraints) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint)
-> Constraints -> Constraints
forall a b. (a -> b) -> [a] -> [b]
List.map ProblemConstraint -> ProblemConstraint
rename
noConstraints
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a -> m a
noConstraints :: m a -> m a
noConstraints problem :: m a
problem = do
(pid :: ProblemId
pid, x :: a
x) <- m a -> m (ProblemId, a)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m a
problem
Constraints
cs <- ProblemId -> m Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constraints -> Bool
forall a. Null a => a -> Bool
null Constraints
cs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
TCWarning
w <- Warning -> m TCWarning
forall (m :: * -> *). MonadWarning m => Warning -> m TCWarning
warning_ (Constraints -> Warning
UnsolvedConstraints Constraints
cs)
TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [ TCWarning
w ]
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
newProblem
:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a -> m (ProblemId, a)
newProblem :: m a -> m (ProblemId, a)
newProblem action :: m a
action = do
ProblemId
pid <- m ProblemId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
a
x <- m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ProblemId -> m a -> m a
forall (m :: * -> *) a.
MonadConstraint m =>
ProblemId -> m a -> m a
solvingProblem ProblemId
pid m a
action
m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
(ProblemId, a) -> m (ProblemId, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProblemId
pid, a
x)
newProblem_
:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a -> m ProblemId
newProblem_ :: m a -> m ProblemId
newProblem_ action :: 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 :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints check :: TCM a
check ifNo :: a -> TCM b
ifNo ifCs :: ProblemId -> a -> TCM b
ifCs = do
(pid :: ProblemId
pid, x :: a
x) <- TCM a -> TCMT IO (ProblemId, a)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem TCM a
check
TCM Bool -> TCM b -> TCM b -> TCM b
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProblemId -> TCM Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid) (a -> TCM b
ifNo a
x) (ProblemId -> a -> TCM b
ifCs ProblemId
pid a
x)
ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ check :: TCM ()
check ifNo :: TCM a
ifNo ifCs :: 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) (\pid :: ProblemId
pid _ -> ProblemId -> TCM a
ifCs ProblemId
pid)
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint c :: Constraint
c blocker :: 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) (Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> TCM ())
-> (ProblemId -> Constraint) -> ProblemId -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> ProblemId -> Constraint
Guarded Constraint
c)
whenConstraints :: TCM () -> TCM () -> TCM ()
whenConstraints :: TCM () -> TCM () -> TCM ()
whenConstraints action :: TCM ()
action handler :: TCM ()
handler =
TCM () -> TCM () -> (ProblemId -> TCM ()) -> TCM ()
forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
action (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((ProblemId -> TCM ()) -> TCM ())
-> (ProblemId -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \pid :: ProblemId
pid -> do
ProblemId -> TCM ()
forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints ProblemId
pid
TCM ()
handler
wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' p :: ProblemConstraint -> TCM Bool
p = do
Bool
skipInstance <- TCM Bool
forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch
(ProblemConstraint -> TCM Bool) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> m Bool) -> m ()
wakeConstraints (\ c :: ProblemConstraint
c -> Bool -> Bool -> Bool
(&&) (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
skipInstance Bool -> Bool -> Bool
&& Constraint -> Bool
isInstanceConstraint (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)) (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemConstraint -> TCM Bool
p ProblemConstraint
c)
wakeupConstraints :: MetaId -> TCM ()
wakeupConstraints :: MetaId -> TCM ()
wakeupConstraints x :: MetaId
x = do
(ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' (Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> TCM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> ProblemConstraint -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x)
TCM ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
wakeupConstraints_ :: TCM ()
wakeupConstraints_ :: TCM ()
wakeupConstraints_ = do
(ProblemConstraint -> TCM Bool) -> TCM ()
wakeConstraints' (Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> TCM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True)
TCM ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
solveAwakeConstraints :: (MonadConstraint m) => m ()
solveAwakeConstraints :: m ()
solveAwakeConstraints = Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
False
solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
solveAwakeConstraints' :: Bool -> m ()
solveAwakeConstraints' = (ProblemConstraint -> Bool) -> Bool -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints (Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True)
solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM solveThis :: ProblemConstraint -> Bool
solveThis force :: Bool
force = do
VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS "profile.constraints" 10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
VerboseKey -> Integer -> m ()
tickMax "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
TCM 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) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM 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
Lens' (Set ProblemId) TCEnv
-> (Set ProblemId -> Set ProblemId) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Set ProblemId) TCEnv
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
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.solve" 10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep [ "Solving awake constraints."
, VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Constraints -> VerboseKey) -> Constraints -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> VerboseKey)
-> (Constraints -> VerboseLevel) -> Constraints -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Constraints -> TCM Doc) -> TCMT IO Constraints -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints
, "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
$ \ c :: 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 c :: Constraint
c = do
VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS "profile.constraints" 10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM ()
forall (m :: * -> *). MonadStatistics m => VerboseKey -> m ()
tick "attempted-constraints"
VerboseKey -> VerboseLevel -> VerboseKey -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket "tc.constr.solve" 20 "solving constraint" (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Set ProblemId
pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.solve.constr" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ([ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([ProblemId] -> VerboseKey) -> [ProblemId] -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
Constraint -> TCM ()
solveConstraint_ Constraint
c
solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ :: Constraint -> TCM ()
solveConstraint_ (ValueCmp cmp :: Comparison
cmp a :: CompareAs
a u :: Term
u v :: 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 cmp :: Comparison
cmp p :: Term
p a :: Type
a u :: Term
u v :: 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 cmp :: [Polarity]
cmp fs :: [IsForced]
fs a :: Type
a e :: Term
e u :: [Elim]
u v :: [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_ (TelCmp a :: Type
a b :: Type
b cmp :: Comparison
cmp tela :: Telescope
tela telb :: Telescope
telb) = Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Type -> Comparison -> Telescope -> Telescope -> m ()
compareTel Type
a Type
b Comparison
cmp Telescope
tela Telescope
telb
solveConstraint_ (SortCmp cmp :: Comparison
cmp s1 :: Sort
s1 s2 :: Sort
s2) = Comparison -> Sort -> Sort -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s1 Sort
s2
solveConstraint_ (LevelCmp cmp :: Comparison
cmp a :: Level
a b :: Level
b) = Comparison -> Level -> Level -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Level -> Level -> m ()
compareLevel Comparison
cmp Level
a Level
b
solveConstraint_ c0 :: Constraint
c0@(Guarded c :: Constraint
c pid :: ProblemId
pid) = do
TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProblemId -> TCM Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid)
(do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.constr.solve" 50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Guarding problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " is solved, moving on..."
Constraint -> TCM ()
solveConstraint_ Constraint
c)
(TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.constr.solve" 50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Guarding problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " is still unsolved."
Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint Constraint
c0
solveConstraint_ (IsEmpty r :: Range
r t :: Type
t) = Range -> Type -> TCM ()
ensureEmptyType Range
r Type
t
solveConstraint_ (CheckSizeLtSat t :: Term
t) = Term -> TCM ()
checkSizeLtSat Term
t
solveConstraint_ (UnquoteTactic _ tac :: Term
tac hole :: Term
hole goal :: Type
goal) = Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
hole Type
goal
solveConstraint_ (UnBlock m :: MetaId
m) =
TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCM Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)) (Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (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
MetaInstantiation
inst <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> TCMT IO MetaVariable -> TCMT IO MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.unblock" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ("unblocking a metavar yields the constraint: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaInstantiation -> VerboseKey
forall a. Show a => a -> VerboseKey
show MetaInstantiation
inst)
case MetaInstantiation
inst of
BlockedConst t :: Term
t -> do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr.blocked" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ("blocked const " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " :=") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
MetaId -> [Arg VerboseKey] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m [] Term
t
PostponedTypeCheckingProblem cl :: Closure TypeCheckingProblem
cl unblock :: TCM Bool
unblock -> Closure TypeCheckingProblem
-> (TypeCheckingProblem -> TCM ()) -> TCM ()
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> TCM ()) -> TCM ())
-> (TypeCheckingProblem -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \prob :: TypeCheckingProblem
prob -> do
TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCM Bool
unblock (Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (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
Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
Term
v <- TCM Term -> TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem TypeCheckingProblem
prob
MetaId -> [Arg VerboseKey] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m (Telescope -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
telToArgs Telescope
tel) Term
v
InstV{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Open -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
OpenInstance -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
solveConstraint_ (FindInstance m :: MetaId
m b :: Maybe MetaId
b cands :: Maybe [Candidate]
cands) = MetaId -> Maybe [Candidate] -> TCM ()
findInstance MetaId
m Maybe [Candidate]
cands
solveConstraint_ (CheckFunDef d :: Delayed
d i :: DefInfo
i q :: QName
q cs :: [Clause]
cs) = 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
$
Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef Delayed
d DefInfo
i QName
q [Clause]
cs
solveConstraint_ (HasBiggerSort a :: Sort
a) = Sort -> TCM ()
hasBiggerSort Sort
a
solveConstraint_ (HasPTSRule a :: Dom Type
a b :: Abs Sort
b) = Dom Type -> Abs Sort -> TCM ()
hasPTSRule Dom Type
a Abs Sort
b
solveConstraint_ (CheckMetaInst m :: MetaId
m) = MetaId -> TCM ()
checkMetaInst MetaId
m
checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem p :: TypeCheckingProblem
p = case TypeCheckingProblem
p of
CheckExpr cmp :: Comparison
cmp e :: Expr
e t :: Type
t -> Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
CheckArgs eh :: ExpandHidden
eh r :: Range
r args :: [NamedArg Expr]
args t0 :: Type
t0 t1 :: Type
t1 k :: [Maybe Range] -> [Elim] -> Type -> CheckedTarget -> TCM Term
k -> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> ([Maybe Range] -> [Elim] -> Type -> CheckedTarget -> TCM Term)
-> TCM Term
checkArguments ExpandHidden
eh Range
r [NamedArg Expr]
args Type
t0 Type
t1 [Maybe Range] -> [Elim] -> Type -> CheckedTarget -> TCM Term
k
CheckProjAppToKnownPrincipalArg cmp :: Comparison
cmp e :: Expr
e o :: ProjOrigin
o ds :: NonEmpty QName
ds args :: [NamedArg Expr]
args t :: Type
t k :: VerboseLevel
k v0 :: Term
v0 pt :: Type
pt ->
Comparison
-> Expr
-> ProjOrigin
-> NonEmpty QName
-> [NamedArg Expr]
-> Type
-> VerboseLevel
-> Term
-> Type
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o NonEmpty QName
ds [NamedArg Expr]
args Type
t VerboseLevel
k Term
v0 Type
pt
CheckLambda cmp :: Comparison
cmp args :: Arg ([WithHiding Name], Maybe Type)
args body :: Expr
body target :: Type
target -> Comparison
-> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
checkPostponedLambda Comparison
cmp Arg ([WithHiding Name], Maybe Type)
args Expr
body Type
target
DoQuoteTerm cmp :: Comparison
cmp et :: Term
et t :: Type
t -> Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t
debugConstraints :: TCM ()
debugConstraints :: TCM ()
debugConstraints = VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS "tc.constr" 50 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Constraints
awake <- Lens' Constraints TCState -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Constraints TCState
stAwakeConstraints
Constraints
sleeping <- Lens' Constraints TCState -> TCMT IO Constraints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Constraints TCState
stSleepingConstraints
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.constr" 50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "Current constraints"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ "awake " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((ProblemConstraint -> TCM Doc) -> Constraints -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraints
awake)
, "asleep" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((ProblemConstraint -> TCM Doc) -> Constraints -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraints
sleeping) ] ]