← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Monad/Options.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-05 23:43:20 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu
Tags: 2.2.6-1
http://bugs.debian.org/559197
* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian) 
* debian/README.source: Remove, no repacking so not necessary any more 
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed. 
    (Closes: #559197). 
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/Options.hs
6
6
import Control.Monad.State
7
7
import Data.Maybe
8
8
import Text.PrettyPrint
9
 
import qualified System.IO.UTF8 as UTF8
 
9
import qualified Agda.Utils.IO.Locale as LocIO
10
10
import System.Directory
 
11
import System.FilePath
11
12
 
12
13
import Agda.TypeChecking.Monad.Base
13
14
import Agda.Interaction.Options
14
15
import Agda.Syntax.Abstract
 
16
import Agda.Utils.FileName
15
17
import Agda.Utils.Monad
16
18
import Agda.Utils.List
17
19
import Agda.Utils.Trie (Trie)
20
22
#include "../../undefined.h"
21
23
import Agda.Utils.Impossible
22
24
 
23
 
 
24
 
setCommandLineOptions :: MonadTCM tcm => CommandLineOptions -> tcm ()
25
 
setCommandLineOptions opts =
 
25
-- | Does the operation apply to the persistent options or only to the
 
26
-- pragma options? In the former case the pragma options are also
 
27
-- updated.
 
28
 
 
29
data Target = PersistentOptions | PragmaOptions
 
30
 
 
31
-- | Sets the command line options.
 
32
--
 
33
-- Ensures that the 'optInputFile' field contains an absolute path.
 
34
--
 
35
-- An empty list of include directories is interpreted as @["."]@.
 
36
 
 
37
setCommandLineOptions
 
38
  :: MonadTCM tcm
 
39
  => Target
 
40
  -> CommandLineOptions
 
41
  -> tcm ()
 
42
setCommandLineOptions target opts =
26
43
  case checkOpts opts of
27
44
    Left err   -> __IMPOSSIBLE__
28
45
    Right opts -> do
34
49
          -- canonicalizePath seems to return absolute paths.
35
50
          f <- liftIO $ canonicalizePath f
36
51
          return (opts { optInputFile = Just f })
37
 
      liftTCM $ modify $ \s -> s { stOptions = opts }
 
52
      let newOpts = opts { optIncludeDirs =
 
53
              case optIncludeDirs opts of
 
54
                [] -> ["."]
 
55
                is -> is
 
56
            }
 
57
      case target of
 
58
        PersistentOptions ->
 
59
          modify $ \s -> s { stPersistentOptions = newOpts
 
60
                           , stPragmaOptions     = newOpts
 
61
                           }
 
62
        PragmaOptions ->
 
63
          modify $ \s -> s { stPragmaOptions     = newOpts
 
64
                           }
38
65
 
39
66
commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions
40
 
commandLineOptions = liftTCM $ gets stOptions
 
67
commandLineOptions = liftTCM $ gets stPragmaOptions
41
68
 
42
69
setOptionsFromPragma :: MonadTCM tcm => Pragma -> tcm ()
43
70
setOptionsFromPragma (OptionsPragma xs) = do
44
71
    opts <- commandLineOptions
45
72
    case parsePragmaOptions xs opts of
46
73
        Left err    -> typeError $ GenericError err
47
 
        Right opts' -> setCommandLineOptions opts'
 
74
        Right opts' -> setCommandLineOptions PragmaOptions opts'
48
75
setOptionsFromPragma _ = return ()
49
76
 
50
77
setOptionsFromPragmas :: MonadTCM tcm => [Pragma] -> tcm ()
72
99
shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool
73
100
shouldReifyInteractionPoints = asks envReifyInteractionPoints
74
101
 
75
 
getIncludeDirs :: MonadTCM tcm => tcm [FilePath]
76
 
getIncludeDirs = addDot . optIncludeDirs <$> commandLineOptions
77
 
    where
78
 
        addDot [] = ["."]   -- if there are no include dirs we use .
79
 
        addDot is = is
 
102
-- | Gets the include directories.
 
103
 
 
104
getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]
 
105
getIncludeDirs =
 
106
  map mkAbsolute . optIncludeDirs <$> commandLineOptions
 
107
 
 
108
-- | Makes the include directories absolute.
 
109
--
 
110
-- Relative directories are made absolute with respect to the given
 
111
-- path.
 
112
 
 
113
makeIncludeDirsAbsolute :: MonadTCM tcm => AbsolutePath -> tcm ()
 
114
makeIncludeDirsAbsolute root = do
 
115
  opts <- commandLineOptions
 
116
  setCommandLineOptions PersistentOptions $
 
117
    opts { optIncludeDirs =
 
118
             map (filePath root </>) $ optIncludeDirs opts }
80
119
 
81
120
setInputFile :: MonadTCM tcm => FilePath -> tcm ()
82
121
setInputFile file =
83
122
    do  opts <- commandLineOptions
84
 
        setCommandLineOptions $ opts { optInputFile = Just file }
 
123
        setCommandLineOptions PersistentOptions $
 
124
          opts { optInputFile = Just file }
85
125
 
86
126
-- | Should only be run if 'hasInputFile'.
87
127
getInputFile :: MonadTCM tcm => tcm FilePath
97
137
proofIrrelevance :: MonadTCM tcm => tcm Bool
98
138
proofIrrelevance = optProofIrrelevance <$> commandLineOptions
99
139
 
 
140
hasUniversePolymorphism :: MonadTCM tcm => tcm Bool
 
141
hasUniversePolymorphism = optUniversePolymorphism <$> commandLineOptions
 
142
 
100
143
showImplicitArguments :: MonadTCM tcm => tcm Bool
101
144
showImplicitArguments = optShowImplicit <$> commandLineOptions
102
145
 
104
147
setShowImplicitArguments showImp ret = do
105
148
  opts <- commandLineOptions
106
149
  let imp = optShowImplicit opts
107
 
  setCommandLineOptions $ opts { optShowImplicit = showImp }
 
150
  setCommandLineOptions PersistentOptions $
 
151
    opts { optShowImplicit = showImp }
108
152
  x <- ret
109
153
  opts <- commandLineOptions
110
 
  setCommandLineOptions $ opts { optShowImplicit = imp }
 
154
  setCommandLineOptions PersistentOptions $
 
155
    opts { optShowImplicit = imp }
111
156
  return x
112
157
 
113
158
ignoreInterfaces :: MonadTCM tcm => tcm Bool
134
179
    when (n <= m) action
135
180
 
136
181
reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
137
 
reportS k n s = verboseS k n $ liftIO $ UTF8.putStr s
 
182
reportS k n s = verboseS k n $ liftIO $ LocIO.putStr s
138
183
 
139
184
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
140
 
reportSLn k n s = verboseS k n $ liftIO $ UTF8.putStrLn s
 
185
reportSLn k n s = verboseS k n $ liftIO $ LocIO.putStrLn s
141
186
 
142
187
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()
143
 
reportSDoc k n d = verboseS k n $ liftIO . UTF8.print =<< d
 
188
reportSDoc k n d = verboseS k n $ liftIO . LocIO.print =<< d
144
189