Safe Haskell	Safe-Inferred
Language	Haskell2010

Theory.Drasil

Contents

Classes
Constraint Sets
Data Definitions
General Definitions
MultiDefn
ModelKinds
Instance Models
Theory Models

Description

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.

Methods

inputs :: Lens' c [(QuantityDict, Maybe (RealInterval Expr Expr))] Source #

Provides a Lens that holds a QuantityDict and maybe constraints.

Instances

Instances details

HasInputs InstanceModel Source #	Finds the inputs of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods inputs :: Lens' InstanceModel [(QuantityDict, Maybe (RealInterval Expr Expr))] Source #

class HasOutput c where Source #

Members of this class may have outputs.

Methods

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

Instances details

HasOutput DataDefinition Source #	Finds the output variable of the `DataDefinition`
Instance details Defined in Theory.Drasil.DataDefinition Methods output :: Getter DataDefinition QuantityDict Source # out_constraints :: Getter DataDefinition [RealInterval Expr Expr] Source #
HasOutput InstanceModel Source #	Finds the outputs and output constraints of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods output :: Getter InstanceModel QuantityDict Source # out_constraints :: Getter InstanceModel [RealInterval Expr Expr] Source #

Constraint Sets

data ConstraintSet e Source #

ConstraintSets are sets of invariants that always hold for underlying domains.

Instances

Instances details

Idea (ConstraintSet e) Source #	Finds the idea of the `ConstraintSet`.
Instance details Defined in Theory.Drasil.ConstraintSet Methods getA :: ConstraintSet e -> Maybe String #
NamedIdea (ConstraintSet e) Source #	Finds the term (`NP`) of the `ConstraintSet`.
Instance details Defined in Theory.Drasil.ConstraintSet Methods term :: Lens' (ConstraintSet e) NP #
ConceptDomain (ConstraintSet e) Source #	Finds the domain of the `ConstraintSet`.
Instance details Defined in Theory.Drasil.ConstraintSet Methods cdom :: ConstraintSet e -> [UID] #
Definition (ConstraintSet e) Source #	Finds the definition of the `ConstraintSet`.
Instance details Defined in Theory.Drasil.ConstraintSet Methods defn :: Lens' (ConstraintSet e) Sentence #
Express e => Express (ConstraintSet e) Source #	The complete `ModelExpr` of a ConstraintSet is the logical conjunction of all the underlying relations (e.g., `a $&& b $&& ... $&& z`).
Instance details Defined in Theory.Drasil.ConstraintSet Methods express :: ConstraintSet e -> ModelExpr #
HasUID (ConstraintSet e) Source #	Finds the `UID` of the `ConstraintSet`.
Instance details Defined in Theory.Drasil.ConstraintSet Methods uid :: Getter (ConstraintSet e) UID #
RequiresChecking (ConstraintSet Expr) Expr Space Source #	Exposes all relations and an expectation of the type of a relation (Bool)
Instance details Defined in Theory.Drasil.ConstraintSet Methods requiredChecks :: ConstraintSet Expr -> [(Expr, Space)] #

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 DecRefs), maybe a derivation, a label (ShortName), a reference address, and other notes (Sentences).

Instances

Instances details

