{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PostfixOperators #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}

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

   -- * Constructors
   mkConstraintSet,
) where

import           Control.Lens (makeLenses, (^.))
import qualified Data.List.NonEmpty as NE
import           Language.Drasil

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

makeLenses ''ConstraintSet

-- | Finds the 'UID' of the 'ConstraintSet'.
instance HasUID        (ConstraintSet e) where uid :: Getter (ConstraintSet e) UID
uid  = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e (f :: * -> *).
Functor f =>
(ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
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 => Getter c UID
Getter ConceptChunk UID
uid
-- | Finds the term ('NP') of the 'ConstraintSet'.
instance NamedIdea     (ConstraintSet e) where term :: Lens' (ConstraintSet e) NP
term = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e (f :: * -> *).
Functor f =>
(ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
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
Lens' ConceptChunk 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 (f :: * -> *).
Functor f =>
(ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
con)
-- | Finds the definition of the 'ConstraintSet'.
instance Definition    (ConstraintSet e) where defn :: Lens' (ConstraintSet e) Sentence
defn = (ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
forall e (f :: * -> *).
Functor f =>
(ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
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
Lens' ConceptChunk 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 (f :: * -> *).
Functor f =>
(ConceptChunk -> f ConceptChunk)
-> ConstraintSet e -> f (ConstraintSet e)
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 a. (a -> a -> a) -> [a] -> a
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 (f :: * -> *).
Functor f =>
(NonEmpty e -> f (NonEmpty e))
-> ConstraintSet e -> f (ConstraintSet e)
invs)
-- | Exposes all relations and an expectation of the type of a relation (Bool)
instance RequiresChecking (ConstraintSet Expr) Expr Space where
  requiredChecks :: ConstraintSet Expr -> [(Expr, Space)]
requiredChecks ConstraintSet Expr
cs = (Expr -> (Expr, Space)) -> [Expr] -> [(Expr, Space)]
forall a b. (a -> b) -> [a] -> [b]
map (,Space
Boolean) ([Expr] -> [(Expr, Space)]) -> [Expr] -> [(Expr, Space)]
forall a b. (a -> b) -> a -> b
$ NonEmpty Expr -> [Expr]
forall a. NonEmpty a -> [a]
NE.toList (ConstraintSet Expr
cs ConstraintSet Expr
-> Getting (NonEmpty Expr) (ConstraintSet Expr) (NonEmpty Expr)
-> NonEmpty Expr
forall s a. s -> Getting a s a -> a
^. Getting (NonEmpty Expr) (ConstraintSet Expr) (NonEmpty Expr)
forall e e (f :: * -> *).
Functor f =>
(NonEmpty e -> f (NonEmpty e))
-> ConstraintSet e -> f (ConstraintSet e)
invs)

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