package linkinversion
- Alphabetic
- Public
- All
Type Members
-
sealed abstract
class
ContinuationStyle extends AnyRef
The continuation style telling LinkInverter.invertLink() how to continue after encountering a RewriteConstantError.
The continuation style telling LinkInverter.invertLink() how to continue after encountering a RewriteConstantError.
Apart from it being used a little bit internally for the control flow in LinkInverter, it usually is returned by a RewriteErrorHandler given as a callback to LinkInverter.invertLink().
-
trait
LinkInversionRulesProvider extends AnyRef
Provider for inverse rewrite rules for links.
Provider for inverse rewrite rules for links.
Initially, the LinkInverter starts with the rules returned by LinkInversionRulesProvider.getInverseRewritingRules() and starts rewriting declarations.
Different implementations may consider different "equality rules".
- The simplest LinkInversionRulesProvider would return AbbrevRule instances for links which are renamings. Namely, those rules would rewrite the RHS of the renaming to the LHS. - A more complex implementation could in addition provide rules for link mappings
d = d'
whered' = OMBINDC(_, _, _)
. Namely, the rule would rewrite termst'
, which are the same asd'
modulo a renaming of the binding context, tod
. - An even more complex implementation would also match terms, e.g. whent'
is the body (scope) of the OMBINDC ofd'
with instantiated variables for the bound context, it woud rewritet'
tod [arguments for the instantiation]
. See LFLinkInversionRulesProvider. - final case class LinkInverterResult(invertedTheory: List[Declaration], generatedMorphism: List[Declaration]) extends Product with Serializable
-
final
case class
RewriteAs(decl: Declaration) extends ContinuationStyle with Product with Serializable
Forcefully rewrite the declaration to a provided one.
Forcefully rewrite the declaration to a provided one.
If you are within a RewriteErrorHandler,
decl
should start with the same new module path as passed to LinkInverter.invertLink().- See also
-
sealed
case class
RewriteConstantError(originalDecl: Constant, attemptedDecl: Option[Declaration], blamableTerms: scala.Predef.Map[ComponentKey, Seq[Term]]) extends RewriteError with Product with Serializable
- originalDecl
The original declaration, which was supposed to be rewritten.
- attemptedDecl
In case any attempt was made to rewrite the declaration, this option contains it. For example, when you received a RewriteError from LinkInverter.invertLink for a constant declaration, then the type or definiens component might still contain references to the theory S which was supposed to be generalized. However, in cases where the declarations wasn't known to LinkInverter.invertLink at all (e.g. proper structures - not inclusions), this might be None.
- blamableTerms
In case the declaration was a constant declaration and could not be fully rewritten due to some left over terms referring to things in the theory S, which was supposed to be generalized, this map contains it grouped by their occurrence in the term's component.
- sealed abstract class RewriteError extends AnyRef
-
trait
RewriteErrorHandler extends AnyRef
An error handler for LinkInverter.invertLink() called upon declarations which could not be rewritten due to a RewriteError.
An error handler for LinkInverter.invertLink() called upon declarations which could not be rewritten due to a RewriteError. The handler decides how to continue using a ContinuationStyle.
- sealed case class RewriteUnknownError(originalDecl: Declaration) extends RewriteError with Product with Serializable
Value Members
-
object
AssumeRewritable extends ContinuationStyle with Product with Serializable
Skip the failed declaration.
Skip the failed declaration.
- See also
-
object
LinkInverter
- To do
ComFreek: Document, especially when terms are not rewritable.
- object LinkUtils
- object ModuleCreator
-
object
SkipDeclaration extends ContinuationStyle with Product with Serializable
Skip the failed declaration.
Skip the failed declaration.
- See also
Deprecated Value Members
-
object
ReferenceSubstituter
- Annotations
- @deprecated
- Deprecated
(Since version 2019-03-14) Directly use info.kwarc.mmt.api.symbols.Renamer