{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-|
This modules performs a Alloy code generation based on CD2Alloy
in order to generate object diagrams
based on (at least) one given class diagram using Alloy.

The whole transformation is based on the following paper
<https://git.rwth-aachen.de/monticore/publications-additional-material/blob/master/cd2alloy/CD2AlloyTranslationTR.pdf>
although a newer version of this document exists
<https://www.se-rwth.de/publications/CD2Alloy-A-Translation-of-Class-Diagrams-to-Alloy.pdf>

Throughout this module there are references to figures of the former paper,
indicating which part of the original work
the previous value definition is representing.

Also to increase readability, some identifiers, predicates, etc.
have been renamed opposed to the original work, these are:

@
Original: umlp2alloy ––– Here: cd2alloy
Original: FName ––– Here: FieldName
Original: fName ––– Here: fieldName
Original: Obj ––– Here: Object
Original: ObjUAttrib ––– Here: ObjectUpperAttribute
Original: ObjLAttrib ––– Here: ObjectLowerAttribute
Original: ObjLUAttrib ––– Here: ObjectLowerUpperAttribute
@

Furthermore refactorings have been made which inline Alloy functions, these are

 * @...CompFieldNamesCD...@
 * @...CompositesCD...@
 * @...FieldNamesCD...@
 * @...SubsCD...@

also the following Alloy predicates, have been inlined

 * @ObjectFieldNames@
 * @ObjectLowerUpperAttribute@
 * @ObjectLowerAttribute@
 * @ObjectLowerUpper@
 * @ObjectLower@
 * @ObjectUpper@
 * @Composition@
-}
module Modelling.CdOd.CD2Alloy.Transform (
  ExtendsAnd (..),
  LinguisticReuse (..),
  Parts {- only for legacy-apps: -} (..),
  combineParts,
  createRunCommand,
  mergeParts,
  overlappingLinksPredicates,
  transform,
  ) where

import qualified Data.List.NonEmpty.Extra         as NE (nubOrd, singleton)

import Modelling.CdOd.Types (
  Cd,
  ClassDiagram (..),
  LimitedLinking (..),
  ObjectConfig (..),
  ObjectProperties (..),
  Relationship (..),
  relationshipName,
  )

import Data.Bifunctor                   (first)
import Data.Foldable                    (Foldable (toList), find)
import Data.Function                    ((&))
import Data.List                        ((\\), delete, intercalate, union)
import Data.List.NonEmpty               (NonEmpty ((:|)))
import Data.List.Extra                  (nubOrd)
import Data.Maybe (
  catMaybes,
  fromMaybe,
  isJust,
  mapMaybe,
  )
import Data.String.Interpolate          (__i, i, iii)
import Data.Tuple.Extra                 ((&&&), dupe, uncurry3)

{-|
Parts belonging to the CD2Alloy Alloy program.
-}
data Parts = Parts {
  Parts -> String
part1 :: !String,
  Parts -> String
part2 :: !String,
  Parts -> String
part3 :: !String
  }

{-|
To what degree, high-level Allow language features should be used
in order to express relationships directly.

Expressiveness is increased when relying less on Alloy language features.
Conciseness is increased when relying more on Alloy language features.
-}
data LinguisticReuse
  = None
  -- ^ not at all
  | ExtendsAnd !ExtendsAnd
  -- ^ use extends for inheritance
  deriving Int -> LinguisticReuse -> ShowS
[LinguisticReuse] -> ShowS
LinguisticReuse -> String
(Int -> LinguisticReuse -> ShowS)
-> (LinguisticReuse -> String)
-> ([LinguisticReuse] -> ShowS)
-> Show LinguisticReuse
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LinguisticReuse -> ShowS
showsPrec :: Int -> LinguisticReuse -> ShowS
$cshow :: LinguisticReuse -> String
show :: LinguisticReuse -> String
$cshowList :: [LinguisticReuse] -> ShowS
showList :: [LinguisticReuse] -> ShowS
Show

{-|
What further to reuse than extends
-}
data ExtendsAnd
  = NothingMore
  -- ^ i.e. only extends
  | FieldPlacement
  -- ^ local field definition
  deriving Int -> ExtendsAnd -> ShowS
[ExtendsAnd] -> ShowS
ExtendsAnd -> String
(Int -> ExtendsAnd -> ShowS)
-> (ExtendsAnd -> String)
-> ([ExtendsAnd] -> ShowS)
-> Show ExtendsAnd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExtendsAnd -> ShowS
showsPrec :: Int -> ExtendsAnd -> ShowS
$cshow :: ExtendsAnd -> String
show :: ExtendsAnd -> String
$cshowList :: [ExtendsAnd] -> ShowS
showList :: [ExtendsAnd] -> ShowS
Show

{-|
Generates Alloy code to generate object diagrams for a given class diagram.
The given class diagram must be valid otherwise the code generation
might not terminate.

The resulting code is split into parts which allows for recombination
with the generated Alloy code for other (similar) class diagrams.

(See 'mergeParts', 'combineParts' and 'createRunCommand')
-}
transform
  :: LinguisticReuse
  -- ^ the degree of linguistic reuse to apply during the translation
  -> Cd
  -- ^ the class diagram for which to generate the code
  -> Maybe [String]
  -- ^ all relationship names to consider
  -- (possibly across multiple class diagrams;
  -- if not provided, they will be taken from the provided class diagram)
  -> [String]
  -- ^ the list of abstract class names
  -> ObjectConfig
  -- ^ size constraints on the object diagrams
  -> ObjectProperties
  -- ^ structural constraints for the object diagrams
  -> String
  -- ^ an identifier for the class diagram
  -> String
  -- ^ a time stamp
  -> Parts
transform :: LinguisticReuse
-> Cd
-> Maybe [String]
-> [String]
-> ObjectConfig
-> ObjectProperties
-> String
-> String
-> Parts
transform
  LinguisticReuse
linguisticReuse
  ClassDiagram {[String]
classNames :: [String]
classNames :: forall className relationshipName.
ClassDiagram className relationshipName -> [className]
classNames, [Relationship String String]
relationships :: [Relationship String String]
relationships :: forall className relationshipName.
ClassDiagram className relationshipName
-> [Relationship className relationshipName]
relationships}
  Maybe [String]
maybeAllRelationshipNames
  [String]
abstractClassNames
  ObjectConfig
objectConfig
  ObjectProperties {Bool
Maybe Bool
Rational
anonymousObjectProportion :: Rational
completelyInhabited :: Maybe Bool
hasLimitedIsolatedObjects :: Bool
hasSelfLoops :: Maybe Bool
usesEveryRelationshipName :: Maybe Bool
anonymousObjectProportion :: ObjectProperties -> Rational
completelyInhabited :: ObjectProperties -> Maybe Bool
hasLimitedIsolatedObjects :: ObjectProperties -> Bool
hasSelfLoops :: ObjectProperties -> Maybe Bool
usesEveryRelationshipName :: ObjectProperties -> Maybe Bool
..}
  String
