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

« back to all changes in this revision

Viewing changes to src/full/Agda/Interaction/Options.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

files added:
README.md

src/data/postprocess-latex.pl

src/full/Agda/TypeChecking/Rewriting.hs

src/full/Agda/TypeChecking/Rewriting.hs-boot

src/full/Agda/TypeChecking/Unquote.hs

src/full/Agda/Utils/AssocList.hs

src/full/Agda/Utils/Bag.hs

src/full/Agda/Utils/Empty.hs

src/full/Agda/Utils/Except.hs

src/full/Agda/Utils/IORef.hs

src/full/Agda/Utils/Lens

src/full/Agda/Utils/Lens.hs

src/full/Agda/Utils/Lens/Examples.hs

src/full/Agda/Utils/Permutation

src/full/Agda/Utils/Permutation/Tests.hs

src/full/undefined.h

files removed:
README

src/full/Agda/Utils/Fresh.hs

src/full/Agda/Utils/Unicode.hs

src/full/Agda/undefined.h

files modified:
Agda.cabal

CHANGELOG

debian/changelog

debian/control

debian/rules

dist/build/Agda/Syntax/Parser/Lexer.hs

dist/build/Agda/Syntax/Parser/Parser.hs

src/data/agda.sty

src/data/emacs-mode/agda2-highlight.el

src/data/emacs-mode/agda2-mode.el

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/CaseSplit.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/NarrowingSearch.hs

src/full/Agda/Auto/SearchControl.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Auto/Typecheck.hs

src/full/Agda/Compiler/CallCompiler.hs

src/full/Agda/Compiler/Epic/AuxAST.hs

src/full/Agda/Compiler/Epic/CompileState.hs

src/full/Agda/Compiler/Epic/Compiler.hs

src/full/Agda/Compiler/Epic/Epic.hs

src/full/Agda/Compiler/Epic/Erasure.hs

src/full/Agda/Compiler/Epic/ForceConstrs.hs

src/full/Agda/Compiler/Epic/Forcing.hs

src/full/Agda/Compiler/Epic/FromAgda.hs

src/full/Agda/Compiler/Epic/Injection.hs

src/full/Agda/Compiler/Epic/Interface.hs

src/full/Agda/Compiler/Epic/NatDetection.hs

src/full/Agda/Compiler/Epic/Primitive.hs

src/full/Agda/Compiler/Epic/Smashing.hs

src/full/Agda/Compiler/Epic/Static.hs

src/full/Agda/Compiler/HaskellTypes.hs

src/full/Agda/Compiler/JS/Case.hs

src/full/Agda/Compiler/JS/Compiler.hs

src/full/Agda/Compiler/JS/Syntax.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs

src/full/Agda/Compiler/MAlonzo/Encode.hs

src/full/Agda/Compiler/MAlonzo/Misc.hs

src/full/Agda/Compiler/MAlonzo/Pretty.hs

src/full/Agda/Compiler/MAlonzo/Primitives.hs

src/full/Agda/ImpossibleTest.hs

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine/CommandLine.hs

src/full/Agda/Interaction/EmacsCommand.hs

src/full/Agda/Interaction/EmacsTop.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/Highlighting/Dot.hs

src/full/Agda/Interaction/Highlighting/Emacs.hs

src/full/Agda/Interaction/Highlighting/Generate.hs

src/full/Agda/Interaction/Highlighting/HTML.hs

src/full/Agda/Interaction/Highlighting/LaTeX.hs

src/full/Agda/Interaction/Highlighting/Precise.hs

src/full/Agda/Interaction/Highlighting/Range.hs

src/full/Agda/Interaction/Highlighting/Vim.hs

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/InteractionTop.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Interaction/Options/Lenses.hs

src/full/Agda/Interaction/Response.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Copatterns.hs

src/full/Agda/Syntax/Abstract/Name.hs

src/full/Agda/Syntax/Abstract/Pretty.hs

src/full/Agda/Syntax/Abstract/Views.hs

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete.hs

src/full/Agda/Syntax/Concrete/Definitions.hs

src/full/Agda/Syntax/Concrete/Generic.hs

src/full/Agda/Syntax/Concrete/Name.hs

src/full/Agda/Syntax/Concrete/Operators.hs

src/full/Agda/Syntax/Concrete/Operators/Parser.hs

src/full/Agda/Syntax/Concrete/Pretty.hs

src/full/Agda/Syntax/Fixity.hs

