{-# LANGUAGE TemplateHaskell, Rank2Types, ScopedTypeVariables, PostfixOperators  #-}

-- | Defines types used in models and theories.
module Theory.Drasil.ConstraintSet (
  -- * Type
  ConstraintSet,
  -- * Constructor
  mkConstraintSet) where

import Control.Lens ((^.), makeLenses)

import Language.Drasil
import qualified Data.List.NonEmpty as NE

-- | 'ConstraintSet's are sets of invariants that always hold for underlying domains.
data ConstraintSet e = CL {
    ConstraintSet e -> ConceptChunk
_con  :: ConceptChunk,
    ConstraintSet e -> NonEmpty e
_invs :: NE.NonEmpty e
}
makeLenses ''ConstraintSet

-- | Finds the 'UID' of the 'ConstraintSet'.
instance HasUID        (ConstraintSet e) where uid :: (UID -> f UID) -> ConstraintSet e -> f (ConstraintSet e)
uid   = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e. Lens' (ConstraintSet e) ConceptChunk
con ((ConceptChunk -> f ConceptChunk)
 -> ConstraintSet e -> f (ConstraintSet e))
-> ((UID -> f UID) -> ConceptChunk -> f ConceptChunk)
-> (UID -> f UID)
-> ConstraintSet e
-> f (ConstraintSet e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UID -> f UID) -> ConceptChunk -> f ConceptChunk
forall c. HasUID c => Lens' c UID
uid
-- | Finds the term ('NP') of the 'ConstraintSet'.
instance NamedIdea     (ConstraintSet e) where term :: (NP -> f NP) -> ConstraintSet e -> f (ConstraintSet e)
term  = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e. Lens' (ConstraintSet e) ConceptChunk
con ((ConceptChunk -> f ConceptChunk)
 -> ConstraintSet e -> f (ConstraintSet e))
-> ((NP -> f NP) -> ConceptChunk -> f ConceptChunk)
-> (NP -> f NP)
-> ConstraintSet e
-> f (ConstraintSet e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP -> f NP) -> ConceptChunk -> f ConceptChunk
forall c. NamedIdea c => Lens' c NP
term
-- | Finds the idea of the 'ConstraintSet'.
instance Idea          (ConstraintSet e) where getA :: ConstraintSet e -> Maybe String
getA  = ConceptChunk -> Maybe String
forall c. Idea c => c -> Maybe String
getA (ConceptChunk -> Maybe String)
-> (ConstraintSet e -> ConceptChunk)
-> ConstraintSet e
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConstraintSet e
-> Getting ConceptChunk (ConstraintSet e) ConceptChunk
-> ConceptChunk
forall s a. s -> Getting a s a -> a
^. Getting ConceptChunk (ConstraintSet e) ConceptChunk
forall e. Lens' (ConstraintSet e) ConceptChunk
con)
-- | Finds the definition of the 'ConstraintSet'.
instance Definition    (ConstraintSet e) where defn :: (Sentence -> f Sentence) -> ConstraintSet e -> f (ConstraintSet e)
defn  = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e. Lens' (ConstraintSet e) ConceptChunk
con ((ConceptChunk -> f ConceptChunk)
 -> ConstraintSet e -> f (ConstraintSet e))
-> ((Sentence -> f Sentence) -> ConceptChunk -> f ConceptChunk)
-> (Sentence -> f Sentence)
-> ConstraintSet e
-> f (ConstraintSet e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sentence -> f Sentence) -> ConceptChunk -> f ConceptChunk
forall c. Definition c => Lens' c Sentence
defn
-- | Finds the domain of the 'ConstraintSet'.
instance ConceptDomain (ConstraintSet e) where cdom :: ConstraintSet e -> [UID]
cdom  = ConceptChunk -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom (ConceptChunk -> [UID])
-> (ConstraintSet e -> ConceptChunk) -> ConstraintSet e -> [UID]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConstraintSet e
-> Getting ConceptChunk (ConstraintSet e) ConceptChunk
-> ConceptChunk
forall s a. s -> Getting a s a -> a
^. Getting ConceptChunk (ConstraintSet e) ConceptChunk
forall e. Lens' (ConstraintSet e) ConceptChunk
con)
-- | The complete 'ModelExpr' of a ConstraintSet is the logical conjunction of
--   all the underlying relations (e.g., `a $&& b $&& ... $&& z`).
instance Express e => Express (ConstraintSet e) where
    express :: ConstraintSet e -> ModelExpr
express = (ModelExpr -> ModelExpr -> ModelExpr) -> [ModelExpr] -> ModelExpr
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ModelExpr -> ModelExpr -> ModelExpr
forall r. ExprC r => r -> r -> r
($&&) ([ModelExpr] -> ModelExpr)
-> (ConstraintSet e -> [ModelExpr]) -> ConstraintSet e -> ModelExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> ModelExpr) -> [e] -> [ModelExpr]
forall a b. (a -> b) -> [a] -> [b]
map e -> ModelExpr
forall c. Express c => c -> ModelExpr
express ([e] -> [ModelExpr])
-> (ConstraintSet e -> [e]) -> ConstraintSet e -> [ModelExpr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty e -> [e]
forall a. NonEmpty a -> [a]
NE.toList (NonEmpty e -> [e])
-> (ConstraintSet e -> NonEmpty e) -> ConstraintSet e -> [e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConstraintSet e
-> Getting (NonEmpty e) (ConstraintSet e) (NonEmpty e)
-> NonEmpty e
forall s a. s -> Getting a s a -> a
^. Getting (NonEmpty e) (ConstraintSet e) (NonEmpty e)
forall e e.
Lens (ConstraintSet e) (ConstraintSet e) (NonEmpty e) (NonEmpty e)
invs)

-- | Smart constructor for building ConstraintSets
mkConstraintSet :: ConceptChunk -> NE.NonEmpty e -> ConstraintSet e
mkConstraintSet :: ConceptChunk -> NonEmpty e -> ConstraintSet e
mkConstraintSet = ConceptChunk -> NonEmpty e -> ConstraintSet e
forall e. ConceptChunk -> NonEmpty e -> ConstraintSet e
CL