2
module Agda.TypeChecking.Constraints where
4
import Control.Monad.State
5
import Control.Monad.Reader
6
import Control.Monad.Error
7
import Control.Applicative
9
import Data.List as List
11
import Agda.Syntax.Internal
12
import Agda.TypeChecking.Monad
13
import Agda.TypeChecking.Errors
14
import Agda.TypeChecking.Pretty
15
import Agda.TypeChecking.Reduce
17
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
18
import {-# SOURCE #-} Agda.TypeChecking.Conversion
19
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
20
import {-# SOURCE #-} Agda.TypeChecking.Empty
22
import Agda.Utils.Fresh
24
#include "../undefined.h"
25
import Agda.Utils.Impossible
27
-- | Catch pattern violation errors and adds a constraint.
29
catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
30
catchConstraint c v = liftTCM $
31
catchError v $ \err ->
33
PatternErr s -> put s >> buildConstraint c
36
-- | Try to solve the constraints to be added.
37
addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()
38
addNewConstraints cs = do addConstraints cs; wakeupConstraints
40
-- | Don't allow the argument to produce any constraints.
41
noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()
43
cs <- solveConstraints =<< m
44
unless (List.null cs) $ typeError $ UnsolvedConstraints cs
48
guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
49
guardConstraint m c = do
50
cs <- solveConstraints =<< m
51
case List.partition isSortConstraint cs of -- sort constraints doesn't block anything
52
(scs, []) -> (scs ++) <$> solveConstraint c
53
(scs, cs) -> (scs ++) <$> buildConstraint (Guarded c cs)
55
isSortConstraint = isSC . clValue
57
isSC ValueCmp{} = False
58
isSC TypeCmp{} = False
60
isSC (Guarded c _) = isSC c
61
isSC UnBlock{} = False
62
isSC IsEmpty{} = False
64
-- | We ignore the constraint ids and (as in Agda) retry all constraints every time.
65
-- We probably generate very few constraints.
66
wakeupConstraints :: MonadTCM tcm => tcm ()
67
wakeupConstraints = do
69
cs <- solveConstraints cs
72
solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
73
solveConstraints cs = do
74
n <- length <$> getInstantiatedMetas
75
cs <- concat <$> mapM (withConstraint solveConstraint) cs
76
n' <- length <$> getInstantiatedMetas
78
then solveConstraints cs -- Go again if we made progress
81
solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
82
solveConstraint (ValueCmp cmp a u v) = compareTerm cmp a u v
83
solveConstraint (TypeCmp cmp a b) = compareType cmp a b
84
solveConstraint (TelCmp cmp a b) = compareTel cmp a b
85
solveConstraint (SortCmp cmp s1 s2) = compareSort cmp s1 s2
86
solveConstraint (Guarded c cs) = guardConstraint (return cs) c
87
solveConstraint (IsEmpty t) = isEmptyTypeC t
88
solveConstraint (UnBlock m) = do
89
inst <- mvInstantiation <$> lookupMeta m
90
reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint:" ++ show inst)
93
verboseS "tc.constr.blocked" 15 $ do
95
debug $ show m ++ " := " ++ show d
98
PostponedTypeCheckingProblem cl -> enterClosure cl $ \(e, t, unblock) -> do
101
then buildConstraint $ UnBlock m
103
tel <- getContextTelescope
104
v <- liftTCM $ checkExpr e t
105
assignTerm m $ teleLam tel v
107
-- Andreas, 2009-02-09, the following were IMPOSSIBLE cases
108
-- somehow they pop up in the context of sized types
110
-- already solved metavariables: no constraints left (Ulf, is that correct?)
113
-- Open (whatever that means)
114
Open -> __IMPOSSIBLE__
added
removed
src/full/Agda/TypeChecking/Constraints.hs