src/full/Agda/Syntax/Info.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Internal/Defs.hs

src/full/Agda/Syntax/Internal/Generic.hs

src/full/Agda/Syntax/Internal/Pattern.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Notation.hs

src/full/Agda/Syntax/Parser.hs

src/full/Agda/Syntax/Parser/Alex.hs

src/full/Agda/Syntax/Parser/Comments.hs

src/full/Agda/Syntax/Parser/Layout.hs

src/full/Agda/Syntax/Parser/LexActions.hs

src/full/Agda/Syntax/Parser/Lexer.x

src/full/Agda/Syntax/Parser/LookAhead.hs

src/full/Agda/Syntax/Parser/Monad.hs

src/full/Agda/Syntax/Parser/Parser.y

src/full/Agda/Syntax/Parser/StringLiterals.hs

src/full/Agda/Syntax/Parser/Tokens.hs

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Scope/Base.hs

src/full/Agda/Syntax/Scope/Monad.hs

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

src/full/Agda/Termination/CallGraph.hs

src/full/Agda/Termination/CallMatrix.hs

src/full/Agda/Termination/Inlining.hs

src/full/Agda/Termination/Monad.hs

src/full/Agda/Termination/Order.hs

src/full/Agda/Termination/RecCheck.hs

src/full/Agda/Termination/Semiring.hs

src/full/Agda/Termination/SparseMatrix.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TheTypeChecker.hs

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/CheckInternal.hs

src/full/Agda/TypeChecking/CompiledClause.hs

src/full/Agda/TypeChecking/CompiledClause/Compile.hs

src/full/Agda/TypeChecking/CompiledClause/Match.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Coverage.hs

src/full/Agda/TypeChecking/Coverage/Match.hs

src/full/Agda/TypeChecking/Coverage/SplitTree.hs

src/full/Agda/TypeChecking/Datatypes.hs

src/full/Agda/TypeChecking/DisplayForm.hs

src/full/Agda/TypeChecking/DropArgs.hs

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/EtaContract.hs

src/full/Agda/TypeChecking/Forcing.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Implicit.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/InstanceArguments.hs

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/LevelConstraints.hs

src/full/Agda/TypeChecking/MetaVars.hs

src/full/Agda/TypeChecking/MetaVars.hs-boot

src/full/Agda/TypeChecking/MetaVars/Mention.hs

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

src/full/Agda/TypeChecking/Monad/Base.hs

src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs

src/full/Agda/TypeChecking/Monad/Base/KillRange.hs

src/full/Agda/TypeChecking/Monad/Benchmark.hs

src/full/Agda/TypeChecking/Monad/Builtin.hs

src/full/Agda/TypeChecking/Monad/Closure.hs

src/full/Agda/TypeChecking/Monad/Constraints.hs

src/full/Agda/TypeChecking/Monad/Context.hs

src/full/Agda/TypeChecking/Monad/Debug.hs

src/full/Agda/TypeChecking/Monad/Env.hs

src/full/Agda/TypeChecking/Monad/Exception.hs

src/full/Agda/TypeChecking/Monad/Imports.hs

src/full/Agda/TypeChecking/Monad/MetaVars.hs

src/full/Agda/TypeChecking/Monad/Mutual.hs

src/full/Agda/TypeChecking/Monad/Open.hs

src/full/Agda/TypeChecking/Monad/Options.hs

src/full/Agda/TypeChecking/Monad/Sharing.hs

src/full/Agda/TypeChecking/Monad/Signature.hs

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

src/full/Agda/TypeChecking/Monad/State.hs

src/full/Agda/TypeChecking/Monad/Statistics.hs

src/full/Agda/TypeChecking/Monad/Trace.hs

src/full/Agda/TypeChecking/Patterns/Abstract.hs

src/full/Agda/TypeChecking/Patterns/Match.hs

src/full/Agda/TypeChecking/Polarity.hs

src/full/Agda/TypeChecking/Positivity.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Pretty.hs-boot

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/ProjectionLike.hs

src/full/Agda/TypeChecking/Quote.hs

src/full/Agda/TypeChecking/RecordPatterns.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Reduce/Monad.hs

src/full/Agda/TypeChecking/Rules/Builtin.hs

src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs

src/full/Agda/TypeChecking/Rules/Data.hs

src/full/Agda/TypeChecking/Rules/Decl.hs

src/full/Agda/TypeChecking/Rules/Decl.hs-boot

