{-# 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,
  -- * 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. DifferentialModel -> ModelKinds e
NewDEModel DifferentialModel
dm) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ DifferentialModel
dm forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (DifferentialModel
dm forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. RelationConcept -> ModelKinds e
DEModel RelationConcept
rc) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ RelationConcept
rc forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (RelationConcept
rc forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. ConstraintSet e -> ModelKinds e
EquationalConstraints ConstraintSet e
qs) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ ConstraintSet e
qs forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (ConstraintSet e
qs forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ QDefinition e
qd forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (QDefinition e
qd forall s a. s -> Getting a s a -> a
^. 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 :: forall e. String -> QDefinition e -> ModelKind e
equationalModelU String
u QDefinition e
qd = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (String -> UID
mkUid String
u) (QDefinition e
qd forall s a. s -> Getting a s a -> a
^. 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 :: forall e. NP -> QDefinition e -> ModelKind e
equationalModelN NP
n QDefinition e
qd = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. QDefinition e -> ModelKinds e
EquationalModel QDefinition e
qd) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ QDefinition e
qd forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c 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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (String -> UID
mkUid String
u) (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. 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 :: forall e. NP -> MultiDefn e -> ModelKind e
equationalRealmN NP
n MultiDefn e
md = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. MultiDefn e -> ModelKinds e
EquationalRealm MultiDefn e
md) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ MultiDefn e
md forall s a. s -> Getting a s a -> a
^. 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 String
u NP
n RelationConcept
rc = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (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 = forall e. ModelKinds e -> UID -> NP -> ModelKind e
MK (forall e. RelationConcept -> ModelKinds e
OthModel RelationConcept
rc) (UID -> UID
modelNs forall a b. (a -> b) -> a -> b
$ RelationConcept
rc forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) (RelationConcept
rc forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c NP
term)

-- | Finds the 'UID' of the 'ModelKinds'.
instance HasUID        (ModelKinds e) where uid :: Lens' (ModelKinds e) UID
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
uid forall c. HasUID c => Lens' c UID
uid forall c. HasUID c => Lens' c UID
uid forall c. HasUID c => Lens' c UID
uid forall c. HasUID c => Lens' c UID
uid
-- | Finds the term ('NP') of the 'ModelKinds'.
instance NamedIdea     (ModelKinds e) where term :: Lens' (ModelKinds e) NP
term    = 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
term forall c. NamedIdea c => Lens' c NP
term forall c. NamedIdea c => Lens' c NP
term forall c. NamedIdea c => Lens' c NP
term forall c. NamedIdea c => Lens' c NP
term
-- | Finds the idea of the 'ModelKinds'.
instance Idea          (ModelKinds e) where getA :: ModelKinds e -> Maybe String
getA    = 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 (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Idea c => c -> Maybe String
getA) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Idea c => c -> Maybe String
getA) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Idea c => c -> Maybe String
getA) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Idea c => c -> Maybe String
getA) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to 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    = 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
defn forall c. Definition c => Lens' c Sentence
defn forall c. Definition c => Lens' c Sentence
defn forall c. Definition c => Lens' c Sentence
defn forall c. Definition c => Lens' c Sentence
defn
-- | Finds the domain of the 'ModelKinds'.
instance ConceptDomain (ModelKinds e) where cdom :: ModelKinds e -> [UID]
cdom    = 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 (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. ConceptDomain c => c -> [UID]
cdom) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. ConceptDomain c => c -> [UID]
cdom) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. ConceptDomain c => c -> [UID]
cdom) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. ConceptDomain c => c -> [UID]
cdom) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to 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 = 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 (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Express c => c -> ModelExpr
express) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Express c => c -> ModelExpr
express) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Express c => c -> ModelExpr
express) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall c. Express c => c -> ModelExpr
express) (forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to 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)            = forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks DifferentialModel
dm
  requiredChecks (DEModel RelationConcept
_)                = forall a. Monoid a => a
mempty
  requiredChecks (EquationalConstraints ConstraintSet Expr
cs) = forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks ConstraintSet Expr
cs
  requiredChecks (EquationalModel QDefinition Expr
qd)       = forall (f :: * -> *) a. Applicative f => a -> f a
pure (QDefinition Expr
qd forall s a. s -> Getting a s a -> a
^. forall (c :: * -> *) e. DefiningExpr c => Lens' (c e) e
defnExpr, QDefinition Expr
qd forall s a. s -> Getting a s a -> a
^. forall c. HasSpace c => Getter c Space
typ)
  requiredChecks (EquationalRealm MultiDefn Expr
md)       = forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks MultiDefn Expr
md
  requiredChecks (OthModel RelationConcept
_)               = 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 :: Lens' (ModelKind e) UID
uid     = forall e. Lens' (ModelKind e) UID
mkUID
-- | Finds the term ('NP') of the 'ModelKind'.
instance NamedIdea     (ModelKind e) where term :: Lens' (ModelKind e) NP
term    = forall e. Lens' (ModelKind e) NP
mkTerm
-- | Finds the idea of the 'ModelKind'.
instance Idea          (ModelKind e) where getA :: ModelKind e -> Maybe String
getA    = forall c. Idea c => c -> Maybe String
getA forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk)
-- | Finds the definition of the 'ModelKind'.
instance Definition    (ModelKind e) where defn :: Lens' (ModelKind e) Sentence
defn    = forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds e)
mk forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Definition c => Lens' c Sentence
defn
-- | Finds the domain of the 'ModelKind'.
instance ConceptDomain (ModelKind e) where cdom :: ModelKind e -> [UID]
cdom    = forall c. ConceptDomain c => c -> [UID]
cdom forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e 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 = forall c. Express c => c -> ModelExpr
express forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e e.
Lens (ModelKind e) (ModelKind e) (ModelKinds e) (ModelKinds 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 = forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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 :: 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 forall s a. s -> Getting a s a -> 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 forall s a. s -> Getting a s a -> 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 forall s a. s -> Getting a s a -> 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 forall s a. s -> Getting a s a -> 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 forall s a. s -> Getting a s a -> 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 forall s a. s -> Getting a s a -> 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 = forall e. DifferentialModel -> ModelKinds e
NewDEModel            forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = forall e. RelationConcept -> ModelKinds e
DEModel               forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = forall e. ConstraintSet e -> ModelKinds e
EquationalConstraints forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = forall e. QDefinition e -> ModelKinds e
EquationalModel       forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = forall e. MultiDefn e -> ModelKinds e
EquationalRealm       forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = forall e. RelationConcept -> ModelKinds e
OthModel              forall a b. (a -> b) -> a -> b
$ forall s t a b. ASetter s t a b -> b -> s -> t
set 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 = 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 = 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
ld Lens' RelationConcept a
lr Lens' (ConstraintSet e) a
lcs Lens' (QDefinition e) a
lq Lens' (MultiDefn e) a
lmd
          s :: ModelKinds e -> a -> ModelKinds e
          s :: ModelKinds e -> a -> ModelKinds e
s ModelKinds e
mk_ = 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
ld Lens' RelationConcept a
lr Lens' (ConstraintSet e) a
lcs Lens' (QDefinition e) a
lq Lens' (MultiDefn e) a
lmd

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