{-| 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 (DLib cgn lib) = do addLib cgn lib addIBC (IBCLib cgn lib) directiveAction (DLink cgn obj) = do dirs <- allImportDirs o <- runIO $ findInPath dirs obj addIBC (IBCObj cgn obj) -- just name, search on loading ibc addObjectFile cgn o directiveAction (DFlag cgn flag) = do let flags = words flag mapM_ (\f -> addIBC (IBCCGFlag cgn f)) flags mapM_ (addFlag cgn) flags directiveAction (DInclude cgn hdr) = do addHdr cgn hdr addIBC (IBCHeader cgn hdr) directiveAction (DHide n') = do ns <- allNamespaces n' mapM_ (\n -> do setAccessibility n Hidden addIBC (IBCAccess n Hidden)) ns directiveAction (DFreeze n') = do ns <- allNamespaces n' mapM_ (\n -> do setAccessibility n Frozen addIBC (IBCAccess n Frozen)) ns directiveAction (DThaw n') = do ns <- allNamespaces n' mapM_ (\n -> do ctxt <- getContext case lookupDefAccExact n False ctxt of Just (_, Frozen) -> do setAccessibility n Public addIBC (IBCAccess n Public) _ -> throwError (Msg (show n ++ " is not frozen"))) ns directiveAction (DInjective n') = do ns <- allNamespaces n' mapM_ (\n -> do setInjectivity n True addIBC (IBCInjective n True)) ns directiveAction (DSetTotal n') = do ns <- allNamespaces n' mapM_ (\n -> do setTotality n (Total []) addIBC (IBCTotal n (Total []))) ns directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc }) directiveAction (DDefault tot) = do updateIState (\i -> i { default_total = tot }) directiveAction (DLogging lvl) = setLogLevel (fromInteger lvl) directiveAction (DDynamicLibs libs) = do added <- addDyLib libs case added of Left lib -> addIBC (IBCDyLib (lib_name lib)) Right msg -> fail msg directiveAction (DNameHint ty tyFC ns) = do ty' <- disambiguate ty mapM_ (addNameHint ty' . fst) ns mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns sendHighlighting $ S.fromList $ [(FC' tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (FC' fc, AnnBoundName n False)) ns directiveAction (DErrorHandlers fn nfc arg afc ns) = do fn' <- disambiguate fn ns' <- mapM (\(n, fc) -> do n' <- disambiguate 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 (\(n, fc) -> (FC' fc, AnnName n Nothing Nothing Nothing)) ns' directiveAction (DLanguage ext) = addLangExt ext directiveAction (DDeprecate n reason) = do n' <- disambiguate n addDeprecated n' reason addIBC (IBCDeprecate n' reason) directiveAction (DFragile n reason) = do n' <- disambiguate n addFragile n' reason addIBC (IBCFragile n' reason) directiveAction (DAutoImplicits b) = setAutoImpls b directiveAction (DUsed fc fn arg) = addUsedName fc fn arg disambiguate :: Name -> Idris Name disambiguate n = do i <- getIState case lookupCtxtName n (idris_implicits i) of [(n', _)] -> return n' [] -> throwError (NoSuchVariable n) more -> throwError (CantResolveAlts (map fst more)) allNamespaces :: Name -> Idris [Name] allNamespaces n = do i <- getIState case lookupCtxtName n (idris_implicits i) of [(n', _)] -> return [n'] [] -> throwError (NoSuchVariable n) more -> return (map fst more)