src/full/Agda/TypeChecking/Rules/Def.hs

src/full/Agda/TypeChecking/Rules/Def.hs-boot

src/full/Agda/TypeChecking/Rules/LHS.hs

src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs

src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

src/full/Agda/TypeChecking/Rules/LHS/Problem.hs

src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs

src/full/Agda/TypeChecking/Rules/LHS/Split.hs

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

src/full/Agda/TypeChecking/Rules/Record.hs

src/full/Agda/TypeChecking/Rules/Term.hs

src/full/Agda/TypeChecking/Rules/Term.hs-boot

src/full/Agda/TypeChecking/Serialise.hs

src/full/Agda/TypeChecking/SizedTypes.hs

src/full/Agda/TypeChecking/SizedTypes/Solve.hs

src/full/Agda/TypeChecking/SizedTypes/Syntax.hs

src/full/Agda/TypeChecking/SizedTypes/Tests.hs

src/full/Agda/TypeChecking/SizedTypes/Utils.hs

src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/SyntacticEquality.hs

src/full/Agda/TypeChecking/Telescope.hs

src/full/Agda/TypeChecking/Test/Generators.hs

src/full/Agda/TypeChecking/Tests.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/BiMap.hs

src/full/Agda/Utils/Char.hs

src/full/Agda/Utils/Cluster.hs

src/full/Agda/Utils/Either.hs

src/full/Agda/Utils/Favorites.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Function.hs

src/full/Agda/Utils/Functor.hs

src/full/Agda/Utils/Geniplate.hs

src/full/Agda/Utils/Graph/AdjacencyMap.hs

src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs

src/full/Agda/Utils/HashMap.hs

src/full/Agda/Utils/IO/UTF8.hs

src/full/Agda/Utils/List.hs

src/full/Agda/Utils/Map.hs

src/full/Agda/Utils/Maybe.hs

src/full/Agda/Utils/Maybe/Strict.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/Null.hs

src/full/Agda/Utils/PartialOrd.hs

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/Pretty.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/SemiRing.hs

src/full/Agda/Utils/Size.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/Time.hs

src/full/Agda/Utils/Trie.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/Update.hs

src/full/Agda/Utils/VarSet.hs

src/full/Agda/Utils/Warshall.hs

src/full/Agda/Version.hs

Show diffs side-by-side

added added

removed removed

src/full/Agda/Interaction/Options.hs

