dedukti-1.1.0: Dedukti.hs

-- |
-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
-- License   : GPL
--
-- This module is the entry point for europa. Based on the command line
-- arguments the appropriate driver is invoked. Everything is coordinated by
-- the driver. This module is also the place where global configuration data
-- is initialized.

module Main where

import System.Environment
import qualified Dedukti.Config as Config
import Dedukti.DkM
import Dedukti.Module
import Dedukti.Driver.Batch
import Dedukti.Driver.Compile
import Text.PrettyPrint.Leijen
import Data.List (partition, isPrefixOf)
import Data.Either (partitionEithers)
import System.Exit
import System.IO
import qualified Data.ByteString.Lazy.Char8 as B
import qualified Paths_dedukti as Cabal (version)
import Data.Version


data Flag = FlagMake
          | FlagJobs Int
          | FlagFormat Config.Format
          | FlagHelp | FlagVersion
          | FlagVerbose | FlagVeryVerbose
            deriving (Eq, Ord, Show)

data FlagArity a = Nullary String Flag
                 | Unary String (String -> Flag)

flagDescriptions =
  [ ([Nullary "--make" FlagMake],
     "Build MODULE and all its dependencies in one go.")
  , ([Unary "-jN" (FlagJobs . read)],
     "Perform N jobs at once.")
  , ([Nullary "-fexternal" (FlagFormat Config.External)],
     "Force recognizing input as (human-readable) external format.")
  , ([Nullary "-fprefix-notation" (FlagFormat Config.Prefix)],
     "Force recognizing input as (fast) prefix format.")
  , ([Unary "-v[v]" $ \arg -> if null arg then FlagVerbose else FlagVeryVerbose],
     "Be verbose, -vv to be even more verbose.")
  , (zipWith ($) [Nullary "-h", Nullary "--help"] (repeat FlagHelp),
     "This usage information.")
  , ([Nullary "--version" FlagVersion],
     "Output version information then exit.") ]

-- Flag descriptions obey the following conventions:
--
-- - double hyphen flags don't have arguments.
--
-- - Everything after the first letter of a hyphen flag is part of the
--   argument.
parseCmdline args =
  let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args
      (errors, flags) = partitionEithers $ map toFlag hyphened
  in (flags, rest, errors)
    where flagmap = concatMap fst flagDescriptions
          unpack ('-':'-':name) = (name, "")
          unpack ('-':name:arg) = ([name], arg)
          unpack x = error $ "Malformed argument: " ++ x
          lookupFlag name arg (Nullary n f : desc)
              | fst (unpack n) == name =
                  if null arg
                  then Right f
                  else Left $ "No argument expected for flag " ++ n
          lookupFlag name arg (Unary n f : desc)
              | fst (unpack n) == name = Right (f arg)
          lookupFlag name _ [] = Left $ "Flag not found: " ++ name
          lookupFlag name arg (_:desc) = lookupFlag name arg desc
          toFlag x | (name, arg) <- unpack x = lookupFlag name arg flagmap

printUsage = do
  self <- parameter Config.imageName
  let header = show $ text "Usage:" <+>
               (text self <+> text "[OPTION]..." <+> text "MODULE")
  io $ hPutStrLn stderr header

printHelp = do
  self <- parameter Config.imageName
  let header = text "Usage:" <+>
               (text self <+> text "[OPTION]..." <+> text "MODULE")
               <$> text "Options:"
      flags = vsep (map pflag flagDescriptions)
  io $ putStrLn $ show $ header <$> indent 4 flags
    where pflag (flags, desc) = fillBreak 14 (hcat $ punctuate (text ", ") $
                                   map (text . name) flags) <+> text desc
          name (Nullary n _) = n
          name (Unary n _) = n

bailout = printUsage >> io exitFailure

printVersion = do
  self <- parameter Config.imageName
  io $ B.putStrLn $ B.pack $ flip displayS "" $ renderPretty 0.70 100 $
     text "Dedukti" <+> text (showVersion Cabal.version) <> line <> line <>
     text "Copyright (c) 2009 CNRS - École Polytechnique - INRIA." <> line <> line <>
     fillText "You may redistribute copies of Dedukti under the terms of \
              \the GNU General Public License. For more information about \
              \these matters, see the file named COPYING."

initializeConfiguration = foldr aux Config.defaultConfig
    where aux FlagVerbose c     = c { Config.verbosity = Verbose }
          aux FlagVeryVerbose c = c { Config.verbosity = Debug }
          aux (FlagFormat f) c  = c { Config.format = Just f }
          aux (FlagJobs n) c    = c { Config.jobs = n }
          aux _ c               = c

main = do
  args <- getArgs
  let (opts, files, errs) = parseCmdline args
  when (not (null errs)) $ do
         hPutDoc stderr (vcat (map text errs) <> line)
         exitFailure
  (`runDkM` initializeConfiguration opts) $
         case undefined of
           _ | FlagHelp `elem` opts -> printHelp
             | FlagVersion `elem` opts -> printVersion
           _ | FlagMake `elem` opts -> do
                     unless (length files == 1) bailout
                     make [moduleFromPath (head files)]
             | otherwise -> do
                     unless (length files == 1) bailout
                     compile (moduleFromPath (head files))