Idea DataDefinition Source #	Finds the idea contained in the `QDefinition` used to make the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods getA :: DataDefinition -> Maybe String #
NamedIdea DataDefinition Source #	Finds the term (`NP`) of the `QDefinition` used to make the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods term :: Lens' DataDefinition NP #
DefinesQuantity DataDefinition Source #	Finds the `Quantity` defined by the `DataDefinition`
Instance details Defined in Theory.Drasil.DataDefinition Methods defLhs :: Getter DataDefinition QuantityDict #
CommonIdea DataDefinition Source #	Finds the idea of a 'DataDefinition where' (abbreviation).
Instance details Defined in Theory.Drasil.DataDefinition Methods abrv :: DataDefinition -> String #
ConceptDomain DataDefinition Source #	Finds the domain of the `QDefinition` used to make the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods cdom :: DataDefinition -> [UID] #
HasAdditionalNotes DataDefinition Source #	Finds any additional notes for the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods getNotes :: Lens' DataDefinition [Sentence] #
HasDecRef DataDefinition Source #	Finds `DecRef`s contained in the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods getDecRefs :: Lens' DataDefinition [DecRef] #
MayHaveDerivation DataDefinition Source #	Finds the derivation of the 'DataDefinition where'. May contain Nothing.
Instance details Defined in Theory.Drasil.DataDefinition Methods derivations :: Lens' DataDefinition (Maybe Derivation) #
Express DataDefinition Source #	Converts the defining expression of a 'DataDefinition where' into the model expression language.
Instance details Defined in Theory.Drasil.DataDefinition Methods express :: DataDefinition -> ModelExpr #
HasRefAddress DataDefinition Source #	Finds the reference address of a 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods getRefAdd :: DataDefinition -> LblType #
Referable DataDefinition Source #	Finds the reference address of a 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods refAdd :: DataDefinition -> String # renderRef :: DataDefinition -> LblType #
HasShortName DataDefinition Source #	Finds the `ShortName` of the 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods shortname :: DataDefinition -> ShortName #
HasUID DataDefinition Source #	Finds the `UID` of a 'DataDefinition where'.
Instance details Defined in Theory.Drasil.DataDefinition Methods uid :: Getter DataDefinition UID #
HasOutput DataDefinition Source #	Finds the output variable of the `DataDefinition`
Instance details Defined in Theory.Drasil.DataDefinition Methods output :: Getter DataDefinition QuantityDict Source # out_constraints :: Getter DataDefinition [RealInterval Expr Expr] Source #
Eq DataDefinition Source #	Equal if `UID`s are equal.
Instance details Defined in Theory.Drasil.DataDefinition Methods (==) :: DataDefinition -> DataDefinition -> Bool # (/=) :: DataDefinition -> DataDefinition -> Bool #
RequiresChecking DataDefinition Expr Space Source #	Expose all expressions that need to be type-checked.
Instance details Defined in Theory.Drasil.DataDefinition Methods requiredChecks :: DataDefinition -> [(Expr, Space)] #

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.

qdEFromDD :: DataDefinition -> Maybe SimpleQDef Source #

General Definitions

data GenDefn Source #

A general definition is a ModelKind that may have units, a derivation, references (as DecRefs), a shortname, a reference address, and notes.

Instances

Instances details

Idea GenDefn Source #	Finds the idea contained in the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods getA :: GenDefn -> Maybe String #
NamedIdea GenDefn Source #	Finds the term (`NP`) of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods term :: Lens' GenDefn NP #
MayHaveUnit GenDefn Source #	Finds the units of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods getUnit :: GenDefn -> Maybe UnitDefn #
CommonIdea GenDefn Source #	Finds the idea of a `GenDefn` (abbreviation).
Instance details Defined in Theory.Drasil.GenDefn Methods abrv :: GenDefn -> String #
ConceptDomain GenDefn Source #	Finds the domain of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods cdom :: GenDefn -> [UID] #
Definition GenDefn Source #	Finds the definition of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods defn :: Lens' GenDefn Sentence #
HasAdditionalNotes GenDefn Source #	Finds the units of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods getNotes :: Lens' GenDefn [Sentence] #
HasDecRef GenDefn Source #	Finds `DecRef`s contained in the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods getDecRefs :: Lens' GenDefn [DecRef] #
MayHaveDerivation GenDefn Source #	Finds the derivation of the `GenDefn`. May contain Nothing.
Instance details Defined in Theory.Drasil.GenDefn Methods derivations :: Lens' GenDefn (Maybe Derivation) #
Express GenDefn Source #	Converts the `GenDefn`s related expression into a `ModelExpr`.
Instance details Defined in Theory.Drasil.GenDefn Methods express :: GenDefn -> ModelExpr #
HasRefAddress GenDefn Source #	Finds the reference address of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods getRefAdd :: GenDefn -> LblType #
Referable GenDefn Source #	Finds the reference address of a `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods refAdd :: GenDefn -> String # renderRef :: GenDefn -> LblType #
HasShortName GenDefn Source #	Finds the `ShortName` of the `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods shortname :: GenDefn -> ShortName #
HasUID GenDefn Source #	Finds the `UID` of a `GenDefn`.
Instance details Defined in Theory.Drasil.GenDefn Methods uid :: Getter GenDefn UID #

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

