module Agda.TypeChecking.Constraints where
import System.IO
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Error
import Control.Applicative
import Data.Map as Map
import Data.List as List
import Data.Set as Set
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Empty
import Agda.TypeChecking.UniversePolymorphism
import Agda.TypeChecking.Free
import Agda.Utils.Fresh
#include "../undefined.h"
import Agda.Utils.Impossible
catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
catchConstraint c v = liftTCM $
catchError_ v $ \err ->
case errError err of
PatternErr s -> put s >> buildConstraint c
_ -> throwError err
addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()
addNewConstraints cs = do addConstraints cs; wakeupConstraints
noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()
noConstraints m = do
cs <- solveConstraints =<< m
unless (List.null cs) $ typeError $ UnsolvedConstraints cs
return ()
guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
guardConstraint m c = do
cs <- solveConstraints =<< m
case List.partition isNonBlocking cs of
(scs, []) -> (scs ++) <$> solveConstraint c
(scs, cs) -> (scs ++) <$> buildConstraint (Guarded c cs)
where
isNonBlocking = isNB . clValue
isNB SortCmp{} = True
isNB LevelCmp{} = True
isNB ValueCmp{} = False
isNB ArgsCmp{} = False
isNB TypeCmp{} = False
isNB TelCmp{} = False
isNB (Guarded c _) = isNB c
isNB UnBlock{} = False
isNB IsEmpty{} = False
wakeupConstraints :: MonadTCM tcm => tcm ()
wakeupConstraints = do
cs <- takeConstraints
cs <- solveConstraints cs
addConstraints cs
solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
solveConstraints [] = return []
solveConstraints cs = do
reportSDoc "tc.constr.solve" 60 $
sep [ text "{ solving", nest 2 $ prettyTCM cs ]
n <- length <$> getInstantiatedMetas
cs0 <- return cs
cs <- concat <$> mapM (withConstraint solveConstraint) cs
n' <- length <$> getInstantiatedMetas
reportSDoc "tc.constr.solve" 70 $
sep [ text "new constraints", nest 2 $ prettyTCM cs
, nest 2 $ text $ "progress: " ++ show n' ++ " --> " ++ show n
]
cs <- if (n' > n)
then solveConstraints cs
else return cs
reportSLn "tc.constr.solve" 60 $ "solved constraints }"
return cs
solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
solveConstraint (ValueCmp cmp a u v) = compareTerm cmp a u v
solveConstraint (ArgsCmp cmp a u v) = compareArgs cmp a u v
solveConstraint (TypeCmp cmp a b) = compareType cmp a b
solveConstraint (TelCmp cmp a b) = compareTel cmp a b
solveConstraint (SortCmp cmp s1 s2) = compareSort cmp s1 s2
solveConstraint (LevelCmp cmp a b) = compareLevel cmp a b
solveConstraint (Guarded c cs) = guardConstraint (return cs) c
solveConstraint (IsEmpty t) = isEmptyTypeC t
solveConstraint (UnBlock m) = do
inst <- mvInstantiation <$> lookupMeta m
reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint: " ++ show inst)
case inst of
BlockedConst t -> do
reportSDoc "tc.constr.blocked" 15 $
text ("blocked const " ++ show m ++ " :=") <+> prettyTCM t
assignTerm m t
return []
PostponedTypeCheckingProblem cl -> enterClosure cl $ \(e, t, unblock) -> do
b <- liftTCM unblock
if not b
then buildConstraint $ UnBlock m
else do
tel <- getContextTelescope
v <- liftTCM $ checkExpr e t
assignTerm m $ teleLam tel v
return []
InstV{} -> return []
InstS{} -> return []
Open -> __IMPOSSIBLE__