{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.Compiler.Common
  ( module Mikan.Compiler.Common
  , IsMain(..)
  )
  where

import Prelude hiding ((!!))

import Data.List (sortBy, isPrefixOf)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.HashMap.Strict qualified as HMap
import Data.Char
import Data.Function (on)

import Control.Monad
import Control.Monad.State

import Mikan.Syntax.Common
import Mikan.Syntax.Internal as I
import Mikan.Syntax.TopLevelModuleName

import Mikan.Interaction.Options
import Mikan.Interaction.Imports  ( CheckResult, crInterface, crSource )
import Mikan.Interaction.Library

import Mikan.TypeChecking.Monad as TCM

import Mikan.Utils.List
import Mikan.Utils.List1          ( pattern (:|) )
import Mikan.Utils.Maybe
import Mikan.Utils.WithDefault    ( lensCollapseDefault )
import Mikan.Utils.Tuple.Strict (Pair(..))
import Mikan.Utils.Tuple.Strict qualified as Strict
import Mikan.Utils.Maybe.Strict qualified as Strict

import Mikan.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
  -- 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
    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 = ShortText
"Agda" ShortText -> [ShortText] -> TopLevelModuleNameParts
forall a. a -> [a] -> NonEmpty a
:| ShortText
"Primitive" ShortText -> [ShortText] -> [ShortText]
forall a. a -> [a] -> [a]
: []
      , rawModuleNameInferred :: Bool
rawModuleNameInferred = Bool
False
      }
      -- 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
  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)
  -- 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.
  stImportedModules `setTCLens`
    Set.fromList (map' fst (iImportedModules i))
  stCurrentModule `setTCLens`
    Strict.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
-> (Pair ModuleName TopLevelModuleName -> TopLevelModuleName)
-> Maybe (Pair ModuleName TopLevelModuleName)
-> TopLevelModuleName
forall b a. b -> (a -> b) -> Maybe a -> b
Strict.maybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ Pair ModuleName TopLevelModuleName -> TopLevelModuleName
forall a b. Pair a b -> b
Strict.snd (Maybe (Pair ModuleName TopLevelModuleName) -> TopLevelModuleName)
-> m (Maybe (Pair ModuleName TopLevelModuleName))
-> m TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getter TCState (Maybe (Pair ModuleName TopLevelModuleName))
-> m (Maybe (Pair ModuleName TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Maybe (Pair ModuleName TopLevelModuleName)
 -> f (Maybe (Pair ModuleName TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (Pair ModuleName TopLevelModuleName))
Getter TCState (Maybe (Pair 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
-> Getting Definitions Signature Definitions -> Definitions
forall s a. s -> Getting a s a -> a
^. Getting Definitions Signature Definitions
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 =
  -- 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).
  ((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


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 []    = []


-- | 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 , 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

    -- 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.
    let iFilePragmaStrings :: Interface -> [[String]]
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
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([String
"--no-main"] [String] -> [[String]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Interface -> [[String]]
iFilePragmaStrings Interface
mainI) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      ASetter' TCState Bool -> Bool -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ((PragmaOptions -> Identity PragmaOptions)
-> TCState -> Identity TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> Identity PragmaOptions)
 -> TCState -> Identity TCState)
-> ((Bool -> Identity Bool)
    -> PragmaOptions -> Identity PragmaOptions)
-> ASetter' TCState Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithDefault 'True -> Identity (WithDefault 'True))
-> PragmaOptions -> Identity PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
lensOptCompileMain ((WithDefault 'True -> Identity (WithDefault 'True))
 -> PragmaOptions -> Identity PragmaOptions)
-> ((Bool -> Identity Bool)
    -> WithDefault 'True -> Identity (WithDefault 'True))
-> (Bool -> Identity Bool)
-> PragmaOptions
-> Identity PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Identity Bool)
-> WithDefault 'True -> Identity (WithDefault 'True)
forall a (b :: Bool).
(Boolean a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'True) Bool
lensCollapseDefault) Bool
False

    ScopeInfo -> TCMT IO ()
setScope (ScopeInfo -> TCMT IO ()) -> ScopeInfo -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
mainI -- so that compiler errors don't use overly qualified names
    -- András, 2025-08-30: this is a fresh creation of a scope from an interface
    -- so inverse scopes don't yet exist.
    TCMT IO ()
forall (m :: * -> *). MonadTCState m => m ()
recomputeInverseScope
    TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode TCM a
cont
  -- keep generated warnings
  let newWarnings = TCState
s TCState
-> Getting (Set TCWarning) TCState (Set TCWarning) -> Set TCWarning
forall s a. s -> Getting a s a -> a
^. Getting (Set TCWarning) TCState (Set TCWarning)
Lens' TCState (Set TCWarning)
stTCWarnings
  stTCWarnings `setTCLens` newWarnings
  return a

topLevelModuleName ::
  ReadTCState m => ModuleName -> m TopLevelModuleName
topLevelModuleName :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
topLevelModuleName ModuleName
m = do
  -- Interfaces of visited modules.
  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
  -- find the module with the longest matching prefix to m
  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)
    -- if we did not get anything, it may be because m is a section
    -- (a module _ ), see e.g. #1866
    []       -> m TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName