call-alloy 0.1.0.2 → 0.2.0.0

raw patch · 6 files changed

+401/−14 lines, 6 filesdep +containersdep +lensdep +mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: containers, lens, mtl, trifecta

API changes (from Hackage documentation)

Files

• call-alloy.cabal +20/−2
• src/Language/Alloy/Call.hs +22/−11
• src/Language/Alloy/Functions.hs +162/−0
• src/Language/Alloy/Parser.hs +105/−0
• src/Language/Alloy/Types.hs +79/−0
• test/Language/Alloy/CallSpec.hs +13/−1

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 54c29a66869bf88b9365e7543b6507d23efdcb3cdac0ac437540d41f4ca0e8c0+-- hash: 3585ba8d1d84b7d988b6fdc0cdb7917691a39aca577d4c3143aa2b8d79a3098d  name:           call-alloy-version:        0.1.0.2+version:        0.2.0.0 synopsis:       A simple library to call Alloy given a specification description:    Please see the README on GitHub at <https://github.com/marcellussiegburg/call-alloy#readme> category:       Language@@ -34,20 +34,27 @@   exposed-modules:       Language.Alloy.Call   other-modules:+      Language.Alloy.Functions+      Language.Alloy.Parser       Language.Alloy.RessourceNames       Language.Alloy.Ressources+      Language.Alloy.Types       Paths_call_alloy   hs-source-dirs:       src   build-depends:       base >=4.7 && <5     , bytestring+    , containers     , directory     , file-embed     , filepath     , hashable+    , lens+    , mtl     , process     , split+    , trifecta   if os(windows)     cpp-options: -DWINDOWS     build-depends:@@ -61,22 +68,33 @@   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      Language.Alloy.Call+      Language.Alloy.Functions+      Language.Alloy.Parser+      Language.Alloy.RessourceNames+      Language.Alloy.Ressources+      Language.Alloy.Types       Language.Alloy.CallSpec       Paths_call_alloy   hs-source-dirs:+      src       test   ghc-options: -threaded -rtsopts -with-rtsopts=-N   build-depends:       base >=4.7 && <5     , bytestring     , call-alloy+    , containers     , directory     , file-embed     , filepath     , hashable     , hspec+    , lens+    , mtl     , process     , split+    , trifecta   if os(windows)     cpp-options: -DWINDOWS     build-depends:

@@ -12,17 +12,22 @@ (as it is required by Alloy). -} {-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-} module Language.Alloy.Call (   existsInstance,   getInstances,+  module Functions,+  module Types,   ) where -import qualified Data.ByteString                  as BS (writeFile)+import qualified Data.ByteString                  as BS+  (hGetLine, intercalate, writeFile)  import Control.Monad                    (unless)+import Control.Lens.Internal.ByteString (unpackStrict8)+import Data.ByteString                  (ByteString) import Data.Hashable                    (hash) import Data.IORef                       (IORef, newIORef, readIORef)-import Data.List                        (intercalate) import Data.List.Split                  (splitOn) import Data.Maybe                       (fromMaybe, isJust) import System.Directory@@ -35,7 +40,7 @@ import System.Exit                      (ExitCode (..)) import System.FilePath   ((</>), (<.>), searchPathSeparator, takeDirectory)-import System.IO                        (hClose, hGetLine, hIsEOF, hPutStr)+import System.IO                        (hClose, hIsEOF, hPutStr) import System.IO.Unsafe                 (unsafePerformIO) import System.Process #if defined(mingw32_HOST_OS)@@ -44,8 +49,12 @@ import System.Posix.User                (getLoginName) #endif +import Language.Alloy.Functions         as Functions+import Language.Alloy.Parser            (parseInstance) import Language.Alloy.RessourceNames    (alloyJarName, className, classPackage) import Language.Alloy.Ressources        (alloyJar, classFile)+import Language.Alloy.Types             as Types+  (AlloyInstance, AlloySig, Entries, Signature)  data CallAlloyConfig = Config {     alloyJarFile   :: FilePath,@@ -70,7 +79,7 @@   -- ^ How many instances to return 'Nothing' for all.   -> String   -- ^ The Alloy specification which should be loaded.-  -> IO [String]+  -> IO [AlloyInstance] getInstances maxInstances content = do   classPath <- getClassPath   let callAlloy = proc "java"@@ -85,22 +94,24 @@   hPutStr hin content   hClose hin   printCallErrors herr-  printContentOnError ph `seq`-    fmap (intercalate "\n") . drop 1 . splitOn [begin] <$> getWholeOutput hout+  instas <- printContentOnError ph `seq`+    fmap (BS.intercalate "\n") . drop 1 . splitOn [begin] <$> getWholeOutput hout+  return $ either (error . show) id . parseInstance <$> instas   where+    begin :: ByteString     begin = "---INSTANCE---"     getWholeOutput h = do       eof <- hIsEOF h       if eof         then return []-        else (:) <$> hGetLine h <*> getWholeOutput h+        else (:) <$> BS.hGetLine h <*> getWholeOutput h     printContentOnError ph = do       code <- waitForProcess ph       unless (code == ExitSuccess)         $ fail $ "Failed parsing your file:\n" <> content     printCallErrors err = do       errors <- getWholeOutput err-      unless (null errors) $ fail $ intercalate "\n" errors+      unless (null errors) $ fail $ unpackStrict8 $ BS.intercalate "\n" errors  {-| Check if the class path was determined already, if so use it, otherwise call@@ -134,7 +145,7 @@   let mconfig = Config <$> alloy <*> callAlloy <*> pure (isJust keep)   case mconfig of     Nothing -> do-      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir" +      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"     Just c  -> return c -} {-@@ -147,7 +158,7 @@     then do     version <- read <$> readFile versionFile     unless (version == versionHash) $ createVersionFile configDir versionFile-    else createVersionFile configDir versionFile +    else createVersionFile configDir versionFile -}  fallbackToTempDir :: IO FilePath -> IO FilePath@@ -161,7 +172,7 @@     login  <- getLoginName #endif     let tmpDir = tmp </> show (hash login) </> appName-    createUserDirectoriesIfMissing $ tmpDir+    createUserDirectoriesIfMissing tmpDir     return tmpDir   else error $ show e 

