{-# 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 (
  getIdentityAs, getSingleAs, getDoubleAs, getTripleAs,
  int, object,
  lookupSig,
  scoped, unscoped,
  ) where

import qualified Data.Set                         as S (fromList, toList)
import qualified Data.Map                         as M (lookup, keys)

import Control.Monad.Catch              (MonadThrow, throwM)
import Data.Map                         (Map)
import Data.Set                         (Set)

import Language.Alloy.Exceptions (
  AlloyLookupFailed (..),
  AlloyObjectNameMismatch (..),
  Alternatives (Alternatives),
  Expected (Expected),
  Got (Got),
  RelationName (RelationName),
  UnexpectedAlloyRelation (..),
  )
import Language.Alloy.Types (
  AlloyInstance,
  AlloySig,
  Entry (..),
  Object (..),
  Relation (..),
  Signature (..),
  )

{-|
Create a 'Signature' given its scope and name.
-}
scoped :: String -> String -> Signature
scoped :: String -> String -> Signature
scoped = Maybe String -> String -> Signature
Signature (Maybe String -> String -> Signature)
-> (String -> Maybe String) -> String -> String -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
forall a. a -> Maybe a
Just

{-|
Create an unscoped 'Signature' given its name.
-}
unscoped :: String -> Signature
unscoped :: String -> Signature
unscoped = Maybe String -> String -> Signature
Signature Maybe String
forall a. Maybe a
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 :: forall a (f :: * -> *) a2.
(Ord a, Applicative f) =>
(a2 -> f a) -> Set a2 -> f (Set a)
traverseSet a2 -> f a
f = ([a] -> Set a) -> f [a] -> f (Set a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList (f [a] -> f (Set a)) -> (Set a2 -> f [a]) -> Set a2 -> f (Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a2 -> f a) -> [a2] -> f [a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a2 -> f a
f ([a2] -> f [a]) -> (Set a2 -> [a2]) -> Set a2 -> f [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a2 -> [a2]
forall a. Set a -> [a]
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
  :: MonadThrow m
  => String
  -> Int
  -> m Int
int :: forall (m :: * -> *). MonadThrow m => String -> Int -> m Int
int = String -> (Int -> Int) -> String -> Int -> m Int
forall (m :: * -> *) a.
MonadThrow m =>
String -> (Int -> a) -> String -> Int -> m a
object String
"" Int -> Int
forall a. a -> a
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
  :: MonadThrow m
  => String
  -> (Int -> a)
  -> String
  -> Int
  -> m a
object :: forall (m :: * -> *) a.
MonadThrow m =>
String -> (Int -> a) -> String -> Int -> m a
object String
s Int -> a
f String
s' Int
g =
  if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
s
  then AlloyObjectNameMismatch -> m a
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM (AlloyObjectNameMismatch -> m a) -> AlloyObjectNameMismatch -> m a
forall a b. (a -> b) -> a -> b
$ Expected -> Got -> AlloyObjectNameMismatch
AlloyObjectNameMismatch (String -> Expected
Expected String
s) (String -> Got
Got String
s')
  else a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Int -> a
f Int
g

specifyObject
  :: (String -> Int -> m a)
  -> Object
  -> m a
specifyObject :: forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m a
f Object
o = case Object
o of
  NumberObject Int
i -> String -> Int -> m a
f String
"" Int
i
  Object String
n Int
i -> String -> Int -> m a
f String
n Int
i
  NamedObject String
g -> String -> m a
forall a. HasCallStack => String -> a
error (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"there is no way of converting Object "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nPlease open an issue at https://github.com/marcellussiegburg/call-alloy stating what you tried to attempt"

{-|
Retrieve a single value of a given 'AlloySig'.
The Value 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 single value.
-}
getIdentityAs
  :: MonadThrow m
  => String
  -> (String -> Int -> m b)
  -> Entry Map a
  -> m b
getIdentityAs :: forall (m :: * -> *) b (a :: * -> *).
MonadThrow m =>
String -> (String -> Int -> m b) -> Entry Map a -> m b
getIdentityAs String
s String -> Int -> m b
f Entry Map a
inst = do
  Object
e <- (Relation a -> m Object) -> String -> Entry Map a -> m Object
forall (m :: * -> *) (a :: * -> *) b.
MonadThrow m =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation a -> m Object
forall (m :: * -> *) (a :: * -> *).
MonadThrow m =>
Relation a -> m Object
identity String
s Entry Map a
inst
  (String -> Int -> m b) -> Object -> m b
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m b
f Object
e

{-|
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
  :: (MonadThrow m, Ord a)
  => String
  -> (String -> Int -> m a)
  -> AlloySig
  -> m (Set a)
getSingleAs :: forall (m :: * -> *) a.
(MonadThrow m, Ord a) =>
String -> (String -> Int -> m a) -> AlloySig -> m (Set a)
getSingleAs String
s String -> Int -> m a
f AlloySig
inst = do
  Set Object
set <- (Relation Set -> m (Set Object))
-> String -> AlloySig -> m (Set Object)
forall (m :: * -> *) (a :: * -> *) b.
MonadThrow m =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set Object)
forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a Object)) =>
Relation a -> m (a Object)
single String
s AlloySig
inst
  (Object -> m a) -> Set Object -> m (Set a)
forall a (f :: * -> *) a2.
(Ord a, Applicative f) =>
(a2 -> f a) -> Set a2 -> f (Set a)
traverseSet ((String -> Int -> m a) -> Object -> m a
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m a
f) Set Object
set

{-|
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
  :: (MonadThrow m, Ord a, Ord b)
  => String
  -> (String -> Int -> m a)
  -> (String -> Int -> m b)
  -> AlloySig
  -> m (Set (a, b))
getDoubleAs :: forall (m :: * -> *) a b.
(MonadThrow m, Ord a, Ord b) =>
String
-> (String -> Int -> m a)
-> (String -> Int -> m b)
-> AlloySig
-> m (Set (a, b))
getDoubleAs String
s String -> Int -> m a
f String -> Int -> m b
g AlloySig
inst = do
  Set (Object, Object)
set <- (Relation Set -> m (Set (Object, Object)))
-> String -> AlloySig -> m (Set (Object, Object))
forall (m :: * -> *) (a :: * -> *) b.
MonadThrow m =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set (Object, Object))
forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a (Object, Object))) =>
Relation a -> m (a (Object, Object))
double String
s AlloySig
inst
  ((Object, Object) -> m (a, b))
-> Set (Object, Object) -> m (Set (a, b))
forall a (f :: * -> *) a2.
(Ord a, Applicative f) =>
(a2 -> f a) -> Set a2 -> f (Set a)
traverseSet (Object, Object) -> m (a, b)
applyMapping Set (Object, Object)
set
  where
    applyMapping :: (Object, Object) -> m (a, b)
applyMapping (Object
x, Object
y) = (,)
      (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Int -> m a) -> Object -> m a
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m a
f Object
x
      m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Int -> m b) -> Object -> m b
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m b
g Object
y

