{-# 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 :: Lens' (ConstraintSet e) UID
uid  = forall e. Lens' (ConstraintSet e) ConceptChunk
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. HasUID c => Lens' c UID
uid
-- | Finds the term ('NP') of the 'ConstraintSet'.
instance NamedIdea     (ConstraintSet e) where term :: Lens' (ConstraintSet e) NP
term = forall e. Lens' (ConstraintSet e) ConceptChunk
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall c. Idea c => c -> Maybe String
getA forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e. Lens' (ConstraintSet e) ConceptChunk
con)
-- | Finds the definition of the 'ConstraintSet'.
instance Definition    (ConstraintSet e) where defn :: Lens' (ConstraintSet e) Sentence
defn = forall e. Lens' (ConstraintSet e) ConceptChunk
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Definition c => Lens' c Sentence
defn
-- | Finds the domain of the 'ConstraintSet'.
instance ConceptDomain (ConstraintSet e) where cdom :: ConstraintSet e -> [UID]
cdom = forall c. ConceptDomain c => c -> [UID]
cdom forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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 = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall r. ExprC r => r -> r -> r
($&&) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall c. Express c => c -> ModelExpr
express forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
NE.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e e.
Lens (ConstraintSet e) (ConstraintSet e) (NonEmpty e) (NonEmpty 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 = forall a b. (a -> b) -> [a] -> [b]
map (,Space
Boolean) forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList (ConstraintSet Expr
cs forall s a. s -> Getting a s a -> a
^. 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 :: forall e. ConceptChunk -> NonEmpty e -> ConstraintSet e
mkConstraintSet = forall e. ConceptChunk -> NonEmpty e -> ConstraintSet e
CL