{-# LANGUAGE TemplateHaskell, Rank2Types, ScopedTypeVariables, PostfixOperators, GADTs  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-- | 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, getterMk,
  -- * Functions
  getEqModQds
  ) where

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

import Drasil.Database (UID, HasUID(..), mkUid, nsUid)
import Language.Drasil (NamedIdea(..), NP, QDefinition, Expr,
  RelationConcept, ConceptDomain(..), Definition(..), Idea(..), Express(..),
  RequiresChecking(..), Space,
  HasSpace(typ), DefiningExpr(..))

import Theory.Drasil.ConstraintSet (ConstraintSet)
import Theory.Drasil.DifferentialModel (DifferentialModel)
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
  -- TODO: Analyze all instances of DEModels, convert them to (new, where
  -- applicable) variants of NewDEModel, and get rid of this.
  DEModel               :: RelationConcept   -> ModelKinds e
  EquationalConstraints :: ConstraintSet e   -> ModelKinds e
  EquationalModel       :: QDefinition e     -> ModelKinds e
  EquationalRealm       :: MultiDefn e       -> ModelKinds e
  -- TODO: Remove OthModel after having removed all instances of it.
  OthModel              :: RelationConcept   -> ModelKinds e

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

makeLenses ''ModelKind

modelNs :: UID -> UID
modelNs :: UID -> UID
modelNs = String -> UID -> UID
nsUid String
"theory"

mkUid' :: String -> UID
mkUid' :: String -> UID
mkUid' = UID -> UID
modelNs (UID -> UID) -> (String -> UID) -> String -> UID
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> UID
mkUid

-- | Smart constructor for 'NewDEModel's
newDEModel :: String -> NP -> DifferentialModel -> ModelKind e
newDEModel :: forall e. String -> NP -> DifferentialModel -> ModelKind e
newDEModel String
u NP
n 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' :: forall e. DifferentialModel -> ModelKind e
newDEModel' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter DifferentialModel 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
Lens' DifferentialModel NP
term)

-- | Smart constructor for 'DEModel's
deModel :: String -> NP -> RelationConcept -> ModelKind e
deModel :: forall e. String -> NP -> RelationConcept -> ModelKind e
deModel String
u NP
n 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' :: forall e. RelationConcept -> ModelKind e
deModel' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter RelationConcept 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
Lens' RelationConcept NP
term)

-- | Smart constructor for 'EquationalConstraints'
equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e
equationalConstraints :: forall e. String -> NP -> ConstraintSet e -> ModelKind e
equationalConstraints String
u NP
n 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' :: forall e. ConstraintSet e -> ModelKind e
equationalConstraints' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter (ConstraintSet e) 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
Lens' (ConstraintSet e) NP
term)

-- | Smart constructor for 'EquationalModel's
equationalModel :: String -> NP -> QDefinition e -> ModelKind e
equationalModel :: forall e. String -> NP -> QDefinition e -> ModelKind e
equationalModel String
u NP
n 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' :: forall e. QDefinition e -> ModelKind e
equationalModel' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter (QDefinition e) 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
Lens' (QDefinition e) NP
term)

-- | Smart constructor for 'EquationalModel's, deriving Term from the 'QDefinition'
equationalModelU :: String -> QDefinition e -> ModelKind e
equationalModelU :: forall e. String -> QDefinition e -> ModelKind e
equationalModelU String
u 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
Lens' (QDefinition e) NP
term)

-- | Smart constructor for 'EquationalModel's, deriving UID from the 'QDefinition'
equationalModelN :: NP -> QDefinition e -> ModelKind e
equationalModelN :: forall e. NP -> QDefinition e -> ModelKind e
equationalModelN NP
n 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter (QDefinition e) UID
uid) NP
n

-- | Smart constructor for 'EquationalRealm's
equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e
equationalRealm :: forall e. String -> NP -> MultiDefn e -> ModelKind e
equationalRealm String
u NP
n 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' :: forall e. MultiDefn e -> ModelKind e
equationalRealm' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter (MultiDefn e) 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
Lens' (MultiDefn e) NP
term)

