{-# LANGUAGE CPP #-}

module Agda.Compiler.Common where

import Prelude hiding ((!!))

import Data.List (sortBy, isPrefixOf)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import qualified Data.HashSet as HSet
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.Syntax.TopLevelModuleName

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

import Agda.TypeChecking.Monad as TCM

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1          ( pattern (:|) )
import Agda.Utils.Maybe
import Agda.Utils.Monad          ( ifNotM )
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
  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
$ StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim forall a b. (a -> b) -> a -> 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
  where
  -- The Agda.Primitive module is only loaded if the --no-load-primitives flag was not given,
  -- thus, only try to compile it if we have visited it.
  compilePrim :: StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim StateT (Set ModuleName) (TCMT IO) r
cont = do
    Maybe ModuleInfo
agdaPrim <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
      TopLevelModuleName
agdaPrim <- RawTopLevelModuleName -> TCM TopLevelModuleName
TCM.topLevelModuleName RawTopLevelModuleName
agdaPrim
      forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
agdaPrim forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m VisitedModules
getVisitedModules
    case Maybe ModuleInfo
agdaPrim of
      Maybe ModuleInfo
Nothing   -> StateT (Set ModuleName) (TCMT IO) r
cont
      Just ModuleInfo
prim ->
        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 (ModuleInfo -> Interface
miInterface ModuleInfo
prim) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (Set ModuleName) (TCMT IO) r
cont
    where
    agdaPrim :: RawTopLevelModuleName
agdaPrim = RawTopLevelModuleName
      { rawModuleNameRange :: Range
rawModuleNameRange = forall a. Monoid a => a
mempty
      , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = Text
"Agda" forall a. a -> [a] -> NonEmpty a
:| Text
"Primitive" forall a. a -> [a] -> [a]
: []
      }
      -- N.B. The Range in TopLevelModuleName is ignored for Ord, so we can set it to mempty.

-- 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
. forall a b. (a, b) -> a
fst) (Interface -> [(TopLevelModuleName, 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)
  -- One could perhaps make the following command lazy. Note, however,
  -- that it doesn't suffice to replace setTCLens' with setTCLens,
  -- because the stPreImportedModules field is strict.
  Lens' (HashSet TopLevelModuleName) TCState
stImportedModules forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens'`
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i))
  Lens' (Maybe (ModuleName, TopLevelModuleName)) TCState
stCurrentModule forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens'`
    forall a. a -> Maybe a
Just (Interface -> ModuleName
iModuleName Interface
i, Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)

curIF :: ReadTCState m => m Interface
curIF :: forall (m :: * -> *). ReadTCState m => m Interface
curIF = do
  TopLevelModuleName
name <- forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
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 TopLevelModuleName
name

curMName :: ReadTCState m => m TopLevelModuleName
curMName :: forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a, b) -> b
snd 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, TopLevelModuleName)) 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]
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. HasCallStack => [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 = Interface -> TopLevelModuleName
iTopLevelModuleName 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
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 TopLevelModuleName
topLevelModuleName :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
topLevelModuleName ModuleName
m = do
  -- Interfaces of visited modules.
  [Interface]
visited <- 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 VisitedModules
getVisitedModules
  -- find the module with the longest matching prefix to m
  let is :: [Interface]
is = 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
iModuleName)) forall a b. (a -> b) -> a -> b
$
           forall a. (a -> Bool) -> [a] -> [a]
filter (\Interface
i -> ModuleName -> [Name]
mnameToList (Interface -> ModuleName
iModuleName Interface
i) forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`
                         ModuleName -> [Name]
mnameToList ModuleName
m)
             [Interface]
visited
  case [Interface]
is of
    (Interface
i : [Interface]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
    -- 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 TopLevelModuleName
curMName