{-|
Module      : Idris.Directives
Description : Act upon Idris directives.

License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.Directives(directiveAction) where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Imports
import Idris.Output (sendHighlighting)

import qualified Data.Set as S

import Util.DynamicLinker

-- | Run the action corresponding to a directive
directiveAction :: Directive -> Idris ()
directiveAction :: Directive -> Idris ()
directiveAction (DLib Codegen
cgn String
lib) = do
  Codegen -> String -> Idris ()
addLib Codegen
cgn String
lib
  IBCWrite -> Idris ()
addIBC (Codegen -> String -> IBCWrite
IBCLib Codegen
cgn String
lib)

directiveAction (DLink Codegen
cgn String
obj) = do
  [String]
dirs <- Idris [String]
allImportDirs
  String
o <- IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> IO String
findInPath [String]
dirs String
obj
  IBCWrite -> Idris ()
addIBC (Codegen -> String -> IBCWrite
IBCObj Codegen
cgn String
obj) -- just name, search on loading ibc
  Codegen -> String -> Idris ()
addObjectFile Codegen
cgn String
o

directiveAction (DFlag Codegen
cgn String
flag) = do
  let flags :: [String]
flags = String -> [String]
words String
flag
  (String -> Idris ()) -> [String] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\String
f -> IBCWrite -> Idris ()
addIBC (Codegen -> String -> IBCWrite
IBCCGFlag Codegen
cgn String
f)) [String]
flags
  (String -> Idris ()) -> [String] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Codegen -> String -> Idris ()
addFlag Codegen
cgn) [String]
flags

directiveAction (DInclude Codegen
cgn String
hdr) = do
  Codegen -> String -> Idris ()
addHdr Codegen
cgn String
hdr
  IBCWrite -> Idris ()
addIBC (Codegen -> String -> IBCWrite
IBCHeader Codegen
cgn String
hdr)

directiveAction (DHide Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Hidden
            IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
Hidden)) [Name]
ns
directiveAction (DFreeze Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Frozen
            IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
Frozen)) [Name]
ns
directiveAction (DThaw Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do
            Context
ctxt <- Idris Context
getContext
            case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False Context
ctxt of
                 Just (Def
_, Accessibility
Frozen) -> do Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Public
                                        IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
Public)
                 Maybe (Def, Accessibility)
_ -> Err -> Idris ()
forall a. Err -> Idris a
throwError (String -> Err
forall t. String -> Err' t
Msg (Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not frozen"))) [Name]
ns
directiveAction (DInjective Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do
            Name -> Bool -> Idris ()
setInjectivity Name
n Bool
True
            IBCWrite -> Idris ()
addIBC (Name -> Bool -> IBCWrite
IBCInjective Name
n Bool
True)) [Name]
ns
directiveAction (DSetTotal Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do
            Name -> Totality -> Idris ()
setTotality Name
n ([Int] -> Totality
Total [])
            IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
n ([Int] -> Totality
Total []))) [Name]
ns

directiveAction (DAccess Accessibility
acc) = do (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { default_access = acc })

directiveAction (DDefault DefaultTotality
tot) =  do (IState -> IState) -> Idris ()
updateIState (\IState
i -> IState
i { default_total = tot })

directiveAction (DLogging Integer
lvl) = Int -> Idris ()
setLogLevel (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
lvl)

directiveAction (DDynamicLibs [String]
libs) = do
  Either DynamicLib String
added <- [String] -> Idris (Either DynamicLib String)
addDyLib [String]
libs
  case Either DynamicLib String
added of
    Left DynamicLib
lib  -> IBCWrite -> Idris ()
addIBC (String -> IBCWrite
IBCDyLib (DynamicLib -> String
lib_name DynamicLib
lib))
    Right String
msg -> String -> Idris ()
forall a. String -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
msg

directiveAction (DNameHint Name
ty FC
tyFC [(Name, FC)]
ns) = do
  Name
ty' <- Name -> Idris Name
disambiguate Name
ty
  ((Name, FC) -> Idris ()) -> [(Name, FC)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name -> Name -> Idris ()
addNameHint Name
ty' (Name -> Idris ())
-> ((Name, FC) -> Name) -> (Name, FC) -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst) [(Name, FC)]
ns
  ((Name, FC) -> Idris ()) -> [(Name, FC)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name, FC)
n -> IBCWrite -> Idris ()
addIBC ((Name, Name) -> IBCWrite
IBCNameHint (Name
ty', (Name, FC) -> Name
forall a b. (a, b) -> a
fst (Name, FC)
n))) [(Name, FC)]
ns
  Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList ([(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation))
-> [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ [(FC -> FC'
FC' FC
tyFC, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
ty' Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)] [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++ ((Name, FC) -> (FC', OutputAnnotation))
-> [(Name, FC)] -> [(FC', OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
fc) -> (FC -> FC'
FC' FC
fc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
n Bool
False)) [(Name, FC)]
ns

directiveAction (DErrorHandlers Name
fn FC
nfc Name
arg FC
afc [(Name, FC)]
ns) = do
  Name
fn' <- Name -> Idris Name
disambiguate Name
fn
  [(Name, FC)]
ns' <- ((Name, FC) -> StateT IState (ExceptT Err IO) (Name, FC))
-> [(Name, FC)] -> StateT IState (ExceptT Err IO) [(Name, FC)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Name
n, FC
fc) -> do
                  Name
n' <- Name -> Idris Name
disambiguate Name
n
                  (Name, FC) -> StateT IState (ExceptT Err IO) (Name, FC)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n', FC
fc)) [(Name, FC)]
ns
  Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers Name