-- | Smart constructor for 'EquationalRealm's
equationalRealmU :: String -> MultiDefn e -> ModelKind e
equationalRealmU :: forall e. String -> MultiDefn e -> ModelKind e
equationalRealmU String
u 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
Lens' (MultiDefn e) NP
term)

-- | Smart constructor for 'EquationalRealm's, deriving UID from the 'MultiDefn'
equationalRealmN :: NP -> MultiDefn e -> ModelKind e
equationalRealmN :: forall e. NP -> MultiDefn e -> ModelKind e
equationalRealmN NP
n 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter (MultiDefn e) UID
uid) NP
n

-- | Smart constructor for 'OthModel's
othModel :: String -> NP -> RelationConcept -> ModelKind Expr
othModel :: String -> NP -> RelationConcept -> ModelKind Expr
othModel String
u NP
n 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' :: forall e. RelationConcept -> ModelKind e
othModel' 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) (UID -> UID
modelNs (UID -> UID) -> UID -> UID
forall a b. (a -> b) -> a -> b
$ 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 => Getter c UID
Getter RelationConcept 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
Lens' RelationConcept NP
term)

-- | Finds the 'UID' of the 'ModelKinds'.
instance HasUID        (ModelKinds e) where uid :: Getter (ModelKinds e) UID
uid     = Getter DifferentialModel UID
-> Getter RelationConcept UID
-> Getter (ConstraintSet e) UID
-> Getter (QDefinition e) UID
-> Getter (MultiDefn e) UID
-> Getter (ModelKinds e) UID
forall e a.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> Getter (ModelKinds e) a
getterMk (UID -> f UID) -> DifferentialModel -> f DifferentialModel
forall c. HasUID c => Getter c UID
Getter DifferentialModel UID
uid (UID -> f UID) -> RelationConcept -> f RelationConcept
forall c. HasUID c => Getter c UID
Getter RelationConcept UID
uid (UID -> f UID) -> ConstraintSet e -> f (ConstraintSet e)
forall c. HasUID c => Getter c UID
Getter (ConstraintSet e) UID
uid (UID -> f UID) -> QDefinition e -> f (QDefinition e)
forall c. HasUID c => Getter c UID
Getter (QDefinition e) UID
uid (UID -> f UID) -> MultiDefn e -> f (MultiDefn e)
forall c. HasUID c => Getter c UID
Getter (MultiDefn e) UID
uid
-- | Finds the term ('NP') of the 'ModelKinds'.
instance NamedIdea     (ModelKinds e) where term :: Lens' (ModelKinds e) NP
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 (NP -> f NP) -> DifferentialModel -> f DifferentialModel
forall c. NamedIdea c => Lens' c NP
Lens' DifferentialModel NP
term (NP -> f NP) -> RelationConcept -> f RelationConcept
forall c. NamedIdea c => Lens' c NP
Lens' RelationConcept NP
term (NP -> f NP) -> ConstraintSet e -> f (ConstraintSet e)
forall c. NamedIdea c => Lens' c NP
Lens' (ConstraintSet e) NP
term (NP -> f NP) -> QDefinition e -> f (QDefinition e)
forall c. NamedIdea c => Lens' c NP
Lens' (QDefinition e) NP
term (NP -> f NP) -> MultiDefn e -> f (MultiDefn e)
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)
-> (Maybe String -> f (Maybe String))
-> DifferentialModel
-> f DifferentialModel
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)
-> (Maybe String -> f (Maybe String))
-> RelationConcept
-> f RelationConcept
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)
-> (Maybe String -> f (Maybe String))
-> ConstraintSet e
-> f (ConstraintSet e)
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)
-> (Maybe String -> f (Maybe String))
-> QDefinition e
-> f (QDefinition e)
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)
-> (Maybe String -> f (Maybe String))
-> MultiDefn e
-> f (MultiDefn e)
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 :: Lens' (ModelKinds e) Sentence
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 (Sentence -> f Sentence)
-> DifferentialModel -> f DifferentialModel
forall c. Definition c => Lens' c Sentence
Lens' DifferentialModel Sentence
defn (Sentence -> f Sentence) -> RelationConcept -> f RelationConcept
forall c. Definition c => Lens' c Sentence
Lens' RelationConcept Sentence
defn (Sentence -> f Sentence) -> ConstraintSet e -> f (ConstraintSet e)
forall c. Definition c => Lens' c Sentence
Lens' (ConstraintSet e) Sentence
defn (Sentence -> f Sentence) -> QDefinition e -> f (QDefinition e)
forall c. Definition c => Lens' c Sentence
Lens' (QDefinition e) Sentence
defn (Sentence -> f Sentence) -> MultiDefn e -> f (MultiDefn e)
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])
-> ([UID] -> f [UID]) -> DifferentialModel -> f DifferentialModel
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])
-> ([UID] -> f [UID]) -> RelationConcept -> f RelationConcept
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])
-> ([UID] -> f [UID]) -> ConstraintSet e -> f (ConstraintSet e)
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])
-> ([UID] -> f [UID]) -> QDefinition e -> f (QDefinition e)
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])
-> ([UID] -> f [UID]) -> MultiDefn e -> f (MultiDefn e)
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)
-> (ModelExpr -> f ModelExpr)
-> DifferentialModel
-> f DifferentialModel
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)
-> (ModelExpr -> f ModelExpr)
-> RelationConcept
-> f RelationConcept
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)
-> (ModelExpr -> f ModelExpr)
-> ConstraintSet e
-> f (ConstraintSet e)
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)
-> (ModelExpr -> f ModelExpr) -> QDefinition e -> f (QDefinition e)
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)
-> (ModelExpr -> f ModelExpr) -> MultiDefn e -> f (MultiDefn e)
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)
-- | Expose all expressions that need to be type-checked for theories that need
--   expose 'Expr's.
instance RequiresChecking (ModelKinds Expr) Expr Space where
  requiredChecks :: ModelKinds Expr -> [(Expr, Space)]
