← 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/Polarity.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/Polarity.hs
1
 
{-# LANGUAGE CPP, PatternGuards #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleInstances #-}
 
3
{-# LANGUAGE PatternGuards #-}
 
4
{-# LANGUAGE TypeSynonymInstances #-}
 
5
 
2
6
module Agda.TypeChecking.Polarity where
3
7
 
4
8
import Control.Applicative
5
9
import Control.Monad.State
6
 
import Control.Monad.Error
 
10
 
7
11
import Data.List
 
12
import Data.Maybe
8
13
import Data.Traversable (traverse)
9
14
 
10
15
import Agda.Syntax.Common
11
 
import Agda.Syntax.Internal
 
16
import Agda.Syntax.Internal as I
12
17
 
13
18
import Agda.TypeChecking.Monad
14
19
import Agda.TypeChecking.Pretty
15
 
import Agda.TypeChecking.Positivity
16
20
import Agda.TypeChecking.Substitute
17
21
import Agda.TypeChecking.Telescope
18
22
import Agda.TypeChecking.Reduce
19
23
import Agda.TypeChecking.Free hiding (Occurrence(..))
20
 
import Agda.TypeChecking.Monad.Builtin
21
24
 
22
25
import Agda.Interaction.Options
23
26
 
24
27
import Agda.Utils.List
25
28
import Agda.Utils.Monad
26
29
import Agda.Utils.Permutation
27
 
import Agda.Utils.Impossible
28
30
import Agda.Utils.Size
29
31
 
30
32
#include "../undefined.h"
 
33
import Agda.Utils.Impossible
31
34
 
32
35
------------------------------------------------------------------------
33
36
-- * Polarity lattice.
112
115
 
113
116
  -- refine polarity again by using type information
114
117
  let t = defType def
 
118
  -- Instantiation takes place in Rules.Decl.instantiateDefinitionType
 
119
  -- t <- instantiateFull t -- Andreas, 2014-04-11 Issue 1099: needed for
 
120
  --                        -- variable occurrence test in  dependentPolarity.
115
121
  reportSDoc "tc.polarity.set" 15 $ text "Refining polarity with type " <+> prettyTCM t
116
122
  pol <- enablePhantomTypes (theDef def) <$> dependentPolarity t pol1
117
123
  reportSLn "tc.polarity.set" 10 $ "Polarity of " ++ show x ++ ": " ++ show pol
120
126
  setPolarity x $ pol -- purgeNonvariant pol -- temporarily disable non-variance
121
127
 
122
128
  -- make 'Nonvariant' args 'UnusedArg' in type and clause telescope
123
 
  t <- nonvariantToUnusedArg pol t
 
129
  -- Andreas 2012-11-18: skip this for abstract definitions (fixing issue 755).
 
130
  -- This means that the most precise type for abstract definitions
 
131
  -- is not available, even to other abstract definitions.
 
132
  -- A proper fix would be to introduce a second type for use within abstract.
 
133
  t <- if (defAbstract def == AbstractDef) then return t else
 
134
         nonvariantToUnusedArg pol t
124
135
  modifySignature $ updateDefinition x $
125
136
   updateTheDef (nonvariantToUnusedArgInDef pol) . updateDefType (const t)
126
137
 
169
180
      ps <- dependentPolarity c ps
170
181
      p  <- case b of
171
182
              Abs{} | p /= Invariant  ->
 
183
                -- Andreas, 2014-04-11 see Issue 1099
 
184
                -- Free variable analysis is not in the monad,
 
185
                -- hence metas must have been instantiated before!
172
186
                ifM (relevantInIgnoringNonvariant 0 c ps)
173
187
                  (return Invariant)
174
188
                  (return p)
202
216
  t <- reduce t
203
217
  case ignoreSharingType t of
204
218
    El s (Pi a b) -> do
205
 
      let a' = if p == Nonvariant then mapDomRelevance mkUnused a else a
 
219
      let a' = if p == Nonvariant then mapRelevance mkUnused a else a
206
220
      El s . Pi a' <$> traverse (nonvariantToUnusedArg ps) b
207
221
        -- we do not lift properly but bound variables do not matter for reduce
208
222
        -- also, we do not maintain the context
217
231
  _ -> def
218
232
 
219
233
nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause
220
 
nonvariantToUnusedArgInClause pol cl@Clause{clauseTel = tel, clausePerm = perm, clausePats = ps} =
 
234
nonvariantToUnusedArgInClause pol cl@Clause{clauseTel = tel, clausePerm = perm, namedClausePats = ps} =
221
235
  let adjPat p Nonvariant
222
 
        | properlyMatching (unArg p) = __IMPOSSIBLE__ -- if we match, we cannot be Nonvariant (sanity check)
223
 
        | otherwise                  = mapArgRelevance mkUnused p
 
236
        | properlyMatching (namedArg p) = __IMPOSSIBLE__ -- if we match, we cannot be Nonvariant (sanity check)
 
237
        | otherwise                     = mapRelevance mkUnused p
224
238
      adjPat p _    = p
225
239
      -- change relevance of 'Nonvariant' arguments to 'UnusedArg'
226
240
      -- note that the associated patterns cannot be 'ConP' or 'LitP'
227
 
      ps'           = zipWith adjPat ps (pol ++ repeat Invariant)
 
241
      ps'   = zipWith adjPat ps (pol ++ repeat Invariant)
228
242
      -- get a list of 'Relevance's for the variables bound in the pattern
229
 
      rels0         = argRelevance <$> (patternVars =<< ps')
 
243
      rels0 = getRelevance <$> (concatMap (patternVars . fmap namedThing) ps')
230
244
      -- this is the order the variables appear in the telescope
231
 
      rels          = permute perm rels0
 
245
      rels  = permute perm rels0
232
246
      -- now improve 'Relevance' in 'Telescope' by pattern relevance
233
 
      updateDom UnusedArg = mapDomRelevance mkUnused
 
247
      updateDom UnusedArg = mapRelevance mkUnused
234
248
      updateDom r          = id
235
249
      tel' = telFromList $ zipWith updateDom rels $ telToList tel
236
 
   in cl { clausePats = ps', clauseTel = tel'}
 
250
   in cl { namedClausePats = ps', clauseTel = tel'}
237
251
 
238
252
------------------------------------------------------------------------
239
253
-- * Sized types
251
265
          (parTel, ixTel) = genericSplitAt np $ telToList tel
252
266
      case ixTel of
253
267
        []                 -> exit  -- No size index
254
 
        Dom _ _ (_, a) : _ -> ifM ((/= Just BoundedNo) <$> isSizeType a) exit $ do
 
268
        Dom _ (_, a) : _ -> ifM ((/= Just BoundedNo) <$> isSizeType a) exit $ do
255
269
          -- we assume the size index to be 'Covariant' ...
256
270
          let pol   = genericTake np pol0
257
271
              polCo = pol ++ [Covariant]
271
285
                        -- First constructor argument has type Size
272
286
 
273
287
                        -- check that only positive occurences in tel
274
 
                        isPos <- underAbstraction arg tel $ \tel -> do
275
 
                          pols <- zipWithM polarity [0..] $ map (snd . unDom) $ telToList tel
276
 
                          return $ all (`elem` [Nonvariant, Covariant]) pols
 
288
                        let isPos = underAbstraction arg tel $ \ tel -> do
 
289
                              pols <- zipWithM polarity [0..] $ map (snd . unDom) $ telToList tel
 
290
                              reportSDoc "tc.polarity.size" 25 $
 
291
                                text $ "to pass size polarity check, the following polarities need all to be covariant: " ++ show pols
 
292
                              return $ all (`elem` [Nonvariant, Covariant]) pols
277
293
 
278
294
                        -- check that the size argument appears in the
279
295
                        -- right spot in the target type
280
296
                        let sizeArg = size tel
281
 
                        isLin <- checkSizeIndex np sizeArg target
 
297
                            isLin = addContext conTel $ checkSizeIndex d np sizeArg target
282
298
 
283
 
                        return $ isPos && isLin
 
299
                        ok <- isPos `and2M` isLin
 
300
                        reportSDoc "tc.polarity.size" 15 $
 
301
                          text "constructor" <+> prettyTCM c <+>
 
302
                          text (if ok then "passes" else "fails") <+>
 
303
                          text "size polarity check"
 
304
                        return ok
284
305
 
285
306
          ifM (andM $ map check cons)
286
307
              (return polCo) -- yes, we have a sized type here
287
308
              (return polIn) -- no, does not conform to the rules of sized types
288
309
    _ -> exit
289
310
 
290
 
checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool
291
 
checkSizeIndex np i a =
 
311
-- | @checkSizeIndex d np i a@ checks that constructor target type @a@
 
312
--   has form @d ps (↑ i) idxs@ where @|ps| = np@.
 
313
--
 
314
--   Precondition: @a@ is reduced and of form @d ps idxs0@.
 
315
checkSizeIndex :: QName -> Nat -> Nat -> Type -> TCM Bool
 
316
checkSizeIndex d np i a = do
 
317
  reportSDoc "tc.polarity.size" 15 $ withShowAllArguments $
 
318
    text "checking that constructor target type " <+> prettyTCM a <+>
 
319
    text "is data type " <+> prettyTCM d <+>
 
320
    text "has size index successor of " <+> prettyTCM (var i)
292
321
  case ignoreSharing $ unEl a of
293
 
    Def _ args -> do
294
 
      let excl = not $ freeIn i (pars ++ ixs)
295
 
      s <- sizeView ix
 
322
    Def d0 es -> do
 
323
      unlessM (isJust <$> sameDef d d0) __IMPOSSIBLE__
 
324
      s <- sizeView $ unArg ix
296
325
      case s of
297
 
        SizeSuc v | Var j [] <- ignoreSharing v
298
 
          -> return $ and [ excl, i == j ]
 
326
        SizeSuc v | Var j [] <- ignoreSharing v, i == j
 
327
          -> return $ not $ freeIn i (pars ++ ixs)
299
328
        _ -> return False
300
329
      where
301
 
        (pars, Arg _ _ ix : ixs) = genericSplitAt np args
 
330
        (pars, Apply ix : ixs) = genericSplitAt np es
302
331
    _ -> __IMPOSSIBLE__
303
332
 
304
333
-- | @polarities i a@ computes the list of polarities of de Bruijn index @i@
315
344
    [] -> return Nonvariant
316
345
    ps -> return $ foldr1 (/\) ps
317
346
 
318
 
instance HasPolarity a => HasPolarity (Arg a) where
 
347
instance HasPolarity a => HasPolarity (I.Arg a) where
319
348
  polarities i = polarities i . unArg
320
349
 
321
 
instance HasPolarity a => HasPolarity (Dom a) where
 
350
instance HasPolarity a => HasPolarity (I.Dom a) where
322
351
  polarities i = polarities i . unDom
323
352
 
324
353
instance HasPolarity a => HasPolarity (Abs a) where
334
363
instance HasPolarity Type where
335
364
  polarities i (El _ v) = polarities i v
336
365
 
 
366
instance HasPolarity a => HasPolarity (Elim' a) where
 
367
  polarities i (Proj p)  = return []
 
368
  polarities i (Apply a) = polarities i a
 
369
 
337
370
instance HasPolarity Term where
338
371
  polarities i v = do
339
372
   v <- instantiate v