call-alloy 0.4.1.1 → 0.5

raw patch · 9 files changed

+445/−103 lines, 9 filesdep +exceptionsdep +file-embeddep −mtldep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: exceptions, file-embed

Dependencies removed: mtl

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• README.md +179/−53
• call-alloy.cabal +9/−4
• src/Language/Alloy/Call.hs +13/−9
• src/Language/Alloy/Exceptions.hs +116/−0
• src/Language/Alloy/Functions.hs +31/−29
• src/Language/Alloy/Parser.hs +7/−8
• test/ReadmeExample.hs +35/−0
• test/ReadmeExampleSpec.hs +50/−0

@@ -4,6 +4,11 @@  ## Released changes +### 0.5++- use MonadThrow instead of MonadError+- add Readme eample to test cases+ ### 0.4.1.1  - introduce flag for testing different SAT solvers

@@ -26,6 +26,8 @@ Consider this Alloy specification of a simple Graph:  ```Alloy+# test/unit/readmeExampleSpecification.als+ abstract sig Node {   flow : Node -> lone Int,   stored : one Int@@ -46,6 +48,7 @@ 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`).@@ -57,52 +60,149 @@ ### An instance example  Calling Alloy using `getInstances` and the above program-could return the following (abbreviated) instance:+could return the following 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})-        ]))-      ]-    })- ]+```hs+-- test/unit/readmeExampleInstance.hs++fromList [+  ( 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 = Nothing, sigName = "Int"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Single (fromList [+            NumberObject {number = -4},+            NumberObject {number = -3},+            NumberObject {number = -2},+            NumberObject {number = -1},+            NumberObject {number = 0},+            NumberObject {number = 1},+            NumberObject {number = 2},+            NumberObject {number = 3}+            ]))+        ]+      }),+  ( Signature {scope = Nothing, sigName = "String"},+    Entry {+      annotation = Nothing,+      relation = fromList [("", EmptyRelation)]+      }),+  ( Signature {scope = Nothing, sigName = "end"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Id (NumberObject {number = 0}))+        ]+      }),+  ( Signature {scope = Nothing, sigName = "integers"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Single (fromList [+            NumberObject {number = -4},+            NumberObject {number = -3},+            NumberObject {number = -2},+            NumberObject {number = -1},+            NumberObject {number = 0},+            NumberObject {number = 1},+            NumberObject {number = 2},+            NumberObject {number = 3}+            ]))+        ]+      }),+  ( Signature {scope = Nothing, sigName = "loop"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Id (NumberObject {number = 0}))+        ]+      }),+  ( Signature {scope = Nothing, sigName = "none"},+    Entry {+      annotation = Nothing,+      relation = fromList [("", EmptyRelation)]+  }),+  ( Signature {scope = Nothing, sigName = "univ"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Single (fromList [+            Object {objSig = "Node", identifier = 0},+            Object {objSig = "Node", identifier = 1},+            NumberObject {number = -4},+            NumberObject {number = -3},+            NumberObject {number = -2},+            NumberObject {number = -1},+            NumberObject {number = 0},+            NumberObject {number = 1},+            NumberObject {number = 2},+            NumberObject {number = 3}+            ]))+        ]+      }),+  ( Signature {scope = Just "seq", sigName = "Int"},+    Entry {+      annotation = Nothing,+      relation = fromList [+        ( "",+          Single (fromList [+            NumberObject {number = 0},+            NumberObject {number = 1},+            NumberObject {number = 2}+            ]))+        ]+      }),+  ( 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 = 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@@ -113,14 +213,36 @@  The following Code might for instance be used for the graph example: -``` Haskell-newtype Node = Node Int deriving (Eq, Show, Ord)+```hs+-- test/readmeExample.hs +module ReadmeExample (+  Node (Node),+  instanceToNames,+  ) where++import Control.Monad.Catch              (MonadThrow)+import Data.Set                         (Set)++import Language.Alloy.Call (+  AlloyInstance,+  getDoubleAs,+  getSingleAs,+  getTripleAs,+  int,+  lookupSig,+  object,+  scoped,+  unscoped,+  )+newtype Node = Node Int deriving (Eq, Show, Ord, Read)+ instanceToNames-  :: AlloyInstance-  -> Either String (Set Node, Set (Node, Int), Set (Node, Node, Int), Set (Node), Set (Node))+  :: MonadThrow m+  => AlloyInstance+  -> m (Set Node, Set (Node, Int), Set (Node, Node, Int), Set Node, Set Node) instanceToNames insta = do-  let node :: String -> Int -> Either String Node+  let node :: MonadThrow m => String -> Int -> m Node       node = object "Node" Node   n     <- lookupSig (scoped "this" "Node") insta   nodes <- getSingleAs "" node n@@ -129,16 +251,20 @@   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 (+```hs+-- test/unit/readmeExampleResult.hs++(   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,Node 0,3)],   fromList [Node 1],   fromList [Node 0]   )+ ```

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           call-alloy-version:        0.4.1.1+version:        0.5 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@@ -13,7 +13,7 @@ bug-reports:    https://github.com/marcellussiegburg/call-alloy/issues author:         Marcellus Siegburg maintainer:     marcellus.siegburg@uni-due.de-copyright:      2019-2022 Marcellus Siegburg+copyright:      2019-2024 Marcellus Siegburg license:        MIT license-file:   LICENSE build-type:     Simple@@ -45,6 +45,7 @@   exposed-modules:       Language.Alloy.Call       Language.Alloy.Debug+      Language.Alloy.Exceptions   other-modules:       Language.Alloy.Functions       Language.Alloy.Internal.Call@@ -62,9 +63,9 @@     , bytestring >=0.10.4 && <0.13     , containers >=0.6 && <0.8     , directory ==1.3.*+    , exceptions >=0.8.1 && <0.11     , extra ==1.7.*     , filepath ==1.4.*-    , mtl >=2.2 && <2.4     , process ==1.6.*     , split ==0.2.*     , transformers >=0.5.0.0 && <0.7@@ -84,6 +85,7 @@   other-modules:       Language.Alloy.Call       Language.Alloy.Debug+      Language.Alloy.Exceptions       Language.Alloy.Functions       Language.Alloy.Internal.Call       Language.Alloy.Parser@@ -91,6 +93,8 @@       Language.Alloy.Ressources       Language.Alloy.Types       Language.Alloy.CallSpec+      ReadmeExample+      ReadmeExampleSpec       Paths_call_alloy   hs-source-dirs:       src@@ -103,10 +107,11 @@     , call-alloy     , containers >=0.6 && <0.8     , directory ==1.3.*+    , exceptions >=0.8.1 && <0.11     , extra ==1.7.*+    , file-embed     , filepath ==1.4.*     , hspec-    , mtl >=2.2 && <2.4     , process ==1.6.*     , split ==0.2.*     , string-interpolate

