dedukti 1.1.2 → 1.1.3

raw patch · 9 files changed

+101/−74 lines, 9 filesdep ~unix

Dependency ranges changed: unix

Files

• Dedukti.hs +12/−53
• Dedukti/Analysis/Rule.hs +2/−0
• Dedukti/CodeGen.hs +2/−0
• Dedukti/Core.hs +1/−0
• Dedukti/Driver/Batch.hs +4/−2
• Dedukti/Driver/Interactive.hs +3/−0
• Dedukti/Module.hs +1/−0
• System/Console/Option.hs +57/−0
• dedukti.cabal +19/−19

@@ -2,24 +2,23 @@ -- Copyright : © 2009 CNRS - École Polytechnique - INRIA -- License   : GPL ----- This module is the entry point for europa. Based on the command line+-- This module is the entry point for Dedukti. 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 System.Console.Option import Text.PrettyPrint.Leijen-import Data.List (partition, isPrefixOf)-import Data.Either (partitionEithers)+import System.Environment import System.Exit-import System.IO+import System.IO (stderr) import qualified Data.ByteString.Lazy.Char8 as B import qualified Paths_dedukti as Cabal (version) import Data.Version@@ -32,9 +31,6 @@           | 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.")@@ -51,50 +47,11 @@   , ([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+usage = do self <- parameter Config.imageName+           return $ text "Usage:" <+>+             (text self <+> text "[OPTION]..." <+> text "MODULE") -bailout = printUsage >> io exitFailure+bailout = usage >>= io . printUsage >> io exitFailure  printVersion = do   self <- parameter Config.imageName@@ -114,13 +71,15 @@  main = do   args <- getArgs-  let (opts, files, errs) = parseCmdline args+  let (opts, files, errs) = parseCmdline flagDescriptions args   when (not (null errs)) $ do          hPutDoc stderr (vcat (map text errs) <> line)          exitFailure   (`runDkM` initializeConfiguration opts) $          case undefined of-           _ | FlagHelp `elem` opts -> printHelp+           _ | FlagHelp `elem` opts -> do+                     u <- usage+                     io $ printHelp u flagDescriptions              | FlagVersion `elem` opts -> printVersion            _ | FlagMake `elem` opts -> do                      unless (length files == 1) bailout

@@ -24,6 +24,8 @@  instance Exception NonContiguousRules +-- | All rules for a same constant must be given contiguously, without+-- intervening rules for other constants. checkOrdering :: [TyRule Qid a] -> DkM () checkOrdering rules = do   say Verbose $ text "Checking rule contiguity ..."

@@ -17,6 +17,8 @@     -- | Emit code corresponding to an individual rule set.     emit :: RuleSet (Id o) (A o) -> o +    -- | Combine code from a number of rule sets, typically forming a module,+    -- into a bundle.     coalesce :: [o] -> Bundle o      -- | Produce the byte sequence to write to a file, given the code

@@ -76,6 +76,7 @@  type Module id a = ([Binding id a], [TyRule id a]) +-- | Type families used to project out the type parameters from the datatypes. type family Id t type family A t 

@@ -2,8 +2,9 @@ -- Copyright : © 2009 CNRS - École Polytechnique - INRIA -- License   : GPL ----- The batch driver. It compiles all given targets and all their dependencies,--- also invoking the Haskell compiler on the generated source code.+-- The batch driver. It compiles all given targets and all their dependencies+-- (using the Compile driver), also invoking the Haskell compiler on the+-- generated source code.  module Dedukti.Driver.Batch (make) where @@ -23,6 +24,7 @@ import Data.Char (toUpper)  +-- The staleness check. cmp x y = do   s <- io $ IO.isStale x y   say Debug $ text "Compared" <+> text x <+> text y <> text ":" <+> text (show s)

@@ -11,6 +11,9 @@ import Data.ByteString.Lazy (ByteString)  +dk = QuasiQuote { quoteExp = parse "<interactive>"+                , quoteDec = undefined }+ -- | Emit Haskell code for one module. eval :: String -> ByteString eval input =

@@ -34,6 +34,7 @@ import StringTable.Atom (Atom)  +-- | A generic stack-like datatype for representing hierarchical names. data Hierarchy = !Hierarchy :. !Atom | Root                  deriving (Eq, Ord, Show) 

@@ -0,0 +1,57 @@+-- |+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA+-- License   : GPL+--+-- Parse command-line options (or flags).+--+-- 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.++module System.Console.Option where++import Text.PrettyPrint.Leijen+import Data.Either (partitionEithers)+import Data.List (partition, isPrefixOf)+import System.IO+++data FlagArity f = Nullary String f+                 | Unary String (String -> f)++type Description f = [([FlagArity f], String)]++parseCmdline :: Description f -> [String] -> ([f], [String], [String])+parseCmdline desc args =+  let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args+      (errors, flags) = partitionEithers $ map toFlag hyphened+  in (flags, rest, errors)+    where flagmap = concatMap fst desc+          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 :: Doc -> IO ()+printUsage = hPutStrLn stderr . show++printHelp :: Doc -> Description f -> IO ()+printHelp usage desc = do+  let flags = vsep (map pflag desc)+  putStrLn $ show $ usage <$> text "Options:" <$> 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

@@ -1,5 +1,5 @@ name:           dedukti-version:        1.1.2+version:        1.1.3 author:         Mathieu Boespflug maintainer:     Mathieu Boespflug <mboes@lix.polytechnique.fr> copyright:      © 2009 CNRS - École Polytechnique - INRIA@@ -46,31 +46,31 @@  library   exposed-modules:     Dedukti.Runtime-  build-depends:       time >= 1.1, unix >= 2.4+  build-depends:       time >= 1.1, unix >= 2.3   extensions:          DeriveDataTypeable, PatternGuards, FlexibleInstances   ghc-options:         -fwarn-unused-binds -fwarn-unused-imports  executable dedukti   main-is:             Dedukti.hs-  other-modules:       Dedukti.Core,-                       Dedukti.Parser,-                       Dedukti.Parser.External,-                       Dedukti.Parser.Prefix,-                       Dedukti.Parser.Interface,-                       Dedukti.Pretty,-                       Dedukti.Driver.Interactive,-                       Dedukti.Driver.Batch,-                       Dedukti.Driver.Compile,-                       Dedukti.Rule,-                       Dedukti.DkM,-                       Dedukti.Config,-                       Dedukti.Module,+  other-modules:       Dedukti.Core+                       Dedukti.Parser+                       Dedukti.Parser.External+                       Dedukti.Parser.Prefix+                       Dedukti.Parser.Interface+                       Dedukti.Pretty+                       Dedukti.Driver.Interactive+                       Dedukti.Driver.Batch+                       Dedukti.Driver.Compile+                       Dedukti.Rule+                       Dedukti.DkM+                       Dedukti.Config+                       Dedukti.Module                        Dedukti.CodeGen-                       Dedukti.CodeGen.Exts,-                       Dedukti.Analysis.Rule,-                       Dedukti.Analysis.Scope,+                       Dedukti.CodeGen.Exts+                       Dedukti.Analysis.Rule+                       Dedukti.Analysis.Scope                        Dedukti.Analysis.Dependency-+                       System.Console.Option   build-depends:       base >= 4 && < 5, mtl >= 1.1, containers >= 0.2,                        directory, filepath, process,                        bytestring >= 0.9.1.0,