Safe Haskell	Safe-Inferred
Language	Haskell2010

Theory.Drasil.Theory

Contents

Types
Constructors

Description

Defines types and functions for Theoretical Models.

Synopsis

data TheoryModel
tm :: ModelKind ModelExpr -> [DecRef] -> String -> [Sentence] -> TheoryModel
tmNoRefs :: ModelKind ModelExpr -> String -> [Sentence] -> TheoryModel

Types

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 (DefinedQuantityDicts),
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

HasChunkRefs TheoryModel Source #
Instance details Defined in Theory.Drasil.Theory Methods chunkRefs :: TheoryModel -> Set UID #
HasUID TheoryModel Source #	Finds the `UID` of a `TheoryModel`.
Instance details Defined in Theory.Drasil.Theory Methods uid :: Getter TheoryModel UID #
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 (`Sentence`) 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] #
Express TheoryModel Source #
Instance details Defined in Theory.Drasil.Theory Methods express :: TheoryModel -> ModelExpr # mexpress :: TheoryModel -> NonEmpty ModelExpr #
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 #

Constructors

tm :: ModelKind ModelExpr -> [DecRef] -> String -> [Sentence] -> TheoryModel Source #

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

tmNoRefs :: ModelKind ModelExpr -> String -> [Sentence] -> TheoryModel Source #

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