git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Directives.hs
129 lines 4.0 kB history raw
1{-|
2Module : Idris.Directives
3Description : Act upon Idris directives.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8module Idris.Directives(directiveAction) where
10import Idris.AbsSyntax
11import Idris.ASTUtils
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import Idris.Imports
15import Idris.Output (sendHighlighting)
17import Util.DynamicLinker
19-- | Run the action corresponding to a directive
20directiveAction :: Directive -> Idris ()
21directiveAction (DLib cgn lib) = do
22 addLib cgn lib
23 addIBC (IBCLib cgn lib)
25directiveAction (DLink cgn obj) = do
26 dirs <- allImportDirs
27 o <- runIO $ findInPath dirs obj
28 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
29 addObjectFile cgn o
31directiveAction (DFlag cgn flag) = do
32 let flags = words flag
33 mapM_ (\f -> addIBC (IBCCGFlag cgn f)) flags
34 mapM_ (addFlag cgn) flags
36directiveAction (DInclude cgn hdr) = do
37 addHdr cgn hdr
38 addIBC (IBCHeader cgn hdr)
40directiveAction (DHide n') = do
41 ns <- allNamespaces n'
42 mapM_ (\n -> do
43 setAccessibility n Hidden
44 addIBC (IBCAccess n Hidden)) ns
45directiveAction (DFreeze n') = do
46 ns <- allNamespaces n'
47 mapM_ (\n -> do
48 setAccessibility n Frozen
49 addIBC (IBCAccess n Frozen)) ns
50directiveAction (DThaw n') = do
51 ns <- allNamespaces n'
52 mapM_ (\n -> do
53 ctxt <- getContext
54 case lookupDefAccExact n False ctxt of
55 Just (_, Frozen) -> do setAccessibility n Public
56 addIBC (IBCAccess n Public)
57 _ -> throwError (Msg (show n ++ " is not frozen"))) ns
58directiveAction (DInjective n') = do
59 ns <- allNamespaces n'
60 mapM_ (\n -> do
61 setInjectivity n True
62 addIBC (IBCInjective n True)) ns
63directiveAction (DSetTotal n') = do
64 ns <- allNamespaces n'
65 mapM_ (\n -> do
66 setTotality n (Total [])
67 addIBC (IBCTotal n (Total []))) ns
69directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })
71directiveAction (DDefault tot) = do updateIState (\i -> i { default_total = tot })
73directiveAction (DLogging lvl) = setLogLevel (fromInteger lvl)
75directiveAction (DDynamicLibs libs) = do
76 added <- addDyLib libs
77 case added of
78 Left lib -> addIBC (IBCDyLib (lib_name lib))
79 Right msg -> fail msg
81directiveAction (DNameHint ty tyFC ns) = do
82 ty' <- disambiguate ty
83 mapM_ (addNameHint ty' . fst) ns
84 mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns
85 sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns
87directiveAction (DErrorHandlers fn nfc arg afc ns) = do
88 fn' <- disambiguate fn
89 ns' <- mapM (\(n, fc) -> do
90 n' <- disambiguate n
91 return (n', fc)) ns
92 addFunctionErrorHandlers fn' arg (map fst ns')
93 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'
94 sendHighlighting $
95 [ (nfc, AnnName fn' Nothing Nothing Nothing)
96 , (afc, AnnBoundName arg False)
97 ] ++ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'
99directiveAction (DLanguage ext) = addLangExt ext
101directiveAction (DDeprecate n reason) = do
102 n' <- disambiguate n
103 addDeprecated n' reason
104 addIBC (IBCDeprecate n' reason)
106directiveAction (DFragile n reason) = do
107 n' <- disambiguate n
108 addFragile n' reason
109 addIBC (IBCFragile n' reason)
111directiveAction (DAutoImplicits b) = setAutoImpls b
112directiveAction (DUsed fc fn arg) = addUsedName fc fn arg
114disambiguate :: Name -> Idris Name
115disambiguate n = do
116 i <- getIState
117 case lookupCtxtName n (idris_implicits i) of
118 [(n', _)] -> return n'
119 [] -> throwError (NoSuchVariable n)
120 more -> throwError (CantResolveAlts (map fst more))
123allNamespaces :: Name -> Idris [Name]
124allNamespaces n = do
125 i <- getIState
126 case lookupCtxtName n (idris_implicits i) of
127 [(n', _)] -> return [n']
128 [] -> throwError (NoSuchVariable n)
129 more -> return (map fst more)