{-# LANGUAGE CPP #-}

module Agda.Compiler.Common where

import Data.List as List
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Data.Char
import Data.Function
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif

import Control.Monad
import Control.Monad.State

import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I

import Agda.Interaction.FindFile ( srcFilePath )
import Agda.Interaction.Options
import Agda.Interaction.Imports ( CheckResult, crInterface, crSource, Source(..) )

import Agda.TypeChecking.Monad

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Pretty

import Agda.Utils.Impossible

data IsMain = IsMain | NotMain
  deriving (IsMain -> IsMain -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsMain -> IsMain -> Bool
$c/= :: IsMain -> IsMain -> Bool
== :: IsMain -> IsMain -> Bool
$c== :: IsMain -> IsMain -> Bool
Eq, Int -> IsMain -> ShowS
[IsMain] -> ShowS
IsMain -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsMain] -> ShowS
$cshowList :: [IsMain] -> ShowS
show :: IsMain -> String
$cshow :: IsMain -> String
showsPrec :: Int -> IsMain -> ShowS
$cshowsPrec :: Int -> IsMain -> ShowS
Show)

-- | Conjunctive semigroup ('NotMain' is absorbing).
instance Semigroup IsMain where
  IsMain
NotMain <> :: IsMain -> IsMain -> IsMain
<> IsMain
_ = IsMain
NotMain
  IsMain
_       <> IsMain
NotMain = IsMain
NotMain
  IsMain
IsMain  <> IsMain
IsMain = IsMain
IsMain

instance Monoid IsMain where
  mempty :: IsMain
mempty = IsMain
IsMain
  mappend :: IsMain -> IsMain -> IsMain
mappend = forall a. Semigroup a => a -> a -> a
(<>)