requiredChecks (NewDEModel DifferentialModel
dm)            = DifferentialModel -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks DifferentialModel
dm
  requiredChecks (DEModel RelationConcept
_)                = [(Expr, Space)]
forall a. Monoid a => a
mempty
  requiredChecks (EquationalConstraints ConstraintSet Expr
cs) = ConstraintSet Expr -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks ConstraintSet Expr
cs
  requiredChecks (EquationalModel QDefinition Expr
qd)       = (Expr, Space) -> [(Expr, Space)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QDefinition Expr
qd QDefinition Expr -> Getting Expr (QDefinition Expr) Expr -> Expr
forall s a. s -> Getting a s a -> a
^. Getting Expr (QDefinition Expr) Expr
forall e. Lens' (QDefinition e) e
forall (c :: * -> *) e. DefiningExpr c => Lens' (c e) e
defnExpr, QDefinition Expr
qd QDefinition Expr -> Getting Space (QDefinition Expr) Space -> Space
forall s a. s -> Getting a s a -> a
^. Getting Space (QDefinition Expr) Space
forall c. HasSpace c => Getter c Space
Getter (QDefinition Expr) Space
typ)
  requiredChecks (EquationalRealm MultiDefn Expr
md)       = MultiDefn Expr -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks MultiDefn Expr
md
  requiredChecks (OthModel RelationConcept
_)               = [(Expr, Space)]
forall a. Monoid a => a
mempty

