{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Compiler.Common
( module Agda.Compiler.Common
, IsMain(..)
)
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 Data.Char
import Data.Function (on)
import Control.Monad
import Control.Monad.State
import Agda.Syntax.Common
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.Interaction.Library
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.WithDefault ( lensCollapseDefault )
import Agda.Utils.Impossible
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
(StateT (Set ModuleName) (TCMT IO) r -> Set ModuleName -> TCM r)
-> Set ModuleName -> StateT (Set ModuleName) (TCMT IO) r -> TCM r
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Set ModuleName) (TCMT IO) r -> Set ModuleName -> TCM r
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Set ModuleName
forall a. Set a
Set.empty (StateT (Set ModuleName) (TCMT IO) r -> TCM r)
-> StateT (Set ModuleName) (TCMT IO) r -> TCM r
forall a b. (a -> b) -> a -> b
$ StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim (StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
forall a b. (a -> b) -> a -> b
$ (IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
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
compilePrim :: StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim StateT (Set ModuleName) (TCMT IO) r
cont = do
agdaPrim <- TCMT IO (Maybe ModuleInfo)
-> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Set ModuleName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Maybe ModuleInfo)
-> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo))
-> TCMT IO (Maybe ModuleInfo)
-> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo)
forall a b. (a -> b) -> a -> b
$ do
agdaPrim <- RawTopLevelModuleName -> TCM TopLevelModuleName
TCM.topLevelModuleName RawTopLevelModuleName
agdaPrim
Map.lookup agdaPrim <$> getVisitedModules
case agdaPrim of
Maybe ModuleInfo
Nothing -> StateT (Set ModuleName) (TCMT IO) r
cont
Just ModuleInfo
prim ->
r -> r -> r
forall a. Monoid a => a -> a -> a
mappend (r -> r -> r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) (r -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
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) StateT (Set ModuleName) (TCMT IO) (r -> r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
forall a b.
StateT (Set ModuleName) (TCMT IO) (a -> b)
-> StateT (Set ModuleName) (TCMT IO) a
-> StateT (Set ModuleName) (TCMT IO) b
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 = Range
forall a. Monoid a => a
mempty
, rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = Text
"Agda" Text -> [Text] -> TopLevelModuleNameParts
forall a. a -> [a] -> NonEmpty a
:| Text
"Primitive" Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: []
}
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
alreadyDone <- (Set ModuleName -> Bool) -> StateT (Set ModuleName) (TCMT IO) Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Interface -> ModuleName
iModuleName Interface
i))
if alreadyDone then return mempty else do
imps <- lift $
map miInterface . catMaybes <$>
mapM (getVisitedModule . fst) (iImportedModules i)
ri <- mconcat <$> mapM (doCompile' f NotMain) imps
lift $ setInterface i
r <- lift $ f isMain i
modify (Set.insert $ iModuleName i)
return $ mappend ri r
setInterface :: Interface -> TCM ()
setInterface :: Interface -> TCMT IO ()
setInterface Interface
i = do
opts <- (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC (PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState)
setCommandLineOptions opts
mapM_ setOptionsFromPragma (iDefaultPragmaOptions i ++ iFilePragmaOptions i)
stImportedModules `setTCLens'`
Set.fromList (map fst (iImportedModules i))
stCurrentModule `setTCLens'`
Just (iModuleName i, iTopLevelModuleName i)
curIF :: ReadTCState m => m Interface
curIF :: forall (m :: * -> *). ReadTCState m => m Interface
curIF = do
name <- m TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
maybe __IMPOSSIBLE__ miInterface <$> getVisitedModule name
curMName :: ReadTCState m => m TopLevelModuleName
curMName :: forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName = TopLevelModuleName
-> ((ModuleName, TopLevelModuleName) -> TopLevelModuleName)
-> Maybe (ModuleName, TopLevelModuleName)
-> TopLevelModuleName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (ModuleName, TopLevelModuleName) -> TopLevelModuleName
forall a b. (a, b) -> b
snd (Maybe (ModuleName, TopLevelModuleName) -> TopLevelModuleName)
-> m (Maybe (ModuleName, TopLevelModuleName))
-> m TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
-> m (Maybe (ModuleName, TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule
curDefs :: ReadTCState m => m Definitions
curDefs :: forall (m :: * -> *). ReadTCState m => m Definitions
curDefs = (Definition -> Bool) -> Definitions -> Definitions
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Bool
defNoCompilation) (Definitions -> Definitions)
-> (Interface -> Definitions) -> Interface -> Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signature -> Lens' Signature Definitions -> Definitions
forall o i. o -> Lens' o i -> i
^. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Signature Definitions
sigDefinitions) (Signature -> Definitions)
-> (Interface -> Signature) -> Interface -> Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Signature
iSignature (Interface -> Definitions) -> m Interface -> m Definitions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
sortDefs :: Definitions -> [(QName, Definition)]
sortDefs :: Definitions -> [(QName, Definition)]
sortDefs Definitions
defs =
((QName, Definition) -> (QName, Definition) -> Ordering)
-> [(QName, Definition)] -> [(QName, Definition)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (QName -> QName -> Ordering)
-> ((QName, Definition) -> QName)
-> (QName, Definition)
-> (QName, Definition)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (QName, Definition) -> QName
forall a b. (a, b) -> a
fst) ([(QName, Definition)] -> [(QName, Definition)])
-> [(QName, Definition)] -> [(QName, Definition)]
forall a b. (a -> b) -> a -> b
$
Definitions -> [(QName, Definition)]
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
mdir <- CommandLineOptions -> Maybe String
optCompileDir (CommandLineOptions -> Maybe String)
-> m CommandLineOptions -> m (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
maybe __IMPOSSIBLE__ return mdir
repl :: [String] -> String -> String
repl :: [String] -> String -> String
repl [String]
subs = String -> String
go where
go :: String -> String
go (Char
'<':Char
'<':Char
c:Char
'>':Char
'>':String
s) | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
subs = [String]
subs [String] -> Int -> String
forall a. HasCallStack => [a] -> Int -> a
!! Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
go String
s
where i :: Int
i = Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
go (Char
c:String
s) = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
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 , s) <- TCM a -> TCM (a, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving (TCM a -> TCM (a, TCState)) -> TCM a -> TCM (a, TCState)
forall a b. (a -> b) -> a -> b
$ do
opts <- (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions)
-> (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
let compileDir = case CommandLineOptions -> Maybe String
optCompileDir CommandLineOptions
opts of
Just String
dir -> String
dir
Maybe String
Nothing ->
let tm :: TopLevelModuleName
tm = Interface -> TopLevelModuleName
iTopLevelModuleName Interface
mainI
f :: AbsolutePath
f = SourceFile -> AbsolutePath
srcFilePath (SourceFile -> AbsolutePath) -> SourceFile -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> SourceFile
srcOrigin Source
checkedSource
in AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
f TopLevelModuleName
tm
setCommandLineOptions $
opts { optCompileDir = Just compileDir }
let iFilePragmaStrings = (OptionsPragma -> [String]) -> [OptionsPragma] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map OptionsPragma -> [String]
pragmaStrings ([OptionsPragma] -> [[String]])
-> (Interface -> [OptionsPragma]) -> Interface -> [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> [OptionsPragma]
iFilePragmaOptions
when (["--no-main"] `elem` iFilePragmaStrings mainI) $
setTCLens (stPragmaOptions . lensOptCompileMain . lensCollapseDefault) False
when (any ("--cubical" `elem`) $ iFilePragmaStrings mainI) $
setTCLens (stPragmaOptions . lensOptCubical) $ Just CFull
when (any ("--erased-cubical" `elem`) $ iFilePragmaStrings mainI) $
setTCLens (stPragmaOptions . lensOptCubical) $ Just CErased
setScope (iInsideScope mainI)
ignoreAbstractMode cont
let newWarnings = PostScopeState -> [TCWarning]
stPostTCWarnings (PostScopeState -> [TCWarning]) -> PostScopeState -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ TCState -> PostScopeState
stPostScopeState (TCState -> PostScopeState) -> TCState -> PostScopeState
forall a b. (a -> b) -> a -> b
$ TCState
s
stTCWarnings `setTCLens` newWarnings
return a
topLevelModuleName ::
ReadTCState m => ModuleName -> m TopLevelModuleName
topLevelModuleName :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
topLevelModuleName ModuleName
m = do
visited <- (ModuleInfo -> Interface) -> [ModuleInfo] -> [Interface]
forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface ([ModuleInfo] -> [Interface])
-> (Map TopLevelModuleName ModuleInfo -> [ModuleInfo])
-> Map TopLevelModuleName ModuleInfo
-> [Interface]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TopLevelModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
Map.elems (Map TopLevelModuleName ModuleInfo -> [Interface])
-> m (Map TopLevelModuleName ModuleInfo) -> m [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
m (Map TopLevelModuleName ModuleInfo)
getVisitedModules
let is = (Interface -> Interface -> Ordering) -> [Interface] -> [Interface]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Interface -> Int) -> Interface -> Interface -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Name] -> Int) -> (Interface -> [Name]) -> Interface -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList (ModuleName -> [Name])
-> (Interface -> ModuleName) -> Interface -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
iModuleName)) ([Interface] -> [Interface]) -> [Interface] -> [Interface]
forall a b. (a -> b) -> a -> b
$
(Interface -> Bool) -> [Interface] -> [Interface]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Interface
i -> ModuleName -> [Name]
mnameToList (Interface -> ModuleName
iModuleName Interface
i) [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`
ModuleName -> [Name]
mnameToList ModuleName
m)
[Interface]
visited
case is of
(Interface
i : [Interface]
_) -> TopLevelModuleName -> m TopLevelModuleName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
[] -> m TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName