package uom
Simplification
The algorithm for immutably computing with MMT content, i.e., simplification (strings to MMT data structures). See api for an overview of the algorithms.
The main interfaces are - Simplifier: the main interface for parser (combining a structure and an object simplifier) - StructureSimplifier: simplifying structural elements - ObjectSimplifier: simplifying objects
The main implementations are - ElaborationBasedSimplifier for structural elements - RuleBasedSimplifier for objects
Structure simplification is extensible using derived elements. Object simplification is extensible using rules.
Literals and semantic objects
This package also contains the classes for using Scala objects as MMT literals.
SemanticType defines types as sets of Scala objects. SemanticValue defines a distinguished element of such a type. SemanitcOperator defines functions on such types as Scala functions.
Literals and operations on them are injected into the MMT language by declaring RealizedValue, RealizedType and RealizedOperator rules, which tie a syntactic type/operator (i.e., an MMT term) to a semantic counterpart.
StandardLiterals defines semantic types for the most important types.
RealizedTheory represents an MMT theory programmed in Scala, usually as a Scala class.
Scala companion objects for MMT theories
TheoryScala and ConstantScala are auxiliary classes that are useful when implementing MMT rules or other logic-specific algorithms.
- Source
- package.scala
- Alphabetic
- By Inheritance
- uom
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
class
AbbrevRule extends SimplificationRule
An AbbrevRule expands a symbol into a term
-
abstract
class
Atomic[V] extends SemanticType with RSemanticType[V]
a type that is equal to an existing Scala type
- class BinaryConstantScala extends ConstantScala
-
sealed abstract
class
CannotSimplify extends Simplifiability
this rule cannot be applied to t at toplevel
-
trait
ComplificationRule extends TermTransformationRule
the term transformation rules that should be used for complification
the term transformation rules that should be used for complification
separating these rules is important to avoid cycles during simplification
- trait ConstantScala extends AnyRef
-
class
DefinitionExpander extends StatelessTraverser
traverses the syntax tree (depth first, argument order) and expands (only) the first defined constant it encounters
traverses the syntax tree (depth first, argument order) and expands (only) the first defined constant it encounters
does not expand in contexts and scopes at the moment
- trait DocumentScala extends AnyRef
-
class
ElaborationBasedSimplifier extends Simplifier with ChangeListener
the primary class for all flattening, materialization, enriching of theories
the primary class for all flattening, materialization, enriching of theories
*internal* flattening of s: change the body of s by flattening all its components and children. *external* flattening of s: change the parent of s by adding all declarations induced by s. Internal flattening includes the recursive internal and external flattening of its children.
Most declarations are subject to either internal (modules and links) or external (includes, structures, derived declarations) flattening. Only non-include structures are subject to both.
- case class ExtendedSimplificationEnvironment(se: SimplificationEnvironment, objectSimplifier: ObjectSimplifier, rules: RuleSet) extends scala.Product with Serializable
- class FlexaryConstantScala extends ConstantScala
- class FouraryConstantScala extends ConstantScala
-
class
FunctionN extends AnyRef
a flexary function, used by RealizationInScala
-
class
GenericScalaExporter extends BuildTarget with Exporter
This trait bundles auxiliary methods for exporting Scala code
-
class
IntModulo extends RQuotient[BigInt]
standard integers modulo, i.e., a finite type of size modulus
-
abstract
class
IntegerLiteral extends Atomic[BigInt] with IntegerRepresented
bundles functions that are typically used when defining literals based on integers
-
trait
IntegerRepresented extends SemanticType with RSemanticType[BigInt]
types whose underlying representation uses integers
-
class
InvFunctionN extends AnyRef
inverse of a flexary function, used by RealizationInScala
-
abstract
class
InverseOperator extends SimplifierRule
counterpart to a RealizedOperator for the partial inverse This is also possible if head is injective.
counterpart to a RealizedOperator for the partial inverse This is also possible if head is injective. See lf.SolutionRules for the non-injective case.
-
trait
Invertible extends AnyRef
adds a Scala-style unapply method
- case class KnownArg(value: Any, pos: Int) extends UnapplyArg with scala.Product with Serializable
- case class ListType(over: SemanticType) extends SemanticType with scala.Product with Serializable
-
abstract
class
MatchingSimplificationRule extends SimplifierRule
rules for simplifying expressions
-
trait
ObjectSimplifier extends Extension
simplifies/rewrites objects
- class OpenMathScalaExporter extends FoundedExporter
- case class Product(left: SemanticType, right: SemanticType) extends SemanticType with scala.Product with Serializable
- abstract class Quotient extends SemanticType
- class RList[U] extends ListType with RSemanticType[List[U]]
- class RProduct[U, V] extends Product with RSemanticType[(U, V)]
- abstract class RQuotient[V] extends Quotient with RSemanticType[V]
-
trait
RSemanticType[V] extends SemanticType
a semantic type whose underlying representation type is made explicit
- abstract class RSubtype[U] extends Subtype with RSemanticType[U]
- class RTuple[U] extends TupleType with RSemanticType[List[U]]
-
abstract
class
RealizationInScala extends RealizedTheory
a model of an MMT theory written in Scala
-
case class
RealizedOperator(synOp: GlobalName, synTp: SynOpType, semOp: SemanticOperator, semTp: SemOpType) extends SimplificationRule with scala.Product with Serializable
A RealizedOperator couples a syntactic function (a Constant) with a semantic function (a Scala function)
-
abstract
class
RealizedTheory extends Theory with SemanticObject
a theory written directly in Scala
-
case class
RealizedType(synType: Term, semType: SemanticType) extends SimplifierRule with scala.Product with Serializable
A RealizedType couples a syntactic type (a Term) with a semantic type (a PER on the universe of Scala values).
-
class
RealizedValue extends AbbrevRule
A RealizedOperator couples a syntactic constant (a Constant) with a semantic function (a Scala function)
-
case class
RecurseOnly(positions: List[Int]) extends CannotSimplify with scala.Product with Serializable
this rule cannot become applicable unless a subterm in one of the given positions is simplified; the first argument has position 1
- class RepresentedRealizedType[V] extends RealizedType
-
class
RewriteRule extends TermTransformationRule
a general rewrite rule
-
class
RuleBasedSimplifier extends ObjectSimplifier
A RuleBasedSimplifier applies DepthRule's and BreadthRule's exhaustively to simplify a Term.
A RuleBasedSimplifier applies DepthRule's and BreadthRule's exhaustively to simplify a Term.
### Invariants
Simplifying transforms a welltyped term into another welltyped term. This especially means that rules have to retain the type.
Only AbbrevRule rules will be applied on OMID (sub)terms. This makes sense given that OMIDs reference constants, for which other reference to other constants could never take place given the welltyping constraint above. The only way for an OMID to be rewritten is by definitorial expansion, which can be enabled in SimplificationUnit.
TODO Add other invariants.
-
case class
SemOpType(args: List[SemanticType], ret: SemanticType) extends scala.Product with Serializable
helper class to store the type of a SemanticOperators
-
abstract
class
SemanticOperator extends SemanticObject
a Scala-level function between SemanticTypes to be used in a RealizedOperator
-
abstract
class
SemanticType extends SemanticObject
A Scala-level type to be used in a RealizedType
A Scala-level type to be used in a RealizedType
See also SemanticOperator
SemanticType's are closed under subtypes and quotients by using valid and normalform. In other words, the triple (U, valid, normalform) forms a partial equivalence relation on a Scala type U.
For technical reasons, U is fixed as the type Any (Scala cannot type check enough to make the overhead worthwhile.) Instead, type-safety-supporting syntax is offered wherever reasonable, see also RSemanticType.
-
case class
SemanticValue(tp: SemanticType, value: Any) extends SemanticObject with scala.Product with Serializable
a Scala-level value to be used in a RealizedValue
-
sealed abstract
class
Simplifiability extends AnyRef
return type of applying a simplification rule to a term t
- class SimplificationEnvironment extends AnyRef
-
abstract
class
SimplificationRule extends MatchingSimplificationRule
Special case for rules that do not need to know about other rules.
-
case class
SimplificationUnit(context: Context, expandDefinitions: Boolean, fullRecursion: Boolean, solverO: Option[Solver] = None) extends MMTTask with scala.Product with Serializable
applies rules to simplify an object
applies rules to simplify an object
- context
the context of the object to simplify
- expandDefinitions
if true, expand all definitions of constant (we speak of *deep* simplification)
- fullRecursion
if false, only recurse into subexpressions that contribute to head-normalizations
-
abstract
class
Simplifier extends StructureSimplifier with LeveledExtension
the designated super class of all simplifiers
-
trait
SimplifierRule extends SyntaxDrivenRule
super class of all rules used by simplification
- case class SimplifierState(t: Term, unit: SimplificationUnit, rules: RuleSet, path: List[Int]) extends scala.Product with Serializable
-
case class
Simplify(result: Term) extends Simplifiability with scala.Product with Serializable
simplify t to result
-
trait
StructureSimplifier extends Extension
simplifies/elaborates structural elements
- abstract class Subtype extends SemanticType
-
case class
SynOpType(under: List[GlobalName], args: List[Term], ret: Term) extends scala.Product with Serializable
helper class to store the type of a RealizedOperators
helper class to store the type of a RealizedOperators
- under
HOAS application operators
- args
argument types
- ret
return type
-
trait
TermTransformationRule extends SimplifierRule
general purpose transformation rule //TODO this is barely used and should be merged with SimplificationRule
-
class
TermTransformer extends StatelessTraverser with Logger
exhaustively applies TermTransformationRules
exhaustively applies TermTransformationRules
will not traverse the same term multiple times if called multiple times
preserves structure sharing
- class TernaryConstantScala extends ConstantScala
- trait TheoryScala extends AnyRef
- case class TupleType(over: SemanticType, dim: Int) extends SemanticType with scala.Product with Serializable
-
sealed abstract
class
UnapplyArg extends AnyRef
used to pass the arguments to the unapply method of a SemanticOperator
- class UnaryConstantScala extends ConstantScala
-
class
UnknownArg extends UnapplyArg
an unknown argument that unapply must solve by calling solve
- trait ViewScala extends TheoryScala
-
case class
ByStructureSimplifier(home: Term, view: Term) extends Origin with scala.Product with Serializable
used by MMTStructureSimplifier
used by MMTStructureSimplifier
- Annotations
- @MMT_TODO( message = "needs review" )
- Deprecated
needs review
Value Members
-
object
Arithmetic
defines SemanticOperators for the standard arithmetic operations
-
object
ComplexRat extends RProduct[(BigInt, BigInt), (BigInt, BigInt)]
rational complex numbers
- object ConstantScala
-
object
DefinitionsExpanded extends BooleanTermProperty
UOM uses this to remember that all definitions inside a Term have been expanded to avoid recursing into it again
-
object
ElaboratedElement extends ClientProperty[StructuralElement, Int]
information about elaboration status 0 or absent: no information, assume not elaborated 2: partially: header has been elaborated, some elements in body (e.g., new elements) body must still be elaborated 3: fully: applyElementEnd has been called -1: in progress, apply or applyElementBegin has been called -2: in progress and header already elaborated
- object FunctionN
- object GenericScalaExporter
- object Integrator
- object InvFunctionN
- object ListType extends Serializable
-
object
OMLiteral
OpenMath's literals These should be moved to an OpenMath plugin, but they are used by the API, e.g., for metadata
- object OpenMath
- object Product extends Serializable
- object RealizedOperator extends Serializable
- object RealizedValue
-
object
Recurse extends CannotSimplify with scala.Product with Serializable
this rule might become applicable if any subterm is simplified
this rule might become applicable if any subterm is simplified
this should be returned by default; it replaces the return value "None" from the previous ComputationRule.apply method that returned Option[Term]
- object RuleBasedSimplifier
-
object
Scala
apply/unapply methods for the constructor Scala(code: String): Term to represent escaped Scala code in an MMT Term
- object SemanticOperator
- object SemanticType
- object Simplifiability
- object StandardBool extends Atomic[Boolean]
- object StandardDouble extends Atomic[Double]
-
object
StandardInt extends IntegerLiteral
standard integer numbers
-
object
StandardNat extends RSubtype[BigInt]
standard natural numbers
-
object
StandardPositive extends RSubtype[BigInt]
standard positive natural numbers
-
object
StandardRat extends RQuotient[(BigInt, BigInt)]
standard rational numbers
- object StandardString extends Atomic[String]
- object StringOperations
-
object
TermLiteral extends Atomic[Term]
MMT terms as a semantic type, e.g., for reflection, quotation
- object TrivialSimplificationEnvironment extends SimplificationEnvironment
- object TupleType extends Serializable
-
object
URILiteral extends Atomic[URI]
URI literals, concrete syntax is uri"..."
-
object
UUIDLiteral extends Atomic[UUID]
UUIDs