data MultiDefn e Source #

MultiDefns are QDefinition factories, used for showing one or more ways we can define a QDefinition.

Instances

Instances details

Idea (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods getA :: MultiDefn e -> Maybe String #
NamedIdea (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods term :: Lens' (MultiDefn e) NP #
MayHaveUnit (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods getUnit :: MultiDefn e -> Maybe UnitDefn #
ConceptDomain (MultiDefn e) Source #	The concept domain of a MultiDefn is the union of the concept domains of the underlying variants.
Instance details Defined in Theory.Drasil.MultiDefn Methods cdom :: MultiDefn e -> [UID] #
Definition (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods defn :: Lens' (MultiDefn e) Sentence #
Quantity (MultiDefn e) Source #
Instance details 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`)
Instance details Defined in Theory.Drasil.MultiDefn Methods express :: MultiDefn e -> ModelExpr #
HasSpace (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods typ :: Getter (MultiDefn e) Space #
HasSymbol (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods symbol :: MultiDefn e -> Stage -> Symbol #
HasUID (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods uid :: Getter (MultiDefn e) UID #
RequiresChecking (MultiDefn Expr) Expr Space Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods requiredChecks :: MultiDefn Expr -> [(Expr, Space)] #

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

Instances details

ConceptDomain (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods cdom :: DefiningExpr e -> [UID] #
Definition (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods defn :: Lens' (DefiningExpr e) Sentence #
HasUID (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods uid :: Getter (DefiningExpr e) UID #
Eq (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods (==) :: DefiningExpr e -> DefiningExpr e -> Bool # (/=) :: DefiningExpr e -> DefiningExpr e -> Bool #

mkMultiDefn :: String -> QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e Source #

Smart constructor for MultiDefns, does nothing special at the moment. First argument is the Space to become a UID.

mkMultiDefnForQuant :: QuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e Source #

Smart constructor for MultiDefns defining UIDs using that of the QuantityDict.

mkDefiningExpr :: String -> [UID] -> Sentence -> e -> DefiningExpr e Source #

Smart constructor for DefiningExprs.

multiDefnGenQD :: MultiDefn e -> DefiningExpr e -> QDefinition e Source #

Convert MultiDefns into QDefinitions via a specific DefiningExpr.

multiDefnGenQDByUID :: MultiDefn e -> UID -> QDefinition e Source #

Convert MultiDefns into QDefinitions via a specific DefiningExpr (by UID).

ModelKinds

data ModelKind e Source #

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

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)] #

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

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

Instances details

Idea InstanceModel Source #	Finds the idea contained in the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods getA :: InstanceModel -> Maybe String #
NamedIdea InstanceModel Source #	Finds the term (`NP`) of the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods term :: Lens' InstanceModel NP #
DefinesQuantity InstanceModel Source #	Finds the `Quantity` of an `InstanceModel`
Instance details Defined in Theory.Drasil.InstanceModel Methods defLhs :: Getter InstanceModel QuantityDict #
CommonIdea InstanceModel Source #	Finds the idea of an `InstanceModel` (abbreviation).
Instance details Defined in Theory.Drasil.InstanceModel Methods abrv :: InstanceModel -> String #
ConceptDomain InstanceModel Source #	Finds the domain of the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods cdom :: InstanceModel -> [UID] #
Definition InstanceModel Source #	Finds the definition of the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods defn :: Lens' InstanceModel Sentence #
HasAdditionalNotes InstanceModel Source #	Finds any additional notes for the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods getNotes :: Lens' InstanceModel [Sentence] #
HasDecRef InstanceModel Source #	Finds `DecRef`s contained in the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods getDecRefs :: Lens' InstanceModel [DecRef] #
MayHaveDerivation InstanceModel Source #	Finds the derivation of the `InstanceModel`. May contain Nothing.
Instance details Defined in Theory.Drasil.InstanceModel Methods derivations :: Lens' InstanceModel (Maybe Derivation) #
Express InstanceModel Source #	Converts the `InstanceModel`s related expression into the display language.
Instance details Defined in Theory.Drasil.InstanceModel Methods express :: InstanceModel -> ModelExpr #
HasRefAddress InstanceModel Source #	Finds the reference address of the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods getRefAdd :: InstanceModel -> LblType #
Referable InstanceModel Source #	Finds the reference address of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods refAdd :: InstanceModel -> String # renderRef :: InstanceModel -> LblType #
HasShortName InstanceModel Source #	Finds the `ShortName` of the `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods shortname :: InstanceModel -> ShortName #
HasUID InstanceModel Source #	Finds the `UID` of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods uid :: Getter InstanceModel UID #
HasInputs InstanceModel Source #	Finds the inputs of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods inputs :: Lens' InstanceModel [(QuantityDict, Maybe (RealInterval Expr Expr))] Source #
HasOutput InstanceModel Source #	Finds the outputs and output constraints of an `InstanceModel`.
Instance details Defined in Theory.Drasil.InstanceModel Methods output :: Getter InstanceModel QuantityDict Source # out_constraints :: Getter InstanceModel [RealInterval Expr Expr] Source #
RequiresChecking InstanceModel Expr Space Source #	Expose all expressions that need to be type-checked.
Instance details Defined in Theory.Drasil.InstanceModel Methods requiredChecks :: InstanceModel -> [(Expr, Space)] #

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 QDefinitions from a list of instance models.

Theory Models

class Theory t where Source #

Theories are the basis for building models with context, spaces, quantities, operations, invariants, etc.

Methods

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

Instances details

Theory TheoryModel Source #

Finds the aspects of the Theory behind the TheoryModel.

Instance details

Defined in Theory.Drasil.Theory

Methods

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 (TheoryModels),
spc - type definitions (SpaceDefns),
quan - quantities (QuantityDicts),
ops - operations (ConceptChunks),
defq - definitions (QDefinitions),
invs - invariants (ModelExprs),
dfun - defined functions (QDefinitions),
ref - accompanying references (DecRefs),
lb - a label (SpaceDefn),
ra - reference address (SpaceDefn),
notes - additional notes (Sentences).

Right now, neither the definition context (vctx) nor the spaces (spc) are ever defined.

Instances

Instances details

Idea TheoryModel Source #	Finds the idea of the `ConceptChunk` contained in the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods getA :: TheoryModel -> Maybe String #
NamedIdea TheoryModel Source #	Finds the term (`NP`) of the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods term :: Lens' TheoryModel NP #
CommonIdea TheoryModel Source #	Finds the idea of a `TheoryModel` (abbreviation).
Instance details Defined in Theory.Drasil.Theory Methods abrv :: TheoryModel -> String #
ConceptDomain TheoryModel Source #	Finds the domain of the `ConceptChunk` contained in a `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods cdom :: TheoryModel -> [UID] #
Definition TheoryModel Source #	Finds the definition of the `ConceptChunk` contained in a `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods defn :: Lens' TheoryModel Sentence #
HasAdditionalNotes TheoryModel Source #	Finds any additional notes for the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods getNotes :: Lens' TheoryModel [Sentence] #
HasDecRef TheoryModel Source #	Finds `DecRef`s contained in the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods getDecRefs :: Lens' TheoryModel [DecRef] #
HasRefAddress TheoryModel Source #	Finds the reference address of the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods getRefAdd :: TheoryModel -> LblType #
Referable TheoryModel Source #	Finds the reference address of a `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods refAdd :: TheoryModel -> String # renderRef :: TheoryModel -> LblType #
HasShortName TheoryModel Source #	Finds the `ShortName` of the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods shortname :: TheoryModel -> ShortName #
HasUID TheoryModel Source #	Finds the `UID` of a `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods uid :: Getter TheoryModel UID #
Theory TheoryModel Source #	Finds the aspects of the `Theory` behind the `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods 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 #

tm :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr -> [q] -> [c] -> [ModelQDef] -> [ModelExpr] -> [ModelQDef] -> [DecRef] -> String -> [Sentence] -> TheoryModel Source #

Constructor for theory models. Must have a source. Uses the shortname of the reference address.

tmNoRefs :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr -> [q] -> [c] -> [ModelQDef] -> [ModelExpr] -> [ModelQDef] -> String -> [Sentence] -> TheoryModel Source #

Constructor for theory models. Uses the shortname of the reference address.