summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Constraints.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Constraints.hs')
-rw-r--r--src/full/Agda/TypeChecking/Constraints.hs50
1 files changed, 36 insertions, 14 deletions
diff --git a/src/full/Agda/TypeChecking/Constraints.hs b/src/full/Agda/TypeChecking/Constraints.hs
index 2271202..9ff4854 100644
--- a/src/full/Agda/TypeChecking/Constraints.hs
+++ b/src/full/Agda/TypeChecking/Constraints.hs
@@ -1,13 +1,22 @@
{-# LANGUAGE CPP #-}
+{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Constraints where
-import Control.Monad.State
+import Prelude hiding (null)
+
+import Control.Applicative hiding (empty)
+
+import Control.Monad
import Control.Monad.Reader
-import Control.Applicative
-import Data.List as List
+import Control.Monad.State
+import Control.Monad.Trans.Maybe
+
+import Data.List as List hiding (null)
import Agda.Syntax.Internal
+
+import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Pretty
@@ -22,10 +31,14 @@ import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.Utils.Except ( MonadError(throwError) )
+import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Lens
+import Agda.Utils.Size
+import qualified Agda.Utils.VarSet as VarSet
#include "undefined.h"
import Agda.Utils.Impossible
@@ -71,22 +84,31 @@ addConstraint c = do
isIFSConstraint FindInScope{} = True
isIFSConstraint _ = False
+ isLvl LevelCmp{} = True
+ isLvl _ = False
+
+ -- Try to simplify a level constraint
simpl :: Constraint -> TCM Constraint
- simpl c = do
+ simpl c = if not $ isLvl c then return c else do
n <- genericLength <$> getContext
- let isLvl LevelCmp{} = True
- isLvl _ = False
- cs <- getAllConstraints
- lvls <- instantiateFull $ List.filter (isLvl . clValue . theConstraint) cs
- when (not $ List.null lvls) $ reportSDoc "tc.constr.add" 40 $ text " simplifying using" <+> prettyTCM lvls
- return $ simplifyLevelConstraint n c lvls
+ cs <- map theConstraint <$> getAllConstraints
+ lvls <- instantiateFull $ List.filter (isLvl . clValue) cs
+ when (not $ null lvls) $ do
+ reportSDoc "tc.constr.lvl" 40 $ text "simplifying level constraint" <+> prettyTCM c
+ $$ nest 2 (hang (text "using") 2 (prettyTCM lvls))
+ let c' = simplifyLevelConstraint c $ map clValue lvls
+ reportSDoc "tc.constr.lvl" 40 $
+ if c' /= c then text "simplified to" <+> prettyTCM c'
+ else text "no simplification"
+ return c'
-- | Don't allow the argument to produce any constraints.
noConstraints :: TCM a -> TCM a
noConstraints problem = liftTCM $ do
(pid, x) <- newProblem problem
cs <- getConstraintsForProblem pid
- unless (List.null cs) $ typeError $ UnsolvedConstraints cs
+ w <- warning_ (UnsolvedConstraints cs)
+ unless (null cs) $ typeError $ NonFatalErrors [ w ]
return x
-- | Create a fresh problem for the given action.
@@ -144,7 +166,9 @@ solveAwakeConstraints' force = do
verboseS "profile.constraints" 10 $ liftTCM $ tickMax "max-open-constraints" . genericLength =<< getAllConstraints
whenM ((force ||) . not <$> isSolvingConstraints) $ nowSolvingConstraints $ do
-- solveSizeConstraints -- Andreas, 2012-09-27 attacks size constrs too early
- solve
+ -- Ulf, 2016-12-06: Don't inherit problems here! Stored constraints
+ -- already contain all their dependencies.
+ locally eActiveProblems (const []) solve
where
solve = do
reportSDoc "tc.constr.solve" 10 $ hsep [ text "Solving awake constraints."
@@ -194,7 +218,6 @@ solveConstraint_ (UnBlock m) =
-- already solved metavariables: should only happen for size
-- metas (not sure why it does, Andreas?)
InstV{} -> return ()
- InstS{} -> return ()
-- Open (whatever that means)
Open -> __IMPOSSIBLE__
OpenIFS -> __IMPOSSIBLE__
@@ -215,4 +238,3 @@ debugConstraints = verboseS "tc.constr" 50 $ do
[ text "Current constraints"
, nest 2 $ vcat [ text "awake " <+> vcat (map prettyTCM awake)
, text "asleep" <+> vcat (map prettyTCM sleeping) ] ]
-