{-# LANGUAGE CPP, MultiParamTypeClasses, FunctionalDependencies,
             FlexibleInstances, UndecidableInstances, OverlappingInstances,
             ScopedTypeVariables, TypeSynonymInstances
  #-}

{-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,
    figuring out infix operator precedences and tidying up definitions.
-}
module Agda.Syntax.Translation.ConcreteToAbstract
    ( ToAbstract(..), localToAbstract
    , concreteToAbstract_
    , concreteToAbstract
    , NewModuleQName(..)
    , OldName(..)
    , TopLevel(..)
    , TopLevelInfo(..)
    , topLevelModuleName
    , AbstractRHS
    , NewModuleName, OldModuleName
    , NewName, OldQName
    , LeftHandSide, RightHandSide
    , PatName, APatName, LetDef, LetDefs
    ) where

import Prelude hiding (mapM)
import Control.Applicative
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Error hiding (mapM)

import Data.Foldable (Foldable, traverse_)
import Data.Traversable (mapM, traverse)
import Data.List ((\\), nub, foldl')
import qualified Data.Map as Map
import Data.Maybe

import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Generic
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Abstract as A
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Info
import Agda.Syntax.Concrete.Definitions as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad

import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
                                     TCErr(..), extendlambdaname)
import Agda.TypeChecking.Monad.Benchmark (billTo, billTop, reimburseTop)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Env (insideDotPattern, isInsideDotPattern)

import Agda.Interaction.FindFile (checkModuleName)
-- import Agda.Interaction.Imports  -- for type-checking in ghci
import {-# SOURCE #-} Agda.Interaction.Imports (scopeCheckImport)
import Agda.Interaction.Options

import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Fresh
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Pretty

#include "../../undefined.h"
import Agda.Utils.Impossible
import Agda.ImpossibleTest (impossibleTest)

{--------------------------------------------------------------------------
    Exceptions
 --------------------------------------------------------------------------}

notAModuleExpr e            = typeError $ NotAModuleExpr e
notAnExpression e           = typeError $ NotAnExpression e
notAValidLetBinding d       = typeError $ NotAValidLetBinding d
nothingAppliedToHiddenArg e = typeError $ NothingAppliedToHiddenArg e
nothingAppliedToInstanceArg e = typeError $ NothingAppliedToInstanceArg e

-- Debugging

printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
  locals <- getLocalVars
  reportSLn "scope.top" v $ s ++ " " ++ show locals

{--------------------------------------------------------------------------
    Helpers
 --------------------------------------------------------------------------}

annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration
annotateDecl m = annotateDecls $ (:[]) <$> m

annotateDecls :: ScopeM [A.Declaration] -> ScopeM A.Declaration
annotateDecls m = do
  ds <- m
  s  <- getScope
  return $ ScopedDecl s ds

annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr
annotateExpr m = do
  e <- m
  s <- getScope
  return $ ScopedExpr s e

expandEllipsis :: C.Pattern -> [C.Pattern] -> C.Clause -> C.Clause
expandEllipsis _ _ c@(C.Clause _ C.LHS{} _ _ _) = c
expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' eqs es) rhs wh wcs) =
  C.Clause x (C.LHS p (ps ++ ps') eqs es) rhs wh wcs

-- | Make sure that each variable occurs only once.
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = case xs \\ nub xs of
    []  -> return ()
    ys  -> typeError $ RepeatedVariablesInPattern $ nub ys
  where
    xs = concatMap vars ps
    vars :: A.Pattern' e -> [C.Name]
    vars p = case p of
      A.VarP x               -> [nameConcrete x]
      A.ConP _ _ args        -> concatMap (vars . namedArg) args
      A.WildP _              -> []
      A.AsP _ x p            -> nameConcrete x : vars p
      A.DotP _ _             -> []
      A.AbsurdP _            -> []
      A.LitP _               -> []
      A.DefP _ _ args        -> concatMap (vars . namedArg) args
        -- Projection pattern, @args@ should be empty unless we have
        -- indexed records.
      A.ImplicitP _          -> __IMPOSSIBLE__
      A.PatternSynP _ _ args -> concatMap (vars . namedArg) args

-- | Compute the type of the record constructor (with bogus target type)
recordConstructorType :: [NiceDeclaration] -> C.Expr
recordConstructorType fields = build fs
  where
    -- drop all declarations after the last field declaration
    fs = reverse $ dropWhile notField $ reverse fields

    notField NiceField{} = False
    notField _           = True

    -- Andreas, 2013-11-08
    -- Turn @open public@ into just @open@, since we cannot have an
    -- @open public@ in a @let@.  Fixes issue 532.
    build (NiceOpen r m dir@ImportDirective{ publicOpen = True }  : fs) =
      build (NiceOpen r m dir{ publicOpen = False } : fs)

    build (NiceModuleMacro r p x modapp open dir@ImportDirective{ publicOpen = True } : fs) =
      build (NiceModuleMacro r p x modapp open dir{ publicOpen = False } : fs)

    build (NiceField r f _ _ x (Common.Arg info e) : fs) =
        C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [mkBoundName x f] e)] $ build fs
      where r = getRange x
    build (d : fs)                     = C.Let (getRange d) [notSoNiceDeclaration d] $
                                           build fs
    build []                           = C.SetN noRange 0 -- todo: nicer


-- | @checkModuleApplication modapp m0 x dir = return (modapp', renD, renM)@
--
--   @m0@ is the new (abstract) module name and
--   @x@ its concret form (used for error messages).
checkModuleApplication
  :: C.ModuleApplication
  -> ModuleName
  -> C.Name
  -> ImportDirective
  -> ScopeM (A.ModuleApplication, Ren A.QName, Ren ModuleName)

checkModuleApplication (C.SectionApp _ tel e) m0 x dir' =
  -- For the following, set the current module to be m0.
  withCurrentModule m0 $ do
    -- check that expression @e@ is of the form @m args@
    (m, args) <- case appView e of
      AppView (Ident m) args -> return (m, args)
      _                      -> notAModuleExpr e

    -- scope check the telescope (introduces bindings!)
    tel' <- toAbstract tel
    -- scope the old module name, the module args
    (m1,args') <- toAbstract (OldModuleName m, args)
    -- Drop constructors (OnlyQualified) if there are arguments. The record constructor
    -- isn't properly in the record module, so copying it will lead to badness.
    let noRecConstr | null args = id
                    | otherwise = removeOnlyQualified
    -- Copy the scope associated with m and take the parts actually imported.
    (s', (renM, renD)) <- copyScope m m0 . noRecConstr =<< getNamedScope m1
    s' <- applyImportDirectiveM (C.QName x) dir' s'
    -- Set the current scope to @s'@
    modifyCurrentScope $ const s'
    printScope "mod.inst" 20 "copied source module"
    reportSLn "scope.mod.inst" 30 $ "renamings:\n  " ++ show renD ++ "\n  " ++ show renM
    return ((A.SectionApp tel' m1 args'), renD, renM)

checkModuleApplication (C.RecordModuleIFS _ recN) m0 x dir' =
  withCurrentModule m0 $ do
    m1 <- toAbstract $ OldModuleName recN
    s <- getNamedScope m1
    (s', (renM, renD)) <- copyScope recN m0 s
    s' <- applyImportDirectiveM recN dir' s'
    modifyCurrentScope $ const s'

    printScope "mod.inst" 20 "copied record module"
    return ((A.RecordModuleIFS m1), renD, renM)

-- | @checkModuleMacro mkApply range access concreteName modapp open dir@
--
--   Preserves local variables.

checkModuleMacro
  :: (ModuleInfo -> ModuleName -> A.ModuleApplication -> Ren A.QName -> Ren ModuleName -> a)
  -> Range
  -> Access
  -> C.Name
  -> C.ModuleApplication
  -> OpenShortHand
  -> ImportDirective
  -> ScopeM [a]
checkModuleMacro apply r p x modapp open dir = withLocalVars $ do
    notPublicWithoutOpen open dir

    m0 <- toAbstract (NewModuleName x)

    printScope "mod.inst" 20 "module macro"

    -- If we're opening, the import directive is applied to the open,
    -- otherwise to the module itself.
    let dir' = case open of
                DontOpen  -> dir
                DoOpen    -> defaultImportDir

    (modapp', renD, renM) <- checkModuleApplication modapp m0 x dir'
    bindModule p x m0
    printScope "mod.inst.copy.after" 20 "after copying"
    when (open == DoOpen) $
      openModule_ (C.QName x) dir
    printScope "mod.inst" 20 $ show open
    stripNoNames
    printScope "mod.inst" 10 $ "after stripping"
    return [ apply info (m0 `withRangesOf` [x]) modapp' renD renM ]
  where
    info = ModuleInfo
             { minfoRange  = r
             , minfoAsName = Nothing
             , minfoAsTo   = renamingRange dir
             , minfoOpenShort = Just open
             , minfoDirective = Just dir
             }

-- | The @public@ keyword must only be used together with @open@.

notPublicWithoutOpen :: OpenShortHand -> ImportDirective -> ScopeM ()
notPublicWithoutOpen DoOpen   dir = return ()
notPublicWithoutOpen DontOpen dir = when (publicOpen dir) $ typeError $
  GenericError
    "The public keyword must only be used together with the open keyword"

-- | Computes the range of all the \"to\" keywords used in a renaming
-- directive.

renamingRange :: ImportDirective -> Range
renamingRange = getRange . map renToRange . renaming

{--------------------------------------------------------------------------
    Translation
 --------------------------------------------------------------------------}

concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract_ x = toAbstract x

concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a
concreteToAbstract scope x = withScope_ scope (toAbstract x)

-- | Things that can be translated to abstract syntax are instances of this
--   class.
class ToAbstract concrete abstract | concrete -> abstract where
    toAbstract    :: concrete -> ScopeM abstract

-- | This function should be used instead of 'toAbstract' for things that need
--   to keep track of precedences to make sure that we don't forget about it.
toAbstractCtx :: ToAbstract concrete abstract =>
                 Precedence -> concrete -> ScopeM abstract
toAbstractCtx ctx c = withContextPrecedence ctx $ toAbstract c

setContextCPS :: Precedence -> (a -> ScopeM b) ->
                 ((a -> ScopeM b) -> ScopeM b) -> ScopeM b
setContextCPS p ret f = do
  p' <- getContextPrecedence
  withContextPrecedence p $ f $ withContextPrecedence p' . ret

localToAbstractCtx :: ToAbstract concrete abstract =>
                     Precedence -> concrete -> (abstract -> ScopeM a) -> ScopeM a
localToAbstractCtx ctx c ret = setContextCPS ctx ret (localToAbstract c)

-- | This operation does not affect the scope, i.e. the original scope
--   is restored upon completion.
localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
localToAbstract x ret = fst <$> localToAbstract' x ret

-- | Like 'localToAbstract' but returns the scope after the completion of the
--   second argument.
localToAbstract' :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM (b, ScopeInfo)
localToAbstract' x ret = do
  scope <- getScope
  withScope scope $ ret =<< toAbstract x

instance (ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1,c2) (a1,a2) where
  toAbstract (x,y) =
    (,) <$> toAbstract x <*> toAbstract y

instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
         ToAbstract (c1,c2,c3) (a1,a2,a3) where
    toAbstract (x,y,z) = flatten <$> toAbstract (x,(y,z))
        where
            flatten (x,(y,z)) = (x,y,z)

instance ToAbstract c a => ToAbstract [c] [a] where
    toAbstract = mapM toAbstract

instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
    toAbstract Nothing  = return Nothing
    toAbstract (Just x) = Just <$> toAbstract x

-- Names ------------------------------------------------------------------

newtype NewName a = NewName a
newtype OldQName  = OldQName C.QName
newtype OldName   = OldName C.Name
newtype PatName   = PatName C.QName

instance ToAbstract (NewName C.Name) A.Name where
  toAbstract (NewName x) = do
    y <- freshAbstractName_ x
    bindVariable x y
    return y

instance ToAbstract (NewName C.BoundName) A.Name where
  toAbstract (NewName BName{ boundName = x, bnameFixity = fx }) = do
    y <- freshAbstractName fx x
    bindVariable x y
    return y

nameExpr :: AbstractName -> A.Expr
nameExpr d = mk (anameKind d) $ anameName d
  where
    mk DefName        = Def
    mk FldName        = Def
    mk ConName        = Con . AmbQ . (:[])
    mk PatternSynName = A.PatternSyn

instance ToAbstract OldQName A.Expr where
  toAbstract (OldQName x) = do
    qx <- resolveName x
    reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
    case qx of
      VarName x'          -> return $ A.Var x'
      DefinedName _ d     -> return $ nameExpr d
      FieldName     d     -> return $ nameExpr d
      ConstructorName ds  -> return $ A.Con $ AmbQ (map anameName ds)
      UnknownName         -> notInScope x
      PatternSynResName d -> return $ nameExpr d

data APatName = VarPatName A.Name
              | ConPatName [AbstractName]
              | PatternSynPatName AbstractName

instance ToAbstract PatName APatName where
  toAbstract (PatName x) = do
    reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
    rx <- resolveName' [ConName, PatternSynName] x -- Andreas, 2013-03-21 ignore conflicting names which cannot be meant since we are in a pattern
    z  <- case (rx, x) of
      -- TODO: warn about shadowing
      (VarName y,       C.QName x)                          -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
      (FieldName d,     C.QName x)                          -> return $ Left x
      (DefinedName _ d, C.QName x) | DefName == anameKind d -> return $ Left x
      (UnknownName,     C.QName x)                          -> return $ Left x
      (ConstructorName ds, _)                               -> return $ Right (Left ds)
      (PatternSynResName d, _)                              -> return $ Right (Right d)
      _                                                     ->
        typeError $ GenericError $
          "Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
    case z of
      Left x  -> do
        reportSLn "scope.pat" 10 $ "it was a var: " ++ show x
        p <- VarPatName <$> toAbstract (NewName x)
        printLocals 10 "bound it:"
        return p
      Right (Left ds) -> do
        reportSLn "scope.pat" 10 $ "it was a con: " ++ show (map anameName ds)
        return $ ConPatName ds
      Right (Right d) -> do
        reportSLn "scope.pat" 10 $ "it was a pat syn: " ++ show (anameName d)
        return $ PatternSynPatName d


-- Should be a defined name.
instance ToAbstract OldName A.QName where
  toAbstract (OldName x) = do
    rx <- resolveName (C.QName x)
    case rx of
      DefinedName _ d -> return $ anameName d
      _               -> __IMPOSSIBLE__
        -- error $ show x ++ " - " ++ show rx

newtype NewModuleName      = NewModuleName      C.Name
newtype NewModuleQName     = NewModuleQName     C.QName
newtype OldModuleName      = OldModuleName      C.QName

freshQModule :: A.ModuleName -> C.Name -> ScopeM A.ModuleName
freshQModule m x = A.qualifyM m . mnameFromList . (:[]) <$> freshAbstractName_ x

checkForModuleClash :: C.Name -> ScopeM ()
checkForModuleClash x = do
  ms <- scopeLookup (C.QName x) <$> getScope
  unless (null ms) $ do
    reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ show ms
    setCurrentRange (getRange x) $
      typeError $ ShadowedModule x $
                map ((`withRangeOf` x) . amodName) ms

instance ToAbstract NewModuleName A.ModuleName where
  toAbstract (NewModuleName x) = do
    checkForModuleClash x
    m <- getCurrentModule
    y <- freshQModule m x
    createModule False y
    return y

instance ToAbstract NewModuleQName A.ModuleName where
  toAbstract (NewModuleQName m) = toAbs noModuleName m
    where
      toAbs m (C.QName x)  = do
        y <- freshQModule m x
        createModule False y
        return y
      toAbs m (C.Qual x q) = do
        m' <- freshQModule m x
        toAbs m' q

instance ToAbstract OldModuleName A.ModuleName where
  toAbstract (OldModuleName q) = amodName <$> resolveModule q

-- Expressions ------------------------------------------------------------

-- | Peel off 'C.HiddenArg' and represent it as an 'NamedArg'.
mkNamedArg :: C.Expr -> C.NamedArg C.Expr
mkNamedArg (C.HiddenArg   _ e) = Common.Arg (setHiding Hidden defaultArgInfo) e
mkNamedArg (C.InstanceArg _ e) = Common.Arg (setHiding Instance defaultArgInfo) e
mkNamedArg e                   = Common.Arg defaultArgInfo $ unnamed e

-- | Peel off 'C.HiddenArg' and represent it as an 'Arg', throwing away any name.
mkArg' :: C.ArgInfo -> C.Expr -> C.Arg C.Expr
mkArg' info (C.HiddenArg   _ e) = Common.Arg (setHiding Hidden info) $ namedThing e
mkArg' info (C.InstanceArg _ e) = Common.Arg (setHiding Instance info) $ namedThing e
mkArg' info e                   = Common.Arg (setHiding NotHidden info) e

-- | By default, arguments are @Relevant@.
mkArg :: C.Expr -> C.Arg C.Expr
-- mkArg (C.Dot _ e) = mkArg' Irrelevant e
mkArg e           = mkArg' defaultArgInfo e


-- | Parse a possibly dotted C.Expr as A.Expr.  Bool = True if dotted.
toAbstractDot :: Precedence -> C.Expr -> ScopeM (A.Expr, Bool)
toAbstractDot prec e = do
    reportSLn "scope.irrelevance" 100 $ "toAbstractDot: " ++ (render $ pretty e)
    traceCall (ScopeCheckExpr e) $ case e of

      C.Dot _ e -> do
        e <- toAbstractCtx prec e
        return (e, True)

      C.RawApp r es -> do
        e <- parseApplication es
        toAbstractDot prec e

      C.Paren _ e -> toAbstractDot TopCtx e

      e -> do
        e <- toAbstractCtx prec e
        return (e, False)

toAbstractOpArg :: Precedence -> OpApp C.Expr -> ScopeM A.Expr
toAbstractOpArg ctx (Ordinary e) = toAbstractCtx ctx e
toAbstractOpArg ctx (SyntaxBindingLambda r bs e) = toAbstractLam r bs e ctx

toAbstractLam :: Range -> [C.LamBinding] -> C.Expr -> Precedence -> ScopeM A.Expr
toAbstractLam r bs e ctx = do
        localToAbstract (map (C.DomainFull . makeDomainFull) bs) $ \bs ->
          case bs of
            b:bs' -> do
              e        <- toAbstractCtx ctx e
              let info = ExprRange r
              return $ A.Lam info b $ foldr mkLam e bs'
              where
                  mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
            [] -> __IMPOSSIBLE__


instance ToAbstract C.Expr A.Expr where
  toAbstract e =
    traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of

  -- Names
      Ident x -> toAbstract (OldQName x)

  -- Literals
      C.Lit l -> return $ A.Lit l

  -- Meta variables
      C.QuestionMark r n -> do
        scope <- getScope
        -- Andreas, 2014-04-06 create interaction point.
        ii <- registerInteractionPoint r n
        let info = MetaInfo
             { metaRange  = r
             , metaScope  = scope
             , metaNumber = n
             , metaNameSuggestion = ""
             }
        return $ A.QuestionMark info ii
      C.Underscore r n -> do
        scope <- getScope
        return $ A.Underscore $ MetaInfo
                    { metaRange  = r
                    , metaScope  = scope
                    , metaNumber = maybe Nothing __IMPOSSIBLE__ n
                    , metaNameSuggestion = fromMaybe "" n
                    }

  -- Raw application
      C.RawApp r es -> do
        e <- reimburseTop Bench.Scoping $ billTo [Bench.Parsing, Bench.Operators] $
          parseApplication es
        toAbstract e

{- Andreas, 2010-09-06 STALE COMMENT
  -- Dots are used in dot patterns and in irrelevant function space .A n -> B
  -- we propagate dots out from the head of applications

      C.Dot r e1 -> do
        t1 <- toAbstract e1
        return $ A.Dot t1
-}

  -- Application
      C.App r e1 e2 -> do
        e1 <- toAbstractCtx FunctionCtx e1
        e2 <- toAbstractCtx ArgumentCtx e2
        return $ A.App (ExprRange r) e1 e2

  -- Operator application
      C.OpApp r op es -> toAbstractOpApp op es

  -- With application
      C.WithApp r e es -> do
        e  <- toAbstractCtx WithFunCtx e
        es <- mapM (toAbstractCtx WithArgCtx) es
        return $ A.WithApp (ExprRange r) e es

  -- Malplaced hidden argument
      C.HiddenArg _ _ -> nothingAppliedToHiddenArg e
      C.InstanceArg _ _ -> nothingAppliedToInstanceArg e

  -- Lambda
      C.AbsurdLam r h -> return $ A.AbsurdLam (ExprRange r) h

      C.Lam r bs e -> toAbstractLam r bs e TopCtx

  -- Extended Lambda
      C.ExtendedLam r cs ->
        ifM isInsideDotPattern (typeError $ GenericError "Extended lambdas are not allowed in dot patterns") $ do
        cname <- nextlamname r 0 extendlambdaname
        name  <- freshAbstractName_ cname
        reportSLn "toabstract.extendlambda" 10 $ "new extended lambda name: " ++ show name
        qname <- qualifyName_ name
        bindName PrivateAccess DefName cname qname
        let insertApp (C.RawAppP r es) = C.RawAppP r ((IdentP (C.QName cname)) : es)
            insertApp (C.IdentP q) = C.RawAppP (getRange q) ((IdentP (C.QName cname)) : [C.IdentP q])
            insertApp _ = __IMPOSSIBLE__
            insertHead (C.LHS p wps eqs with) = C.LHS (insertApp p) wps eqs with
            insertHead (C.Ellipsis r wps eqs with) = C.Ellipsis r wps eqs with
        scdef <- toAbstract (C.FunDef r [] defaultFixity' ConcreteDef True cname
                               (map (\(lhs,rhs,wh) -> -- wh = NoWhere, see parser for more info
                                      C.Clause cname (insertHead lhs) rhs wh []) cs))
        case scdef of
          (A.ScopedDecl si [A.FunDef di qname' NotDelayed cs]) -> do
            setScope si
            return $ A.ExtendedLam (ExprRange r) di qname' cs
          _ -> __IMPOSSIBLE__
          where
            nextlamname :: Range -> Int -> String -> ScopeM C.Name
            nextlamname r i s = do
              let cname_pre = C.Name r [Id $ s ++ show i]
              rn <- resolveName (C.QName cname_pre)
              case rn of
                UnknownName -> return $ cname_pre
                _           -> nextlamname r (i+1) s

-- Irrelevant non-dependent function type

      C.Fun r e1 e2 -> do
        Common.Arg info (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
        info <- toAbstract info
        let e1 = Common.Arg ((if dotted then setRelevance Irrelevant else id) info) e0
        e2 <- toAbstractCtx TopCtx e2
        return $ A.Fun (ExprRange r) e1 e2

{-
-- Other function types

      C.Fun r e1 e2 -> do
        e1 <- toAbstractCtx FunctionSpaceDomainCtx $ mkArg e1
        e2 <- toAbstractCtx TopCtx e2
        let info = ExprRange r
        return $ A.Fun info e1 e2
-}

      e0@(C.Pi tel e) ->
        localToAbstract tel $ \tel -> do
        e    <- toAbstractCtx TopCtx e
        let info = ExprRange (getRange e0)
        return $ A.Pi info tel e

  -- Sorts
      C.Set _    -> return $ A.Set (ExprRange $ getRange e) 0
      C.SetN _ n -> return $ A.Set (ExprRange $ getRange e) n
      C.Prop _   -> return $ A.Prop $ ExprRange $ getRange e

  -- Let
      e0@(C.Let _ ds e) ->
        ifM isInsideDotPattern (typeError $ GenericError $ "Let-expressions are not allowed in dot patterns") $
        localToAbstract (LetDefs ds) $ \ds' -> do
        e        <- toAbstractCtx TopCtx e
        let info = ExprRange (getRange e0)
        return $ A.Let info ds' e

  -- Record construction
      C.Rec r fs  -> do
        let (xs, es) = unzip fs
        es <- toAbstractCtx TopCtx es
        return $ A.Rec (ExprRange r) $ zip xs es

  -- Record update
      C.RecUpdate r e fs -> do
        let (xs, es) = unzip fs
        e <- toAbstract e
        es <- toAbstractCtx TopCtx es
        return $ A.RecUpdate (ExprRange r) e $ zip xs es

  -- Parenthesis
      C.Paren _ e -> toAbstractCtx TopCtx e

  -- Pattern things
      C.Dot _ _  -> notAnExpression e
      C.As _ _ _ -> notAnExpression e
      C.Absurd _ -> notAnExpression e

  -- Impossible things
      C.ETel _  -> __IMPOSSIBLE__
      C.Equal{} -> typeError $ GenericError "Parse error: unexpected '='"

  -- Quoting
      C.QuoteGoal _ x e -> do
        x' <- toAbstract (NewName x)
        e' <- toAbstract e
        return $ A.QuoteGoal (ExprRange $ getRange e) x' e'
      C.QuoteContext _ x e -> do
        x' <- toAbstract (NewName x)
        e' <- toAbstract e
        return $ A.QuoteContext (ExprRange $ getRange e) x' e'
      C.Quote r -> return $ A.Quote (ExprRange r)
      C.QuoteTerm r -> return $ A.QuoteTerm (ExprRange r)
      C.Unquote r -> return $ A.Unquote (ExprRange r)

  -- DontCare
      C.DontCare e -> A.DontCare <$> toAbstract e

instance ToAbstract C.LamBinding A.LamBinding where
  toAbstract (C.DomainFree info x) = A.DomainFree <$> toAbstract info <*> toAbstract (NewName x)
  toAbstract (C.DomainFull tb)     = A.DomainFull <$> toAbstract tb

makeDomainFull :: C.LamBinding -> C.TypedBindings
makeDomainFull (C.DomainFull b)      = b
makeDomainFull (C.DomainFree info x) =
  C.TypedBindings r $ Common.Arg info $ C.TBind r [x] $ C.Underscore r Nothing
  where r = getRange x

instance ToAbstract C.TypedBindings A.TypedBindings where
  toAbstract (C.TypedBindings r bs) = A.TypedBindings r <$> toAbstract bs

instance ToAbstract C.TypedBinding A.TypedBinding where
  toAbstract (C.TBind r xs t) = do
    t' <- toAbstractCtx TopCtx t
    xs' <- toAbstract (map NewName xs)
    return $ A.TBind r xs' t'
  toAbstract (C.TLet r ds) = do
    ds' <- toAbstract (LetDefs ds)
    return $ A.TLet r ds'

-- | Scope check a module (top level function).
--
scopeCheckNiceModule
  :: Range
  -> Access
  -> C.Name
  -> C.Telescope
  -> ScopeM [A.Declaration]
  -> ScopeM [A.Declaration]
scopeCheckNiceModule r p name tel checkDs
  | telHasOpenStms tel = do
      -- Andreas, 2013-12-10:
      -- If the module telescope contains open statements,
      -- add an extra anonymous module around the current one.
      -- Otherwise, the open statements would create
      -- identifiers in the parent scope of the current module.
      -- But open statements in the module telescope should
      -- only affect the current module!
      scopeCheckNiceModule noRange p noName_ [] $
        scopeCheckNiceModule_

  | otherwise = do
        scopeCheckNiceModule_
  where
    -- The actual workhorse:
    scopeCheckNiceModule_ = do

      -- Check whether we are dealing with an anonymous module.
      -- This corresponds to a Coq/LEGO section.
      (name, p, open) <- do
        if isNoName name then do
          (i :: NameId) <- fresh
          return (C.NoName (getRange name) i, PrivateAccess, True)
         else return (name, p, False)

      -- Check and bind the module, using the supplied check for its contents.
      aname <- toAbstract (NewModuleName name)
      ds <- snd <$> do
        scopeCheckModule r (C.QName name) aname tel checkDs
      bindModule p name aname

      -- If the module was anonymous open it public.
      when open $
        openModule_ (C.QName name) $
          defaultImportDir { publicOpen = True }
      return ds

-- | Check whether a telescope has open declarations.
telHasOpenStms :: C.Telescope -> Bool
telHasOpenStms = any isOpenBinds
  where
    isOpenBinds (C.TypedBindings _ tb) = isOpenBind $ unArg tb
    isOpenBind C.TBind{}     = False
    isOpenBind (C.TLet _ ds) = any isOpen ds
    isOpen (C.ModuleMacro _ _ _ DoOpen _) = True
    isOpen C.Open{}          = True
    isOpen C.Import{}        = __IMPOSSIBLE__
    isOpen (C.Mutual   _ ds) = any isOpen ds
    isOpen (C.Abstract _ ds) = any isOpen ds
    isOpen (C.Private  _ ds) = any isOpen ds
    isOpen   _               = False

{- UNUSED
telHasLetStms :: C.Telescope -> Bool
telHasLetStms = any isLetBinds
  where
    isLetBinds (C.TypedBindings _ tb) = isLetBind $ unArg tb
    isLetBind C.TBind{} = False
    isLetBind C.TLet{}  = True
-}

-- | We for now disallow let-bindings in @data@ and @record@ telescopes.
--   This due "nested datatypes"; there is no easy interpretation of
--   @
--      data D (A : Set) (open M A) (b : B) : Set where
--        c : D (A × A) b → D A b
--   @
--   where @B@ is brought in scope by @open M A@.

class EnsureNoLetStms a where
  ensureNoLetStms :: a -> ScopeM ()

{- From ghc 7.2, there is LANGUAGE DefaultSignatures
  default ensureNoLetStms :: Foldable t => t a -> ScopeM ()
  ensureNoLetStms = traverse_ ensureNoLetStms
-}

instance EnsureNoLetStms C.TypedBinding where
  ensureNoLetStms tb =
    case tb of
      C.TLet{}  -> typeError $ IllegalLetInTelescope tb
      C.TBind{} -> return ()

instance EnsureNoLetStms a => EnsureNoLetStms (LamBinding' a) where
  ensureNoLetStms = traverse_ ensureNoLetStms

instance EnsureNoLetStms a => EnsureNoLetStms (TypedBindings' a) where
  ensureNoLetStms = traverse_ ensureNoLetStms

instance EnsureNoLetStms a => EnsureNoLetStms [a] where
  ensureNoLetStms = traverse_ ensureNoLetStms


-- | Returns the scope inside the checked module.
scopeCheckModule
  :: Range
  -> C.QName                 -- ^ The concrete name of the module.
  -> A.ModuleName            -- ^ The abstract name of the module.
  -> C.Telescope             -- ^ The module telescope.
  -> ScopeM [A.Declaration]  -- ^ The code for checking the module contents.
  -> ScopeM (ScopeInfo, [A.Declaration])
scopeCheckModule r x qm tel checkDs = do
  printScope "module" 20 $ "checking module " ++ show x
  -- Andreas, 2013-12-10: Telescope does not live in the new module
  -- but its parent, so check it before entering the new module.
  -- This is important for Nicolas Pouillard's open parametrized modules
  -- statements inside telescopes.
  res <- withLocalVars $ do
    tel <- toAbstract tel
    withCurrentModule qm $ do
      -- pushScope m
      -- qm <- getCurrentModule
      printScope "module" 20 $ "inside module " ++ show x
      ds    <- checkDs
      scope <- getScope
      return (scope, [ A.Section info (qm `withRangesOfQ` x) tel ds ])

  -- Binding is done by the caller
  printScope "module" 20 $ "after module " ++ show x
  return res
  where
    info = ModuleInfo r noRange Nothing Nothing Nothing

-- | Temporary data type to scope check a file.
data TopLevel a = TopLevel
  { topLevelPath           :: AbsolutePath
    -- ^ The file path from which we loaded this module.
  , topLevelTheThing       :: a
    -- ^ The file content.
  }

data TopLevelInfo = TopLevelInfo
        { topLevelDecls :: [A.Declaration]
        , outsideScope  :: ScopeInfo
        , insideScope   :: ScopeInfo
        }

-- | The top-level module name.

topLevelModuleName :: TopLevelInfo -> A.ModuleName
topLevelModuleName topLevel = scopeCurrent (insideScope topLevel)

-- Top-level declarations are always (import|open)* module
instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
    toAbstract (TopLevel file ds) =
      -- A file is a bunch of preliminary decls (imports etc.)
      -- plus a single module decl.
      case splitAt (length ds - 1) ds of
        (ds', [C.Module r m0 tel ds]) -> do
          -- If the module name is _ compute the name from the file path
          m <- if isNoName m0
                then return $ C.QName $ C.Name noRange [Id $ rootName file]
                else do
                -- Andreas, 2014-03-28  Issue 1078
                -- We need to check the module name against the file name here.
                -- Otherwise one could sneak in a lie and confuse the scope
                -- checker.
                  checkModuleName (C.toTopLevelModuleName m0) file
                  return m0
          setTopLevelModule m
          am           <- toAbstract (NewModuleQName m)
          ds'          <- toAbstract ds'
          (scope0, ds) <- scopeCheckModule r m am tel $ toAbstract ds
          scope        <- getScope
          return $ TopLevelInfo (ds' ++ ds) scope scope0
        _ -> __IMPOSSIBLE__

-- | runs Syntax.Concrete.Definitions.niceDeclarations on main module
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
niceDecls ds = case runNice $ niceDeclarations ds of
  Left e   -> throwError $ Exception (getRange e) (show e)
  Right ds -> return ds

instance ToAbstract [C.Declaration] [A.Declaration] where
  toAbstract ds = do
    -- don't allow to switch off termination checker in --safe mode
    ds <- ifM (optSafe <$> commandLineOptions) (mapM noNoTermCheck ds) (return ds)
    toAbstract =<< niceDecls ds
   where
    noNoTermCheck (C.Pragma (NoTerminationCheckPragma r)) =
      typeError $ SafeFlagNoTerminationCheck
    noNoTermCheck d = return d

newtype LetDefs = LetDefs [C.Declaration]
newtype LetDef = LetDef NiceDeclaration

instance ToAbstract LetDefs [A.LetBinding] where
  toAbstract (LetDefs ds) =
    concat <$> (toAbstract =<< map LetDef <$> niceDecls ds)

instance ToAbstract LetDef [A.LetBinding] where
    toAbstract (LetDef d) =
        case d of
            NiceMutual _ _ d@[C.FunSig _ fx _ info _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
                do  when (abstract == AbstractDef) $ do
                      typeError $ GenericError $ "abstract not allowed in let expressions"
                    e <- letToAbstract cl
                    t <- toAbstract t
                    x <- toAbstract (NewName $ mkBoundName x fx)
                    info <- toAbstract info
                    return [ A.LetBind (LetRange $ getRange d) info x t e ]

            -- irrefutable let binding, like  (x , y) = rhs
            NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause lhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
              mp  <- setCurrentRange (getRange p) $ (Right <$> parsePattern p) `catchError` (return . Left)
              case mp of
                Right p -> do
                  rhs <- toAbstract rhs
                  p   <- toAbstract p
                  checkPatternLinearity [p]
                  p   <- toAbstract p
                  return [ A.LetPatBind (LetRange r) p rhs ]
                -- It's not a record pattern, so it should be a prefix left-hand side
                Left err ->
                  case definedName p of
                    Nothing -> throwError err
                    Just x  -> toAbstract $ LetDef $ NiceMutual r termCheck
                      [ C.FunSig r defaultFixity' PublicAccess defaultArgInfo termCheck x (C.Underscore (getRange x) Nothing)
                      , C.FunDef r __IMPOSSIBLE__ __IMPOSSIBLE__ ConcreteDef __IMPOSSIBLE__ __IMPOSSIBLE__
                        [C.Clause x lhs (C.RHS rhs) NoWhere []]
                      ]
                  where
                    definedName (C.IdentP (C.QName x)) = Just x
                    definedName C.IdentP{}             = Nothing
                    definedName (C.RawAppP _ (p : _))  = definedName p
                    definedName (C.ParenP _ p)         = definedName p
                    definedName C.WildP{}              = Nothing   -- for instance let _ + x = x in ... (not allowed)
                    definedName C.AbsurdP{}            = Nothing
                    definedName C.AsP{}                = Nothing
                    definedName C.DotP{}               = Nothing
                    definedName C.LitP{}               = Nothing
                    definedName C.HiddenP{}            = __IMPOSSIBLE__
                    definedName C.InstanceP{}          = __IMPOSSIBLE__
                    definedName C.RawAppP{}            = __IMPOSSIBLE__
                    definedName C.AppP{}               = __IMPOSSIBLE__
                    definedName C.OpAppP{}             = __IMPOSSIBLE__

            -- You can't open public in a let
            NiceOpen r x dirs | not (C.publicOpen dirs) -> do
              m       <- toAbstract (OldModuleName x)
              n       <- length . scopeLocals <$> getScope
              openModule_ x dirs
              return [A.LetOpen (ModuleInfo
                                   { minfoRange  = r
                                   , minfoAsName = Nothing
                                   , minfoAsTo   = renamingRange dirs
                                   , minfoOpenShort = Nothing
                                   , minfoDirective = Just dirs
                                   })
                                m
                     ]

            NiceModuleMacro r p x modapp open dir | not (C.publicOpen dir) ->
              checkModuleMacro LetApply r p x modapp open dir

            _   -> notAValidLetBinding d
        where
            letToAbstract (C.Clause top clhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere []) = do
{-
                p    <- parseLHS top p
                localToAbstract (snd $ lhsArgs p) $ \args ->
-}
                (x, args) <- do
                  res <- setCurrentRange (getRange p) $ parseLHS top p
                  case res of
                    C.LHSHead x args -> return (x, args)
                    C.LHSProj{} -> typeError $ GenericError $ "copatterns not allowed in let bindings"

                localToAbstract args $ \args ->
                    do  rhs <- toAbstract rhs
                        foldM lambda rhs (reverse args)  -- just reverse because these DomainFree
            letToAbstract _ = notAValidLetBinding d

            -- Named patterns not allowed in let definitions
            lambda e (Common.Arg info (Named Nothing (A.VarP x))) =
                    return $ A.Lam i (A.DomainFree info x) e
                where
                    i = ExprRange (fuseRange x e)
            lambda e (Common.Arg info (Named Nothing (A.WildP i))) =
                do  x <- freshNoName (getRange i)
                    return $ A.Lam i' (A.DomainFree info x) e
                where
                    i' = ExprRange (fuseRange i e)
            lambda _ _ = notAValidLetBinding d

newtype Blind a = Blind { unBlind :: a }

instance ToAbstract (Blind a) (Blind a) where
  toAbstract = return

-- The only reason why we return a list is that open declarations disappears.
-- For every other declaration we get a singleton list.
instance ToAbstract NiceDeclaration A.Declaration where

  toAbstract d = annotateDecls $
    traceCall (ScopeCheckDeclaration d) $
    case d of

  -- Axiom (actual postulate)
    C.Axiom r f p rel x t -> do
      -- check that we do not postulate in --safe mode
      clo <- commandLineOptions
      when (optSafe clo) (typeError (SafeFlagPostulate x))
      -- check the postulate
      toAbstractNiceAxiom A.NoFunSig d

  -- Fields
    C.NiceField r f p a x t -> do
      unless (p == PublicAccess) $ typeError $ GenericError "Record fields can not be private"
      -- Interaction points for record fields have already been introduced
      -- when checking the type of the record constructor.
      -- To avoid introducing interaction points (IP) twice, we turn
      -- all question marks to underscores.  (See issue 1138.)
      let maskIP (C.QuestionMark r _) = C.Underscore r Nothing
          maskIP e                     = e
      t' <- toAbstractCtx TopCtx $ mapExpr maskIP t
      y  <- freshAbstractQName f x
      irrProj <- optIrrelevantProjections <$> pragmaOptions
      unless (isIrrelevant t && not irrProj) $
        -- Andreas, 2010-09-24: irrelevant fields are not in scope
        -- this ensures that projections out of irrelevant fields cannot occur
        -- Ulf: unless you turn on --irrelevant-projections
        bindName p FldName x y
      return [ A.Field (mkDefInfo x f p a r) y t' ]

  -- Primitive function
    PrimitiveFunction r f p a x t -> do
      t' <- toAbstractCtx TopCtx t
      y  <- freshAbstractQName f x
      bindName p DefName x y
      return [ A.Primitive (mkDefInfo x f p a r) y t' ]

  -- Definitions (possibly mutual)
    NiceMutual r termCheck ds -> do
      ds' <- toAbstract ds
      return [ A.Mutual (MutualInfo termCheck r) ds' ]

    C.NiceRecSig r f a x ls t -> do
      ensureNoLetStms ls
      withLocalVars $ do
        ls' <- toAbstract (map makeDomainFull ls)
        x'  <- freshAbstractQName f x
        bindName a DefName x x'
        t' <- toAbstract t
        return [ A.RecSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]

    C.NiceDataSig r f a x ls t -> withLocalVars $ do
        printScope "scope.data.sig" 20 ("checking DataSig for " ++ show x)
        ensureNoLetStms ls
        ls' <- toAbstract (map makeDomainFull ls)
        x'  <- freshAbstractQName f x
        {- -- Andreas, 2012-01-16: remember number of parameters
        bindName a (DataName (length ls)) x x' -}
        bindName a DefName x x'
        t' <- toAbstract t
        return [ A.DataSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
  -- Type signatures
    C.FunSig r f p rel tc x t -> toAbstractNiceAxiom A.FunSig (C.Axiom r f p rel x t)
  -- Function definitions
    C.FunDef r ds f a tc x cs -> do
        printLocals 10 $ "checking def " ++ show x
        (x',cs) <- toAbstract (OldName x,cs)
        let delayed = NotDelayed
        -- (delayed, cs) <- translateCopatternClauses cs -- TODO
        return [ A.FunDef (mkDefInfo x f PublicAccess a r) x' delayed cs ]

  -- Uncategorized function clauses
    C.NiceFunClause r acc abs termCheck (C.FunClause lhs rhs wcls) ->
      typeError $ GenericError $
        "Missing type signature for left hand side " ++ show lhs
    C.NiceFunClause{} -> __IMPOSSIBLE__

  -- Data definitions
    C.DataDef r f a x pars cons -> withLocalVars $ do
        printScope "scope.data.def" 20 ("checking DataDef for " ++ show x)
        ensureNoLetStms pars
        -- Check for duplicate constructors
        do let cs   = map conName cons
               dups = nub $ cs \\ nub cs
               bad  = filter (`elem` dups) cs
           unless (distinct cs) $
             setCurrentRange (getRange bad) $
                typeError $ DuplicateConstructors dups

        pars <- toAbstract pars
        DefinedName p ax <- resolveName (C.QName x)
        let x' = anameName ax
        -- Create the module for the qualified constructors
        checkForModuleClash x -- disallow shadowing previously defined modules
        let m = mnameFromList $ qnameToList x'
        createModule True m
        bindModule p x m  -- make it a proper module
        cons <- toAbstract (map (ConstrDecl NoRec m a p) cons)
        -- Open the module
        -- openModule_ (C.QName x) defaultImportDir{ publicOpen = True }
        printScope "data" 20 $ "Checked data " ++ show x
        return [ A.DataDef (mkDefInfo x f PublicAccess a r) x' pars cons ]
      where
        conName (C.Axiom _ _ _ _ c _) = c
        conName _ = __IMPOSSIBLE__

  -- Record definitions (mucho interesting)
    C.RecDef r f a x ind cm pars fields -> do
      ensureNoLetStms pars
      withLocalVars $ do
        -- Check that the generated module doesn't clash with a previously
        -- defined module
        checkForModuleClash x
        pars   <- toAbstract pars
        DefinedName p ax <- resolveName (C.QName x)
        let x' = anameName ax
        -- We scope check the fields a first time when putting together
        -- the type of the constructor.
        contel <- toAbstract $ recordConstructorType fields
        m0     <- getCurrentModule
        let m = A.qualifyM m0 $ mnameFromList $ (:[]) $ last $ qnameToList x'
        printScope "rec" 15 "before record"
        createModule False m
        -- We scope check the fields a second time, as actual fields.
        afields <- withCurrentModule m $ do
          afields <- toAbstract fields
          printScope "rec" 15 "checked fields"
          return afields
        bindModule p x m
        cm' <- mapM (\(ThingWithFixity c f) -> bindConstructorName m c f a p YesRec) cm
        printScope "rec" 15 "record complete"
        return [ A.RecDef (mkDefInfo x f PublicAccess a r) x' ind cm' pars contel afields ]

    NiceModule r p a x@(C.QName name) tel ds ->
      traceCall (ScopeCheckDeclaration $ NiceModule r p a x tel []) $ do
        scopeCheckNiceModule r p name tel $ toAbstract ds

    NiceModule _ _ _ m@C.Qual{} _ _ ->
      typeError $ GenericError $ "Local modules cannot have qualified names"

    NiceModuleMacro r p x modapp open dir ->
      checkModuleMacro Apply r p x modapp open dir

    NiceOpen r x dir -> do
      m <- toAbstract (OldModuleName x)
      printScope "open" 20 $ "opening " ++ show x
      openModule_ x dir
      printScope "open" 20 $ "result:"
      return [A.Open (ModuleInfo
                        { minfoRange  = r
                        , minfoAsName = Nothing
                        , minfoAsTo   = renamingRange dir
                        , minfoOpenShort = Nothing
                        , minfoDirective = Just dir
                        })
                     m]

    NicePragma r p -> do
      ps <- toAbstract p
      return $ map (A.Pragma r) ps

    NiceImport r x as open dir -> do
      notPublicWithoutOpen open dir

      -- First scope check the imported module and return its name and
      -- interface. This is done with that module as the top-level module.
      -- This is quite subtle. We rely on the fact that when setting the
      -- top-level module and generating a fresh module name the generated
      -- name will be exactly the same as the name generated when checking
      -- the imported module.
      (m, i) <- withCurrentModule noModuleName $ withTopLevelModule x $ do
        m <- toAbstract $ NewModuleQName x
        printScope "import" 10 "before import:"
        (m, i) <- scopeCheckImport m
        printScope "import" 10 $ "scope checked import: " ++ show i
        -- We don't want the top scope of the imported module (things happening
        -- before the module declaration)
        return (m, Map.delete noModuleName i)

      -- Merge the imported scopes with the current scopes
      modifyScopes $ \ ms -> Map.unionWith mergeScope (Map.delete m ms) i

      -- Bind the desired module name to the right abstract name.
      case as of
        Nothing -> bindQModule PrivateAccess x m
        Just y  -> bindModule PrivateAccess (asName y) m

      printScope "import" 10 "merged imported sig:"

      -- Open if specified, otherwise apply import directives
      let (name, theAsSymbol, theAsName) = case as of
            Nothing -> (x,                  noRange,   Nothing)
            Just a  -> (C.QName (asName a), asRange a, Just (asName a))
      case open of
        DoOpen   -> do
          toAbstract [ C.Open r name dir ]
          return ()
        DontOpen -> do
          -- If not opening import directives are applied to the original scope
          modifyNamedScopeM m $ applyImportDirectiveM x dir
      return [ A.Import (ModuleInfo
                           { minfoRange  = r
                           , minfoAsName = theAsName
                           , minfoAsTo   =
                               getRange (theAsSymbol, renamingRange dir)
                           , minfoOpenShort = Just open
                           , minfoDirective = Just dir
                           })
                        m ]

    NicePatternSyn r fx n as p -> do
      reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ show r

      y <- freshAbstractQName fx n
      bindName PublicAccess PatternSynName n y
      defn@(as, p) <- withLocalVars $ do
         p  <- toAbstract =<< toAbstract =<< parsePatternSyn p
         as <- (traverse . mapM) (unVarName <=< resolveName . C.QName) as
         as <- (map . fmap) unBlind <$> toAbstract ((map . fmap) Blind as)
         return (as, p)
      modifyPatternSyns (Map.insert y defn)
      return [A.PatternSynDef y as p]   -- only for highlighting
      where unVarName (VarName a) = return a
            unVarName _           = typeError $ UnusedVariableInPatternSynonym

    where
      -- checking postulate or type sig. without checking safe flag
      toAbstractNiceAxiom funSig (C.Axiom r f p info x t) = do
        t' <- toAbstractCtx TopCtx t
        y  <- freshAbstractQName f x
        info <- toAbstract info
        bindName p DefName x y
        return [ A.Axiom funSig (mkDefInfo x f p ConcreteDef r) info y t' ]
      toAbstractNiceAxiom _ _ = __IMPOSSIBLE__


data IsRecordCon = YesRec | NoRec
data ConstrDecl = ConstrDecl IsRecordCon A.ModuleName IsAbstract Access C.NiceDeclaration

bindConstructorName m x f a p record = do
  -- The abstract name is the qualified one
  y <- withCurrentModule m $ freshAbstractQName f x
  -- Bind it twice, once unqualified and once qualified
  bindName p' ConName x y
  withCurrentModule m $ bindName p'' ConName x y
  return y
  where
    -- An abstract constructor is private (abstract constructor means
    -- abstract datatype, so the constructor should not be exported).
    p' = case a of
           AbstractDef -> PrivateAccess
           _           -> p
    p'' = case (a, record) of
            (AbstractDef, _) -> PrivateAccess
            (_, YesRec)      -> OnlyQualified   -- record constructors aren't really in the record module
            _                -> PublicAccess

instance ToAbstract ConstrDecl A.Declaration where
  toAbstract (ConstrDecl record m a p (C.Axiom r f _ info x t)) = do -- rel==Relevant
    t' <- toAbstractCtx TopCtx t
    -- The abstract name is the qualified one
    -- Bind it twice, once unqualified and once qualified
    y <- bindConstructorName m x f a p record
    info <- toAbstract info
    printScope "con" 15 "bound constructor"
    return $ A.Axiom NoFunSig (mkDefInfo x f p ConcreteDef r) info y t'

  toAbstract _ = __IMPOSSIBLE__    -- a constructor is always an axiom

instance ToAbstract C.Pragma [A.Pragma] where
    toAbstract (C.ImpossiblePragma _) = impossibleTest
    toAbstract (C.OptionsPragma _ opts) = return [ A.OptionsPragma opts ]
    toAbstract (C.CompiledTypePragma _ x hs) = do
      e <- toAbstract $ OldQName x
      case e of
        A.Def x -> return [ A.CompiledTypePragma x hs ]
        _       -> fail $ "Bad compiled type: " ++ show x  -- TODO: error message
    toAbstract (C.CompiledDataPragma _ x hs hcs) = do
      e <- toAbstract $ OldQName x
      case e of
        A.Def x -> return [ A.CompiledDataPragma x hs hcs ]
        _       -> fail $ "Not a datatype: " ++ show x  -- TODO: error message
    toAbstract (C.CompiledPragma _ x hs) = do
      e <- toAbstract $ OldQName x
      y <- case e of
            A.Def x -> return x
            A.Con _ -> fail "Use COMPILED_DATA for constructors" -- TODO
            _       -> __IMPOSSIBLE__
      return [ A.CompiledPragma y hs ]
    toAbstract (C.CompiledExportPragma _ x hs) = do
      e <- toAbstract $ OldQName x
      y <- case e of
            A.Def x -> return x
            --A.Con x -> return x
            _       -> __IMPOSSIBLE__
      return [ A.CompiledExportPragma y hs ]
    toAbstract (C.CompiledEpicPragma _ x ep) = do
      e <- toAbstract $ OldQName x
      y <- case e of
            A.Def x -> return x
            _       -> __IMPOSSIBLE__
      return [ A.CompiledEpicPragma y ep ]
    toAbstract (C.CompiledJSPragma _ x ep) = do
      e <- toAbstract $ OldQName x
      y <- case e of
            A.Def x -> return x
            A.Con (AmbQ [x]) -> return x
            A.Con x -> fail ("COMPILED_JS used on ambiguous name " ++ show x)
            _       -> __IMPOSSIBLE__
      return [ A.CompiledJSPragma y ep ]
    toAbstract (C.StaticPragma _ x) = do
        e <- toAbstract $ OldQName x
        y <- case e of
            A.Def x -> return x
            _       -> __IMPOSSIBLE__
        return [ A.StaticPragma y ]
    toAbstract (C.BuiltinPragma _ b e) = do
        e <- toAbstract e
        return [ A.BuiltinPragma b e ]
    toAbstract (C.ImportPragma _ i) = do
      addHaskellImport i
      return []
    toAbstract (C.EtaPragma _ x) = do
      e <- toAbstract $ OldQName x
      case e of
        A.Def x -> return [ A.EtaPragma x ]
        _       -> fail "Bad ETA pragma"
    -- NO_TERMINATION_CHECK is handled by the nicifier
    toAbstract (C.NoTerminationCheckPragma _) = __IMPOSSIBLE__

instance ToAbstract C.Clause A.Clause where
    toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
    toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
      -- Andreas, 2012-02-14: need to reset local vars before checking subclauses
      vars <- getLocalVars
      let wcs' = for wcs $ \ c -> do
           setLocalVars vars
           return $ expandEllipsis p wps c
      lhs' <- toAbstract (LeftHandSide top p wps)
      printLocals 10 "after lhs:"
      let (whname, whds) = case wh of
            NoWhere        -> (Nothing, [])
            AnyWhere ds    -> (Nothing, ds)
            SomeWhere m ds -> (Just m, ds)
      if not (null eqs)
        then do
          rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs whds)
          return $ A.Clause lhs' rhs []
        else do
          -- the right hand side is checked inside the module of the local definitions
          (rhs, ds) <- whereToAbstract (getRange wh) whname whds $
                        toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs [])
          rhs <- toAbstract rhs
          return $ A.Clause lhs' rhs ds

whereToAbstract :: Range -> Maybe C.Name -> [C.Declaration] -> ScopeM a -> ScopeM (a, [A.Declaration])
whereToAbstract _ _ [] inner = do
  x <- inner
  return (x, [])
whereToAbstract r whname whds inner = do
  m <- maybe (nameConcrete <$> freshNoName noRange) return whname
  m <- if (maybe False isNoName whname)
       then do
         (i :: NameId) <- fresh
         return (C.NoName (getRange m) i)
       else return m
  let acc = maybe PrivateAccess (const PublicAccess) whname  -- unnamed where's are private
  let tel = []
  old <- getCurrentModule
  am  <- toAbstract (NewModuleName m)
  (scope, ds) <- scopeCheckModule r (C.QName m) am tel $ toAbstract whds
  setScope scope
  x <- inner
  setCurrentModule old
  bindModule acc m am
  -- Issue 848: if the module was anonymous (module _ where) open it public
  when (maybe False isNoName whname) $
    openModule_ (C.QName m) $
      defaultImportDir { publicOpen = True }
  return (x, ds)

data RightHandSide = RightHandSide
  { rhsRewriteEqn :: [C.RewriteEqn]  -- ^ @rewrite e@ (many)
  , rhsWithExpr   :: [C.WithExpr]    -- ^ @with e@ (many)
  , rhsSubclauses :: [ScopeM C.Clause] -- ^ the subclauses spawned by a with (monadic because we need to reset the local vars before checking these clauses)
  , rhs           :: C.RHS
  , rhsWhereDecls :: [C.Declaration]
  }

data AbstractRHS = AbsurdRHS'
                 | WithRHS' [A.Expr] [ScopeM C.Clause]  -- ^ The with clauses haven't been translated yet
                 | RHS' A.Expr
                 | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]

qualifyName_ :: A.Name -> ScopeM A.QName
qualifyName_ x = do
  m <- getCurrentModule
  return $ A.qualify m x

withFunctionName :: String -> ScopeM A.QName
withFunctionName s = do
  NameId i _ <- fresh
  qualifyName_ =<< freshName_ (s ++ show i)

instance ToAbstract AbstractRHS A.RHS where
  toAbstract AbsurdRHS'            = return A.AbsurdRHS
  toAbstract (RHS' e)              = return $ A.RHS e
  toAbstract (RewriteRHS' eqs rhs wh) = do
    auxs <- replicateM (length eqs) $ withFunctionName "rewrite-"
    rhs  <- toAbstract rhs
    return $ RewriteRHS auxs eqs rhs wh
  toAbstract (WithRHS' es cs) = do
    aux <- withFunctionName "with-"
    A.WithRHS aux es <$> do toAbstract =<< sequence cs

instance ToAbstract RightHandSide AbstractRHS where
  toAbstract (RightHandSide eqs@(_:_) es cs rhs wh) = do
    eqs <- toAbstractCtx TopCtx eqs
                 -- TODO: remember named where
    (rhs, ds) <- whereToAbstract (getRange wh) Nothing wh $
                  toAbstract (RightHandSide [] es cs rhs [])
    return $ RewriteRHS' eqs rhs ds
  toAbstract (RightHandSide [] [] (_ : _) _ _)        = __IMPOSSIBLE__
  toAbstract (RightHandSide [] (_ : _) _ (C.RHS _) _) = typeError $ BothWithAndRHS
  toAbstract (RightHandSide [] [] [] rhs [])          = toAbstract rhs
  toAbstract (RightHandSide [] es cs C.AbsurdRHS [])  = do
    es <- toAbstractCtx TopCtx es
    return $ WithRHS' es cs
  -- TODO: some of these might be possible
  toAbstract (RightHandSide [] (_ : _) _ C.AbsurdRHS (_ : _)) = __IMPOSSIBLE__
  toAbstract (RightHandSide [] [] [] (C.RHS _) (_ : _))       = __IMPOSSIBLE__
  toAbstract (RightHandSide [] [] [] C.AbsurdRHS (_ : _))     = __IMPOSSIBLE__

instance ToAbstract C.RHS AbstractRHS where
    toAbstract C.AbsurdRHS = return $ AbsurdRHS'
    toAbstract (C.RHS e)   = RHS' <$> toAbstract e

data LeftHandSide = LeftHandSide C.Name C.Pattern [C.Pattern]

instance ToAbstract LeftHandSide A.LHS where
    toAbstract (LeftHandSide top lhs wps) =
      traceCall (ScopeCheckLHS top lhs) $ do
        lhscore <- parseLHS top lhs
        reportSLn "scope.lhs" 5 $ "parsed lhs: " ++ show lhscore
        printLocals 10 "before lhs:"
        -- error if copattern parsed but no --copatterns option
        haveCoPats <- optCopatterns <$> pragmaOptions
        unless haveCoPats $
          case lhscore of
            C.LHSHead x ps -> return ()
            C.LHSProj{} -> typeError $ NeedOptionCopatterns
        -- scope check patterns except for dot patterns
        lhscore <- toAbstract lhscore
        reportSLn "scope.lhs" 5 $ "parsed lhs patterns: " ++ show lhscore
        wps  <- toAbstract =<< mapM parsePattern wps
        checkPatternLinearity $ lhsCoreAllPatterns lhscore ++ wps
        printLocals 10 "checked pattern:"
        -- scope check dot patterns
        lhscore <- toAbstract lhscore
        reportSLn "scope.lhs" 5 $ "parsed lhs dot patterns: " ++ show lhscore
        wps     <- toAbstract wps
        printLocals 10 "checked dots:"
        return $ A.LHS (LHSRange $ getRange (lhs, wps)) lhscore wps

-- does not check pattern linearity
instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
    toAbstract (C.LHSHead x ps) = do
        x    <- withLocalVars $ setLocalVars [] >> toAbstract (OldName x)
        args <- toAbstract ps
        return $ A.LHSHead x args
    toAbstract (C.LHSProj d ps1 l ps2) = do
        qx <- resolveName d
        d  <- case qx of
                FieldName d -> return $ anameName d
                UnknownName -> notInScope d
                _           -> typeError $ GenericError $
                  "head of copattern needs to be a field identifier, but "
                  ++ show d ++ " isn't one"
        args1 <- toAbstract ps1
        l     <- toAbstract l
        args2 <- toAbstract ps2
        return $ A.LHSProj d args1 l args2

instance ToAbstract c a => ToAbstract (C.Arg c) (A.Arg a) where
    toAbstract (Common.Arg info e) =
        Common.Arg <$> toAbstract info <*> toAbstractCtx (hiddenArgumentCtx $ getHiding info) e

instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
    toAbstract (Named n e) = Named n <$> toAbstract e

{- DOES NOT WORK ANYMORE with pattern synonyms
instance ToAbstract c a => ToAbstract (A.LHSCore' c) (A.LHSCore' a) where
    toAbstract = mapM toAbstract
-}

instance ToAbstract (A.LHSCore' C.Expr) (A.LHSCore' A.Expr) where
    toAbstract (A.LHSHead f ps)             = A.LHSHead f <$> mapM toAbstract ps
    toAbstract (A.LHSProj d ps lhscore ps') = A.LHSProj d <$> mapM toAbstract ps
      <*> mapM toAbstract lhscore <*> mapM toAbstract ps'

instance ToAbstract c a => ToAbstract (A.NamedArg c) (A.NamedArg a) where
    toAbstract (Common.Arg info c) = liftM2 Common.Arg (return info) (toAbstract c)

instance ToAbstract C.ArgInfo A.ArgInfo where
    toAbstract info = do cs <- mapM toAbstract $ argInfoColors info
                         return $ info { argInfoColors = cs }

-- Patterns are done in two phases. First everything but the dot patterns, and
-- then the dot patterns. This is because dot patterns can refer to variables
-- bound anywhere in the pattern.

instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
    toAbstract (A.VarP x)             = return $ A.VarP x
    toAbstract (A.ConP i ds as)       = A.ConP i ds <$> mapM toAbstract as
    toAbstract (A.DefP i x as)        = A.DefP i x <$> mapM toAbstract as
    toAbstract (A.WildP i)            = return $ A.WildP i
    toAbstract (A.AsP i x p)          = A.AsP i x <$> toAbstract p
    toAbstract (A.DotP i e)           = A.DotP i <$> insideDotPattern (toAbstract e)
    toAbstract (A.AbsurdP i)          = return $ A.AbsurdP i
    toAbstract (A.LitP l)             = return $ A.LitP l
    toAbstract (A.ImplicitP i)        = return $ A.ImplicitP i
    toAbstract (A.PatternSynP i x as) = A.PatternSynP i x <$> mapM toAbstract as

instance ToAbstract C.Pattern (A.Pattern' C.Expr) where

    toAbstract p@(C.IdentP x) = do
        px <- toAbstract (PatName x)
        case px of
            VarPatName y        -> return $ VarP y
            ConPatName ds       -> return $ ConP (ConPatInfo False $ PatRange (getRange p))
                                                 (AmbQ $ map anameName ds)
                                                 []
            PatternSynPatName d -> return $ PatternSynP (PatRange (getRange p))
                                                        (anameName d) []

    toAbstract p0@(AppP p q) = do
        (p', q') <- toAbstract (p,q)
        case p' of
            ConP i x as        -> return $ ConP (i {patInfo = info}) x (as ++ [q'])
            DefP _ x as        -> return $ DefP info x (as ++ [q'])
            PatternSynP _ x as -> return $ PatternSynP info x (as ++ [q'])
            _                  -> typeError $ InvalidPattern p0
        where
            r = getRange p0
            info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0

    toAbstract p0@(OpAppP r op ps) = do
        p <- toAbstract (IdentP op)
        ps <- toAbstract ps
        case p of
          ConP        i x as -> return $ ConP (i {patInfo = info}) x
                                    (as ++ ps)
          DefP        _ x as -> return $ DefP info x
                                    (as ++ ps)
          PatternSynP _ x as -> return $ PatternSynP info x
                                    (as ++ ps)
          _                  -> __IMPOSSIBLE__
        where
            r    = getRange p0
            info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0

    -- Removed when parsing
    toAbstract (HiddenP _ _)   = __IMPOSSIBLE__
    toAbstract (InstanceP _ _) = __IMPOSSIBLE__
    toAbstract (RawAppP _ _)   = __IMPOSSIBLE__

    toAbstract p@(C.WildP r)    = return $ A.WildP (PatSource r $ const p)
    toAbstract (C.ParenP _ p)   = toAbstract p
    toAbstract (C.LitP l)       = return $ A.LitP l
    toAbstract p0@(C.AsP r x p) = typeError $ NotSupported "@-patterns"
      {- do
        x <- toAbstract (NewName x)
        p <- toAbstract p
        return $ A.AsP info x p
        where
            info = PatSource r $ \_ -> p0
      -}
    -- we have to do dot patterns at the end
    toAbstract p0@(C.DotP r e) = return $ A.DotP info e
        where info = PatSource r $ \_ -> p0
    toAbstract p0@(C.AbsurdP r) = return $ A.AbsurdP info
        where info = PatSource r $ \_ -> p0

-- | Turn an operator application into abstract syntax. Make sure to record the
-- right precedences for the various arguments.
toAbstractOpApp :: C.QName -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
toAbstractOpApp op es = do
    f  <- getFixity op
    let (_,_,parts) = oldToNewNotation $ (op, f)
    op <- toAbstract (OldQName op)
    foldl' app op <$> left (theFixity f) [p | p <- parts, not (isBindingHole p)] es
    where
        app e arg = A.App (ExprRange (fuseRange e arg)) e (setArgColors [] arg)

        toAbsOpArg cxt = traverse $ traverse $ toAbstractOpArg cxt

        left f (IdPart _ : xs) es = inside f xs es
        left f (_ : xs) (e : es) = do
            e  <- toAbsOpArg (LeftOperandCtx f) e
            es <- inside f xs es
            return (e : es)
        left f (_  : _)  [] = __IMPOSSIBLE__
        left f []        _  = __IMPOSSIBLE__

        inside f [x]          es    = right f x es
        inside f (IdPart _ : xs) es = inside f xs es
        inside f (_  : xs) (e : es) = do
            e  <- toAbsOpArg InsideOperandCtx e
            es <- inside f xs es
            return (e : es)
        inside _ (_ : _) [] = __IMPOSSIBLE__
        inside _ []         _  = __IMPOSSIBLE__

        right _ (IdPart _)  [] = return []
        right f _          [e] = do
            e <- toAbsOpArg (RightOperandCtx f) e
            return [e]
        right _ _     _  = __IMPOSSIBLE__