{-# LANGUAGE CPP #-}

{-# LANGUAGE DeriveFunctor #-}

#if __GLASGOW_HASKELL__ <= 706

{-# LANGUAGE DeriveFunctor #-}

{-# LANGUAGE StandaloneDeriving #-}

#endif

module Agda.Interaction.Options

( CommandLineOptions(..)

) where

import Control.Monad ( when )

import Control.Monad.Error ( MonadError(..) )

import Data.Maybe ( isJust )

import Data.List ( isSuffixOf , intercalate )

import System.Console.GetOpt ( getOpt, usageInfo, ArgOrder(ReturnInOrder)

, OptDescr(..), ArgDescr(..)

)

import Data.List ( isSuffixOf , intercalate )

import System.Console.GetOpt ( getOpt, usageInfo, ArgOrder(ReturnInOrder)

, OptDescr(..), ArgDescr(..)

)

import Agda.Termination.CutOff ( CutOff(..) )

import Agda.Utils.TestHelpers ( runTests )

import Agda.Utils.QuickCheck ( quickCheck' )

import Agda.Utils.FileName ( AbsolutePath )

import Agda.Utils.Monad ( readM )

import Agda.Utils.List ( wordsBy )

import Agda.Utils.String ( indent )

import Agda.Utils.Trie ( Trie )

import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Except ( MonadError(catchError, throwError) )

-- | This should probably go somewhere else.

isLiterate :: FilePath -> Bool

isLiterate file = ".lagda" `isSuffixOf` file

-- interpreted as @["."]@ (see

-- 'Agda.TypeChecking.Monad.Options.makeIncludeDirsAbsolute').

data CommandLineOptions =

Options { optProgramName :: String

, optInputFile :: Maybe FilePath

, optIncludeDirs :: IncludeDirs

, optShowVersion :: Bool

, optShowHelp :: Bool

, optInteractive :: Bool

, optRunTests :: Bool

, optGHCiInteraction :: Bool

, optCompile :: Bool

, optCompileNoMain :: Bool

, optEpicCompile :: Bool

, optJSCompile :: Bool

, optCompileDir :: Maybe FilePath

-- ^ In the absence of a path the project root is used.

, optGenerateVimFile :: Bool

, optGenerateLaTeX :: Bool

, optGenerateHTML :: Bool

, optDependencyGraph :: Maybe FilePath

, optLaTeXDir :: FilePath

, optHTMLDir :: FilePath

, optCSSFile :: Maybe FilePath

, optIgnoreInterfaces :: Bool

, optForcing :: Bool

, optGhcFlags :: [String]

, optPragmaOptions :: PragmaOptions

, optEpicFlags :: [String]

, optSafe :: Bool

}

deriving Show

data CommandLineOptions = Options

{ optProgramName :: String

, optInputFile :: Maybe FilePath

, optIncludeDirs :: IncludeDirs

, optShowVersion :: Bool

, optShowHelp :: Bool

, optInteractive :: Bool

, optRunTests :: Bool

, optGHCiInteraction :: Bool

, optCompile :: Bool

, optCompileNoMain :: Bool

, optEpicCompile :: Bool

, optJSCompile :: Bool

, optCompileDir :: Maybe FilePath

-- ^ In the absence of a path the project root is used.

, optGenerateVimFile :: Bool

, optGenerateLaTeX :: Bool

, optGenerateHTML :: Bool

, optDependencyGraph :: Maybe FilePath

, optLaTeXDir :: FilePath

, optHTMLDir :: FilePath

, optCSSFile :: Maybe FilePath

, optIgnoreInterfaces :: Bool

, optForcing :: Bool

, optGhcFlags :: [String]

, optPragmaOptions :: PragmaOptions

, optEpicFlags :: [String]

, optSafe :: Bool

}

100

deriving Show

101

102

-- | Options which can be set in a pragma.

103

140

144

defaultInteractionOptions = defaultPragmaOptions

141

145

142

146

defaultOptions :: CommandLineOptions

143

defaultOptions =

144

Options { optProgramName = "agda"

145

, optInputFile = Nothing

146

, optIncludeDirs = Left []

147

, optShowVersion = False

148

, optShowHelp = False

149

, optInteractive = False

150

, optRunTests = False

151

, optGHCiInteraction = False

152

, optCompile = False

153

, optCompileNoMain = False

154

, optEpicCompile = False

155

, optJSCompile = False

156

, optCompileDir = Nothing

157

, optGenerateVimFile = False

158

, optGenerateLaTeX = False

159

, optGenerateHTML = False

160

, optDependencyGraph = Nothing

161

, optLaTeXDir = defaultLaTeXDir

162

, optHTMLDir = defaultHTMLDir

163

, optCSSFile = Nothing

164

, optIgnoreInterfaces = False

165

, optForcing = True

166

, optGhcFlags = []

167

, optPragmaOptions = defaultPragmaOptions

168

, optEpicFlags = []

169

, optSafe = False

170

}

147

defaultOptions = Options

148

{ optProgramName = "agda"

149

, optInputFile = Nothing

150

, optIncludeDirs = Left []

151

, optShowVersion = False

152

, optShowHelp = False

153

, optInteractive = False

154

, optRunTests = False

155

, optGHCiInteraction = False

156

, optCompile = False

157

, optCompileNoMain = False

158

, optEpicCompile = False

159

, optJSCompile = False

160

, optCompileDir = Nothing

161

, optGenerateVimFile = False

162

, optGenerateLaTeX = False

163

, optGenerateHTML = False

164

, optDependencyGraph = Nothing

165

, optLaTeXDir = defaultLaTeXDir

166

, optHTMLDir = defaultHTMLDir

167

, optCSSFile = Nothing

168

, optIgnoreInterfaces = False

169

, optForcing = True

170

, optGhcFlags = []

171

, optPragmaOptions = defaultPragmaOptions

172

, optEpicFlags = []

173

, optSafe = False

174

}

171

175

172

176

defaultPragmaOptions :: PragmaOptions

173

177

defaultPragmaOptions = PragmaOptions

194

198

195

199

-- | The default termination depth.

196

200

201

defaultCutOff :: CutOff

197

202

defaultCutOff = CutOff 0 -- minimum value

198

203

199

204

-- | The default output directory for LaTeX.

200

205

206

defaultLaTeXDir :: String

201

207

defaultLaTeXDir = "latex"

202

208

203

209

-- | The default output directory for HTML.

204

210

211

defaultHTMLDir :: String

205

212

defaultHTMLDir = "html"

206

213

214

prop_defaultOptions :: Bool

207

215

prop_defaultOptions = case checkOpts defaultOptions of

208

216

Left _ -> False

209

217

Right _ -> True

278

286

Nothing -> return $ o { optInputFile = Just f }

279

287

Just _ -> throwError "only one input file allowed"

280

288

281

versionFlag o = return $ o { optShowVersion = True }

282

helpFlag o = return $ o { optShowHelp = True }

283

safeFlag o = return $ o { optSafe = True }

284

proofIrrelevanceFlag o = return $ o { optProofIrrelevance = True }

285

experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True }

286

noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False }

287

ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }

288

allowUnsolvedFlag o = return $ o { optAllowUnsolved = True }

289

showImplicitFlag o = return $ o { optShowImplicit = True }

290

showIrrelevantFlag o = return $ o { optShowIrrelevant = True }

291

runTestsFlag o = return $ o { optRunTests = True }

292

ghciInteractionFlag o = return $ o { optGHCiInteraction = True }

293

vimFlag o = return $ o { optGenerateVimFile = True }

294

latexFlag o = return $ o { optGenerateLaTeX = True }

295

latexDirFlag d o = return $ o { optLaTeXDir = d }

296

noPositivityFlag o = return $ o { optDisablePositivity = True }

297

dontTerminationCheckFlag o = return $ o { optTerminationCheck = False }

298

dontCompletenessCheckFlag o = return $ o { optCompletenessCheck = False }

299

dontUniverseCheckFlag o = return $ o { optUniverseCheck = False

300

, optUniversePolymorphism = False }

301

sizedTypes o = return $ o { optSizedTypes = True }

302

noSizedTypes o = return $ o { optSizedTypes = False }

303

injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True }

304

guardingTypeConstructorFlag o = return $ o { optGuardingTypeConstructors = True }

305

universePolymorphismFlag o = return $ o { optUniversePolymorphism = True }

306

noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False }