fn' Name
arg (((Name, FC) -> Name) -> [(Name, FC)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, FC) -> Name
forall a b. (a, b) -> a
fst [(Name, FC)]
ns')
  ((Name, FC) -> Idris ()) -> [(Name, FC)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IBCWrite -> Idris ()
addIBC (IBCWrite -> Idris ())
-> ((Name, FC) -> IBCWrite) -> (Name, FC) -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name -> Name -> IBCWrite
IBCFunctionErrorHandler Name
fn' Name
arg (Name -> IBCWrite)
-> ((Name, FC) -> Name) -> (Name, FC) -> IBCWrite
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst) [(Name, FC)]
ns'
  Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList ([(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation))
-> [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
       [ (FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
fn' Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)
       , (FC -> FC'
FC' FC
afc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
arg Bool
False)
       ] [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++ ((Name, FC) -> (FC', OutputAnnotation))
-> [(Name, FC)] -> [(FC', OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
fc) -> (FC -> FC'
FC' FC
fc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)) [(Name, FC)]
ns'

directiveAction (DLanguage LanguageExt
ext) = LanguageExt -> Idris ()
addLangExt LanguageExt
ext

directiveAction (DDeprecate Name
n String
reason) = do
  Name
n' <- Name -> Idris Name
disambiguate Name
n
  Name -> String -> Idris ()
addDeprecated Name
n' String
reason
  IBCWrite -> Idris ()
addIBC (Name -> String -> IBCWrite
IBCDeprecate Name
n' String
reason)

directiveAction (DFragile Name
n String
reason) = do
  Name
n' <- Name -> Idris Name
disambiguate Name
n
  Name -> String -> Idris ()
addFragile Name
n' String
reason
  IBCWrite -> Idris ()
addIBC (Name -> String -> IBCWrite
IBCFragile Name
n' String
reason)

directiveAction (DAutoImplicits Bool
b) = Bool -> Idris ()
setAutoImpls Bool
b
directiveAction (DUsed FC
fc Name
fn Name
arg)  = FC -> Name -> Name -> Idris ()
addUsedName FC
fc Name
fn Name
arg

disambiguate :: Name -> Idris Name
disambiguate :: Name -> Idris Name
disambiguate Name
n = do
  IState
i <- Idris IState
getIState
  case Name -> Ctxt [PArg] -> [(Name, [PArg])]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
    [(Name
n', [PArg]
_)] -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
    []        -> Err -> Idris Name
forall a. Err -> Idris a
throwError (Name -> Err
forall t. Name -> Err' t
NoSuchVariable Name
n)
    [(Name, [PArg])]
more      -> Err -> Idris Name
forall a. Err -> Idris a
throwError ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Name, [PArg]) -> Name) -> [(Name, [PArg])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [PArg]) -> Name
forall a b. (a, b) -> a
fst [(Name, [PArg])]
more))


allNamespaces :: Name -> Idris [Name]
allNamespaces :: Name -> Idris [Name]
allNamespaces Name
n = do
  IState
i <- Idris IState
getIState
  case Name -> Ctxt [PArg] -> [(Name, [PArg])]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
    [(Name
n', [PArg]
_)] -> [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name
n']
    []        -> Err -> Idris [Name]
forall a. Err -> Idris a
throwError (Name -> Err
forall t. Name -> Err' t
NoSuchVariable Name
n)
    [(Name, [PArg])]
more      -> [Name] -> Idris [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, [PArg]) -> Name) -> [(Name, [PArg])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [PArg]) -> Name
forall a b. (a, b) -> a
fst [(Name, [PArg])]
more)