{-# LANGUAGE TemplateHaskell, Rank2Types, ScopedTypeVariables, PostfixOperators, GADTs  #-}
-- | Defines types and functions for creating models.
module Theory.Drasil.ModelKinds (
  -- * Types
  ModelKind(..), ModelKinds(..),
  -- * Constructors
  newDEModel, deModel, equationalConstraints, equationalModel, equationalRealm, othModel,
  newDEModel', deModel', equationalConstraints', equationalModel', equationalRealm', othModel',
  equationalModelU, equationalModelN, equationalRealmU, equationalRealmN,
  -- * Lenses
  setMk, elimMk, lensMk,
  -- * Functions
  getEqModQds
  ) where

import Control.Lens (makeLenses, set, lens, to, (^.), Setter', Getter, Lens')
import Data.Maybe (mapMaybe)

import Language.Drasil (NamedIdea(..), NP, QDefinition, HasUID(..), Expr,
  RelationConcept, ConceptDomain(..), Definition(..), Idea(..), Express(..),
  UID, DifferentialModel, mkUid)
import Theory.Drasil.ConstraintSet (ConstraintSet)
import Theory.Drasil.MultiDefn (MultiDefn)

-- | Models can be of different kinds: 
--
--     * 'NewDEModel's represent differential equations as 'DifferentialModel's
--     * 'DEModel's represent differential equations as 'RelationConcept's
--     * 'EquationalConstraint's represent invariants that will hold in a system of equations.
--     * 'EquationalModel's represent quantities that are calculated via a single definition/'QDefinition'.
--     * 'EquationalRealm's represent MultiDefns; quantities that may be calculated using any one of many 'DefiningExpr's (e.g., 'x = A = ... = Z')
--     * 'FunctionalModel's represent quantity-resulting function definitions.
--     * 'OthModel's are placeholders for models. No new 'OthModel's should be created, they should be using one of the other kinds.
data ModelKinds e where
  NewDEModel            :: DifferentialModel -> ModelKinds e
  DEModel               :: RelationConcept   -> ModelKinds e -- TODO: Split into ModelKinds Expr and ModelKinds ModelExpr resulting variants. The Expr variant should carry enough information that it can be solved properly.
  EquationalConstraints :: ConstraintSet e   -> ModelKinds e
  EquationalModel       :: QDefinition e     -> ModelKinds e
  EquationalRealm       :: MultiDefn e       -> ModelKinds e
  OthModel              :: RelationConcept   -> ModelKinds e -- TODO: Remove (after having removed all instances of it).

-- | 'ModelKinds' carrier, used to carry commonly overwritten information from the IMs/TMs/GDs.
data ModelKind e = MK {
  ModelKind e -> ModelKinds e
_mk     :: ModelKinds e,
  ModelKind e -> UID
_mkUID  :: UID,
  ModelKind e -> NP
_mkTerm :: NP
}

makeLenses ''ModelKind

-- | Smart constructor for 'NewDEModel's
newDEModel :: String -> NP -> DifferentialModel -> ModelKind e
newDEModel :: String -> NP -> DifferentialModel -> ModelKind e
newDEModel u :: String
u n :: NP
n dm :: DifferentialModel
dm = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (DifferentialModel -> ModelKinds e
forall e. DifferentialModel -> ModelKinds e
NewDEModel DifferentialModel
dm) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'NewDEModel's, deriving UID+Term from the 'DifferentialModel'
newDEModel' :: DifferentialModel -> ModelKind e
newDEModel' :: DifferentialModel -> ModelKind e
newDEModel' dm :: DifferentialModel
dm = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (DifferentialModel -> ModelKinds e
forall e. DifferentialModel -> ModelKinds e
NewDEModel DifferentialModel
dm) (DifferentialModel
dm DifferentialModel -> Getting UID DifferentialModel UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID DifferentialModel UID
forall c. HasUID c => Lens' c UID
uid) (DifferentialModel
dm DifferentialModel -> Getting NP DifferentialModel NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP DifferentialModel NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'DEModel's
deModel :: String -> NP -> RelationConcept -> ModelKind e
deModel :: String -> NP -> RelationConcept -> ModelKind e
deModel u :: String
u n :: NP
n rc :: RelationConcept
rc = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (RelationConcept -> ModelKinds e
forall e. RelationConcept -> ModelKinds e
DEModel RelationConcept
rc) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'DEModel's, deriving UID+Term from the 'RelationConcept'
deModel' :: RelationConcept -> ModelKind e
deModel' :: RelationConcept -> ModelKind e
deModel' rc :: RelationConcept
rc = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (RelationConcept -> ModelKinds e
forall e. RelationConcept -> ModelKinds e
DEModel RelationConcept
rc) (RelationConcept
rc RelationConcept -> Getting UID RelationConcept UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID RelationConcept UID
forall c. HasUID c => Lens' c UID
uid) (RelationConcept
rc RelationConcept -> Getting NP RelationConcept NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP RelationConcept NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalConstraints'
equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e
equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e
equationalConstraints u :: String
u n :: NP
n qs :: ConstraintSet e
qs = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (ConstraintSet e -> ModelKinds e
forall e. ConstraintSet e -> ModelKinds e
EquationalConstraints ConstraintSet e
qs) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'EquationalConstraints', deriving UID+Term from the 'ConstraintSet'
equationalConstraints' :: ConstraintSet e -> ModelKind e
equationalConstraints' :: ConstraintSet e -> ModelKind e
equationalConstraints' qs :: ConstraintSet e
qs = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (ConstraintSet e -> ModelKinds e
forall e. ConstraintSet e -> ModelKinds e
EquationalConstraints ConstraintSet e
qs) (ConstraintSet e
qs ConstraintSet e -> Getting UID (ConstraintSet e) UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID (ConstraintSet e) UID
forall c. HasUID c => Lens' c UID
uid) (ConstraintSet e
qs ConstraintSet e -> Getting NP (ConstraintSet e) NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP (ConstraintSet e) NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalModel's
equationalModel :: String -> NP -> QDefinition e -> ModelKind e
equationalModel :: String -> NP -> QDefinition e -> ModelKind e
equationalModel u :: String
u n :: NP
n qd :: QDefinition e
qd = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (QDefinition e -> ModelKinds e
forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'EquationalModel's, deriving UID+Term from the 'QDefinition'
equationalModel' :: QDefinition e -> ModelKind e
equationalModel' :: QDefinition e -> ModelKind e
equationalModel' qd :: QDefinition e
qd = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (QDefinition e -> ModelKinds e
forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (QDefinition e
qd QDefinition e -> Getting UID (QDefinition e) UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID (QDefinition e) UID
forall c. HasUID c => Lens' c UID
uid) (QDefinition e
qd QDefinition e -> Getting NP (QDefinition e) NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP (QDefinition e) NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalModel's, deriving Term from the 'QDefinition'
equationalModelU :: String -> QDefinition e -> ModelKind e
equationalModelU :: String -> QDefinition e -> ModelKind e
equationalModelU u :: String
u qd :: QDefinition e
qd = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (QDefinition e -> ModelKinds e
forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (String -> UID
mkUid String
u) (QDefinition e
qd QDefinition e -> Getting NP (QDefinition e) NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP (QDefinition e) NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalModel's, deriving UID from the 'QDefinition'
equationalModelN :: NP -> QDefinition e -> ModelKind e
equationalModelN :: NP -> QDefinition e -> ModelKind e
equationalModelN n :: NP
n qd :: QDefinition e
qd = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (QDefinition e -> ModelKinds e
forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (QDefinition e
qd QDefinition e -> Getting UID (QDefinition e) UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID (QDefinition e) UID
forall c. HasUID c => Lens' c UID
uid) NP
n

-- | Smart constructor for 'EquationalRealm's
equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e
equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e
equationalRealm u :: String
u n :: NP
n md :: MultiDefn e
md = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (MultiDefn e -> ModelKinds e
forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'EquationalRealm's, deriving UID+Term from the 'MultiDefn'
equationalRealm' :: MultiDefn e -> ModelKind e
equationalRealm' :: MultiDefn e -> ModelKind e
equationalRealm' md :: MultiDefn e
md = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (MultiDefn e -> ModelKinds e
forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (MultiDefn e
md MultiDefn e -> Getting UID (MultiDefn e) UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID (MultiDefn e) UID
forall c. HasUID c => Lens' c UID
uid) (MultiDefn e
md MultiDefn e -> Getting NP (MultiDefn e) NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP (MultiDefn e) NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalRealm's
equationalRealmU :: String -> MultiDefn e -> ModelKind e
equationalRealmU :: String -> MultiDefn e -> ModelKind e
equationalRealmU u :: String
u md :: MultiDefn e
md = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (MultiDefn e -> ModelKinds e
forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (String -> UID
mkUid String
u) (MultiDefn e
md MultiDefn e -> Getting NP (MultiDefn e) NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP (MultiDefn e) NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Smart constructor for 'EquationalRealm's, deriving UID from the 'MultiDefn'
equationalRealmN :: NP -> MultiDefn e -> ModelKind e
equationalRealmN :: NP -> MultiDefn e -> ModelKind e
equationalRealmN n :: NP
n md :: MultiDefn e
md = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (MultiDefn e -> ModelKinds e
forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (MultiDefn e
md MultiDefn e -> Getting UID (MultiDefn e) UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID (MultiDefn e) UID
forall c. HasUID c => Lens' c UID
uid) NP
n

-- | Smart constructor for 'OthModel's
othModel :: String -> NP -> RelationConcept -> ModelKind Expr
othModel :: String -> NP -> RelationConcept -> ModelKind Expr
othModel u :: String
u n :: NP
n rc :: RelationConcept
rc = ModelKinds Expr -> UID -> NP -> ModelKind Expr
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (RelationConcept -> ModelKinds Expr
forall e. RelationConcept -> ModelKinds e
OthModel RelationConcept
rc) (String -> UID
mkUid String
u) NP
n

-- | Smart constructor for 'OthModel's, deriving UID+Term from the 'RelationConcept'
othModel' :: RelationConcept -> ModelKind e
othModel' :: RelationConcept -> ModelKind e
othModel' rc :: RelationConcept
rc = ModelKinds e -> UID -> NP -> ModelKind e
forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (RelationConcept -> ModelKinds e
forall e. RelationConcept -> ModelKinds e
OthModel RelationConcept
rc) (RelationConcept
rc RelationConcept -> Getting UID RelationConcept UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID RelationConcept UID
forall c. HasUID c => Lens' c UID
uid) (RelationConcept
rc RelationConcept -> Getting NP RelationConcept NP -> NP
forall s a. s -> Getting a s a -> a
^. Getting NP RelationConcept NP
forall c. NamedIdea c => Lens' c NP
term)

-- | Finds the 'UID' of the 'ModelKinds'.
instance HasUID        (ModelKinds e) where uid :: (UID -> f UID) -> ModelKinds e -> f (ModelKinds e)
uid     = Lens' DifferentialModel UID
-> Lens' RelationConcept UID
-> Lens' (ConstraintSet e) UID
-> Lens' (QDefinition e) UID
-> Lens' (MultiDefn e) UID
-> Lens' (ModelKinds e) UID
forall e a.
Lens' DifferentialModel a
-> Lens' RelationConcept a
-> Lens' (ConstraintSet e) a
-> Lens' (QDefinition e) a
-> Lens' (MultiDefn e) a
-> Lens' (ModelKinds e) a
lensMk forall c. HasUID c => Lens' c UID
Lens' DifferentialModel UID
uid forall c. HasUID c => Lens' c UID
Lens' RelationConcept UID
uid forall c. HasUID c => Lens' c UID
Lens' (ConstraintSet e) UID
uid forall c. HasUID c => Lens' c UID
Lens' (QDefinition e) UID
uid forall c. HasUID c => Lens' c UID
Lens' (MultiDefn e) UID
uid
-- | Finds the term ('NP') of the 'ModelKinds'.
instance NamedIdea     (ModelKinds e) where term :: (NP -> f NP) -> ModelKinds e -> f (ModelKinds e)
term    = Lens' DifferentialModel NP
-> Lens' RelationConcept NP
-> Lens' (ConstraintSet e) NP
-> Lens' (QDefinition e) NP
-> Lens' (MultiDefn e) NP
-> Lens' (ModelKinds e) NP
forall e a.
Lens' DifferentialModel a
-> Lens' RelationConcept a
-> Lens' (ConstraintSet e) a
-> Lens' (QDefinition e) a
-> Lens' (MultiDefn e) a
-> Lens' (ModelKinds e) a
lensMk forall c. NamedIdea c => Lens' c NP
Lens' DifferentialModel NP
term forall c. NamedIdea c => Lens' c NP
Lens' RelationConcept NP
term forall c. NamedIdea c => Lens' c NP
Lens' (ConstraintSet e) NP
term forall c. NamedIdea c => Lens' c NP
Lens' (QDefinition e) NP
term forall c. NamedIdea c => Lens' c NP
Lens' (MultiDefn e) NP
term
-- | Finds the idea of the 'ModelKinds'.
instance Idea          (ModelKinds e) where getA :: ModelKinds e -> Maybe String
getA    = Getter DifferentialModel (Maybe String)
-> Getter RelationConcept (Maybe String)
-> Getter (ConstraintSet e) (Maybe String)
-> Getter (QDefinition e) (Maybe String)
-> Getter (MultiDefn e) (Maybe String)
-> ModelKinds e
-> Maybe String
forall a e.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
elimMk ((DifferentialModel -> Maybe String)
-> Optic' (->) f DifferentialModel (Maybe String)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to DifferentialModel -> Maybe String
forall c. Idea c => c -> Maybe String
getA) ((RelationConcept -> Maybe String)
-> Optic' (->) f RelationConcept (Maybe String)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to RelationConcept -> Maybe String
forall c. Idea c => c -> Maybe String
getA) ((ConstraintSet e -> Maybe String)
-> Optic' (->) f (ConstraintSet e) (Maybe String)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ConstraintSet e -> Maybe String
forall c. Idea c => c -> Maybe String
getA) ((QDefinition e -> Maybe String)
-> Optic' (->) f (QDefinition e) (Maybe String)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to QDefinition e -> Maybe String
forall c. Idea c => c -> Maybe String
getA) ((MultiDefn e -> Maybe String)
-> Optic' (->) f (MultiDefn e) (Maybe String)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to MultiDefn e -> Maybe String
forall c. Idea c => c -> Maybe String
getA)
-- | Finds the definition of the 'ModelKinds'.
instance Definition    (ModelKinds e) where defn :: (Sentence -> f Sentence) -> ModelKinds e -> f (ModelKinds e)
defn    = Lens' DifferentialModel Sentence
-> Lens' RelationConcept Sentence
-> Lens' (ConstraintSet e) Sentence
-> Lens' (QDefinition e) Sentence
-> Lens' (MultiDefn e) Sentence
-> Lens' (ModelKinds e) Sentence
forall e a.
Lens' DifferentialModel a
-> Lens' RelationConcept a
-> Lens' (ConstraintSet e) a
-> Lens' (QDefinition e) a
-> Lens' (MultiDefn e) a
-> Lens' (ModelKinds e) a
lensMk forall c. Definition c => Lens' c Sentence
Lens' DifferentialModel Sentence
defn forall c. Definition c => Lens' c Sentence
Lens' RelationConcept Sentence
defn forall c. Definition c => Lens' c Sentence
Lens' (ConstraintSet e) Sentence
defn forall c. Definition c => Lens' c Sentence
Lens' (QDefinition e) Sentence
defn forall c. Definition c => Lens' c Sentence
Lens' (MultiDefn e) Sentence
defn
-- | Finds the domain of the 'ModelKinds'.
instance ConceptDomain (ModelKinds e) where cdom :: ModelKinds e -> [UID]
cdom    = Getter DifferentialModel [UID]
-> Getter RelationConcept [UID]
-> Getter (ConstraintSet e) [UID]
-> Getter (QDefinition e) [UID]
-> Getter (MultiDefn e) [UID]
-> ModelKinds e
-> [UID]
forall a e.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
elimMk ((DifferentialModel -> [UID])
-> Optic' (->) f DifferentialModel [UID]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to DifferentialModel -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom) ((RelationConcept -> [UID]) -> Optic' (->) f RelationConcept [UID]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to RelationConcept -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom) ((ConstraintSet e -> [UID]) -> Optic' (->) f (ConstraintSet e) [UID]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ConstraintSet e -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom) ((QDefinition e -> [UID]) -> Optic' (->) f (QDefinition e) [UID]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to QDefinition e -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom) ((MultiDefn e -> [UID]) -> Optic' (->) f (MultiDefn e) [UID]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to MultiDefn e -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom)
-- | Rewrites the underlying model using 'ModelExpr'
instance Express e => Express (ModelKinds e) where
  express :: ModelKinds e -> ModelExpr
express = Getter DifferentialModel ModelExpr
-> Getter RelationConcept ModelExpr
-> Getter (ConstraintSet e) ModelExpr
-> Getter (QDefinition e) ModelExpr
-> Getter (MultiDefn e) ModelExpr
-> ModelKinds e
-> ModelExpr
forall a e.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
elimMk ((DifferentialModel -> ModelExpr)
-> Optic' (->) f DifferentialModel ModelExpr
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to DifferentialModel -> ModelExpr
forall c. Express c => c -> ModelExpr
express) ((RelationConcept -> ModelExpr)
-> Optic' (->) f RelationConcept ModelExpr
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to RelationConcept -> ModelExpr
forall c. Express c => c -> ModelExpr
express) ((ConstraintSet e -> ModelExpr)
-> Optic' (->) f (ConstraintSet e) ModelExpr
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ConstraintSet e -> ModelExpr
forall c. Express c => c -> ModelExpr
express) ((QDefinition e -> ModelExpr)
-> Optic' (->) f (QDefinition e) ModelExpr
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to QDefinition e -> ModelExpr
forall c. Express c => c -> ModelExpr
express) ((MultiDefn e -> ModelExpr) -> Optic' (->) f (MultiDefn e) ModelExpr
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to MultiDefn e -> ModelExpr
forall c. Express c => c -> ModelExpr
express)

-- TODO: implement MayHaveUnit for ModelKinds once we've sufficiently removed OthModels & RelationConcepts (else we'd be breaking too much of `stable`)

-- | Finds the 'UID' of the 'ModelKind'.
instance HasUID        (ModelKind e) where uid :: (UID -> f UID) -> ModelKind e -> f (ModelKind e)
uid     = (UID -> f UID) -> ModelKind e -> f (ModelKind e)
forall e. Lens' (ModelKind e) UID
mkUID
-- | Finds the term ('NP') of the 'ModelKind'.
instance NamedIdea     (ModelKind e) where term :: (NP -> f NP) -> ModelKind e -> f (ModelKind e)
term    = (NP -> f NP) -> ModelKind e -> f (ModelKind e)
forall e. Lens' (ModelKind e) NP
mkTerm
-- | Finds the idea of the 'ModelKind'.
instance Idea          (ModelKind e) where getA :: ModelKind e -> Maybe String
getA    = ModelKinds e -> Maybe String
forall c. Idea c => c -> Maybe String
getA (ModelKinds e -> Maybe String)
-> (ModelKind e -> ModelKinds e) -> ModelKind e -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModelKind e
-> Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
-> ModelKinds e
forall s a. s -> Getting a s a -> a
^. Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk)
-- | Finds the definition of the 'ModelKind'.
instance Definition    (ModelKind e) where defn :: (Sentence -> f Sentence) -> ModelKind e -> f (ModelKind e)
defn    = (ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind e)
forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk ((ModelKinds e -> f (ModelKinds e))
 -> ModelKind e -> f (ModelKind e))
-> ((Sentence -> f Sentence) -> ModelKinds e -> f (ModelKinds e))
-> (Sentence -> f Sentence)
-> ModelKind e
-> f (ModelKind e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sentence -> f Sentence) -> ModelKinds e -> f (ModelKinds e)
forall c. Definition c => Lens' c Sentence
defn
-- | Finds the domain of the 'ModelKind'.
instance ConceptDomain (ModelKind e) where cdom :: ModelKind e -> [UID]
cdom    = ModelKinds e -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom (ModelKinds e -> [UID])
-> (ModelKind e -> ModelKinds e) -> ModelKind e -> [UID]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModelKind e
-> Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
-> ModelKinds e
forall s a. s -> Getting a s a -> a
^. Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk)
-- | Rewrites the underlying model using 'ModelExpr'
instance Express e => Express (ModelKind e) where
  express :: ModelKind e -> ModelExpr
express = ModelKinds e -> ModelExpr
forall c. Express c => c -> ModelExpr
express (ModelKinds e -> ModelExpr)
-> (ModelKind e -> ModelKinds e) -> ModelKind e -> ModelExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModelKind e
-> Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
-> ModelKinds e
forall s a. s -> Getting a s a -> a
^. Getting (ModelKinds e) (ModelKind e) (ModelKinds e)
forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk)

-- | Retrieve internal data from ModelKinds
elimMk :: Getter DifferentialModel a 
  -> Getter RelationConcept a -> Getter (ConstraintSet e) a
  -> Getter (QDefinition e) a -> Getter (MultiDefn e) a
  -> ModelKinds e -> a
elimMk :: Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
elimMk f :: Getter DifferentialModel a
f _ _ _ _ (NewDEModel q :: DifferentialModel
q)            = DifferentialModel
q DifferentialModel -> Getting a DifferentialModel a -> a
forall s a. s -> Getting a s a -> a
^. Getting a DifferentialModel a
Getter DifferentialModel a
f
elimMk _ f :: Getter RelationConcept a
f _ _ _ (DEModel q :: RelationConcept
q)               = RelationConcept
q RelationConcept -> Getting a RelationConcept a -> a
forall s a. s -> Getting a s a -> a
^. Getting a RelationConcept a
Getter RelationConcept a
f
elimMk _ _ f :: Getter (ConstraintSet e) a
f _ _ (EquationalConstraints q :: ConstraintSet e
q) = ConstraintSet e
q ConstraintSet e -> Getting a (ConstraintSet e) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (ConstraintSet e) a
Getter (ConstraintSet e) a
f
elimMk _ _ _ f :: Getter (QDefinition e) a
f _ (EquationalModel q :: QDefinition e
q)       = QDefinition e
q QDefinition e -> Getting a (QDefinition e) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (QDefinition e) a
Getter (QDefinition e) a
f
elimMk _ _ _ _ f :: Getter (MultiDefn e) a
f (EquationalRealm q :: MultiDefn e
q)       = MultiDefn e
q MultiDefn e -> Getting a (MultiDefn e) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (MultiDefn e) a
Getter (MultiDefn e) a
f
elimMk _ f :: Getter RelationConcept a
f _ _ _ (OthModel q :: RelationConcept
q)              = RelationConcept
q RelationConcept -> Getting a RelationConcept a -> a
forall s a. s -> Getting a s a -> a
^. Getting a RelationConcept a
Getter RelationConcept a
f

-- | Map into internal representations of ModelKinds
setMk :: ModelKinds e
  -> Setter' DifferentialModel a
  -> Setter' RelationConcept a -> Setter' (ConstraintSet e) a
  -> Setter' (QDefinition e) a -> Setter' (MultiDefn e) a
  -> a -> ModelKinds e
setMk :: ModelKinds e
-> Setter' DifferentialModel a
-> Setter' RelationConcept a
-> Setter' (ConstraintSet e) a
-> Setter' (QDefinition e) a
-> Setter' (MultiDefn e) a
-> a
-> ModelKinds e
setMk (NewDEModel q :: DifferentialModel
q)            f :: Setter' DifferentialModel a
f _ _ _ _ x :: a
x = DifferentialModel -> ModelKinds e
forall e. DifferentialModel -> ModelKinds e
NewDEModel            (DifferentialModel -> ModelKinds e)
-> DifferentialModel -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter DifferentialModel DifferentialModel a a
-> a -> DifferentialModel -> DifferentialModel
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter DifferentialModel DifferentialModel a a
Setter' DifferentialModel a
f a
x DifferentialModel
q
setMk (DEModel q :: RelationConcept
q)               _ f :: Setter' RelationConcept a
f _ _ _ x :: a
x = RelationConcept -> ModelKinds e
forall e. RelationConcept -> ModelKinds e
DEModel               (RelationConcept -> ModelKinds e)
-> RelationConcept -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter RelationConcept RelationConcept a a
-> a -> RelationConcept -> RelationConcept
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter RelationConcept RelationConcept a a
Setter' RelationConcept a
f a
x RelationConcept
q
setMk (EquationalConstraints q :: ConstraintSet e
q) _ _ f :: Setter' (ConstraintSet e) a
f _ _ x :: a
x = ConstraintSet e -> ModelKinds e
forall e. ConstraintSet e -> ModelKinds e
EquationalConstraints (ConstraintSet e -> ModelKinds e)
-> ConstraintSet e -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter (ConstraintSet e) (ConstraintSet e) a a
-> a -> ConstraintSet e -> ConstraintSet e
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (ConstraintSet e) (ConstraintSet e) a a
Setter' (ConstraintSet e) a
f a
x ConstraintSet e
q
setMk (EquationalModel q :: QDefinition e
q)       _ _ _ f :: Setter' (QDefinition e) a
f _ x :: a
x = QDefinition e -> ModelKinds e
forall e. QDefinition e -> ModelKinds e
EquationalModel       (QDefinition e -> ModelKinds e) -> QDefinition e -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter (QDefinition e) (QDefinition e) a a
-> a -> QDefinition e -> QDefinition e
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (QDefinition e) (QDefinition e) a a
Setter' (QDefinition e) a
f a
x QDefinition e
q
setMk (EquationalRealm q :: MultiDefn e
q)       _ _ _ _ f :: Setter' (MultiDefn e) a
f x :: a
x = MultiDefn e -> ModelKinds e
forall e. MultiDefn e -> ModelKinds e
EquationalRealm       (MultiDefn e -> ModelKinds e) -> MultiDefn e -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter (MultiDefn e) (MultiDefn e) a a
-> a -> MultiDefn e -> MultiDefn e
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (MultiDefn e) (MultiDefn e) a a
Setter' (MultiDefn e) a
f a
x MultiDefn e
q
setMk (OthModel q :: RelationConcept
q)              _ f :: Setter' RelationConcept a
f _ _ _ x :: a
x = RelationConcept -> ModelKinds e
forall e. RelationConcept -> ModelKinds e
OthModel              (RelationConcept -> ModelKinds e)
-> RelationConcept -> ModelKinds e
forall a b. (a -> b) -> a -> b
$ ASetter RelationConcept RelationConcept a a
-> a -> RelationConcept -> RelationConcept
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter RelationConcept RelationConcept a a
Setter' RelationConcept a
f a
x RelationConcept
q

-- | Make a 'Lens' for 'ModelKinds'.
lensMk :: forall e a.
     Lens' DifferentialModel a
  -> Lens' RelationConcept a -> Lens' (ConstraintSet e) a 
  -> Lens' (QDefinition e) a -> Lens' (MultiDefn e) a
  -> Lens' (ModelKinds e) a
lensMk :: Lens' DifferentialModel a
-> Lens' RelationConcept a
-> Lens' (ConstraintSet e) a
-> Lens' (QDefinition e) a
-> Lens' (MultiDefn e) a
-> Lens' (ModelKinds e) a
lensMk ld :: Lens' DifferentialModel a
ld lr :: Lens' RelationConcept a
lr lcs :: Lens' (ConstraintSet e) a
lcs lq :: Lens' (QDefinition e) a
lq lmd :: Lens' (MultiDefn e) a
lmd = (ModelKinds e -> a)
-> (ModelKinds e -> a -> ModelKinds e) -> Lens' (ModelKinds e) a
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ModelKinds e -> a
g ModelKinds e -> a -> ModelKinds e
s
    where g :: ModelKinds e -> a
          g :: ModelKinds e -> a
g = Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
forall a e.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> ModelKinds e
-> a
elimMk Lens' DifferentialModel a
Getter DifferentialModel a
ld Lens' RelationConcept a
Getter RelationConcept a
lr Lens' (ConstraintSet e) a
Getter (ConstraintSet e) a
lcs Lens' (QDefinition e) a
Getter (QDefinition e) a
lq Lens' (MultiDefn e) a
Getter (MultiDefn e) a
lmd
          s :: ModelKinds e -> a -> ModelKinds e
          s :: ModelKinds e -> a -> ModelKinds e
s mk_ :: ModelKinds e
mk_ = ModelKinds e
-> Setter' DifferentialModel a
-> Setter' RelationConcept a
-> Setter' (ConstraintSet e) a
-> Setter' (QDefinition e) a
-> Setter' (MultiDefn e) a
-> a
-> ModelKinds e
forall e a.
ModelKinds e
-> Setter' DifferentialModel a
-> Setter' RelationConcept a
-> Setter' (ConstraintSet e) a
-> Setter' (QDefinition e) a
-> Setter' (MultiDefn e) a
-> a
-> ModelKinds e
setMk ModelKinds e
mk_ Lens' DifferentialModel a
Setter' DifferentialModel a
ld Lens' RelationConcept a
Setter' RelationConcept a
lr Lens' (ConstraintSet e) a
Setter' (ConstraintSet e) a
lcs Lens' (QDefinition e) a
Setter' (QDefinition e) a
lq Lens' (MultiDefn e) a
Setter' (MultiDefn e) a
lmd

-- | Extract a list of 'QDefinition's from a list of 'ModelKinds'.
getEqModQds :: [ModelKind e] -> [QDefinition e]
getEqModQds :: [ModelKind e] -> [QDefinition e]
getEqModQds = (ModelKind e -> Maybe (QDefinition e))
-> [ModelKind e] -> [QDefinition e]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ModelKind e -> Maybe (QDefinition e)
forall e. ModelKind e -> Maybe (QDefinition e)
eqMod
  where
    eqMod :: ModelKind e -> Maybe (QDefinition e)
eqMod (MK (EquationalModel f :: QDefinition e
f) _ _) = QDefinition e -> Maybe (QDefinition e)
forall a. a -> Maybe a
Just QDefinition e
f
    eqMod _                            = Maybe (QDefinition e)
forall a. Maybe a
Nothing