307

noForcingFlag o = return $ o { optForcing = False }

308

withoutKFlag o = return $ o { optWithoutK = True }

309

copatternsFlag o = return $ o { optCopatterns = True }

310

noPatternMatchingFlag o = return $ o { optPatternMatching = False }

311

289

versionFlag :: Flag CommandLineOptions

290

versionFlag o = return $ o { optShowVersion = True }

291

292

helpFlag :: Flag CommandLineOptions

293

helpFlag o = return $ o { optShowHelp = True }

294

295

safeFlag :: Flag CommandLineOptions

296

safeFlag o = return $ o { optSafe = True }

297

298

proofIrrelevanceFlag :: Flag PragmaOptions

299

proofIrrelevanceFlag o = return $ o { optProofIrrelevance = True }

300

301

experimentalIrrelevanceFlag :: Flag PragmaOptions

302

experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True }

303

304

noIrrelevantProjectionsFlag :: Flag PragmaOptions

305

noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False }

306

307

ignoreInterfacesFlag :: Flag CommandLineOptions

308

ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }

309

310

allowUnsolvedFlag :: Flag PragmaOptions

311

allowUnsolvedFlag o = return $ o { optAllowUnsolved = True }

312

313

showImplicitFlag :: Flag PragmaOptions

314

showImplicitFlag o = return $ o { optShowImplicit = True }

315

316

showIrrelevantFlag :: Flag PragmaOptions

317

showIrrelevantFlag o = return $ o { optShowIrrelevant = True }

318

319

runTestsFlag :: Flag CommandLineOptions

320

runTestsFlag o = return $ o { optRunTests = True }

321

322

ghciInteractionFlag :: Flag CommandLineOptions

323

ghciInteractionFlag o = return $ o { optGHCiInteraction = True }

324

325

vimFlag :: Flag CommandLineOptions

326

vimFlag o = return $ o { optGenerateVimFile = True }

327

328

latexFlag :: Flag CommandLineOptions

329

latexFlag o = return $ o { optGenerateLaTeX = True }

330

331

latexDirFlag :: FilePath -> Flag CommandLineOptions

332

latexDirFlag d o = return $ o { optLaTeXDir = d }

333

334

noPositivityFlag :: Flag PragmaOptions

335

noPositivityFlag o = return $ o { optDisablePositivity = True }

336

337

dontTerminationCheckFlag :: Flag PragmaOptions

338

dontTerminationCheckFlag o = return $ o { optTerminationCheck = False }

