Safe Haskell	Safe-Inferred
Language	Haskell2010

Theory.Drasil.MultiDefn

Contents

Types
Constructors
Functions

Description

Defines types and functions for creating mult-definitions.

Synopsis

data MultiDefn e
data DefiningExpr e
mkMultiDefn :: String -> DefinedQuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e
mkMultiDefnForQuant :: DefinedQuantityDict -> 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

Types

data MultiDefn e Source #

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

Instances

Instances details

HasUID (MultiDefn e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods uid :: Getter (MultiDefn e) UID #
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 #
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

HasUID (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods uid :: Getter (DefiningExpr e) UID #
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 #
Eq (DefiningExpr e) Source #
Instance details Defined in Theory.Drasil.MultiDefn Methods (==) :: DefiningExpr e -> DefiningExpr e -> Bool # (/=) :: DefiningExpr e -> DefiningExpr e -> Bool #

Constructors

mkMultiDefn :: String -> DefinedQuantityDict -> 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 :: DefinedQuantityDict -> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e Source #

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

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

Smart constructor for DefiningExprs.

Functions

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