← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/Main.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/Main.hs
16
16
import System.Environment
17
17
import System.Exit
18
18
import System.FilePath
19
 
import qualified System.IO.UTF8 as UTF8
 
19
import qualified Agda.Utils.IO.Locale as LocIO
 
20
import System.Time
20
21
 
21
22
import Agda.Syntax.Position
22
23
import Agda.Syntax.Parser
34
35
import Agda.Interaction.CommandLine.CommandLine
35
36
import Agda.Interaction.Options
36
37
import Agda.Interaction.Monad
37
 
import Agda.Interaction.GhciTop ()      -- to make sure it compiles
 
38
import Agda.Interaction.GhciTop ()      -- to make sure it compiles
38
39
import qualified Agda.Interaction.Imports as Imp
39
40
import Agda.Interaction.Highlighting.HTML
40
41
 
64
65
 
65
66
-- | The main function
66
67
runAgda :: TCM ()
67
 
runAgda =
68
 
    do  progName <- liftIO getProgName
69
 
        argv     <- liftIO getArgs
70
 
        let opts = parseStandardOptions progName argv
71
 
        case opts of
72
 
            Left err -> liftIO $ optionError err
73
 
            Right opts
74
 
                | optShowHelp opts      -> liftIO printUsage
75
 
                | optShowVersion opts   -> liftIO printVersion
76
 
                | optRunTests opts      -> liftIO $ do
77
 
                    ok <- testSuite
78
 
                    unless ok exitFailure
79
 
                | isNothing (optInputFile opts)
80
 
                    && not (optInteractive opts)
81
 
                                        -> liftIO printUsage
82
 
                | otherwise             -> do setCommandLineOptions opts
83
 
                                              checkFile
84
 
    where
85
 
        checkFile :: TCM ()
86
 
        checkFile =
87
 
            do  i       <- optInteractive <$> liftTCM commandLineOptions
88
 
                compile <- optCompile <$> liftTCM commandLineOptions
89
 
                alonzo  <- optCompileAlonzo <$> liftTCM commandLineOptions
90
 
                malonzo <- optCompileMAlonzo <$> liftTCM commandLineOptions
91
 
                when i $ liftIO $ UTF8.putStr splashScreen
92
 
                let failIfError (_, Right _)  = return ()
93
 
                    failIfError (_, Left err) = typeError err
94
 
 
95
 
                    failIfNoInt (_, Right (Just i)) = return i
96
 
                    -- The allowed combinations of command-line
97
 
                    -- options should rule out Right Nothing here.
98
 
                    failIfNoInt (_, Right Nothing)  = __IMPOSSIBLE__
99
 
                    failIfNoInt (_, Left err)       = typeError err
100
 
 
101
 
                    interaction
102
 
                      :: TCM (ScopeInfo, Either TypeError (Maybe Interface))
103
 
                      -> TCM ()
104
 
                    interaction | i       = runIM . interactionLoop
105
 
                                | compile = Agate.compilerMain   . (failIfError =<<)
106
 
                                | alonzo  = Alonzo.compilerMain  . (failIfError =<<)
107
 
                                | malonzo = MAlonzo.compilerMain . (failIfNoInt =<<)
108
 
                                | otherwise = (failIfError =<<)
109
 
                interaction $
110
 
                    do  hasFile <- hasInputFile
111
 
                        resetState
112
 
                        if hasFile then
113
 
                            do  file    <- getInputFile
114
 
                                options <- commandLineOptions
115
 
 
116
 
                                (topLevel, ok) <- Imp.createInterface options
117
 
                                  noTrace [] Map.empty
118
 
                                  Map.empty emptySignature
119
 
                                  Map.empty Nothing file False
120
 
 
121
 
                                -- The value of options from above
122
 
                                -- cannot be reused here, because then
123
 
                                -- options set in pragmas would have
124
 
                                -- no effect.
125
 
                                unsolvedOK <- optAllowUnsolved <$> commandLineOptions
126
 
 
127
 
                                let result = case ok of
128
 
                                      Imp.Warnings []             [] -> __IMPOSSIBLE__
129
 
                                      Imp.Warnings _  unsolved@(_:_)
130
 
                                        | unsolvedOK -> Right Nothing
131
 
                                        | otherwise  -> Left $ UnsolvedMetas unsolved
132
 
                                      Imp.Warnings termErrs@(_:_) _  ->
133
 
                                        Left (TerminationCheckFailed termErrs)
134
 
                                      Imp.Success { Imp.cirInterface = i } ->
135
 
                                        Right (Just i)
136
 
 
137
 
                                -- Print stats
138
 
                                stats <- Map.toList <$> getStatistics
139
 
                                case stats of
140
 
                                    []  -> return ()
141
 
                                    _   -> liftIO $ do
142
 
                                        UTF8.putStrLn "Statistics"
143
 
                                        UTF8.putStrLn "----------"
144
 
                                        mapM_ (\ (s,n) -> UTF8.putStrLn $ s ++ " : " ++ show n) $
145
 
                                            sortBy (\x y -> compare (snd x) (snd y)) stats
146
 
 
147
 
                                whenM (optGenerateHTML <$> commandLineOptions) $ do
148
 
                                  case ok of
149
 
                                    Imp.Success {} -> generateHTML $ topLevelModuleName topLevel
150
 
                                    _ -> return ()
151
 
                                         -- The error will be handled by interaction.
152
 
 
153
 
                                return (insideScope topLevel, result)
154
 
                          else return (emptyScopeInfo, Right Nothing)
 
68
runAgda = do
 
69
  progName <- liftIO getProgName
 
