← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Rules/LHS/Split.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Rules/LHS/Split.hs
4
4
 
5
5
import Control.Applicative
6
6
import Control.Monad.Error
7
 
import Data.Monoid
 
7
import Data.Monoid (mempty, mappend)
8
8
import Data.List
9
9
import Data.Traversable hiding (mapM, sequence)
10
10
 
25
25
import Agda.TypeChecking.Constraints
26
26
import Agda.TypeChecking.Conversion
27
27
import Agda.TypeChecking.Rules.LHS.Problem
28
 
import Agda.TypeChecking.Rules.Term
 
28
import Agda.TypeChecking.Rules.LHS.ProblemRest
 
29
-- import Agda.TypeChecking.Rules.Term
29
30
import Agda.TypeChecking.Monad.Builtin
30
31
import Agda.TypeChecking.Free
31
32
import Agda.TypeChecking.Irrelevance
56
57
                        ++ "the literal to the corresponding constructor pattern, so "
57
58
                        ++ "you probably don't want to do it this way."
58
59
        | otherwise -> do
59
 
          Con z _ <- primZero
60
 
          Con s _ <- primSuc
 
60
          Con z _ <- ignoreSharing <$> primZero
 
61
          Con s _ <- ignoreSharing <$> primSuc
61
62
          let zero  = A.ConP info (A.AmbQ [setRange r z]) []
62
 
              suc p = A.ConP info (A.AmbQ [setRange r s]) [defaultArg $ unnamed p]
 
63
              suc p = A.ConP info (A.AmbQ [setRange r s]) [defaultNamedArg p]
63
64
              info  = A.PatRange r
64
65
              p'    = foldr ($) zero $ genericReplicate n suc
65
66
          return $ foldr (A.AsP info) p' xs
68
69
-- | Split a problem at the first constructor of datatype type. Implicit
69
70
--   patterns should have been inserted.
70
71
splitProblem :: Problem -> TCM (Either SplitError SplitProblem)
71
 
splitProblem (Problem ps (perm, qs) tel) = do
 
72
splitProblem (Problem ps (perm, qs) tel pr) = do
72
73
    reportS "tc.lhs.split" 20 $ "initiating splitting\n"
73
74
    runErrorT $
74
75
      splitP ps (permute perm $ zip [0..] $ allHoles qs) tel
81
82
    splitP (p : ps) ((i, q) : qs) tel0@(ExtendTel a tel) = do
82
83
      let tryAgain = splitP (p : ps) ((i, q) : qs) tel0
83
84
      p <- lift $ expandLitPattern p
84
 
      case asView $ namedThing $ unArg p of
 
85
      case asView $ namedArg p of
85
86
 
86
87
        -- Case: literal pattern
87
88
        (xs, p@(A.LitP lit))  -> do
90
91
          -- not indexed.
91
92
 
92
93
          -- Andreas, 2010-09-07 cannot split on irrelevant args
93
 
          when (unusableRelevance $ argRelevance a) $
 
94
          when (unusableRelevance $ domRelevance a) $
94
95
            typeError $ SplitOnIrrelevant p a
95
96
          b <- lift $ litType lit
96
97
          ok <- lift $ do
97
 
              noConstraints (equalType (unArg a) b)
 
98
              noConstraints (equalType (unDom a) b)
98
99
              return True
99
100
            `catchError` \_ -> return False
100
101
          if ok
101
102
            then return $
102
103
              Split mempty
103
104
                    xs
104
 
                    (fmap (LitFocus lit q i) a)
105
 
                    (fmap (Problem ps ()) tel)
 
105
                    (argFromDom $ fmap (LitFocus lit q i) a)
 
106
                    (fmap (\ tel -> Problem ps () tel __IMPOSSIBLE__) tel)
106
107
            else keepGoing
107
108
 
108
109
        -- Case: constructor pattern
109
110
        (xs, p@(A.ConP _ (A.AmbQ cs) args)) -> do
110
 
          a' <- liftTCM $ reduce $ unArg a
111
 
          case unEl a' of
112
 
 
113
 
            -- Type is a meta and constructor is unambiguous,
114
 
            -- in this case try to instantiate the meta.
115
 
            MetaV{} | [c] <- cs -> do
116
 
              ok <- lift $ do
117
 
                Constructor{ conData = d } <- theDef <$> getConstInfo c
118
 
                dt            <- defType <$> getConstInfo d
119
 
                vs            <- newArgsMeta dt
120
 
                El _ (Sort s) <- reduce $ apply dt vs
