← 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/Injectivity.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Injectivity.hs
1
 
{-# LANGUAGE CPP #-}
 
1
{-# LANGUAGE CPP           #-}
 
2
{-# LANGUAGE TupleSections #-}
2
3
 
3
4
module Agda.TypeChecking.Injectivity where
4
5
 
5
6
import Prelude hiding (mapM)
 
7
 
6
8
import Control.Applicative
7
 
import Control.Monad.Error hiding (mapM, forM)
8
9
import Control.Monad.State hiding (mapM, forM)
9
10
import Control.Monad.Reader hiding (mapM, forM)
 
11
 
10
12
import Data.Map (Map)
11
13
import qualified Data.Map as Map
12
14
import qualified Data.Set as Set
13
15
import Data.Maybe
14
16
import Data.Traversable hiding (for)
15
17
 
 
18
import qualified Agda.Syntax.Abstract.Name as A
16
19
import Agda.Syntax.Common
17
20
import Agda.Syntax.Internal
 
21
 
18
22
import Agda.TypeChecking.Monad
19
23
import Agda.TypeChecking.Substitute
20
24
import Agda.TypeChecking.Reduce
24
28
import Agda.TypeChecking.Pretty
25
29
import Agda.TypeChecking.Constraints
26
30
import Agda.TypeChecking.Polarity
 
31
 
 
32
import Agda.Utils.Except ( MonadError(catchError, throwError) )
27
33
import Agda.Utils.List
28
 
import Agda.Utils.Functor (for)
 
34
import Agda.Utils.Functor
29
35
import Agda.Utils.Permutation
30
36
 
31
 
#include "../undefined.h"
 
37
#include "undefined.h"
32
38
import Agda.Utils.Impossible
33
39
 
34
40
headSymbol :: Term -> TCM (Maybe TermHead)
68
74
    MetaV{} -> return Nothing
69
75
    DontCare{} -> return Nothing
70
76
    Shared{}   -> __IMPOSSIBLE__
 
77
    ExtLam{}   -> __IMPOSSIBLE__
71
78
 
72
79
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
73
80
checkInjectivity f cs
74
81
  | pointLess cs = do
75
 
      reportSLn "tc.inj.check" 20 $ "Injectivity of " ++ show f ++ " would be pointless."
 
82
      reportSLn "tc.inj.check.pointless" 20 $
 
83
        "Injectivity of " ++ show (A.qnameToConcrete f) ++ " would be pointless."
76
84
      return NotInjective
77
85
  where
78
86
    -- Is it pointless to use injectivity for this function?
87
95
  -- Extract the head symbol of the rhs of each clause (skip absurd clauses)
88
96
  es <- catMaybes <$> do
89
97
    forM cs $ \ c -> do             -- produces a list ...
90
 
      forM (getBody c) $ \ v -> do  -- ... of maybes
91
 
        h <- headSymbol v
92
 
        return (h, c)
 
98
      mapM ((,c) <.> headSymbol) $ getBodyUnraised c -- ... of maybes
93
99
  let (hs, ps) = unzip es
94
100
  reportSLn "tc.inj.check" 40 $ "  right hand sides: " ++ show hs
95
101
  if all isJust hs && distinct hs
121
127
data InvView = Inv QName [Elim] (Map TermHead Clause)
122
128
             | NoInv
123
129
 
 
130
data MaybeAbort = Abort | KeepGoing
 
131
 
124
132
useInjectivity :: Comparison -> Type -> Term -> Term -> TCM ()
125
133
useInjectivity cmp a u v = do
126
134
  reportSDoc "tc.inj.use" 30 $ fsep $
174
182
    invert org f ftype inv args (Just h) = case Map.lookup h inv of
175
183
      Nothing -> typeError $ UnequalTerms cmp u v a
176
184
      Just cl@Clause{ clauseTel  = tel
177
 
                    , clausePerm = perm } -> do
 
185
                    , clausePerm = perm } -> maybeAbort $ do
178
186
          let ps = clausePats cl
179
187
          -- These are what dot patterns should be instantiated at
180
188
          ms <- map unArg <$> newTelMeta tel
185
193
            , text "  ps   =" <+> prettyList (map (text . show) ps)
186
194
            ]
187
195
          -- and this is the order the variables occur in the patterns
188
 
          let ms' = permute (invertP $ compactP perm) ms
 
196
          let ms' = permute (invertP __IMPOSSIBLE__ $ compactP perm) ms
189
197
          let sub = parallelS (reverse ms)
190
198
          margs <- runReaderT (evalStateT (mapM metaElim ps) ms') sub
191
199
          reportSDoc "tc.inj.invert" 20 $ vcat
203
211
          -- The clause might not give as many patterns as there
204
212
          -- are arguments (point-free style definitions).
205
213
          let args' = take (length margs) args
206
 
          compareElims pol ftype org margs args'
 
214
          compareElims pol ftype (Def f []) margs args'
207
215
{- Andreas, 2011-05-09 allow unsolved constraints as long as progress
208
216
          unless (null cs) $ do
209
217
            reportSDoc "tc.inj.invert" 30 $
215
223
          org <- reduce org
216
224
          h <- headSymbol org
217
225
          case h of
218
 
            Just h  -> compareTerm cmp a u v
 
226
            Just h  -> KeepGoing <$ compareTerm cmp a u v
219
227
            Nothing -> do
220
 
             reportSDoc "tc.inj.invert" 30 $ vcat
221
 
               [ text "aborting inversion;" <+> prettyTCM org
222
 
               , text "plainly," <+> text (show org)
223
 
               , text "has TermHead" <+> text (show h)
224
 
               , text "which does not expose a constructor"
225
 
               ]
226
 
             patternViolation
227
 
        `catchError` \err -> case err of
228
 
          TypeError   {} -> throwError err
229
 
          Exception   {} -> throwError err
230
 
          IOException {} -> throwError err
231
 
          PatternErr  {} -> fallBack
232
 
          {- AbortAssign {} -> fallBack -- UNUSED -}
 
228
              reportSDoc "tc.inj.invert" 30 $ vcat
 
229
                [ text "aborting inversion;" <+> prettyTCM org
 
230
                , text "plainly," <+> text (show org)
 
231
                , text "has TermHead" <+> text (show h)
 
232
                , text "which does not expose a constructor"
 
233
                ]
 
234
              return Abort
 
235
 
 
236
    maybeAbort m = do
 
237
      (a, s) <- localTCStateSaving m
 
238
      case a of
 
239
        KeepGoing -> put s
 
240
        Abort     -> fallBack
233
241
 
234
242
    nextMeta = do
235
243
      m : ms <- get