70
  argv   <- liftIO getArgs
 
71
  let opts = parseStandardOptions progName argv
 
72
  case opts of
 
73
    Left err -> liftIO $ optionError err
 
74
    Right opts
 
75
      | optShowHelp opts    -> liftIO printUsage
 
76
      | optShowVersion opts -> liftIO printVersion
 
77
      | optRunTests opts    -> liftIO $ do
 
78
          ok <- testSuite
 
79
          unless ok exitFailure
 
80
      | isNothing (optInputFile opts)
 
81
          && not (optInteractive opts)
 
82
                            -> liftIO printUsage
 
83
      | otherwise           -> do
 
84
          setCommandLineOptions PersistentOptions opts
 
85
          checkFile
 
86
  where
 
87
    checkFile :: TCM ()
 
88
    checkFile = do
 
89
      i       <- optInteractive    <$> liftTCM commandLineOptions
 
90
      compile <- optCompile        <$> liftTCM commandLineOptions
 
91
      alonzo  <- optCompileAlonzo  <$> liftTCM commandLineOptions
 
92
      malonzo <- optCompileMAlonzo <$> liftTCM commandLineOptions
 
93
      when i $ liftIO $ LocIO.putStr splashScreen
 
94
      let failIfNoInt (Just i) = return i
 
95
          -- The allowed combinations of command-line
 
96
          -- options should rule out Nothing here.
 
97
          failIfNoInt Nothing  = __IMPOSSIBLE__
 
98
 
 
99
          interaction :: TCM (Maybe Interface) -> TCM ()
 
100
          interaction | i         = runIM . interactionLoop
 
101
                      | compile   = Agate.compilerMain         . (() <$)
 
102
                      | alonzo    = Alonzo.compilerMain        . (() <$)
 
103
                      | malonzo   = (MAlonzo.compilerMain =<<) . (failIfNoInt =<<)
 
104
                      | otherwise = (() <$)
 
105
      interaction $ do
 
106
        hasFile <- hasInputFile
 
107
        resetState
 
108
        if not hasFile then return Nothing else do
 
109
          file    <- getInputFile
 
110
          (i, mw) <- Imp.typeCheck file Imp.CurrentDir Nothing
 
111
 
 
112
          unsolvedOK <- optAllowUnsolved <$> commandLineOptions
 
113
 
 
114
          result <- case mw of
 
115
            Just (Imp.Warnings [] [] []) -> __IMPOSSIBLE__
 
116
            Just (Imp.Warnings _ unsolved@(_:_) _)
 
117
              | not unsolvedOK -> typeError $ UnsolvedMetas unsolved
 
118
            Just (Imp.Warnings _ _ unsolved@(_:_))
 
119
              | not unsolvedOK -> typeError $ UnsolvedConstraints unsolved
 
120
            Just (Imp.Warnings termErrs@(_:_) _ _) ->
 
121
              typeError $ TerminationCheckFailed termErrs
 
122
            Just _  -> return Nothing
 
123
            Nothing -> return $ Just i
 
124
 
 
125
          -- Print stats
 
126
          stats <- Map.toList <$> getStatistics
 
127
          case stats of
 
128
            []      -> return ()
 
129
            _       -> liftIO $ do
 
130
              LocIO.putStrLn "Statistics"
 
131
              LocIO.putStrLn "----------"
 
132
              mapM_ (\ (s,n) -> LocIO.putStrLn $ s ++ " : " ++ show n) $
 
133
                sortBy (\x y -> compare (snd x) (snd y)) stats
 
134
 
 
135
          whenM (optGenerateHTML <$> commandLineOptions) $ do
 
136
            case mw of
 
137
              Nothing -> generateHTML $ iModuleName i
 
138
              Just _  -> reportSLn "" 1
 
139
                "HTML is not generated (unsolved meta-variables)."
 
140
 
 
141
          return result
155
142
 
156
143
-- | Print usage information.
157
144
printUsage :: IO ()
158
 
printUsage =
159
 
    do  progName <- getProgName
160
 
        UTF8.putStr $ usage standardOptions_ [] progName
 
145
printUsage = do
 
146
  progName <- getProgName
 
147
  LocIO.putStr $ usage standardOptions_ [] progName
161
148
 
162
149
-- | Print version information.
163
150
printVersion :: IO ()
164
151
printVersion =
165
 
    UTF8.putStrLn $ "Agda version " ++ version
 
152
  LocIO.putStrLn $ "Agda version " ++ version
166
153
 
167
154
-- | What to do for bad options.
168
155
optionError :: String -> IO ()
169
 
optionError err =
170
 
    do  UTF8.putStrLn $ "Error: " ++ err
171
 
        printUsage
172
 
        exitFailure
 
156
optionError err = do
 
157
  LocIO.putStrLn $ "Error: " ++ err
 
158
  printUsage
 
159
  exitFailure
173
160
 
174
161
-- | Main
175
162
main :: IO ()
176
163
main = do
177
164
    r <- runTCM $ runAgda `catchError` \err -> do
178
 
        s <- prettyError err
179
 
        liftIO $ UTF8.putStrLn s
180
 
        throwError err
 
165
      s <- prettyError err
 
166
      liftIO $ LocIO.putStrLn s
 
167
      throwError err
181
168
    case r of
182
 
        Right _ -> exitSuccess
183
 
        Left _  -> exitFailure
 
169
      Right _ -> exitSuccess
 
170
      Left _  -> exitFailure
184
171
  `catchImpossible` \e -> do
185
 
    UTF8.putStr $ show e
 
172
    LocIO.putStr $ show e
186
173
    exitFailure
187
174