{-|
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
  dirs <- Idris [String]
allImportDirs
  o <- runIO $ findInPath dirs obj
  addIBC (IBCObj cgn obj) -- just name, search on loading ibc
  addObjectFile cgn 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
  ns <- Name -> Idris [Name]
allNamespaces Name
n'
  mapM_ (\Name
n -> do
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Hidden
            IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
Hidden)) ns
directiveAction (DFreeze Name
n') = do
  ns <- Name -> Idris [Name]
allNamespaces Name
n'
  mapM_ (\Name
n -> do
            Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
Frozen
            IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
Frozen)) ns
directiveAction (DThaw Name
n') = do
  ns <- Name -> Idris [Name]
allNamespaces Name
n'
  mapM_ (\Name
n -> do
            ctxt <- Idris Context
getContext
            case lookupDefAccExact n False 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"))) ns
directiveAction (DInjective Name
n') = do
  ns <- Name -> Idris [Name]
allNamespaces Name
n'
  mapM_ (\Name
n -> do
            Name -> Bool -> Idris ()
setInjectivity Name
n Bool
True
            IBCWrite -> Idris ()
addIBC (Name -> Bool -> IBCWrite
IBCInjective Name
n Bool
True)) ns
directiveAction (DSetTotal Name
n') = do
  ns <- Name -> Idris [Name]
allNamespaces Name
n'
  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 []))) 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
  added <- [String] -> Idris (Either DynamicLib String)
addDyLib [String]
libs
  case 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
  ty' <- Name -> Idris Name
disambiguate Name
ty
  mapM_ (addNameHint ty' . fst) ns
  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))) ns
  sendHighlighting $ S.fromList $ [(FC' tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(Name
n, FC
fc) -> (FC -> FC'
FC' FC
fc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
n Bool
False)) ns

directiveAction (DErrorHandlers Name
fn FC
nfc Name
arg FC
afc [(Name, FC)]
ns) = do
  fn' <- Name -> Idris Name
disambiguate Name
fn
  ns' <- mapM (\(Name
n, FC
fc) -> do
                  n' <- Name -> Idris Name
disambiguate Name
n
                  return (n', fc)) ns
  addFunctionErrorHandlers fn' arg (map fst ns')
  mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'
  sendHighlighting $ S.fromList $
       [ (FC' nfc, AnnName fn' Nothing Nothing Nothing)
       , (FC' afc, AnnBoundName arg False)
       ] ++ 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)) ns'

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

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

directiveAction (DFragile Name
n String
reason) = do
  n' <- Name -> Idris Name
disambiguate Name
n
  addFragile n' reason
  addIBC (IBCFragile n' 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
  i <- Idris IState
getIState
  case lookupCtxtName n (idris_implicits 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
  i <- Idris IState
getIState
  case lookupCtxtName n (idris_implicits 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)