← 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/Telescope.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/Telescope.hs
3
3
module Agda.TypeChecking.Telescope where
4
4
 
5
5
import Control.Applicative
6
 
 
 
6
import Control.Monad (forM_, unless)
7
7
import Data.List
8
8
 
9
9
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
20
20
import Agda.Utils.Size
21
21
import Agda.Utils.Tuple
22
22
import Agda.Utils.VarSet (VarSet)
23
 
import qualified Agda.Utils.VarSet as Set
 
23
import qualified Agda.Utils.VarSet as VarSet
24
24
 
25
 
#include "../undefined.h"
 
25
#include "undefined.h"
26
26
import Agda.Utils.Impossible
27
27
 
 
28
data OutputTypeName
 
29
  = OutputTypeName QName
 
30
  | OutputTypeNameNotYetKnown
 
31
  | NoOutputTypeName
 
32
 
 
33
-- | Strips all Pi's and return the head definition name, if possible.
 
34
getOutputTypeName :: Type -> TCM OutputTypeName
 
35
getOutputTypeName t = do
 
36
  TelV tel t' <- telView t
 
37
  ifBlocked (unEl t') (\ _ _ -> return OutputTypeNameNotYetKnown) $ \ v ->
 
38
    case ignoreSharing v of
 
39
      -- Possible base types:
 
40
      Def n _  -> return $ OutputTypeName n
 
41
      Sort{}   -> return NoOutputTypeName
 
42
      Var{}    -> return NoOutputTypeName
 
43
      -- Not base types:
 
44
      Con{}    -> __IMPOSSIBLE__
 
45
      ExtLam{} -> __IMPOSSIBLE__
 
46
      Lam{}    -> __IMPOSSIBLE__
 
47
      Lit{}    -> __IMPOSSIBLE__
 
48
      Level{}  -> __IMPOSSIBLE__
 
49
      MetaV{}  -> __IMPOSSIBLE__
 
50
      Pi{}     -> __IMPOSSIBLE__
 
51
      Shared{} -> __IMPOSSIBLE__
 
52
      DontCare{} -> __IMPOSSIBLE__
 
53
 
28
54
-- | The permutation should permute the corresponding telescope. (left-to-right list)
29
55
renameP :: Subst t => Permutation -> t -> t
30
56
renameP p = applySubst (renaming p)
33
59
renaming :: Permutation -> Substitution
34
60
renaming p = gamma'
35
61
  where
36
 
    n      = size p
37
 
    gamma  = permute (reverseP $ invertP $ reverseP p) $ map var [0..]
38
 
    gamma' = gamma ++# raiseS n
 
62
    n      = size p
 
63
    gamma  = safePermute (reverseP $ invertP (-1) $ reverseP p) $ map var [0..]
 
64
    gamma' = prependS __IMPOSSIBLE__ gamma (raiseS n)
39
65
 
40
66
-- | If @permute π : [a]Γ -> [a]Δ@, then @substs (renamingR π) : Term Δ -> Term Γ@
41
67
renamingR :: Permutation -> Substitution
43
69
 
44
70
-- | Flatten telescope: (Γ : Tel) -> [Type Γ]
45
71
flattenTel :: Telescope -> [Dom Type]
46
 
flattenTel EmptyTel          = []
 
72
flattenTel EmptyTel          = []
47
73
flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
48
74
 
49
75
-- | Order a flattened telescope in the correct dependeny order: Γ ->
65
91
-- | Unflatten: turns a flattened telescope into a proper telescope. Must be
66
92
--   properly ordered.
67
93
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
68
 
unflattenTel []   []            = EmptyTel
 
94
unflattenTel []   []            = EmptyTel
69
95
unflattenTel (x : xs) (a : tel) = ExtendTel a' (Abs x tel')
70
96
  where
71
97
    tel' = unflattenTel xs tel
87
113
 
88
114
-- | A telescope split in two.
89
115
data SplitTel = SplitTel
90
 
      { firstPart  :: Telescope
91
 
      , secondPart :: Telescope
92
 
      , splitPerm  :: Permutation
93
 
      }
 
