← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Implicit.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/Implicit.hs
4
4
-}
5
5
module Agda.TypeChecking.Implicit where
6
6
 
 
7
import Control.Applicative
 
8
import Control.Monad
 
9
 
7
10
import Agda.Syntax.Common
 
11
import Agda.Syntax.Internal
 
12
 
 
13
import Agda.TypeChecking.Irrelevance
 
14
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
 
15
import Agda.TypeChecking.Monad
 
16
import Agda.TypeChecking.Reduce
 
17
import Agda.TypeChecking.Substitute
 
18
import Agda.TypeChecking.Telescope
 
19
import {-# SOURCE #-} Agda.TypeChecking.InstanceArguments
 
20
 
 
21
import Agda.Utils.Size
 
22
import Agda.Utils.Tuple
8
23
 
9
24
#include "../undefined.h"
10
25
import Agda.Utils.Impossible
11
 
import Control.Applicative
 
26
 
 
27
 
 
28
-- | @implicitArgs n expand t@ generates up to @n@ implicit arguments
 
29
--   metas (unbounded if @n<0@), as long as @t@ is a function type
 
30
--   and @expand@ holds on the hiding info of its domain.
 
31
implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)
 
32
implicitArgs 0 expand t0 = return ([], t0)
 
33
implicitArgs n expand t0 = do
 
34
    t0' <- reduce t0
 
35
    case ignoreSharing $ unEl t0' of
 
36
      Pi (Dom h rel a) b | expand h -> do
 
37
          when (h == Instance) $ reportSLn "tc.term.args.ifs" 15 $
 
38
            "inserting implicit meta for type " ++ show a
 
39
          v  <- applyRelevanceToContext rel $ newMeta h (absName b) a
 
40
          let arg = Arg h rel v
 
41
          mapFst (arg:) <$> implicitArgs (n-1) expand (absApp b v)
 
42
      _ -> return ([], t0')
 
43
  where
 
44
    newMeta Hidden   = newNamedValueMeta RunMetaOccursCheck
 
45
    newMeta Instance = initializeIFSMeta
 
46
    newMeta _        = __IMPOSSIBLE__
 
47
 
 
48
{- UNUSED, BUT DONT REMOVE (Andreas, 2012-07-31)
 
49
introImplicits :: (Hiding -> Bool) -> Type -> (Int -> Type -> TCM a) -> TCM a
 
50
introImplicits expand t cont = do
 
51
  TelV tel t0 <- telViewUpTo' (-1) (expand . domHiding) t
 
52
  addCtxTel tel $ cont (size tel) t0
 
53
-}
 
54
 
 
55
{- POINTLESS, NEEDS TO BE CONTINUATION-PASSING
 
56
-- | @introImplicits expand t@ introduces domain types of @t@
 
57
--   into the context, as long as @expand@ holds on them.
 
58
introImplicits :: (Hiding -> Bool) -> Type -> TCM (Int, Type)
 
59
introImplicits expand t = do
 
60
  t <- reduce t
 
61
  case unEl t of
 
62
    Pi dom@(Dom h rel a) b | expand h ->
 
63
      addCtxString (absName b) dom $ do
 
64
        mapFst (+1) <$> introImplicits expand (absBody b)
 
65
    _ -> return (0, t)
 
66
-}
 
67
 
 
68
---------------------------------------------------------------------------
12
69
 
13
70
data ImplicitInsertion
14
71
      = ImpInsert [Hiding]        -- ^ this many implicits have to be inserted