-- 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 :: Getter (ModelKind e) UID
uid     = (UID -> f UID) -> ModelKind e -> f (ModelKind e)
forall e (f :: * -> *).
Functor f =>
(UID -> f UID) -> ModelKind e -> f (ModelKind e)
mkUID
-- | Finds the term ('NP') of the 'ModelKind'.
instance NamedIdea     (ModelKind e) where term :: Lens' (ModelKind e) NP
term    = (NP -> f NP) -> ModelKind e -> f (ModelKind e)
forall e (f :: * -> *).
Functor f =>
(NP -> f NP) -> ModelKind e -> f (ModelKind e)
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 (f :: * -> *).
Functor f =>
(ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind e)
mk)
-- | Finds the definition of the 'ModelKind'.
instance Definition    (ModelKind e) where defn :: Lens' (ModelKind e) Sentence
defn    = (ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind e)
forall e e (f :: * -> *).
Functor f =>
(ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind 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
Lens' (ModelKinds e) 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 (f :: * -> *).
Functor f =>
(ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind 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 (f :: * -> *).
Functor f =>
(ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind e)
mk)
-- | Expose all expressions that need to be type-checked for theories that need
--   expose 'Expr's.
instance RequiresChecking (ModelKind Expr) Expr Space where
  requiredChecks :: ModelKind Expr -> [(Expr, Space)]
requiredChecks = ModelKinds Expr -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks (ModelKinds Expr -> [(Expr, Space)])
-> (ModelKind Expr -> ModelKinds Expr)
-> ModelKind Expr
-> [(Expr, Space)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModelKind Expr
-> Getting (ModelKinds Expr) (ModelKind Expr) (ModelKinds Expr)
-> ModelKinds Expr
forall s a. s -> Getting a s a -> a
^. Getting (ModelKinds Expr) (ModelKind Expr) (ModelKinds Expr)
forall e e (f :: * -> *).
Functor f =>
(ModelKinds e -> f (ModelKinds e))
-> ModelKind e -> f (ModelKind 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 :: 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 Getter DifferentialModel a
f Getter RelationConcept a
_ Getter (ConstraintSet e) a
_ Getter (QDefinition e) a
_ Getter (MultiDefn e) a
_ (NewDEModel 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 Getter DifferentialModel a
_ Getter RelationConcept a
f Getter (ConstraintSet e) a
_ Getter (QDefinition e) a
_ Getter (MultiDefn e) a
_ (DEModel 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 Getter DifferentialModel a
_ Getter RelationConcept a
_ Getter (ConstraintSet e) a
f Getter (QDefinition e) a
_ Getter (MultiDefn e) a
_ (EquationalConstraints 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 Getter DifferentialModel a
_ Getter RelationConcept a
_ Getter (ConstraintSet e) a
_ Getter (QDefinition e) a
f Getter (MultiDefn e) a
_ (EquationalModel 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 Getter DifferentialModel a
_ Getter RelationConcept a
_ Getter (ConstraintSet e) a
_ Getter (QDefinition e) a
_ Getter (MultiDefn e) a
f (EquationalRealm 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 Getter DifferentialModel a
_ Getter RelationConcept a
f Getter (ConstraintSet e) a
_ Getter (QDefinition e) a
_ Getter (MultiDefn e) a
_ (OthModel 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 :: 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 (NewDEModel DifferentialModel
q)            Setter' DifferentialModel a
f Setter' RelationConcept a
_ Setter' (ConstraintSet e) a
_ Setter' (QDefinition e) a
_ Setter' (MultiDefn e) a
_ 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 RelationConcept
q)               Setter' DifferentialModel a
_ Setter' RelationConcept a
f Setter' (ConstraintSet e) a
_ Setter' (QDefinition e) a
_ Setter' (MultiDefn e) a
_ 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 ConstraintSet e
q) Setter' DifferentialModel a
_ Setter' RelationConcept a
_ Setter' (ConstraintSet e) a
f Setter' (QDefinition e) a
_ Setter' (MultiDefn e) a
_ 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 QDefinition e
q)       Setter' DifferentialModel a
_ Setter' RelationConcept a
_ Setter' (ConstraintSet e) a
_ Setter' (QDefinition e) a
f Setter' (MultiDefn e) a
_ 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 MultiDefn e
q)       Setter' DifferentialModel a
_ Setter' RelationConcept a
_ Setter' (ConstraintSet e) a
_ Setter' (QDefinition e) a
_ Setter' (MultiDefn e) a
f 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 RelationConcept
q)              Setter' DifferentialModel a
_ Setter' RelationConcept a
f Setter' (ConstraintSet e) a
_ Setter' (QDefinition e) a
_ Setter' (MultiDefn e) a
_ 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 :: 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
ld Lens' RelationConcept a
lr Lens' (ConstraintSet e) a
lcs Lens' (QDefinition e) a
lq Lens' (MultiDefn e) a
lmd = (ModelKinds e -> a)
-> (ModelKinds e -> a -> ModelKinds e)
-> Lens (ModelKinds e) (ModelKinds e) a 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 (a -> f a) -> DifferentialModel -> f DifferentialModel
Lens' DifferentialModel a
Getter DifferentialModel a
ld (a -> f a) -> RelationConcept -> f RelationConcept
Lens' RelationConcept a
Getter RelationConcept a
lr (a -> f a) -> ConstraintSet e -> f (ConstraintSet e)
Lens' (ConstraintSet e) a
Getter (ConstraintSet e) a
lcs (a -> f a) -> QDefinition e -> f (QDefinition e)
Lens' (QDefinition e) a
Getter (QDefinition e) a
lq (a -> f a) -> MultiDefn e -> f (MultiDefn e)
Lens' (MultiDefn e) a
Getter (MultiDefn e) a
lmd
          s :: ModelKinds e -> a -> ModelKinds e
          s :: ModelKinds e -> a -> ModelKinds e
s 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_ (a -> f a) -> DifferentialModel -> f DifferentialModel
Lens' DifferentialModel a
Setter' DifferentialModel a
ld (a -> f a) -> RelationConcept -> f RelationConcept
Lens' RelationConcept a
Setter' RelationConcept a
lr (a -> f a) -> ConstraintSet e -> f (ConstraintSet e)
Lens' (ConstraintSet e) a
Setter' (ConstraintSet e) a
lcs (a -> f a) -> QDefinition e -> f (QDefinition e)
Lens' (QDefinition e) a
Setter' (QDefinition e) a
lq (a -> f a) -> MultiDefn e -> f (MultiDefn e)
Lens' (MultiDefn e) a
Setter' (MultiDefn e) a
lmd

-- | Make a 'Getter' for 'ModelKinds'.
getterMk :: forall e a.
     Getter DifferentialModel a
  -> Getter RelationConcept a
  -> Getter (ConstraintSet e) a
  -> Getter (QDefinition e) a
  -> Getter (MultiDefn e) a
  -> Getter (ModelKinds e) a
getterMk :: forall e a.
Getter DifferentialModel a
-> Getter RelationConcept a
-> Getter (ConstraintSet e) a
-> Getter (QDefinition e) a
-> Getter (MultiDefn e) a
-> Getter (ModelKinds e) a
getterMk Getter DifferentialModel a
gd Getter RelationConcept a
gr Getter (ConstraintSet e) a
gcs Getter (QDefinition e) a
gq Getter (MultiDefn e) a
gmd = (ModelKinds e -> a) -> Optic' (->) f (ModelKinds e) a
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((ModelKinds e -> a) -> Optic' (->) f (ModelKinds e) a)
-> (ModelKinds e -> a) -> Optic' (->) f (ModelKinds e) a
forall a b. (a -> b) -> a -> b
$ \ModelKinds e
modelKinds ->
    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 (a -> f a) -> DifferentialModel -> f DifferentialModel
Getter DifferentialModel a
gd (a -> f a) -> RelationConcept -> f RelationConcept
Getter RelationConcept a
gr (a -> f a) -> ConstraintSet e -> f (ConstraintSet e)
Getter (ConstraintSet e) a
gcs (a -> f a) -> QDefinition e -> f (QDefinition e)
Getter (QDefinition e) a
gq (a -> f a) -> MultiDefn e -> f (MultiDefn e)
Getter (MultiDefn e) a
gmd ModelKinds e
modelKinds

-- | Extract a list of 'QDefinition's from a list of 'ModelKinds'.
getEqModQds :: [ModelKind e] -> [QDefinition e]
getEqModQds :: forall e. [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 QDefinition e
f) UID
_ NP
_) = QDefinition e -> Maybe (QDefinition e)
forall a. a -> Maybe a
Just QDefinition e
f
    eqMod ModelKind e
_                            = Maybe (QDefinition e)
forall a. Maybe a
Nothing