drasil-theory-0.1.0.0: A framework for code and document generation for scientific software - Theory SubPackage
Safe HaskellSafe-Inferred
LanguageHaskell2010

Theory.Drasil

Description

Re-export many things to simplify external use.

Synopsis

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

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

HasOutput InstanceModel Source #

Finds the outputs and output constraints of an InstanceModel.

Instance details

Defined in Theory.Drasil.InstanceModel

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

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

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

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

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

CommonIdea DataDefinition Source #

Finds the idea of a 'DataDefinition where' (abbreviation).

Instance details

Defined in Theory.Drasil.DataDefinition

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

Express DataDefinition Source #

Converts the defining expression of a 'DataDefinition where' into the model expression language.

Instance details

Defined in Theory.Drasil.DataDefinition

HasRefAddress DataDefinition Source #

Finds the reference address of a 'DataDefinition where'.

Instance details

Defined in Theory.Drasil.DataDefinition

Referable DataDefinition Source #

Finds the reference address of a 'DataDefinition where'.

Instance details

Defined in Theory.Drasil.DataDefinition

HasShortName DataDefinition Source #

Finds the ShortName of the 'DataDefinition where'.

Instance details

Defined in Theory.Drasil.DataDefinition

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

Eq DataDefinition Source #

Equal if UIDs are equal.

Instance details

Defined in Theory.Drasil.DataDefinition

RequiresChecking DataDefinition Expr Space Source #

Expose all expressions that need to be type-checked.

Instance details

Defined in Theory.Drasil.DataDefinition

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

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

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

Express GenDefn Source #

Converts the GenDefns 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

HasShortName GenDefn Source #

Finds the ShortName of the GenDefn.

Instance details

Defined in Theory.Drasil.GenDefn

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

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

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

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.

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

Instance details

Defined in Theory.Drasil.ModelKinds

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

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

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

Express InstanceModel Source #

Converts the InstanceModels related expression into the display language.

Instance details

Defined in Theory.Drasil.InstanceModel

HasRefAddress InstanceModel Source #

Finds the reference address of the InstanceModel.

Instance details

Defined in Theory.Drasil.InstanceModel

Referable InstanceModel Source #

Finds the reference address of an InstanceModel.

Instance details

Defined in Theory.Drasil.InstanceModel

HasShortName InstanceModel Source #

Finds the ShortName of the InstanceModel.

Instance details

Defined in Theory.Drasil.InstanceModel

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

HasOutput InstanceModel Source #

Finds the outputs and output constraints of an InstanceModel.

Instance details

Defined in Theory.Drasil.InstanceModel

RequiresChecking InstanceModel Expr Space Source #

Expose all expressions that need to be type-checked.

Instance details

Defined in Theory.Drasil.InstanceModel

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

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

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

Referable TheoryModel Source #

Finds the reference address of a TheoryModel.

Instance details

Defined in Theory.Drasil.Theory

HasShortName TheoryModel Source #

Finds the ShortName of the TheoryModel.

Instance details

Defined in Theory.Drasil.Theory

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

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.