{-|
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
  :: (MonadThrow 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 :: forall (m :: * -> *) a b c.
(MonadThrow 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 String
s String -> Int -> m a
f String -> Int -> m b
g String -> Int -> m c
h AlloySig
inst = do
  Set (Object, Object, Object)
set <- (Relation Set -> m (Set (Object, Object, Object)))
-> String -> AlloySig -> m (Set (Object, Object, Object))
forall (m :: * -> *) (a :: * -> *) b.
MonadThrow m =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set (Object, Object, Object))
forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a (Object, Object, Object))) =>
Relation a -> m (a (Object, Object, Object))
triple String
s AlloySig
inst
  ((Object, Object, Object) -> m (a, b, c))
-> Set (Object, Object, Object) -> m (Set (a, b, c))
forall a (f :: * -> *) a2.
(Ord a, Applicative f) =>
(a2 -> f a) -> Set a2 -> f (Set a)
traverseSet (Object, Object, Object) -> m (a, b, c)
applyMapping Set (Object, Object, Object)
set
  where
    applyMapping :: (Object, Object, Object) -> m (a, b, c)
applyMapping (Object
x, Object
y, Object
z) = (,,)
      (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Int -> m a) -> Object -> m a
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m a
f Object
x
      m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Int -> m b) -> Object -> m b
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m b
g Object
y
      m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Int -> m c) -> Object -> m c
forall (m :: * -> *) a. (String -> Int -> m a) -> Object -> m a
specifyObject String -> Int -> m c
h Object
z

lookupRel
  :: MonadThrow m
  => (Relation a -> m b)
  -> String
  -> Entry Map a
  -> m b
