← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Scope/Monad.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Scope/Monad.hs
6
6
module Agda.Syntax.Scope.Monad where
7
7
 
8
8
import Prelude hiding (mapM)
 
9
import Control.Arrow ((***), first, second)
9
10
import Control.Applicative
10
11
import Control.Monad hiding (mapM)
11
12
import Control.Monad.Writer hiding (mapM)
12
13
import Control.Monad.State hiding (mapM)
 
14
 
 
15
import Data.List
13
16
import Data.Map (Map)
 
17
import qualified Data.Map as Map
 
18
import Data.Maybe
14
19
import Data.Traversable
15
 
import Data.List
16
 
import qualified Data.Map as Map
17
20
 
18
21
import Agda.Syntax.Common
19
22
import Agda.Syntax.Position
20
23
import Agda.Syntax.Fixity
21
 
import Agda.Syntax.Notation
22
24
import Agda.Syntax.Abstract.Name as A
23
25
import Agda.Syntax.Concrete as C
24
26
import Agda.Syntax.Scope.Base
43
45
 
44
46
-- * Errors
45
47
 
46
 
notInScope :: C.QName -> ScopeM a
47
 
notInScope x = typeError $ NotInScope [x]
48
 
 
49
48
isDatatypeModule :: A.ModuleName -> ScopeM Bool
50
49
isDatatypeModule m = do
51
50
   sc <- getScope
158
157
getLocalVars = scopeLocals <$> getScope
159
158
 
160
159
setLocalVars :: LocalVars -> ScopeM ()
161
 
setLocalVars vars = modifyScope $ \s -> s { scopeLocals = vars }
 
160
setLocalVars vars = modifyScope $ setScopeLocals vars
162
161
 
163
162
-- | Run a computation without changing the local variables.
164
163
withLocalVars :: ScopeM a -> ScopeM a
171
170
-- * Names
172
171
 
173
172
-- | Create a fresh abstract name from a concrete name.
 
173
--
 
174
--   This function is used when we translate a concrete name
 
175
--   in a binder.  The 'Range' of the concrete name is
 
176
--   saved as the 'nameBindingSite' of the abstract name.
174
177
freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name
175
178
freshAbstractName fx x = do
176
179
  i <- fresh
177
 
  return $ A.Name i x (getRange x) fx
 
180
  return $ A.Name
 
181
    { nameId          = i
 
182
    , nameConcrete    = x
 
183
    , nameBindingSite = getRange x
 
184
    , nameFixity      = fx
 
185
    }
178
186
 
179
187
-- | @freshAbstractName_ = freshAbstractName defaultFixity@
180
188
freshAbstractName_ :: C.Name -> ScopeM A.Name
199
207
 
200
208
-- | Look up the abstract name referred to by a given concrete name.
201
209
resolveName :: C.QName -> ScopeM ResolvedName
202
 
resolveName x = do
 
210
resolveName = resolveName' allKindsOfNames
 
211
 
 
212
-- | Look up the abstract name corresponding to a concrete name of
 
213
--   a certain kind.
 
214
--   Sometimes we know already that we are dealing with a constructor
 
215
--   or pattern synonym (e.g. when we have parsed a pattern).
 
216
--   Then, we can ignore conflicting definitions of that name
 
217
--   of a different kind. (See issue 822.)
 
218
resolveName' :: [KindOfName] -> C.QName -> ScopeM ResolvedName
 
219
resolveName' kinds x = do
203
220
  scope <- getScope
204
221
  let vars = map (C.QName -*- id) $ scopeLocals scope
205
222
  case lookup x vars of
206
223
    Just y  -> return $ VarName $ y { nameConcrete = unqualify x }
207
 
    Nothing -> case scopeLookup' x scope of
 
224
    Nothing -> case filter ((`elem` kinds) . anameKind . fst) $ scopeLookup' x scope of
208
225
      [] -> return UnknownName
209
226
      ds | all ((==ConName) . anameKind . fst) ds ->
210
227
        return $ ConstructorName
