← 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/MetaVars/Occurs.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/MetaVars/Occurs.hs
 
1
 
 
2
module Agda.TypeChecking.MetaVars.Occurs where
 
3
 
 
4
import Control.Applicative
 
5
import Control.Monad
 
6
import Control.Monad.Error
 
7
 
 
8
import Agda.Syntax.Common
 
9
import Agda.Syntax.Internal
 
10
import Agda.TypeChecking.Monad
 
11
import Agda.TypeChecking.Reduce
 
12
import Agda.TypeChecking.Pretty
 
13
import Agda.Utils.Monad
 
14
 
 
15
-- | Extended occurs check.
 
16
class Occurs t where
 
17
  occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM t
 
18
 
 
19
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term
 
20
occursCheck m xs v = liftTCM $ do
 
21
  v <- instantiate v
 
22
  case v of
 
23
    -- Don't fail if trying to instantiate to just itself
 
24
    MetaV m' _        | m == m' -> patternViolation
 
25
    Sort (MetaS m' _) | m == m' -> patternViolation
 
26
    _                           ->
 
27
                              -- Produce nicer error messages
 
28
      occurs typeError m xs v `catchError` \err -> case errError err of
 
29
        TypeError _ cl -> case clValue cl of
 
30
          MetaOccursInItself{} ->
 
31
            typeError . GenericError . show =<<
 
32
              fsep [ text ("Refuse to construct infinite term by instantiating " ++ show m ++ " to")
 
33
                   , prettyTCM v
 
34
                   ]
 
35
          MetaCannotDependOn _ _ i ->
 
36
            ifM ((&&) <$> isSortMeta m <*> (not <$> hasUniversePolymorphism))
 
37
            ( typeError . GenericError . show =<<
 
38
              fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to")
 
39
                   , prettyTCM v
 
40
                   , text "since universe polymorphism is not enabled"
 
41
                   , text "(use the --universe-polymorphism flag to enable)"
 
42
                   ]
 
43
            )
 
44
            ( typeError . GenericError . show =<<
 
45
              fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to")
 
46
                   , prettyTCM v
 
47
                   , text "since it contains the variable"
 
48
                   , enterClosure cl $ \_ -> prettyTCM (Var i [])
 
49
                   , text $ "which " ++ show m ++ " cannot depend on"
 
50
                   ]
 
51
            )
 
52
          _ -> throwError err
 
53
        _ -> throwError err
 
54
 
 
55
instance Occurs Term where
 
56
    occurs abort m xs v = do
 
57
        v <- reduceB v
 
58
        case v of
 
59
            -- Don't fail on blocked terms or metas
 
60
            Blocked _ v  -> occurs' (const patternViolation) v
 
61
            NotBlocked v -> occurs' abort v
 
62
        where
 
63
            occurs' abort v = case v of
 
64
                Var i vs   -> do
 
65
                  unless (i `elem` xs) $ abort $ MetaCannotDependOn m xs i
 
66
                  Var i <$> occ vs
 
67
                Lam h f     -> Lam h <$> occ f
 
68
                Lit l       -> return v
 
69
                Def c vs    -> Def c <$> occ vs
 
70
                Con c vs    -> Con c <$> occ vs
 
71
                Pi a b      -> uncurry Pi <$> occ (a,b)
 
72
                Fun a b     -> uncurry Fun <$> occ (a,b)
 
73
                Sort s      -> Sort <$> occ s
 
74
                MetaV m' vs -> do
 
75
                    when (m == m') $ abort $ MetaOccursInItself m
 
76
                    -- Don't fail on flexible occurrence
 
77
                    MetaV m' <$> occurs (const patternViolation) m xs vs
 
78
                where
 
79
                    occ x = occurs abort m xs x
 
80
 
 
81
instance Occurs Type where
 
82
    occurs abort m xs (El s v) = uncurry El <$> occurs abort m xs (s,v)
 
83
 
 
84
instance Occurs Sort where
 
85
    occurs abort m xs s =
 
86
        do  s' <- reduce s
 
87
            case s' of
 
88
                MetaS m' args -> do
 
89
                  when (m == m') $ abort $ MetaOccursInItself m
 
90
                  MetaS m' <$> occurs (const patternViolation) m xs args
 
91
                Lub s1 s2  -> uncurry Lub <$> occurs abort m xs (s1,s2)
 
92
                DLub s1 s2 -> uncurry DLub <$> occurs abort m xs (s1, s2)
 
93
                Suc s      -> Suc <$> occurs abort m xs s
 
94
                Type a     -> Type <$> occurs abort m xs a
 
95
                Prop       -> return s'
 
96
                Inf        -> return s'
 
97
 
 
98
instance Occurs a => Occurs (Abs a) where
 
99
    occurs abort m xs (Abs s x) = Abs s <$> occurs abort m (0 : map (1+) xs) x
 
100
 
 
101
instance Occurs a => Occurs (Arg a) where
 
102
    occurs abort m xs (Arg h x) = Arg h <$> occurs abort m xs x
 
103
 
 
104
instance (Occurs a, Occurs b) => Occurs (a,b) where
 
105
    occurs abort m xs (x,y) = (,) <$> occurs abort m xs x <*> occurs abort m xs y
 
106
 
 
107
instance Occurs a => Occurs [a] where
 
108
    occurs abort m xs ys = mapM (occurs abort m xs) ys
 
109