← 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/Translation/ConcreteToAbstract.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/Translation/ConcreteToAbstract.hs
1
 
{-# LANGUAGE CPP, MultiParamTypeClasses, FunctionalDependencies,
2
 
             FlexibleInstances, UndecidableInstances, OverlappingInstances,
3
 
             ScopedTypeVariables
4
 
  #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleInstances #-}
 
3
{-# LANGUAGE FunctionalDependencies #-}
 
4
{-# LANGUAGE MultiParamTypeClasses #-}
 
5
{-# LANGUAGE OverlappingInstances #-}
 
6
{-# LANGUAGE ScopedTypeVariables #-}
 
7
{-# LANGUAGE TypeSynonymInstances #-}
 
8
{-# LANGUAGE UndecidableInstances #-}
5
9
 
6
10
{-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,
7
11
    figuring out infix operator precedences and tidying up definitions.
26
30
import Control.Applicative
27
31
import Control.Monad.Reader hiding (mapM)
28
32
import Control.Monad.Error hiding (mapM)
29
 
import Data.Typeable
 
33
 
 
34
import Data.Foldable (Foldable, traverse_)
30
35
import Data.Traversable (mapM, traverse)
31
36
import Data.List ((\\), nub, foldl')
32
37
import qualified Data.Map as Map
 
38
import Data.Maybe
33
39
 
34
40
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
 
41
import Agda.Syntax.Concrete.Generic
35
42
import Agda.Syntax.Concrete.Operators
36
43
import Agda.Syntax.Abstract as A
37
 
import Agda.Syntax.Abstract.Copatterns
38
44
import Agda.Syntax.Position
39
 
import Agda.Syntax.Common
 
45
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
 
46
import qualified Agda.Syntax.Common as Common
40
47
import Agda.Syntax.Info
41
48
import Agda.Syntax.Concrete.Definitions as C
42
 
import Agda.Syntax.Concrete.Pretty
43
 
import Agda.Syntax.Abstract.Pretty
44
49
import Agda.Syntax.Fixity
45
50
import Agda.Syntax.Notation
46
51
import Agda.Syntax.Scope.Base
49
53
 
50
54
import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
51
55
                                     TCErr(..), extendlambdaname)
52
 
import Agda.TypeChecking.Monad.Trace (traceCall, traceCallCPS, setCurrentRange)
 
56
import Agda.TypeChecking.Monad.Benchmark (billTo, billTop, reimburseTop)
 
57
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 
58
import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
53
59
import Agda.TypeChecking.Monad.State
 
60
import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
54
61
import Agda.TypeChecking.Monad.Options
 
62
import Agda.TypeChecking.Monad.Env (insideDotPattern, isInsideDotPattern)
55
63
 
 
64
import Agda.Interaction.FindFile (checkModuleName)
 
65
-- import Agda.Interaction.Imports  -- for type-checking in ghci
56
66
import {-# SOURCE #-} Agda.Interaction.Imports (scopeCheckImport)
57
67
import Agda.Interaction.Options
58
68
 
 
69
import Agda.Utils.FileName
 
70
import Agda.Utils.Functor
 
71
import Agda.Utils.Fresh
 
72
import Agda.Utils.List
59
73
import Agda.Utils.Monad
60
 
import Agda.Utils.Tuple
61
 
import Agda.Utils.List
62
 
import Agda.Utils.Fresh
63
74
import Agda.Utils.Pretty
64
75
 
65
76
#include "../../undefined.h"
81
92
printLocals :: Int -> String -> ScopeM ()
82
93
printLocals v s = verboseS "scope.top" v $ do
83
94
  locals <- getLocalVars
84
 
  reportSLn "" 0 $ s ++ " " ++ show locals
85
 
 
86
 
printScope :: String -> Int -> String -> ScopeM ()
87
 
printScope tag v s = verboseS ("scope." ++ tag) v $ do
88
 
  scope <- getScope
89
 
  reportSDoc "" 0 $ return $ vcat [ text s, text $ show scope ]
 
95
  reportSLn "scope.top" v $ s ++ " " ++ show locals
90
96
 
91
97
{--------------------------------------------------------------------------
92
98
    Helpers
138
144
recordConstructorType :: [NiceDeclaration] -> C.Expr
139
145
recordConstructorType fields = build fs
140
146
  where
 
147
    -- drop all declarations after the last field declaration
141
148
    fs = reverse $ dropWhile notField $ reverse fields
142
149
 
143
150
    notField NiceField{} = False
144
151
    notField _           = True
145
152
 
146
 
    build (NiceField r f _ _ x (Arg h rel e) : fs) =
147
 
        C.Pi [C.TypedBindings r $ Arg h rel (C.TBind r [BName x f] e)] $ build fs
 
153
    -- Andreas, 2013-11-08
 
154
    -- Turn @open public@ into just @open@, since we cannot have an
 
155
    -- @open public@ in a @let@.  Fixes issue 532.
 
156
    build (NiceOpen r m dir@ImportDirective{ publicOpen = True }  : fs) =
 
157
      build (NiceOpen r m dir{ publicOpen = False } : fs)
 
158
 
 
159
    build (NiceModuleMacro r p x modapp open dir@ImportDirective{ publicOpen = True } : fs) =
 
160
      build (NiceModuleMacro r p x modapp open dir{ publicOpen = False } : fs)
 
161
 
 
162
    build (NiceField r f _ _ x (Common.Arg info e) : fs) =
 
163
        C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [mkBoundName x f] e)] $ build fs
148
164
      where r = getRange x
149
 
    build (d : fs)                     = C.Let noRange [killRange $ notSoNiceDeclaration d] $
 
165
    build (d : fs)                     = C.Let (getRange d) [notSoNiceDeclaration d] $
150
166
                                           build fs
151
167
    build []                           = C.SetN noRange 0 -- todo: nicer
152
168
 
 
169
 
 
170
-- | @checkModuleApplication modapp m0 x dir = return (modapp', renD, renM)@
 
171
--
 
172
--   @m0@ is the new (abstract) module name and
 
173
--   @x@ its concret form (used for error messages).
 
174
checkModuleApplication
 
175
  :: C.ModuleApplication
 
176
  -> ModuleName
 
177
  -> C.Name
 
178
  -> ImportDirective
 
179
  -> ScopeM (A.ModuleApplication, Ren A.QName, Ren ModuleName)
 
180
 
153
181
checkModuleApplication (C.SectionApp _ tel e) m0 x dir' =
 
182
  -- For the following, set the current module to be m0.
154
183
  withCurrentModule m0 $ do
 
184
    -- check that expression @e@ is of the form @m args@
155
185
    (m, args) <- case appView e of
156
186
      AppView (Ident m) args -> return (m, args)
157
187
      _                      -> notAModuleExpr e
158
188
 
 
189
    -- scope check the telescope (introduces bindings!)
159
190
    tel' <- toAbstract tel
160
 
    (m1,args') <- toAbstract (OldModuleName m
161
 
                             , args
162
 
                             )
163
 
    s  <- getNamedScope m1
 
191
    -- scope the old module name, the module args
 
192
    (m1,args') <- toAbstract (OldModuleName m, args)
164
193
    -- Drop constructors (OnlyQualified) if there are arguments. The record constructor
165
194
    -- isn't properly in the record module, so copying it will lead to badness.
166
195
    let noRecConstr | null args = id
167
196
                    | otherwise = removeOnlyQualified
168
 
    (s', (renM, renD)) <- copyScope m0 . noRecConstr =<< getNamedScope m1
 
197
    -- Copy the scope associated with m and take the parts actually imported.
 
198
    (s', (renM, renD)) <- copyScope m m0 . noRecConstr =<< getNamedScope m1
169
199
    s' <- applyImportDirectiveM (C.QName x) dir' s'
 
200
    -- Set the current scope to @s'@
170
201
    modifyCurrentScope $ const s'
171
202
    printScope "mod.inst" 20 "copied source module"
172
203
    reportSLn "scope.mod.inst" 30 $ "renamings:\n  " ++ show renD ++ "\n  " ++ show renM
173
204
    return ((A.SectionApp tel' m1 args'), renD, renM)
 
205
 
174
206
checkModuleApplication (C.RecordModuleIFS _ recN) m0 x dir' =
175
207
  withCurrentModule m0 $ do
176
208
    m1 <- toAbstract $ OldModuleName recN
177
209
    s <- getNamedScope m1
178
 
    (s', (renM, renD)) <- copyScope m0 s
 
210
    (s', (renM, renD)) <- copyScope recN m0 s
179
211
    s' <- applyImportDirectiveM recN dir' s'
180
212
    modifyCurrentScope $ const s'
181
213
 
182
214
    printScope "mod.inst" 20 "copied record module"
183
215
    return ((A.RecordModuleIFS m1), renD, renM)
184
216
 
 
217
-- | @checkModuleMacro mkApply range access concreteName modapp open dir@
 
218
--
 
219
--   Preserves local variables.
 
220
 
 
221
checkModuleMacro
 
222
  :: (ModuleInfo -> ModuleName -> A.ModuleApplication -> Ren A.QName -> Ren ModuleName -> a)
 
223
  -> Range
 
224
  -> Access
 
225
  -> C.Name
 
226
  -> C.ModuleApplication
 
227
  -> OpenShortHand
 
228
  -> ImportDirective
 
229
  -> ScopeM [a]
185
230
checkModuleMacro apply r p x modapp open dir = withLocalVars $ do
186
231
    notPublicWithoutOpen open dir
187
232
 
198
243
    (modapp', renD, renM) <- checkModuleApplication modapp m0 x dir'
199
244
    bindModule p x m0
200
245
    printScope "mod.inst.copy.after" 20 "after copying"
201
 
    case open of
202
 
      DoOpen   -> openModule_ (C.QName x) dir
203
 
      DontOpen -> return ()
 
246
    when (open == DoOpen) $
 
247
      openModule_ (C.QName x) dir
204
248
    printScope "mod.inst" 20 $ show open
205
249
    stripNoNames
206
250
    printScope "mod.inst" 10 $ "after stripping"
225
269
-- | Computes the range of all the \"to\" keywords used in a renaming
226
270
-- directive.
227
271
 
 
272
renamingRange :: ImportDirective -> Range
228
273
renamingRange = getRange . map renToRange . renaming
229
274
 
230
275
{--------------------------------------------------------------------------
301
346
    return y
302
347
 
303
348
instance ToAbstract (NewName C.BoundName) A.Name where
304
 
  toAbstract (NewName (BName x fx)) = do
 
349
  toAbstract (NewName BName{ boundName = x, bnameFixity = fx }) = do
305
350
    y <- freshAbstractName fx x
306
351
    bindVariable x y
307
352
    return y
333
378
instance ToAbstract PatName APatName where
334
379
  toAbstract (PatName x) = do
335
380
    reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
336
 
    rx <- resolveName x
 
381
    rx <- resolveName' [ConName, PatternSynName] x -- Andreas, 2013-03-21 ignore conflicting names which cannot be meant since we are in a pattern
337
382
    z  <- case (rx, x) of
338
383
      -- TODO: warn about shadowing
339
384
      (VarName y,       C.QName x)                          -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
365
410
    rx <- resolveName (C.QName x)
366
411
    case rx of
367
412
      DefinedName _ d -> return $ anameName d
368
 
      _               -> error $ show x ++ " - " ++ show rx
 
413
      _               -> __IMPOSSIBLE__
 
414
        -- error $ show x ++ " - " ++ show rx
369
415
 
370
416
newtype NewModuleName      = NewModuleName      C.Name
371
417
newtype NewModuleQName     = NewModuleQName     C.QName
408
454
-- Expressions ------------------------------------------------------------
409
455
 
410
456
-- | Peel off 'C.HiddenArg' and represent it as an 'NamedArg'.
411
 
mkNamedArg :: C.Expr -> NamedArg C.Expr
412
 
mkNamedArg (C.HiddenArg _ e) = Arg Hidden    Relevant e
413
 
mkNamedArg (C.InstanceArg _ e) = Arg Instance    Relevant e
414
 
mkNamedArg e                 = Arg NotHidden Relevant $ unnamed e
 
457
mkNamedArg :: C.Expr -> C.NamedArg C.Expr
 
458
mkNamedArg (C.HiddenArg   _ e) = Common.Arg (setHiding Hidden defaultArgInfo) e
 
459
mkNamedArg (C.InstanceArg _ e) = Common.Arg (setHiding Instance defaultArgInfo) e
 
460
mkNamedArg e                   = Common.Arg defaultArgInfo $ unnamed e
415
461
 
416
462
-- | Peel off 'C.HiddenArg' and represent it as an 'Arg', throwing away any name.
417
 
mkArg' :: Relevance -> C.Expr -> Arg C.Expr
418
 
mkArg' r (C.HiddenArg _ e) = Arg Hidden    r $ namedThing e
419
 
mkArg' r (C.InstanceArg _ e) = Arg Instance    r $ namedThing e
420
 
mkArg' r e                 = Arg NotHidden r e
 
463
mkArg' :: C.ArgInfo -> C.Expr -> C.Arg C.Expr
 
464
mkArg' info (C.HiddenArg   _ e) = Common.Arg (setHiding Hidden info) $ namedThing e
 
465
mkArg' info (C.InstanceArg _ e) = Common.Arg (setHiding Instance info) $ namedThing e
 
466
mkArg' info e                   = Common.Arg (setHiding NotHidden info) e
421
467
 
422
468
-- | By default, arguments are @Relevant@.
423
 
mkArg :: C.Expr -> Arg C.Expr
 
469
mkArg :: C.Expr -> C.Arg C.Expr
424
470
-- mkArg (C.Dot _ e) = mkArg' Irrelevant e
425
 
mkArg e           = mkArg' Relevant e
 
471
mkArg e           = mkArg' defaultArgInfo e
426
472
 
427
473
 
428
474
-- | Parse a possibly dotted C.Expr as A.Expr.  Bool = True if dotted.
430
476
toAbstractDot prec e = do
431
477
    reportSLn "scope.irrelevance" 100 $ "toAbstractDot: " ++ (render $ pretty e)
432
478
    traceCall (ScopeCheckExpr e) $ case e of
433
 
    -- annotateExpr e = ScopedExpr <scope from Monad> e
 
479
 
434
480
      C.Dot _ e -> do
435
481
        e <- toAbstractCtx prec e
436
482
        return (e, True)
451
497
 
452
498
toAbstractLam :: Range -> [C.LamBinding] -> C.Expr -> Precedence -> ScopeM A.Expr
453
499
toAbstractLam r bs e ctx = do
454
 
        localToAbstract (map makeDomainFull bs) $ \bs ->
 
500
        localToAbstract (map (C.DomainFull . makeDomainFull) bs) $ \bs ->
455
501
          case bs of
456
502
            b:bs' -> do
457
503
              e        <- toAbstractCtx ctx e
465
511
instance ToAbstract C.Expr A.Expr where
466
512
  toAbstract e =
467
513
    traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
468
 
    -- annotateExpr e = ScopedExpr <scope from Monad> e
469
514
 
470
515
  -- Names
471
516
      Ident x -> toAbstract (OldQName x)
476
521
  -- Meta variables
477
522
      C.QuestionMark r n -> do
478
523
        scope <- getScope
479
 
        return $ A.QuestionMark $ MetaInfo
480
 
                    { metaRange  = r
481
 
                    , metaScope  = scope
482
 
                    , metaNumber = n
483
 
                    , metaNameSuggestion = ""
484
 
                    }
 
524
        -- Andreas, 2014-04-06 create interaction point.
 
525
        ii <- registerInteractionPoint r n
 
526
        let info = MetaInfo
 
527
             { metaRange  = r
 
528
             , metaScope  = scope
 
529
             , metaNumber = n
 
530
             , metaNameSuggestion = ""
 
531
             }
 
532
        return $ A.QuestionMark info ii
485
533
      C.Underscore r n -> do
486
534
        scope <- getScope
487
535
        return $ A.Underscore $ MetaInfo
488
536
                    { metaRange  = r
489
537
                    , metaScope  = scope
490
538
                    , metaNumber = maybe Nothing __IMPOSSIBLE__ n
491
 
                    , metaNameSuggestion = maybe "" id n
 
539
                    , metaNameSuggestion = fromMaybe "" n
492
540
                    }
493
541
 
494
542
  -- Raw application
495
543
      C.RawApp r es -> do
496
 
        e <- parseApplication es
 
544
        e <- reimburseTop Bench.Scoping $ billTo [Bench.Parsing, Bench.Operators] $
 
545
          parseApplication es
497
546
        toAbstract e
498
547
 
499
548
{- Andreas, 2010-09-06 STALE COMMENT
530
579
      C.Lam r bs e -> toAbstractLam r bs e TopCtx
531
580
 
532
581
  -- Extended Lambda
533
 
      C.ExtendedLam r cs -> do
 
582
      C.ExtendedLam r cs ->
 
583
        ifM isInsideDotPattern (typeError $ GenericError "Extended lambdas are not allowed in dot patterns") $ do
534
584
        cname <- nextlamname r 0 extendlambdaname
535
585
        name  <- freshAbstractName_ cname
536
586
        reportSLn "toabstract.extendlambda" 10 $ "new extended lambda name: " ++ show name
553
602
          where
554
603
            nextlamname :: Range -> Int -> String -> ScopeM C.Name
555
604
            nextlamname r i s = do
556
 
              let cname_pre = C.Name r [Id $ s ++ show i]
 
605
              let cname_pre = C.Name r [Id $ stringToRawName $ s ++ show i]
557
606
              rn <- resolveName (C.QName cname_pre)
558
607
              case rn of
559
608
                UnknownName -> return $ cname_pre
562
611
-- Irrelevant non-dependent function type
563
612
 
564
613
      C.Fun r e1 e2 -> do
565
 
        Arg h rel (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
566
 
        let e1 = Arg h (if dotted then Irrelevant else rel) e0
 
614
        Common.Arg info (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
 
615
        info <- toAbstract info
 
616
        let e1 = Common.Arg ((if dotted then setRelevance Irrelevant else id) info) e0
567
617
        e2 <- toAbstractCtx TopCtx e2
568
 
        let info = ExprRange r
569
 
        return $ A.Fun info e1 e2
 
618
        return $ A.Fun (ExprRange r) e1 e2
570
619
 
571
620
{-
572
621
-- Other function types
591
640
 
592
641
  -- Let
593
642
      e0@(C.Let _ ds e) ->
 
643
        ifM isInsideDotPattern (typeError $ GenericError $ "Let-expressions are not allowed in dot patterns") $
594
644
        localToAbstract (LetDefs ds) $ \ds' -> do
595
645
        e        <- toAbstractCtx TopCtx e
596
646
        let info = ExprRange (getRange e0)
618
668
      C.Absurd _ -> notAnExpression e
619
669
 
620
670
  -- Impossible things
621
 
      C.ETel _   -> __IMPOSSIBLE__
 
671
      C.ETel _  -> __IMPOSSIBLE__
 
672
      C.Equal{} -> typeError $ GenericError "Parse error: unexpected '='"
622
673
 
623
674
  -- Quoting
624
675
      C.QuoteGoal _ x e -> do
625
676
        x' <- toAbstract (NewName x)
626
677
        e' <- toAbstract e
627
678
        return $ A.QuoteGoal (ExprRange $ getRange e) x' e'
 
679
      C.QuoteContext _ x e -> do
 
680
        x' <- toAbstract (NewName x)
 
681
        e' <- toAbstract e
 
682
        return $ A.QuoteContext (ExprRange $ getRange e) x' e'
628
683
      C.Quote r -> return $ A.Quote (ExprRange r)
629
684
      C.QuoteTerm r -> return $ A.QuoteTerm (ExprRange r)
630
685
      C.Unquote r -> return $ A.Unquote (ExprRange r)
633
688
      C.DontCare e -> A.DontCare <$> toAbstract e
634
689
 
635
690
instance ToAbstract C.LamBinding A.LamBinding where
636
 
  toAbstract (C.DomainFree h rel x) = A.DomainFree h rel <$> toAbstract (NewName x)
637
 
  toAbstract (C.DomainFull tb)      = A.DomainFull <$> toAbstract tb
 
691
  toAbstract (C.DomainFree info x) = A.DomainFree <$> toAbstract info <*> toAbstract (NewName x)
 
692
  toAbstract (C.DomainFull tb)     = A.DomainFull <$> toAbstract tb
638
693
 
639
 
makeDomainFull :: C.LamBinding -> C.LamBinding
640
 
makeDomainFull b@C.DomainFull{} = b
641
 
makeDomainFull (C.DomainFree h rel x) =
642
 
  C.DomainFull $ C.TypedBindings r $ Arg h rel $ C.TBind r [x] $ C.Underscore r Nothing
 
694
makeDomainFull :: C.LamBinding -> C.TypedBindings
 
695
makeDomainFull (C.DomainFull b)      = b
 
696
makeDomainFull (C.DomainFree info x) =
 
697
  C.TypedBindings r $ Common.Arg info $ C.TBind r [x] $ C.Underscore r Nothing
643
698
  where r = getRange x
 
699
 
644
700
instance ToAbstract C.TypedBindings A.TypedBindings where
645
701
  toAbstract (C.TypedBindings r bs) = A.TypedBindings r <$> toAbstract bs
646
702
 
649
705
    t' <- toAbstractCtx TopCtx t
650
706
    xs' <- toAbstract (map NewName xs)
651
707
    return $ A.TBind r xs' t'
652
 
  toAbstract (C.TNoBind e) = do
653
 
    e <- toAbstractCtx TopCtx e
654
 
    return (A.TNoBind e)
 
708
  toAbstract (C.TLet r ds) = do
 
709
    ds' <- toAbstract (LetDefs ds)
 
710
    return $ A.TLet r ds'
 
711
 
 
712
-- | Scope check a module (top level function).
 
713
--
 
714
scopeCheckNiceModule
 
715
  :: Range
 
716
  -> Access
 
717
  -> C.Name
 
718
  -> C.Telescope
 
719
  -> ScopeM [A.Declaration]
 
720
  -> ScopeM [A.Declaration]
 
721
scopeCheckNiceModule r p name tel checkDs
 
722
  | telHasOpenStms tel = do
 
723
      -- Andreas, 2013-12-10:
 
724
      -- If the module telescope contains open statements,
 
725
      -- add an extra anonymous module around the current one.
 
726
      -- Otherwise, the open statements would create
 
727
      -- identifiers in the parent scope of the current module.
 
728
      -- But open statements in the module telescope should
 
729
      -- only affect the current module!
 
730
      scopeCheckNiceModule noRange p noName_ [] $
 
731
        scopeCheckNiceModule_
 
732
 
 
733
  | otherwise = do
 
734
        scopeCheckNiceModule_
 
735
  where
 
736
    -- The actual workhorse:
 
737
    scopeCheckNiceModule_ = do
 
738
 
 
739
      -- Check whether we are dealing with an anonymous module.
 
740
      -- This corresponds to a Coq/LEGO section.
 
741
      (name, p, open) <- do
 
742
        if isNoName name then do
 
743
          (i :: NameId) <- fresh
 
744
          return (C.NoName (getRange name) i, PrivateAccess, True)
 
745
         else return (name, p, False)
 
746
 
 
747
      -- Check and bind the module, using the supplied check for its contents.
 
748
      aname <- toAbstract (NewModuleName name)
 
749
      ds <- snd <$> do
 
750
        scopeCheckModule r (C.QName name) aname tel checkDs
 
751
      bindModule p name aname
 
752
 
 
753
      -- If the module was anonymous open it public.
 
754
      when open $
 
755
        openModule_ (C.QName name) $
 
756
          defaultImportDir { publicOpen = True }
 
757
      return ds
 
758
 
 
759
-- | Check whether a telescope has open declarations.
 
760
telHasOpenStms :: C.Telescope -> Bool
 
761
telHasOpenStms = any isOpenBinds
 
762
  where
 
763
    isOpenBinds (C.TypedBindings _ tb) = isOpenBind $ unArg tb
 
764
    isOpenBind C.TBind{}     = False
 
765
    isOpenBind (C.TLet _ ds) = any isOpen ds
 
766
    isOpen (C.ModuleMacro _ _ _ DoOpen _) = True
 
767
    isOpen C.Open{}          = True
 
768
    isOpen C.Import{}        = __IMPOSSIBLE__
 
769
    isOpen (C.Mutual   _ ds) = any isOpen ds
 
770
    isOpen (C.Abstract _ ds) = any isOpen ds
 
771
    isOpen (C.Private  _ ds) = any isOpen ds
 
772
    isOpen   _               = False
 
773
 
 
774
{- UNUSED
 
775
telHasLetStms :: C.Telescope -> Bool
 
776
telHasLetStms = any isLetBinds
 
777
  where
 
778
    isLetBinds (C.TypedBindings _ tb) = isLetBind $ unArg tb
 
779
    isLetBind C.TBind{} = False
 
780
    isLetBind C.TLet{}  = True
 
781
-}
 
782
 
 
783
-- | We for now disallow let-bindings in @data@ and @record@ telescopes.
 
784
--   This due "nested datatypes"; there is no easy interpretation of
 
785
--   @
 
786
--      data D (A : Set) (open M A) (b : B) : Set where
 
787
--        c : D (A × A) b → D A b
 
788
--   @
 
789
--   where @B@ is brought in scope by @open M A@.
 
790
 
 
791
class EnsureNoLetStms a where
 
792
  ensureNoLetStms :: a -> ScopeM ()
 
793
 
 
794
{- From ghc 7.2, there is LANGUAGE DefaultSignatures
 
795
  default ensureNoLetStms :: Foldable t => t a -> ScopeM ()
 
796
  ensureNoLetStms = traverse_ ensureNoLetStms
 
797
-}
 
798
 
 
799
instance EnsureNoLetStms C.TypedBinding where
 
800
  ensureNoLetStms tb =
 
801
    case tb of
 
802
      C.TLet{}  -> typeError $ IllegalLetInTelescope tb
 
803
      C.TBind{} -> return ()
 
804
 
 
805
instance EnsureNoLetStms a => EnsureNoLetStms (LamBinding' a) where
 
806
  ensureNoLetStms = traverse_ ensureNoLetStms
 
807
 
 
808
instance EnsureNoLetStms a => EnsureNoLetStms (TypedBindings' a) where
 
809
  ensureNoLetStms = traverse_ ensureNoLetStms
 
810
 
 
811
instance EnsureNoLetStms a => EnsureNoLetStms [a] where
 
812
  ensureNoLetStms = traverse_ ensureNoLetStms
 
813
 
655
814
 
656
815
-- | Returns the scope inside the checked module.
657
 
scopeCheckModule :: Range -> C.QName -> A.ModuleName -> C.Telescope -> [C.Declaration] ->
658
 
                    ScopeM (ScopeInfo, [A.Declaration])
659
 
scopeCheckModule r x qm tel ds = do
 
816
scopeCheckModule
 
817
  :: Range
 
818
  -> C.QName                 -- ^ The concrete name of the module.
 
819
  -> A.ModuleName            -- ^ The abstract name of the module.
 
820
  -> C.Telescope             -- ^ The module telescope.
 
821
  -> ScopeM [A.Declaration]  -- ^ The code for checking the module contents.
 
822
  -> ScopeM (ScopeInfo, [A.Declaration])
 
823
scopeCheckModule r x qm tel checkDs = do
660
824
  printScope "module" 20 $ "checking module " ++ show x
661
 
  res <- withCurrentModule qm $ do
662
 
    -- pushScope m
663
 
    -- qm <- getCurrentModule
664
 
    printScope "module" 20 $ "inside module " ++ show x
665
 
    withLocalVars $ do
666
 
      tel   <- toAbstract tel
667
 
      ds    <- (:[]) . A.Section info (qm `withRangesOfQ` x) tel <$>
668
 
                 toAbstract ds
 
825
  -- Andreas, 2013-12-10: Telescope does not live in the new module
 
826
  -- but its parent, so check it before entering the new module.
 
827
  -- This is important for Nicolas Pouillard's open parametrized modules
 
828
  -- statements inside telescopes.
 
829
  res <- withLocalVars $ do
 
830
    tel <- toAbstract tel
 
831
    withCurrentModule qm $ do
 
832
      -- pushScope m
 
833
      -- qm <- getCurrentModule
 
834
      printScope "module" 20 $ "inside module " ++ show x
 
835
      ds    <- checkDs
669
836
      scope <- getScope
670
 
      return (scope, ds)
 
837
      return (scope, [ A.Section info (qm `withRangesOfQ` x) tel ds ])
671
838
 
672
839
  -- Binding is done by the caller
673
840
  printScope "module" 20 $ "after module " ++ show x
675
842
  where
676
843
    info = ModuleInfo r noRange Nothing Nothing Nothing
677
844
 
678
 
newtype TopLevel a = TopLevel a
 
845
-- | Temporary data type to scope check a file.
 
846
data TopLevel a = TopLevel
 
847
  { topLevelPath           :: AbsolutePath
 
848
    -- ^ The file path from which we loaded this module.
 
849
  , topLevelTheThing       :: a
 
850
    -- ^ The file content.
 
851
  }
679
852
 
680
853
data TopLevelInfo = TopLevelInfo
681
854
        { topLevelDecls :: [A.Declaration]
690
863
 
691
864
-- Top-level declarations are always (import|open)* module
692
865
instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
693
 
    toAbstract (TopLevel ds) = case splitAt (length ds - 1) ds of
694
 
        (ds', [C.Module r m tel ds]) -> do
 
866
    toAbstract (TopLevel file ds) =
 
867
      -- A file is a bunch of preliminary decls (imports etc.)
 
868
      -- plus a single module decl.
 
869
      case splitAt (length ds - 1) ds of
 
870
        (ds', [C.Module r m0 tel ds]) -> do
 
871
          -- If the module name is _ compute the name from the file path
 
872
          m <- if isNoName m0
 
873
                then return $ C.QName $ C.Name noRange [Id $ stringToRawName $ rootName file]
 
874
                else do
 
875
                -- Andreas, 2014-03-28  Issue 1078
 
876
                -- We need to check the module name against the file name here.
 
877
                -- Otherwise one could sneak in a lie and confuse the scope
 
878
                -- checker.
 
879
                  checkModuleName (C.toTopLevelModuleName m0) file
 
880
                  return m0
695
881
          setTopLevelModule m
696
882
          am           <- toAbstract (NewModuleQName m)
697
883
          ds'          <- toAbstract ds'
698
 
          (scope0, ds) <- scopeCheckModule r m am tel ds
 
884
          (scope0, ds) <- scopeCheckModule r m am tel $ toAbstract ds
699
885
          scope        <- getScope
700
886
          return $ TopLevelInfo (ds' ++ ds) scope scope0
701
887
        _ -> __IMPOSSIBLE__
726
912
instance ToAbstract LetDef [A.LetBinding] where
727
913
    toAbstract (LetDef d) =
728
914
        case d of
729
 
            NiceMutual _ _ d@[C.FunSig _ fx _ rel _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
 
915
            NiceMutual _ _ d@[C.FunSig _ fx _ info _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
730
916
                do  when (abstract == AbstractDef) $ do
731
917
                      typeError $ GenericError $ "abstract not allowed in let expressions"
732
918
                    e <- letToAbstract cl
733
919
                    t <- toAbstract t
734
 
                    x <- toAbstract (NewName $ C.BName x fx)
735
 
                    return [ A.LetBind (LetRange $ getRange d) rel x t e ]
 
920
                    x <- toAbstract (NewName $ mkBoundName x fx)
 
921
                    info <- toAbstract info
 
922
                    return [ A.LetBind (LetRange $ getRange d) info x t e ]
736
923
 
737
924
            -- irrefutable let binding, like  (x , y) = rhs
738
 
            NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause (C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
739
 
              rhs <- toAbstract rhs
740
 
              p   <- parsePattern p
741
 
              p   <- toAbstract p
742
 
              checkPatternLinearity [p]
743
 
              p   <- toAbstract p
744
 
              return [ A.LetPatBind (LetRange r) p rhs ]
 
925
            NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause lhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
 
926
              mp  <- setCurrentRange (getRange p) $ (Right <$> parsePattern p) `catchError` (return . Left)
 
927
              case mp of
 
928
                Right p -> do
 
929
                  rhs <- toAbstract rhs
 
930
                  p   <- toAbstract p
 
931
                  checkPatternLinearity [p]
 
932
                  p   <- toAbstract p
 
933
                  return [ A.LetPatBind (LetRange r) p rhs ]
 
934
                -- It's not a record pattern, so it should be a prefix left-hand side
 
935
                Left err ->
 
936
                  case definedName p of
 
937
                    Nothing -> throwError err
 
938
                    Just x  -> toAbstract $ LetDef $ NiceMutual r termCheck
 
939
                      [ C.FunSig r defaultFixity' PublicAccess defaultArgInfo termCheck x (C.Underscore (getRange x) Nothing)
 
940
                      , C.FunDef r __IMPOSSIBLE__ __IMPOSSIBLE__ ConcreteDef __IMPOSSIBLE__ __IMPOSSIBLE__
 
941
                        [C.Clause x lhs (C.RHS rhs) NoWhere []]
 
942
                      ]
 
943
                  where
 
944
                    definedName (C.IdentP (C.QName x)) = Just x
 
945
                    definedName C.IdentP{}             = Nothing
 
946
                    definedName (C.RawAppP _ (p : _))  = definedName p
 
947
                    definedName (C.ParenP _ p)         = definedName p
 
948
                    definedName C.WildP{}              = Nothing   -- for instance let _ + x = x in ... (not allowed)
 
949
                    definedName C.AbsurdP{}            = Nothing
 
950
                    definedName C.AsP{}                = Nothing
 
951
                    definedName C.DotP{}               = Nothing
 
952
                    definedName C.LitP{}               = Nothing
 
953
                    definedName C.HiddenP{}            = __IMPOSSIBLE__
 
954
                    definedName C.InstanceP{}          = __IMPOSSIBLE__
 
955
                    definedName C.RawAppP{}            = __IMPOSSIBLE__
 
956
                    definedName C.AppP{}               = __IMPOSSIBLE__
 
957
                    definedName C.OpAppP{}             = __IMPOSSIBLE__
745
958
 
746
959
            -- You can't open public in a let
747
960
            NiceOpen r x dirs | not (C.publicOpen dirs) -> do
758
971
                                m
759
972
                     ]
760
973
 
761
 
            NiceModuleMacro r p a x modapp open dir | not (C.publicOpen dir) ->
 
974
            NiceModuleMacro r p x modapp open dir | not (C.publicOpen dir) ->
762
975
              checkModuleMacro LetApply r p x modapp open dir
763
976
 
764
977
            _   -> notAValidLetBinding d
769
982
                localToAbstract (snd $ lhsArgs p) $ \args ->
770
983
-}
771
984
                (x, args) <- do
772
 
                  res <- parseLHS top p
 
985
                  res <- setCurrentRange (getRange p) $ parseLHS top p
773
986
                  case res of
774
987
                    C.LHSHead x args -> return (x, args)
775
988
                    C.LHSProj{} -> typeError $ GenericError $ "copatterns not allowed in let bindings"
780
993
            letToAbstract _ = notAValidLetBinding d
781
994
 
782
995
            -- Named patterns not allowed in let definitions
783
 
            lambda e (Arg h rel (Named Nothing (A.VarP x))) = return $ A.Lam i (A.DomainFree h rel x) e
 
996
            lambda e (Common.Arg info (Named Nothing (A.VarP x))) =
 
997
                    return $ A.Lam i (A.DomainFree info x) e
784
998
                where
785
999
                    i = ExprRange (fuseRange x e)
786
 
            lambda e (Arg h rel (Named Nothing (A.WildP i))) =
 
1000
            lambda e (Common.Arg info (Named Nothing (A.WildP i))) =
787
1001
                do  x <- freshNoName (getRange i)
788
 
                    return $ A.Lam i' (A.DomainFree h rel x) e
 
1002
                    return $ A.Lam i' (A.DomainFree info x) e
789
1003
                where
790
1004
                    i' = ExprRange (fuseRange i e)
791
1005
            lambda _ _ = notAValidLetBinding d
792
1006
 
 
1007
newtype Blind a = Blind { unBlind :: a }
 
1008
 
 
1009
instance ToAbstract (Blind a) (Blind a) where
 
1010
  toAbstract = return
 
1011
 
793
1012
-- The only reason why we return a list is that open declarations disappears.
794
1013
-- For every other declaration we get a singleton list.
795
1014
instance ToAbstract NiceDeclaration A.Declaration where
798
1017
    traceCall (ScopeCheckDeclaration d) $
799
1018
    case d of
800
1019
 
801
 
  -- Axiom
 
1020
  -- Axiom (actual postulate)
802
1021
    C.Axiom r f p rel x t -> do
803
1022
      -- check that we do not postulate in --safe mode
804
1023
      clo <- commandLineOptions
805
1024
      when (optSafe clo) (typeError (SafeFlagPostulate x))
806
1025
      -- check the postulate
807
 
      toAbstractNiceAxiom d
 
1026
      toAbstractNiceAxiom A.NoFunSig d
808
1027
 
809
1028
  -- Fields
810
1029
    C.NiceField r f p a x t -> do
811
1030
      unless (p == PublicAccess) $ typeError $ GenericError "Record fields can not be private"
812
 
      t' <- toAbstractCtx TopCtx t
 
1031
      -- Interaction points for record fields have already been introduced
 
1032
      -- when checking the type of the record constructor.
 
1033
      -- To avoid introducing interaction points (IP) twice, we turn
 
1034
      -- all question marks to underscores.  (See issue 1138.)
 
1035
      let maskIP (C.QuestionMark r _) = C.Underscore r Nothing
 
1036
          maskIP e                     = e
 
1037
      t' <- toAbstractCtx TopCtx $ mapExpr maskIP t
813
1038
      y  <- freshAbstractQName f x
814
1039
      irrProj <- optIrrelevantProjections <$> pragmaOptions
815
 
      unless (argRelevance t == Irrelevant && not irrProj) $
 
1040
      unless (isIrrelevant t && not irrProj) $
816
1041
        -- Andreas, 2010-09-24: irrelevant fields are not in scope
817
1042
        -- this ensures that projections out of irrelevant fields cannot occur
818
1043
        -- Ulf: unless you turn on --irrelevant-projections
831
1056
      ds' <- toAbstract ds
832
1057
      return [ A.Mutual (MutualInfo termCheck r) ds' ]
833
1058
 
834
 
    C.NiceRecSig r f a x ls t -> withLocalVars $ do
835
 
        let toTypeBinding :: C.LamBinding -> C.TypedBindings
836
 
            toTypeBinding b = case makeDomainFull b of
837
 
               C.DomainFull b -> b
838
 
               _            -> __IMPOSSIBLE__
839
 
        ls' <- toAbstract (map toTypeBinding ls)
 
1059
    C.NiceRecSig r f a x ls t -> do
 
1060
      ensureNoLetStms ls
 
1061
      withLocalVars $ do
 
1062
        ls' <- toAbstract (map makeDomainFull ls)
840
1063
        x'  <- freshAbstractQName f x
841
1064
        bindName a DefName x x'
842
1065
        t' <- toAbstract t
843
1066
        return [ A.RecSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
 
1067
 
844
1068
    C.NiceDataSig r f a x ls t -> withLocalVars $ do
845
1069
        printScope "scope.data.sig" 20 ("checking DataSig for " ++ show x)
846
 
        let toTypeBinding :: C.LamBinding -> C.TypedBindings
847
 
            toTypeBinding b = case makeDomainFull b of
848
 
               C.DomainFull b -> b
849
 
               _            -> __IMPOSSIBLE__
850
 
        ls' <- toAbstract (map toTypeBinding ls)
 
1070
        ensureNoLetStms ls
 
1071
        ls' <- toAbstract (map makeDomainFull ls)
851
1072
        x'  <- freshAbstractQName f x
852
1073
        {- -- Andreas, 2012-01-16: remember number of parameters
853
1074
        bindName a (DataName (length ls)) x x' -}
855
1076
        t' <- toAbstract t
856
1077
        return [ A.DataSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
857
1078
  -- Type signatures
858
 
    C.FunSig r f p rel tc x t -> toAbstractNiceAxiom (C.Axiom r f p rel x t)
 
1079
    C.FunSig r f p rel tc x t -> toAbstractNiceAxiom A.FunSig (C.Axiom r f p rel x t)
859
1080
  -- Function definitions
860
1081
    C.FunDef r ds f a tc x cs -> do
861
1082
        printLocals 10 $ "checking def " ++ show x
862
1083
        (x',cs) <- toAbstract (OldName x,cs)
863
 
        (delayed, cs) <- translateCopatternClauses cs
 
1084
        let delayed = NotDelayed
 
1085
        -- (delayed, cs) <- translateCopatternClauses cs -- TODO
864
1086
        return [ A.FunDef (mkDefInfo x f PublicAccess a r) x' delayed cs ]
865
1087
 
866
1088
  -- Uncategorized function clauses
872
1094
  -- Data definitions
873
1095
    C.DataDef r f a x pars cons -> withLocalVars $ do
874
1096
        printScope "scope.data.def" 20 ("checking DataDef for " ++ show x)
 
1097
        ensureNoLetStms pars
875
1098
        -- Check for duplicate constructors
876
1099
        do let cs   = map conName cons
877
1100
               dups = nub $ cs \\ nub cs
898
1121
        conName _ = __IMPOSSIBLE__
899
1122
 
900
1123
  -- Record definitions (mucho interesting)
901
 
    C.RecDef r f a x ind cm pars fields ->
 
1124
    C.RecDef r f a x ind cm pars fields -> do
 
1125
      ensureNoLetStms pars
902
1126
      withLocalVars $ do
903
1127
        -- Check that the generated module doesn't clash with a previously
904
1128
        -- defined module
906
1130
        pars   <- toAbstract pars
907
1131
        DefinedName p ax <- resolveName (C.QName x)
908
1132
        let x' = anameName ax
 
1133
        -- We scope check the fields a first time when putting together
 
1134
        -- the type of the constructor.
909
1135
        contel <- toAbstract $ recordConstructorType fields
910
1136
        m0     <- getCurrentModule
911
1137
        let m = A.qualifyM m0 $ mnameFromList $ (:[]) $ last $ qnameToList x'
912
1138
        printScope "rec" 15 "before record"
913
1139
        createModule False m
 
1140
        -- We scope check the fields a second time, as actual fields.
914
1141
        afields <- withCurrentModule m $ do
915
1142
          afields <- toAbstract fields
916
1143
          printScope "rec" 15 "checked fields"
920
1147
        printScope "rec" 15 "record complete"
921
1148
        return [ A.RecDef (mkDefInfo x f PublicAccess a r) x' ind cm' pars contel afields ]
922
1149
 
923
 
    -- Andreas, 2012-10-30 anonymous modules are like Coq sections
924
 
    NiceModule r p a (C.QName name) tel ds ->
925
 
      traceCall (ScopeCheckDeclaration $ NiceModule r p a (C.QName name) tel []) $ do
926
 
      (name, p, isSection) <- if not (C.isNoName name)
927
 
        then return (name, p, False)
928
 
        else do
929
 
          (i :: NameId) <- fresh
930
 
          return (C.NoName (getRange name) i, PrivateAccess, True)
931
 
      aname <- toAbstract (NewModuleName name)
932
 
      ds <- snd <$> scopeCheckModule r (C.QName name) aname tel ds
933
 
      bindModule p name aname
934
 
      -- if the module was anonymous open it public
935
 
      when isSection $
936
 
        openModule_ (C.QName name) $
937
 
          defaultImportDir { publicOpen = True }
938
 
      return ds
939
 
 
940
 
    NiceModule _ _ _ C.Qual{} _ _ -> __IMPOSSIBLE__
941
 
 
942
 
    NiceModuleMacro r p a x modapp open dir ->
 
1150
    NiceModule r p a x@(C.QName name) tel ds ->
 
1151
      traceCall (ScopeCheckDeclaration $ NiceModule r p a x tel []) $ do
 
1152
        scopeCheckNiceModule r p name tel $ toAbstract ds
 
1153
 
 
1154
    NiceModule _ _ _ m@C.Qual{} _ _ ->
 
1155
      typeError $ GenericError $ "Local modules cannot have qualified names"
 
1156
 
 
1157
    NiceModuleMacro r p x modapp open dir ->
943
1158
      checkModuleMacro Apply r p x modapp open dir
944
1159
 
945
1160
    NiceOpen r x dir -> do
979
1194
        return (m, Map.delete noModuleName i)
980
1195
 
981
1196
      -- Merge the imported scopes with the current scopes
982
 
      modifyScopeInfo $ \s -> s { scopeModules = Map.unionWith mergeScope
983
 
                                                  (Map.delete m $ scopeModules s) i }
 
1197
      modifyScopes $ \ ms -> Map.unionWith mergeScope (Map.delete m ms) i
984
1198
 
985
1199
      -- Bind the desired module name to the right abstract name.
986
1200
      case as of
1013
1227
    NicePatternSyn r fx n as p -> do
1014
1228
      reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ show r
1015
1229
 
1016
 
      isparameterised <- not . null <$> getLocalVars
1017
 
      when isparameterised $ typeError $ NotSupported
1018
 
          "pattern synonym in parameterised module"
1019
 
 
1020
1230
      y <- freshAbstractQName fx n
1021
1231
      bindName PublicAccess PatternSynName n y
1022
 
      defn <- withLocalVars $ do
1023
 
               p'   <- killRange <$> (toAbstract =<< toAbstract =<< parsePatternSyn p)
1024
 
               as'  <- mapM (\a -> unVarName =<< resolveName (C.QName a)) as
1025
 
               return (as', p')
 
1232
      defn@(as, p) <- withLocalVars $ do
 
1233
         p  <- toAbstract =<< toAbstract =<< parsePatternSyn p
 
1234
         as <- (traverse . mapM) (unVarName <=< resolveName . C.QName) as
 
1235
         as <- (map . fmap) unBlind <$> toAbstract ((map . fmap) Blind as)
 
1236
         return (as, p)
1026
1237
      modifyPatternSyns (Map.insert y defn)
1027
 
      return []
 
1238
      return [A.PatternSynDef y as p]   -- only for highlighting
1028
1239
      where unVarName (VarName a) = return a
1029
1240
            unVarName _           = typeError $ UnusedVariableInPatternSynonym
1030
1241
 
1031
1242
    where
1032
1243
      -- checking postulate or type sig. without checking safe flag
1033
 
      toAbstractNiceAxiom (C.Axiom r f p rel x t) = do
 
1244
      toAbstractNiceAxiom funSig (C.Axiom r f p info x t) = do
1034
1245
        t' <- toAbstractCtx TopCtx t
1035
1246
        y  <- freshAbstractQName f x
 
1247
        info <- toAbstract info
1036
1248
        bindName p DefName x y
1037
 
        return [ A.Axiom (mkDefInfo x f p ConcreteDef r) rel y t' ]
1038
 
      toAbstractNiceAxiom _ = __IMPOSSIBLE__
 
1249
        return [ A.Axiom funSig (mkDefInfo x f p ConcreteDef r) info y t' ]
 
1250
      toAbstractNiceAxiom _ _ = __IMPOSSIBLE__
1039
1251
 
1040
1252
 
1041
1253
data IsRecordCon = YesRec | NoRec
1060
1272
            _                -> PublicAccess
1061
1273
 
1062
1274
instance ToAbstract ConstrDecl A.Declaration where
1063
 
  toAbstract (ConstrDecl record m a p (C.Axiom r f _ rel x t)) = do -- rel==Relevant
 
1275
  toAbstract (ConstrDecl record m a p (C.Axiom r f _ info x t)) = do -- rel==Relevant
1064
1276
    t' <- toAbstractCtx TopCtx t
1065
1277
    -- The abstract name is the qualified one
1066
1278
    -- Bind it twice, once unqualified and once qualified
1067
1279
    y <- bindConstructorName m x f a p record
 
1280
    info <- toAbstract info
1068
1281
    printScope "con" 15 "bound constructor"
1069
 
    return $ A.Axiom (mkDefInfo x f p ConcreteDef r) rel y t'
 
1282
    return $ A.Axiom NoFunSig (mkDefInfo x f p ConcreteDef r) info y t'
1070
1283
 
1071
1284
  toAbstract _ = __IMPOSSIBLE__    -- a constructor is always an axiom
1072
1285
 
1090
1303
            A.Con _ -> fail "Use COMPILED_DATA for constructors" -- TODO
1091
1304
            _       -> __IMPOSSIBLE__
1092
1305
      return [ A.CompiledPragma y hs ]
 
1306
    toAbstract (C.CompiledExportPragma _ x hs) = do
 
1307
      e <- toAbstract $ OldQName x
 
1308
      y <- case e of
 
1309
            A.Def x -> return x
 
1310
            --A.Con x -> return x
 
1311
            _       -> __IMPOSSIBLE__
 
1312
      return [ A.CompiledExportPragma y hs ]
1093
1313
    toAbstract (C.CompiledEpicPragma _ x ep) = do
1094
1314
      e <- toAbstract $ OldQName x
1095
1315
      y <- case e of
1127
1347
instance ToAbstract C.Clause A.Clause where
1128
1348
    toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
1129
1349
    toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
1130
1350
      -- Andreas, 2012-02-14: need to reset local vars before checking subclauses
1131
1351
      vars <- getLocalVars
1132
 
      let wcs' = map (\ c -> setLocalVars vars >> do return $ expandEllipsis p wps c) wcs
 
1352
      let wcs' = for wcs $ \ c -> do
 
1353
           setLocalVars vars
 
1354
           return $ expandEllipsis p wps c
1133
1355
      lhs' <- toAbstract (LeftHandSide top p wps)
1134
1356
      printLocals 10 "after lhs:"
1135
1357
      let (whname, whds) = case wh of
1154
1375
  return (x, [])
1155
1376
whereToAbstract r whname whds inner = do
1156
1377
  m <- maybe (nameConcrete <$> freshNoName noRange) return whname
 
1378
  m <- if (maybe False isNoName whname)
 
1379
       then do
 
1380
         (i :: NameId) <- fresh
 
1381
         return (C.NoName (getRange m) i)
 
1382
       else return m
1157
1383
  let acc = maybe PrivateAccess (const PublicAccess) whname  -- unnamed where's are private
1158
1384
  let tel = []
1159
1385
  old <- getCurrentModule
1160
1386
  am  <- toAbstract (NewModuleName m)
1161
 
  (scope, ds) <- scopeCheckModule r (C.QName m) am tel whds
 
1387
  (scope, ds) <- scopeCheckModule r (C.QName m) am tel $ toAbstract whds
1162
1388
  setScope scope
1163
1389
  x <- inner
1164
1390
  setCurrentModule old
1165
1391
  bindModule acc m am
 
1392
  -- Issue 848: if the module was anonymous (module _ where) open it public
 
1393
  when (maybe False isNoName whname) $
 
1394
    openModule_ (C.QName m) $
 
1395
      defaultImportDir { publicOpen = True }
1166
1396
  return (x, ds)
1167
1397
 
1168
1398
data RightHandSide = RightHandSide
1267
1497
        args2 <- toAbstract ps2
1268
1498
        return $ A.LHSProj d args1 l args2
1269
1499
 
1270
 
instance ToAbstract c a => ToAbstract (Arg c) (Arg a) where
1271
 
    toAbstract (Arg h r e) = Arg h r <$> toAbstractCtx (hiddenArgumentCtx h) e
 
1500
instance ToAbstract c a => ToAbstract (C.Arg c) (A.Arg a) where
 
1501
    toAbstract (Common.Arg info e) =
 
1502
        Common.Arg <$> toAbstract info <*> toAbstractCtx (hiddenArgumentCtx $ getHiding info) e
1272
1503
 
1273
1504
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
1274
1505
    toAbstract (Named n e) = Named n <$> toAbstract e
1283
1514
    toAbstract (A.LHSProj d ps lhscore ps') = A.LHSProj d <$> mapM toAbstract ps
1284
1515
      <*> mapM toAbstract lhscore <*> mapM toAbstract ps'
1285
1516
 
 
1517
instance ToAbstract c a => ToAbstract (A.NamedArg c) (A.NamedArg a) where
 
1518
    toAbstract (Common.Arg info c) = liftM2 Common.Arg (return info) (toAbstract c)
 
1519
 
 
1520
instance ToAbstract C.ArgInfo A.ArgInfo where
 
1521
    toAbstract info = do cs <- mapM toAbstract $ argInfoColors info
 
1522
                         return $ info { argInfoColors = cs }
 
1523
 
1286
1524
-- Patterns are done in two phases. First everything but the dot patterns, and
1287
1525
-- then the dot patterns. This is because dot patterns can refer to variables
1288
1526
-- bound anywhere in the pattern.
1293
1531
    toAbstract (A.DefP i x as)        = A.DefP i x <$> mapM toAbstract as
1294
1532
    toAbstract (A.WildP i)            = return $ A.WildP i
1295
1533
    toAbstract (A.AsP i x p)          = A.AsP i x <$> toAbstract p
1296
 
    toAbstract (A.DotP i e)           = A.DotP i <$> toAbstract e
 
1534
    toAbstract (A.DotP i e)           = A.DotP i <$> insideDotPattern (toAbstract e)
1297
1535
    toAbstract (A.AbsurdP i)          = return $ A.AbsurdP i
1298
1536
    toAbstract (A.LitP l)             = return $ A.LitP l
1299
1537
    toAbstract (A.ImplicitP i)        = return $ A.ImplicitP i
1300
 
    toAbstract (A.PatternSynP i x as) = do
1301
 
        p   <- lookupPatternSyn x
1302
 
        as' <- mapM toAbstract as
1303
 
        instPatternSyn p as'
1304
 
      where
1305
 
        instPatternSyn :: A.PatternSynDefn -> [NamedArg A.Pattern] -> ScopeM A.Pattern
1306
 
        instPatternSyn (ns, p) as
1307
 
            | length ns == length as = return $ substPattern s $ setRange (getRange i) p
1308
 
            | otherwise              = typeError $ PatternSynonymArityMismatch x
1309
 
          where
1310
 
          s = zipWith' (\n a -> (n, namedThing (unArg a))) ns as
1311
 
 
 
1538
    toAbstract (A.PatternSynP i x as) = A.PatternSynP i x <$> mapM toAbstract as
1312
1539
 
1313
1540
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
1314
1541
 
1316
1543
        px <- toAbstract (PatName x)
1317
1544
        case px of
1318
1545
            VarPatName y        -> return $ VarP y
1319
 
            ConPatName ds       -> return $ ConP (PatRange (getRange p))
 
1546
            ConPatName ds       -> return $ ConP (ConPatInfo False $ PatRange (getRange p))
1320
1547
                                                 (AmbQ $ map anameName ds)
1321
1548
                                                 []
1322
1549
            PatternSynPatName d -> return $ PatternSynP (PatRange (getRange p))
1325
1552
    toAbstract p0@(AppP p q) = do
1326
1553
        (p', q') <- toAbstract (p,q)
1327
1554
        case p' of
1328
 
            ConP _ x as        -> return $ ConP info x (as ++ [q'])
 
1555
            ConP i x as        -> return $ ConP (i {patInfo = info}) x (as ++ [q'])
1329
1556
            DefP _ x as        -> return $ DefP info x (as ++ [q'])
1330
1557
            PatternSynP _ x as -> return $ PatternSynP info x (as ++ [q'])
1331
1558
            _                  -> typeError $ InvalidPattern p0
1337
1564
        p <- toAbstract (IdentP op)
1338
1565
        ps <- toAbstract ps
1339
1566
        case p of
1340
 
          ConP        _ x as -> return $ ConP info x
1341
 
                                    (as ++ map (Arg NotHidden Relevant . unnamed) ps)
 
1567
          ConP        i x as -> return $ ConP (i {patInfo = info}) x
 
1568
                                    (as ++ ps)
1342
1569
          DefP        _ x as -> return $ DefP info x
1343
 
                                    (as ++ map (Arg NotHidden Relevant . unnamed) ps)
 
1570
                                    (as ++ ps)
1344
1571
          PatternSynP _ x as -> return $ PatternSynP info x
1345
 
                                    (as ++ map (Arg NotHidden Relevant . unnamed) ps)
 
1572
                                    (as ++ ps)
1346
1573
          _                  -> __IMPOSSIBLE__
1347
1574
        where
1348
1575
            r    = getRange p0
1372
1599
 
1373
1600
-- | Turn an operator application into abstract syntax. Make sure to record the
1374
1601
-- right precedences for the various arguments.
1375
 
toAbstractOpApp :: C.QName -> [OpApp C.Expr] -> ScopeM A.Expr
 
1602
toAbstractOpApp :: C.QName -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
1376
1603
toAbstractOpApp op es = do
1377
1604
    f  <- getFixity op
1378
1605
    let (_,_,parts) = oldToNewNotation $ (op, f)
1379
1606
    op <- toAbstract (OldQName op)
1380
1607
    foldl' app op <$> left (theFixity f) [p | p <- parts, not (isBindingHole p)] es
1381
1608
    where
1382
 
        app e arg = A.App (ExprRange (fuseRange e arg)) e
1383
 
                  $ Arg NotHidden Relevant $ unnamed arg
 
1609
        app e arg = A.App (ExprRange (fuseRange e arg)) e (setArgColors [] arg)
 
1610
 
 
1611
        toAbsOpArg cxt = traverse $ traverse $ toAbstractOpArg cxt
1384
1612
 
1385
1613
        left f (IdPart _ : xs) es = inside f xs es
1386
1614
        left f (_ : xs) (e : es) = do
1387
 
            e  <- toAbstractOpArg (LeftOperandCtx f) e
 
1615
            e  <- toAbsOpArg (LeftOperandCtx f) e
1388
1616
            es <- inside f xs es
1389
1617
            return (e : es)
1390
1618
        left f (_  : _)  [] = __IMPOSSIBLE__
1391
1619
        left f []        _  = __IMPOSSIBLE__
1392
1620
 
1393
 
        inside f [x]          es       = right f x es
1394
 
        inside f (IdPart _ : xs) es       = inside f xs es
 
1621
        inside f [x]          es    = right f x es
 
1622
        inside f (IdPart _ : xs) es = inside f xs es
1395
1623
        inside f (_  : xs) (e : es) = do
1396
 
            e  <- toAbstractOpArg InsideOperandCtx e
 
1624
            e  <- toAbsOpArg InsideOperandCtx e
1397
1625
            es <- inside f xs es
1398
1626
            return (e : es)
1399
1627
        inside _ (_ : _) [] = __IMPOSSIBLE__
1401
1629
 
1402
1630
        right _ (IdPart _)  [] = return []
1403
1631
        right f _          [e] = do
1404
 
            e <- toAbstractOpArg (RightOperandCtx f) e
 
1632
            e <- toAbsOpArg (RightOperandCtx f) e
1405
1633
            return [e]
1406
1634
        right _ _     _  = __IMPOSSIBLE__