121
 
                (True <$ noConstraints (equalType a' (El s $ Def d vs)))
122
 
                  `catchError` \_ -> return False
123
 
              if not ok then keepGoing else
124
 
                tryAgain
 
111
          let tryInstantiate a'
 
112
                | [c] <- cs = do
 
113
                    -- Type is blocked by a meta and constructor is unambiguous,
 
114
                    -- in this case try to instantiate the meta.
 
115
                  ok <- lift $ do
 
116
                    Constructor{ conData = d } <- theDef <$> getConstInfo c
 
117
                    dt     <- defType <$> getConstInfo d
 
118
                    vs     <- newArgsMeta dt
 
119
                    Sort s <- ignoreSharing . unEl <$> reduce (apply dt vs)
 
120
                    (True <$ noConstraints (equalType a' (El s $ Def d vs)))
 
121
                      `catchError` \_ -> return False
 
122
                  if ok then tryAgain else keepGoing
 
123
                | otherwise = keepGoing
 
124
          ifBlockedType (unDom a) (const tryInstantiate) $ \ a' -> do
 
125
          case ignoreSharing $ unEl a' of
125
126
 
126
127
            -- Subcase: split type is a Def
127
128
            Def d vs    -> do
128
129
              def <- liftTCM $ theDef <$> getConstInfo d
129
130
              unless (defIsRecord def) $
130
131
                -- cannot split on irrelevant or non-strict things
131
 
                when (unusableRelevance $ argRelevance a) $ do
 
132
                when (unusableRelevance $ domRelevance a) $ do
132
133
                  -- Andreas, 2011-10-04 unless allowed by option
133
134
                  allowed <- liftTCM $ optExperimentalIrrelevance <$> pragmaOptions
134
135
                  unless allowed $ typeError $ SplitOnIrrelevant p a
140
141
              case mp of
141
142
                Nothing -> keepGoing
142
143
                Just np ->
143
 
                  liftTCM $ traceCall (CheckPattern p EmptyTel (unArg a)) $ do  -- TODO: wrong telescope
 
144
                  liftTCM $ traceCall (CheckPattern p EmptyTel (unDom a)) $ do  -- TODO: wrong telescope
144
145
                  -- Check that we construct something in the right datatype
145
146
                  c <- do
146
147
                      cs' <- mapM canonicalName cs
168
169
                         ]
169
170
 
170
171
                  whenM (optWithoutK <$> pragmaOptions) $
171
 
                    wellFormedIndices pars ixs
 
172
                    wellFormedIndices a'
172
173
 
173
174
                  return $ Split mempty
174
175
                                 xs
175
 
                                 (fmap (Focus c args (getRange p) q i d pars ixs) a)
176
 
                                 (fmap (Problem ps ()) tel)
 
176
                                 (argFromDom $ fmap (Focus c args (getRange p) q i d pars ixs) a)
 
177
                                 (fmap (\ tel -> Problem ps () tel __IMPOSSIBLE__) tel)
177
178
            -- Subcase: split type is not a Def
178
179
            _   -> keepGoing
179
180
        -- Case: neither literal nor constructor pattern
180
181
        p -> keepGoing
181
182
      where
182
183
        keepGoing = do
183
 
          let p0 = Problem [p] () (ExtendTel a $ fmap (const EmptyTel) tel)
 
184
          let p0 = Problem [p] () (ExtendTel a $ fmap (const EmptyTel) tel) mempty
184
185
          Split p1 xs foc p2 <- underAbstraction a tel $ \tel -> splitP ps qs tel
185
186
          return $ Split (mappend p0 p1) xs foc p2
186
187
 
187
 
 
188
 
wellFormedIndices
189
 
  :: [Arg Term] -- ^ Parameters.
190
 
  -> [Arg Term] -- ^ Indices.
191
 
  -> TCM ()
192
 
wellFormedIndices pars ixs = do
193
 
  pars <- normalise pars
194
 
  ixs  <- normalise ixs
195
 
  vs   <- case constructorApplications ixs of
196
 
            Nothing -> typeError $ IndicesNotConstructorApplications ixs
197
 
            Just vs -> return vs
 
188
-- | Takes a type, which must be a data or record type application,
 
189
-- and checks that the indices are constructors (or literals) applied
 
190
-- to distinct variables which do not occur free in the parameters.
 
191
-- For the purposes of this check parameters count as constructor
 
192
-- arguments; parameters are reconstructed from the given type.
 
193
--
 
194
-- Precondition: The type must be a data or record type application.
 
195
 
 
196
wellFormedIndices :: Type -> TCM ()
 
197
wellFormedIndices t = do
 
198
  t <- reduce t
 
199
 
 
200
  reportSDoc "tc.lhs.split.well-formed" 10 $
 
201
    fsep [ text "Checking if indices are well-formed:"
 
202
         , nest 2 $ prettyTCM t
 
203
         ]
 
204
 
 
205
  (pars, ixs) <- normalise =<< case ignoreSharing $ unEl t of
 
206
    Def d args -> do
 
207
      def       <- getConstInfo d
 
208
      typedArgs <- args `withTypesFrom` defType def
 
209
 
 
210
      let noPars = case theDef def of
 
211
            Datatype { dataPars = n } -> n
 
212
            Record   { recPars  = n } -> n
 
213
            _                         -> __IMPOSSIBLE__
 
214
          (pars, ixs) = genericSplitAt noPars typedArgs
 
215
      return (map fst pars, ixs)
 
216
 
 
217
    _ -> __IMPOSSIBLE__
 
218
 
 
219
  mvs <- constructorApplications ixs
 
220
  vs  <- case mvs of
 
221
           Nothing -> typeError $
 
222
                        IndicesNotConstructorApplications (map fst ixs)
 
223
           Just vs -> return vs
 
224
 
198
225
  unless (fastDistinct vs) $
199
 
    typeError $ IndexVariablesNotDistinct ixs
200
 
  case filter snd $ zip vs (map (`freeIn` pars) vs) of
201
 
    []          -> return ()
202
 
    (v , _) : _ -> typeError $ IndexFreeInParameter v pars
 
226
    typeError $ IndexVariablesNotDistinct vs (map fst ixs)
 
227
 
 
228
  case map fst $ filter snd $ zip vs (map (`freeIn` pars) vs) of
 
229
    [] -> return ()
 
230
    vs ->
 
231
      typeError $ IndicesFreeInParameters vs (map fst ixs) pars
 
232
 
203
233
  where
204
234
  -- | If the term consists solely of constructors (or literals)
205
 
  -- applied to variables, then the variables are returned, and
206
 
  -- otherwise nothing.
207
 
  constructorApplication :: Term -> Maybe [Nat]
208
 
  constructorApplication (Var x [])   = Just [x]
209
 
  constructorApplication (Con c args) = constructorApplications args
210
 
  constructorApplication (Lit {})     = Just []
211
 
  constructorApplication _            = Nothing
212
 
 
213
 
  constructorApplications :: [Arg Term] -> Maybe [Nat]
214
 
  constructorApplications args =
215
 
    concat <$> mapM (constructorApplication . unArg) args
 
235
  -- applied to variables (after parameter reconstruction), then the
 
236
  -- variables are returned, and otherwise nothing.
 
237
  constructorApplication :: Term
 
238
                         -> Type  -- ^ The term's type.
 
239
                         -> TCM (Maybe [Nat])
 
240
  constructorApplication (Var x [])      _ = return (Just [x])
 
241
  constructorApplication (Lit {})        _ = return (Just [])
 
242
  constructorApplication (Shared p)      t  = constructorApplication (derefPtr p) t
 
243
  constructorApplication (Con c conArgs) (El _ (Def d dataArgs)) = do
 
244
    conDef  <- getConstInfo c
 
245
    dataDef <- getConstInfo d
 
246
 
 
247
    let noPars = case theDef dataDef of
 
248
          Datatype { dataPars = n } -> n
 
249
          Record   { recPars  = n } -> n
 
250
          _                         -> __IMPOSSIBLE__
 
251
        pars    = genericTake noPars dataArgs
 
252
        allArgs = pars ++ conArgs
 
253
 
 
254
    reportSDoc "tc.lhs.split.well-formed" 20 $
 
255
      fsep [ text "Reconstructed parameters:"
 
256
           , nest 2 $
 
257
               prettyTCM (Con c []) <+>
 
258
               text "(:" <+> prettyTCM (defType conDef) <> text ")" <+>
 
259
               text "<<" <+> prettyTCM pars <+> text ">>" <+>
 
260
               prettyTCM conArgs
 
261
           ]
 
262
 
 
263
    constructorApplications =<< allArgs `withTypesFrom` defType conDef
 
264
 
 
265
  constructorApplication _ _ = return Nothing
 
266
 
 
267
  constructorApplications :: [(Arg Term, Dom Type)] -> TCM (Maybe [Nat])
 
268
  constructorApplications args = do
 
269
    xs <- mapM (\(e, t) -> constructorApplication (unArg e) (ignoreSharingType $ unDom t))
 
270
               args
 
271
    return (concat <$> sequence xs)
 
272
 
 
273
-- | @args \`withTypesFrom\` t@ returns the arguments @args@ paired up
 
274
-- with their types, taken from @t@, which is assumed to be a @length
 
275
-- args@-ary pi.
 
276
--
 
277
-- Precondition: @t@ has to start with @length args@ pis.
 
278
 
 
279
withTypesFrom :: Args -> Type -> TCM [(Arg Term, Dom Type)]
 
280
[]           `withTypesFrom` _ = return []
 
281
(arg : args) `withTypesFrom` t = do
 
282
  t <- reduce t
 
283
  case ignoreSharing $ unEl t of
 
284
    Pi a b -> ((arg, a) :) <$>
 
285
              args `withTypesFrom` absApp b (unArg arg)
 
286
    _      -> __IMPOSSIBLE__