{-# 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)
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
[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
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 =
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 [] = []
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
(a
a , TCState
s) <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving forall a b. (a -> b) -> a -> b
$ do
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 ->
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 }
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 }
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)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode TCM a
cont
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
[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
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'
[] -> forall (m :: * -> *). ReadTCState m => m ModuleName
curMName