{-# 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,
  getSingleAs, getDoubleAs, getTripleAs,
  int, object,
  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 :: 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 :: (a2 -> f a) -> Set a2 -> f (Set a)
traverseSet f :: a2 -> f a
f = ([a] -> Set a) -> f [a] -> f (Set a)
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)
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
  :: (IsString s, MonadError s m, Semigroup s)
  => String
  -> Int
  -> m Int
int :: String -> Int -> m Int
int = String -> (Int -> Int) -> String -> Int -> m Int
forall s (m :: * -> *) a.
(IsString s, MonadError s m, Semigroup s) =>
String -> (Int -> a) -> String -> Int -> m a
object "" 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
  :: (IsString s, MonadError s m, Semigroup s)
  => String
  -> (Int -> a)
  -> String
  -> Int
  -> m a
object :: String -> (Int -> a) -> String -> Int -> m a
object s :: String
s f :: Int -> a
f s' :: String
s' g :: Int
g =
  if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
s
  then s -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (s -> m a) -> s -> m a
forall a b. (a -> b) -> a -> b
$ "expected an object of name " s -> s -> s
forall a. Semigroup a => a -> a -> a
<> String -> s
forall a. IsString a => String -> a
fromString String
s
    s -> s -> s
forall a. Semigroup a => a -> a -> a
<> " but got an object of name "
    s -> s -> s
forall a. Semigroup a => a -> a -> a
<> String -> s
forall a. IsString a => String -> a
fromString String
s' s -> s -> s
forall a. Semigroup a => a -> a -> a
<> "."
  else 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 :: (String -> Int -> m a) -> Object -> m a
specifyObject f :: String -> Int -> m a
f o :: Object
o = case Object
o of
  NumberObject i :: Int
i -> String -> Int -> m a
f "" Int
i
  Object n :: String
n i :: Int
i -> String -> Int -> m a
f String
n Int
i
  NamedObject g :: String
g -> String -> m a
forall a. HasCallStack => String -> a
error (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ "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]
++ "\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 :: String -> (String -> Int -> m a) -> AlloySig -> m (Set a)
getSingleAs s :: String
s f :: String -> Int -> m a
f inst :: AlloySig
inst = do
  Set Object
set <- String -> AlloySig -> m (Set Object)
forall s (m :: * -> *).
(IsString s, MonadError s m) =>
String -> AlloySig -> m (Set Object)
getSingle 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

{-# 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).
-}
getSingle
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set Object)
getSingle :: String -> AlloySig -> m (Set Object)
getSingle = (Relation Set -> m (Set Object))
-> String -> AlloySig -> m (Set Object)
forall s (m :: * -> *) (a :: * -> *) b.
(IsString s, MonadError s m) =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set Object)
forall s (m :: * -> *) (a :: * -> *).
(IsString s, MonadError s m, Monoid (a Object)) =>
Relation a -> m (a Object)
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 :: String
-> (String -> Int -> m a)
-> (String -> Int -> m b)
-> AlloySig
-> m (Set (a, b))
getDoubleAs s :: String
s f :: String -> Int -> m a
f g :: String -> Int -> m b
g inst :: AlloySig
inst = do
  Set (Object, Object)
set <- String -> AlloySig -> m (Set (Object, Object))
forall s (m :: * -> *).
(IsString s, MonadError s m) =>
String -> AlloySig -> m (Set (Object, Object))
getDouble 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 (x :: Object
x, y :: 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 (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

{-# 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).
-}
getDouble
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set (Object, Object))
getDouble :: String -> AlloySig -> m (Set (Object, Object))
getDouble = (Relation Set -> m (Set (Object, Object)))
-> String -> AlloySig -> m (Set (Object, Object))
forall s (m :: * -> *) (a :: * -> *) b.
(IsString s, MonadError s m) =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set (Object, Object))
forall s (m :: * -> *) (a :: * -> *).
(IsString s, MonadError s m, Monoid (a (Object, Object))) =>
Relation a -> m (a (Object, Object))
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 :: String
-> (String -> Int -> m a)
-> (String -> Int -> m b)
-> (String -> Int -> m c)
-> AlloySig
-> m (Set (a, b, c))
getTripleAs s :: String
s f :: String -> Int -> m a
f g :: String -> Int -> m b
g h :: String -> Int -> m c
h inst :: AlloySig
inst = do
  Set (Object, Object, Object)
