bellerophon

package bellerophon

Ordering

Alphabetic

Visibility

Public
All

Type Members

case class AppliedBuiltinTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr with (ProvableSig) ⇒ ProvableSig with Product with Serializable
Motivation is similar to AppliedPositionTactic, but for BuiltInTwoPositionTactic
class AppliedDependentPositionTactic extends DependentTactic
class AppliedDependentPositionTacticWithAppliedInput extends AppliedDependentPositionTactic
case class AppliedPositionTactic(positionTactic: PositionalTactic, locator: PositionLocator) extends BelleExpr with (ProvableSig) ⇒ ProvableSig with Product with Serializable
Stores the position tactic and position at which the tactic was applied.
Stores the position tactic and position at which the tactic was applied. Useful for storing execution traces.
case class ApplyDefTactic(t: DefTactic) extends BelleExpr with Product with Serializable
Applies the tactic definition t.
trait AtPosition[T <: BelleExpr] extends BelleExpr with (PositionLocator) ⇒ T with Logging
Applied at a position, AtPosition turns into a tactic of type T.
Applied at a position, AtPosition turns into a tactic of type T. Turns a position or position locator into a tactic. That is, an AtPosition[T] tactic is essentially a function of type
```
Position => T
```
but one that also supports indirect positioning via position locators that merely identify positions
```
PositionLocator => T
```
An AtPosition tactic t supports direct positions and indirect position locators.
- t(1) applied at the first succedent formula.
- t(-1) applied at the first antecedent formula.
- t(-4, 0::1::1::Nil) applied at subexpression positioned at .0.1.1 of the fourth antecedent formula, that is at the second child of the second child of the first child of the fourth antecedent formula in the sequent.
- t('L) applied at the first applicable position in the antecedent (left side of the sequent).
- t('R) applied at the first applicable position in the succedent (right side of the sequent).
- t('_) applied at the first applicable position in the side of the sequent to which tactic t applies. The side of the sequent is uniquely determined by type of tactic.
- t('Llast) applied at the last antecedent position (left side of the sequent).
- t('Rlast) applied at the last succedent position (right side of the sequent).
In addition, the formulas expected or sought for at the respective positions identified by the locators can be provided, which is useful for tactic contract and tactic documentation purposes. It is also useful for finding a corresponding formula by pattern matching.
- t(2, fml) applied at the second succedent formula, ensuring that the formula fml is at that position.
- t(-2, fml) applied at the second antecedent formula, ensuring that the formula fml is at that position.
- t(5, 0::1::1::Nil, ex) applied at subexpression positioned at .0.1.1 of the fifth succedent formula, that is at the second child of the second child of the first child of the fifth succcedent formula in the sequent, ensuring that the expression ex is at that position.
- t('L, fml) applied at the antecedent position (left side of the sequent) where the expected formula fml can be found (on the top level).
- t('R, fml) applied at the succedent position (right side of the sequent) where the expected formula fml can be found (on the top level).
- t('_, fml) applied at the suitable position (uniquely determined by type of tactic) where the expected formula fml can be found (on the top level).
class BelleAbort extends BelleProofSearchControl
Raised when a tactic decides that all further tactical work on a goal is useless and bellerophon should immediately stop
abstract class BelleBaseInterpreter extends Interpreter with Logging
Sequential interpreter for Bellerophon tactic expressions.
case class BelleCEX(message: String, cex: Map[NamedSymbol, Expression], s: Sequent) extends BelleProofSearchControl with Product with Serializable
Raised when counterexamples are found in sequent s; cex contains counterexample values per named symbol.
sealed trait BelleContext extends (Map[BelleDot, BelleExpr]) ⇒ BelleExpr
abstract class BelleCriticalException extends BelleThrowable
Reported bug: Major syntactic and semantic errors in bellerophon tactics that indicate a tactic is broken.
Reported bug: Major syntactic and semantic errors in bellerophon tactics that indicate a tactic is broken. For example, forgetting to provide an expected position or applying a left tactic on the right. BelleInterpreter will raise the error to the user's attention but it needs an internal fix to KeYmaera X.
class BelleDelayedSubstProvable extends BelleProvable
A Provable that was produced with a delayed substitution subst.
class BelleDot extends BelleExpr
⎵: Placeholder for tactics in tactic contexts.
⎵: Placeholder for tactics in tactic contexts. Reserved tactic expression that cannot be executed.
sealed abstract class BelleExpr extends AnyRef
Algebraic Data Type whose elements are well-formed Bellephoron tactic expressions.
Algebraic Data Type whose elements are well-formed Bellephoron tactic expressions. All Bellerophon tactic expressions are of type edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr, which provides the following tactic combinators
- s ; t alias s & t sequential composition executes t on the output of s, failing if either fail.
- s | t alternative composition executes t if applying s fails, failing if both fail.
- t* saturating repetition executes tactic t repeatedly to a fixpoint, casting result to type annotation, diverging if no fixpoint.
- t*n bounded repetition executes t tactic n number of times, failing if any of those repetitions fail.
- t+ saturating repetition executes tactic t to a fixpoint, requires at least one successful application.
- <(e1,...,en) branching to run tactic ei on branch i, failing if any of them fail or if there are not exactly n branches.
To do
Consolidate the members of BelleExpr and finalize an abstract syntax.
See also
Table 1 of Bellerophon: A Typed Language for Automated Deduction in a Uniform Substitution Calculus. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. Springer, 2017.
edu.cmu.cs.ls.keymaerax.bellerophon.Interpreter
edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
trait BelleLabel extends AnyRef
Bellerophon labels for proof branches.
Bellerophon labels for proof branches.

See also
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.label()
edu.cmu.cs.ls.keymaerax.btactics.Idioms.<()
edu.cmu.cs.ls.keymaerax.btactics.BelleLabels
case class BelleLabelTx(r: BelleLabel, c: Option[BelleLabel], label: String = "") extends BelleLabel with Product with Serializable
Label transaction with rollback point r and collected labels c since rollback point.
class BelleNoProgress extends BelleProofSearchControl
Raised when a tactic wants to indicate that it is/was not able to make progress on the goal.
abstract class BelleProofSearchControl extends BelleThrowable
Search control: Silently raises issues to control proof search, indicating that one proof attempt did not succeed so other proof options should be tried.
Search control: Silently raises issues to control proof search, indicating that one proof attempt did not succeed so other proof options should be tried. They will be swallowed by any outer proof search tactics that will try something else instead. For example, trying to apply an implyR tactic at a succedent position that contains an Or will be inapplicable but does not indicate a bug in the tactic, merely that a different branch needs to be taken in proof search.

See also
BelleTacticFailure
TacticInapplicableFailure
case class BelleProvable(p: ProvableSig, label: Option[List[BelleLabel]]) extends BelleExpr with BelleValue with Product with Serializable
A Provable during a Bellerophon interpreter run, readily paired with an optional list of BelleLabels
case class BelleSubLabel(parent: BelleLabel, label: String) extends BelleLabel with Product with Serializable
A sublabel for a BelleProvable
case class BelleSubProof(id: Int) extends BelleValue with Product with Serializable
Internal: To communicate proof IDs of subproofs opened in the spoon-feeding interpreter in Let between requests.
Internal: To communicate proof IDs of subproofs opened in the spoon-feeding interpreter in Let between requests. NOT TO BE USED FOR ANYTHING ELSE
abstract class BelleTacticFailure extends BelleProofSearchControl
Signaling that a tactic was not applicable or did not work at the current goal.
Signaling that a tactic was not applicable or did not work at the current goal. BelleTacticFailures will be consumed by the BelleInterpreter which will try something else instead.
abstract class BelleThrowable extends ProverException
Common exception type for all Bellerophon tactic problems and exceptions.
Common exception type for all Bellerophon tactic problems and exceptions. Tactic exceptions come on three different kinds:
1. BelleCriticalException indicates an internal bug in a tactic implementation, such as applying left rules on the right. They will be reported but need a KeYmaera X implementation change to fix. 2. BelleUserCorrectableException indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step. They will be reported back to the user along with a legible message describing what needs to be changed in the problem or proof. 3. BelleProofSearchControl indicates that one proof attempt did not succeed so other proof options should be tried. They will be swallowed by any outer proof search tactics that will try something else instead. Some advanced proof search tactics may "convert" between these exception types or swallow more of them when they deliberately try steps they know may fail spectacularly but have a backup plan.
case class BelleTopLevelLabel(label: String) extends BelleLabel with Product with Serializable
A top-level label for a BelleProvable
class BelleUnexpectedProofStateError extends BelleCriticalException
Signals an unexpected proof state (e.g., an open goal that should have been closed).
case class BelleUnfinished(message: String, p: Provable) extends BelleProofSearchControl with Product with Serializable
Raised when provable p is not yet proved.
abstract class BelleUserCorrectableException extends BelleThrowable
User feedback: Indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step.
User feedback: Indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step. They will be reported back to the user along with a legible message describing what needs to be changed in the problem or proof.
trait BelleValue extends AnyRef
Bellerophon expressions that are values, so should not be evaluated any further since irreducible.
case class BranchTactic(children: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
<(e1,...,en) branching to run tactic ei on branch i, failing if any of them fail or if there are not exactly n branches.
abstract case class BuiltInLeftTactic(name: String) extends BelleExpr with LeftTactic with NamedBelleExpr with Product with Serializable
Built-in position tactics that are to be applied on the left
abstract case class BuiltInPositionTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable
Built-in position tactics such as assertAt
abstract case class BuiltInRightTactic(name: String) extends BelleExpr with RightTactic with NamedBelleExpr with Product with Serializable
Built-in position tactics that are to be applied on the right
abstract case class BuiltInTactic(name: String) extends BelleExpr with NamedBelleExpr with (ProvableSig) ⇒ ProvableSig with Product with Serializable
abstract case class BuiltInTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
class Cancellable[T] extends AnyRef
Cancellable future, @see https://stackoverflow.com/questions/16009837/how-to-cancel-future-in-scala
case class CaseTactic(children: Seq[(BelleLabel, BelleExpr)]) extends BelleExpr with Product with Serializable
<("l1":e1,...,"ln":en) branching to run tactic ei on label li, failing if any of them fail, if there are not exactly n branches, or if any of the labels does not exist.
case class ChooseSome[A](options: () ⇒ Iterator[A], e: (A) ⇒ BelleExpr) extends BelleExpr with Product with Serializable
ChooseSome(options, e)(pr) proves e(o)(pr) after choosing some option o from options whose proof with tactic e succeeds after supplying argument o to e.
ChooseSome(options, e)(pr) proves e(o)(pr) after choosing some option o from options whose proof with tactic e succeeds after supplying argument o to e. It's usually one of the first options o for which e(o)(pr) does not fail. Fails if no choice from options made e(o)(pr) succeed.
options
The (lazy) iterator or stream from which subsequent options o will be tried.
e
The tactic generator e that will be tried with input o on the Provable subsequently for each of the options o in options until one is found for which e(o) does not fail.

See also
EitherTactic
class CompoundCriticalException extends BelleCriticalException
A Bellerophon critical exception that consists of two reasons why it is being raised, for example, if two things went wrong out of which it would have sufficed if only one succeeds.
class CompoundProofSearchException extends BelleProofSearchControl
A Bellerophon proof search exception that consists of two reasons why it is being raised, for example, if two things went wrong out of which it would have sufficed if only one succeeds.
case class ConcurrentInterpreter(listeners: Seq[IOListener] = Nil, throwWithDebugInfo: Boolean = false) extends BelleBaseInterpreter with Logging with Product with Serializable
Concurrent interpreter that runs parallel tactics concurrently.
abstract case class CoreLeftTactic(name: String) extends BelleExpr with LeftTactic with NamedBelleExpr with Product with Serializable
Built-in position tactics coming from the core that are to be applied on the left.
Built-in position tactics coming from the core that are to be applied on the left. Unlike BuiltInLeftTactic, wraps MatchError from the core in readable errors.

See also
TacticInapplicableFailure
abstract case class CoreRightTactic(name: String) extends BelleExpr with RightTactic with NamedBelleExpr with Product with Serializable
Built-in position tactics coming from the core that are to be applied on the right Unlike BuiltInRightTactic, wraps MatchError from the core in readable errors.
Built-in position tactics coming from the core that are to be applied on the right Unlike BuiltInRightTactic, wraps MatchError from the core in readable errors.

See also
TacticInapplicableFailure
case class DbAtomPointer(id: Int) extends ExecutionContext with Product with Serializable
Computes IDs for atomic steps stored in the database.
Computes IDs for atomic steps stored in the database. Anticipates how the DB issues IDs.
case class DbBranchPointer(parent: Int, branch: Int, predStep: Int, openBranchesAfterExec: List[Int] = Nil) extends ExecutionContext with Product with Serializable
Computes IDs for branching steps stored in the database.
Computes IDs for branching steps stored in the database. Anticipates how the DB issues IDs.
case class DefTactic(name: String, t: BelleExpr) extends BelleExpr with Product with Serializable
Defines a tactic for later execution.
abstract case class DependentPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with AtPosition[DependentTactic] with Product with Serializable
DependentPositionTactics are tactics that can be applied at positions giving dependent tactics.
DependentPositionTactics are tactics that can be applied at positions giving dependent tactics.

See also
AtPosition
abstract class DependentPositionWithAppliedInputTactic extends DependentPositionTactic
abstract case class DependentTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
Dependent tactics compute a tactic to apply based on their input.
Dependent tactics compute a tactic to apply based on their input. These tactics are probably not necessary very often, but are useful for idiomatic shortcuts. See e.g., AtSubgoal.
name
The name of the tactic.

To do
is there a short lambda abstraction notation as syntactic sugar?
Note
similar to the ConstructionTactics in the old framework, except they should not be necessary nearly as often because BuiltIns have direct access to a Provable.
case class EitherTactic(alts: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
trait ExecutionContext extends AnyRef
case class ExhaustiveSequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq(), throwWithDebugInfo: Boolean = false) extends SequentialInterpreter with Product with Serializable
Sequential interpreter that explores branching tactics exhaustively, regardless of failure of some.
case class Find(goal: Int, shape: Option[Expression], start: Position, exact: Boolean, defs: Declaration) extends PositionLocator with Product with Serializable
Locates the first applicable top-level position that matches shape (exactly or unifiably) at or after position start (remaining in antecedent/succedent as start says).
case class Fixed extends PositionLocator with Product with Serializable
Locates the formula at the specified fixed position.
Locates the formula at the specified fixed position. Can optionally specify the expected formula or expected shape of formula at that position as contract.
trait IOListener extends AnyRef
Listeners for input/output results during the interpretation of Bellerophon tactic expressions.
class IllFormedTacticApplicationException extends BelleCriticalException
Ill-formed ways of applying tactics, such as missing position for a position tactic or supplying a term when a formula was expected.
Ill-formed ways of applying tactics, such as missing position for a position tactic or supplying a term when a formula was expected. Or applying a tactic at -1 that can only applied in the succedent or vice versa. This indicates a catastrophic logical error in the whole tactic implementation.
class InapplicableUnificationKeyFailure extends BelleTacticFailure
Tactic was unable to unify with the given key and is, thus, inapplicable as indicated in the present sequent.
Tactic was unable to unify with the given key and is, thus, inapplicable as indicated in the present sequent. Besides indicating genuine unifiable situations, this may indicate that the wrong key was chosen for the (derived) axiom in its edu.cmu.cs.ls.keymaerax.btactics.macros.AxiomInfo.
class InfiniteTacticLoopError extends BelleCriticalException
Error indicates that a (critical) infinite tactic loop is detected indicating an implementation error.
class InputFormatFailure extends BelleTacticFailure
Signaling that a tactic input was not as expected.
abstract case class InputTactic(name: String, inputs: Seq[Any]) extends BelleExpr with NamedBelleExpr with Product with Serializable
trait Interpreter extends AnyRef
Interpreter for Bellerophon tactic expressions that transforms Bellerophon values using Bellerophon tactic language expressions to ultimately produce ProvableSig.
Interpreter for Bellerophon tactic expressions that transforms Bellerophon values using Bellerophon tactic language expressions to ultimately produce ProvableSig.
```
Interpreter : BelleExpr * BelleValue => BelleValue
```
See also
SequentialInterpreter
case class LabelBranch(label: BelleLabel) extends BelleExpr with NoOpTactic with Product with Serializable
Assign the given label label to the present BelleProvable.
case class LastAnte(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable
'Llast Locates the last position in the antecedent.
case class LastSucc(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable
'Rlast Locates the last position in the succedent.
case class LazySequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq(), throwWithDebugInfo: Boolean = false) extends SequentialInterpreter with Product with Serializable
Sequential interpreter that stops exploring branching on the first failing branch.
trait LeftTactic extends BelleExpr with PositionalTactic
Tactics that can only be applied in the antecedent on the left.
Tactics that can only be applied in the antecedent on the left.

See also
LeftRule
case class Let(abbr: Expression, value: Expression, inner: BelleExpr) extends BelleExpr with Product with Serializable
Let(abbr, value, inner) alias let abbr=value in inner abbreviates value by abbr in the provable and proceeds with an internal proof by tactic inner, resuming to the outer proof by a uniform substitution of value for abbr of the resulting provable.
Let(abbr, value, inner) alias let abbr=value in inner abbreviates value by abbr in the provable and proceeds with an internal proof by tactic inner, resuming to the outer proof by a uniform substitution of value for abbr of the resulting provable.

To do
generalize inner to also AtPosition[E]
See also
ProvableSig.apply(USubst)
case class LetInspect(abbr: Expression, instantiator: (ProvableSig) ⇒ Expression, inner: BelleExpr) extends BelleExpr with Product with Serializable
LetInspect(abbr, instantiator, inner) alias let abbr := inspect instantiator in inner postpones the choice for the definition of abbr until tactic inner finished on the Provable, and asks instantiator to choose a value for abbr based on that Provable at the end of inner.
LetInspect(abbr, instantiator, inner) alias let abbr := inspect instantiator in inner postpones the choice for the definition of abbr until tactic inner finished on the Provable, and asks instantiator to choose a value for abbr based on that Provable at the end of inner. Resumes to the outer proof by a uniform substitution of instantiator(result) for abbr of the resulting provable.

To do
generalize inner to also AtPosition[E]
Note
abbr should be fresh in the Provable
See also
ProvableSig.apply(USubst)
class MissingLyapunovFunction extends BelleUserCorrectableException
trait NamedBelleExpr extends BelleExpr
A BelleExpr that has a proper code name, so is not just used internally during application.
case class NamedTactic(name: String, tactic: BelleExpr) extends BelleExpr with NamedBelleExpr with Product with Serializable
Give a code name to the given tactic tactic for serialization purposes.
trait NoOpTactic extends AnyRef
Marker for no-op tactics.
case class OnAll(e: BelleExpr) extends BelleExpr with Product with Serializable
OnAll(e)(BelleProvable(p)) == <(e, ..., e) does the same tactic on all branches where e occurs the appropriate number of times, which is p.subgoals.length times.
OnAll(e)(BelleProvable(p)) == <(e, ..., e) does the same tactic on all branches where e occurs the appropriate number of times, which is p.subgoals.length times.

To do
eisegesis
case class ParallelTactic(expr: List[BelleExpr]) extends BelleExpr with Product with Serializable
left || right alternative composition executes both left and right simultaneously and succeeds with the first success, failing if both fail.
case class PartialTactic(child: BelleExpr, label: Option[BelleLabel] = None) extends BelleExpr with Product with Serializable
A partial tactic marks an unclosed proof (mainly for testing purposes to not insist on a closed proof).
A partial tactic marks an unclosed proof (mainly for testing purposes to not insist on a closed proof). To check for closed subgoals, use TactixLibrary.done.
sealed trait PositionLocator extends AnyRef
Position locators identify a position directly or indirectly in a sequent.
Position locators identify a position directly or indirectly in a sequent.

See also
AtPosition.apply()
trait PositionalTactic extends BelleExpr with AtPosition[AppliedPositionTactic]
PositionTactics are tactics that can be applied at positions giving ordinary tactics.
PositionTactics are tactics that can be applied at positions giving ordinary tactics.

See also
AtPosition
class ProofSearchFailure extends BelleTacticFailure
Signals a proof search failure.
Signals a proof search failure. Also thrown by calls that are not "tactics" per se but might, e.g., be called internally by a tactic May be caught internally by tactics to direct searches.
class ProverSetupException extends BelleCriticalException
Incorrect prover setup, such as insufficient stack size or missing tools.
case class RepeatTactic(child: BelleExpr, times: Int) extends BelleExpr with Product with Serializable
child*times bounded repetition executes child tactic times number of times, failing if any of those repetitions fail.
case class ReplacementBelleContext(t: BelleExpr) extends BelleContext with Product with Serializable
trait RightTactic extends BelleExpr with PositionalTactic
Tactics that can only be applied in the succedent on the right.
Tactics that can only be applied in the succedent on the right.

See also
RightRule
case class SaturateTactic(child: BelleExpr) extends BelleExpr with Product with Serializable
child* saturating repetition executes tactic child repeatedly to a fixpoint, casting result to type annotation, diverging if no fixpoint.
case class SearchAndRescueAgain(abbr: Seq[Expression], common: BelleExpr, instantiator: (ProvableSig, ProverException) ⇒ Seq[Expression], continuation: BelleExpr) extends BelleExpr with Product with Serializable
SearchAndRescue(abbr, common, instantiator, continuation) alias search abbr := after common among instantiator in continuation postpones the choice for the definition of abbr until tactic common finished on the Provable, but then searches for the definition of abbr by trying to run continuation from the outcome of common until continuation is successful.
SearchAndRescue(abbr, common, instantiator, continuation) alias search abbr := after common among instantiator in continuation postpones the choice for the definition of abbr until tactic common finished on the Provable, but then searches for the definition of abbr by trying to run continuation from the outcome of common until continuation is successful. Each time it asks instantiator to choose a value for abbr based on the same Provable at the end of common in addition to the present ProverException obtained after the current attempt of running continuation with the last choice for abbr. Resumes to the outer proof by a uniform substitution of instantiator(result) for abbrof the resulting provable which corresponds to having runUSubst(abbr,inst){ common } ; continuation. Thus, the logical effect is identical to directly running USubst(abbr,inst){ common } ; continuation but the operational effect differs by the above search to find the instantiationinstin the first place.
abbr
the abbreviation to instantie, which should be fresh in the Provable

See also
ProvableSig.apply(USubst)
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017. Example 32.
NoProverException
case class SeqTactic(seq: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
abstract class SequentialInterpreter extends BelleBaseInterpreter with Logging
Sequential interpreter that runs parallel tactics as alternatives sequentially.
abstract class SingleGoalDependentTactic extends DependentTactic
case class SpoonFeedingInterpreter(rootProofId: Int, startStepIndex: Int, idProvider: (ProvableSig) ⇒ Int, defs: Declaration, listenerFactory: (Int) ⇒ (String, Int, Int) ⇒ Seq[IOListener], inner: (Seq[IOListener]) ⇒ Interpreter, descend: Int, strict: Boolean, convertPending: Boolean, recordInternal: Boolean) extends Interpreter with Logging with Product with Serializable
Sequential interpreter for Bellerophon tactic expressions: breaks apart combinators and spoon-feeds "atomic" tactics to another interpreter.
Sequential interpreter for Bellerophon tactic expressions: breaks apart combinators and spoon-feeds "atomic" tactics to another interpreter.
rootProofId
The ID of the proof this interpreter is working on.
startStepIndex
The index in the proof trace where the interpreter starts appending steps (-1 for none, e.g., in a fresh proof).
idProvider
Provides IDs for child provables created in this interpreter.
listenerFactory
Creates listener that are notified from the inner interpreter, takes (tactic name, parent step index in trace, branch).
inner
Processes atomic tactics.
descend
How far to descend into depending tactics (default: do not descend)
strict
If true, follow tactic strictly; otherwise perform some optimizations (e.g., do not execute nil).
abstract class StringInputTactic extends BuiltInTactic
class TacticAssertionError extends BelleCriticalException
Tactic assertions.
class TacticComparator[T <: BelleExpr] extends AnyRef
class TacticInapplicableFailure extends BelleTacticFailure
Tactic happens to not be applicable as indicated in the present sequent.
Tactic happens to not be applicable as indicated in the present sequent. For example, InapplicableTactic can be raised when trying to apply edu.cmu.cs.ls.keymaerax.btactics.SequentCalculus.andR at the correct position 2 in bounds on the right-hand side where it turns out there is an Or formula not an And formula. This does not indicate a catastrophic failure in the tactic implementation, merely a promising but unsuccessful attempt of applying a tactic.
class TacticRequirementError extends BelleCriticalException
Tactic requirements that failed and indicate a critical logical error in using it.
case class TryCatch[T <: Throwable](t: BelleExpr, cCatch: Class[T], c: (T) ⇒ BelleExpr, f: Option[BelleExpr] = None) extends BelleExpr with Product with Serializable
Tries tactic t and executes - c (catch) on exceptions of type T that occur when executing t - f (finally) on the result of t (if t is successful), on the result of c (if c is successful), or on the initial problem if neither t nor c are successful (throwing the exceptions of t or c even if f is successful).
Tries tactic t and executes - c (catch) on exceptions of type T that occur when executing t - f (finally) on the result of t (if t is successful), on the result of c (if c is successful), or on the initial problem if neither t nor c are successful (throwing the exceptions of t or c even if f is successful). Pattern: TryCatch should usually be used together with |. In that case, c should throw a proof search control exception instead of supplying a tactic, since it is usually intended to also execute the alternative tactic on success of t or if t throws other unrelated proof search control exceptions.
```
TryCatch(useAt("[:=] assign")(1), classOf[SubstitutionClashException],
  (ex: SubstitutionClashException) => throw new TacticInapplicableFailure("Inapplicable", ex)) | alternativeTactic
```
If indeed an alternative tactic should only be executed on exception, use
```
TryCatch(useAt("[:=] assign")(1), classOf[SubstitutionClashException],
  (ex: SubstitutionClashException) => alternativeTactic)
```
case class USubstPatternTactic(options: Seq[(BelleType, (RenUSubst) ⇒ BelleExpr)]) extends BelleExpr with Product with Serializable
USubstPatternTactic((form1, us=>t1) :: ...
USubstPatternTactic((form1, us=>t1) :: ... (form2, us=>t2) :: Nil) runs the first tactic ti for the unification us with the first pattern formi that matches the current goal.
In other words: case _ of {fi => ei} uniform substitution case pattern applies the first ei such that fi uniformly substitutes to current provable for which ei does not fail, fails if the ei of all matching fi fail.
class UnexpandedDefinitionsFailure extends BelleUserCorrectableException
class UnificationException extends BelleCriticalException
Raised to indicate that two expressions are not unifiable in the single-sided matching sense.
class UnprovableAnnotatedInvariant extends BelleUserCorrectableException
Signals that an annotated invariant is not provable and needs fixing.
class UnsupportedTacticFeature extends BelleTacticFailure
Signaling that a tactic's implementation was incomplete and did not work out as planned, so tactic execution might continue, but it is indicating a potential problem in the tactic's implementation.
case class Using(es: List[Expression], t: BelleExpr) extends BelleExpr with Product with Serializable
Positive mention of expressions es to use when executing tactic t.
case class AppliedDependentTwoPositionTactic(t: DependentTwoPositionTactic, p1: Position, p2: Position) extends BelleExpr with Product with Serializable

Annotations
@deprecated
Deprecated
trait BelleType extends AnyRef

Annotations
@deprecated
Deprecated
remove
To do
eisegesis -- simple types
abstract case class DependentTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable

Annotations
@deprecated
Deprecated
case class SequentType(s: Sequent) extends BelleType with Product with Serializable

Annotations
@deprecated
Deprecated
remove
To do
Added because SequentTypes are needed for unification tactics.
case class TheType() extends BelleType with Product with Serializable

Annotations
@deprecated
Deprecated
remove

Value Members

object BelleCommitTxLabel extends BelleLabel
Commits a label transaction.
object BelleDot extends BelleDot
object BelleExpr
object BelleInterpreter extends Interpreter
Provides the interpreter for running tactics.
object BelleLabel
Conversion functions for labels from/to strings.
object BelleProvable extends Serializable
object BelleRollbackTxLabel extends BelleLabel
Rollback a label transaction.
object BelleStartTxLabel extends BelleLabel
object Cancellable
object EitherTactic extends Serializable
left | right alternative composition executes right if applying left fails, failing if both fail.
object Find extends Serializable
object Fixed extends Serializable
object IOListeners
Some tactic listeners.
Some tactic listeners. Created by smitsch on 9/3/17.
object NoOpTactic
Mixing in NoOpTactic with existing tactic instances (e.g., obtained through TacticFactory methods)
Mixing in NoOpTactic with existing tactic instances (e.g., obtained through TacticFactory methods)

See also
https://stackoverflow.com/a/3896244
object PositionLocator
object ReflectiveExpressionBuilder extends Logging
Constructs a edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr from a tactic name
object SeqTactic extends Serializable
left ; right sequential composition executes right on the output of left, failing if either fail.
object TacticComparator
object TacticDiff
Computes a diff.
Computes a diff. (C,d1,d2) of two tactics t1 and t2 such that C(d1)=t1 and C(d2)=t2.
object TacticStatistics
Computes tactic statistics (e.g., size).
object UIIndex
User-Interface Axiom/Tactic Index: Indexing data structure for all canonically applicable (derived) axioms/rules/tactics in User-Interface.
User-Interface Axiom/Tactic Index: Indexing data structure for all canonically applicable (derived) axioms/rules/tactics in User-Interface.

See also
edu.cmu.cs.ls.keymaerax.btactics.AxIndex

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

KeYmaera X Kernel

Usage Overview

Constructing Proofs

Combining Proofs

Differential Dynamic Logic

Syntax

Static Semantics

Theorem Prover

Axioms

Uniform Substitutions

Sequent Proof Rules

Additional Capabilities

Stored Provable Mechanism

Error Reporting

Set Lattice

Overall Code Complexity

Lemma Mechanism

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

bellerophon 

package bellerophon

Type Members

Value Members

Ungrouped

bellerophon