index
  String
time =
  Parts { String
part1 :: String
part1 :: String
part1, String
part2 :: String
part2 :: String
part2, String
part3 :: String
part3 :: String
part3 }
  where
    allRelationshipNames :: [String]
allRelationshipNames = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe
      ((Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Relationship String String -> Maybe String
forall c r. Relationship c r -> Maybe r
relationshipName [Relationship String String]
relationships)
      Maybe [String]
maybeAllRelationshipNames
    part1 :: String
    part1 :: String
part1 = [i|
// Alloy Model for CD#{index}
// Produced by Haskell reimplementation of Eclipse plugin transformation
// Generated: #{time}

module cd2alloy/CD#{index}Module

///////////////////////////////////////////////////
// Generic Head of CD Model - adapted/simplified;
// and now specialized for a fixed FieldName set originally appearing further below
///////////////////////////////////////////////////

#{objectDefinition}
#{objectsFact}
#{sizeConstraints}
#{loops}
#{inhabitance}
#{relationshipNameAppearance}
///////////////////////////////////////////////////
// Structures potentially common to multiple CDs
///////////////////////////////////////////////////
|]
    objectDefinition :: String
objectDefinition = case LinguisticReuse
linguisticReuse of
      ExtendsAnd ExtendsAnd
FieldPlacement -> String
""
      LinguisticReuse
_ -> [__i|
        //Parent of all classes relating fields and values
        abstract sig Object {
        #{fields}
        }
        |]
    fields :: String
fields = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
",\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
      (\String
fieldName -> [i|  #{fieldName} : set Object|])
      [String]
allRelationshipNames
    objectsFact :: String
    objectsFact :: String
objectsFact
      | Bool
hasLimitedIsolatedObjects
      = String
limitIsolatedObjects
      | Bool
otherwise
      = String
noEmptyInstances
    limitIsolatedObjects :: String
limitIsolatedObjects
      | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
allRelationshipNames = [i|
fact LimitIsolatedObjects {
  #{false}
}
|]
      | Bool
otherwise = [i|
fact LimitIsolatedObjects {
 let get = #{alloySetOf allRelationshipNames} |
  \##{objectsParens} > mul[2, \#{o : #{objects} | no o.get and no get.o}]
}
|]
    noEmptyInstances :: String
noEmptyInstances = [i|
fact NonEmptyInstancesOnly {
  some #{objects}
}
|]
    (String
objects, String
objectsParens)
      | ExtendsAnd ExtendsAnd
FieldPlacement <- LinguisticReuse
linguisticReuse
      = [String] -> String
alloySetOf ([String] -> String)
-> ([String] -> String) -> [String] -> (String, String)
forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
&&& [String] -> String
alloySetOfParens ([String] -> (String, String)) -> [String] -> (String, String)
forall a b. (a -> b) -> a -> b
$ [String]
complete
      | Bool
otherwise = String -> (String, String)
forall a. a -> (a, a)
dupe String
"Object"
    complete :: [String]
complete = case LinguisticReuse
linguisticReuse of
      LinguisticReuse
None -> [String]
nonAbstractClassNames
      ExtendsAnd {} -> [String]
nonAbstractSuperClassNames
    nonAbstractSuperClassNames :: [String]
nonAbstractSuperClassNames = [String]
nonAbstractClassNames [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
subClasses
    subClasses :: [String]
subClasses = ((Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` [Relationship String String]
relationships) ((Relationship String String -> Maybe String) -> [String])
-> (Relationship String String -> Maybe String) -> [String]
forall a b. (a -> b) -> a -> b
$ \case
        Inheritance {String
subClass :: String
superClass :: String
subClass :: forall className relationshipName.
Relationship className relationshipName -> className
superClass :: forall className relationshipName.
Relationship className relationshipName -> className
..} -> String -> Maybe String
forall a. a -> Maybe a
Just String
subClass
        Relationship String String
_ -> Maybe String
forall a. Maybe a
Nothing
    withJusts :: ([a] -> String) -> [Maybe a] -> String
withJusts [a] -> String
f [Maybe a]
xs
      | (Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe a -> Bool
forall a. Maybe a -> Bool
isJust [Maybe a]
xs = [a] -> String
f ([a] -> String) -> [a] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes [Maybe a]
xs
      | Bool
otherwise     = String
""
    sizeConstraints :: String
sizeConstraints = ([String] -> String) -> [Maybe String] -> String
forall {a}. ([a] -> String) -> [Maybe a] -> String
withJusts (\[String]
ps -> [i|
fact SizeConstraints {
#{unlines ps}
}
|]) [
      ([i|  \##{objectsParens} >= |] String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show
        (Int -> String) -> Maybe Int -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> (Int, Int) -> Maybe Int
forall {b} {b}. Ord b => b -> (b, b) -> Maybe b
maybeLower Int
1 (ObjectConfig -> (Int, Int)
objectLimits ObjectConfig
objectConfig),
      String
"  " String -> (String -> Maybe String) -> Maybe String
forall a b. a -> (a -> b) -> b
& (Maybe Int -> Maybe Int -> String -> Maybe String)
-> (Maybe Int, Maybe Int) -> String -> Maybe String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Int -> Maybe Int -> String -> Maybe String
count ((Int -> Maybe Int) -> (Int, Maybe Int) -> (Maybe Int, Maybe Int)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int -> Int -> Maybe Int
forall {a}. Ord a => a -> a -> Maybe a
maybeLow Int
0) ((Int, Maybe Int) -> (Maybe Int, Maybe Int))
-> (Int, Maybe Int) -> (Maybe Int, Maybe Int)
forall a b. (a -> b) -> a -> b
$ ObjectConfig -> (Int, Maybe Int)
linkLimits ObjectConfig
objectConfig),
      (Maybe Int -> Maybe Int -> Maybe String)
-> (Maybe Int, Maybe Int) -> Maybe String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Int -> Maybe Int -> Maybe String
linksPerObjects
        ((Maybe Int, Maybe Int) -> Maybe String)
-> (Maybe Int, Maybe Int) -> Maybe String
forall a b. (a -> b) -> a -> b
$ (Int -> Maybe Int) -> (Int, Maybe Int) -> (Maybe Int, Maybe Int)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int -> Int -> Maybe Int
forall {a}. Ord a => a -> a -> Maybe a
maybeLow Int
0)
        ((Int, Maybe Int) -> (Maybe Int, Maybe Int))
-> (Int, Maybe Int) -> (Maybe Int, Maybe Int)
forall a b. (a -> b) -> a -> b
$ ObjectConfig -> (Int, Maybe Int)
linksPerObjectLimits ObjectConfig
objectConfig
      ]
    count :: Maybe Int -> Maybe Int -> String -> Maybe String
count = Maybe String -> Maybe Int -> Maybe Int -> String -> Maybe String
alloyCompare (Maybe String -> Maybe Int -> Maybe Int -> String -> Maybe String)
-> Maybe String -> Maybe Int -> Maybe Int -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe String
alloyPlus ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char
'#'Char -> ShowS
forall a. a -> [a] -> [a]
:) [String]
allRelationshipNames
    linksPerObjects :: Maybe Int -> Maybe Int -> Maybe String
    linksPerObjects :: Maybe Int -> Maybe Int -> Maybe String
linksPerObjects Maybe Int
maybeMin Maybe Int
maybeMax =
      let maybeLinkCount :: Maybe String
maybeLinkCount = [String] -> Maybe String
alloyPlus ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
            (\String
link -> [i|plus[\#o.#{link}, minus[\##{link}.o, \#(o.#{link} & o)]]|])
            [String]
allRelationshipNames
      in [i|  all o : #{objects} | |] String -> (String -> Maybe String) -> Maybe String
forall a b. a -> (a -> b) -> b
& Maybe String -> Maybe Int -> Maybe Int -> String -> Maybe String
alloyCompare Maybe String
maybeLinkCount Maybe Int
maybeMin Maybe Int
maybeMax
    maybeLower :: b -> (b, b) -> Maybe b
maybeLower b
l = b -> b -> Maybe b
forall {a}. Ord a => a -> a -> Maybe a
maybeLow b
l (b -> Maybe b) -> ((b, b) -> b) -> (b, b) -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b, b) -> b
forall a b. (a, b) -> a
fst
    maybeLow :: a -> a -> Maybe a
maybeLow a
l a
x = if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
l then Maybe a
forall a. Maybe a
Nothing else a -> Maybe a
forall a. a -> Maybe a
Just a
x
    part2 :: String
part2 = [i|
// Classes
#{unlines (classSigs linguisticReuse relationships classNames)}
|] -- Figure 2.1, Rule 1, part 1
    part3 :: String
part3 = [i|
///////////////////////////////////////////////////
// CD#{index}
///////////////////////////////////////////////////

// Properties
#{predicate
  linguisticReuse
  index
  allRelationshipNames
  relationships
  complete
  }
|]
    nonAbstractClassNames :: [String]
nonAbstractClassNames = [String]
classNames [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
abstractClassNames
    nonAbstractObjects :: [String]
nonAbstractObjects = case LinguisticReuse
linguisticReuse of
      LinguisticReuse
None -> [String]
nonAbstractClassNames
      ExtendsAnd {} -> (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
`map` [String]
nonAbstractClassNames) (ShowS -> [String]) -> ShowS -> [String]
forall a b. (a -> b) -> a -> b
$ \String
name ->
        String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" - " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [Relationship String String] -> String -> [String]
directSubclassesOf [Relationship String String]
relationships String
name
    inhabitance :: String
inhabitance = case Maybe Bool
completelyInhabited of
      Maybe Bool
Nothing   -> String
""
      Just Bool
False -> [i|
fact NotCompletelyInhabited {
  #{intercalate " or " $ map ("no " ++) nonAbstractObjects}
}|]
      Just Bool
True -> [i|
fact CompletelyInhabited {
#{unlines $ map ("  some " ++) nonAbstractObjects}
}|]
    relationshipNameAppearance :: String
relationshipNameAppearance = case Maybe Bool
usesEveryRelationshipName of
      Maybe Bool
Nothing -> String
""
      Just Bool
False ->
        let notEvery :: String
notEvery = case [String]
allRelationshipNames of
              [] -> String
false
              [String]
names -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" or " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"no " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
names
        in [i|
fact UsesNotEveryRelationshipName {
  #{notEvery}
}|]
      Just Bool
True -> [i|
fact UsesEveryRelationshipName {
#{unlines $ map ("  some " ++) allRelationshipNames}
}|]
    loops :: String
loops            = case Maybe Bool
hasSelfLoops of
      Maybe Bool
Nothing    -> String
""
      Just Bool
hasLoops
        | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
allRelationshipNames, Bool
hasLoops -> [__i|
          fact SomeSelfLoops {
            #{false}
          }|]
        | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
allRelationshipNames -> String
""
        | Bool
otherwise ->
        if Bool
hasLoops
        then [i|
fact SomeSelfLoops {
  some o : #{objects} | o in o.#{relationshipSet}
}|]
        else [i|
fact NoSelfLoops {
  no o : #{objects} | o in o.#{relationshipSet}
}|]
    relationshipSet :: String
relationshipSet
      | [String
_] <- [String]
allRelationshipNames
      = [String] -> String
alloySetOf [String]
allRelationshipNames
      | Bool
otherwise
      = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
alloySetOf [String]
allRelationshipNames String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

{-|
Generates Alloy code which is a contradiction that can never be satisfied,
i.e. essentially resolves to false.
-}
false :: String
false :: String
false = String
"some none // i.e. false"

{-|
Given a possible counter formula and two limiters this function generates
Alloy code which is to be applied to an Alloy code prefix in order
to possible generate Alloy code that describes the resulting constraint.

(If the result is 'Nothing', nothing needs to be constrained)
-}
alloyCompare
  :: Maybe String
  -- ^ if 'Nothing' this counter formula is assumed to be equal to '0'
  -- (e.g. the case for the result of 'alloyPlus')
  -> Maybe Int
  -- ^ the lower limit
  -> Maybe Int
  -- ^ the upper limit
  -> String
  -- ^ the Alloy code prefix to prepend
  -> Maybe String
alloyCompare :: Maybe String -> Maybe Int -> Maybe Int -> String -> Maybe String
alloyCompare Maybe String
maybeWhat Maybe Int
maybeMin Maybe Int
maybeMax = case Maybe String
maybeWhat of
  Maybe String
Nothing
    | Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
maybeMin Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Maybe String -> String -> Maybe String
forall a b. a -> b -> a
const Maybe String
forall a. Maybe a
Nothing
    | Bool
otherwise -> Maybe String -> String -> Maybe String
forall a b. a -> b -> a
const (Maybe String -> String -> Maybe String)
-> Maybe String -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
false
  Just String
what -> case Maybe Int
maybeMax of
    Maybe Int
Nothing -> case Maybe Int
maybeMin of
      Maybe Int
Nothing -> Maybe String -> String -> Maybe String
forall a b. a -> b -> a
const Maybe String
forall a. Maybe a
Nothing
      Just Int
low -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> ShowS -> String -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{what} >= #{low}|])
    Just Int
up -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> ShowS -> String -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. case Maybe Int
maybeMin of
      Maybe Int
Nothing -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{what} =< #{up}|])
      Just Int
low
        | Int
low Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
up -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{what} = #{up}|])
        | Bool
otherwise ->
          (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|let count = #{what} | count >= #{low} and count =< #{up}|])

{-|
Creates an Alloy run command line taking provided size constraints into account.
-}
createRunCommand
  :: String
  -> Maybe [String]
  -- ^ if provided, object limit will be defined as constraint rather than
  -- by scope (by scope should be preferred, but is not possible for
  -- @ExtendsAnd FieldPlacement@)
  -> Int
  -> ObjectConfig
  -> [Relationship a b]
  -> String
createRunCommand :: forall a b.
String
-> Maybe [String]
-> Int
-> ObjectConfig
-> [Relationship a b]
-> String
createRunCommand
  String
command
  Maybe [String]
maybeNonAbstractClassNames
  Int
numClasses
  ObjectConfig
objectConfig
  [Relationship a b]
relationships
  = [i|
///////////////////////////////////////////////////
// Run commands
///////////////////////////////////////////////////
#{limitObjects}
run { #{command} } for #{maxObjects} #{what} #{intSize} Int
|]
  where
    maxLimit :: Int
maxLimit = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Relationship a b -> Int) -> [Relationship a b] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Relationship a b -> Int
forall a b. Relationship a b -> Int
maximumLimitOf [Relationship a b]
relationships
    maxObjects :: Int
maxObjects = (Int, Int) -> Int
forall a b. (a, b) -> b
snd ((Int, Int) -> Int) -> (Int, Int) -> Int
forall a b. (a -> b) -> a -> b
$ ObjectConfig -> (Int, Int)
objectLimits ObjectConfig
objectConfig
    intSize :: Int
    intSize :: Int
intSize = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Double
intSize'
    intSize' :: Double
    intSize' :: Double
intSize' = Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 (Double -> Double) -> Double -> Double
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxInt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    maxInt :: Int
maxInt = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [
      Int
numClasses Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxObjects,
      Int
maxLimit,
      Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxObjects,
      (ObjectConfig -> (Int, Maybe Int)) -> Int
forall {a}. (ObjectConfig -> (a, Maybe a)) -> a
count ObjectConfig -> (Int, Maybe Int)
linkLimits,
      (ObjectConfig -> (Int, Maybe Int)) -> Int
forall {a}. (ObjectConfig -> (a, Maybe a)) -> a
count ObjectConfig -> (Int, Maybe Int)
linksPerObjectLimits
      ]
    (String
what, String
limitObjects) = case Maybe [String]
maybeNonAbstractClassNames of
      Maybe [String]
Nothing -> (String
"Object,", String
"")
      Just [String]
nonAbstractClassNames -> (
        String
"but",
        [__i|
        fact objectsMaximum {
          \##{alloySetOfParens nonAbstractClassNames} <= #{maxObjects}
        }
        |]
        )
    count :: (ObjectConfig -> (a, Maybe a)) -> a
count ObjectConfig -> (a, Maybe a)
f = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe ((a, Maybe a) -> a
forall a b. (a, b) -> a
fst ((a, Maybe a) -> a) -> (a, Maybe a) -> a
forall a b. (a -> b) -> a -> b
$ ObjectConfig -> (a, Maybe a)
f ObjectConfig
objectConfig) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ (a, Maybe a) -> Maybe a
forall a b. (a, b) -> b
snd (ObjectConfig -> (a, Maybe a)
f ObjectConfig
objectConfig)

maximumLimitOf :: Relationship a b -> Int
maximumLimitOf :: forall a b. Relationship a b -> Int
maximumLimitOf = \case
  Association {b
LimitedLinking a
associationName :: b
associationFrom :: LimitedLinking a
associationTo :: LimitedLinking a
associationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
associationFrom :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
associationTo :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
..} -> LimitedLinking a -> LimitedLinking a -> Int
forall {nodeName} {nodeName}.
LimitedLinking nodeName -> LimitedLinking nodeName -> Int
maximumLimit LimitedLinking a
associationFrom LimitedLinking a
associationTo
  Aggregation {b
LimitedLinking a
aggregationName :: b
aggregationPart :: LimitedLinking a
aggregationWhole :: LimitedLinking a
aggregationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
aggregationPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
aggregationWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
..} -> LimitedLinking a -> LimitedLinking a -> Int
forall {nodeName} {nodeName}.
LimitedLinking nodeName -> LimitedLinking nodeName -> Int
maximumLimit LimitedLinking a
aggregationPart LimitedLinking a
aggregationWhole
  Composition {b
LimitedLinking a
compositionName :: b
compositionPart :: LimitedLinking a
compositionWhole :: LimitedLinking a
compositionName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
compositionPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
compositionWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
..} -> LimitedLinking a -> LimitedLinking a -> Int
forall {nodeName} {nodeName}.
LimitedLinking nodeName -> LimitedLinking nodeName -> Int
maximumLimit LimitedLinking a
compositionPart LimitedLinking a
compositionWhole
  Inheritance {}   -> Int
0
  where
    maximumLimit :: LimitedLinking nodeName -> LimitedLinking nodeName -> Int
maximumLimit LimitedLinking nodeName
l1 LimitedLinking nodeName
l2 = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (LimitedLinking nodeName -> Int
forall {nodeName}. LimitedLinking nodeName -> Int
maximumLinking LimitedLinking nodeName
l1) (LimitedLinking nodeName -> Int
forall {nodeName}. LimitedLinking nodeName -> Int
maximumLinking LimitedLinking nodeName
l2)
    maximumLinking :: LimitedLinking nodeName -> Int
maximumLinking LimitedLinking {limits :: forall nodeName. LimitedLinking nodeName -> (Int, Maybe Int)
limits = (Int
low, Maybe Int
high)} = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
low Maybe Int
high

classSigs
  :: LinguisticReuse
  -> [Relationship String String]
  -> [String]
  -> [String]
classSigs :: LinguisticReuse
-> [Relationship String String] -> [String] -> [String]
classSigs LinguisticReuse
linguisticReuse [Relationship String String]
relationships = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
classSig
  where
    classSig :: String -> String
    classSig :: ShowS
classSig String
name = case LinguisticReuse
linguisticReuse of
      LinguisticReuse
None -> [i|sig #{name} extends Object {}|]
      ExtendsAnd ExtendsAnd
NothingMore ->
        (\String
super -> [i|sig #{name} extends #{super} {}|])
        ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
-> (Relationship String String -> String)
-> Maybe (Relationship String String)
-> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"Object" Relationship String String -> String
forall className relationshipName.
Relationship className relationshipName -> className
superClass
        (Maybe (Relationship String String) -> String)
-> Maybe (Relationship String String) -> String
forall a b. (a -> b) -> a -> b
$ (Relationship String String -> Bool)
-> [Relationship String String]
-> Maybe (Relationship String String)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (String -> Relationship String String -> Bool
forall {a} {relationshipName}.
Eq a =>
a -> Relationship a relationshipName -> Bool
hasSuperClass String
name) [Relationship String String]
relationships
      ExtendsAnd ExtendsAnd
FieldPlacement ->
        (\String
extends -> [__i|
          sig #{name}#{extends} #{fields name}#{spaced $ fieldConstraints name}|]
          )
        ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
-> (Relationship String String -> String)
-> Maybe (Relationship String String)
-> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((String
" extends " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> (Relationship String String -> String)
-> Relationship String String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relationship String String -> String
forall className relationshipName.
Relationship className relationshipName -> className
superClass)
        (Maybe (Relationship String String) -> String)
-> Maybe (Relationship String String) -> String
forall a b. (a -> b) -> a -> b
$ (Relationship String String -> Bool)
-> [Relationship String String]
-> Maybe (Relationship String String)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (String -> Relationship String String -> Bool
forall {a} {relationshipName}.
Eq a =>
a -> Relationship a relationshipName -> Bool
hasSuperClass String
name) [Relationship String String]
relationships
    fromTos :: [(String, LimitedLinking String, LimitedLinking String)]
fromTos = (Relationship String String
 -> Maybe (String, LimitedLinking String, LimitedLinking String))
-> [Relationship String String]
-> [(String, LimitedLinking String, LimitedLinking String)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Relationship String String
-> Maybe (String, LimitedLinking String, LimitedLinking String)
forall a b.
Relationship a b -> Maybe (b, LimitedLinking a, LimitedLinking a)
nameFromTo [Relationship String String]
relationships
    fields :: ShowS
fields String
className = [String] -> String
linesWrappedInOrBraces ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
commaSeparated ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
      [ [iii|#{name} : set #{linking to}|]
      | (String
name, LimitedLinking String
from, LimitedLinking String
to) <- [(String, LimitedLinking String, LimitedLinking String)]
fromTos
      , LimitedLinking String -> String
forall nodeName. LimitedLinking nodeName -> nodeName
linking LimitedLinking String
from String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
className
      ]
    commaSeparated :: [String] -> [String]
commaSeparated (String
x:xs :: [String]
xs@(String
_:[String]
_)) = (String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
",") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
commaSeparated [String]
xs
    commaSeparated [String]
xs = [String]
xs
    spaced :: ShowS
spaced [] = []
    spaced String
xs = Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:String
xs
    fieldConstraints :: ShowS
fieldConstraints String
className = [String] -> String
linesWrappedInBraces ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
      [ ShowS -> (Int, Maybe Int) -> ShowS
nonInheritanceLimits (String -> ShowS
forall a b. a -> b -> a
const String
name) (LimitedLinking String -> (Int, Maybe Int)
forall nodeName. LimitedLinking nodeName -> (Int, Maybe Int)
limits LimitedLinking String
to) String
""
      | (String
name, LimitedLinking String
from, LimitedLinking String
to) <- [(String, LimitedLinking String, LimitedLinking String)]
fromTos
      , LimitedLinking String -> String
forall nodeName. LimitedLinking nodeName -> nodeName
linking LimitedLinking String
from String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
className
      ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
      [ ShowS -> (Int, Maybe Int) -> ShowS
nonInheritanceLimits (String -> ShowS
forall a b. a -> b -> a
const [iii|@#{name}.this|]) (LimitedLinking String -> (Int, Maybe Int)
forall nodeName. LimitedLinking nodeName -> (Int, Maybe Int)
limits LimitedLinking String
from) String
""
      | (String
name, LimitedLinking String
from, LimitedLinking String
to) <- [(String, LimitedLinking String, LimitedLinking String)]
fromTos
      , LimitedLinking String -> String
forall nodeName. LimitedLinking nodeName -> nodeName
linking LimitedLinking String
to String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
className
      ]
    hasSuperClass :: a -> Relationship a relationshipName -> Bool
hasSuperClass a
name = \case
      Inheritance {a
subClass :: forall className relationshipName.
Relationship className relationshipName -> className
superClass :: forall className relationshipName.
Relationship className relationshipName -> className
subClass :: a
superClass :: a
..} | a
subClass a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
name -> Bool
True
      Relationship a relationshipName
_ -> Bool
False

{-| Puts curly braces arround the given lines which are indented,
puts a pair of empty curly braces if no lines are given, and
puts surrounding braces on that single line if just one line is given.
-}
linesWrappedInOrBraces :: [String] -> String
linesWrappedInOrBraces :: [String] -> String
linesWrappedInOrBraces [] = String
"{}"
linesWrappedInOrBraces [String]
xs = [String] -> String
linesWrappedInBraces [String]
xs

{-| Puts curly braces arround the given lines which are indented,
returns an empty string if no lines are given, and
puts surrounding braces on that single line if just one line is given.
-}
linesWrappedInBraces :: [String] -> String
linesWrappedInBraces :: [String] -> String
linesWrappedInBraces [] = String
""
linesWrappedInBraces [String
x] = [iii|{#{x}}|]
linesWrappedInBraces [String]
xs = [i|{
  #{intercalate "\n  " xs}
}|]

{-|
Retrieve the set of direct subclasses of the given class.
-}
directSubclassesOf
  :: [Relationship String String]
  -- ^ all relationships of the class diagram
  -> String
  -- ^ the name of the class to consider
  -> [String]
directSubclassesOf :: [Relationship String String] -> String -> [String]
directSubclassesOf [Relationship String String]
relationships String
name = ((Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` [Relationship String String]
relationships) ((Relationship String String -> Maybe String) -> [String])
-> (Relationship String String -> Maybe String) -> [String]
forall a b. (a -> b) -> a -> b
$ \case
  Inheritance {superClass :: forall className relationshipName.
Relationship className relationshipName -> className
superClass = String
s, String
subClass :: forall className relationshipName.
Relationship className relationshipName -> className
subClass :: String
..} | String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s -> String -> Maybe String
forall a. a -> Maybe a
Just String
subClass
  Relationship String String
_ -> Maybe String
forall a. Maybe a
Nothing

-- Figure 2.1, Rule 1, part 2, alternative implementation
-- (SubsCD - inlined)
{-|
Retrieve the set of all subclasses of the given class.
-}
allSubclassesOf
  :: [Relationship String String]
  -- ^ all relationships of the class diagram
  -> String
  -- ^ the name of the class to consider
  -> NonEmpty String
allSubclassesOf :: [Relationship String String] -> String -> NonEmpty String
allSubclassesOf [Relationship String String]
relationships String
name =
  NonEmpty String -> NonEmpty String
forall a. Ord a => NonEmpty a -> NonEmpty a
NE.nubOrd
  (NonEmpty String -> NonEmpty String)
-> NonEmpty String -> NonEmpty String
forall a b. (a -> b) -> a -> b
$ String
name String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| (String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NonEmpty String -> [String])
-> (String -> NonEmpty String) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Relationship String String] -> String -> NonEmpty String
allSubclassesOf [Relationship String String]
relationships) [String]
subclasses
  where
    subclasses :: [String]
subclasses = [Relationship String String] -> String -> [String]
directSubclassesOf [Relationship String String]
relationships String
name

{-|
The predicate constraining the specific class diagram.
-}
predicate
  :: LinguisticReuse
  -- ^ the degree of linguistic reuse to apply during the translation
  -> String
  -- ^ an identifier for the class diagram
  -> [String]
  -- ^ all relationship names to consider
  -- (possibly across multiple class diagrams)
  -> [Relationship String String]
  -- ^ all relationships belonging to the class diagram
  -> [String]
  -- ^ a complete set of class names that contains all possible objects
  -> String
predicate :: LinguisticReuse
-> String
-> [String]
-> [Relationship String String]
-> [String]
-> String
predicate
  LinguisticReuse
linguisticReuse
  String
index
  [String]
allRelationshipNames
  [Relationship String String]
relationships
  [String]
complete
  = [i|
pred cd#{index} {
#{objects}
  // Contents
#{unlines nonExistingRelationships}
  // Associations
#{nonInheritanceConstraints linguisticReuse relationships}
  // Compositions
#{compositions}
}
|]
  where
    objects :: String
objects
      | ExtendsAnd ExtendsAnd
FieldPlacement <- LinguisticReuse
linguisticReuse = String
""
      | Bool
otherwise = [i|
  Object = #{alloySetOf complete}
|]
      -- Figure 2.2, Rule 5
    objectSet :: String
objectSet
      | ExtendsAnd ExtendsAnd
FieldPlacement <- LinguisticReuse
linguisticReuse = [String] -> String
alloySetOf [String]
complete
      | Bool
otherwise = String
"Object"
    nonExistingRelationships :: [String]
nonExistingRelationships = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  no " String -> ShowS
forall a. [a] -> [a] -> [a]
++)
      ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [String]
allRelationshipNames [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ (Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Relationship String String -> Maybe String
forall c r. Relationship c r -> Maybe r
relationshipName [Relationship String String]
relationships
    compositions :: String
compositions = String -> [String] -> String
compositeConstraint
      String
objectSet
      ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ((Relationship String String -> Maybe String)
 -> [Relationship String String] -> [String])
-> [Relationship String String]
-> (Relationship String String -> Maybe String)
-> [String]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Relationship String String]
relationships
      ((Relationship String String -> Maybe String) -> [String])
-> (Relationship String String -> Maybe String) -> [String]
forall a b. (a -> b) -> a -> b
$ \case
        Composition {String
compositionName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
compositionName :: String
compositionName} -> String -> Maybe String
forall a. a -> Maybe a
Just String
compositionName
        Relationship String String
_ -> Maybe String
forall a. Maybe a
Nothing
      -- Figure 2.2, Rule 4, corrected, simplified

{-|
Generates a predicate for each non-inheritance relationship - relationship name
combination (except its actual)
this can be used to prevent or force overlapping links
(i.e. that could match to two relationships)
in order to steer difficulty.

The function returns a list of both, the predicates names
as well as the predicates themselves.
-}
overlappingLinksPredicates
  :: [Relationship String String]
  -> [(String, String)]
overlappingLinksPredicates :: [Relationship String String] -> [(String, String)]
overlappingLinksPredicates [Relationship String String]
relationships =
  [[(String, String)]] -> [(String, String)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, String)]] -> [(String, String)])
