git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/Directives.hs
128 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.Core.Evaluate
12import Idris.Core.TT
13import Idris.Imports
14import Idris.Output (sendHighlighting)
16import Util.DynamicLinker
18-- | Run the action corresponding to a directive
19directiveAction :: Directive -> Idris ()
20directiveAction (DLib cgn lib) = do
21 addLib cgn lib
22 addIBC (IBCLib cgn lib)
24directiveAction (DLink cgn obj) = do
25 dirs <- allImportDirs
26 o <- runIO $ findInPath dirs obj
27 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
28 addObjectFile cgn o
30directiveAction (DFlag cgn flag) = do
31 let flags = words flag
32 mapM_ (\f -> addIBC (IBCCGFlag cgn f)) flags
33 mapM_ (addFlag cgn) flags
35directiveAction (DInclude cgn hdr) = do
36 addHdr cgn hdr
37 addIBC (IBCHeader cgn hdr)
39directiveAction (DHide n') = do
40 ns <- allNamespaces n'
41 mapM_ (\n -> do
42 setAccessibility n Hidden
43 addIBC (IBCAccess n Hidden)) ns
44directiveAction (DFreeze n') = do
45 ns <- allNamespaces n'
46 mapM_ (\n -> do
47 setAccessibility n Frozen
48 addIBC (IBCAccess n Frozen)) ns
49directiveAction (DThaw n') = do
50 ns <- allNamespaces n'
51 mapM_ (\n -> do
52 ctxt <- getContext
53 case lookupDefAccExact n False ctxt of
54 Just (_, Frozen) -> do setAccessibility n Public
55 addIBC (IBCAccess n Public)
56 _ -> throwError (Msg (show n ++ " is not frozen"))) ns
57directiveAction (DInjective n') = do
58 ns <- allNamespaces n'
59 mapM_ (\n -> do
60 setInjectivity n True
61 addIBC (IBCInjective n True)) ns
62directiveAction (DSetTotal n') = do
63 ns <- allNamespaces n'
64 mapM_ (\n -> do
65 setTotality n (Total [])
66 addIBC (IBCTotal n (Total []))) ns
68directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })
70directiveAction (DDefault tot) = do updateIState (\i -> i { default_total = tot })
72directiveAction (DLogging lvl) = setLogLevel (fromInteger lvl)
74directiveAction (DDynamicLibs libs) = do
75 added <- addDyLib libs
76 case added of
77 Left lib -> addIBC (IBCDyLib (lib_name lib))
78 Right msg -> fail msg
80directiveAction (DNameHint ty tyFC ns) = do
81 ty' <- disambiguate ty
82 mapM_ (addNameHint ty' . fst) ns
83 mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns
84 sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns
86directiveAction (DErrorHandlers fn nfc arg afc ns) = do
87 fn' <- disambiguate fn
88 ns' <- mapM (\(n, fc) -> do
89 n' <- disambiguate n
90 return (n', fc)) ns
91 addFunctionErrorHandlers fn' arg (map fst ns')
92 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'
93 sendHighlighting $
94 [ (nfc, AnnName fn' Nothing Nothing Nothing)
95 , (afc, AnnBoundName arg False)
96 ] ++ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'
98directiveAction (DLanguage ext) = addLangExt ext
100directiveAction (DDeprecate n reason) = do
101 n' <- disambiguate n
102 addDeprecated n' reason
103 addIBC (IBCDeprecate n' reason)
105directiveAction (DFragile n reason) = do
106 n' <- disambiguate n
107 addFragile n' reason
108 addIBC (IBCFragile n' reason)
110directiveAction (DAutoImplicits b) = setAutoImpls b
111directiveAction (DUsed fc fn arg) = addUsedName fc fn arg
113disambiguate :: Name -> Idris Name
114disambiguate n = do
115 i <- getIState
116 case lookupCtxtName n (idris_implicits i) of
117 [(n', _)] -> return n'
118 [] -> throwError (NoSuchVariable n)
119 more -> throwError (CantResolveAlts (map fst more))
122allNamespaces :: Name -> Idris [Name]
123allNamespaces n = do
124 i <- getIState
125 case lookupCtxtName n (idris_implicits i) of
126 [(n', _)] -> return [n']
127 [] -> throwError (NoSuchVariable n)
128 more -> return (map fst more)