← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Monad/Signature.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/Signature.hs
1
 
{-# LANGUAGE CPP, PatternGuards #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleContexts #-}
 
3
{-# LANGUAGE FlexibleInstances #-}
 
4
{-# LANGUAGE PatternGuards #-}
 
5
 
2
6
module Agda.TypeChecking.Monad.Signature where
3
7
 
4
 
import Control.Arrow ((***))
 
8
import Control.Applicative
5
9
import Control.Monad.State
6
10
import Control.Monad.Reader
7
 
import Data.Set (Set)
8
 
import qualified Data.Set as Set
 
11
 
 
12
import Data.List
9
13
import Data.Map (Map)
10
14
import qualified Data.Map as Map
11
 
import Data.List
12
 
import Data.Function
 
15
import Data.Maybe
13
16
 
14
17
import Agda.Syntax.Abstract.Name
15
18
import Agda.Syntax.Common
16
 
import Agda.Syntax.Internal
 
19
import Agda.Syntax.Internal as I
17
20
import Agda.Syntax.Position
18
21
 
19
22
import qualified Agda.Compiler.JS.Parser as JS
24
27
import Agda.TypeChecking.Monad.Env
25
28
import Agda.TypeChecking.Monad.Mutual
26
29
import Agda.TypeChecking.Monad.Open
27
 
import Agda.TypeChecking.Free (isBinderUsed)
 
30
import Agda.TypeChecking.Monad.State
28
31
import Agda.TypeChecking.Substitute
29
32
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
30
33
import {-# SOURCE #-} Agda.TypeChecking.Polarity
31
34
import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike
32
35
 
 
36
import Agda.Utils.Map as Map
 
37
import Agda.Utils.Maybe
33
38
import Agda.Utils.Monad
34
 
import Agda.Utils.Map as Map
35
39
import Agda.Utils.Size
36
40
import Agda.Utils.Permutation
37
41
import Agda.Utils.Pretty
69
72
 
70
73
-- * modifiers for parts of the signature
71
74
 
 
75
lookupDefinition :: QName -> Signature -> Maybe Definition
 
76
lookupDefinition q sig = HMap.lookup q $ sigDefinitions sig
 
77
 
72
78
updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
73
79
updateDefinition q f sig = sig { sigDefinitions = HMap.adjust f q (sigDefinitions sig) }
74
80
 
87
93
updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
88
94
updateDefCompiledRep f def = def { defCompiledRep = f (defCompiledRep def) }
89
95
 
 
96
updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
 
97
updateFunClauses f def@Function{ funClauses = cs} = def { funClauses = f cs }
 
98
updateFunClauses f _                              = __IMPOSSIBLE__
 
99
 
90
100
-- | Add a constant to the signature. Lifts the definition to top level.
91
101
addConstant :: QName -> Definition -> TCM ()
92
102
addConstant q d = do
93
103
  reportSLn "tc.signature" 20 $ "adding constant " ++ show q ++ " to signature"
94
104
  tel <- getContextTelescope
95
 
  let tel' = killRange $ case theDef d of
96
 
              Constructor{} -> fmap (mapDomHiding (const Hidden)) tel
 
105
  let tel' = replaceEmptyName "r" $ killRange $ case theDef d of
 
106
              Constructor{} -> fmap (setHiding Hidden) tel
97
107
              _             -> tel
98
108
  let d' = abstract tel' $ d { defName = q }
99
109
  reportSLn "tc.signature" 30 $ "lambda-lifted definition = " ++ show d'
111
121
    setT def@Function{} = def { funTerminates = Just b }
112
122
    setT def            = def
113
123
 
 
124
-- | Modify the clauses of a function.
 
125
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
 
126
modifyFunClauses q f =
 
127
  modifySignature $ updateDefinition q $ updateTheDef $ updateFunClauses f
 
128
 
 
129
-- | Lifts clauses to the top-level and adds them to definition.
 
130
addClauses :: QName -> [Clause] -> TCM ()
 
131
addClauses q cls = do
 
132
  tel <- getContextTelescope
 
133
  modifyFunClauses q (++ abstract tel cls)
 
134
 
114
135
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
115
136
addHaskellCode q hsTy hsDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
116
137
  -- TODO: sanity checking
117
138
  where
118
139
    addHs crep = crep { compiledHaskell = Just $ HsDefn hsTy hsDef }
119
140
 
 
141
addHaskellExport :: QName -> HaskellType -> String -> TCM ()
 
142
addHaskellExport q hsTy hsName = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
 
143
  -- TODO: sanity checking
 
144
  where
 
145
    addHs crep = crep { exportHaskell = Just (HsExport hsTy hsName)}
 
146
 
120
147
addHaskellType :: QName -> HaskellType -> TCM ()
121
148
addHaskellType q hsTy = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
122
149
  -- TODO: sanity checking
169
196
-- Add display forms to all names @xn@ such that @x = x1 es1@, ... @xn-1 = xn esn@.
170
197
addDisplayForms :: QName -> TCM ()
171
198
addDisplayForms x = do
 
199
  def  <- getConstInfo x
172
200
  args <- getContextArgs
 
201
{- OLD
173
202
  n    <- do
174
203
    proj <- isProjection x
175
204
    return $ case proj of
176
205
      Just (_, n) -> n
177
206
      Nothing     -> 0
178
 
  add (drop (n - 1) args) x x []
 
207
-}
 
208
  add (drop (projectionArgs $ theDef def) args) x x []
179
209
  where
180
210
    add args top x vs0 = do
181
211
      def <- getConstInfo x
182
212
      let cs = defClauses def
183
213
      case cs of
184
 
        [ Clause{ clausePats = pats, clauseBody = b } ]
185
 
          | all (isVar . unArg) pats
186
 
          , Just (m, Def y vs) <- strip (b `apply` vs0) -> do
187
 
              let ps = raise 1 (map unArg vs)
188
 
                  df = Display 0 ps $ DTerm $ Def top args
 
214
        [ Clause{ namedClausePats = pats, clauseBody = b } ]
 
215
          | all (isVar . namedArg) pats
 
216
          , Just (m, Def y es) <- strip (b `apply` vs0)
 
217
          , Just vs <- mapM isApplyElim es -> do
 
218
              let ps = raise 1 $ map unArg vs
 
219
                  df = Display 0 ps $ DTerm $ Def top $ map Apply args
189
220
              reportSLn "tc.display.section" 20 $ "adding display form " ++ show y ++ " --> " ++ show top
190
221
                                                ++ "\n  " ++ show df
191
222
              addDisplayForm y df
196
227
                    _:_:_ -> "many clauses"
197
228
                    [ Clause{ clauseBody = b } ] -> case strip b of
198
229
                      Nothing -> "bad body"
199
 
                      Just (m, Def y vs)
 
230
                      Just (m, Def y es)
200
231
                        | m < length args -> "too few args"
201
232
                        | m > length args -> "too many args"
202
 
                        | otherwise       -> "args=" ++ show args ++ " vs=" ++ show vs
 
233
                        | otherwise       -> "args=" ++ show args ++ " es=" ++ show es
203
234
                      Just (m, v) -> "not a def body"
204
235
              reportSLn "tc.display.section" 30 $ "no display form from " ++ show x ++ " because " ++ reason
205
236
              return ()
206
 
    strip (Body v)   = return (0, v)
 
237
    strip (Body v)   = return (0, unSpine v)
207
238
    strip  NoBody    = Nothing
208
239
    strip (Bind b)   = do
209
240
      (n, v) <- strip $ absBody b
212
243
    isVar VarP{} = True
213
244
    isVar _      = False
214
245
 
215
 
applySection ::
216
 
  ModuleName -> Telescope -> ModuleName -> Args ->
217
 
  Map QName QName -> Map ModuleName ModuleName -> TCM ()
 
246
-- | Module application (followed by module parameter abstraction).
 
247
applySection
 
248
  :: ModuleName                -- ^ Name of new module defined by the module macro.
 
249
  -> Telescope                 -- ^ Parameters of new module.
 
250
  -> ModuleName                -- ^ Name of old module applied to arguments.
 
251
  -> Args                      -- ^ Arguments of module application.
 
252
  -> Map QName QName           -- ^ Imported names (given as renaming).
 
253
  -> Map ModuleName ModuleName -- ^ Imported modules (given as renaming).
 
254
  -> TCM ()
218
255
applySection new ptel old ts rd rm = do
219
256
  sig  <- getSignature
220
257
  isig <- getImportedSignature
244
281
    partOfOldM x = x `isSubModuleOf` old
245
282
    partOfOldD x = x `isInModule`    old
246
283
 
247
 
    copyName x = maybe x id $ Map.lookup x rd
 
284
    -- Andreas, 2013-10-29
 
285
    -- Here, if the name x is not imported, it persists as
 
286
    -- old, possibly out-of-scope name.
 
287
    -- This old name may used by the case split tactic, leading to
 
288
    -- names that cannot be printed properly.
 
289
    -- I guess it would make sense to mark non-imported names
 
290
    -- as such (out-of-scope) and let splitting fail if it would
 
291
    -- produce out-of-scope constructors.
 
292
    copyName x = Map.findWithDefault x x rd
248
293
 
249
294
    copyDef :: Args -> (QName, Definition) -> TCM ()
250
 
    copyDef ts (x, d) = case Map.lookup x rd of
 
295
    copyDef ts (x, d) =
 
296
      case Map.lookup x rd of
251
297
        Nothing -> return ()  -- if it's not in the renaming it was private and
252
298
                              -- we won't need it
253
299
        Just y  -> do
265
311
        pol = defPolarity d `apply` ts
266
312
        occ = defArgOccurrences d `apply` ts
267
313
        -- the name is set by the addConstant function
268
 
        nd y = Defn (defRelevance d) y t pol occ [] (-1) noCompiledRep <$> def  -- TODO: mutual block?
 
314
        nd y = Defn (defArgInfo d) y t pol occ [] (-1) noCompiledRep <$> def  -- TODO: mutual block?
269
315
        oldDef = theDef d
270
 
        isCon = case oldDef of
271
 
          Constructor{} -> True
272
 
          _             -> False
273
 
{- OLD
274
 
        getOcc d = case d of
275
 
          Function { funArgOccurrences  = os } -> os
276
 
          Datatype { dataArgOccurrences = os } -> os
277
 
          Record   { recArgOccurrences  = os } -> os
278
 
          _ -> []
279
 
        oldOcc = getOcc oldDef
 
316
        isCon  = case oldDef of { Constructor{} -> True ; _ -> False }
 
317
        mutual = case oldDef of { Function{funMutual = m} -> m              ; _ -> [] }
 
318
        extlam = case oldDef of { Function{funExtLam = e} -> e              ; _ -> Nothing }
 
319
        with   = case oldDef of { Function{funWith = w}   -> copyName <$> w ; _ -> Nothing }
 
320
{- THIS BREAKS A LOT OF THINGS:
 
321
        -- Andreas, 2013-10-21:
 
322
        -- Even if we apply the record argument, we stay a projection.
 
323
        -- This is because we may abstract the record argument later again.
 
324
        -- See succeed/ProjectionNotNormalized.agda
 
325
        proj   = case oldDef of
 
326
          Function{funProjection = Just p@Projection{projIndex = n}}
 
327
            -> Just $ p { projIndex    = n - size ts
 
328
                        , projDropPars = projDropPars p `apply` ts
 
329
                        }
 
330
          _ -> Nothing
280
331
-}
 
332
        -- NB (Andreas, 2013-10-19):
 
333
        -- If we apply the record argument, we are no longer a projection!
 
334
        proj   = case oldDef of
 
335
          Function{funProjection = Just p@Projection{projIndex = n}} | size ts < n
 
336
            -> Just $ p { projIndex    = n - size ts
 
337
                        , projDropPars = projDropPars p `apply` ts
 
338
                        }
 
339
          _ -> Nothing
 
340
 
281
341
        def  = case oldDef of
282
342
                Constructor{ conPars = np, conData = d } -> return $
283
 
                  oldDef { conPars = np - size ts, conData = copyName d }
 
343
                  oldDef { conPars = np - size ts
 
344
                         , conData = copyName d
 
345
                         }
284
346
                Datatype{ dataPars = np, dataCons = cs } -> return $
285
 
                  oldDef { dataPars = np - size ts, dataClause = Just cl, dataCons = map copyName cs
286
 
                         {- , dataArgOccurrences = drop (length ts) oldOcc -} }
 
347
                  oldDef { dataPars   = np - size ts
 
348
                         , dataClause = Just cl
 
349
                         , dataCons   = map copyName cs
 
350
                         }
287
351
                Record{ recPars = np, recConType = t, recTel = tel } -> return $
288
 
                  oldDef { recPars = np - size ts, recClause = Just cl
289
 
                         , recConType = apply t ts, recTel = apply tel ts
290
 
                         {- , recArgOccurrences = drop (length ts) oldOcc -}
 
352
                  oldDef { recPars    = np - size ts
 
353
                         , recClause  = Just cl
 
354
                         , recConType = apply t ts
 
355
                         , recTel     = apply tel ts
291
356
                         }
292
357
                _ -> do
293
358
                  cc <- compileClauses Nothing [cl] -- Andreas, 2012-10-07 non need for record pattern translation
294
359
                  let newDef = Function
295
360
                        { funClauses        = [cl]
296
 
                        , funCompiled       = cc
 
361
                        , funCompiled       = Just $ cc
297
362
                        , funDelayed        = NotDelayed
298
363
                        , funInv            = NotInjective
299
 
{-
300
 
                        , funPolarity       = []
301
 
                        , funArgOccurrences = drop (length ts') oldOcc
302
 
-}
303
364
                        , funMutual         = mutual
304
365
                        , funAbstr          = ConcreteDef
305
366
                        , funProjection     = proj
306
367
                        , funStatic         = False
307
368
                        , funCopy           = True
308
369
                        , funTerminates     = Just True
 
370
                        , funExtLam         = extlam
 
371
                        , funWith           = with
309
372
                        }
310
373
                  reportSLn "tc.mod.apply" 80 $ "new def for " ++ show x ++ "\n  " ++ show newDef
311
374
                  return newDef
312
 
                  where
313
 
                    mutual = case oldDef of
314
 
                      Function{funMutual = m} -> m
315
 
                      _ -> []
316
 
                    proj = case oldDef of
317
 
                      Function{funProjection = Just (r, n)}
318
 
                        | size ts < n -> Just (r, n - size ts)
319
 
                      _ -> Nothing
 
375
{-
320
376
        ts' | null ts   = []
321
377
            | otherwise = case oldDef of
322
 
                Function{funProjection = Just (_, n)}
 
378
                Function{funProjection = Just Projection{ projIndex = n}}
323
379
                  | n == 0       -> __IMPOSSIBLE__
324
380
                  | otherwise    -> drop (n - 1) ts
325
381
                _ -> ts
326
 
        cl = Clause { clauseRange = getRange $ defClauses d
327
 
                    , clauseTel   = EmptyTel
328
 
                    , clausePerm  = idP 0
329
 
                    , clausePats  = []
330
 
                    , clauseBody  = Body $ Def x ts'
 
382
-}
 
383
        head = case oldDef of
 
384
                 Function{funProjection = Just Projection{ projDropPars = f}}
 
385
                   -> f
 
386
                 _ -> Def x []
 
387
        cl = Clause { clauseRange     = getRange $ defClauses d
 
388
                    , clauseTel       = EmptyTel
 
389
                    , clausePerm      = idP 0
 
390
                    , namedClausePats = []
 
391
                    , clauseBody      = Body $ head `apply` ts
 
392
                    , clauseType      = Just $ defaultArg t
331
393
                    }
332
394
 
333
395
    copySec :: Args -> (ModuleName, Section) -> TCM ()
354
416
canonicalName x = do
355
417
  def <- theDef <$> getConstInfo x
356
418
  case def of
357
 
    Constructor{conSrcCon = c}                                -> return c
 
419
    Constructor{conSrcCon = c}                                -> return $ conName c
358
420
    Record{recClause = Just (Clause{ clauseBody = body })}    -> canonicalName $ extract body
359
421
    Datatype{dataClause = Just (Clause{ clauseBody = body })} -> canonicalName $ extract body
360
422
    _                                                         -> return x
365
427
    extract (Body _)         = __IMPOSSIBLE__
366
428
    extract (Bind b)         = extract (unAbs b)
367
429
 
 
430
sameDef :: QName -> QName -> TCM (Maybe QName)
 
431
sameDef d1 d2 = do
 
432
  c1 <- canonicalName d1
 
433
  c2 <- canonicalName d2
 
434
  if (c1 == c2) then return $ Just c1 else return Nothing
 
435
 
368
436
-- | Can be called on either a (co)datatype, a record type or a
369
437
--   (co)constructor.
370
438
whatInduction :: QName -> TCM Induction
393
461
        _                          -> __IMPOSSIBLE__
394
462
    _ -> __IMPOSSIBLE__
395
463
 
396
 
{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}
397
 
getConstInfo :: MonadTCM tcm => QName -> tcm Definition
398
 
getConstInfo q = liftTCM $ join $ pureTCM $ \st env ->
399
 
  let defs  = sigDefinitions $ stSignature st
400
 
      idefs = sigDefinitions $ stImports st
401
 
      smash = (++) `on` maybe [] (:[])
402
 
  in case smash (HMap.lookup q defs) (HMap.lookup q idefs) of
403
 
      []  -> fail $ "Unbound name: " ++ show q ++ " " ++ showQNameId q
404
 
      [d] -> mkAbs env d
405
 
      ds  -> fail $ "Ambiguous name: " ++ show q
406
 
  where
407
 
    mkAbs env d
408
 
      | treatAbstractly' q' env =
409
 
        case makeAbstract d of
410
 
          Just d        -> return d
411
 
          Nothing       -> typeError $ NotInScope [qnameToConcrete q]
412
 
            -- the above can happen since the scope checker is a bit sloppy with 'abstract'
413
 
      | otherwise = return d
414
 
      where
415
 
        q' = case theDef d of
416
 
          -- Hack to make abstract constructors work properly. The constructors
417
 
          -- live in a module with the same name as the datatype, but for 'abstract'
418
 
          -- purposes they're considered to be in the same module as the datatype.
419
 
          Constructor{} -> dropLastModule q
420
 
          _             -> q
421
 
 
422
 
        dropLastModule q@QName{ qnameModule = m } =
423
 
          q{ qnameModule = mnameFromList $ init' $ mnameToList m }
424
 
 
425
 
        init' [] = {-'-} __IMPOSSIBLE__
426
 
        init' xs = init xs
 
464
class (Functor m, Applicative m, Monad m) => HasConstInfo m where
 
465
  -- | Lookup the definition of a name. The result is a closed thing, all free
 
466
  --   variables have been abstracted over.
 
467
  getConstInfo :: QName -> m Definition
 
468
 
 
469
{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}
 
470
 
 
471
instance HasConstInfo (TCMT IO) where
 
472
  getConstInfo q = join $ pureTCM $ \st env ->
 
473
    let defs  = sigDefinitions $ stSignature st
 
474
        idefs = sigDefinitions $ stImports st
 
475
    in case catMaybes [HMap.lookup q defs, HMap.lookup q idefs] of
 
476
        []  -> fail $ "Unbound name: " ++ show q ++ " " ++ showQNameId q
 
477
        [d] -> mkAbs env d
 
478
        ds  -> fail $ "Ambiguous name: " ++ show q
 
479
    where
 
480
      mkAbs env d
 
481
        | treatAbstractly' q' env =
 
482
          case makeAbstract d of
 
483
            Just d      -> return d
 
484
            Nothing     -> notInScope $ qnameToConcrete q
 
485
              -- the above can happen since the scope checker is a bit sloppy with 'abstract'
 
486
        | otherwise = return d
 
487
        where
 
488
          q' = case theDef d of
 
489
            -- Hack to make abstract constructors work properly. The constructors
 
490
            -- live in a module with the same name as the datatype, but for 'abstract'
 
491
            -- purposes they're considered to be in the same module as the datatype.
 
492
            Constructor{} -> dropLastModule q
 
493
            _             -> q
 
494
 
 
495
          dropLastModule q@QName{ qnameModule = m } =
 
496
            q{ qnameModule = mnameFromList $ init' $ mnameToList m }
 
497
 
 
498
          init' [] = {-'-} __IMPOSSIBLE__
 
499
          init' xs = init xs
 
500
 
 
501
{-# INLINE getConInfo #-}
 
502
{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}
 
503
getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
 
504
getConInfo = liftTCM . getConstInfo . conName
427
505
 
428
506
-- | Look up the polarity of a definition.
429
507
getPolarity :: QName -> TCM [Polarity]
430
508
getPolarity q = defPolarity <$> getConstInfo q
431
509
 
432
 
{- OLD
433
 
getPolarity :: QName -> TCM [Polarity]
434
 
getPolarity q = do
435
 
  defn <- theDef <$> getConstInfo q
436
 
  case defn of
437
 
    Function{ funPolarity  = p } -> return p
438
 
    Datatype{ dataPolarity = p } -> return p
439
 
    Record{ recPolarity    = p } -> return p
440
 
    _                            -> return []
441
 
-}
442
 
 
443
510
-- | Look up polarity of a definition and compose with polarity
444
511
--   represented by 'Comparison'.
445
512
getPolarity' :: Comparison -> QName -> TCM [Polarity]
453
517
setPolarity :: QName -> [Polarity] -> TCM ()
454
518
setPolarity q pol = modifySignature $ updateDefinition q $ updateDefPolarity $ const pol
455
519
 
456
 
{- OLD
457
 
setPolarity :: QName -> [Polarity] -> TCM ()
458
 
setPolarity q pol = do
459
 
  modifySignature setP
460
 
  where
461
 
    setP sig = sig { sigDefinitions = HMap.adjust setPx q defs }
462
 
      where
463
 
        setPx def = def { theDef = setPd $ theDef def }
464
 
        setPd d   = case d of
465
 
          Function{} -> d { funPolarity  = pol }
466
 
          Datatype{} -> d { dataPolarity = pol }
467
 
          Record{}   -> d { recPolarity  = pol }
468
 
          _          -> d
469
 
        defs      = sigDefinitions sig
470
 
-}
471
 
 
472
520
-- | Return a finite list of argument occurrences.
473
521
getArgOccurrences :: QName -> TCM [Occurrence]
474
522
getArgOccurrences d = defArgOccurrences <$> getConstInfo d
513
560
    _                                    -> Mixed
514
561
  where
515
562
    look i os = (os ++ repeat Mixed) !! fromIntegral i
516
 
 
517
 
setArgOccurrences :: QName -> [Occurrence] -> TCM ()
518
 
setArgOccurrences d os =
519
 
  modifySignature setO
520
 
  where
521
 
    setO sig = sig { sigDefinitions = HMap.adjust setOx d defs }
522
 
      where
523
 
        setOx def = def { theDef = setOd $ theDef def }
524
 
        setOd d   = case d of
525
 
          Function{} -> d { funArgOccurrences  = os }
526
 
          Datatype{} -> d { dataArgOccurrences = os }
527
 
          Record{}   -> d { recArgOccurrences  = os }
528
 
          _          -> d
529
 
        defs      = sigDefinitions sig
530
563
-}
531
564
 
532
565
-- | Get the mutually recursive identifiers.
560
593
  isig <- sigSections <$> getImportedSignature
561
594
  top <- currentModule
562
595
  case top `isSubModuleOf` m || top == m of
563
 
    True  -> return $ maybe 0 secFreeVars $ Map.lookup m (Map.union sig isig)
 
596
    True  -> return $ maybe 0 secFreeVars $
 
597
               Map.lookup m sig <|> Map.lookup m isig
564
598
    False -> return 0
565
599
 
566
600
-- | Compute the number of free variables of a module. This is the sum of
587
621
  verboseS "tc.sig.inst" 30 $ do
588
622
    ctx <- getContext
589
623
    m   <- currentModule
590
 
    reportSLn "" 0 $ "instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++
591
 
                        unwords (map show . take (size vs) . reverse . map (fst . unDom) $ ctx)
 
624
    reportSLn "tc.sig.inst" 30 $
 
625
      "instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++
 
626
      unwords (map show . take (size vs) . reverse . map (fst . unDom) $ ctx)
592
627
  return $ d `apply` vs
593
628
 
594
629
-- | Give the abstract view of a definition.
595
630
makeAbstract :: Definition -> Maybe Definition
596
 
makeAbstract d = do def <- makeAbs $ theDef d
597
 
                    return d { theDef = def }
598
 
    where
599
 
        makeAbs Datatype   {dataAbstr = AbstractDef} = Just Axiom
600
 
        makeAbs Function   {funAbstr  = AbstractDef} = Just Axiom
601
 
        makeAbs Constructor{conAbstr  = AbstractDef} = Nothing
602
 
        makeAbs d                                    = Just d
 
631
makeAbstract d =
 
632
  case defAbstract d of
 
633
    ConcreteDef -> return d
 
634
    AbstractDef -> do
 
635
      def <- makeAbs $ theDef d
 
636
      return d { defArgOccurrences = [] -- no positivity info for abstract things!
 
637
               , defPolarity       = [] -- no polarity info for abstract things!
 
638
               , theDef = def
 
639
               }
 
640
  where
 
641
    makeAbs Datatype   {} = Just Axiom
 
642
    makeAbs Function   {} = Just Axiom
 
643
    makeAbs Constructor{} = Nothing
 
644
    -- Andreas, 2012-11-18:  Make record constructor and projections abstract.
 
645
    makeAbs d@Record{}    = Just Axiom
 
646
    -- Q: what about primitive?
 
647
    makeAbs d             = Just d
603
648
 
604
649
-- | Enter abstract mode. Abstract definition in the current module are transparent.
605
650
inAbstractMode :: TCM a -> TCM a
613
658
inConcreteMode = local $ \e -> e { envAbstractMode = ConcreteMode }
614
659
 
615
660
-- | Ignore abstract mode. All abstract definitions are transparent.
616
 
ignoreAbstractMode :: TCM a -> TCM a
 
661
ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
617
662
ignoreAbstractMode = local $ \e -> e { envAbstractMode = IgnoreAbstractMode,
618
663
                                       envAllowDestructiveUpdate = False }
619
664
                                       -- Allowing destructive updates when ignoring
622
667
-- | Check whether a name might have to be treated abstractly (either if we're
623
668
--   'inAbstractMode' or it's not a local name). Returns true for things not
624
669
--   declared abstract as well, but for those 'makeAbstract' will have no effect.
625
 
treatAbstractly :: QName -> TCM Bool
626
 
treatAbstractly q = treatAbstractly' q <$> ask
 
670
treatAbstractly :: MonadReader TCEnv m => QName -> m Bool
 
671
treatAbstractly q = asks $ treatAbstractly' q
627
672
 
628
673
treatAbstractly' :: QName -> TCEnv -> Bool
629
674
treatAbstractly' q env = case envAbstractMode env of
634
679
    current = envCurrentModule env
635
680
    m       = qnameModule q
636
681
 
 
682
-- | Get type of a constant, instantiated to the current context.
637
683
typeOfConst :: QName -> TCM Type
638
684
typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q)
639
685
 
 
686
-- | Get relevance of a constant.
640
687
relOfConst :: QName -> TCM Relevance
641
688
relOfConst q = defRelevance <$> getConstInfo q
642
689
 
 
690
-- | Get colors of a constant.
 
691
colOfConst :: QName -> TCM [Color]
 
692
colOfConst q = defColors <$> getConstInfo q
 
693
 
643
694
-- | The name must be a datatype.
644
695
sortOfConst :: QName -> TCM Sort
645
696
sortOfConst q =
651
700
            _                      -> fail $ "Expected " ++ show q ++ " to be a datatype."
652
701
 
653
702
-- | Is it the name of a record projection?
654
 
isProjection :: QName -> TCM (Maybe (QName, Int))
655
 
isProjection qn = do
656
 
  def <- theDef <$> getConstInfo qn
 
703
isProjection :: QName -> TCM (Maybe Projection)
 
704
isProjection qn = isProjection_ . theDef <$> getConstInfo qn
 
705
 
 
706
isProjection_ :: Defn -> Maybe Projection
 
707
isProjection_ def =
657
708
  case def of
658
 
    Function { funProjection = result } -> return $ result
659
 
    _                                   -> return $ Nothing
 
709
    Function { funProjection = result } -> result
 
710
    _                                   -> Nothing
 
711
 
 
712
isProperProjection :: Defn -> Bool
 
713
isProperProjection = isJust . (projProper <=< isProjection_)
 
714
-- isProperProjection = maybe False projProper . isProjection_
 
715
 
 
716
-- | Number of dropped initial arguments.
 
717
projectionArgs :: Defn -> Int
 
718
projectionArgs = maybe 0 (pred . projIndex) . isProjection_
 
719
 
 
720
-- | Apply a function @f@ to its first argument, producing the proper
 
721
--   postfix projection if @f@ is a projection.
 
722
applyDef :: QName -> I.Arg Term -> TCM Term
 
723
applyDef f a = do
 
724
  -- get the original projection, if existing
 
725
  res <- (projProper =<<) <$> isProjection f
 
726
  case res of
 
727
    Nothing -> return $ Def f [Apply a]
 
728
    Just f' -> return $ unArg a `applyE` [Proj f']
 
729
 
 
730
-- | @getDefType f t@ computes the type of (possibly projection-(like))
 
731
--   function @t@ whose first argument has type @t@.
 
732
--   The `parameters' for @f@ are extracted from @t@.
 
733
--   @Nothing@ if @f@ is projection(like) but
 
734
--   @t@ is not a data/record/axiom type.
 
735
--
 
736
--   Precondition: @t@ is reduced.
 
737
--
 
738
--   See also: 'Agda.TypeChecking.Datatypes.getConType'
 
739
getDefType :: QName -> Type -> TCM (Maybe Type)
 
740
getDefType f t = do
 
741
  def <- getConstInfo f
 
742
  let a = defType def
 
743
  -- if @f@ is not a projection (like) function, @a@ is the correct type
 
744
  caseMaybe (isProjection_ $ theDef def) (return $ Just a) $
 
745
    \ (Projection{ projIndex = n }) -> do
 
746
      -- otherwise, we have to instantiate @a@ to the "parameters" of @f@
 
747
      let npars | n == 0    = __IMPOSSIBLE__
 
748
                | otherwise = n - 1
 
749
      -- we get the parameters from type @t@
 
750
      case ignoreSharing $ unEl t of
 
751
        Def d es -> do
 
752
          -- Andreas, 2013-10-22
 
753
          -- we need to check this @Def@ is fully reduced.
 
754
          -- If it is stuck due to disabled reductions
 
755
          -- (because of failed termination check),
 
756
          -- we will produce garbage parameters.
 
757
          flip (ifM $ eligibleForProjectionLike d) (return Nothing) $ do
 
758
            -- now we know it is reduced, we can safely take the parameters
 
759
            let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take npars es
 
760
            -- pars <- maybe (return Nothing) return $ allApplyElims $ take npars es
 
761
            return $ Just $ a `apply` pars
 
762
        _ -> return Nothing