@@ -28,7 +28,8 @@ import Language.Alloy.Types             as Types   (AlloyInstance, AlloySig, Entries, Object, Signature) -import Control.Monad.Trans.Except       (runExceptT)+import Control.Monad.Catch              (MonadThrow)+import Control.Monad.IO.Class           (MonadIO (liftIO))  {-| This function may be used to get all model instances for a given Alloy@@ -36,11 +37,12 @@ answers before returning the resulting list of 'AlloyInstance's. -} getInstances-  :: Maybe Integer+  :: (MonadIO m, MonadThrow m)+  => Maybe Integer   -- ^ How many instances to return; 'Nothing' for all.   -> String   -- ^ The Alloy specification which should be loaded.-  -> IO [AlloyInstance]+  -> m [AlloyInstance] getInstances maxIs = getInstancesWith defaultCallAlloyConfig {   maxInstances = maxIs   }@@ -52,14 +54,15 @@ Parameters are set using a 'CallAlloyConfig'. -} getInstancesWith-  :: CallAlloyConfig+  :: (MonadIO m, MonadThrow m)+  => CallAlloyConfig   -- ^ The configuration to be used.   -> String   -- ^ The Alloy specification which should be loaded.-  -> IO [AlloyInstance]+  -> m [AlloyInstance] getInstancesWith config content =-  getRawInstancesWith config content-  >>= mapM (fmap (either (error . show) id) . runExceptT . parseInstance)+  liftIO (getRawInstancesWith config content)+  >>= mapM parseInstance  {-| Check if there exists a model for the given specification. This function calls@@ -67,8 +70,9 @@ This function calls 'getInstances'. -} existsInstance-  :: String+  :: (MonadIO m, MonadThrow m)+  => String   -- ^ The Alloy specification which should be loaded.-  -> IO Bool+  -> m Bool   -- ^ Whether there exists an instance (within the relevant scope). existsInstance = fmap (not . null) . getInstances (Just 1)