set <- String -> AlloySig -> m (Set (Object, Object, Object))
forall s (m :: * -> *).
(IsString s, MonadError s m) =>
String -> AlloySig -> m (Set (Object, Object, Object))
getTriple 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 (x :: Object
x, y :: Object
y, z :: 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 (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 (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

{-# 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).
-}
getTriple
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set (Object, Object, Object))
getTriple :: String -> AlloySig -> m (Set (Object, Object, Object))
getTriple = (Relation Set -> m (Set (Object, Object, Object)))
-> String -> AlloySig -> m (Set (Object, Object, Object))
forall s (m :: * -> *) (a :: * -> *) b.
(IsString s, MonadError s m) =>
(Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel Relation Set -> m (Set (Object, Object, Object))
forall s (m :: * -> *) (a :: * -> *).
(IsString s, MonadError s m,
 Monoid (a (Object, Object, Object))) =>
Relation a -> m (a (Object, Object, Object))
triple

{-|
Transforms a relation into a Mapping.
-}
binaryToMap :: (Ord k, Ord v) => Set (k, v) -> Map k (Set v)
binaryToMap :: Set (k, v) -> Map k (Set v)
binaryToMap bin :: Set (k, v)
bin = [(k, Set v)] -> Map k (Set v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  [((k, v) -> k
forall a b. (a, b) -> a
fst ([(k, v)] -> (k, v)
forall a. [a] -> a
head [(k, v)]
gs), [v] -> Set v
forall a. Ord a => [a] -> Set a
S.fromList ([v] -> Set v) -> [v] -> Set v
forall a b. (a -> b) -> a -> b
$ (k, v) -> v
forall a b. (a, b) -> b
snd ((k, v) -> v) -> [(k, v)] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
gs)
  | [(k, v)]
gs <- ((k, v) -> (k, v) -> Bool) -> [(k, v)] -> [[(k, v)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (k -> k -> Bool
forall a. Eq a => a -> a -> Bool
(==) (k -> k -> Bool) -> ((k, v) -> k) -> (k, v) -> (k, v) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (k, v) -> k
forall a b. (a, b) -> a
fst) ([(k, v)] -> [[(k, v)]]) -> [(k, v)] -> [[(k, v)]]
forall a b. (a -> b) -> a -> b
$ Set (k, v) -> [(k, v)]
forall a. Set a -> [a]
S.toList Set (k, v)
bin]

{-# DEPRECATED relToMap "use binaryToMap instead" #-}
relToMap
  :: (IsString s, MonadError s m, Ord k, Ord v)
  => (a -> (k, v))
  -> Set a
  -> m (Map k (Set v))
relToMap :: (a -> (k, v)) -> Set a -> m (Map k (Set v))
relToMap f :: a -> (k, v)
f rel :: Set a
rel
  | Set (k, v) -> Int
forall a. Set a -> Int
S.size Set (k, v)
map' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
rel' = Map k (Set v) -> m (Map k (Set v))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map k (Set v) -> m (Map k (Set v)))
-> Map k (Set v) -> m (Map k (Set v))
forall a b. (a -> b) -> a -> b
$ Set (k, v) -> Map k (Set v)
forall k v. (Ord k, Ord v) => Set (k, v) -> Map k (Set v)
binaryToMap Set (k, v)
map'
  | Bool
otherwise                  =
    s -> m (Map k (Set v))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "relToMap: The performed transformation is not injective."
  where
    rel' :: [a]
rel' = Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
rel
    map' :: Set (k, v)
map' = [(k, v)] -> Set (k, v)
forall a. Ord a => [a] -> Set a
S.fromList ([(k, v)] -> Set (k, v)) -> [(k, v)] -> Set (k, v)
forall a b. (a -> b) -> a -> b
$ (a -> (k, v)) -> [a] -> [(k, v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> (k, v)
f [a]
rel'

lookupRel
  :: (IsString s, MonadError s m)
  => (Relation a -> m b)
  -> String
  -> Entry Map a
  -> m b
lookupRel :: (Relation a -> m b) -> String -> Entry Map a -> m b
lookupRel kind :: Relation a -> m b
kind rel :: String
rel e :: 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
  Nothing -> s -> m b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (s -> m b) -> s -> m b
forall a b. (a -> b) -> a -> b
$ String -> s
forall a. IsString a => String -> a
fromString (String -> s) -> String -> s
forall a b. (a -> b) -> a -> b
$ "relation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. IsString a => String -> a
fromString String
rel
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is missing in the Alloy instance"
  Just r :: Relation a
r  -> Relation a -> m b
kind Relation a
r

{-|
Lookup a signature within a given Alloy instance.
-}
lookupSig
  :: (IsString s, MonadError s m)
  => Signature
  -> AlloyInstance
  -> m AlloySig
lookupSig :: Signature -> AlloyInstance -> m AlloySig
lookupSig s :: Signature
s insta :: 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
  Nothing -> s -> m AlloySig
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (s -> m AlloySig) -> s -> m AlloySig
forall a b. (a -> b) -> a -> b
$ String -> s
forall a. IsString a => String -> a
fromString (String -> s) -> String -> s
forall a b. (a -> b) -> a -> b
$ String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/") (Signature -> Maybe String
scope Signature
s) String -> String -> String
forall a. [a] -> [a] -> [a]
++ Signature -> String
sigName Signature
s
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is missing in the Alloy instance"
  Just e :: AlloySig
e   -> AlloySig -> m AlloySig
forall (m :: * -> *) a. Monad m => a -> m a
return AlloySig
e

{-# DEPRECATED objectName "use the typed versions of get... e.g. getSingleAs instead of getSingle" #-}
{-|
Retrieve an object's name.
-}
objectName :: Object -> String
objectName :: Object -> String
objectName o :: Object
o = case Object
o of
  Object s :: String
s n :: Int
n     -> String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ '$' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n
  NumberObject n :: Int
n -> Int -> String
forall a. Show a => a -> String
show Int
n
  NamedObject n :: String
n  -> String
n

single
  :: (IsString s, MonadError s m, Monoid (a Object))
  => Relation a
  -> m (a Object)
single :: Relation a -> m (a Object)
single EmptyRelation = a Object -> m (a Object)
forall (m :: * -> *) a. Monad m => a -> m a
return a Object
forall a. Monoid a => a
mempty
single (Single r :: a Object
r)    = a Object -> m (a Object)
forall (m :: * -> *) a. Monad m => a -> m a
return a Object
r
single _             = s -> m (a Object)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "Relation is (unexpectedly) a mapping"

double
  :: (IsString s, MonadError s m, Monoid (a (Object, Object)))
  => Relation a
  -> m (a (Object, Object))
double :: Relation a -> m (a (Object, Object))
double EmptyRelation = a (Object, Object) -> m (a (Object, Object))
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object)
forall a. Monoid a => a
mempty
double (Double r :: a (Object, Object)
r)    = a (Object, Object) -> m (a (Object, Object))
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object)
r
double _             = s -> m (a (Object, Object))
forall e (m :: * -> *) a. MonadError e m => e -> m a
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 :: Relation a -> m (a (Object, Object, Object))
triple EmptyRelation = a (Object, Object, Object) -> m (a (Object, Object, Object))
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object, Object)
forall a. Monoid a => a
mempty
triple (Triple r :: a (Object, Object, Object)
r)    = a (Object, Object, Object) -> m (a (Object, Object, Object))
forall (m :: * -> *) a. Monad m => a -> m a
return a (Object, Object, Object)
r
triple _             = s -> m (a (Object, Object, Object))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "Relation is not a ternary mapping"