← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Constraints.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-05 23:43:20 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu
Tags: 2.2.6-1
http://bugs.debian.org/559197
* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian) 
* debian/README.source: Remove, no repacking so not necessary any more 
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed. 
    (Closes: #559197). 
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Constraints.hs
1
1
{-# LANGUAGE CPP #-}
2
2
module Agda.TypeChecking.Constraints where
3
3
 
 
4
import System.IO
 
5
 
4
6
import Control.Monad.State
5
7
import Control.Monad.Reader
6
8
import Control.Monad.Error
7
9
import Control.Applicative
8
10
import Data.Map as Map
9
11
import Data.List as List
 
12
import Data.Set as Set
10
13
 
11
14
import Agda.Syntax.Internal
12
15
import Agda.TypeChecking.Monad
18
21
import {-# SOURCE #-} Agda.TypeChecking.Conversion
19
22
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
20
23
import {-# SOURCE #-} Agda.TypeChecking.Empty
 
24
import Agda.TypeChecking.Free
21
25
 
22
26
import Agda.Utils.Fresh
23
27
 
29
33
catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
30
34
catchConstraint c v = liftTCM $
31
35
   catchError v $ \err ->
32
 
   case err of
 
36
   case errError err of
33
37
       PatternErr s -> put s >> buildConstraint c
34
38
       _            -> throwError err
35
39
 
48
52
guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
49
53
guardConstraint m c = do
50
54
    cs <- solveConstraints =<< m
51
 
    case List.partition isSortConstraint cs of   -- sort constraints doesn't block anything
 
55
    case List.partition isNonBlocking cs of
52
56
        (scs, []) -> (scs ++) <$> solveConstraint c
53
57
        (scs, cs) -> (scs ++) <$> buildConstraint (Guarded c cs)
54
58
    where
55
 
        isSortConstraint = isSC . clValue
56
 
        isSC SortCmp{}     = True
57
 
        isSC ValueCmp{}    = False
58
 
        isSC TypeCmp{}     = False
59
 
        isSC TelCmp{}      = False
60
 
        isSC (Guarded c _) = isSC c
61
 
        isSC UnBlock{}     = False
62
 
        isSC IsEmpty{}     = False
 
59
        isNonBlocking = isNB . clValue
 
60
        isNB SortCmp{}        = True
 
61
        isNB ValueCmp{}       = False
 
62
        isNB TypeCmp{}        = False
 
63
        isNB TelCmp{}         = False
 
64
        isNB (Guarded c _)    = isNB c
 
65
        isNB UnBlock{}        = False
 
66
        isNB IsEmpty{}        = False
63
67
 
64
68
-- | We ignore the constraint ids and (as in Agda) retry all constraints every time.
65
69
--   We probably generate very few constraints.
70
74
    addConstraints cs
71
75
 
72
76
solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
 
77
solveConstraints [] = return []
73
78
solveConstraints cs = do
 
79
    reportSDoc "tc.constr.solve" 60 $
 
80
      sep [ text "{ solving", nest 2 $ prettyTCM cs ]
74
81
    n  <- length <$> getInstantiatedMetas
 
82
    cs0 <- return cs
75
83
    cs <- concat <$> mapM (withConstraint solveConstraint) cs
76
84
    n' <- length <$> getInstantiatedMetas
77
 
    if (n' > n)
 
85
    reportSDoc "tc.constr.solve" 70 $
 
86
      sep [ text "new constraints", nest 2 $ prettyTCM cs ]
 
87
    cs <- if (n' > n)
78
88
        then solveConstraints cs -- Go again if we made progress
79
89
        else return cs
 
90
    reportSLn "tc.constr.solve" 60 $ "solved constraints }"
 
91
    return cs
80
92
 
81
93
solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
82
94
solveConstraint (ValueCmp cmp a u v) = compareTerm cmp a u v
87
99
solveConstraint (IsEmpty t)          = isEmptyTypeC t
88
100
solveConstraint (UnBlock m)          = do
89
101
    inst <- mvInstantiation <$> lookupMeta m
90
 
    reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint:" ++ show inst)
 
102
    reportSDoc "tc.constr.unblock" 15 $ text ("unblocking a metavar yields the constraint: " ++ show inst)
91
103
    case inst of
92
104
      BlockedConst t -> do
93
 
        verboseS "tc.constr.blocked" 15 $ do
94
 
            d <- prettyTCM t
95
 
            debug $ show m ++ " := " ++ show d
 
105
        reportSDoc "tc.constr.blocked" 15 $
 
106
          text ("blocked const " ++ show m ++ " :=") <+> prettyTCM t
96
107
        assignTerm m t
97
108
        return []
98
109
      PostponedTypeCheckingProblem cl -> enterClosure cl $ \(e, t, unblock) -> do