@@ -0,0 +1,116 @@+{-# LANGUAGE GADTs #-}+-- | Defines Exceptions that can occur while using the call-alloy library++module Language.Alloy.Exceptions (+  CallAlloyException (..),+  AlloyLookupFailed (..),+  AlloyObjectNameMismatch (..),+  AlloyResponseFailure (..),+  UnexpectedAlloyRelation (..),+  Alternatives (..),+  Expected (..),+  Got (..),+  RelationName (..),+  ) where++import qualified Data.Map                         as M (keys)++import Control.Exception (+  Exception (fromException, toException),+  SomeException,+  )+import Data.List                        (intercalate)+import Data.Typeable                    (cast)+import Language.Alloy.Types (+  AlloyInstance,+  Signature (..),+  showSignature,+  )+import Text.Trifecta.Result             (ErrInfo)++data CallAlloyException where+  CallAlloyException :: Exception e => e -> CallAlloyException++instance Show CallAlloyException where+    show (CallAlloyException e) = show e++instance Exception CallAlloyException++alloyExceptionToException :: Exception e => e -> SomeException+alloyExceptionToException = toException . CallAlloyException++alloyExceptionFromException :: Exception e => SomeException -> Maybe e+alloyExceptionFromException x = do+  CallAlloyException a <- fromException x+  cast a++newtype AlloyResponseFailure+  = ParsingAlloyResponseFailed ErrInfo+  deriving Show++instance Exception AlloyResponseFailure where+  toException = alloyExceptionToException+  fromException = alloyExceptionFromException++newtype Expected = Expected {unExpected :: String}+newtype Got = Got {unGot :: String}++data AlloyObjectNameMismatch+  = AlloyObjectNameMismatch !Expected !Got++instance Show AlloyObjectNameMismatch where+  show (AlloyObjectNameMismatch expected got)+    = "AlloyObjectNameMismatch: "+    <> "expected an object of name " <> unExpected expected+    <> " but got an object of name " <> unGot got++instance Exception AlloyObjectNameMismatch where+  toException = alloyExceptionToException+  fromException = alloyExceptionFromException++newtype RelationName = RelationName {unRelationName :: String}+newtype Alternatives a = Alternatives {unAlternatives :: [a]}++data AlloyLookupFailed+  = LookupAlloySignatureFailed !Signature !AlloyInstance+  | LookupAlloyRelationFailed !RelationName !(Alternatives RelationName)++instance Show AlloyLookupFailed where+  show (LookupAlloySignatureFailed s insta) = "LookupAlloySignatureFailed: "+    <> showSignature s+    <> " is missing in the Alloy instance"+    <> "; available are: \""+    <> intercalate "\", " (showSignature <$> M.keys insta)+  show (LookupAlloyRelationFailed rel xs) = "LookupAlloyRelationFailed: "+    <> "relation " ++ unRelationName rel+    <> " is missing in the Alloy instance"+    <> "; available are: "+    <> intercalate ", " (map unRelationName $ unAlternatives xs)++instance Exception AlloyLookupFailed where+  toException = alloyExceptionToException+  fromException = alloyExceptionFromException++data UnexpectedAlloyRelation+  = ExpectedIdenticalRelationship+  | ExpectedSingleRelationship+  | ExpectedDoubleRelationship+  | ExpectedTripleRelationship++instance Show UnexpectedAlloyRelation where+  show ExpectedIdenticalRelationship+    = "ExpectedIdenticalRelationship: "+    <> "Relation is (unexpectedly) not exactly a single element"+  show ExpectedSingleRelationship+    = "ExpectedSingleRelationship: "+    <> "Relation is (unexpectedly) a mapping"+  show ExpectedDoubleRelationship+    = "ExpectedDoubleRelationship: "+    <> "Relation is not a binary mapping"+  show ExpectedTripleRelationship+    = "ExpectedTripleRelationship: "+    <> "Relation is not a ternary mapping"++instance Exception UnexpectedAlloyRelation where+  toException = alloyExceptionToException+  fromException = alloyExceptionFromException

@@ -19,12 +19,19 @@ import qualified Data.Set                         as S (fromList, toList) import qualified Data.Map                         as M (lookup, keys) -import Control.Monad.Except             (MonadError, throwError)-import Data.List                        (intercalate)+import Control.Monad.Catch              (MonadThrow, throwM) import Data.Map                         (Map) import Data.Set                         (Set)-import Data.String                      (IsString, fromString) +import Language.Alloy.Exceptions (+  AlloyLookupFailed (..),+  AlloyObjectNameMismatch (..),+  Alternatives (Alternatives),+  Expected (Expected),+  Got (Got),+  RelationName (RelationName),+  UnexpectedAlloyRelation (..),+  ) import Language.Alloy.Types (   AlloyInstance,   AlloySig,@@ -32,7 +39,6 @@   Object (..),   Relation (..),   Signature (..),-  showSignature,   )  {-|@@ -67,7 +73,7 @@ >    getSingleAs "" int n -} int-  :: (IsString s, MonadError s m, Semigroup s)+  :: MonadThrow m   => String   -> Int   -> m Int@@ -81,7 +87,7 @@ but failing in case anything different appears (unexpectedly). -} object-  :: (IsString s, MonadError s m, Semigroup s)+  :: MonadThrow m   => String   -> (Int -> a)   -> String@@ -89,9 +95,7 @@   -> 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' <> "."+  then throwM $ AlloyObjectNameMismatch (Expected s) (Got s')   else return $ f g  specifyObject@@ -113,7 +117,7 @@ Successful if the signature's relation is a single value. -} getIdentityAs-  :: (MonadError s m, IsString s)+  :: MonadThrow m   => String   -> (String -> Int -> m b)   -> Entry Map a@@ -130,7 +134,7 @@ Successful if the signature's relation is a set (or empty). -} getSingleAs-  :: (IsString s, MonadError s m, Ord a)+  :: (MonadThrow m, Ord a)   => String   -> (String -> Int -> m a)   -> AlloySig@@ -147,7 +151,7 @@ Successful if the signature's relation is binary (or empty). -} getDoubleAs-  :: (IsString s, MonadError s m, Ord a, Ord b)+  :: (MonadThrow m, Ord a, Ord b)   => String   -> (String -> Int -> m a)   -> (String -> Int -> m b)@@ -169,7 +173,7 @@ Successful if the signature's relation is ternary (or empty). -} getTripleAs-  :: (IsString s, MonadError s m, Ord a, Ord b, Ord c)+  :: (MonadThrow m, Ord a, Ord b, Ord c)   => String   -> (String -> Int -> m a)   -> (String -> Int -> m b)@@ -186,58 +190,56 @@       <*> specifyObject h z  lookupRel-  :: (IsString s, MonadError s m)+  :: MonadThrow 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"-    ++ "; available are: " ++ intercalate ", " (M.keys $ relation e)+  Nothing -> throwM $ LookupAlloyRelationFailed+    (RelationName rel)+    (Alternatives $ map RelationName $ M.keys $ relation e)   Just r  -> kind r  {-| Lookup a signature within a given Alloy instance. -} lookupSig-  :: (IsString s, MonadError s m)+  :: MonadThrow m   => Signature   -> AlloyInstance   -> m AlloySig lookupSig s insta = case M.lookup s insta of-  Nothing -> throwError $ fromString $ showSignature s-    ++ " is missing in the Alloy instance"-    ++ "; available are: \"" ++ intercalate "\", " (showSignature <$> M.keys insta)+  Nothing -> throwM $ LookupAlloySignatureFailed s insta   Just e   -> return e  identity-  :: (IsString s, MonadError s m)+  :: (MonadThrow m)   => Relation a   -> m Object identity (Id r) = return r-identity _      = throwError "Relation is (unexpectedly) not exactly a single element"+identity _      = throwM ExpectedIdenticalRelationship  single-  :: (IsString s, MonadError s m, Monoid (a Object))+  :: (MonadThrow 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"+single _             = throwM ExpectedSingleRelationship  double-  :: (IsString s, MonadError s m, Monoid (a (Object, Object)))+  :: (MonadThrow 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"+double _             = throwM ExpectedDoubleRelationship  triple-  :: (IsString s, MonadError s m, Monoid (a (Object, Object, Object)))+  :: (MonadThrow 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"+triple _             = throwM ExpectedTripleRelationship

@@ -24,8 +24,8 @@  import Control.Applicative              ((<|>)) import Control.Monad                    (void)+import Control.Monad.Catch              (MonadThrow (throwM)) import Control.Monad.IO.Class           (MonadIO (liftIO))-import Control.Monad.Except             (MonadError, throwError) import Data.ByteString                  (ByteString) import Data.Functor                     (($>)) import Data.List                        (intercalate)@@ -34,6 +34,7 @@ import Data.Set                         (Set) import Text.Trifecta +import Language.Alloy.Exceptions        (AlloyResponseFailure (..)) import Language.Alloy.Types (   AlloyInstance,   Annotation (..),@@ -46,17 +47,17 @@  {-| Parse an Alloy instance from a given String.-May fail with 'ErrInfo'.+May fail with 'ParsingAlloyResponseFailed'. -} parseInstance-  :: (MonadIO m, MonadError ErrInfo m)+  :: (MonadIO m, MonadThrow m)   => ByteString   -> m AlloyInstance parseInstance inst = case parseByteString alloyInstance mempty inst of   Failure l -> do     liftIO $ BS.putStrLn "Failed parsing Alloys response as AlloyInstance:"     liftIO $ BS.putStrLn inst-    throwError l+    throwM $ ParsingAlloyResponseFailed l   Success r -> return $ combineEntries r  combineEntries :: [Entries (,)] -> AlloyInstance@@ -84,11 +85,9 @@ entry = do   entryAnnotation <- try (string "skolem " $> Just Skolem) <|> pure Nothing   entrySignature <- sig-  (entrySignature,)-    <$> (Entry entryAnnotation-         <$> ((,)+  (entrySignature,) . Entry entryAnnotation <$> ((,)               <$> ((string "<:" *> word) <|> pure "")-              <*> parseRelations <* (void endOfLine <|> eof)))+              <*> parseRelations <* (void endOfLine <|> eof))  sig :: Parser Signature sig = do

@@ -0,0 +1,35 @@+module ReadmeExample (+  Node (Node),+  instanceToNames,+  ) where++import Control.Monad.Catch              (MonadThrow)+import Data.Set                         (Set)++import Language.Alloy.Call (+  AlloyInstance,+  getDoubleAs,+  getSingleAs,+  getTripleAs,+  int,+  lookupSig,+  object,+  scoped,+  unscoped,+  )+newtype Node = Node Int deriving (Eq, Show, Ord, Read)++instanceToNames+  :: MonadThrow m+  => AlloyInstance+  -> m (Set Node, Set (Node, Int), Set (Node, Node, Int), Set Node, Set Node)+instanceToNames insta = do+  let node :: MonadThrow m => String -> Int -> m 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)

@@ -0,0 +1,50 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wno-orphans #-}+module ReadmeExampleSpec (spec) where++import Data.FileEmbed                   (embedStringFile)+import Data.Map                         (Map)+import Data.Set                         (Set)+import Test.Hspec++import Language.Alloy.Call              (getInstances)+import ReadmeExample                    (instanceToNames)++import Language.Alloy.Types (+  Annotation (..),+  Entry (..),+  Object (..),+  Relation (..),+  Signature (..),+  )++deriving instance Eq (Entry Map Set)+deriving instance Eq (Relation Set)+deriving instance Read Annotation+deriving instance Read (Entry Map Set)+deriving instance Read Object+deriving instance Read (Relation Set)+deriving instance Read Signature+deriving instance Show (Entry Map Set)+deriving instance Show (Relation Set)++spec :: Spec+spec =+  describe "readme example" $ do+    it "returns expected instance" $+      getFirstInstance+        `shouldReturn`+        read $(embedStringFile "test/unit/readmeExampleInstance.hs")+    it "returns expected result" $ do+      i <- getFirstInstance+      instanceToNames i+        `shouldReturn`+        read $(embedStringFile "test/unit/readmeExampleResult.hs")+  where+    getFirstInstance = do+      i:_ <- getInstances+        (Just 1)+        $(embedStringFile "test/unit/readmeExampleSpecification.als")+      pure i