← 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/LHS/Unify.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/LHS/Unify.hs
9
9
 
10
10
import Data.Map (Map)
11
11
import qualified Data.Map as Map
12
 
import Data.List
 
12
import Data.List hiding (sort)
 
13
import Data.Traversable (traverse)
13
14
 
14
15
import Agda.Syntax.Common
15
16
import Agda.Syntax.Internal
184
185
      case funView $ unEl a of
185
186
        FunV (Arg _ b) _  -> do
186
187
          unify b u v
 
188
          arg <- traverse ureduce arg
187
189
          unifyArgs (a `piApply` [arg]) us vs
188
190
        _         -> __IMPOSSIBLE__
189
191
 
230
232
        (u, Var j []) | flexible j -> j |->> (u, a)
231
233
        (Con c us, Con c' vs)
232
234
          | c == c' -> do
233
 
              -- The type is a datatype or a record.
234
 
              Def d args <- reduce $ unEl a
235
 
              -- Get the number of parameters.
236
 
              def <- theDef <$> getConstInfo d
237
 
              a'  <- case def of
238
 
                Datatype{dataPars = n} -> do
239
 
                  a <- defType <$> getConstInfo c
240
 
                  return $ piApply a (genericTake n args)
241
 
                Record{recPars = n} -> getRecordConstructorType d (genericTake n args)
242
 
                _                   -> __IMPOSSIBLE__
 
235
              a' <- dataOrRecordType c a
243
236
              unifyArgs a' us vs
244
237
          | otherwise -> constructorMismatch a u v
245
238
        -- Definitions are ok as long as they can't reduce (i.e. datatypes/axioms)
278
271
                  else addEquality a u v
279
272
        _  -> addEquality a u v
280
273
 
 
274
    -- The contexts are transient when unifying, so we should just instantiate to
 
275
    -- constructor heads and generate fresh metas for the arguments. Beware of
 
276
    -- constructors that aren't fully applied.
281
277
    instMeta a m us v = do
282
278
      app <- inertApplication a v
283
279
      reportSDoc "tc.lhs.unify" 50 $
287
283
            ]
288
284
      case app of
289
285
        Nothing -> return False
290
 
        Just (v', b, _) -> do
 
286
        Just (v', b, vs) -> do
291
287
            margs <- do
292
288
              -- The new metas should have the same dependencies as the original meta
293
289
              mi <- getMetaInfo <$> lookupMeta m
 
290
 
 
291
              -- Only generate metas for the arguments v' is actually applied to
 
292
              -- (in case of partial application)
 
293
              let b' = telePi tel (sort Prop)
 
294
                    where
 
295
                      TelV tel0 _ = telView b
 
296
                      tel = telFromList $ take (length vs) $ telToList tel0
294
297
              withMetaInfo mi $ do
295
298
                tel <- getContextTelescope
296
299
                -- important: create the meta in the same environment as the original meta
297
 
                newArgsMetaCtx b tel us
 
300
                newArgsMetaCtx b' tel us
298
301
            noConstraints $ assignV a m us (v' `apply` margs)
299
302
            return True
300
303
          `catchError` \_ -> return False
303
306
    inertApplication a v =
304
307
      case v of
305
308
        Con c vs -> do
306
 
          Def d args <- reduce $ unEl a
307
 
          def <- theDef <$> getConstInfo d
308
 
          b   <- case def of
309
 
            Datatype{dataPars = n} -> do
310
 
              a <- defType <$> getConstInfo c
311
 
              return $ piApply a (genericTake n args)
312
 
            Record{recPars = n} -> getRecordConstructorType d (genericTake n args)
313
 
            _               -> __IMPOSSIBLE__
 
309
          b <- dataOrRecordType c a
314
310
          return $ Just (Con c [], b, vs)
315
311
        Def d vs -> do
316
312
          def <- getConstInfo d
322
318
            _          -> Nothing
323
319
        _        -> return Nothing
324
320
 
 
321
-- | Given the type of a constructor application the corresponding
 
322
-- data or record type, applied to its parameters (extracted from the
 
323
-- given type), is returned.
 
324
--
 
325
-- Precondition: The type has to correspond to an application of the
 
326
-- given constructor.
 
327
 
 
328
dataOrRecordType :: MonadTCM tcm
 
329
                 => QName -- ^ Constructor name.
 
330
                 -> Type -> tcm Type
 
331
dataOrRecordType c a = do
 
332
  -- The telescope ends with a datatype or a record.
 
333
  TelV _ (El _ (Def d args)) <- telView <$> reduce a
 
334
  def <- theDef <$> getConstInfo d
 
335
  (n, a')  <- case def of
 
336
    Datatype{dataPars = n} -> ((,) n) . defType <$> getConstInfo c
 
337
    Record  {recPars  = n} -> ((,) n) <$> getRecordConstructorType d
 
338
    _                      -> __IMPOSSIBLE__
 
339
  return (a' `apply` genericTake n args)