339

340

dontCompletenessCheckFlag :: Flag PragmaOptions

341

dontCompletenessCheckFlag o = return $ o { optCompletenessCheck = False }

342

343

dontUniverseCheckFlag :: Flag PragmaOptions

344

dontUniverseCheckFlag o = return $ o { optUniverseCheck = False

345

, optUniversePolymorphism = False

346

}

347

348

sizedTypes :: Flag PragmaOptions

349

sizedTypes o = return $ o { optSizedTypes = True }

350

351

noSizedTypes :: Flag PragmaOptions

352

noSizedTypes o = return $ o { optSizedTypes = False }

353

354

injectiveTypeConstructorFlag :: Flag PragmaOptions

355

injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True }

356

357

guardingTypeConstructorFlag :: Flag PragmaOptions

358

guardingTypeConstructorFlag o = return $ o { optGuardingTypeConstructors = True }

359

360

universePolymorphismFlag :: Flag PragmaOptions

361

universePolymorphismFlag o = return $ o { optUniversePolymorphism = True }

362

363

noUniversePolymorphismFlag :: Flag PragmaOptions

364

noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False }

365

366

noForcingFlag :: Flag CommandLineOptions

367

noForcingFlag o = return $ o { optForcing = False }

368

369

withKFlag :: Flag PragmaOptions

370

withKFlag o = return $ o { optWithoutK = False }

371

372

withoutKFlag :: Flag PragmaOptions

373

withoutKFlag o = return $ o { optWithoutK = True }

374

375

copatternsFlag :: Flag PragmaOptions

376

copatternsFlag o = return $ o { optCopatterns = True }

377

378

noPatternMatchingFlag :: Flag PragmaOptions

379

noPatternMatchingFlag o = return $ o { optPatternMatching = False }

380

381

interactiveFlag :: Flag CommandLineOptions

312

382

interactiveFlag o = return $ o { optInteractive = True

313

383

, optPragmaOptions = (optPragmaOptions o)

314

{ optAllowUnsolved = True }

384

{ optAllowUnsolved = True }

315

385

}

316

compileFlag o = return $ o { optCompile = True }

317

compileFlagNoMain o = return $ o { optCompileNoMain = True }

318

compileEpicFlag o = return $ o { optEpicCompile = True}

319

compileJSFlag o = return $ o { optJSCompile = True}

320

compileDirFlag f o = return $ o { optCompileDir = Just f }

321

ghcFlag f o = return $ o { optGhcFlags = optGhcFlags o ++ [f] } -- NOTE: Quadratic in number of flags.

322

epicFlagsFlag s o = return $ o { optEpicFlags = optEpicFlags o ++ [s] } -- NOTE: Quadratic in number of flags.

323

324

htmlFlag o = return $ o { optGenerateHTML = True }

325

dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f }

326

htmlDirFlag d o = return $ o { optHTMLDir = d }

327

cssFlag f o = return $ o { optCSSFile = Just f }

328

386

387

compileFlag :: Flag CommandLineOptions

388

compileFlag o = return $ o { optCompile = True }

389

390

compileFlagNoMain :: Flag CommandLineOptions

391

compileFlagNoMain o = return $ o { optCompileNoMain = True }

392

393

compileEpicFlag :: Flag CommandLineOptions

394

compileEpicFlag o = return $ o { optEpicCompile = True}

395

396

compileJSFlag :: Flag CommandLineOptions

397

compileJSFlag o = return $ o { optJSCompile = True }

398

399

compileDirFlag :: FilePath -> Flag CommandLineOptions

400

compileDirFlag f o = return $ o { optCompileDir = Just f }

401

402

-- NOTE: Quadratic in number of flags.

403

ghcFlag :: String -> Flag CommandLineOptions

404

ghcFlag f o = return $ o { optGhcFlags = optGhcFlags o ++ [f] }

405

406

-- NOTE: Quadratic in number of flags.

407

epicFlagsFlag :: String -> Flag CommandLineOptions

408

epicFlagsFlag s o = return $ o { optEpicFlags = optEpicFlags o ++ [s] }

409

410

htmlFlag :: Flag CommandLineOptions

411

htmlFlag o = return $ o { optGenerateHTML = True }

412

413

dependencyGraphFlag :: FilePath -> Flag CommandLineOptions

414

dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f }

415

416

htmlDirFlag :: FilePath -> Flag CommandLineOptions

417

