Safe Haskell	Safe-Inferred
Language	Haskell2010

Theory.Drasil.ModelKinds

Contents

Types
Constructors
Lenses
Functions

Description

Defines types and functions for creating models.

Synopsis

data ModelKind e = MK {
- _mk :: ModelKinds e
- _mkUID :: UID
- _mkTerm :: NP
}
data ModelKinds e where
- NewDEModel :: DifferentialModel -> ModelKinds e
- DEModel :: RelationConcept -> ModelKinds e
- EquationalConstraints :: ConstraintSet e -> ModelKinds e
- EquationalModel :: QDefinition e -> ModelKinds e
- EquationalRealm :: MultiDefn e -> ModelKinds e
- OthModel :: RelationConcept -> ModelKinds e
newDEModel :: String -> NP -> DifferentialModel -> ModelKind e
deModel :: String -> NP -> RelationConcept -> ModelKind e
equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e
equationalModel :: String -> NP -> QDefinition e -> ModelKind e
equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e
othModel :: String -> NP -> RelationConcept -> ModelKind Expr
newDEModel' :: DifferentialModel -> ModelKind e
deModel' :: RelationConcept -> ModelKind e
equationalConstraints' :: ConstraintSet e -> ModelKind e
equationalModel' :: QDefinition e -> ModelKind e
equationalRealm' :: MultiDefn e -> ModelKind e
othModel' :: RelationConcept -> ModelKind e
equationalModelU :: String -> QDefinition e -> ModelKind e
equationalModelN :: NP -> QDefinition e -> ModelKind e
equationalRealmU :: String -> MultiDefn e -> ModelKind e
equationalRealmN :: NP -> MultiDefn e -> ModelKind e
setMk :: ModelKinds e -> Setter' DifferentialModel a -> Setter' RelationConcept a -> Setter' (ConstraintSet e) a -> Setter' (QDefinition e) a -> Setter' (MultiDefn e) a -> a -> ModelKinds e
elimMk :: Getter DifferentialModel a -> Getter RelationConcept a -> Getter (ConstraintSet e) a -> Getter (QDefinition e) a -> Getter (MultiDefn e) a -> 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
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
getEqModQds :: [ModelKind e] -> [QDefinition e]

Types

data ModelKind e Source #

ModelKinds carrier, used to carry commonly overwritten information from the IMsTMsGDs.

Constructors

MK
Fields _mk :: ModelKinds e _mkUID :: UID _mkTerm :: NP

Instances

Instances details

Idea (ModelKind e) Source #	Finds the idea of the `ModelKind`.
Instance details Defined in Theory.Drasil.ModelKinds Methods getA :: ModelKind e -> Maybe String #
NamedIdea (ModelKind e) Source #	Finds the term (`NP`) of the `ModelKind`.
Instance details Defined in Theory.Drasil.ModelKinds Methods term :: Lens' (ModelKind e) NP #
ConceptDomain (ModelKind e) Source #	Finds the domain of the `ModelKind`.
Instance details Defined in Theory.Drasil.ModelKinds Methods cdom :: ModelKind e -> [UID] #
Definition (ModelKind e) Source #	Finds the definition of the `ModelKind`.
Instance details Defined in Theory.Drasil.ModelKinds Methods defn :: Lens' (ModelKind e) Sentence #
Express e => Express (ModelKind e) Source #	Rewrites the underlying model using `ModelExpr`
Instance details Defined in Theory.Drasil.ModelKinds Methods express :: ModelKind e -> ModelExpr #
HasUID (ModelKind e) Source #	Finds the `UID` of the `ModelKind`.
Instance details Defined in Theory.Drasil.ModelKinds Methods uid :: Getter (ModelKind e) UID #
RequiresChecking (ModelKind Expr) Expr Space Source #	Expose all expressions that need to be type-checked for theories that need expose `Expr`s.
Instance details Defined in Theory.Drasil.ModelKinds Methods requiredChecks :: ModelKind Expr -> [(Expr, Space)] #

data ModelKinds e where Source #

Models can be of different kinds:

NewDEModels represent differential equations as DifferentialModels
DEModels represent differential equations as RelationConcepts
EquationalConstraints represent invariants that will hold in a system of equations.
EquationalModels represent quantities that are calculated via a single definition/QDefinition.
EquationalRealms represent MultiDefns; quantities that may be calculated using any one of many DefiningExprs (e.g., 'x = A = ... = Z')
FunctionalModels represent quantity-resulting function definitions.
OthModels are placeholders for models. No new OthModels should be created, they should be using one of the other kinds.

Constructors