@@ -0,0 +1,162 @@+{-# LANGUAGE OverloadedStrings #-}+{-|+Module      : Language.Alloy.Functions+Description : Type definitions for Call Alloy library+Copyright   : (c) Marcellus Siegburg, 2019+License     : MIT+Maintainer  : marcellus.siegburg@uni-due.de++This module exports basic types in order to work with parsed Alloy instances.+Furthermore, it provides functions to handle these parsed instances.+-}+module Language.Alloy.Functions (+  getSingle, getDouble, getTriple,+  lookupSig,+  objectName,+  relToMap,+  scoped, unscoped,+  ) where++import qualified Data.Set                         as S (fromList, size, toList)+import qualified Data.Map                         as M (fromList, lookup)++import Control.Monad.Except             (MonadError, throwError)+import Data.Function                    (on)+import Data.List                        (groupBy)+import Data.Map                         (Map)+import Data.Set                         (Set)+import Data.String                      (IsString, fromString)++import Language.Alloy.Types (+  AlloyInstance,+  AlloySig,+  Entry (..),+  Object (..),+  Relation (..),+  Signature (..),+  )++{-|+Create a 'Signature' given its scope and name.+-}+scoped :: String -> String -> Signature+scoped = Signature . Just++{-|+Create an unscoped Signature given its name.+-}+unscoped :: String -> Signature+unscoped = Signature Nothing++{-|+Retrieve a set of objects of a given 'AlloySig'.+Successful if the signatures relation is a set (or empty).+-}+getSingle+  :: (IsString s, MonadError s m)+  => String+  -> AlloySig+  -> m (Set Object)+getSingle = lookupRel single++{-|+Retrieve a binary relation of objects of a given 'AlloySig'.+Successful if the signatures relation is binary (or empty).+-}+getDouble+  :: (IsString s, MonadError s m)+  => String+  -> AlloySig+  -> m (Set (Object, Object))+getDouble = lookupRel double++{-|+Retrieve a ternary relation of objects of a given 'AlloySig'.+Successful if the signatures relation is ternary (or empty).+-}+getTriple+  :: (IsString s, MonadError s m)+  => String+  -> AlloySig+  -> m (Set (Object, Object, Object))+getTriple = lookupRel triple++binaryToMap :: (Ord k, Ord v) => Set (k, v) -> Map k (Set v)+binaryToMap bin = M.fromList+  [(fst (head gs), S.fromList $ snd <$> gs)+  | gs <- groupBy ((==) `on` fst) $ S.toList bin]++{-|+Transforms a relation into a Mapping.+Is only successful (i.e. returns 'return' if the given transformation function is+able to map the given values injectively.+-}+relToMap+  :: (IsString s, MonadError s m, Ord k, Ord v)+  => (a -> (k, v))+  -> Set a+  -> m (Map k (Set v))+relToMap f rel+  | S.size map' == length rel' = return $ binaryToMap map'+  | otherwise                  =+    throwError "relToMap: The performed transformation is not injective."+  where+    rel' = S.toList rel+    map' = S.fromList $ fmap f rel'++lookupRel+  :: (IsString s, MonadError s m)+  => (Relation a -> m b)+  -> String+  -> Entry Map a+  -> m b+lookupRel kind rel e = case M.lookup rel (relation e) of+  Nothing -> throwError $ fromString $ "relation " ++ fromString rel+    ++ " is missing in the Alloy instance"+  Just r  -> kind r++{-|+Lookup a signature within a given Alloy Instance.+-}+lookupSig+  :: (IsString s, MonadError s m)+  => Signature+  -> AlloyInstance+  -> m AlloySig+lookupSig s insta = case M.lookup s insta of+  Nothing -> throwError $ fromString $ maybe "" (++ "/") (scope s) ++ sigName s+    ++ " is missing in the Alloy instance"+  Just e   -> return e++{-|+Retrieve an objects name.+-}+objectName :: Object -> String+objectName o = case o of+  Object s n     -> s ++ '$' : show n+  NumberObject n -> show n+  NamedObject n  -> n++single+  :: (IsString s, MonadError s m, Monoid (a Object))+  => Relation a+  -> m (a Object)+single EmptyRelation = return mempty+single (Single r)    = return r+single _             = throwError "Relation is (unexpectedly) a mapping"++double+  :: (IsString s, MonadError s m, Monoid (a (Object, Object)))+  => Relation a+  -> m (a (Object, Object))+double EmptyRelation = return mempty+double (Double r)    = return r+double _             = throwError "Relation is not a binary mapping"++triple+  :: (IsString s, MonadError s m, Monoid (a (Object, Object, Object)))+  => Relation a+  -> m (a (Object, Object, Object))+triple EmptyRelation = return mempty+triple (Triple r)    = return r+triple _             = throwError "Relation is not a ternary mapping"

@@ -0,0 +1,105 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TupleSections #-}+{-|+Module      : Language.Alloy.Parser+Description : A generic Alloy instance parser for Call Alloy library+Copyright   : (c) Marcellus Siegburg, 2019+License     : MIT+Maintainer  : marcellus.siegburg@uni-due.de++This module allows for parsing and converting instances into Haskell data+structures.+Basically all modules are parsed into a Map of Map of Set allowing easy lookup+of every returned set and relation.+-}+module Language.Alloy.Parser (+  parseInstance,+  ) where++import qualified Data.Set                         as S (fromList)+import qualified Data.Map                         as M+  (alter, empty, insert, singleton)++import Control.Applicative              ((<|>))+import Control.Monad                    (void)+import Control.Monad.Except             (MonadError, throwError)+import Data.ByteString                  (ByteString)+import Data.Functor                     (($>))+import Data.Set                         (Set)+import Text.Trifecta++import Language.Alloy.Types (+  AlloyInstance,+  Annotation (..),+  Entries,+  Entry (..),+  Object (..),+  Relation (..),+  Signature (..),+  )++{-|+Parse an Alloy instance from a given String.+May fail with a 'ParseError'.+-}+parseInstance :: (MonadError ErrInfo m) => ByteString -> m AlloyInstance+parseInstance inst = case parseByteString alloyInstance mempty inst of+  Failure l -> throwError l+  Success r -> return $ combineEntries r++combineEntries :: [Entries (,)] -> AlloyInstance+combineEntries = foldl createOrInsert M.empty+  where+    createOrInsert ys (s, e) = M.alter (Just . alterSig e) s ys+    alterSig e Nothing  = e { relation = uncurry M.singleton $ relation e}+    alterSig e (Just y) = y { relation = uncurry M.insert (relation e) (relation y) }++alloyInstance :: Parser [Entries (,)]+alloyInstance = (try (void $ string "---INSTANCE---" *> newline) <|> return ())+  *> many entry++entry :: Parser (Entries (,))+entry = do+  entryAnnotation <- try (string "skolem " $> Just Skolem) <|> pure Nothing+  entrySignature <- sig+  (entrySignature,)+    <$> (Entry+         <$> pure entryAnnotation+         <*> ((,)+              <$> ((string "<:" *> word) <|> pure "")+              <*> parseRelations <* (void newline <|> eof)))++sig :: Parser Signature+sig =+  try (Signature <$> (Just <$> word) <* char '/' <*> word)+  <|> Signature <$> pure Nothing <*> word++parseRelations :: Parser (Relation Set)+parseRelations = char '='+  *> (try (string "{}" $> EmptyRelation)+      <|> fmap Triple (try $ sep tripleRel)+      <|> fmap Double (try $ sep doubleRel)+      <|> fmap Single (sep singleRel))+  where+    sep rel = S.fromList+      <$> between (char '{') (char '}') (rel `sepBy` string ", ")+    tripleRel = (,,) <$> nextObject <*> nextObject <*> object+    doubleRel = (,) <$> nextObject <*> object+    singleRel = object+    nextObject = object <* string "->"++object :: Parser Object+object =+  try (Object <$> word <* char '$' <*> (read <$> some digit))+  <|> try (NumberObject <$> int)+  <|> NamedObject <$> word++int :: Parser Int+int = fmap read $ (++)+  <$> (try (string "-") <|> pure "")+  <*> some digit++word :: Parser String+word = (:)+  <$> (letter <|> char '$')+  <*> many (letter <|> digit <|> char '_')

@@ -0,0 +1,79 @@+{-|+Module      : Language.Alloy.Types+Description : Type definitions for Call Alloy library+Copyright   : (c) Marcellus Siegburg, 2019+License     : MIT+Maintainer  : marcellus.siegburg@uni-due.de++This module defines required types for the Alloy instance parser.+Unless reexported, these types are considered as internal.+-}+module Language.Alloy.Types (+  AlloyInstance, AlloySig, Annotation (..),+  Entries, Entry (..), Object (..), Relation (..), Signature (..),+  ) where++import Data.Map                         (Map)+import Data.Set                         (Set)++{-|+A complete Alloy instance.+-}+type AlloyInstance = Entries Map++{-|+A signature with all its objects and relations.+-}+type AlloySig      = Entry Map Set++{-|+A collection of Signatures with associated entries.+-}+type Entries a = a Signature (Entry a Set)++{-|+An Alloy signature.+-}+data Signature = Signature {+    scope    :: Maybe String,+    sigName  :: String+  } deriving (Eq, Ord, Show)++{-|+A concrete instance of an Alloy signature.+-}+data Object =+    Object {+      objSig     :: String,+      identifier :: Int+    }+  | NumberObject {+      number :: Int+    }+  | NamedObject {+      objName :: String+    } deriving (Eq, Ord, Show)++{-|+An Alloy relation, i.e. a collection of a tuple of 'Object's.+The collection may be a singleton, a set, a list, ...+-}+data Relation a =+    EmptyRelation+  | Single (a Object)+  | Double (a (Object, Object))+  | Triple (a (Object, Object, Object))++{-|+Specifically marked values.+-}+data Annotation = Skolem deriving (Eq, Show)++{-|+An entry is a collection of a 'Relation'.+This collection may be a singleton, a set, a list, ...+-}+data Entry a b = Entry {+    annotation :: Maybe Annotation,+    relation   :: a String (Relation b)+  }

@@ -1,9 +1,21 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# OPTIONS_GHC -Wno-orphans #-} module Language.Alloy.CallSpec (spec) where +import Data.Map                         (Map)+import Data.Set                         (Set) import Test.Hspec  import Language.Alloy.Call              (existsInstance, getInstances)+import Language.Alloy.Types             (Entry (..), Relation (..)) +deriving instance Eq (Relation Set)+deriving instance Eq (Entry Map Set)++deriving instance Show (Relation Set)+deriving instance Show (Entry Map Set)+ spec :: Spec spec = do   describe "existsInstance" $ do@@ -13,6 +25,6 @@       existsInstance "pred a (a: Int) { a > a }\nrun a" `shouldReturn` False   describe "getInstances" $ do     it "an empty spec returns a single trivial instance" $-      getInstances (Just 2) "" `shouldReturn` ["integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nuniv={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nInt={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nseq/Int={0, 1, 2, 3}\nString={}\nnone={}"]+      (show <$> getInstances (Just 2) "") `shouldReturn` "[fromList [(Signature {scope = Nothing, sigName = \"Int\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Nothing, sigName = \"String\"},Entry {annotation = Nothing, relation = fromList [(\"\",EmptyRelation)]}),(Signature {scope = Nothing, sigName = \"integers\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Nothing, sigName = \"none\"},Entry {annotation = Nothing, relation = fromList [(\"\",EmptyRelation)]}),(Signature {scope = Nothing, sigName = \"univ\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Just \"seq\", sigName = \"Int\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3}]))]})]]"     it "a conflicting spec returns no instance" $       getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` []