{-# LANGUAGE OverloadedStrings #-}
{-|
Module      : Language.Alloy.Functions
Description : Type definitions for Call Alloy library
Copyright   : (c) Marcellus Siegburg, 2019
License     : MIT
Maintainer  : marcellus.siegburg@uni-due.de

This module exports basic types in order to work with parsed Alloy instances.
Furthermore, it provides functions to handle these parsed instances.
-}
module Language.Alloy.Functions (
  getSingle, getDouble, getTriple,
  lookupSig,
  objectName,
  relToMap,
  scoped, unscoped,
  ) where

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

import Control.Monad.Except             (MonadError, throwError)
import Data.Function                    (on)
import Data.List                        (groupBy)
import Data.Map                         (Map)
import Data.Set                         (Set)
import Data.String                      (IsString, fromString)

import Language.Alloy.Types (
  AlloyInstance,
  AlloySig,
  Entry (..),
  Object (..),
  Relation (..),
  Signature (..),
  )

{-|
Create a 'Signature' given its scope and name.
-}
scoped :: String -> String -> Signature
scoped :: 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

{-|
Retrieve a set of objects of a given 'AlloySig'.
Successful if the signatures relation is a set (or empty).
-}
getSingle
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set Object)
getSingle :: 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 objects of a given 'AlloySig'.
Successful if the signatures relation is binary (or empty).
-}
getDouble
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set (Object, Object))
getDouble :: 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 objects of a given 'AlloySig'.
Successful if the signatures relation is ternary (or empty).
-}
getTriple
  :: (IsString s, MonadError s m)
  => String
  -> AlloySig
  -> m (Set (Object, Object, Object))
getTriple :: 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

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]

{-|
Transforms a relation into a Mapping.
Is only successful (i.e. returns 'return' if the given transformation function is
able to map the given values injectively.
-}
relToMap
  :: (IsString s, MonadError s m, Ord k, Ord v)
  => (a -> (k, v))
  -> Set a
  -> m (Map k (Set v))
relToMap :: (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

{-|
Retrieve an objects 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"