NewDEModel :: DifferentialModel -> ModelKinds e
DEModel :: RelationConcept -> ModelKinds e
EquationalConstraints :: ConstraintSet e -> ModelKinds e
EquationalModel :: QDefinition e -> ModelKinds e
EquationalRealm :: MultiDefn e -> ModelKinds e
OthModel :: RelationConcept -> ModelKinds e

Instances

Instances details

Idea (ModelKinds e) Source #	Finds the idea of the `ModelKinds`.
Instance details Defined in Theory.Drasil.ModelKinds Methods getA :: ModelKinds e -> Maybe String #
NamedIdea (ModelKinds e) Source #	Finds the term (`NP`) of the `ModelKinds`.
Instance details Defined in Theory.Drasil.ModelKinds Methods term :: Lens' (ModelKinds e) NP #
ConceptDomain (ModelKinds e) Source #	Finds the domain of the `ModelKinds`.
Instance details Defined in Theory.Drasil.ModelKinds Methods cdom :: ModelKinds e -> [UID] #
Definition (ModelKinds e) Source #	Finds the definition of the `ModelKinds`.
Instance details Defined in Theory.Drasil.ModelKinds Methods defn :: Lens' (ModelKinds e) Sentence #
Express e => Express (ModelKinds e) Source #	Rewrites the underlying model using `ModelExpr`
Instance details Defined in Theory.Drasil.ModelKinds Methods express :: ModelKinds e -> ModelExpr #
HasUID (ModelKinds e) Source #	Finds the `UID` of the `ModelKinds`.
Instance details Defined in Theory.Drasil.ModelKinds Methods uid :: Getter (ModelKinds e) UID #
RequiresChecking (ModelKinds Expr) Expr Space Source #	Expose all expressions that need to be type-checked for theories that need expose `Expr`s.
Instance details Defined in Theory.Drasil.ModelKinds Methods requiredChecks :: ModelKinds Expr -> [(Expr, Space)] #

Constructors

newDEModel :: String -> NP -> DifferentialModel -> ModelKind e Source #

Smart constructor for NewDEModels

deModel :: String -> NP -> RelationConcept -> ModelKind e Source #

Smart constructor for DEModels

equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e Source #

Smart constructor for EquationalConstraints

equationalModel :: String -> NP -> QDefinition e -> ModelKind e Source #

Smart constructor for EquationalModels

equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e Source #

Smart constructor for EquationalRealms

othModel :: String -> NP -> RelationConcept -> ModelKind Expr Source #

Smart constructor for OthModels

newDEModel' :: DifferentialModel -> ModelKind e Source #

Smart constructor for NewDEModels, deriving UID+Term from the DifferentialModel

deModel' :: RelationConcept -> ModelKind e Source #

Smart constructor for DEModels, deriving UID+Term from the RelationConcept

equationalConstraints' :: ConstraintSet e -> ModelKind e Source #

Smart constructor for EquationalConstraints, deriving UID+Term from the ConstraintSet

equationalModel' :: QDefinition e -> ModelKind e Source #

Smart constructor for EquationalModels, deriving UID+Term from the QDefinition

equationalRealm' :: MultiDefn e -> ModelKind e Source #

Smart constructor for EquationalRealms, deriving UID+Term from the MultiDefn

othModel' :: RelationConcept -> ModelKind e Source #

Smart constructor for OthModels, deriving UID+Term from the RelationConcept

equationalModelU :: String -> QDefinition e -> ModelKind e Source #

Smart constructor for EquationalModels, deriving Term from the QDefinition

equationalModelN :: NP -> QDefinition e -> ModelKind e Source #

Smart constructor for EquationalModels, deriving UID from the QDefinition

equationalRealmU :: String -> MultiDefn e -> ModelKind e Source #

Smart constructor for EquationalRealms

equationalRealmN :: NP -> MultiDefn e -> ModelKind e Source #

Smart constructor for EquationalRealms, deriving UID from the MultiDefn

Lenses

setMk :: ModelKinds e -> Setter' DifferentialModel a -> Setter' RelationConcept a -> Setter' (ConstraintSet e) a -> Setter' (QDefinition e) a -> Setter' (MultiDefn e) a -> a -> ModelKinds e Source #

Map into internal representations of ModelKinds

elimMk :: Getter DifferentialModel a -> Getter RelationConcept a -> Getter (ConstraintSet e) a -> Getter (QDefinition e) a -> Getter (MultiDefn e) a -> ModelKinds e -> a Source #

Retrieve internal data from 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 Source #

Make a Lens 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 Source #

Make a Getter for ModelKinds.

Functions

getEqModQds :: [ModelKind e] -> [QDefinition e] Source #

Extract a list of QDefinitions from a list of ModelKinds.