-> [[(String, String)]] -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ (Relationship String String -> Maybe [(String, String)])
-> [Relationship String String] -> [[(String, String)]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Relationship String String -> Maybe [(String, String)]
allPredicatesFor [Relationship String String]
relationships
  where
    relationshipNames :: [String]
relationshipNames = (Relationship String String -> Maybe String)
-> [Relationship String String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Relationship String String -> Maybe String
forall c r. Relationship c r -> Maybe r
relationshipName [Relationship String String]
relationships
    allPredicatesFor :: Relationship String String -> Maybe [(String, String)]
allPredicatesFor = \case
      Inheritance {} -> Maybe [(String, String)]
forall a. Maybe a
Nothing
      Aggregation {String
aggregationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
aggregationName :: String
aggregationName, LimitedLinking String
aggregationPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
aggregationWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
aggregationPart :: LimitedLinking String
aggregationWhole :: LimitedLinking String
..} -> [(String, String)] -> Maybe [(String, String)]
forall a. a -> Maybe a
Just ([(String, String)] -> Maybe [(String, String)])
-> [(String, String)] -> Maybe [(String, String)]
forall a b. (a -> b) -> a -> b
$ String
-> (String -> Relationship String String) -> [(String, String)]
predicatesFor
        String
aggregationName
        ((String -> Relationship String String) -> [(String, String)])
-> (String -> Relationship String String) -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ \String
name -> Aggregation {aggregationName :: String
aggregationName = String
name, LimitedLinking String
aggregationPart :: LimitedLinking String
aggregationWhole :: LimitedLinking String
aggregationPart :: LimitedLinking String
aggregationWhole :: LimitedLinking String
..}
      Association {String
associationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
associationName :: String
associationName, LimitedLinking String
associationFrom :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
associationTo :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
associationFrom :: LimitedLinking String
associationTo :: LimitedLinking String
..} -> [(String, String)] -> Maybe [(String, String)]
forall a. a -> Maybe a
Just ([(String, String)] -> Maybe [(String, String)])
-> [(String, String)] -> Maybe [(String, String)]
forall a b. (a -> b) -> a -> b
$ String
-> (String -> Relationship String String) -> [(String, String)]
predicatesFor
        String
associationName
        ((String -> Relationship String String) -> [(String, String)])
-> (String -> Relationship String String) -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ \String
name -> Association {associationName :: String
associationName = String
name, LimitedLinking String
associationFrom :: LimitedLinking String
associationTo :: LimitedLinking String
associationFrom :: LimitedLinking String
associationTo :: LimitedLinking String
..}
      Composition {String
compositionName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
compositionName :: String
compositionName, LimitedLinking String
compositionPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
compositionWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
compositionPart :: LimitedLinking String
compositionWhole :: LimitedLinking String
..} -> [(String, String)] -> Maybe [(String, String)]
forall a. a -> Maybe a
Just ([(String, String)] -> Maybe [(String, String)])
-> [(String, String)] -> Maybe [(String, String)]
forall a b. (a -> b) -> a -> b
$ String
-> (String -> Relationship String String) -> [(String, String)]
predicatesFor
        String
compositionName
        ((String -> Relationship String String) -> [(String, String)])
-> (String -> Relationship String String) -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ \String
name -> Composition {compositionName :: String
compositionName = String
name, LimitedLinking String
compositionPart :: LimitedLinking String
compositionWhole :: LimitedLinking String
compositionPart :: LimitedLinking String
compositionWhole :: LimitedLinking String
..}
    predicatesFor :: String
-> (String -> Relationship String String) -> [(String, String)]
predicatesFor String
originalName String -> Relationship String String
relationshipNamed = (String -> (String, String)) -> [String] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map
      (\String
usedAs -> String -> Relationship String String -> (String, String)
relationshipPredicate
        (String
"only_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
originalName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_as_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
usedAs)
        (Relationship String String -> (String, String))
-> Relationship String String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String -> Relationship String String
relationshipNamed String
usedAs)
      ([String] -> [(String, String)]) -> [String] -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. Eq a => a -> [a] -> [a]
delete String
originalName [String]
relationshipNames
    relationshipPredicate
      :: String
      -> Relationship String String
      -> (String, String)
    relationshipPredicate :: String -> Relationship String String -> (String, String)
relationshipPredicate String
predicateName Relationship String String
relationship = (String
predicateName, [__i|
      pred #{predicateName} {
      #{nonInheritanceConstraints (ExtendsAnd NothingMore) [relationship]}}
      |])


nonInheritanceConstraints
  :: LinguisticReuse
  -> [Relationship String String]
  -> String
nonInheritanceConstraints :: LinguisticReuse -> [Relationship String String] -> String
nonInheritanceConstraints LinguisticReuse
linguisticReuse [Relationship String String]
relationships
  | ExtendsAnd ExtendsAnd
FieldPlacement <- LinguisticReuse
linguisticReuse
  = String
""
  | Bool
otherwise
  = [__i|
    #{unlines objectAttributes}
    |]
  where
    objectAttributes :: [String]
objectAttributes = (Relationship String String -> [String])
-> [Relationship String String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
      ([String]
-> ((String, LimitedLinking String, LimitedLinking String)
    -> [String])
-> Maybe (String, LimitedLinking String, LimitedLinking String)
-> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((String
 -> LimitedLinking String -> LimitedLinking String -> [String])
-> (String, LimitedLinking String, LimitedLinking String)
-> [String]
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 String
-> LimitedLinking String -> LimitedLinking String -> [String]
associationFromTo) (Maybe (String, LimitedLinking String, LimitedLinking String)
 -> [String])
-> (Relationship String String
    -> Maybe (String, LimitedLinking String, LimitedLinking String))
-> Relationship String String
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relationship String String
-> Maybe (String, LimitedLinking String, LimitedLinking String)
forall a b.
Relationship a b -> Maybe (b, LimitedLinking a, LimitedLinking a)
nameFromTo)
      [Relationship String String]
relationships
    associationFromTo :: String
-> LimitedLinking String -> LimitedLinking String -> [String]
associationFromTo String
name LimitedLinking String
from LimitedLinking String
to = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [
      [String] -> String -> [String] -> String
makeNonInheritance (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty String
subsFrom) String
name (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty String
subsTo),
      ShowS -> NonEmpty String -> (Int, Maybe Int) -> String
makeNonInheritanceLimits (String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char
'.' Char -> ShowS
forall a. a -> [a] -> [a]
: String
name)) NonEmpty String
subsFrom (LimitedLinking String -> (Int, Maybe Int)
forall nodeName. LimitedLinking nodeName -> (Int, Maybe Int)
limits LimitedLinking String
to),
      ShowS -> NonEmpty String -> (Int, Maybe Int) -> String
makeNonInheritanceLimits ((String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'.' Char -> ShowS
forall a. a -> [a] -> [a]
:)) NonEmpty String
subsTo (LimitedLinking String -> (Int, Maybe Int)
forall nodeName. LimitedLinking nodeName -> (Int, Maybe Int)
limits LimitedLinking String
from)
      ]
      where
        subsCd :: String -> NonEmpty String
subsCd = case LinguisticReuse
linguisticReuse of
          LinguisticReuse
None -> [Relationship String String] -> String -> NonEmpty String
allSubclassesOf [Relationship String String]
relationships
          ExtendsAnd {} -> String -> NonEmpty String
forall a. a -> NonEmpty a
NE.singleton
        subsFrom :: NonEmpty String
subsFrom = String -> NonEmpty String
subsCd (String -> NonEmpty String) -> String -> NonEmpty String
forall a b. (a -> b) -> a -> b
$ LimitedLinking String -> String
forall nodeName. LimitedLinking nodeName -> nodeName
linking LimitedLinking String
from
        subsTo :: NonEmpty String
subsTo = String -> NonEmpty String
subsCd (String -> NonEmpty String) -> String -> NonEmpty String
forall a b. (a -> b) -> a -> b
$ LimitedLinking String -> String
forall nodeName. LimitedLinking nodeName -> nodeName
linking LimitedLinking String
to

nameFromTo
  :: Relationship a b
  -> Maybe (b, LimitedLinking a, LimitedLinking a)
nameFromTo :: forall a b.
Relationship a b -> Maybe (b, LimitedLinking a, LimitedLinking a)
nameFromTo = \case
  Association {b
LimitedLinking a
associationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
associationFrom :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
associationTo :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
associationName :: b
associationFrom :: LimitedLinking a
associationTo :: LimitedLinking a
..} ->
    (b, LimitedLinking a, LimitedLinking a)
-> Maybe (b, LimitedLinking a, LimitedLinking a)
forall a. a -> Maybe a
Just (b
associationName, LimitedLinking a
associationFrom, LimitedLinking a
associationTo)
  Aggregation {b
LimitedLinking a
aggregationName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
aggregationPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
aggregationWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
aggregationName :: b
aggregationPart :: LimitedLinking a
aggregationWhole :: LimitedLinking a
..} ->
    (b, LimitedLinking a, LimitedLinking a)
-> Maybe (b, LimitedLinking a, LimitedLinking a)
forall a. a -> Maybe a
Just (b
aggregationName, LimitedLinking a
aggregationPart, LimitedLinking a
aggregationWhole)
  Composition {b
LimitedLinking a
compositionName :: forall className relationshipName.
Relationship className relationshipName -> relationshipName
compositionPart :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
compositionWhole :: forall className relationshipName.
Relationship className relationshipName -> LimitedLinking className
compositionName :: b
compositionPart :: LimitedLinking a
compositionWhole :: LimitedLinking a
..} ->
    (b, LimitedLinking a, LimitedLinking a)
-> Maybe (b, LimitedLinking a, LimitedLinking a)
forall a. a -> Maybe a
Just (b
compositionName, LimitedLinking a
compositionPart, LimitedLinking a
compositionWhole)
  Inheritance {} ->
    Maybe (b, LimitedLinking a, LimitedLinking a)
forall a. Maybe a
Nothing

{-|
Generates inlined Alloy code equivalent to a combination of the first parts of
the @ObjectLowerAttribute@ or @ObjectLowerUpperAttribute@
and the @ObjectFieldNames@ predicate.
-}
makeNonInheritance
  :: [String]
  -> String
  -> [String]
  -> String
makeNonInheritance :: [String] -> String -> [String] -> String
makeNonInheritance [String]
fromSet String
name [String]
toSet =
  [i|  #{name} in #{alloySetOfParens fromSet} -> #{alloySetOfParens toSet}|]
  -- alternative to @ObjectFieldNames@ predicate inlined and simplified

{-|
Generates inline, simplified Alloy code equivalent to
the @ObjectLowerAttribute@ or @ObjectLowerUpperAttribute@ predicate
or
the @ObjectLower@ or @ObjectLowerUpper@ predicate,
depending on the first parameter.
-}
makeNonInheritanceLimits
  :: (String -> String)
  -> NonEmpty String
  -> (Int, Maybe Int)
  -> String
makeNonInheritanceLimits :: ShowS -> NonEmpty String -> (Int, Maybe Int) -> String
makeNonInheritanceLimits ShowS
nameLinking NonEmpty String
fromSet (Int, Maybe Int)
limits =
  [i|  all o : #{alloySetOf $ toList fromSet} | |]
  String -> ShowS -> String
forall a b. a -> (a -> b) -> b
& ShowS -> (Int, Maybe Int) -> ShowS
nonInheritanceLimits ShowS
nameLinking (Int, Maybe Int)
limits

{-|
Reusable part of defining multiplicity constraints for a non-inheritance
relationship.
-}
nonInheritanceLimits
  :: (String -> String)
  -> (Int, Maybe Int)
  -> String
  -- ^ String to prepend (if constraint needs to be set)
  -> String
nonInheritanceLimits :: ShowS -> (Int, Maybe Int) -> ShowS
nonInheritanceLimits ShowS
nameLinking (Int
low, Maybe Int
maybeUp) =
  case Maybe Int
maybeUp of
    Maybe Int
Nothing -> case Int
low of
      Int
0 -> String -> ShowS
forall a b. a -> b -> a
const String
""
      Int
_ -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{linkCount} >= #{low}|])
      -- @ObjectLowerAttribute@ or @ObjectLower@ predicate
      -- inlined and simplified
    Just Int
up -> case Int
low of
      Int
0 -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{linkCount} =< #{up}|])
      Int
_ | Int
low Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
up -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{linkCount} = #{up}|])
        | Bool
otherwise -> (String -> ShowS
forall a. [a] -> [a] -> [a]
++ [iii|#{linkCount} >= #{low} and #{linkCount} =< #{up}|])
      -- @ObjectLowerUpperAttribute@ or @ObjectLowerUpper@ predicate
      -- inlined and simplified
  where
    linkCount :: String
linkCount = Char
'#' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
nameLinking String
"o"

{-|
Generates inlined, simplified Alloy code
equivalent to the @Composition@ predicate.
-}
compositeConstraint :: String -> [String] -> String
compositeConstraint :: String -> [String] -> String
compositeConstraint String
objectSet [String]
nameSet =
  String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
""
    (\String
usedFieldCount -> [i|  all o : #{objectSet} | #{usedFieldCount} =< 1|])
    (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe String
alloyPlus
    ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
`map` [String] -> [String]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [String]
nameSet) (ShowS -> [String]) -> ShowS -> [String]
forall a b. (a -> b) -> a -> b
$ \String
fieldName ->
      [iii|\#o.#{fieldName}|]
  -- @Composition@ predicate inlined and simplified

{-|
Generates the code to add the Alloy Int values of the given list.
-}
alloyPlus :: [String] -> Maybe String
alloyPlus :: [String] -> Maybe String
alloyPlus = \case
  [] -> Maybe String
forall a. Maybe a
Nothing
  [String
x] -> String -> Maybe String
forall a. a -> Maybe a
Just String
x
  xs :: [String]
xs@(String
_:String
_:[String]
_) -> [String] -> Maybe String
alloyPlus ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
pairPlus [String]
xs
  where
    pairPlus :: [String] -> [String]
pairPlus = \case
      [] -> []
      x :: [String]
x@[String
_] -> [String]
x
      (String
x:String
y:[String]
zs) -> [i|plus[#{x}, #{y}]|] String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
pairPlus [String]
zs

{-|
Merges Alloy code 'Parts' for multiple class diagrams
to be used in a single Alloy query.
-}
mergeParts
  :: Parts
  -> Parts
  -> Parts
mergeParts :: Parts -> Parts -> Parts
mergeParts Parts
p Parts
p' = String -> String -> String -> Parts
Parts
  (Parts -> String
part1 Parts
p)
  (Parts -> String
part2 Parts
p String -> ShowS
`unionL` Parts -> String
part2 Parts
p')
  (Parts -> String
part3 Parts
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ Parts -> String
part3 Parts
p')
  where
    unionL :: String -> ShowS
unionL String
x String
y = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ([String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
""]) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
x [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` String -> [String]
lines String
y

{-|
Transforms 'Parts' into an Alloy program (besides the run command).

(See 'createRunCommand' for the latter)
-}
combineParts :: Parts -> String
combineParts :: Parts -> String
combineParts Parts {String
part1 :: Parts -> String
part2 :: Parts -> String
part3 :: Parts -> String
part1 :: String
part2 :: String
part3 :: String
..} = String
part1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
part2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
part3

{-|
Transform a set into Alloy code of a set.
-}
alloySetOf :: [String] -> String
alloySetOf :: [String] -> String
alloySetOf [String]
xs
  | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
xs = String
"none"
  | Bool
otherwise = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" + " [String]
xs

alloySetOfParens :: [String] -> String
alloySetOfParens :: [String] -> String
alloySetOfParens xs :: [String]
xs@(String
_:String
_:[String]
_) = [i|(#{alloySetOf xs})|]
alloySetOfParens [String]
xs = [String] -> String
alloySetOf [String]
xs