{-# 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 Language.Drasil (NamedIdea(..), NP, QDefinition, HasUID(..), Expr,
  RelationConcept, ConceptDomain(..), Definition(..), Idea(..), Express(..),
  UID, DifferentialModel, mkUid, nsUid, RequiresChecking(..), Space,
  HasSpace(typ), DefiningExpr(..))
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
  -- 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"

-- | 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