{-|
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 <- forall a. IO a -> Idris a
runIO 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
  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
  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'
  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'
  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'
  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)
_ -> forall a. Err -> Idris a
throwError (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" is not frozen"))) [Name]
ns
directiveAction (DInjective Name
n') = do
  [Name]
ns <- Name -> Idris [Name]
allNamespaces Name
n'
  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'
  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 :: Accessibility
default_access = Accessibility
acc })

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

directiveAction (DLogging Integer
lvl) = Int -> Idris ()
setLogLevel (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 -> 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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name -> Name -> Idris ()
addNameHint Name
ty' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, FC)]
ns
  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', forall a b. (a, b) -> a
fst (Name, FC)
n))) [(Name, FC)]
ns
  Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ [(FC -> FC'
FC' FC
tyFC, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
ty' forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)] forall a. [a] -> [a] -> [a]
++ 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Name
n, FC
fc) -> do
                  Name
n' <- Name -> Idris Name
disambiguate Name
n
                  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 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, FC)]
ns')
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IBCWrite -> Idris ()
addIBC forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name -> Name -> IBCWrite
IBCFunctionErrorHandler Name
fn' Name
arg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, FC)]
ns'
  Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$
       [ (FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
fn' forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)
       , (FC -> FC'
FC' FC
afc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
arg Bool
False)
       ] forall a. [a] -> [a] -> [a]
++ 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 forall a. Maybe a
Nothing forall a. Maybe a
Nothing 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 forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
    [(Name
n', [PArg]
_)] -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
    []        -> forall a. Err -> Idris a
throwError (forall t. Name -> Err' t
NoSuchVariable Name
n)
    [(Name, [PArg])]
more      -> forall a. Err -> Idris a
throwError (forall t. [Name] -> Err' t
CantResolveAlts (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
    [(Name
n', [PArg]
_)] -> forall (m :: * -> *) a. Monad m => a -> m a
return [Name
n']
    []        -> forall a. Err -> Idris a
throwError (forall t. Name -> Err' t
NoSuchVariable Name
n)
    [(Name, [PArg])]
more      -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, [PArg])]
more)