htmlDirFlag d o = return $ o { optHTMLDir = d }

418

419

cssFlag :: FilePath -> Flag CommandLineOptions

420

cssFlag f o = return $ o { optCSSFile = Just f }

421

422

includeFlag :: FilePath -> Flag CommandLineOptions

329

423

includeFlag d o = return $ o { optIncludeDirs = Left (d : ds) }

330

424

where ds = either id (const []) $ optIncludeDirs o

331

425

426

verboseFlag :: String -> Flag PragmaOptions

332

427

verboseFlag s o =

333

428

do (k,n) <- parseVerbose s

334

429

return $ o { optVerbose = Trie.insert k n $ optVerbose o }

340

435

return (init ss, n)

341

436

usage = throwError "argument to verbose should be on the form x.y.z:N or N"

342

437

438

terminationDepthFlag :: String -> Flag PragmaOptions

343

439

terminationDepthFlag s o =

344

440

do k <- readM s `catchError` \_ -> usage

345

441

when (k < 1) $ usage -- or: turn termination checking off for 0

366

462

, Option [] ["epic"] (NoArg compileEpicFlag) "compile program using the Epic backend"

367

463

, Option [] ["js"] (NoArg compileJSFlag) "compile program using the JS backend"

368

464

, Option [] ["compile-dir"] (ReqArg compileDirFlag "DIR")

369

("directory for compiler output (default: the project root)")

465

("directory for compiler output (default: the project root)")

370

466

, Option [] ["ghc-flag"] (ReqArg ghcFlag "GHC-FLAG")

371

467

"give the flag GHC-FLAG to GHC when compiling using MAlonzo"

372

468

, Option [] ["epic-flag"] (ReqArg epicFlagsFlag "EPIC-FLAG")

373

469

"give the flag EPIC-FLAG to Epic when compiling using Epic"

374

, Option [] ["test"] (NoArg runTestsFlag)

375

"run internal test suite"

376

, Option [] ["vim"] (NoArg vimFlag)

377

"generate Vim highlighting files"

378

, Option [] ["latex"] (NoArg latexFlag)

470

, Option [] ["test"] (NoArg runTestsFlag)

471

"run internal test suite"

472

, Option [] ["vim"] (NoArg vimFlag)

473

"generate Vim highlighting files"

474

, Option [] ["latex"] (NoArg latexFlag)

379

475

"generate LaTeX with highlighted source code"

380

, Option [] ["latex-dir"] (ReqArg latexDirFlag "DIR")

476

, Option [] ["latex-dir"] (ReqArg latexDirFlag "DIR")

381

477

("directory in which LaTeX files are placed (default: " ++

382

478

defaultLaTeXDir ++ ")")

383

, Option [] ["html"] (NoArg htmlFlag)

384

"generate HTML files with highlighted source code"

385

, Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")

386

"generate a Dot file with a module dependency graph"

387

, Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR")

479

, Option [] ["html"] (NoArg htmlFlag)

480

"generate HTML files with highlighted source code"

481

, Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")

482

"generate a Dot file with a module dependency graph"

483

, Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR")

388

484

("directory in which HTML files are placed (default: " ++

389

485

defaultHTMLDir ++ ")")

390

, Option [] ["css"] (ReqArg cssFlag "URL")

391

"the CSS file used by the HTML files (can be relative)"

392

, Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)

393

"ignore interface files (re-type check everything)"

486

, Option [] ["css"] (ReqArg cssFlag "URL")

487

"the CSS file used by the HTML files (can be relative)"

488

, Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)

489

"ignore interface files (re-type check everything)"

394

490

, Option ['i'] ["include-path"] (ReqArg includeFlag "DIR")

395

"look for imports in DIR"

491

"look for imports in DIR"

396

492

, Option [] ["no-forcing"] (NoArg noForcingFlag)

397

493

"disable the forcing optimisation"

398

494

, Option [] ["safe"] (NoArg safeFlag)

406

502

407

503

pragmaOptions :: [OptDescr (Flag PragmaOptions)]

408

504

pragmaOptions =

409

[ Option [] ["show-implicit"] (NoArg showImplicitFlag)

410

"show implicit arguments when printing"

411

, Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag)

412

"show irrelevant arguments when printing"

413

, Option ['v'] ["verbose"] (ReqArg verboseFlag "N")

505

[ Option [] ["show-implicit"] (NoArg showImplicitFlag)

506

"show implicit arguments when printing"

507

, Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag)

