← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Main.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Main.hs
1
1
{-# LANGUAGE CPP #-}
2
 
{-# LANGUAGE PatternGuards #-}
3
2
 
4
3
{-| Agda main module.
5
4
-}
6
5
module Agda.Main where
7
6
 
8
7
import Control.Monad.State
9
 
import Control.Monad.Error
10
8
import Control.Applicative
11
9
 
12
10
import qualified Data.List as List
39
37
import Agda.Compiler.Epic.Compiler as Epic
40
38
import Agda.Compiler.JS.Compiler as JS
41
39
 
 
40
import Agda.Utils.Lens
42
41
import Agda.Utils.Monad
 
42
import Agda.Utils.Pretty (prettyShow)
 
43
import Agda.Utils.String
43
44
import qualified Agda.Utils.Trie as Trie
44
45
 
45
46
import Agda.Tests
46
47
import Agda.Version
47
48
 
 
49
import Agda.Utils.Except ( MonadError(catchError, throwError) )
 
50
import Agda.Utils.Impossible
 
51
 
48
52
#include "undefined.h"
49
 
import Agda.Utils.Impossible
50
53
 
51
54
-- | The main function
52
55
runAgda :: TCM ()
83
86
                       map (Boxes.text . showAccount) $
84
87
                       accounts
85
88
                -- Second column is times.
86
 
                -- CPU times are in pico seconds, convert to milliseconds.
87
89
                col2 = Boxes.vcat Boxes.right $
88
 
                       map (Boxes.text . (++ " ms") . show . (`div` 1000000000)) $
 
90
                       map (Boxes.text . prettyShow) $
89
91
                       times
90
92
                table = Boxes.hsep 1 Boxes.left [col1, col2]
91
93
            reportBenchmarkingLn $ Boxes.render table
 
94
 
 
95
          -- Print accumulated statistics.
 
96
          printStatistics 20 Nothing =<< use lensAccumStatistics
 
97
 
92
98
  where
93
99
    checkFile :: TCM ()
94
100
    checkFile = do
129
135
 
130
136
          unsolvedOK <- optAllowUnsolved <$> pragmaOptions
131
137
 
 
138
          -- Reported unsolved problems as error unless unsolvedOK.
 
139
          -- An interface is only generated if NoWarnings.
132
140
          result <- case mw of
133
 
                          -- we get here if there are unfilled interaction
134
 
                          -- points that have been solved by unification
135
 
            SomeWarnings (Warnings [] [] []) -> return Nothing
136
 
            SomeWarnings (Warnings _ unsolved@(_:_) _)
137
 
              | not unsolvedOK -> typeError $ UnsolvedMetas unsolved
138
 
            SomeWarnings (Warnings _ _ unsolved@(_:_))
139
 
              | not unsolvedOK -> typeError $ UnsolvedConstraints unsolved
140
 
            SomeWarnings (Warnings termErrs@(_:_) _ _) ->
141
 
              typeError $ TerminationCheckFailed termErrs
142
 
            SomeWarnings _  -> return Nothing
143
 
            NoWarnings -> return $ Just i
 
141
            -- Unsolved metas.
 
142
            SomeWarnings (Warnings w@(_:_) _)
 
143
              | not unsolvedOK                 -> typeError $ UnsolvedMetas w
 
144
            -- Unsolved constraints.
 
145
            SomeWarnings (Warnings _ w@(_:_))
 
146
              | not unsolvedOK                 -> typeError $ UnsolvedConstraints w
 
147
            -- Unsolved metas, unsolved constraints, or
 
148
            -- interaction points left whose metas have been solved
 
149
            -- automatically.  (See Issue 1296).
 
150
            SomeWarnings (Warnings _ _)        -> return Nothing
 
151
            NoWarnings                         -> return $ Just i
144
152
 
145
153
          whenM (optGenerateHTML <$> commandLineOptions) $
146
154
            generateHTML