224
241
resolveModule x = do
225
242
  ms <- scopeLookup x <$> getScope
226
243
  case ms of
227
 
    [AbsModule m] -> return $ AbsModule (m `withRangesOfQ` x)
228
 
    []            -> typeError $ NoSuchModule x
229
 
    ms            -> typeError $ AmbiguousModule x (map amodName ms)
 
244
    [AbsModule m why] -> return $ AbsModule (m `withRangesOfQ` x) why
 
245
    []                -> typeError $ NoSuchModule x
 
246
    ms                -> typeError $ AmbiguousModule x (map amodName ms)
230
247
 
231
248
-- | Get the fixity of a name. The name is assumed to be in scope.
232
249
getFixity :: C.QName -> ScopeM Fixity'
263
280
    VarName z          -> typeError $ ClashingDefinition (C.QName x) $ A.qualify (mnameFromList []) z
264
281
    ConstructorName [] -> __IMPOSSIBLE__
265
282
    ConstructorName ds
266
 
      | kind == ConName && all ((==ConName) . anameKind) ds -> return [ AbsName y kind ]
 
283
      | kind == ConName && all ((==ConName) . anameKind) ds -> return [ AbsName y kind Defined ]
267
284
      | otherwise -> typeError $ ClashingDefinition (C.QName x) $ anameName (head' ds)
268
285
    PatternSynResName n -> typeError $ ClashingDefinition (C.QName x) $ anameName n
269
 
    UnknownName         -> return [AbsName y kind]
 
286
    UnknownName         -> return [AbsName y kind Defined]
270
287
  modifyCurrentScope $ addNamesToScope (localNameSpace acc) x ys
271
288
  where
272
289
    head' []    = {- ' -} __IMPOSSIBLE__
275
292
-- | Bind a module name.
276
293
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
277
294
bindModule acc x m = modifyCurrentScope $
278
 
  addModuleToScope (localNameSpace acc) x (AbsModule m)
 
295
  addModuleToScope (localNameSpace acc) x (AbsModule m Defined)
279
296
 
280
297
-- | Bind a qualified module name. Adds it to the imports field of the scope.
281
298
bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
299
316
-- | Create a new scope with the given name from an old scope. Renames
300
317
--   public names in the old scope to match the new name and returns the
301
318
--   renamings.
302
 
copyScope :: A.ModuleName -> Scope -> ScopeM (Scope, (Ren A.ModuleName, Ren A.QName))
303
 
copyScope new s = runStateT (copy new s) (Map.empty, Map.empty)
 
319
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, (Ren A.ModuleName, Ren A.QName))
 
320
copyScope cm new s = first (inScopeBecause $ Applied cm) <$> runStateT (copy new s) (Map.empty, Map.empty)
304
321
  where
305
322
    copy new s = do
306
323
      s0 <- lift $ getNamedScope new
313
330
    old  = scopeName s
314
331
 
315
332
    copyM :: NameSpaceId -> ModulesInScope -> WSM ModulesInScope
316
 
    copyM ImportedNS      ms = return ms
 
333
    copyM ImportedNS      ms = traverse (mapM $ onMod renMod) ms
317
334
    copyM PrivateNS       _  = return Map.empty
318
335
    copyM PublicNS        ms = traverse (mapM $ onMod renMod) ms
319
336
    copyM OnlyQualifiedNS ms = traverse (mapM $ onMod renMod) ms
320
337
 
321
338
    copyD :: NameSpaceId -> NamesInScope -> WSM NamesInScope
322
 
    copyD ImportedNS      ds = return ds
 
339
    copyD ImportedNS      ds = traverse (mapM $ onName renName) ds
323
340
    copyD PrivateNS       _  = return Map.empty
324
341
    copyD PublicNS        ds = traverse (mapM $ onName renName) ds
325
342
    copyD OnlyQualifiedNS ds = traverse (mapM $ onName renName) ds
328
345
      x <- f $ amodName m
329
346
      return m { amodName = x }
330
347
 
331
 
    onName f d = do
332
 
      x <- f $ anameName d
333
 
      return d { anameName = x }
 
