PandocAgda (empty) → 2.3.3
raw patch · 11 files changed
+1239/−0 lines, 11 filesdep +Agdadep +PandocAgdadep +QuickChecksetup-changed
Dependencies added: Agda, PandocAgda, QuickCheck, Win32, base, containers, directory, filepath, mtl, old-time, pandoc, pandoc-types, text, time, xhtml
Files
- LICENSE +31/−0
- PandocAgda.cabal +112/−0
- Setup.hs +2/−0
- src/data/Agda.css +33/−0
- src/data/Agda.template +58/−0
- src/full/Agda/Interaction/Highlighting/PandocHTML.hs +288/−0
- src/full/Agda/Interaction/PandocConvertOptions.hs +41/−0
- src/full/Agda/Interaction/PandocOptions.hs +484/−0
- src/full/Agda/PandocMain.hs +176/−0
- src/full/Agda/undefined.h +2/−0
- src/main/Main.hs +12/−0
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright Péter Diviánszky 2013++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of the copyright holder nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ PandocAgda.cabal view
@@ -0,0 +1,112 @@+name: PandocAgda+version: 2.3.3+cabal-version: >= 1.8+build-type: Simple+license: BSD3+license-file: LICENSE+author: Péter Diviánszky+maintainer: Péter Diviánszky <divipp@gmail.com>+category: Dependent types+synopsis: Pandoc support for literate Agda+description:+ Agda is a dependently typed functional programming language+ and a proof assistant.+ .+ This package contains a modified Agda compiler which+ process comments in literate Agda files with Pandoc.+ Pandoc is a universal document converter.+tested-with: GHC == 7.6.1+extra-source-files: src/full/Agda/undefined.h+data-dir: src/data+data-files: Agda.template+ Agda.css++source-repository head+ type: darcs+ location: http://code.haskell.org/Agda/++library+ hs-source-dirs: src/full++ if os(windows)+ build-depends: Win32 == 2.2.*++ build-depends: Agda == 2.3.3,+ base >= 4.2 && < 4.7,+ -- mtl-2.1 contains a severe bug+ mtl >= 2.0 && < 2.1 || >= 2.1.1 && < 2.2,+ QuickCheck >= 2.3 && < 2.6,+ -- haskell-src-exts >= 1.9.6 && < 1.14,+ containers >= 0.1 && < 0.6,+ -- unordered-containers == 0.2.*,+ -- pretty >= 1.0 && < 1.2,+ -- bytestring >= 0.9.0.1 && < 0.11,+ -- array >= 0.1 && < 0.5,+ -- binary >= 0.4.4 && < 0.6,+ -- zlib >= 0.4.0.1 && < 0.6,+ filepath >= 1.1 && < 1.4,+ -- process >= 1.0.1.0 && < 1.2,+ -- haskeline >= 0.6.3.2 && < 0.8,+ xhtml == 3000.2.*,+ -- hashable >= 1.1.2.3 && < 1.3,+ -- hashtables == 1.0.*,+ -- geniplate >= 0.6.0.3 && < 0.7,+ -- parallel < 3.3,+ -- deepseq == 1.3.*,+ pandoc == 1.10.*,+ pandoc-types == 1.10.*,+ text == 0.11.*++ if impl(ghc < 7.6)+ build-depends: old-time >= 1.0 && < 1.2,+ directory >= 1.0 && < 1.2+ else+ build-depends: time == 1.4.*,+ directory == 1.2.*++ extensions: CPP+ exposed-modules: Agda.PandocMain+ Agda.Interaction.Highlighting.PandocHTML+ Agda.Interaction.PandocOptions+ Agda.Interaction.PandocConvertOptions+ other-modules: Paths_PandocAgda+ if true+ ghc-options: -w+ -fwarn-deprecated-flags+ -fwarn-dodgy-foreign-imports+ -fwarn-dodgy-imports+ -fwarn-duplicate-exports+ -fwarn-hi-shadowing+ -fwarn-incomplete-patterns+ -fwarn-missing-fields+ -fwarn-missing-methods+ -fwarn-overlapping-patterns+ -fwarn-warnings-deprecations+ -- The Cabal-generated module Paths_Agda triggers a warning under+ -- GHC 7.2.1/7.2.2 (at least when certain versions of Cabal are+ -- used).+ if impl(ghc < 7.2.1) || impl(ghc > 7.2.2)+ ghc-options: -Werror+ if impl(ghc >= 6.12)+ ghc-options: -fwarn-dodgy-exports+ -fwarn-wrong-do-bind+ if impl(ghc >= 7.2)+ ghc-options: -fwarn-identities+ ghc-prof-options: -auto-all++executable agdapandoc+ hs-source-dirs: src/main+ main-is: Main.hs+ build-depends: PandocAgda == 2.3.3,+ -- Nothing is used from the following package, except+ -- for the prelude.+ base >= 3 && < 6+ if impl(ghc >= 7)+ -- If someone installs Agda with the setuid bit set, then the+ -- presence of +RTS may be a security problem (see GHC bug #3910).+ -- However, we sometimes recommend people to use +RTS to control+ -- Agda's memory usage, so we want this functionality enabled by+ -- default.+ ghc-options: -rtsopts++
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/data/Agda.css view
@@ -0,0 +1,33 @@+/* Aspects. */+.Comment { color: #B22222 }+.Keyword { color: #CD6600 }+.String { color: #B22222 }+.Number { color: #A020F0 }+.Symbol { color: #404040 }+.PrimitiveType { color: #0000CD }+.Operator {}++/* NameKinds. */+.Bound { color: black }+.InductiveConstructor { color: #008B00 }+.CoinductiveConstructor { color: #8B7500 }+.Datatype { color: #0000CD }+.Field { color: #EE1289 }+.Function { color: #0000CD }+.Module { color: #A020F0 }+.Postulate { color: #0000CD }+.Primitive { color: #0000CD }+.Record { color: #0000CD }++/* OtherAspects. */+.DottedPattern {}+.UnsolvedMeta { color: black; background: yellow }+.UnsolvedConstraint { color: black; background: yellow }+.TerminationProblem { color: black; background: #FFA07A }+.IncompletePattern { color: black; background: #F5DEB3 }+.Error { color: red; text-decoration: underline }+.TypeChecks { color: black; background: #ADD8E6 }++/* Standard attributes. */+a { text-decoration: none }+a[href]:hover { background-color: #B4EEB4 }
+ src/data/Agda.template view
@@ -0,0 +1,58 @@+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">+<html xmlns="http://www.w3.org/1999/xhtml"$if(lang)$ lang="$lang$" xml:lang="$lang$"$endif$>+<head>+ <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />+ <meta http-equiv="Content-Style-Type" content="text/css" />+ <meta name="generator" content="pandoc" />+$for(author-meta)$+ <meta name="author" content="$author-meta$" />+$endfor$+$if(date-meta)$+ <meta name="date" content="$date-meta$" />+$endif$+ <title>$if(title-prefix)$$title-prefix$ - $endif$$pagetitle$</title>+ <style type="text/css">code{white-space: pre;}</style>+$if(quotes)$+ <style type="text/css">q { quotes: "“" "”" "‘" "’"; }</style>+$endif$+$if(highlighting-css)$+ <style type="text/css">+$highlighting-css$+ </style>+$endif$+$for(css)$+ <link rel="stylesheet" href="$css$" $if(html5)$$else$type="text/css" $endif$/>+$endfor$+$if(math)$+ $math$+$endif$+$for(header-includes)$+ $header-includes$+$endfor$+</head>+<body>+$for(include-before)$+$include-before$+$endfor$+$if(title)$+<div id="$idprefix$header">+<h1 class="title">$title$</h1>+$for(author)$+<h2 class="author">$author$</h2>+$endfor$+$if(date)$+<h3 class="date">$date$</h3>+$endif$+</div>+$endif$+$if(toc)$+<div id="$idprefix$TOC">+$toc$+</div>+$endif$+$body$+$for(include-after)$+$include-after$+$endfor$+</body>+</html>
+ src/full/Agda/Interaction/Highlighting/PandocHTML.hs view
@@ -0,0 +1,288 @@+{-# LANGUAGE CPP #-}++-- | Function for generating highlighted, hyperlinked HTML from Agda+-- sources.++module Agda.Interaction.Highlighting.PandocHTML+ ( generateHTML+ ) where++import Control.Applicative+import Control.Monad+import Control.Monad.Trans+import Control.Monad.State.Class+import Control.Arrow ((***))+import System.FilePath+import System.Directory+import Text.XHtml.Strict+import Data.Function+import Data.Monoid+import Data.Maybe+import qualified Data.Map as Map+import qualified Data.List as List+import qualified Data.Char as Char++import Text.Pandoc.Definition+import qualified Text.Pandoc.Definition as Pandoc+import Text.Pandoc.Options+import Text.Pandoc.Readers.Markdown+import Text.Pandoc.Writers.HTML++import Paths_PandocAgda++import Agda.Interaction.FindFile+import Agda.Interaction.Highlighting.Generate+import Agda.Interaction.Highlighting.Precise+import Agda.Interaction.Highlighting.Range+import Agda.TypeChecking.Monad (TCM)+import qualified Agda.TypeChecking.Monad as TCM+import qualified Agda.Syntax.Abstract as A+import qualified Agda.Syntax.Concrete as C+import Agda.Syntax.Common+import qualified Agda.Syntax.Scope.Monad as Scope+import Agda.Syntax.Translation.ConcreteToAbstract+import Agda.Interaction.Options+import qualified Agda.Interaction.PandocOptions as PO+import Agda.Utils.FileName (filePath)+import qualified Agda.Utils.IO.UTF8 as UTF8+import Agda.Utils.Pretty++import Agda.Utils.Impossible+#include "../../undefined.h"++-- | The name of the default CSS file.++defaultCSSFile :: FilePath+defaultCSSFile = "Agda.css"++-- | The name of the default template file for pandoc.++defaultTemplateFile :: FilePath+defaultTemplateFile = "Agda.template"++-- | Generates HTML files from all the sources which the given module+-- depends on (including the module itself).+--+-- This function should only be called after type checking has+-- completed successfully.++generateHTML :: PO.CommandLineOptions -> A.ModuleName -> TCM ()+generateHTML fullopts mod = do+ options <- TCM.commandLineOptions++ -- There is a default directory given by 'defaultHTMLDir'+ let dir = optHTMLDir options+ liftIO $ createDirectoryIfMissing True dir++ -- If the default CSS file should be used, then it is copied to+ -- the output directory.+ liftIO $ when (isNothing $ optCSSFile options) $ do+ cssFile <- getDataFileName defaultCSSFile+ copyFile cssFile (dir </> defaultCSSFile)++ TCM.reportSLn "html" 1 $ unlines+ [ ""+ , "Warning: HTML is currently generated for ALL files which can be"+ , "reached from the given module, including library files."+ ]++ -- Pull highlighting info from the state and generate all the+ -- web pages.+ mapM_ (\(m, h) -> generatePage fullopts dir m h) =<<+ map (id *** TCM.iHighlighting . TCM.miInterface) .+ Map.toList <$> TCM.getVisitedModules++-- | Converts module names to the corresponding HTML file names.++modToFile :: C.TopLevelModuleName -> FilePath+modToFile m = render (pretty m) <.> "html"++-- | Generates an HTML file with a highlighted, hyperlinked version of+-- the given module.++generatePage+ :: PO.CommandLineOptions+ -> FilePath -- ^ Directory in which to create files.+ -> C.TopLevelModuleName -- ^ Module to be highlighted.+ -> HighlightingInfo -- ^ Syntax highlighting info for the module.+ -> TCM ()+generatePage fullopts dir mod highlighting = do+ mf <- Map.lookup mod . TCM.stModuleToSource <$> get+ case mf of+ Nothing -> __IMPOSSIBLE__+ Just f -> do+ contents <- liftIO $ UTF8.readTextFile $ filePath f+ css <- maybe defaultCSSFile id . optCSSFile <$>+ TCM.commandLineOptions+ let mSlideVariant = fmap read $ PO.optGenerateHTML fullopts+ html <- case mSlideVariant of+ Just slideVariant | isLiterate (filePath f) -> do+ templateFile <- maybe (liftIO $ getDataFileName defaultTemplateFile) return+ (PO.optTemplateFile fullopts)+ template <- liftIO $ UTF8.readTextFile templateFile+ return $ pandocPage template css slideVariant mod contents highlighting+ _ -> do+ return $ renderHtml $ page css mod contents highlighting+ TCM.reportSLn "html" 1 $ "Generating HTML for " +++ render (pretty mod) +++ " (" ++ target ++ ")."+ liftIO $ UTF8.writeFile target html+ where target = dir </> modToFile mod+++-- | Constructs the web page, including headers.++page :: FilePath -- ^ URL to the CSS file.+ -> C.TopLevelModuleName -- ^ Module to be highlighted.+ -> String -- ^ The contents of the module.+ -> CompressedFile -- ^ Highlighting information.+ -> Html+page css modName contents info =+ header (thetitle << render (pretty modName)+ ++++ meta ! [ httpequiv "Content-Type"+ , content "text/html; charset=UTF-8"+ ]+ ++++ meta ! [ httpequiv "Content-Style-Type"+ , content "text/css"+ ]+ ++++ thelink noHtml ! [ href css+ , rel "stylesheet"+ , thetype "text/css"+ ])+ ++++ body << pre << code contents info++--- | Constructs the HTML displaying the code.++code :: String -- ^ The contents of the module.+ -> CompressedFile -- ^ Highlighting information.+ -> Html+code contents info =+ mconcat $+ map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) $+ tokenStream contents info++-- | Constructs the web page, including headers, with pandoc.++pandocPage+ :: String -- ^ Template+ -> FilePath -- ^ URL to the CSS file.+ -> HTMLSlideVariant -- ^ Slide variant+ -> C.TopLevelModuleName -- ^ Module to be highlighted.+ -> String -- ^ The contents of the module.+ -> CompressedFile -- ^ Highlighting information.+ -> String+pandocPage template css slideVariant modName contents info =+ writeHtmlString def { writerStandalone = True+ , writerTemplate = template+ , writerTableOfContents = True+ , writerSlideVariant = slideVariant+ , writerVariables = [("css",css)]+ }+ $ Pandoc meta $ concat $ zipWith ($) (removeCodeBlocks md []) cf+ where+ cf = (++ [[]])+ . map conv+ . getCode+ . splitComment "\n\\begin{code}"+ . splitComment "\n\\end{code}"+ $ tokenStream contents info++ (Pandoc meta md) = readMarkdown def contents ++ conv x = [Para [ RawInline "html"+ . renderHtmlFragment+ . (pre <<) + . mconcat+ . map (\(pos, s, mi) -> annotate pos mi (stringToHtml s))+ $ x+ ]]++ getCode ((_,s,_):xs)+ | s == "\n\\begin{code}" || List.isPrefixOf "\\begin{code}" s+ = getCode' xs []+ getCode (_:xs) = getCode xs+ getCode [] = []++ getCode' ((_,s,_):xs)+ | s == "\n\\end{code}" || List.isPrefixOf "\\end{code}" s+ = (: getCode xs) . reverse+ getCode' (x:xs) = getCode' xs . (x:)+ getCode' [] = error "__IMPOSSIBLE__" -- ???++ splitComment w = concatMap f+ where+ f (pos, s, mi) = [(pos, t, mi) | t <- filter (not . null) $ g s []]++ g s | List.isPrefixOf w s = (: (w : g (drop (length w) s) [])) . reverse+ g [] = (:[]) . reverse+ g (c:cs) = g cs . (c:)++ removeCodeBlocks (RawBlock "latex" s: xs) | List.isPrefixOf "\\begin{code}" s+ = removeCodeBlocks' (++) xs+ removeCodeBlocks (RawBlock "html" s: xs) | List.isPrefixOf "<!--\n\\begin{code}" s+ = removeCodeBlocks' const xs+ removeCodeBlocks xs@(Para (Pandoc.Str "\\begin{code}":_):_)+ = removeCodeBlocks' (++) (drop 1 $ dropWhile (not . end) xs)+ where+ end (Para xs@(_:_)) = last xs == Pandoc.Str "\\end{code}"+ end _ = False+ removeCodeBlocks (x:xs) = removeCodeBlocks xs . (x:)+ removeCodeBlocks [] = removeCodeBlocks' (++) []++ removeCodeBlocks' f xs acc = f (reverse acc): case xs of+ [] -> []+ xs -> removeCodeBlocks xs []++-- | Constructs token stream ready to print.++tokenStream+ :: String -- ^ The contents of the module.+ -> CompressedFile -- ^ Highlighting information.+ -> [(Integer, String, MetaInfo)] -- ^ (position, contents, info)+tokenStream contents info =+ map (\cs -> case cs of+ (mi, (pos, _)) : _ ->+ (pos, map (snd . snd) cs, maybe mempty id mi)+ [] -> __IMPOSSIBLE__) $+ List.groupBy ((==) `on` fst) $+ map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c))) $+ zip [1..] contents+ where+ infoMap = toMap (decompress info)++annotate :: Integer -> MetaInfo -> Html -> Html+annotate pos mi = anchor ! attributes+ where+ attributes =+ [name (show pos)] +++ maybe [] link (definitionSite mi) +++ (case classes of+ [] -> []+ cs -> [theclass $ unwords cs])++ classes =+ maybe [] noteClasses (note mi)+ ++ otherAspectClasses (otherAspects mi)+ ++ maybe [] aspectClasses (aspect mi)++ aspectClasses (Name mKind op) = kindClass ++ opClass+ where+ kindClass = maybe [] ((: []) . showKind) mKind++ showKind (Constructor Inductive) = "InductiveConstructor"+ showKind (Constructor CoInductive) = "CoinductiveConstructor"+ showKind k = show k++ opClass = if op then ["Operator"] else []+ aspectClasses a = [show a]++ otherAspectClasses = map show++ -- Notes are not included.+ noteClasses s = []++ link (m, pos) = [href $ modToFile m ++ "#" ++ show pos]
+ src/full/Agda/Interaction/PandocConvertOptions.hs view
@@ -0,0 +1,41 @@+module Agda.Interaction.PandocConvertOptions+ ( convertOptions+ ) where++import Agda.Interaction.Options+import qualified Agda.Interaction.PandocOptions as PO++import Data.Maybe++convertOptions :: PO.CommandLineOptions -> CommandLineOptions+convertOptions opts =+ Options { optProgramName = PO.optProgramName opts+ , optInputFile = PO.optInputFile opts+ , optIncludeDirs = PO.optIncludeDirs opts+ , optShowVersion = PO.optShowVersion opts+ , optShowHelp = PO.optShowHelp opts+ , optInteractive = PO.optInteractive opts + , optRunTests = PO.optRunTests opts + , optGHCiInteraction = PO.optGHCiInteraction opts + , optCompile = PO.optCompile opts + , optEpicCompile = PO.optEpicCompile opts + , optJSCompile = PO.optJSCompile opts + , optCompileDir = PO.optCompileDir opts + , optGenerateVimFile = PO.optGenerateVimFile opts + , optGenerateLaTeX = PO.optGenerateLaTeX opts + , optGenerateHTML = isJust $ PO.optGenerateHTML opts+ , optDependencyGraph = PO.optDependencyGraph opts + , optLaTeXDir = PO.optLaTeXDir opts + , optHTMLDir = PO.optHTMLDir opts + , optCSSFile = PO.optCSSFile opts + , optIgnoreInterfaces = PO.optIgnoreInterfaces opts + , optForcing = PO.optForcing opts + , optGhcFlags = PO.optGhcFlags opts+ , optPragmaOptions = PO.optPragmaOptions opts+ , optEpicFlags = PO.optEpicFlags opts+ , optSafe = PO.optSafe opts + }++ ++
+ src/full/Agda/Interaction/PandocOptions.hs view
@@ -0,0 +1,484 @@+{-# LANGUAGE StandaloneDeriving, DeriveFunctor #-}++module Agda.Interaction.PandocOptions+ ( CommandLineOptions(..)+ , PragmaOptions(..)+ , OptionsPragma+ , Flag+ , Verbosity+ , checkOpts+ , parseStandardOptions+ , parsePragmaOptions+ , parsePluginOptions+ , defaultOptions+ , defaultInteractionOptions+ , defaultVerbosity+ , standardOptions_+ , unsafePragmaOptions+ , isLiterate+ , mapFlag+ , usage+ , tests+ ) where++import Agda.Interaction.Options+ ( PragmaOptions (..)+ , OptionsPragma+ )++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 Text.Pandoc.Options (HTMLSlideVariant(..))++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++-- | This should probably go somewhere else.+isLiterate :: FilePath -> Bool+isLiterate file = ".lagda" `isSuffixOf` file++type Verbosity = Trie String Int++data CommandLineOptions =+ Options { optProgramName :: String+ , optInputFile :: Maybe FilePath+ , optIncludeDirs :: Either [FilePath] [AbsolutePath]+ -- ^ 'Left' is used temporarily, before the paths have+ -- been made absolute. An empty 'Left' list is+ -- interpreted as @["."]@ (see+ -- 'Agda.TypeChecking.Monad.Options.makeIncludeDirsAbsolute').+ , optShowVersion :: Bool+ , optShowHelp :: Bool+ , optInteractive :: Bool+ , optRunTests :: Bool+ , optGHCiInteraction :: Bool+ , optCompile :: Bool+ , optEpicCompile :: Bool+ , optJSCompile :: Bool+ , optCompileDir :: Maybe FilePath+ -- ^ In the absence of a path the project root is used.+ , optGenerateVimFile :: Bool+ , optGenerateLaTeX :: Bool+ , optGenerateHTML :: Maybe SlideVariant+ , optDependencyGraph :: Maybe FilePath+ , optLaTeXDir :: FilePath+ , optHTMLDir :: FilePath+ , optCSSFile :: Maybe FilePath+ , optTemplateFile :: Maybe FilePath+ , optIgnoreInterfaces :: Bool+ , optForcing :: Bool+ , optGhcFlags :: [String]+ , optPragmaOptions :: PragmaOptions+ , optEpicFlags :: [String]+ , optSafe :: Bool+ }+ deriving Show++-- | Options for HTML generation with pandoc++type SlideVariant = String++-- | Map a function over the long options. Also removes the short options.+-- Will be used to add the plugin name to the plugin options.+mapFlag :: (String -> String) -> OptDescr a -> OptDescr a+mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr++-- | For batch usage.+defaultVerbosity :: Verbosity+defaultVerbosity = Trie.singleton [] 1++-- | For interactive usage, do not print any debug messages+-- by default.+defaultInteractionVerbosity :: Verbosity+defaultInteractionVerbosity = Trie.singleton [] 0++defaultInteractionOptions :: PragmaOptions+defaultInteractionOptions = defaultPragmaOptions+ { optVerbose = defaultInteractionVerbosity }++defaultOptions :: CommandLineOptions+defaultOptions =+ Options { optProgramName = "agda"+ , optInputFile = Nothing+ , optIncludeDirs = Left []+ , optShowVersion = False+ , optShowHelp = False+ , optInteractive = False+ , optRunTests = False+ , optGHCiInteraction = False+ , optCompile = False+ , optEpicCompile = False+ , optJSCompile = False+ , optCompileDir = Nothing+ , optGenerateVimFile = False+ , optGenerateLaTeX = False+ , optGenerateHTML = Nothing+ , optDependencyGraph = Nothing+ , optLaTeXDir = defaultLaTeXDir+ , optHTMLDir = defaultHTMLDir+ , optCSSFile = Nothing+ , optTemplateFile = Nothing+ , optIgnoreInterfaces = False+ , optForcing = True+ , optGhcFlags = []+ , optPragmaOptions = defaultPragmaOptions+ , optEpicFlags = []+ , optSafe = False+ }++defaultPragmaOptions :: PragmaOptions+defaultPragmaOptions = PragmaOptions+ { optShowImplicit = False+ , optShowIrrelevant = False+ , optVerbose = defaultVerbosity+ , optProofIrrelevance = False+ , optExperimentalIrrelevance = False+ , optIrrelevantProjections = True+ , optAllowUnsolved = False+ , optDisablePositivity = False+ , optTerminationCheck = True+ , optTerminationDepth = 0 -- this is the cutoff value+ , optCompletenessCheck = True+ , optUniverseCheck = True+ , optSizedTypes = False+ , optInjectiveTypeConstructors = False+ , optGuardingTypeConstructors = False+ , optUniversePolymorphism = True+ , optWithoutK = False+ , optCopatterns = False+ }++-- | The default output directory for LaTeX.++defaultLaTeXDir = "latex"++-- | The default output directory for HTML.++defaultHTMLDir = "html"++prop_defaultOptions = case checkOpts defaultOptions of+ Left _ -> False+ Right _ -> True++{- | @f :: Flag opts@ is an action on the option record that results from+ parsing an option. @f opts@ produces either an error message or an+ updated options record+-}+type Flag opts = opts -> Either String opts++-- | Checks that the given options are consistent.++checkOpts :: Flag CommandLineOptions+checkOpts opts+ | not (atMostOne [optAllowUnsolved . p, optCompile]) = Left+ "Unsolved meta variables are not allowed when compiling.\n"+ | not (atMostOne [optGHCiInteraction, isJust . optInputFile]) =+ Left "Choose at most one: input file or --interaction.\n"+ | not (atMostOne $ interactive ++ [optCompile, optEpicCompile, optJSCompile]) =+ Left "Choose at most one: compilers/--interactive/--interaction.\n"+ | not (atMostOne $ interactive ++ [isJust . optGenerateHTML]) =+ Left "Choose at most one: --html/--interactive/--interaction.\n"+ | not (atMostOne $ interactive ++ [isJust . optDependencyGraph]) =+ Left "Choose at most one: --dependency-graph/--interactive/--interaction.\n"+ | not (atMostOne [ optUniversePolymorphism . p+ , not . optUniverseCheck . p+ ]) =+ Left "Cannot have both universe polymorphism and type in type.\n"+ | not (atMostOne $ interactive ++ [optGenerateLaTeX]) =+ Left "Choose at most one: --latex/--interactive/--interaction.\n"+ | (not . null . optEpicFlags $ opts)+ && not (optEpicCompile opts) =+ Left "Cannot set Epic flags without using the Epic backend.\n"+ | not (maybe True ((==1) . length . (reads :: ReadS HTMLSlideVariant)) $ optGenerateHTML opts) =+ Left $ "Available slide variants: "+ ++ intercalate " " (map show [NoSlides, S5Slides, SlidySlides, SlideousSlides, DZSlides])+ | otherwise = Right opts+ where+ atMostOne bs = length (filter ($ opts) bs) <= 1++ p = optPragmaOptions++ interactive = [optInteractive, optGHCiInteraction]++-- Check for unsafe pramas. Gives a list of used unsafe flags.++unsafePragmaOptions :: PragmaOptions -> [String]+unsafePragmaOptions opts =+ [ "--allow-unsolved-metas" | optAllowUnsolved opts ] +++ [ "--no-positivity-check" | optDisablePositivity opts ] +++ [ "--no-termination-check" | not (optTerminationCheck opts) ] +++ [ "--no-coverage-check" | not (optCompletenessCheck opts) ] +++ [ "--type-in-type" | not (optUniverseCheck opts) ] +++ [ "--sized-types" | optSizedTypes opts ] +++ [ "--injective-type-constructors" | optInjectiveTypeConstructors opts ] +++ [ "--guardedness-preserving-type-constructors" | optGuardingTypeConstructors opts ] +++ [ "--experimental-irrelevance" | optExperimentalIrrelevance opts ] +++ [ "--copatterns" | optCopatterns opts ]++-- The default pragma options should be considered safe++defaultPragmaOptionsSafe :: IO Bool+defaultPragmaOptionsSafe+ | null unsafe = return True+ | otherwise = do putStrLn $ "Following pragmas are default but not safe: "+ ++ intercalate ", " unsafe+ return False+ where unsafe = unsafePragmaOptions defaultPragmaOptions++inputFlag :: FilePath -> Flag CommandLineOptions+inputFlag f o =+ case optInputFile o of+ Nothing -> return $ o { optInputFile = Just f }+ Just _ -> throwError "only one input file allowed"++versionFlag o = return $ o { optShowVersion = True }+helpFlag o = return $ o { optShowHelp = True }+safeFlag o = return $ o { optSafe = True }+proofIrrelevanceFlag o = return $ o { optProofIrrelevance = True }+experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True }+noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False }+ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }+allowUnsolvedFlag o = return $ o { optAllowUnsolved = True }+showImplicitFlag o = return $ o { optShowImplicit = True }+showIrrelevantFlag o = return $ o { optShowIrrelevant = True }+runTestsFlag o = return $ o { optRunTests = True }+ghciInteractionFlag o = return $ o { optGHCiInteraction = True }+vimFlag o = return $ o { optGenerateVimFile = True }+latexFlag o = return $ o { optGenerateLaTeX = True }+latexDirFlag d o = return $ o { optLaTeXDir = d }+noPositivityFlag o = return $ o { optDisablePositivity = True }+dontTerminationCheckFlag o = return $ o { optTerminationCheck = False }+dontCompletenessCheckFlag o = return $ o { optCompletenessCheck = False }+dontUniverseCheckFlag o = return $ o { optUniverseCheck = False+ , optUniversePolymorphism = False }+sizedTypes o = return $ o { optSizedTypes = True }+injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True }+guardingTypeConstructorFlag o = return $ o { optGuardingTypeConstructors = True }+universePolymorphismFlag o = return $ o { optUniversePolymorphism = True }+noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False }+noForcingFlag o = return $ o { optForcing = False }+withoutKFlag o = return $ o { optWithoutK = True }+copatternsFlag o = return $ o { optCopatterns = True }++interactiveFlag o = return $ o { optInteractive = True+ , optPragmaOptions = (optPragmaOptions o)+ { optAllowUnsolved = True }+ }+compileFlag o = return $ o { optCompile = True }+compileEpicFlag o = return $ o { optEpicCompile = True}+compileJSFlag o = return $ o { optJSCompile = True}+compileDirFlag f o = return $ o { optCompileDir = Just f }+ghcFlag f o = return $ o { optGhcFlags = f : optGhcFlags o }+epicFlagsFlag s o = return $ o { optEpicFlags = optEpicFlags o ++ [s]}++htmlFlag s o = return $ o { optGenerateHTML = s }+dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f }+htmlDirFlag d o = return $ o { optHTMLDir = d }+cssFlag f o = return $ o { optCSSFile = Just f }+templateFlag f o = return $ o { optTemplateFile = Just f }++includeFlag d o = return $ o { optIncludeDirs = Left (d : ds) }+ where ds = either id (const []) $ optIncludeDirs o++verboseFlag s o =+ do (k,n) <- parseVerbose s+ return $ o { optVerbose = Trie.insert k n $ optVerbose o }+ where+ parseVerbose s = case wordsBy (`elem` ":.") s of+ [] -> usage+ ss -> do+ n <- readM (last ss) `catchError` \_ -> usage+ return (init ss, n)+ usage = throwError "argument to verbose should be on the form x.y.z:N or N"++terminationDepthFlag s o =+ do k <- readM s `catchError` \_ -> usage+ when (k < 1) $ usage -- or: turn termination checking off for 0+ return $ o { optTerminationDepth = k-1 }+ where usage = throwError "argument to termination-depth should be >= 1"++integerArgument :: String -> String -> Either String Int+integerArgument flag s =+ readM s `catchError` \_ ->+ throwError $ "option '" ++ flag ++ "' requires an integer argument"++standardOptions :: [OptDescr (Flag CommandLineOptions)]+standardOptions =+ [ Option ['V'] ["version"] (NoArg versionFlag) "show version number"+ , Option ['?'] ["help"] (NoArg helpFlag) "show this help"+ , Option ['I'] ["interactive"] (NoArg interactiveFlag)+ "start in interactive mode"+ , Option [] ["interaction"] (NoArg ghciInteractionFlag)+ "for use with the Emacs mode"+ , Option ['c'] ["compile"] (NoArg compileFlag)+ "compile program using the MAlonzo backend (experimental)"+ , Option [] ["epic"] (NoArg compileEpicFlag) "compile program using the Epic backend"+ , Option [] ["js"] (NoArg compileJSFlag) "compile program using the JS backend"+ , Option [] ["compile-dir"] (ReqArg compileDirFlag "DIR")+ ("directory for compiler output (default: the project root)")+ , Option [] ["ghc-flag"] (ReqArg ghcFlag "GHC-FLAG")+ "give the flag GHC-FLAG to GHC when compiling using MAlonzo"+ , Option [] ["epic-flag"] (ReqArg epicFlagsFlag "EPIC-FLAG")+ "give the flag EPIC-FLAG to Epic when compiling using Epic"+ , Option [] ["test"] (NoArg runTestsFlag)+ "run internal test suite"+ , Option [] ["vim"] (NoArg vimFlag)+ "generate Vim highlighting files"+ , Option [] ["latex"] (NoArg latexFlag)+ "generate LaTeX with highlighted source code"+ , Option [] ["latex-dir"] (ReqArg latexDirFlag "DIR")+ ("directory in which LaTeX files are placed (default: " +++ defaultLaTeXDir ++ ")")+ , Option [] ["html"] (OptArg htmlFlag "SLIDEVARIANT")+ ("generate HTML files with highlighted source code; " +++ "giving slide variant invokes pandoc")+ , Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")+ "generate a Dot file with a module dependency graph"+ , Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR")+ ("directory in which HTML files are placed (default: " +++ defaultHTMLDir ++ ")")+ , Option [] ["css"] (ReqArg cssFlag "URL")+ "the CSS file used by the HTML files (can be relative)"+ , Option [] ["template"] (ReqArg templateFlag "URL")+ "the template file used for HTML generation with pandoc (can be relative)"+ , Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)+ "ignore interface files (re-type check everything)"+ , Option ['i'] ["include-path"] (ReqArg includeFlag "DIR")+ "look for imports in DIR"+ , Option [] ["no-forcing"] (NoArg noForcingFlag)+ "disable the forcing optimisation"+ , Option [] ["safe"] (NoArg safeFlag)+ "disable postulates, unsafe OPTION pragmas and primTrustMe"+ ] ++ map (fmap lift) pragmaOptions+ where+ lift :: Flag PragmaOptions -> Flag CommandLineOptions+ lift f = \opts -> do+ ps <- f (optPragmaOptions opts)+ return (opts { optPragmaOptions = ps })++pragmaOptions :: [OptDescr (Flag PragmaOptions)]+pragmaOptions =+ [ Option [] ["show-implicit"] (NoArg showImplicitFlag)+ "show implicit arguments when printing"+ , Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag)+ "show irrelevant arguments when printing"+ , Option ['v'] ["verbose"] (ReqArg verboseFlag "N")+ "set verbosity level to N"+ -- , Option [] ["proof-irrelevance"] (NoArg proofIrrelevanceFlag)+ -- "enable proof irrelevance (experimental feature)"+ , Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)+ "allow unsolved meta variables (only needed in batch mode)"+ , Option [] ["no-positivity-check"] (NoArg noPositivityFlag)+ "do not warn about not strictly positive data types"+ , Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag)+ "do not warn about possibly nonterminating code"+ , Option [] ["termination-depth"] (ReqArg terminationDepthFlag "N")+ "allow termination checker to count decrease/increase upto N (default N=1)"+ , Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)+ "do not warn about possibly incomplete pattern matches"+ , Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag)+ "ignore universe levels (this makes Agda inconsistent)"+ , Option [] ["sized-types"] (NoArg sizedTypes)+ "use sized types (inconsistent with coinduction)"+ , Option [] ["injective-type-constructors"] (NoArg injectiveTypeConstructorFlag)+ "enable injective type constructors (makes Agda anti-classical and possibly inconsistent)"+ , Option [] ["guardedness-preserving-type-constructors"] (NoArg guardingTypeConstructorFlag)+ "treat type constructors as inductive constructors when checking productivity"+ , Option [] ["no-universe-polymorphism"] (NoArg noUniversePolymorphismFlag)+ "disable universe polymorphism"+ , Option [] ["universe-polymorphism"] (NoArg universePolymorphismFlag)+ "enable universe polymorphism (default)"+ , Option [] ["no-irrelevant-projections"] (NoArg noIrrelevantProjectionsFlag)+ "disable projection of irrelevant record fields"+ , Option [] ["experimental-irrelevance"] (NoArg experimentalIrrelevanceFlag)+ "enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)"+ , Option [] ["without-K"] (NoArg withoutKFlag)+ "disable the K rule (maybe)"+ , Option [] ["copatterns"] (NoArg copatternsFlag)+ "enable definitions by copattern matching"+ ]++-- | Used for printing usage info.+standardOptions_ :: [OptDescr ()]+standardOptions_ = map (fmap $ const ()) standardOptions++-- | Don't export+parseOptions' ::+ [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts+parseOptions' argv opts fileArg = \defaults ->+ case getOpt (ReturnInOrder fileArg) opts argv of+ (o,_,[]) -> foldl (>>=) (return defaults) o+ (_,_,errs) -> throwError $ concat errs++-- | Parse the standard options.+parseStandardOptions :: [String] -> Either String CommandLineOptions+parseStandardOptions argv =+ checkOpts =<<+ parseOptions' argv standardOptions inputFlag defaultOptions++-- | Parse options from an options pragma.+parsePragmaOptions+ :: [String]+ -- ^ Pragma options.+ -> CommandLineOptions+ -- ^ Command-line options which should be updated.+ -> Either String PragmaOptions+parsePragmaOptions argv opts = do+ ps <- parseOptions' argv pragmaOptions+ (\s _ -> throwError $ "Bad option in pragma: " ++ s)+ (optPragmaOptions opts)+ checkOpts (opts { optPragmaOptions = ps })+ return ps++-- | Parse options for a plugin.+parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts+parsePluginOptions argv opts =+ parseOptions' argv opts+ (\s _ -> throwError $+ "Internal error: Flag " ++ s ++ " passed to a plugin")++-- | The usage info message. The argument is the program name (probably+-- agda).+usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String+usage options pluginInfos progName =+ usageInfo (header progName) options +++ "\nPlugins:\n" +++ indent 2 (concatMap pluginMsg pluginInfos)++ where+ header progName = unlines [ "Agda"+ , ""+ , "Usage: " ++ progName ++ " [OPTIONS...] [FILE]"+ ]++ pluginMsg (name, help, inherited, opts)+ | null opts && null inherited = optHeader+ | otherwise = usageInfo (optHeader +++ " Plugin-specific options:" +++ inheritedOptions inherited+ ) opts+ where+ optHeader = "\n" ++ name ++ "-plugin:\n" ++ indent 2 help+ inheritedOptions [] = ""+ inheritedOptions pls =+ "\n Inherits options from: " ++ unwords pls++------------------------------------------------------------------------+-- All tests++tests :: IO Bool+tests = runTests "Agda.Interaction.Options"+ [ quickCheck' prop_defaultOptions+ , defaultPragmaOptionsSafe+ ]
+ src/full/Agda/PandocMain.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}++{-| Agda main module.+-}+module Agda.PandocMain where++import Control.Monad.State+import Control.Monad.Error+import Control.Applicative++import Data.List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe++import System.Environment+import System.Exit+import System.FilePath++import Agda.Syntax.Position+import Agda.Syntax.Parser+import Agda.Syntax.Concrete.Pretty ()+import qualified Agda.Syntax.Abstract as A+import Agda.Syntax.Abstract.Pretty+import Agda.Syntax.Translation.ConcreteToAbstract+import Agda.Syntax.Translation.AbstractToConcrete+import Agda.Syntax.Translation.InternalToAbstract+import Agda.Syntax.Abstract.Name+import Agda.Syntax.Scope.Base++import Agda.Interaction.Exceptions+import Agda.Interaction.CommandLine.CommandLine+import Agda.Interaction.Options+import qualified Agda.Interaction.PandocOptions as PO+import Agda.Interaction.PandocConvertOptions+import Agda.Interaction.Monad+import Agda.Interaction.GhcTop (mimicGHCi)+import qualified Agda.Interaction.Imports as Imp+import qualified Agda.Interaction.Highlighting.Dot as Dot+import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX+import Agda.Interaction.Highlighting.PandocHTML++import Agda.TypeChecker+import Agda.TypeChecking.Monad+import Agda.TypeChecking.Reduce+import Agda.TypeChecking.Errors+import qualified Agda.TypeChecking.Serialise+import Agda.TypeChecking.Serialise+import Agda.TypeChecking.SizedTypes++import Agda.Compiler.MAlonzo.Compiler as MAlonzo+import Agda.Compiler.Epic.Compiler as Epic+import Agda.Compiler.JS.Compiler as JS++import Agda.Termination.TermCheck++import Agda.Utils.Monad+import Agda.Utils.FileName+import Agda.Utils.Pretty++import Agda.Tests+import Agda.Version++import qualified System.IO as IO++#include "undefined.h"+import Agda.Utils.Impossible++-- | The main function+runAgda :: TCM ()+runAgda = do+ progName <- liftIO getProgName+ argv <- liftIO getArgs+ let opts = PO.parseStandardOptions argv+ case fmap (\opts -> (opts, convertOptions opts)) opts of+ Left err -> liftIO $ optionError err+ Right (fullopts, opts)+ | optShowHelp opts -> liftIO printUsage+ | optShowVersion opts -> liftIO printVersion+ | optRunTests opts -> liftIO $ do+ ok <- testSuite+ unless ok exitFailure+ | isNothing (optInputFile opts)+ && not (optInteractive opts)+ && not (optGHCiInteraction opts)+ -> liftIO printUsage+ | otherwise -> do+ setCommandLineOptions opts+ checkFile fullopts+ where+ checkFile :: PO.CommandLineOptions -> TCM ()+ checkFile fullopts = do+ i <- optInteractive <$> liftTCM commandLineOptions+ ghci <- optGHCiInteraction <$> liftTCM commandLineOptions+ compile <- optCompile <$> liftTCM commandLineOptions+ epic <- optEpicCompile <$> liftTCM commandLineOptions+ js <- optJSCompile <$> liftTCM commandLineOptions+ when i $ liftIO $ putStr splashScreen+ let failIfNoInt (Just i) = return i+ -- The allowed combinations of command-line+ -- options should rule out Nothing here.+ failIfNoInt Nothing = __IMPOSSIBLE__++ failIfInt x Nothing = x+ failIfInt _ (Just _) = __IMPOSSIBLE__++ interaction :: TCM (Maybe Interface) -> TCM ()+ interaction | i = runIM . interactionLoop+ | ghci = (failIfInt mimicGHCi =<<)+ | compile = (MAlonzo.compilerMain =<<) . (failIfNoInt =<<)+ | epic = (Epic.compilerMain =<<) . (failIfNoInt =<<)+ | js = (JS.compilerMain =<<) . (failIfNoInt =<<)+ | otherwise = (() <$)+ interaction $ do+ hasFile <- hasInputFile+ resetState+ if not hasFile then return Nothing else do+ file <- getInputFile+ (i, mw) <- Imp.typeCheck file++ unsolvedOK <- optAllowUnsolved <$> pragmaOptions++ result <- case mw of+ Just (Warnings [] [] []) -> __IMPOSSIBLE__+ Just (Warnings _ unsolved@(_:_) _)+ | not unsolvedOK -> typeError $ UnsolvedMetas unsolved+ Just (Warnings _ _ unsolved@(_:_))+ | not unsolvedOK -> typeError $ UnsolvedConstraints unsolved+ Just (Warnings termErrs@(_:_) _ _) ->+ typeError $ TerminationCheckFailed termErrs+ Just _ -> return Nothing+ Nothing -> return $ Just i++ whenM (optGenerateHTML <$> commandLineOptions) $+ generateHTML fullopts $ iModuleName i++ whenM (isJust . optDependencyGraph <$> commandLineOptions) $+ Dot.generateDot $ i++ whenM (optGenerateLaTeX <$> commandLineOptions) $+ LaTeX.generateLaTeX (iModuleName i) (iHighlighting i)++ return result++-- | Print usage information.+printUsage :: IO ()+printUsage = do+ progName <- getProgName+ putStr $ usage standardOptions_ [] progName++-- | Print version information.+printVersion :: IO ()+printVersion =+ putStrLn $ "Agda version " ++ version++-- | What to do for bad options.+optionError :: String -> IO ()+optionError err = do+ putStrLn $ "Error: " ++ err+ printUsage+ exitFailure++-- | Main+main :: IO ()+main = do+ r <- runTCM $ runAgda `catchError` \err -> do+ s <- prettyError err+ liftIO $ putStrLn s+ throwError err+ case r of+ Right _ -> exitSuccess+ Left _ -> exitFailure+ `catchImpossible` \e -> do+ putStr $ show e+ exitFailure
+ src/full/Agda/undefined.h view
@@ -0,0 +1,2 @@+#define __IMPOSSIBLE__ (throwImpossible (Impossible __FILE__ __LINE__))+#define __IMPOSSIBLE_TERM__ (impossibleTerm __FILE__ __LINE__)
+ src/main/Main.hs view
@@ -0,0 +1,12 @@+-- | Wrapper for "Agda.Main".+--+-- Agda is installed as a library. This module is used to build the+-- executable.++module Main (main) where++import qualified Agda.PandocMain ( main )+import Prelude ( IO )++main :: IO ()+main = Agda.PandocMain.main