116
  { firstPart  :: Telescope
 
117
  , secondPart :: Telescope
 
118
  , splitPerm  :: Permutation
 
119
    -- ^ The permutation takes us from the original telescope to
 
120
    --   @firstPart ++ secondPart@.
 
121
  }
94
122
 
95
123
-- | Split a telescope into the part that defines the given variables and the
96
124
--   part that doesn't.
97
 
splitTelescope :: VarSet -> Telescope -> SplitTel
 
125
--
 
126
--   See 'Agda.TypeChecking.Tests.prop_splitTelescope'.
 
127
splitTelescope
 
128
  :: VarSet     -- ^ A set of de Bruijn indices.
 
129
  -> Telescope  -- ^ Original telescope.
 
130
  -> SplitTel   -- ^ @firstPart@ mentions the given variables, @secondPart@ not.
98
131
splitTelescope fv tel = SplitTel tel1 tel2 perm
99
132
  where
100
133
    names = teleNames tel
101
134
    ts0   = flattenTel tel
102
 
 
103
135
    n     = size tel
104
136
 
105
137
    -- We start with a rough split into fv and the rest. This will most likely
106
138
    -- not be correct so we patch it up later with reorderTel.
107
 
    is    = map (n - 1 -) $ filter (< n) $ reverse $ Set.toList fv
 
139
 
 
140
    -- Convert given de Bruijn indices into ascending list of de Bruijn levels.
 
141
    is    = map (n - 1 -) $ dropWhile (>= n) $ VarSet.toDescList fv
 
142
    -- Compute the complement (de Bruijn levels not mentioned in @fv@).
108
143
    isC   = [0..n - 1] \\ is
109
144
    perm0 = Perm n $ is ++ isC
110
145
 
120
155
 
121
156
    tel'  = unflattenTel (permute perm names) ts2
122
157
 
123
 
    Perm _ js = perm
124
 
    m         = genericLength $ takeWhile (`notElem` is) (reverse js)
125
 
    (tel1, tel2) = telFromList -*- telFromList $ genericSplitAt (n - m) $ telToList tel'
 
158
    m            = length $ takeWhile (`notElem` is) $ reverse $ permPicks perm
 
159
    (tel1, tel2) = telFromList -*- telFromList $ splitAt (n - m) $ telToList tel'
126
160
 
127
161
telView :: Type -> TCM TelView
128
162
telView = telViewUpTo (-1)
154
188
  case ignoreSharing $ unEl t of
155
189
    Pi  _ b -> absApp b (unArg arg) `piApplyM` args
156
190
    _       -> __IMPOSSIBLE__
 
191
 
 
192
---------------------------------------------------------------------------
 
193
-- * Instance definitions
 
194
---------------------------------------------------------------------------
 
195
 
 
196
addTypedInstance :: QName -> Type -> TCM ()
 
197
addTypedInstance x t = do
 
198
  n <- getOutputTypeName t
 
199
  case n of
 
200
    OutputTypeName n -> addNamedInstance x n
 
201
    OutputTypeNameNotYetKnown -> addUnknownInstance x
 
202
    NoOutputTypeName -> typeError $ GenericError $ "Terms marked as eligible for instance search should end with a name"
 
203
 
 
204
resolveUnknownInstanceDefs :: TCM ()
 
205
resolveUnknownInstanceDefs = do
 
206
  anonInstanceDefs <- getAnonInstanceDefs
 
207
  clearAnonInstanceDefs
 
208
  forM_ anonInstanceDefs $ \ n -> addTypedInstance n =<< typeOfConst n
 
209
 
 
210
-- | Try to solve the instance definitions whose type is not yet known, report
 
211
--   an error if it doesn't work and return the instance table otherwise.
 
212
getInstanceDefs :: TCM InstanceTable
 
213
getInstanceDefs = do
 
214
  resolveUnknownInstanceDefs
 
215
  insts <- getAllInstanceDefs
 
216
  unless (null $ snd insts) $
 
217
    typeError $ GenericError $ "There are instances whose type is still unsolved"
 
218
  return $ fst insts