← 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/Rules/Data.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/Rules/Data.hs
5
5
import Control.Applicative
6
6
import Control.Monad
7
7
import Control.Monad.Trans
8
 
import qualified System.IO.UTF8 as UTF8
9
8
 
10
9
import qualified Agda.Syntax.Abstract as A
11
10
import Agda.Syntax.Internal
21
20
import Agda.TypeChecking.Constraints
22
21
import Agda.TypeChecking.Pretty
23
22
import Agda.TypeChecking.Polarity
 
23
import Agda.TypeChecking.Free
24
24
 
25
25
import Agda.TypeChecking.Rules.Term ( isType_ )
26
26
 
57
57
            -- the indices. We count the number of indices and return s.
58
58
            (nofIxs, s) <- splitType =<< normalise t0
59
59
 
 
60
            when (any (`freeIn` s) [0..nofIxs - 1]) $ do
 
61
              err <- fsep [ text "The sort of" <+> prettyTCM name
 
62
                          , text "cannot depend on its indices in the type"
 
63
                          , prettyTCM t0
 
64
                          ]
 
65
              typeError $ GenericError $ show err
 
66
 
 
67
            s <- return $ raise (-nofIxs) s
 
68
 
 
69
            reportSDoc "tc.data.sort" 20 $ vcat
 
70
              [ text "checking datatype" <+> prettyTCM name
 
71
              , nest 2 $ vcat
 
72
                [ text "type:   " <+> prettyTCM t0
 
73
                , text "sort:   " <+> prettyTCM s
 
74
                , text "indices:" <+> text (show nofIxs)
 
75
                ]
 
76
              ]
 
77
 
60
78
            -- Change the datatype from an axiom to a datatype with no constructors.
61
79
            let dataDef = Datatype { dataPars           = npars
62
80
                                   , dataIxs            = nofIxs
108
126
        hideTel (ExtendTel (Arg _ t) tel) = ExtendTel (Arg Hidden t) $ hideTel <$> tel
109
127
 
110
128
        splitType (El _ (Pi _ b))  = ((+ 1) -*- id) <$> splitType (absBody b)
111
 
        splitType (El _ (Fun _ b)) = ((+ 1) -*- id) <$> splitType b
 
129
        splitType (El _ (Fun _ b)) = ((+ 1) -*- raise 1) <$> splitType b
112
130
        splitType (El _ (Sort s))  = return (0, s)
113
131
        splitType (El _ t)         = typeError $ DataMustEndInSort t
114
132
 
124
142
    traceCall (CheckConstructor d tel s con) $ do
125
143
        t <- isType_ e
126
144
        n <- size <$> getContextTelescope
127
 
        verboseS "tc.data.con" 15 $ do
128
 
            td <- prettyTCM t
129
 
            liftIO $ UTF8.putStrLn $ "checking that " ++ show td ++ " ends in " ++ show d
130
 
            liftIO $ UTF8.putStrLn $ "  nofPars = " ++ show n
 
145
        reportSDoc "tc.data.con" 15 $ vcat
 
146
          [ sep [ text "checking that"
 
147
                , nest 2 $ prettyTCM t
 
148
                , text "ends in" <+> prettyTCM d
 
149
                ]
 
150
          , nest 2 $ text "nofPars =" <+> text (show n)
 
151
          ]
131
152
        constructs n t d
132
 
        verboseS "tc.data.con" 15 $ do
133
 
            d <- prettyTCM s
134
 
            liftIO $ UTF8.putStrLn $ "checking that the type fits in " ++ show d
 
153
        reportSDoc "tc.data.con" 15 $ sep
 
154
          [ text "checking that the type fits in"
 
155
          , nest 2 $ prettyTCM s
 
156
          ]
135
157
        t `fitsIn` s
136
158
        escapeContext (size tel)
137
159
            $ addConstant c
163
185
-- | Check that the arguments to a constructor fits inside the sort of the datatype.
164
186
--   The first argument is the type of the constructor.
165
187
fitsIn :: Type -> Sort -> TCM ()
166
 
fitsIn t s =
167
 
    do  t <- instantiate t
168
 
        case funView $ unEl t of
169
 
            FunV arg@(Arg h a) _ -> do
170
 
                let s' = getSort a
171
 
                s' `leqSort` s
172
 
                x <- freshName_ (argName t)
173
 
                let v  = Arg h $ Var 0 []
174
 
                    t' = piApply (raise 1 t) [v]
175
 
                addCtx x arg $ fitsIn t' s
176
 
            _                -> return ()
 
188
fitsIn t s = do
 
189
  t <- instantiateFull t
 
190
  s' <- instantiateFull (getSort t)
 
191
  reportSDoc "tc.data.fits" 10 $
 
192
    sep [ text "does" <+> prettyTCM t
 
193
        , text "of sort" <+> prettyTCM s'
 
194
        , text "fit in" <+> prettyTCM s <+> text "?"
 
195
        ]
 
196
  -- The line below would be simpler, but doesn't allow datatypes
 
197
  -- to be indexed by the universe level.
 
198
--   noConstraints $ s' `leqSort` s
 
199
  case funView $ unEl t of
 
200
    FunV arg@(Arg h a) _ -> do
 
201
      let s' = getSort a
 
202
      cs <- s' `leqSort` s
 
203
      addConstraints cs
 
204
      x <- freshName_ (argName t)
 
205
      let v  = Arg h $ Var 0 []
 
206
          t' = piApply (raise 1 t) [v]
 
207
      addCtx x arg $ fitsIn t' (raise 1 s)
 
208
    _                -> return ()
177
209
 
178
210
-- | Check that a type constructs something of the given datatype. The first
179
211
--   argument is the number of parameters to the datatype.
202
234
 
203
235
                sameVar v i = do
204
236
                    t <- typeOfBV i
205
 
                    noConstraints $ equalTerm t v (Var i [])
 
237
                    addConstraints =<< equalTerm t v (Var i [])
206
238
 
207
239
 
208
240
-- | Force a type to be a specific datatype.