508

"show irrelevant arguments when printing"

509

, Option ['v'] ["verbose"] (ReqArg verboseFlag "N")

414

510

"set verbosity level to N"

415

-- , Option [] ["proof-irrelevance"] (NoArg proofIrrelevanceFlag)

416

-- "enable proof irrelevance (experimental feature)"

417

, Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)

418

"allow unsolved meta variables (only needed in batch mode)"

419

, Option [] ["no-positivity-check"] (NoArg noPositivityFlag)

420

"do not warn about not strictly positive data types"

421

, Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag)

422

"do not warn about possibly nonterminating code"

423

, Option [] ["termination-depth"] (ReqArg terminationDepthFlag "N")

424

"allow termination checker to count decrease/increase upto N (default N=1)"

425

, Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)

426

"do not warn about possibly incomplete pattern matches"

427

, Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag)

428

"ignore universe levels (this makes Agda inconsistent)"

511

-- , Option [] ["proof-irrelevance"] (NoArg proofIrrelevanceFlag)

512

-- "enable proof irrelevance (experimental feature)"

513

, Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)

514

"allow unsolved meta variables (only needed in batch mode)"

515

, Option [] ["no-positivity-check"] (NoArg noPositivityFlag)

516

"do not warn about not strictly positive data types"

517

, Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag)

518

"do not warn about possibly nonterminating code"

519

, Option [] ["termination-depth"] (ReqArg terminationDepthFlag "N")

520

"allow termination checker to count decrease/increase upto N (default N=1)"

521

, Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)

522

"do not warn about possibly incomplete pattern matches"

523

, Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag)

524

"ignore universe levels (this makes Agda inconsistent)"

429

525

, Option [] ["sized-types"] (NoArg sizedTypes)

430

526

"use sized types (default, inconsistent with `musical' coinduction)"

431

527

, Option [] ["no-sized-types"] (NoArg noSizedTypes)

442

538

"disable projection of irrelevant record fields"

443

539

, Option [] ["experimental-irrelevance"] (NoArg experimentalIrrelevanceFlag)

444

540

"enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)"

541

, Option [] ["with-K"] (NoArg withKFlag)

542

"enable the K rule in pattern matching"

445

543

, Option [] ["without-K"] (NoArg withoutKFlag)

446

544

"disable the K rule in pattern matching"

447

545

, Option [] ["copatterns"] (NoArg copatternsFlag)

459

557

[String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts

460

558

parseOptions' argv opts fileArg = \defaults ->

461

559

case getOpt (ReturnInOrder fileArg) opts argv of

462

(o,_,[]) -> foldl (>>=) (return defaults) o

463

(_,_,errs) -> throwError $ concat errs

560

(o,_,[]) -> foldl (>>=) (return defaults) o

561

(_,_,errs) -> throwError $ concat errs

464

562

465

563

-- | Parse the standard options.

466

564

parseStandardOptions :: [String] -> Either String CommandLineOptions

493

591

-- agda).

494

592

usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String

495

593

usage options pluginInfos progName =

496

usageInfo (header progName) options ++

497

"\nPlugins:\n" ++

594

usageInfo (header progName) options ++

595

"\nPlugins:\n" ++

498

596

indent 2 (concatMap pluginMsg pluginInfos)

499

597

500

598

where

501

header progName = unlines [ "Agda"

502

, ""

503

, "Usage: " ++ progName ++ " [OPTIONS...] [FILE]"

504

]

599

header progName = unlines [ "Agda"

600

, ""

601

, "Usage: " ++ progName ++ " [OPTIONS...] [FILE]"

602

]

505

603

506

604

pluginMsg (name, help, inherited, opts)

507

605

| null opts && null inherited = optHeader

508

606

| otherwise = usageInfo (optHeader ++

509

607

" Plugin-specific options:" ++

510

inheritedOptions inherited

511

) opts

608

inheritedOptions inherited

609

) opts

512

610

where

513

optHeader = "\n" ++ name ++ "-plugin:\n" ++ indent 2 help

514

inheritedOptions [] = ""

515

inheritedOptions pls =

516

"\n Inherits options from: " ++ unwords pls

611

optHeader = "\n" ++ name ++ "-plugin:\n" ++ indent 2 help

612

inheritedOptions [] = ""

613

inheritedOptions pls =

614

"\n Inherits options from: " ++ unwords pls

517

615

518

616

------------------------------------------------------------------------

519

617

-- All tests

Older »