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