call-alloy 0.2.1.1 → 0.2.2.0

raw patch · 7 files changed

+662/−339 lines, 7 filesdep −lensdep ~Win32dep ~basedep ~bytestringPVP ok

version bump matches the API change (PVP)

Dependencies removed: lens

Dependency ranges changed: Win32, base, bytestring, hashable

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−0
• README.md +126/−0
• call-alloy.cabal +29/−26
• src/Language/Alloy/Call.hs +5/−308
• src/Language/Alloy/Debug.hs +14/−0
• src/Language/Alloy/Functions.hs +131/−5
• src/Language/Alloy/Internal/Call.hs +350/−0

@@ -4,6 +4,13 @@  ## Released changes +### 0.2.2.0++- deprecate 'relToMap'+- provide functions for returning raw output of instances+- provide functions for typed retrieval+- deprecate 'getSingle', 'getDouble', 'getTriple', 'objectName'+ ### 0.2.1.1  - fix errors due to long Alloy code by starting timeout after transferring code

@@ -19,3 +19,129 @@  On every call the application checks the [`XdgDirectory`](https://hackage.haskell.org/package/directory/docs/System-Directory.html#t:XdgDirectory) if the libraries exist in a current version. If not they are placed there together with a version identifier.++## The library in action++This is a basic description on how to use the library.++### A specification example++Consider this Alloy specification of a simple Graph:++```Alloy+abstract sig Node {+  flow : Node -> lone Int,+  stored : one Int+} {+  stored >= 0+  all n : Node | some flow[n] implies flow[n] >= 0+  no flow[this]+}++fun currentFlow(x, y : one Node) : Int {+  let s = x.stored, f = x.flow[y] | s < f implies s else f+}++pred withFlow[x, y : one Node] {+  currentFlow[x, y] > 0+}++pred show {}++run withFlow for 3 Int, 2 Node+```++The graph is consisting of `Node`s, which might have some goods `stored` and may deliver them to other `Node`s (via `flow`).+`Node`s do not have `flow` to themselves.+The `currentFlow` is the minimum between the flow from the starting `Node` to the end `Node` and the currently `stored` goods at the starting `Node` (note: intermediate `Node`s are not allowed).+We call two `Nodes` `x` and `y` `withFlow` if `currentFlow` from `x` to `y` is greater than `0`.+We restrict our search to `3`-Bit signed `Int` values and `2` `Nodes`.++### An instance example++Calling Alloy using `getInstances` and the above program,+could return the following (abbreviated) instance:++``` Haskell+[(Signature {+    scope = Nothing,+    sigName = "$withFlow_x"+    },+  Entry {+    annotation = Just Skolem,+    relation = fromList [+      ("",Single (fromList [Object {objSig = "Node", identifier = 1}]))+      ]+    }),+ (Signature {+    scope = Nothing,+    sigName = "$withFlow_y"+    },+  Entry {+    annotation = Just Skolem,+    relation = fromList [+      ("",Single (fromList [Object {objSig = "Node", identifier = 0}]))+      ]+    }),+ ...+ (Signature {+    scope = Just "this",+    sigName = "Node"+    },+  Entry {+    annotation = Nothing,+    relation = fromList [+      ("",Single (fromList [+        Object {objSig = "Node", identifier = 0},+        Object {objSig = "Node", identifier = 1}+        ])),+      ("flow",Triple (fromList [+        (Object {objSig = "Node", identifier = 0},Object {objSig = "Node", identifier = 1},NumberObject {number = 0}),+        (Object {objSig = "Node", identifier = 1},Object {objSig = "Node", identifier = 0},NumberObject {number = 3})+        ])),+      ("stored",Double (fromList [+        (Object {objSig = "Node", identifier = 0},NumberObject {number = 0}),+        (Object {objSig = "Node", identifier = 1},NumberObject {number = 1})+        ]))+      ]+    })+ ]+```++### A retrieval example++Using this library we may retrieve returned signature values using `lookupSig`,+then query parameter variables of the queried predicate using `unscoped`,+and query signature sets and relations using `getSingleAs`, `getDoubleAs`, and `getTripleAs`.++The following Code might for instance be used for the graph example:++``` Haskell+newtype Node = Node Int deriving (Eq, Show, Ord)++instanceToNames+  :: AlloyInstance+  -> Either String (Set Node, Set (Node, Int), Set (Node, Node, Int), Set (Node), Set (Node))+instanceToNames insta = do+  let node :: String -> Int -> Either String Node+      node = object "Node" Node+  n     <- lookupSig (scoped "this" "Node") insta+  nodes <- getSingleAs "" node n+  store <- getDoubleAs "stored" node int n+  flow  <- getTripleAs "flow" node node int n+  x     <- lookupSig (unscoped "$withFlow_x") insta >>= getSingleAs "" node+  y     <- lookupSig (unscoped "$withFlow_y") insta >>= getSingleAs "" node+  return (nodes, store, flow, x, y)+```++Calling `instanceToNames` on the above instance would result in the following expression:++``` Haskell+Right (+  fromList [Node 0,Node 1],+  fromList [(Node 0,0),(Node 1,1)],+  fromList [(Node 0,Node 1,0),(Node 1,Node 0,3)],+  fromList [Node 1],+  fromList [Node 0]+  )+```

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack ----- hash: a6397f9e52550d7e13e9e9b7b80fdbdc15cd29ab28396f6c2ad8dbd8cf0774b2+-- hash: 5c150629bcf8420718ec571afc36561ad329e6a349265b2719b219d59a96a022  name:           call-alloy-version:        0.2.1.1+version:        0.2.2.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@@ -36,8 +36,10 @@ library   exposed-modules:       Language.Alloy.Call+      Language.Alloy.Debug   other-modules:       Language.Alloy.Functions+      Language.Alloy.Internal.Call       Language.Alloy.Parser       Language.Alloy.RessourceNames       Language.Alloy.Ressources@@ -45,26 +47,26 @@       Paths_call_alloy   hs-source-dirs:       src+  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Widentities -Wredundant-constraints   build-depends:-      base >=4.7 && <5-    , bytestring >=0.10 && <0.12-    , containers >=0.6 && <0.7-    , directory >=1.3 && <1.4+      base >=4.12 && <5+    , bytestring >=0.10.4 && <0.12+    , containers ==0.6.*+    , directory ==1.3.*     , file-embed >=0.0.11 && <0.1-    , filepath >=1.4 && <1.5+    , filepath ==1.4.*     , hashable >=1.2 && <1.4-    , lens >=4.17 && <4.20-    , mtl >=2.2 && <2.3-    , process >=1.6 && <1.7-    , split >=0.2 && <0.3+    , mtl ==2.2.*+    , process ==1.6.*+    , split ==0.2.*     , trifecta >=2 && <2.2   if os(windows)     cpp-options: -DWINDOWS     build-depends:-        Win32 >=2.5 && <2.11+        Win32 >=2.5 && <2.14   else     build-depends:-        unix >=2.7 && <2.8+        unix ==2.7.*   default-language: Haskell2010  test-suite call-alloy-test@@ -72,7 +74,9 @@   main-is: Spec.hs   other-modules:       Language.Alloy.Call+      Language.Alloy.Debug       Language.Alloy.Functions+      Language.Alloy.Internal.Call       Language.Alloy.Parser       Language.Alloy.RessourceNames       Language.Alloy.Ressources@@ -82,27 +86,26 @@   hs-source-dirs:       src       test-  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Widentities -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N   build-depends:-      base >=4.7 && <5-    , bytestring >=0.10 && <0.12+      base >=4.12 && <5+    , bytestring >=0.10.4 && <0.12     , call-alloy-    , containers >=0.6 && <0.7-    , directory >=1.3 && <1.4+    , containers ==0.6.*+    , directory ==1.3.*     , file-embed >=0.0.11 && <0.1-    , filepath >=1.4 && <1.5+    , filepath ==1.4.*     , hashable >=1.2 && <1.4     , hspec-    , lens >=4.17 && <4.20-    , mtl >=2.2 && <2.3-    , process >=1.6 && <1.7-    , split >=0.2 && <0.3+    , mtl ==2.2.*+    , process ==1.6.*+    , split ==0.2.*     , trifecta >=2 && <2.2   if os(windows)     cpp-options: -DWINDOWS     build-depends:-        Win32 >=2.5 && <2.11+        Win32 >=2.5 && <2.14   else     build-depends:-        unix >=2.7 && <2.8+        unix ==2.7.*   default-language: Haskell2010

@@ -1,8 +1,7 @@-{-# LANGUAGE ScopedTypeVariables #-} {-| Module      : Language.Alloy.Call Description : A simple library to call Alloy given a specification-Copyright   : (c) Marcellus Siegburg, 2019+Copyright   : (c) Marcellus Siegburg, 2019 - 2021 License     : MIT Maintainer  : marcellus.siegburg@uni-due.de @@ -12,8 +11,6 @@ A requirement for this library to work is a Java Runtime Environment (as it is required by Alloy). -}-{-# LANGUAGE CPP #-}-{-# LANGUAGE OverloadedStrings #-} module Language.Alloy.Call (   CallAlloyConfig (maxInstances, noOverflow, timeout),   defaultCallAlloyConfig,@@ -24,92 +21,13 @@   module Types,   ) where -import qualified Data.ByteString                  as BS-  (hGetLine, intercalate, isSuffixOf, writeFile)-import qualified Data.ByteString.Char8            as BS (unlines)--import Control.Concurrent (-  ThreadId,-  forkIO, killThread, newEmptyMVar, putMVar, takeMVar, threadDelay,-  )-import Control.Exception                (IOException)-import Control.Lens.Internal.ByteString (unpackStrict8)-import Control.Monad                    (unless, void, when)-import Data.ByteString                  (ByteString)-import Data.Hashable                    (hash)-import Data.IORef                       (IORef, newIORef, readIORef)-import Data.List.Split                  (splitOn)-import Data.Maybe                       (fromMaybe)-import System.Directory-  (XdgDirectory (..), createDirectory, doesFileExist, doesDirectoryExist,-   getTemporaryDirectory, getXdgDirectory)-import System.Directory.Internal        (setFileMode)-import System.Directory.Internal.Prelude-  (catch, isDoesNotExistError)-import System.Exit                      (ExitCode (..))-import System.FilePath-  ((</>), (<.>), searchPathSeparator, takeDirectory)-import System.IO-  (BufferMode (..), Handle, hClose, hFlush, hIsEOF, hPutStr, hSetBuffering)-import System.IO.Unsafe                 (unsafePerformIO)-import System.Process (-  CreateProcess (..), StdStream (..), ProcessHandle,-  createProcess, proc, terminateProcess, waitForProcess,-  )-#if defined(mingw32_HOST_OS)-import System.Win32.Info                (getUserName)-#else-import System.Posix.User                (getLoginName)-#endif- import Language.Alloy.Functions         as Functions+import Language.Alloy.Internal.Call import Language.Alloy.Parser            (parseInstance)-import Language.Alloy.RessourceNames (-  alloyJarName, className, classPackage, commonsCliJarName-  )-import Language.Alloy.Ressources        (alloyJar, classFile, commonsCliJar) import Language.Alloy.Types             as Types   (AlloyInstance, AlloySig, Entries, Object, Signature)  {-|-Configuration for calling alloy. These are:-- * maximal number of instances to retrieve ('Nothing' for all)- * wheather to not overflow when calculating numbers within Alloy- * an timeout after which to forcibly kill Alloy-   (retrieving only instances that were returned before killing the process)--}-data CallAlloyConfig = CallAlloyConfig {-  -- | maximal number of instances to retrieve ('Nothing' for all)-  maxInstances :: Maybe Integer,-  -- | wheather to not overflow when calculating numbers within Alloy-  noOverflow   :: Bool,-  -- | the time in microseconds after which to forcibly kill Alloy-  --   ('Nothing' for never)-  timeout      :: Maybe Int-  }--{-|-Default configuration for calling Alloy. Defaults to:-- * retrieve all instances- * do not overflow--}-defaultCallAlloyConfig :: CallAlloyConfig-defaultCallAlloyConfig = CallAlloyConfig {-  maxInstances = Nothing,-  noOverflow   = True,-  timeout      = Nothing-  }--{-# NOINLINE mclassPath #-}-{-|-'IORef' for storing the class path.--}-mclassPath :: IORef (Maybe FilePath)-mclassPath = unsafePerformIO (newIORef Nothing)--{-| This function may be used to get all model instances for a given Alloy specification. It calls Alloy via a Java interface and parses the raw instance answers before returning the resulting list of 'AlloyInstance's.@@ -136,212 +54,9 @@   -> String   -- ^ The Alloy specification which should be loaded.   -> IO [AlloyInstance]-getInstancesWith config content = do-  classPath <- getClassPath-  let callAlloy = proc "java"-        $ ["-cp", classPath, classPackage ++ '.' : className,-           "-i", show $ fromMaybe (-1) $ maxInstances config]-        ++ ["-o" | not $ noOverflow config]-  (Just hin, Just hout, Just herr, ph) <--    createProcess callAlloy {-        std_out = CreatePipe,-        std_in  = CreatePipe,-        std_err = CreatePipe-      }-  pout <- listenForOutput hout-  perr <- listenForOutput herr-#ifndef mingw32_HOST_OS-  hSetBuffering hin NoBuffering-#endif-  hPutStr hin content-  hFlush hin-  hClose hin-  maybe (return ()) (void . startTimeout hin hout herr ph) $ timeout config-  out <- getOutput pout-  err <- getOutput perr-  printContentOnError ph-  unless (null err) $ fail $ unpackStrict8 $ BS.unlines err-  let instas = fmap (BS.intercalate "\n") $ drop 1 $ splitOn [begin] out-  let finstas = filterLast (not . (partialInstance `BS.isSuffixOf`)) instas-  return $ either (error . show) id . parseInstance <$> finstas-  where-    begin :: ByteString-    begin = "---INSTANCE---"-    partialInstance :: ByteString-    partialInstance = "---PARTIAL_INSTANCE---"-    filterLast _ []     = []-    filterLast p x@[_]  = filter p x-    filterLast p (x:xs) = x:filterLast p xs-    getWholeOutput h = do-      eof <- hIsEOF h-      if eof-        then return []-      else catch-        ((:) <$> BS.hGetLine h <*> getWholeOutput h)-        (\(_ :: IOException) -> return [partialInstance])-    printContentOnError ph = do-      code <- waitForProcess ph-      when (code == ExitFailure 1)-        $ putStrLn $ "Failed parsing the Alloy code:\n" <> content-    listenForOutput h = do-      mvar <- newEmptyMVar-      pid <- forkIO $ getWholeOutput h >>= putMVar mvar-      return (pid, mvar)-    getOutput (pid, mvar) = do-      output <- takeMVar mvar-      killThread pid-      return output--{-|-Start a new process that aborts execution by closing all handles and-killing the processes after the given amount of time.--}-startTimeout-  :: Handle-  -- ^ the input handle to close-  -> Handle-  -- ^ the output handle to close-  -> Handle-  -- ^ the error handle to close-  -> ProcessHandle-  -- ^ the main process handle-  -> Int -> IO ThreadId-startTimeout i o e ph t = forkIO $ do-  threadDelay t-  void $ forkIO $ hClose e-  void $ forkIO $ hClose o-  terminateProcess ph-  hClose i--{-|-Check if the class path was determined already, if so use it, otherwise call-'readClassPath'.--Returns the class path.--}-getClassPath :: IO FilePath-getClassPath = do-  mclassPath' <- readIORef mclassPath-  maybe readClassPath return mclassPath'--{--{--data CallAlloyConfig = Config {-    alloyJarFile   :: FilePath,-    alloyClassFile :: FilePath,-    keepFiles      :: Bool-  }--}--jarFileEnv :: String-jarFileEnv = "ALLOY_JAR_FILE"--callAlloyEnv :: String-callAlloyEnv = "CALL_ALLOY_CLASS_FILE"--keepFilesEnv :: String-keepFilesEnv = "KEEP_ALLOY_FILES"--{-|-Lookup environment variables which are to prefer if present.--}-getEnvironmentInformation :: IO CallAlloyConfig-getEnvironmentInformation = do-  alloy     <- lookupEnv jarFileEnv-  callAlloy <- lookupEnv callAlloyEnv-  keep      <- lookupEnv keepFilesEnv-  let mconfig = Config <$> alloy <*> callAlloy <*> pure (isJust keep)-  case mconfig of-    Nothing -> do-      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"-    Just c  -> return c--}-{--getVersionFile :: IO FilePath-getVersionFile = do-  configDir <- getXdgDirectory XdgConfig appName-  let versionFile = configDir </> "version"-  exists <- doesFileExist versionFile-  if exists-    then do-    version <- read <$> readFile versionFile-    unless (version == versionHash) $ createVersionFile configDir versionFile-    else createVersionFile configDir versionFile--}--fallbackToTempDir :: IO FilePath -> IO FilePath-fallbackToTempDir m = catch m $ \e ->-  if isDoesNotExistError e-  then do-    tmp    <- getTemporaryDirectory-#if defined(mingw32_HOST_OS)-    login  <- getUserName-#else-    login  <- getLoginName-#endif-    let tmpDir = tmp </> show (hash login) </> appName-    createUserDirectoriesIfMissing tmpDir-    return tmpDir-  else error $ show e--{-|-Read the class path version specified in the user directory, if it is not-current or if it does not exist, call 'createVersionFile'.--Returns the class path.--}-readClassPath :: IO FilePath-readClassPath = do-  configDir <- fallbackToTempDir $ getXdgDirectory XdgConfig appName-  let versionFile = configDir </> "version"-  exists <- doesFileExist versionFile-  if exists-    then do-    version <- read <$> readFile versionFile-    unless (version == versionHash) $ createVersionFile configDir versionFile-    else createVersionFile configDir versionFile-  dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"-  return $ dataDir ++ searchPathSeparator : dataDir </> alloyJarName-    ++ searchPathSeparator : dataDir </> commonsCliJarName--{-|-Create all library files within the users 'XdgDirectory' by calling-'createDataDir' then place the current version number into a configuration File.--}-createVersionFile :: FilePath -> FilePath -> IO ()-createVersionFile configDir versionFile = do-  createDataDir-  createUserDirectoriesIfMissing configDir-  writeFile versionFile $ show versionHash--{-|-Create all library files within the users 'XdgDirectory' based on the source-files enclosed into this library (see also 'Language.Alloy.RessourceNames' and-'Language.Alloy.Ressources').--}-createDataDir :: IO ()-createDataDir = do-  dataDir <- fallbackToTempDir $ getXdgDirectory XdgData $ appName </> "dataDir"-  createUserDirectoriesIfMissing $ dataDir </> classPackage-  BS.writeFile (dataDir </> classPackage </> className <.> "class") classFile-  BS.writeFile (dataDir </> alloyJarName) alloyJar-  BS.writeFile (dataDir </> commonsCliJarName) commonsCliJar--{-|-Creates user directories using the file permissions 700.-This function creates the specified directory and all its parent directories as-well (if they are also missing).--}-createUserDirectoriesIfMissing :: FilePath -> IO ()-createUserDirectoriesIfMissing fp = do-  isDir <- doesDirectoryExist fp-  let parent = takeDirectory fp-  unless (isDir || parent == fp) $ do-    createUserDirectoriesIfMissing parent-    createDirectory fp-#ifndef mingw32_HOST_OS-    setFileMode fp (7*8*8)-#endif+getInstancesWith config content =+  map (either (error . show) id . parseInstance)+  <$> getRawInstancesWith config content  {-| Check if there exists a model for the given specification. This function calls@@ -354,21 +69,3 @@   -> IO Bool   -- ^ Whether there exists an instance (within the relevant scope). existsInstance = fmap (not . null) . getInstances (Just 1)--{-|-The application name (used to store data in a specific directory.--}-appName :: String-appName = "call-alloy"--{-# INLINE versionHash #-}-{-|-Used to determine possible source code and Alloy version changes across multiple-versions of this library.--}-versionHash :: Int-versionHash = hash $ alloyHash + commonsCliHash + classFileHash-  where-    alloyHash = hash alloyJar-    commonsCliHash = hash commonsCliJar-    classFileHash = hash classFile

@@ -0,0 +1,14 @@+{-|+Module      : Language.Alloy.Call+Copyright   : (c) Marcellus Siegburg, 2019 - 2021+License     : MIT++This module provides functions to retrieve raw instances form Alloy,+i.e. as Alloy provides them.+-}+module Language.Alloy.Debug (+  getRawInstances,+  getRawInstancesWith,+  ) where++import Language.Alloy.Internal.Call     (getRawInstances, getRawInstancesWith)

@@ -11,6 +11,8 @@ -} module Language.Alloy.Functions (   getSingle, getDouble, getTriple,+  getSingleAs, getDoubleAs, getTripleAs,+  int, object,   lookupSig,   objectName,   relToMap,@@ -48,7 +50,83 @@ unscoped :: String -> Signature unscoped = Signature Nothing +{-+Might be introduced some time in Data.Set in the containers package+see https://github.com/haskell/containers/issues/779+-}+traverseSet+  :: (Ord a, Applicative f)+  => (a2 -> f a)+  -> Set a2+  -> f (Set a)+traverseSet f = fmap S.fromList . traverse f . S.toList+ {-|+For retrieval of 'Int' values using a get... function.++e.g. returning all (within Alloy) available Int values could look like this++> do n <- lookupSig (unscoped "Int")+>    getSingleAs "" int n+-}+int+  :: (IsString s, MonadError s m, Semigroup s)+  => String+  -> Int+  -> m Int+int = object "" id++{-|+For retrieval of an unmixed type of values using a get... function+(should be the case for uniformly base named values;+this is usually never true for the universe (@lookupSig (unscoped "univ")@))+I.e. setting and checking the 'String' for the base name of the value to look for,+but failing in case anything different appears (unexpectedly).+-}+object+  :: (IsString s, MonadError s m, Semigroup s)+  => String+  -> (Int -> a)+  -> String+  -> Int+  -> m a+object s f s' g =+  if s /= s+  then throwError $ "expected an object of name " <> fromString s+    <> " but got an object of name "+    <> fromString s' <> "."+  else return $ f g++specifyObject+  :: (String -> Int -> m a)+  -> Object+  -> m a+specifyObject f o = case o of+  NumberObject i -> f "" i+  Object n i -> f n i+  NamedObject g -> error $ "there is no way of converting Object "+    ++ g+    ++ "\nPlease open an issue at https://github.com/marcellussiegburg/call-alloy stating what you tried to attempt"++{-|+Retrieve a set of values of a given 'AlloySig'.+Values will be created by applying the given mapping function from object Name+and 'Int' to value.+The mapping has to be injective (for all expected cases).+Successful if the signature's relation is a set (or empty).+-}+getSingleAs+  :: (IsString s, MonadError s m, Ord a)+  => String+  -> (String -> Int -> m a)+  -> AlloySig+  -> m (Set a)+getSingleAs s f inst = do+  set <- getSingle s inst+  traverseSet (specifyObject f) set++{-# DEPRECATED getSingle "use the typed version getSingleAs instead" #-}+{-| Retrieve a set of objects of a given 'AlloySig'. Successful if the signature's relation is a set (or empty). -}@@ -60,6 +138,29 @@ getSingle = lookupRel single  {-|+Retrieve a binary relation of values of given 'AlloySig'.+Values will be created by applying the given mapping functions from object Name+and 'Int' to the value.+The mapping has to be injective (for all expected cases).+Successful if the signature's relation is binary (or empty).+-}+getDoubleAs+  :: (IsString s, MonadError s m, Ord a, Ord b)+  => String+  -> (String -> Int -> m a)+  -> (String -> Int -> m b)+  -> AlloySig+  -> m (Set (a, b))+getDoubleAs s f g inst = do+  set <- getDouble s inst+  traverseSet applyMapping set+  where+    applyMapping (x, y) = (,)+      <$> specifyObject f x+      <*> specifyObject g y++{-# DEPRECATED getDouble "use the typed version getDoubleAs instead" #-}+{-| Retrieve a binary relation of objects of a given 'AlloySig'. Successful if the signature's relation is binary (or empty). -}@@ -71,6 +172,31 @@ getDouble = lookupRel double  {-|+Retrieve a ternary relation of values of a given 'AlloySig'.+Values will be created by applying the given mapping functions from object Name+and 'Int' to the value.+The mapping has to be injective (for all expected cases).+Successful if the signature's relation is ternary (or empty).+-}+getTripleAs+  :: (IsString s, MonadError s m, Ord a, Ord b, Ord c)+  => String+  -> (String -> Int -> m a)+  -> (String -> Int -> m b)+  -> (String -> Int -> m c)+  -> AlloySig+  -> m (Set (a, b, c))+getTripleAs s f g h inst = do+  set <- getTriple s inst+  traverseSet applyMapping set+  where+    applyMapping (x, y, z) = (,,)+      <$> specifyObject f x+      <*> specifyObject g y+      <*> specifyObject h z++{-# DEPRECATED getTriple "use the typed version getTripleAs instead" #-}+{-| Retrieve a ternary relation of objects of a given 'AlloySig'. Successful if the signature's relation is ternary (or empty). -}@@ -81,16 +207,15 @@   -> m (Set (Object, Object, Object)) getTriple = lookupRel triple +{-|+Transforms a relation into a Mapping.+-} 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.--}+{-# DEPRECATED relToMap "use binaryToMap instead" #-} relToMap   :: (IsString s, MonadError s m, Ord k, Ord v)   => (a -> (k, v))@@ -128,6 +253,7 @@     ++ " is missing in the Alloy instance"   Just e   -> return e +{-# DEPRECATED objectName "use the typed versions of get... e.g. getSingleAs instead of getSingle" #-} {-| Retrieve an object's name. -}

@@ -0,0 +1,350 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-|+Module      : Language.Alloy.Internal.Call+Copyright   : (c) Marcellus Siegburg, 2019 - 2021+License     : MIT++This module provides the basic internal functionality to retrieve the raw+results from calling Alloy.+It provides data types and functions to interact with Alloy.+-}+module Language.Alloy.Internal.Call (+  CallAlloyConfig (maxInstances, noOverflow, timeout),+  defaultCallAlloyConfig,+  getRawInstances,+  getRawInstancesWith,+  ) where++import qualified Data.ByteString                  as BS+  (hGetLine, intercalate, isSuffixOf, writeFile)+import qualified Data.ByteString.Char8            as BS (unlines)++import Control.Concurrent (+  ThreadId,+  forkIO, killThread, newEmptyMVar, putMVar, takeMVar, threadDelay,+  )+import Control.Exception                (IOException)+import Control.Monad                    (unless, void, when)+import Data.ByteString                  (ByteString)+import Data.ByteString.Char8            (unpack)+import Data.Hashable                    (hash)+import Data.IORef                       (IORef, newIORef, readIORef)+import Data.List.Split                  (splitOn)+import Data.Maybe                       (fromMaybe)+import System.Directory+  (XdgDirectory (..), createDirectory, doesFileExist, doesDirectoryExist,+   getTemporaryDirectory, getXdgDirectory)+import System.Directory.Internal        (setFileMode)+import System.Directory.Internal.Prelude+  (catch, isDoesNotExistError)+import System.Exit                      (ExitCode (..))+import System.FilePath+  ((</>), (<.>), searchPathSeparator, takeDirectory)+import System.IO+  (BufferMode (..), Handle, hClose, hFlush, hIsEOF, hPutStr, hSetBuffering)+import System.IO.Unsafe                 (unsafePerformIO)+import System.Process (+  CreateProcess (..), StdStream (..), ProcessHandle,+  createProcess, proc, terminateProcess, waitForProcess,+  )+#if defined(mingw32_HOST_OS)+import System.Win32.Info                (getUserName)+#else+import System.Posix.User                (getLoginName)+#endif++import Language.Alloy.RessourceNames (+  alloyJarName, className, classPackage, commonsCliJarName+  )+import Language.Alloy.Ressources        (alloyJar, classFile, commonsCliJar)++{-|+Configuration for calling alloy. These are:++ * maximal number of instances to retrieve ('Nothing' for all)+ * whether to not overflow when calculating numbers within Alloy+ * an timeout after which to forcibly kill Alloy+   (retrieving only instances that were returned before killing the process)+-}+data CallAlloyConfig = CallAlloyConfig {+  -- | maximal number of instances to retrieve ('Nothing' for all)+  maxInstances :: Maybe Integer,+  -- | whether to not overflow when calculating numbers within Alloy+  noOverflow   :: Bool,+  -- | the time in microseconds after which to forcibly kill Alloy+  --   ('Nothing' for never)+  timeout      :: Maybe Int+  }++{-|+Default configuration for calling Alloy. Defaults to:++ * retrieve all instances+ * do not overflow+-}+defaultCallAlloyConfig :: CallAlloyConfig+defaultCallAlloyConfig = CallAlloyConfig {+  maxInstances = Nothing,+  noOverflow   = True,+  timeout      = Nothing+  }++{-# NOINLINE mclassPath #-}+{-|+'IORef' for storing the class path.+-}+mclassPath :: IORef (Maybe FilePath)+mclassPath = unsafePerformIO (newIORef Nothing)++{-|+This function may be used to get all raw model instances for a given Alloy+specification. It calls Alloy via a Java interface and splits the raw instance+answers before returning the resulting list of raw instances.+-}+getRawInstances+  :: Maybe Integer+  -- ^ How many instances to return; 'Nothing' for all.+  -> String+  -- ^ The Alloy specification which should be loaded.+  -> IO [ByteString]+getRawInstances maxIs = getRawInstancesWith defaultCallAlloyConfig {+  maxInstances = maxIs+  }++{-|+This function may be used to get all raw model instances for a given Alloy+specification. It calls Alloy via a Java interface and splits the raw instance+answers before returning the resulting list of raw instances.+Parameters are set using a 'CallAlloyConfig'.+-}+getRawInstancesWith+  :: CallAlloyConfig+  -- ^ The configuration to be used.+  -> String+  -- ^ The Alloy specification which should be loaded.+  -> IO [ByteString]+getRawInstancesWith config content = do+  classPath <- getClassPath+  let callAlloy = proc "java"+        $ ["-cp", classPath, classPackage ++ '.' : className,+           "-i", show $ fromMaybe (-1) $ maxInstances config]+        ++ ["-o" | not $ noOverflow config]+  (Just hin, Just hout, Just herr, ph) <-+    createProcess callAlloy {+        std_out = CreatePipe,+        std_in  = CreatePipe,+        std_err = CreatePipe+      }+  pout <- listenForOutput hout+  perr <- listenForOutput herr+#ifndef mingw32_HOST_OS+  hSetBuffering hin NoBuffering+#endif+  hPutStr hin content+  hFlush hin+  hClose hin+  maybe (return ()) (void . startTimeout hin hout herr ph) $ timeout config+  out <- getOutput pout+  err <- getOutput perr+  printContentOnError ph+  unless (null err) $ fail $ unpack $ BS.unlines err+  let instas = fmap (BS.intercalate "\n") $ drop 1 $ splitOn [begin] out+  return $ filterLast (not . (partialInstance `BS.isSuffixOf`)) instas+  where+    begin :: ByteString+    begin = "---INSTANCE---"+    partialInstance :: ByteString+    partialInstance = "---PARTIAL_INSTANCE---"+    filterLast _ []     = []+    filterLast p x@[_]  = filter p x+    filterLast p (x:xs) = x:filterLast p xs+    getWholeOutput h = do+      eof <- hIsEOF h+      if eof+        then return []+      else catch+        ((:) <$> BS.hGetLine h <*> getWholeOutput h)+        (\(_ :: IOException) -> return [partialInstance])+    printContentOnError ph = do+      code <- waitForProcess ph+      when (code == ExitFailure 1)+        $ putStrLn $ "Failed parsing the Alloy code:\n" <> content+    listenForOutput h = do+      mvar <- newEmptyMVar+      pid <- forkIO $ getWholeOutput h >>= putMVar mvar+      return (pid, mvar)+    getOutput (pid, mvar) = do+      output <- takeMVar mvar+      killThread pid+      return output++{-|+Start a new process that aborts execution by closing all handles and+killing the processes after the given amount of time.+-}+startTimeout+  :: Handle+  -- ^ the input handle to close+  -> Handle+  -- ^ the output handle to close+  -> Handle+  -- ^ the error handle to close+  -> ProcessHandle+  -- ^ the main process handle+  -> Int -> IO ThreadId+startTimeout i o e ph t = forkIO $ do+  threadDelay t+  void $ forkIO $ hClose e+  void $ forkIO $ hClose o+  terminateProcess ph+  hClose i++{-|+Check if the class path was determined already, if so use it, otherwise call+'readClassPath'.++Returns the class path.+-}+getClassPath :: IO FilePath+getClassPath = do+  mclassPath' <- readIORef mclassPath+  maybe readClassPath return mclassPath'++{-+{-+data CallAlloyConfig = Config {+    alloyJarFile   :: FilePath,+    alloyClassFile :: FilePath,+    keepFiles      :: Bool+  }+-}++jarFileEnv :: String+jarFileEnv = "ALLOY_JAR_FILE"++callAlloyEnv :: String+callAlloyEnv = "CALL_ALLOY_CLASS_FILE"++keepFilesEnv :: String+keepFilesEnv = "KEEP_ALLOY_FILES"++{-|+Lookup environment variables which are to prefer if present.+-}+getEnvironmentInformation :: IO CallAlloyConfig+getEnvironmentInformation = do+  alloy     <- lookupEnv jarFileEnv+  callAlloy <- lookupEnv callAlloyEnv+  keep      <- lookupEnv keepFilesEnv+  let mconfig = Config <$> alloy <*> callAlloy <*> pure (isJust keep)+  case mconfig of+    Nothing -> do+      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"+    Just c  -> return c+-}+{-+getVersionFile :: IO FilePath+getVersionFile = do+  configDir <- getXdgDirectory XdgConfig appName+  let versionFile = configDir </> "version"+  exists <- doesFileExist versionFile+  if exists+    then do+    version <- read <$> readFile versionFile+    unless (version == versionHash) $ createVersionFile configDir versionFile+    else createVersionFile configDir versionFile+-}++fallbackToTempDir :: IO FilePath -> IO FilePath+fallbackToTempDir m = catch m $ \e ->+  if isDoesNotExistError e+  then do+    tmp    <- getTemporaryDirectory+#if defined(mingw32_HOST_OS)+    login  <- getUserName+#else+    login  <- getLoginName+#endif+    let tmpDir = tmp </> show (hash login) </> appName+    createUserDirectoriesIfMissing tmpDir+    return tmpDir+  else error $ show e++{-|+Read the class path version specified in the user directory, if it is not+current or if it does not exist, call 'createVersionFile'.++Returns the class path.+-}+readClassPath :: IO FilePath+readClassPath = do+  configDir <- fallbackToTempDir $ getXdgDirectory XdgConfig appName+  let versionFile = configDir </> "version"+  exists <- doesFileExist versionFile+  if exists+    then do+    version <- read <$> readFile versionFile+    unless (version == versionHash) $ createVersionFile configDir versionFile+    else createVersionFile configDir versionFile+  dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"+  return $ dataDir ++ searchPathSeparator : dataDir </> alloyJarName+    ++ searchPathSeparator : dataDir </> commonsCliJarName++{-|+Create all library files within the users 'XdgDirectory' by calling+'createDataDir' then place the current version number into a configuration File.+-}+createVersionFile :: FilePath -> FilePath -> IO ()+createVersionFile configDir versionFile = do+  createDataDir+  createUserDirectoriesIfMissing configDir+  writeFile versionFile $ show versionHash++{-|+Create all library files within the users 'XdgDirectory' based on the source+files enclosed into this library (see also 'Language.Alloy.RessourceNames' and+'Language.Alloy.Ressources').+-}+createDataDir :: IO ()+createDataDir = do+  dataDir <- fallbackToTempDir $ getXdgDirectory XdgData $ appName </> "dataDir"+  createUserDirectoriesIfMissing $ dataDir </> classPackage+  BS.writeFile (dataDir </> classPackage </> className <.> "class") classFile+  BS.writeFile (dataDir </> alloyJarName) alloyJar+  BS.writeFile (dataDir </> commonsCliJarName) commonsCliJar++{-|+Creates user directories using the file permissions 700.+This function creates the specified directory and all its parent directories as+well (if they are also missing).+-}+createUserDirectoriesIfMissing :: FilePath -> IO ()+createUserDirectoriesIfMissing fp = do+  isDir <- doesDirectoryExist fp+  let parent = takeDirectory fp+  unless (isDir || parent == fp) $ do+    createUserDirectoriesIfMissing parent+    createDirectory fp+#ifndef mingw32_HOST_OS+    setFileMode fp (7*8*8)+#endif++{-|+The application name (used to store data in a specific directory.+-}+appName :: String+appName = "call-alloy"++{-# INLINE versionHash #-}+{-|+Used to determine possible source code and Alloy version changes across multiple+versions of this library.+-}+versionHash :: Int+versionHash = hash $ alloyHash + commonsCliHash + classFileHash+  where+    alloyHash = hash alloyJar+    commonsCliHash = hash commonsCliJar+    classFileHash = hash classFile