lookupRel :: forall (m :: * -> *) (a :: * -> *) b.
MonadThrow m =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation a -> m b
kind String
rel Entry Map a
e = case String -> Map String (Relation a) -> Maybe (Relation a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
rel (Entry Map a -> Map String (Relation a)
forall (a :: * -> * -> *) (b :: * -> *).
Entry a b -> a String (Relation b)
relation Entry Map a
e) of
  Maybe (Relation a)
Nothing -> AlloyLookupFailed -> m b
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM (AlloyLookupFailed -> m b) -> AlloyLookupFailed -> m b
forall a b. (a -> b) -> a -> b
$ RelationName -> Alternatives RelationName -> AlloyLookupFailed
LookupAlloyRelationFailed
    (String -> RelationName
RelationName String
rel)
    ([RelationName] -> Alternatives RelationName
forall a. [a] -> Alternatives a
Alternatives ([RelationName] -> Alternatives RelationName)
-> [RelationName] -> Alternatives RelationName
forall a b. (a -> b) -> a -> b
$ (String -> RelationName) -> [String] -> [RelationName]
forall a b. (a -> b) -> [a] -> [b]
map String -> RelationName
RelationName ([String] -> [RelationName]) -> [String] -> [RelationName]
forall a b. (a -> b) -> a -> b
$ Map String (Relation a) -> [String]
forall k a. Map k a -> [k]
M.keys (Map String (Relation a) -> [String])
-> Map String (Relation a) -> [String]
forall a b. (a -> b) -> a -> b
$ Entry Map a -> Map String (Relation a)
forall (a :: * -> * -> *) (b :: * -> *).
Entry a b -> a String (Relation b)
relation Entry Map a
e)
  Just Relation a
r  -> Relation a -> m b
kind Relation a
r

{-|
Lookup a signature within a given Alloy instance.
-}
lookupSig
  :: MonadThrow m
  => Signature
  -> AlloyInstance
  -> m AlloySig
lookupSig :: forall (m :: * -> *).
MonadThrow m =>
Signature -> AlloyInstance -> m AlloySig
lookupSig Signature
s AlloyInstance
insta = case Signature -> AlloyInstance -> Maybe AlloySig
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Signature
s AlloyInstance
insta of
  Maybe AlloySig
Nothing -> AlloyLookupFailed -> m AlloySig
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM (AlloyLookupFailed -> m AlloySig)
-> AlloyLookupFailed -> m AlloySig
forall a b. (a -> b) -> a -> b
$ Signature -> AlloyInstance -> AlloyLookupFailed
LookupAlloySignatureFailed Signature
s AlloyInstance
insta
  Just AlloySig
e   -> AlloySig -> m AlloySig
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return AlloySig
e

identity
  :: (MonadThrow m)
  => Relation a
  -> m Object
identity :: forall (m :: * -> *) (a :: * -> *).
MonadThrow m =>
Relation a -> m Object
identity (Id Object
r) = Object -> m Object
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Object
r
identity Relation a
_      = UnexpectedAlloyRelation -> m Object
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM UnexpectedAlloyRelation
ExpectedIdenticalRelationship

single
  :: (MonadThrow m, Monoid (a Object))
  => Relation a
  -> m (a Object)
single :: forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a Object)) =>
Relation a -> m (a Object)
single Relation a
EmptyRelation = a Object -> m (a Object)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a Object
forall a. Monoid a => a
mempty
single (Single a Object
r)    = a Object -> m (a Object)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a Object
r
single Relation a
_             = UnexpectedAlloyRelation -> m (a Object)
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM UnexpectedAlloyRelation
ExpectedSingleRelationship

double
  :: (MonadThrow m, Monoid (a (Object, Object)))
  => Relation a
  -> m (a (Object, Object))
double :: forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a (Object, Object))) =>
Relation a -> m (a (Object, Object))
double Relation a
EmptyRelation = a (Object, Object) -> m (a (Object, Object))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object)
forall a. Monoid a => a
mempty
double (Double a (Object, Object)
r)    = a (Object, Object) -> m (a (Object, Object))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object)
r
double Relation a
_             = UnexpectedAlloyRelation -> m (a (Object, Object))
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM UnexpectedAlloyRelation
ExpectedDoubleRelationship

triple
  :: (MonadThrow m, Monoid (a (Object, Object, Object)))
  => Relation a
  -> m (a (Object, Object, Object))
triple :: forall (m :: * -> *) (a :: * -> *).
(MonadThrow m, Monoid (a (Object, Object, Object))) =>
Relation a -> m (a (Object, Object, Object))
triple Relation a
EmptyRelation = a (Object, Object, Object) -> m (a (Object, Object, Object))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object, Object)
forall a. Monoid a => a
mempty
triple (Triple a (Object, Object, Object)
r)    = a (Object, Object, Object) -> m (a (Object, Object, Object))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object, Object)
r
triple Relation a
_             = UnexpectedAlloyRelation -> m (a (Object, Object, Object))
forall e a. (HasCallStack, Exception e) => e -> m a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM UnexpectedAlloyRelation
ExpectedTripleRelationship