348
    onName f d =
 
349
      case anameKind d of
 
350
        PatternSynName -> return d  -- Pattern synonyms are simply aliased, not renamed
 
351
        _ -> do
 
352
          x <- f $ anameName d
 
353
          return d { anameName = x }
334
354
 
335
355
    addName x y = addNames (Map.singleton x y)
336
356
    addMod  x y = addMods (Map.singleton x y)
341
361
    findName x = Map.lookup x <$> gets snd
342
362
    findMod  x = Map.lookup x <$> gets fst
343
363
 
 
364
    isInOld qs = isPrefixOf (A.mnameToList old) qs
 
365
 
344
366
    -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
 
367
    -- Ulf, 2013-11-06: We should run this also on the imported name space
 
368
    -- (issue892), so make sure to only rename things with the prefix M.
345
369
    renName :: A.QName -> WSM A.QName
 
370
    renName x | not (isInOld $ A.qnameToList x) = return x
346
371
    renName x = do
347
372
      -- Check if we've seen it already
348
373
      my <- findName x
360
385
 
361
386
    -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
362
387
    renMod :: A.ModuleName -> WSM A.ModuleName
 
388
    renMod x | not (isInOld $ A.mnameToList x) = return x
363
389
    renMod x = do
364
390
      -- Check if we've seen it already
365
391
      my <- findMod x
378
404
      where
379
405
        dequalify = A.mnameFromList . drop (size old) . A.mnameToList
380
406
 
 
407
-- | Apply an import directive and check that all the names mentioned actually
381
408
--   exist.
382
409
applyImportDirectiveM :: C.QName -> ImportDirective -> Scope -> ScopeM Scope
383
410
applyImportDirectiveM m dir scope = do
384
 
  xs <- filterM doesntExist names
385
 
  reportSLn "scope.import.apply" 20 $ "non existing names: " ++ show xs
386
 
  case xs of
387
 
    []  -> case targetNames \\ nub targetNames of
388
 
      []  -> return $ applyImportDirective dir scope
389
 
      dup -> typeError $ DuplicateImports m dup
390
 
    _   -> typeError $ ModuleDoesntExport m xs
 
411
    let xs = filter doesntExist names
 
412
    reportSLn "scope.import.apply" 20 $ "non existing names: " ++ show xs
 
413
    unless (null xs)  $ typeError $ ModuleDoesntExport m xs
 
414
 
 
415
    let dup = targetNames \\ nub targetNames
 
416
    unless (null dup) $ typeError $ DuplicateImports m dup
 
417
    return $ applyImportDirective dir scope
 
418
 
391
419
  where
392
420
    names :: [ImportedName]
393
421
    names = map renFrom (renaming dir) ++ case usingOrHiding dir of
402
429
      where
403
430
        renName r = (renFrom r) { importedName = renTo r }
404
431
 
405
 
    doesntExist (ImportedName x) =
406
 
      case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractName) of
407
 
        Just _  -> return False
408
 
        Nothing -> return True
409
 
    doesntExist (ImportedModule x) =
410
 
      case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractModule) of
411
 
        Just _  -> return False
412
 
        Nothing -> return True
 
432
    doesntExist (ImportedName   x) = isNothing $
 
433
      Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractName)
 
434
    doesntExist (ImportedModule x) = isNothing $
 
435
      Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractModule)
413
436
 
414
437
-- | Open a module.
415
438
openModule_ :: C.QName -> ImportDirective -> ScopeM ()
418
441
  m <- amodName <$> resolveModule cm
419
442
  let ns = namespace current m
420
443
  s <- setScopeAccess ns <$>
421
 
        (applyImportDirectiveM cm dir . removeOnlyQualified . restrictPrivate =<< getNamedScope m)
 
444
        (applyImportDirectiveM cm dir . inScopeBecause (Opened cm) . removeOnlyQualified . restrictPrivate =<< getNamedScope m)
422
445
  checkForClashes (scopeNameSpace ns s)
423
446
  modifyCurrentScope (`mergeScope` s)
424
447
  where