Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Re-export many things to simplify external use.
Synopsis
- class HasInputs c where
- inputs :: Lens' c [(QuantityDict, Maybe (RealInterval Expr Expr))]
- class HasOutput c where
- output :: Getter c QuantityDict
- out_constraints :: Getter c [RealInterval Expr Expr]
- data ConstraintSet e
- mkConstraintSet :: ConceptChunk -> NonEmpty e -> ConstraintSet e
- data DataDefinition
- ddE :: SimpleQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
- ddENoRefs :: SimpleQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
- ddME :: ModelQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
- ddMENoRefs :: ModelQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
- qdFromDD :: DataDefinition -> Either SimpleQDef ModelQDef
- qdEFromDD :: DataDefinition -> Maybe SimpleQDef
- data GenDefn
- gd :: IsUnit u => ModelKind ModelExpr -> Maybe u -> Maybe Derivation -> [DecRef] -> String -> [Sentence] -> GenDefn
- gdNoRefs :: IsUnit u => ModelKind ModelExpr -> Maybe u -> Maybe Derivation -> String -> [Sentence] -> GenDefn
- getEqModQdsFromGd :: [GenDefn] -> [ModelQDef]
- data MultiDefn e
- data DefiningExpr e
- mkMultiDefn :: String -> QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e
- mkMultiDefnForQuant :: QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e
- mkDefiningExpr :: String -> [UID] -> Sentence -> e -> DefiningExpr e
- multiDefnGenQD :: MultiDefn e -> DefiningExpr e -> QDefinition e
- multiDefnGenQDByUID :: MultiDefn e -> UID -> QDefinition e
- data ModelKind 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
- data InstanceModel
- im :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> InstanceModel
- imNoDeriv :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> [DecRef] -> String -> [Sentence] -> InstanceModel
- imNoRefs :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> Maybe Derivation -> String -> [Sentence] -> InstanceModel
- imNoDerivNoRefs :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> String -> [Sentence] -> InstanceModel
- qwUC :: (Quantity q, MayHaveUnit q) => q -> Input
- qwC :: (Quantity q, MayHaveUnit q) => q -> RealInterval Expr Expr -> Input
- getEqModQdsFromIm :: [InstanceModel] -> [SimpleQDef]
- class Theory t where
- valid_context :: Lens' t [TheoryModel]
- spaces :: Lens' t [SpaceDefn]
- quantities :: Lens' t [QuantityDict]
- operations :: Lens' t [ConceptChunk]
- defined_quant :: Lens' t [ModelQDef]
- invariants :: Lens' t [ModelExpr]
- defined_fun :: Lens' t [ModelQDef]
- data TheoryModel
- tm :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr -> [q] -> [c] -> [ModelQDef] -> [ModelExpr] -> [ModelQDef] -> [DecRef] -> String -> [Sentence] -> TheoryModel
- tmNoRefs :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr -> [q] -> [c] -> [ModelQDef] -> [ModelExpr] -> [ModelQDef] -> String -> [Sentence] -> TheoryModel
Classes
class HasInputs c where Source #
Members of this class may have inputs.
inputs :: Lens' c [(QuantityDict, Maybe (RealInterval Expr Expr))] Source #
Provides a Lens
that holds a QuantityDict
and maybe constraints.
Instances
HasInputs InstanceModel Source # | Finds the inputs of an |
Defined in Theory.Drasil.InstanceModel inputs :: Lens' InstanceModel [(QuantityDict, Maybe (RealInterval Expr Expr))] Source # |
class HasOutput c where Source #
Members of this class may have outputs.
output :: Getter c QuantityDict Source #
Provides a Getter
that holds a QuantityDict
for output.
out_constraints :: Getter c [RealInterval Expr Expr] Source #
Provides a Getter
that holds constraints on the output.
Instances
HasOutput DataDefinition Source # | Finds the output variable of the |
Defined in Theory.Drasil.DataDefinition output :: Getter DataDefinition QuantityDict Source # out_constraints :: Getter DataDefinition [RealInterval Expr Expr] Source # | |
HasOutput InstanceModel Source # | Finds the outputs and output constraints of an |
Defined in Theory.Drasil.InstanceModel output :: Getter InstanceModel QuantityDict Source # out_constraints :: Getter InstanceModel [RealInterval Expr Expr] Source # |
Constraint Sets
data ConstraintSet e Source #
ConstraintSet
s are sets of invariants that always hold for underlying domains.
Instances
mkConstraintSet :: ConceptChunk -> NonEmpty e -> ConstraintSet e Source #
Smart constructor for building ConstraintSets
Data Definitions
data DataDefinition Source #
A data definition is a QDefinition
that may have additional notes:
the scope, any references (as DecRef
s), maybe a derivation, a label (ShortName
), a reference address, and other notes (Sentence
s).
Instances
ddE :: SimpleQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition Source #
Smart constructor for data definitions.
ddENoRefs :: SimpleQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition Source #
Smart constructor for data definitions with no references.
ddME :: ModelQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition Source #
Smart constructor for data definitions.
ddMENoRefs :: ModelQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition Source #
Smart constructor for data definitions with no references.
qdFromDD :: DataDefinition -> Either SimpleQDef ModelQDef Source #
Extracts the 'QDefinition e' from a DataDefinition
.
General Definitions
A general definition is a ModelKind
that may have units, a derivation,
references (as DecRef
s), a shortname, a reference address, and notes.
Instances
gd :: IsUnit u => ModelKind ModelExpr -> Maybe u -> Maybe Derivation -> [DecRef] -> String -> [Sentence] -> GenDefn Source #
Smart constructor for general definitions.
gdNoRefs :: IsUnit u => ModelKind ModelExpr -> Maybe u -> Maybe Derivation -> String -> [Sentence] -> GenDefn Source #
Smart constructor for general definitions with no references.
getEqModQdsFromGd :: [GenDefn] -> [ModelQDef] Source #
Grab all related QDefinitions
from a list of general definitions.
MultiDefn
MultiDefn
s are QDefinition factories, used for showing one or more ways
we can define a QDefinition.
Instances
Idea (MultiDefn e) Source # | |
NamedIdea (MultiDefn e) Source # | |
Defined in Theory.Drasil.MultiDefn | |
MayHaveUnit (MultiDefn e) Source # | |
ConceptDomain (MultiDefn e) Source # | The concept domain of a MultiDefn is the union of the concept domains of the underlying variants. |
Defined in Theory.Drasil.MultiDefn | |
Definition (MultiDefn e) Source # | |
Defined in Theory.Drasil.MultiDefn | |
Quantity (MultiDefn e) Source # | |
Defined in Theory.Drasil.MultiDefn | |
Express e => Express (MultiDefn e) Source # | The complete Relation of a MultiDefn is defined as the quantity and the related expressions being equal (e.g., `q $= a $= b $= ... $= z`) |
Defined in Theory.Drasil.MultiDefn | |
HasSpace (MultiDefn e) Source # | |
Defined in Theory.Drasil.MultiDefn | |
HasSymbol (MultiDefn e) Source # | |
HasUID (MultiDefn e) Source # | |
Defined in Theory.Drasil.MultiDefn | |
RequiresChecking (MultiDefn Expr) Expr Space Source # | |
Defined in Theory.Drasil.MultiDefn |
data DefiningExpr e Source #
DefiningExpr
are the data that make up a (quantity) definition, namely
the description, the defining (rhs) expression and the context domain(s).
These are meant to be alternate
but equivalent definitions for a single
concept.
Instances
ConceptDomain (DefiningExpr e) Source # | |
Defined in Theory.Drasil.MultiDefn cdom :: DefiningExpr e -> [UID] # | |
Definition (DefiningExpr e) Source # | |
Defined in Theory.Drasil.MultiDefn defn :: Lens' (DefiningExpr e) Sentence # | |
HasUID (DefiningExpr e) Source # | |
Defined in Theory.Drasil.MultiDefn uid :: Lens' (DefiningExpr e) UID # | |
Eq (DefiningExpr e) Source # | |
Defined in Theory.Drasil.MultiDefn (==) :: DefiningExpr e -> DefiningExpr e -> Bool # (/=) :: DefiningExpr e -> DefiningExpr e -> Bool # |
mkMultiDefn :: String -> QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e Source #
mkMultiDefnForQuant :: QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e Source #
Smart constructor for MultiDefn
s defining UID
s using that of the QuantityDict
.
mkDefiningExpr :: String -> [UID] -> Sentence -> e -> DefiningExpr e Source #
Smart constructor for DefiningExpr
s.
multiDefnGenQD :: MultiDefn e -> DefiningExpr e -> QDefinition e Source #
Convert MultiDefn
s into QDefinition
s via a specific DefiningExpr
.
multiDefnGenQDByUID :: MultiDefn e -> UID -> QDefinition e Source #
Convert MultiDefn
s into QDefinition
s via a specific DefiningExpr
(by UID
).
ModelKinds
ModelKinds
carrier, used to carry commonly overwritten information from
the IMsTMsGDs.
Instances
Idea (ModelKind e) Source # | Finds the idea of the |
NamedIdea (ModelKind e) Source # | |
Defined in Theory.Drasil.ModelKinds | |
ConceptDomain (ModelKind e) Source # | Finds the domain of the |
Defined in Theory.Drasil.ModelKinds | |
Definition (ModelKind e) Source # | Finds the definition of the |
Defined in Theory.Drasil.ModelKinds | |
Express e => Express (ModelKind e) Source # | Rewrites the underlying model using |
Defined in Theory.Drasil.ModelKinds | |
HasUID (ModelKind e) Source # | |
Defined in Theory.Drasil.ModelKinds | |
RequiresChecking (ModelKind Expr) Expr Space Source # | Expose all expressions that need to be type-checked for theories that need
expose |
Defined in Theory.Drasil.ModelKinds |
newDEModel :: String -> NP -> DifferentialModel -> ModelKind e Source #
Smart constructor for NewDEModel
s
equationalConstraints :: String -> NP -> ConstraintSet e -> ModelKind e Source #
Smart constructor for EquationalConstraints
equationalModel :: String -> NP -> QDefinition e -> ModelKind e Source #
Smart constructor for EquationalModel
s
equationalRealm :: String -> NP -> MultiDefn e -> ModelKind e Source #
Smart constructor for EquationalRealm
s
othModel :: String -> NP -> RelationConcept -> ModelKind Expr Source #
Smart constructor for OthModel
s
newDEModel' :: DifferentialModel -> ModelKind e Source #
Smart constructor for NewDEModel
s, deriving UID+Term from the DifferentialModel
deModel' :: RelationConcept -> ModelKind e Source #
Smart constructor for DEModel
s, 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 EquationalModel
s, deriving UID+Term from the QDefinition
equationalRealm' :: MultiDefn e -> ModelKind e Source #
Smart constructor for EquationalRealm
s, deriving UID+Term from the MultiDefn
othModel' :: RelationConcept -> ModelKind e Source #
Smart constructor for OthModel
s, deriving UID+Term from the RelationConcept
equationalModelU :: String -> QDefinition e -> ModelKind e Source #
Smart constructor for EquationalModel
s, deriving Term from the QDefinition
equationalModelN :: NP -> QDefinition e -> ModelKind e Source #
Smart constructor for EquationalModel
s, deriving UID from the QDefinition
equationalRealmU :: String -> MultiDefn e -> ModelKind e Source #
Smart constructor for EquationalRealm
s
equationalRealmN :: NP -> MultiDefn e -> ModelKind e Source #
Smart constructor for EquationalRealm
s, deriving UID from the MultiDefn
Instance Models
data InstanceModel Source #
An instance model is a ModelKind that may have specific inputs, outputs,
and output constraints. It also has attributes like references, derivation,
labels (ShortName
), reference address, and notes.
Instances
im :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> InstanceModel Source #
Smart constructor for instance models with everything defined.
imNoDeriv :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> [DecRef] -> String -> [Sentence] -> InstanceModel Source #
Smart constructor for instance models with a custom term, and no derivation.
imNoRefs :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> Maybe Derivation -> String -> [Sentence] -> InstanceModel Source #
Smart constructor for instance models with a custom term, and no references.
imNoDerivNoRefs :: ModelKind Expr -> Inputs -> Output -> OutputConstraints -> String -> [Sentence] -> InstanceModel Source #
Smart constructor for instance models with a custom term, and no derivations or references.
qwUC :: (Quantity q, MayHaveUnit q) => q -> Input Source #
For building a quantity with no constraint.
qwC :: (Quantity q, MayHaveUnit q) => q -> RealInterval Expr Expr -> Input Source #
For building a quantity with a constraint.
getEqModQdsFromIm :: [InstanceModel] -> [SimpleQDef] Source #
Grab all related QDefinition
s from a list of instance models.
Theory Models
Theories are the basis for building models with context, spaces, quantities, operations, invariants, etc.
valid_context :: Lens' t [TheoryModel] Source #
spaces :: Lens' t [SpaceDefn] Source #
quantities :: Lens' t [QuantityDict] Source #
operations :: Lens' t [ConceptChunk] Source #
defined_quant :: Lens' t [ModelQDef] Source #
invariants :: Lens' t [ModelExpr] Source #
defined_fun :: Lens' t [ModelQDef] Source #
Instances
Theory TheoryModel Source # | Finds the aspects of the |
Defined in Theory.Drasil.Theory valid_context :: Lens' TheoryModel [TheoryModel] Source # spaces :: Lens' TheoryModel [SpaceDefn] Source # quantities :: Lens' TheoryModel [QuantityDict] Source # operations :: Lens' TheoryModel [ConceptChunk] Source # defined_quant :: Lens' TheoryModel [ModelQDef] Source # invariants :: Lens' TheoryModel [ModelExpr] Source # defined_fun :: Lens' TheoryModel [ModelQDef] Source # |
data TheoryModel Source #
A TheoryModel is a collection of:
- tUid - a UID,
- con - a ConceptChunk,
- vctx - definition context (
TheoryModel
s), - spc - type definitions (
SpaceDefn
s), - quan - quantities (
QuantityDict
s), - ops - operations (
ConceptChunk
s), - defq - definitions (
QDefinition
s), - invs - invariants (
ModelExpr
s), - dfun - defined functions (
QDefinition
s), - ref - accompanying references (
DecRef
s), - lb - a label (
SpaceDefn
), - ra - reference address (
SpaceDefn
), - notes - additional notes (
Sentence
s).
Right now, neither the definition context (vctx) nor the spaces (spc) are ever defined.