doCompile :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile :: forall r.
Monoid r =>
(IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = do
  -- The Agda.Primitive module is implicitly assumed to be always imported,
  -- even though it not necesseraly occurs in iImportedModules.
  -- TODO: there should be a better way to get hold of Agda.Primitive?
  [Interface
agdaPrimInter] <- forall a. (a -> Bool) -> [a] -> [a]
filter ((String
"Agda.Primitive"forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
iModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
m (Map TopLevelModuleName ModuleInfo)
getVisitedModules
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT forall a. Set a
Set.empty forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a -> a -> a
mappend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
NotMain Interface
agdaPrimInter forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i

-- This helper function is called for both `Agda.Primitive` and the module in question.
-- It's also called for each imported module, recursively. (Avoiding duplicates).
doCompile'
  :: Monoid r
  => (IsMain -> Interface -> TCM r) -> (IsMain -> Interface -> StateT (Set ModuleName) TCM r)
doCompile' :: forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = do
  Bool
alreadyDone <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. Ord a => a -> Set a -> Bool
Set.member (Interface -> ModuleName
iModuleName Interface
i))
  if Bool
alreadyDone then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty else do
    [Interface]
imps <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> TopLevelModuleName
toTopLevelModuleName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
    r
ri <- forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
NotMain) [Interface]
imps
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Interface -> TCM ()
setInterface Interface
i
    r
r <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Ord a => a -> Set a -> Set a
Set.insert forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a -> a -> a
mappend r
ri r
r

setInterface :: Interface -> TCM ()
setInterface :: Interface -> TCM ()
setInterface Interface
i = do
  CommandLineOptions
opts <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC (PersistentTCState -> CommandLineOptions
stPersistentOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState)
  CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma (Interface -> [OptionsPragma]
iDefaultPragmaOptions Interface
i forall a. [a] -> [a] -> [a]
++ Interface -> [OptionsPragma]
iFilePragmaOptions Interface
i)
  Lens' (Set ModuleName) TCState
stImportedModules forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
  Lens' (Maybe ModuleName) TCState
stCurrentModule   forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` forall a. a -> Maybe a
Just (Interface -> ModuleName
iModuleName Interface
i)

curIF :: ReadTCState m => m Interface
curIF :: forall (m :: * -> *). ReadTCState m => m Interface
curIF = do
  ModuleName
name <- forall (m :: * -> *). ReadTCState m => m ModuleName
curMName
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ ModuleInfo -> Interface
miInterface forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule (ModuleName -> TopLevelModuleName
toTopLevelModuleName ModuleName
name)

curMName :: ReadTCState m => m ModuleName
curMName :: forall (m :: * -> *). ReadTCState m => m ModuleName
curMName = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe ModuleName) TCState
stCurrentModule

curDefs :: ReadTCState m => m Definitions
curDefs :: forall (m :: * -> *). ReadTCState m => m Definitions
curDefs = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Bool
defNoCompilation) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall o i. o -> Lens' i o -> i
^. Lens' Definitions Signature
sigDefinitions) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Signature
iSignature forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Interface
curIF

sortDefs :: Definitions -> [(QName, Definition)]
sortDefs :: Definitions -> [(QName, Definition)]
sortDefs Definitions
defs =
  -- The list is sorted to ensure that the order of the generated
  -- definitions does not depend on things like the number of bits
  -- in an Int (see Issue 1900).
  forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
  forall k v. HashMap k v -> [(k, v)]
HMap.toList Definitions
defs

compileDir :: HasOptions m => m FilePath
compileDir :: forall (m :: * -> *). HasOptions m => m String
compileDir = do
  Maybe String
mdir <- CommandLineOptions -> Maybe String
optCompileDir forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
mdir


repl :: [String] -> String -> String
repl :: OptionsPragma -> ShowS
repl OptionsPragma
subs = ShowS
go where
  go :: ShowS
go (Char
'<':Char
'<':Char
c:Char
'>':Char
'>':String
s) | Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length OptionsPragma
subs = OptionsPragma
subs forall a. [a] -> Int -> a
!! Int
i forall a. [a] -> [a] -> [a]
++ ShowS
go String
s
     where i :: Int
i = Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
  go (Char
c:String
s) = Char
c forall a. a -> [a] -> [a]
: ShowS
go String
s
  go []    = []


-- | Sets up the compilation environment.
inCompilerEnv :: CheckResult -> TCM a -> TCM a
inCompilerEnv :: forall a. CheckResult -> TCM a -> TCM a
inCompilerEnv CheckResult
checkResult TCM a
cont = do
  let mainI :: Interface
mainI = CheckResult -> Interface
crInterface CheckResult
checkResult
      checkedSource :: Source
checkedSource = CheckResult -> Source
crSource CheckResult
checkResult

  -- Preserve the state (the compiler modifies the state).
  -- Andreas, 2014-03-23 But we might want to collect Benchmark info,
  -- so use localTCState.
  -- FNF, 2017-02-22 we also want to keep the warnings we have encountered,
  -- so use localTCStateSaving and pick them out.
  (a
a , TCState
s) <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving forall a b. (a -> b) -> a -> b
$ do

    -- Compute the output directory. Note: using commandLineOptions would make
    -- the current pragma options persistent when we setCommandLineOptions
    -- below.
    CommandLineOptions
opts <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC forall a b. (a -> b) -> a -> b
$ PersistentTCState -> CommandLineOptions
stPersistentOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
    let compileDir :: String
compileDir = case CommandLineOptions -> Maybe String
optCompileDir CommandLineOptions
opts of
          Just String
dir -> String
dir
          Maybe String
Nothing  ->
            -- The default output directory is the project root.
            let tm :: TopLevelModuleName
tm = ModuleName -> TopLevelModuleName
toTopLevelModuleName forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
mainI
                f :: AbsolutePath
f  = SourceFile -> AbsolutePath
srcFilePath forall a b. (a -> b) -> a -> b
$ Source -> SourceFile
srcOrigin Source
checkedSource
            in AbsolutePath -> String
filePath forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> AbsolutePath
C.projectRoot AbsolutePath
f TopLevelModuleName
tm
    CommandLineOptions -> TCM ()
setCommandLineOptions forall a b. (a -> b) -> a -> b
$
      CommandLineOptions
opts { optCompileDir :: Maybe String
optCompileDir = forall a. a -> Maybe a
Just String
compileDir }

    -- Andreas, 2017-08-23, issue #2714 recover pragma option --no-main
    -- Unfortunately, a pragma option is stored in the interface file as
    -- just a list of strings, thus, the solution is a bit of hack:
    -- We match on whether @["--no-main"]@ is one of the stored options.
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([String
"--no-main"] forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Interface -> [OptionsPragma]
iFilePragmaOptions Interface
mainI) forall a b. (a -> b) -> a -> b
$
      Lens' PragmaOptions TCState
stPragmaOptions forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ PragmaOptions
o -> PragmaOptions
o { optCompileNoMain :: Bool
optCompileNoMain = Bool
True }

    -- Perhaps all pragma options from the top-level module should be
    -- made available to the compiler in a suitable way. Here are more
    -- hacks:
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String
"--cubical" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Interface -> [OptionsPragma]
iFilePragmaOptions Interface
mainI)) forall a b. (a -> b) -> a -> b
$
      Lens' PragmaOptions TCState
stPragmaOptions forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ PragmaOptions
o -> PragmaOptions
o { optCubical :: Maybe Cubical
optCubical = forall a. a -> Maybe a
Just Cubical
CFull }
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String
"--erased-cubical" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Interface -> [OptionsPragma]
iFilePragmaOptions Interface
mainI)) forall a b. (a -> b) -> a -> b
$
      Lens' PragmaOptions TCState
stPragmaOptions forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ PragmaOptions
o -> PragmaOptions
o { optCubical :: Maybe Cubical
optCubical = forall a. a -> Maybe a
Just Cubical
CErased }

    ScopeInfo -> TCM ()
setScope (Interface -> ScopeInfo
iInsideScope Interface
mainI) -- so that compiler errors don't use overly qualified names
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode TCM a
cont
  -- keep generated warnings
  let newWarnings :: [TCWarning]
newWarnings = PostScopeState -> [TCWarning]
stPostTCWarnings forall a b. (a -> b) -> a -> b
$  TCState -> PostScopeState
stPostScopeState forall a b. (a -> b) -> a -> b
$ TCState
s
  Lens' [TCWarning] TCState
stTCWarnings forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` [TCWarning]
newWarnings
  forall (m :: * -> *) a. Monad m => a -> m a
return a
a

topLevelModuleName :: ReadTCState m => ModuleName -> m ModuleName
topLevelModuleName :: forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
topLevelModuleName ModuleName
m = do
  -- get the names of the visited modules
  [ModuleName]
visited <- forall a b. (a -> b) -> [a] -> [b]
List.map (Interface -> ModuleName
iModuleName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> Interface
miInterface) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall (m :: * -> *).
ReadTCState m =>
m (Map TopLevelModuleName ModuleInfo)
getVisitedModules
  -- find the module with the longest matching prefix to m
  let ms :: [ModuleName]
ms = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList)) forall a b. (a -> b) -> a -> b
$
       forall a. (a -> Bool) -> [a] -> [a]
List.filter (\ ModuleName
m' -> ModuleName -> [Name]
mnameToList ModuleName
m' forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` ModuleName -> [Name]
mnameToList ModuleName
m) [ModuleName]
visited
  case [ModuleName]
ms of
    (ModuleName
m' : [ModuleName]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
m'
    -- if we did not get anything, it may be because m is a section
    -- (a module _ ), see e.g. #1866
    []       -> forall (m :: * -> *). ReadTCState m => m ModuleName
curMName