← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/Auto/Auto.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/Auto/Auto.hs
39
39
import qualified Agda.Syntax.Abstract.Name as AN
40
40
import qualified Agda.TypeChecking.Monad.Base as MB
41
41
import Agda.TypeChecking.EtaContract (etaContract)
 
42
import qualified Agda.Utils.HashMap as HMap
42
43
 
43
44
import Agda.Auto.Convert
44
45
import Agda.Auto.NarrowingSearch
163
164
                  [] -> case Map.elems tccons of
164
165
                   (m, mytype, mylocalVars, _) : [] -> do
165
166
                       defdfv <- case thisdefinfo of
166
 
                                  Just (def, _, _) -> fromIntegral `liftM` getdfv mi def
 
167
                                  Just (def, _, _) -> getdfv mi def
167
168
                                  Nothing -> return 0
168
169
                       ee <- liftIO $ newIORef $ ConstDef {cdname = "T", cdorigin = __IMPOSSIBLE__, cdtype = NotM $ Sort (Set 0), cdcont = Postulate, cddeffreevars = 0}
169
170
                       let modargs = drop (length mylocalVars - defdfv) mylocalVars
196
197
                   Just (def, clause, _) -> do
197
198
                    let [rectyp'] = mymrectyp
198
199
                    defdfv <- getdfv mi def
199
 
                    myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = fromIntegral defdfv}
 
200
                    myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = defdfv}
200
201
                    (_, pats) <- constructPats cmap mi clause
201
 
                    defdfv <- fromIntegral `liftM` getdfv mi def
 
202
                    defdfv <- getdfv mi def
202
203
                    return $ if contains_constructor pats then
203
204
                      (Just (pats, myrecdef), defdfv)
204
205
                     else
285
286
                 ticks <- liftIO $ newIORef 0
286
287
                 let [rectyp'] = mymrectyp
287
288
                 defdfv <- getdfv mi def
288
 
                 myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = fromIntegral defdfv}
 
289
                 myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = defdfv}
289
290
                 sols <- liftIO $ System.Timeout.timeout (timeout * 1000000) (
290
291
                    let r d = do
291
292
                         sols <- liftIO $ caseSplitSearch ticks __IMPOSSIBLE__ myhints meqr __IMPOSSIBLE__ d myrecdef ctx mytype pats
304
305
                        -- Normalise the dot patterns
305
306
                        ps <- addCtxTel tel $ normalise ps
306
307
                        body <- etaContractBody body
307
 
                        liftM modifyAbstractClause $ inContext [] $ reify $ NamedClause def $ I.Clause noRange tel perm ps body
 
308
                        liftM modifyAbstractClause $ inContext [] $ reify $ AN.QNamed def $ I.Clause noRange tel perm ps body
308
309
                      ) cls'
309
310
                     pcs <- withInteractionId ii $ mapM prettyA cls''
310
311
                     ticks <- liftIO $ readIORef ticks
319
320
 
320
321
            MRefine listmode -> do
321
322
             mv <- lookupMeta mi
322
 
             let HasType _ tt = mvJudgement mv
 
323
             let tt = jMetaType $ mvJudgement mv
323
324
                 minfo = getMetaInfo mv
324
325
             targettyp <- withMetaInfo minfo $ do
325
326
              vs <- getContextArgs
326
 
              let targettype = tt `piApply` permute (takeP (fromIntegral $ length vs) $ mvPermutation mv) vs
 
327
              let targettype = tt `piApply` permute (takeP (length vs) $ mvPermutation mv) vs
327
328
              normalise targettype
328
329
             let tctx = length $ envContext $ clEnv minfo
329
330
 
331
332
               st <- liftTCM $ join $ pureTCM $ \st _ -> return st
332
333
               let defs = sigDefinitions $ stSignature st
333
334
                   idefs = sigDefinitions $ stImports st
334
 
                   alldefs = Map.keys defs ++ Map.keys idefs
 
335
                   alldefs = HMap.keys defs ++ HMap.keys idefs
335
336
               liftM catMaybes $ mapM (\n ->
336
337
                 case thisdefinfo of
337
338
                  Just (def, _, _) | def == n -> return Nothing
343
344
                     c <- getConstInfo n
344
345
                     ctyp <- normalise $ defType c
345
346
                     cdfv <- withMetaInfo minfo $ getDefFreeVars n
346
 
                     return $ case matchType cdfv (fromIntegral tctx) ctyp targettyp of
 
347
                     return $ case matchType cdfv tctx ctyp targettyp of
347
348
                      Nothing -> Nothing
348
349
                      Just score -> Just (show cn, score)
349
350
                ) alldefs
359
360
                 c <- getConstInfo n
360
361
                 ctyp <- normalise $ defType c
361
362
                 cdfv <- withMetaInfo minfo $ getDefFreeVars n
362
 
                 return $ case matchType cdfv (fromIntegral tctx) ctyp targettyp of
 
363
                 return $ case matchType cdfv tctx ctyp targettyp of
363
364
                  Nothing -> Nothing
364
365
                  Just score -> Just (show cn, score)
365
366
                ) modnames