← 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/Free.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/Free.hs
3
3
-- | Computing the free variables of a term.
4
4
module Agda.TypeChecking.Free
5
5
    ( FreeVars(..)
6
 
    , Free(..)
 
6
    , Free
 
7
    , freeVars
7
8
    , allVars
8
9
    , freeIn
 
10
    , freeInIgnoringSorts
9
11
    ) where
10
12
 
11
13
import qualified Data.Set as Set
52
54
 
53
55
-- | Doesn't go inside metas.
54
56
class Free a where
55
 
  freeVars :: a -> FreeVars
 
57
  freeVars' :: FreeConf -> a -> FreeVars
 
58
 
 
59
data FreeConf = FreeConf
 
60
  { fcIgnoreSorts :: Bool
 
61
    -- ^ Ignore free variables in sorts.
 
62
  }
 
63
 
 
64
freeVars :: Free a => a -> FreeVars
 
65
freeVars = freeVars' FreeConf{ fcIgnoreSorts = False }
56
66
 
57
67
instance Free Term where
58
 
  freeVars t = case t of
59
 
    Var n ts   -> singleton n `union` freeVars ts
60
 
    Lam _ t    -> freeVars t
 
68
  freeVars' conf t = case t of
 
69
    Var n ts   -> singleton n `union` freeVars' conf ts
 
70
    Lam _ t    -> freeVars' conf t
61
71
    Lit _      -> empty
62
 
    Def _ ts   -> freeVars ts
63
 
    Con _ ts   -> freeVars ts
64
 
    Pi a b     -> freeVars (a,b)
65
 
    Fun a b    -> freeVars (a,b)
66
 
    Sort _     -> empty
67
 
    MetaV _ ts -> flexible $ freeVars ts
 
72
    Def _ ts   -> freeVars' conf ts
 
73
    Con _ ts   -> freeVars' conf ts
 
74
    Pi a b     -> freeVars' conf (a,b)
 
75
    Fun a b    -> freeVars' conf (a,b)
 
76
    Sort s     -> freeVars' conf s
 
77
    MetaV _ ts -> flexible $ freeVars' conf ts
68
78
 
69
79
instance Free Type where
70
 
  freeVars (El _ t) = freeVars t
 
80
  freeVars' conf (El s t) = freeVars' conf (s, t)
 
81
 
 
82
instance Free Sort where
 
83
  freeVars' conf s
 
84
    | fcIgnoreSorts conf = empty
 
85
    | otherwise          = case s of
 
86
      Type a     -> freeVars' conf a
 
87
      Suc s      -> freeVars' conf s
 
88
      Lub s1 s2  -> freeVars' conf (s1, s2)
 
89
      Prop       -> empty
 
90
      Inf        -> empty
 
91
      MetaS _ ts -> flexible $ freeVars' conf ts
 
92
      DLub s1 s2 -> freeVars' conf (s1, s2)
71
93
 
72
94
instance Free a => Free [a] where
73
 
  freeVars xs = unions $ map freeVars xs
 
95
  freeVars' conf xs = unions $ map (freeVars' conf) xs
74
96
 
75
97
instance (Free a, Free b) => Free (a,b) where
76
 
  freeVars (x,y) = freeVars x `union` freeVars y
 
98
  freeVars' conf (x,y) = freeVars' conf x `union` freeVars' conf y
77
99
 
78
100
instance Free a => Free (Arg a) where
79
 
  freeVars = freeVars . unArg
 
101
  freeVars' conf = freeVars' conf . unArg
80
102
 
81
103
instance Free a => Free (Abs a) where
82
 
  freeVars (Abs _ b) = mapFV (subtract 1) $ delete 0 $ freeVars b
 
104
  freeVars' conf (Abs _ b) = mapFV (subtract 1) $ delete 0 $ freeVars' conf b
83
105
 
84
106
instance Free Telescope where
85
 
  freeVars EmptyTel          = empty
86
 
  freeVars (ExtendTel a tel) = freeVars (a, tel)
 
107
  freeVars' conf EmptyTel            = empty
 
108
  freeVars' conf (ExtendTel a tel) = freeVars' conf (a, tel)
87
109
 
88
110
instance Free ClauseBody where
89
 
  freeVars (Body t)   = freeVars t
90
 
  freeVars (Bind b)   = freeVars b
91
 
  freeVars (NoBind b) = freeVars b
92
 
  freeVars  NoBody    = empty
 
111
  freeVars' conf (Body t)   = freeVars' conf t
 
112
  freeVars' conf (Bind b)   = freeVars' conf b
 
113
  freeVars' conf (NoBind b) = freeVars' conf b
 
114
  freeVars' conf  NoBody    = empty
93
115
 
94
116
freeIn :: Free a => Nat -> a -> Bool
95
117
freeIn v t = v `Set.member` allVars (freeVars t)
96
118
 
 
119
freeInIgnoringSorts :: Free a => Nat -> a -> Bool
 
120
freeInIgnoringSorts v t =
 
121
  v `Set.member` allVars (freeVars' FreeConf{ fcIgnoreSorts = True } t)
 
122