package objects
MMT objects are
- Terms
- Contexts, which are lists of VarDecl
- Substitutions, which are lists of Sub
AnonymousDiagram, AnonymousTheory, and AnonymousMorphism represent anonymous counterparts to libraries.Library modules.Module}.
This package also contains various auxiliary classes: - Position defines paths within objects - SubstitutionApplier is the main interface for substitution strategies. - Matcher is a simple matcher.
- Source
- package.scala
- Alphabetic
- By Inheritance
- objects
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
trait
AnonymousBody extends ElementContainer[OML] with DefaultLookup[OML] with ShortURIPrinter
auxiliary class for storing lists of declarations statefully without giving it a global name
auxiliary class for storing lists of declarations statefully without giving it a global name
anonymous modules are object that can be converted into these helper classes using the objects AnonymousTheory and AnonymousMorphism
-
case class
AnonymousDiagram(nodes: List[DiagramNode], arrows: List[DiagramArrow], distNode: Option[LocalName]) extends Product with Serializable
a diagram in the category of theories and morphisms
a diagram in the category of theories and morphisms
- nodes
the nodes
- arrows
the arrows
- distNode
the label of a distinguished node to be used if this diagram is used like a theory invariant: codomain of distArrow is distNode
-
case class
AnonymousMorphism(decls: List[OML]) extends AnonymousBody with Product with Serializable
a morphism given by domain, codomain, and body
-
case class
AnonymousTheory(mt: Option[MPath], decls: List[OML]) extends AnonymousBody with Product with Serializable
a theory given by meta-theory and body
-
case class
Appendage(head: GlobalName, extremities: List[Term]) extends Product with Serializable
see TorsoForm for explanation on the intended use
-
abstract
class
BinaryObjJudgement extends Judgement
Common code for some binary judgements
-
class
CongruenceClosure extends AnyRef
reduces an equality to a list of equalities by applying congruence and alpha-renaming
reduces an equality to a list of equalities by applying congruence and alpha-renaming
no context-specific reasoning or simplification is applied always succeeds (returns List(eq) at worst)
-
case class
Context(variables: VarDecl*) extends Obj with ElementContainer[VarDecl] with DefaultLookup[VarDecl] with Product with Serializable
An MMT context as a list of variable declarations VarDecl.
An MMT context as a list of variable declarations VarDecl.
Being a list especially implies that there is an **order of the entries**. For example, this is important when using the Context in an OMBINDC to represent a lambda term: (λxy. x + y) will be represented as OMBINDC whose context has VarDecl entries "x", "y" in that order.
Another situation where order is important is when later VarDecl declarations refer to previous ones.Note that
variablesis not necessarily meant in a strict sense of only variables, namely a context can also include declarations of a whole theory and all of its (transitively) included theories by use of IncludeVarDecl. There is an helper apply method on the companion object of Context:scala Context(MPath(/* ... */))- variables
The context's variables
- class DerivedOMLFeature extends AnyRef
-
class
DerivedVarDeclFeature extends AnyRef
use this to create apply/unapply functions for variable declarations for a specific feature
-
case class
DiagramArrow(label: LocalName, from: LocalName, to: LocalName, morphism: AnonymousMorphism, isImplicit: Boolean) extends DiagramElement with Product with Serializable
an arrow in an AnonymousDiagram
an arrow in an AnonymousDiagram
- label
the label of this arrow
- from
the label of the domain node in the same diagram
- to
the label of the codomain node in the same diagram
- morphism
the morphism attached to this arrow (the same theory may be attached to multiple nodes)
-
sealed abstract
class
DiagramElement extends ShortURIPrinter
used in AnonymousDiagram
-
case class
DiagramNode(label: LocalName, theory: AnonymousTheory) extends DiagramElement with Product with Serializable
a node in an AnonymousDiagram
a node in an AnonymousDiagram
- label
the label of this node
- theory
the theory attached to this node (the same theory may be attached to multiple nodes)
-
case class
DomainElement(name: LocalName, defined: Boolean, subdomain: Option[(Term, List[LocalName])]) extends Product with Serializable
an auxiliary class to store domains of Contexts and theory expressions (see TheoryExp)
an auxiliary class to store domains of Contexts and theory expressions (see TheoryExp)
if parameter name is an import, subdomain is the imported theory and (if not defined as in symbols.DeclaredStructure and StructureVarDecl) the instantiated names of the partial morphism
- name
the name
- defined
true if name has a definiens (including total morphisms in symbols.DefinedStructure and StructureVarDecl)
- subdomain
see above
-
case class
Equality(stack: Stack, tm1: Term, tm2: Term, tpOpt: Option[Term]) extends Judgement with Product with Serializable
represents an equality judgement, optionally at a type context |- t1 = t2 : tp if t = Some(tp) or context |- t1 = t2 if t = None
-
case class
EqualityContext(stack: Stack, context1: Context, context2: Context, uptoAlpha: Boolean) extends Judgement with Product with Serializable
represents an equality judgement between contexts context |- context1 = context2
- case class Formal(obj: Term) extends SemiFormalObject with Product with Serializable
-
case class
Inhabitable(stack: Stack, wfo: Term) extends UnaryObjJudgement with WFJudgement with Product with Serializable
A term wfo is inhabitable if it can occur on the right side of a Typing judgement.
A term wfo is inhabitable if it can occur on the right side of a Typing judgement. Such terms can be used as the types of constants and variables.
-
case class
Inhabited(stack: Stack, tp: Term) extends UnaryObjJudgement with Product with Serializable
A term tp is inhabited if it occurs on the right side of a Typing judgement.
A term tp is inhabited if it occurs on the right side of a Typing judgement. Via Curry-Howard, such terms can be thought of as provable propositions. Therefore, this judgement is usually undecidable.
-
case class
IsContext(stack: Stack, wfo: Context) extends UnaryObjJudgement with WFJudgement with Product with Serializable
well-formedness of contexts
-
abstract
class
Judgement extends HashEquality[Judgement] with HistoryEntry
the type of object level judgments as used for typing and equality of terms
-
sealed abstract
class
MatchResult extends AnyRef
returned by the Matcher
-
final
case class
MatchSuccess(solution: Substitution, total: Boolean) extends MatchResult with Product with Serializable
- solution
the substitution for the query (template) variables
- total
true if all query variables were solved; if false, the terms are equal for any value of the unsolved variables
-
class
Matcher extends Logger
Matches a goal term against a template term.
Matches a goal term against a template term.
- Input: terms template and goal
- Output: substitution solution such that
template ^ solution == goal, where Term.^ is the method applying the substitution.
Full code example see below.
In normed vector spaces you might have the template term
||x - y||and would like to match the goal term||(a - b) - c||with it.
The matcher will give you the substitutionsolution = [x := (a - b), y := c]. This is a special case of (typed!) unification. In general, unification seeks a solution substitution such thattemplate solution == goal solution, i.e. the substitution applied on *both* sides. Thus the template usually contains variables intended for substitution ("matching"), but the goal does not. Still, the goal term may contain free variables as in the example above, they will then be part of the solution substitution - but only in the RHS of the substitutions. No equality relation is taken into account except alpha-conversion of bound variables and solution rules. , scala // Construct the goal and template terms // val namespace = DPath(URI("http://example.com")) val module = namespace ? "myModule" val norm = OMID(module ? "norm") val minus = OMID(module ? "minus") // "||(x - y) - z||" val goal = OMA( norm, List( OMA( minus, List( OMA(minus, List(OMV("x"), OMV("y"))), OMV("z") ) ) ) ) // "||a - b||" val template = OMA( norm, List(OMA( minus, List(OMV("a"), OMV("b")) )) ) // Empty rule set because we don't use any logic foundation // specific typing rules (e.g. the rule in LF for function // application) val matcher = new Matcher(ctrl, new MutableRuleSet) val matchResult = matcher( Context(VarDecl(LocalName("x"), LocalName("y"), LocalName("z"))), goal, Context(VarDecl(LocalName("a"), LocalName("b"))), template ) // MatchSuccess(a:=(http://example.com?myModule?minus x y), b:=z,true)- Note
The class can be reused for multiple matches using the same RuleSet but is not thread-safe.
,Beware of situations where the template and goal term share some variables. E.g. take template term = "a", goal term = "a - a". Intuitively, this should be a match with the substitution [a := a - a], but this class cannot handle this. The following code will lead to a MatchFail:
scala val matchResult = matcher( Context(VarDecl(LocalName("a"))), OMA(minus, List(OMV("a"), OMV("a"))), Context(VarDecl(LocalName("a"))), OMV("a") )scala val matchResult = matcher( Context(VarDecl(LocalName("a"))), OMA(minus, List(OMV("a"), OMV("a"))), Context(VarDecl(LocalName("b"))), OMV("b") ) // MatchSuccess(b:=(http://example.com?myModule?minus a a),true) println(matchResult)
Examples: - Input: terms template and goal
-
class
MemoizedSubstitutionApplier extends SubstitutionApplier
Like SmartSubstitutionApplier, but remembers previous applications.
-
case class
OMA(fun: Term, args: List[Term]) extends Term with Product with Serializable
An OMA represents an application of a term to a list of terms
An OMA represents an application of a term to a list of terms
- fun
the function term
- args
the list of argument terms (may be Nil)
-
case class
OMATTR(arg: Term, key: OMID, value: Term) extends Term with Product with Serializable
An OMATTR represents an attributed term.
An OMATTR represents an attributed term.
- arg
the term without attribution
- key
the key (This must be an OMS in OpenMath.)
- value
the value
-
case class
OMBINDC(binder: Term, context: Context, scopes: List[Term]) extends Term with Product with Serializable
An OMBINDC represents a binding with arbitrarily many scopes
An OMBINDC represents a binding with arbitrarily many scopes
- binder
the binder
- context
the bound variables (from outside to inside)
- scopes
the scopes/bodies/matrices of the binder (usually exactly 1)
-
case class
OMFOREIGN(node: Node) extends Term with Product with Serializable
An OMFOREIGN represents an OpenMath foreign object.
An OMFOREIGN represents an OpenMath foreign object.
- node
the XML element holding the foreign object
-
case class
OMID(path: ContentPath) extends Term with Product with Serializable
An OMID represents an MMT reference
-
case class
OML(name: LocalName, tp: Option[Term], df: Option[Term], nt: Option[TextNotation] = None, featureOpt: Option[String] = None) extends Term with NamedElement with Product with Serializable
local declarations with type and/or definiens, with scope, but not subject to alpha-renaming and substitution
local declarations with type and/or definiens, with scope, but not subject to alpha-renaming and substitution
These could be used for the typed/defined fields in a record type/value or the selection function.
-
case class
OMLIT(value: Any, rt: RealizedType) extends Term with OMLITTrait with Product with Serializable
A literal consists of a RealizedType rt and a value of SemanticType rt.semType.
A literal consists of a RealizedType rt and a value of SemanticType rt.semType.
Literals can be constructed conveniently using RealizedType.apply
invariant for structurally well-formed literals: the value is valid and normal, i.e, rt.semType.valid(value) and rt.semType.normalform(value) == value
-
sealed
trait
OMLITTrait extends Term
The joint methods of OMLIT and UnknownOMLIT
-
case class
OMV(name: LocalName) extends Term with Product with Serializable
An OMV represents a reference to a variable.
An OMV represents a reference to a variable.
- name
the name of the referenced variable
-
abstract
class
Obj extends Content with BaseType with ShortURIPrinter with HashEquality[Obj]
An Obj represents an MMT object.
An Obj represents an MMT object. MMT objects are represented by immutable Scala objects.
-
case class
Position(indices: List[Int]) extends Product with Serializable
A path in the syntax tree of an object
- trait SemiFormalObject extends Content
- trait SemiFormalObjectList extends AnyRef
- trait ShortURIPrinter extends AnyRef
- case class Stack(context: Context) extends Product with Serializable
-
abstract
class
StatelessTraverser extends Traverser[Unit]
A StatelessTraverser is like a Traverser but does not carry a state during the traversal.
-
case class
Sub(name: LocalName, target: Term) extends Obj with Product with Serializable
a case in a substitution
-
case class
Substitution(subs: Sub*) extends Obj with Product with Serializable
substitution between two contexts
-
abstract
class
SubstitutionApplier extends AnyRef
A SubstitutionApplier is an abstraction for the substitution application function.
A SubstitutionApplier is an abstraction for the substitution application function.
Its purpose is to permit optimized versions of substitution that share the traversal and capture-avoidance code.
A SubstitutionApplier is carried along as an implicit argument of Obj.^^, which implements the shared parts.
-
case class
Subtyping(stack: Stack, tp1: Term, tp2: Term) extends BinaryObjJudgement with Product with Serializable
represents a subtyping judgement context |- tp1 <: tp2
-
sealed abstract
class
Term extends Obj with ThisTypeTrait
A Term represents an MMT term.
- case class Text(format: String, obj: String) extends SemiFormalObject with Product with Serializable
- trait ThisTypeTrait extends AnyRef
-
case class
TorsoForm(torso: Term, apps: List[Appendage]) extends HashEquality[TorsoForm] with Product with Serializable
The torso form of a term is named akin to the head normal forms.
The torso form of a term is named akin to the head normal forms.
For example, OMA(h1, OMA(h2, tr, ext2), ext1) is in torso form with tr as the torso and (h1,ext1) and (h2,ext2) as Appendages that are attached to the torso.
Its torso normal form is TorsoNormalForm(c, Appendage(h1, ext1) :: Appendage(h2, ext2) :: Nil)
The point of the torso normal form is understood by considering a type theory, whose constructor are paired into introduction and elimination operators. Then the torso form is a useful representation for a series h1, h2, ... of eliminators applied to a term (the torso). The torso is either atomic or a sequence of introductors. In the latter case, a reduction rule (e.g., beta) can be applied, which eventually yields an atomic torso.
For example, OMA(@,OMA(pi1,c),a) arises from the constant c (of product type) by first projection out a component (a function) and then applying it to a.
-
case class
TorsoNormalForm(unknowns: List[LocalName]) extends Product with Serializable
In the torso normal form, the torso cannot be further decomposed anymore, typically it is a variable or constant.
In the torso normal form, the torso cannot be further decomposed anymore, typically it is a variable or constant. See TorsoForm for further explanations.
-
abstract
class
Traverser[A] extends AnyRef
A Traverser is a function on Term defined by context-sensitive induction.
A Traverser is a function on Term defined by context-sensitive induction.
The auxiliary methods in the companion object can be used to handle all cases that traverse the object without any change. During the traversal, a value of type State may be used to carry along state.
-
case class
Typing(stack: Stack, tm: Term, tp: Term, tpSymb: Option[GlobalName] = None) extends BinaryObjJudgement with WFJudgement with Product with Serializable
represents a typing judgement context |- tm : tp tpSymb - optionally specified typing symbol
-
abstract
class
UnaryObjJudgement extends Judgement
Common code for some judgements
-
case class
Universe(stack: Stack, wfo: Term) extends UnaryObjJudgement with WFJudgement with Product with Serializable
A term univ is a universe if all its inhabitants are Inhabitable.
-
case class
UnknownOMLIT(valueString: String, synType: Term) extends Term with OMLITTrait with Product with Serializable
degenerate case of OMLIT when no RealizedType was known to parse a literal
degenerate case of OMLIT when no RealizedType was known to parse a literal
This class is awkward but necessary to permit a lookup-free parser, which delays parsing of literals to a later phase. UnknownOMLITs are replaced with OMLITs in the libraries.StructureChecker.
- synType
the type of the this literal
-
case class
VarDecl(name: LocalName, feature: Option[String], tp: Option[Term], df: Option[Term], not: Option[TextNotation]) extends Obj with NamedElement with Product with Serializable
represents an MMT term variable declaration
represents an MMT term variable declaration
- name
name
- tp
optional type
- df
optional definiens
- not
optional notation
-
trait
WFJudgement extends Judgement
A WFJudgment defines well-formed objects
- case class XMLNode(obj: Node) extends SemiFormalObject with Product with Serializable
-
case class
OMSemiFormal(tokens: List[SemiFormalObject]) extends Term with SemiFormalObjectList with Product with Serializable
An OMSemiFormal represents a mathematical object that mixes formal and informal components
An OMSemiFormal represents a mathematical object that mixes formal and informal components
- Annotations
- @MMT_TODO( message = ... )
- Deprecated
this should be replaced with the urtheory for semiformal objects
Value Members
-
object
AnonymousDiagramCombinator
bridges between AnonymousDiagram and Term
-
object
AnonymousMorphismCombinator
bridges between AnonymousMorphism and Term
-
object
AnonymousTheoryCombinator
bridges between AnonymousTheory and Term
- object ComplexMorphism
-
object
ComplexTerm
ComplexTerm provides apply/unapply methods to unify OMA and OMBINDC as well as named arguments and complex binders
ComplexTerm provides apply/unapply methods to unify OMA and OMBINDC as well as named arguments and complex binders
It does not subsume the OMID case
-
object
ComplexTheory
the normal form of a theory expression is a context
the normal form of a theory expression is a context
the apply/unapply functions convert between them
-
object
CongruenceClosure extends CongruenceClosure
trivial case without any assumptions
-
object
Context extends Serializable
helper object
-
object
Conversions
Stores all implicit conversions related to MMT objects This is imported in all source files that use conversions
- object DerivedOMLFeature
- object DerivedVarDeclFeature
- object Free
-
object
FreeOrAny
always matches, possibly with empty context
- object IncludeOML extends DerivedOMLFeature with Unnamed
- object IncludeSub
- object IncludeVarDecl extends DerivedVarDeclFeature
-
object
IsMorphism
An abbreviation for the meta-level typing judgement for valid morphisms
-
object
IsRealization
An abbreviation for a IsMorphism into the current theory
-
object
IsTheory
An abbreviation for the meta-level typing judgement for valid theories
-
object
MatchFail extends MatchResult with Product with Serializable
definitely not equal
- object ModExp extends TheoryScala
- object Morph
-
object
MorphType
MorphType(from,to) is the type of morphisms
-
object
OMATTRMany
apply/unapply methods for a list of attributions
-
object
OMAorAny
special application that elides empty argument lists:
special application that elides empty argument lists:
- returns
f if args is Nil, OMA(f, args) otherwise; always matches
-
object
OMBIND
OMBIND represents a binding without condition
-
object
OMCOMP
An OMCOMP represents the associative composition of a list of morphisms.
An OMCOMP represents the associative composition of a list of morphisms. Compositions may be nested.
-
object
OMIDENT
An OMIDENT represents the identity morphism of a theory.
-
object
OMINST
Covariant interpretation of theory parameters: a morphism m:S(args) --> T is seen as a morphism args,m: S --> T Such morphisms occur in particular if S(args) is included into T, i.e., if m is the identity of S This case is represented by OMINST(S,T,args).
Covariant interpretation of theory parameters: a morphism m:S(args) --> T is seen as a morphism args,m: S --> T Such morphisms occur in particular if S(args) is included into T, i.e., if m is the identity of S This case is represented by OMINST(S,T,args). args must be well-typed relative to T. invariant: args.nonEmpty (apply method allows it by using OMIDENT instead; unapply method does not match OMIDENT)
- object OML extends Serializable
- object OMLList
-
object
OMM
An OMM represents the application of a morphism to a term
-
object
OMMOD
An OMMOD represents a reference to a module (which may be a theory or a morphism expression).
-
object
OMPMOD
An OMPMOD represents a reference to a parametric module applied to arguments
- object OMS
- object OMSemiFormal extends Serializable
-
object
OMStructuralInclude
OMStructuralInclude(f,t): f -> t is the identity on the meta-theory of f (if any) and renames every declaration f?c in f to t?c For now, f may not have includes.
-
object
OMV extends Serializable
helper object
-
object
Obj
Obj contains the parsing methods for objects.
-
object
PlainSubstitutionApplier extends SubstitutionApplier
the default SubstitutionApplier defined in the usual way
the default SubstitutionApplier defined in the usual way
This is used by Obj.^
- object Position extends Serializable
-
object
RealizeOML extends DerivedOMLFeature with Unnamed
a realization declaration is like a structure/include except it *postulates* the existence of a theory morphism if partial, the morphism maps declarations to declarations of the same local name in the containing theory
-
object
SmartSubstitutionApplier extends SubstitutionApplier
A SubstitutionApplier that only recurses if the subobject has a free variable that is non-trivially affected by the substitution.
- object Stack extends Serializable
- object StructureOML extends DerivedOMLFeature with Named
-
object
StructureSharingSubstitutionApplier extends SubstitutionApplier
like SmartSubstitutionApplier but also preserves structure sharing
- object StructureSub
- object StructureVarDecl extends DerivedVarDeclFeature
-
object
Sub extends Serializable
helper object
-
object
Substitution extends Serializable
helper object
- object TUnion
- object TheoryExp
- object TheoryType
- object TorsoForm extends Serializable
- object Traverser
-
object
VarDecl extends Serializable
helper object