Packages

p

edu.cmu.cs.ls.keymaerax

bellerophon

package bellerophon

Bellerophon tactics language framework. This package includes

All Bellerophon tactic expressions are of type edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr, which provides the following tactic combinators

  • 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.
  • 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.
  • t partial partial tactic marker marks that tactic t is allowed to not close all its goals.

Positional tactics support flexible modes of identifying what position to apply them to via edu.cmu.cs.ls.keymaerax.bellerophon.AtPosition. Applying a positional tactic t at a position supports many different ways of specifying the position:

  • 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).
See also

Nathan Fulton, Stefan Mitsch, Brandon Bohrer and Andre Platzer. Bellerophon: Tactical theorem proving for hybrid systems. In Mauricio Ayala-Rincon and Cesar Munoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS. Springer, 2017.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. bellerophon
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class AfterTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable
  2. trait AntePosition extends Position

    A position guaranteed to identify an antecedent position

    A position guaranteed to identify an antecedent position

    See also

    AntePos

  3. case class AppliedBuiltinTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr with Product with Serializable

    Motivation is similar to AppliedPositionTactic, but for BuiltInTwoPositionTactic

  4. class AppliedDependentPositionTactic extends DependentTactic
  5. class AppliedDependentPositionTacticWithAppliedInput extends AppliedDependentPositionTactic
  6. case class AppliedPositionTactic(positionTactic: PositionalTactic, locator: PositionLocator) extends BelleExpr 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.

  7. case class ApplyDefTactic(t: DefTactic) extends BelleExpr with Product with Serializable

    Applies the tactic definition t.

  8. 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).
  9. trait BaseMatcher extends Matcher

    A matcher that forwards all unification functionality to BaseMatcher.unify().

  10. class BelleAbort extends BelleThrowable

    Raised when a tactic decides that all further tactical work on a goal is useless and bellerophon should immediately stop

  11. sealed trait BelleContext extends (Map[BelleDot, BelleExpr]) ⇒ BelleExpr
  12. class BelleDot extends BelleExpr

    ⎵: Placeholder for tactics in tactic contexts.

    ⎵: Placeholder for tactics in tactic contexts. Reserved tactic expression that cannot be executed.

  13. 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. See Table 1 of "Bellerophon: A Typed Language for Automated Deduction in a Uniform Substitution Calculus"

    To do

    Consolidate the members of BelleExpr and finalize an abstract syntax.

    See also

    edu.cmu.cs.ls.keymaerax.bellerophon

    edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter

  14. class BelleFriendlyUserMessage extends Exception

    These exceptions have well-understood causes and the given explanation should be propagated all the way to the user.

    These exceptions have well-understood causes and the given explanation should be propagated all the way to the user.

    To do

    give proper formatting and inContext and such.

  15. case class BelleIllFormedError(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable

    Syntactic and semantic errors in bellerophon tactics, such as forgetting to provide an expected position.

    Syntactic and semantic errors in bellerophon tactics, such as forgetting to provide an expected position. BelleInterpreter will raise the error to the user's attention.

  16. trait BelleLabel extends AnyRef

    Bellerophon labels for proof branches.

    Bellerophon labels for proof branches.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.BelleLabels

    edu.cmu.cs.ls.keymaerax.btactics.Idioms.<()

    edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.label()

  17. case class BelleProvable(p: ProvableSig, label: Option[List[BelleLabel]] = None) extends BelleExpr with BelleValue with Product with Serializable

    A Provable during a Bellerophon interpreter run, readily paired with an optional list of BelleLabels

  18. case class BelleSubLabel(parent: BelleLabel, label: String) extends BelleLabel with Product with Serializable

    A sublabel for a BelleProvable

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

  20. case class BelleTacticFailure(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable

    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.

  21. class BelleThrowable extends ProverException

    Common exception type for all Bellerophon tactic exceptions.

  22. case class BelleTopLevelLabel(label: String) extends BelleLabel with Product with Serializable

    A top-level label for a BelleProvable

  23. case class BelleUnsupportedFailure(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable

    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.

  24. case class BelleUserGeneratedError(msg: String) extends BelleThrowable with Product with Serializable
  25. trait BelleValue extends AnyRef

    Bellerophon expressions that are values.

  26. case class BranchTactic(children: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
  27. abstract case class BuiltInLeftTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable

    Built-in position tactics that are to be applied on the left

  28. abstract case class BuiltInPositionTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable

    Built-in position tactics such as assertAt

  29. abstract case class BuiltInRightTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable

    Built-in position tactics that are to be applied on the right

  30. abstract case class BuiltInTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
  31. abstract case class BuiltInTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
  32. 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

  33. class CompoundException extends BelleThrowable
  34. 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.

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

  36. case class DefExpression(exprDef: Formula) extends BelleExpr with Product with Serializable

    Defines an expression (function or predicate) for later expansion.

  37. case class DefTactic(name: String, t: BelleExpr) extends BelleExpr with Product with Serializable

    Defines a tactic for later execution.

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

  39. abstract class DependentPositionWithAppliedInputTactic extends DependentPositionTactic
  40. abstract case class DependentTactic(name: String) extends BelleExpr with NamedBelleExpr with Logging 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.

  41. final class DirectUSubstAboveURen extends RenUSubst

    Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.

    Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.

    s(RG) |- s(RD)
    -------------- USubst
      RG  |- RD
    -------------- URen
       G  |- D

    Semantic renaming may be supported if need be.

    DirectUSubstAboveURen is a direct implementation in tactics land of a joint renaming and substitution algorithm. It uses a single direct fast USubstRen for internal applications via DirectUSubstAboveURen.apply() but schedules separate uniform substitutions and uniform renamings to the core when asked. The first fast pass supports semantic renaming, which is useful during unification to "apply" renamings already to predicationals without clash. The final core pass does not support semantic renaming, but is only needed for the final unifier.

    Note

    reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.

  42. case class EitherTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable
  43. trait ExecutionContext extends AnyRef
  44. case class ExhaustiveSequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq()) extends SequentialInterpreter with Product with Serializable

    Sequential interpreter that explores branching tactics exhaustively, regardless of failure of some.

  45. case class ExpandDef(expr: DefExpression) extends BelleExpr with Product with Serializable

    Expands a function or predicate.

  46. case class Find(goal: Int, shape: Option[Expression], start: Position, exact: Boolean = true) 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).

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

  48. class FreshPostUnificationMatch extends SchematicUnificationMatch

    Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms).

    Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms). Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast 1.5-pass matcher gathering uncomposed unifiers with a subsequent post-processing pass preparing for the after renaming.

    Note

    Expects shape to have fresh names that do not occur in the input. Usually shape has all built-in names ending in underscore _ and no input is like that.

  49. class FreshUnificationMatch extends SchematicUnificationMatch

    Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms).

    Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms). Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher.

    Note

    Expects shape to have fresh names that do not occur in the input. Usually shape has all built-in names ending in underscore _ and no input is like that.

  50. trait IOListener extends AnyRef

    Listeners for input/output results during the interpretation of Bellerophon tactic expressions.

  51. abstract case class InputTactic(name: String, inputs: Seq[Any]) extends BelleExpr with NamedBelleExpr with Product with Serializable
  52. trait InsistentMatcher extends Matcher

    A matcher that insists on always matching as if there were arbitrary expressions as opposed to specializing to Term versus Formula etc.

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

  54. case class LabelBranch(label: BelleLabel) extends BelleExpr with Product with Serializable
  55. abstract class LabelledGoalsDependentTactic extends DependentTactic with Logging
  56. case class LastAnte(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable

    'Llast Locates the last position in the antecedent.

  57. case class LastSucc(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable

    'Rlast Locates the last position in the succedent.

  58. case class LazySequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq()) extends SequentialInterpreter with Product with Serializable

    Sequential interpreter that stops exploring branching on the first failing branch.

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

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

  61. trait Matcher extends (Expression, Expression) ⇒ RenUSubst with Logging

    Matcher(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa.

    Matcher(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape.

  62. final case class MultiRename(rens: Seq[(Variable, Variable)]) extends (Expression) ⇒ Expression with Product with Serializable

    Uniformly rename multiple variables at once.

    Uniformly rename multiple variables at once. Uniformly all occurrences of what and what' to repl and repl' and vice versa, for all (what,repl) in renames.

    Performs semantic renaming, i.e. leaves program constants etc. unmodified.

    See also

    edu.cmu.cs.ls.keymaerax.core.URename

  63. trait NamedBelleExpr extends BelleExpr

    A BelleExpr that has a proper code name, so is not just used internally during application.

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

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

  66. sealed case class PosInExpr(pos: List[Int] = Nil) extends Product with Serializable

    Positions identify subexpressions of an expression.

    Positions identify subexpressions of an expression. A position is a finite sequence of binary numbers where 0 identifies the left or only subexpression of an expression and 1 identifies the right subexpression of an expression.

    Example:
    1. import StringConverter._
      val fml = "(x>2 & x+1<9) -> [x:=2*x+1; y:=0;] x^2>=2".asFormula
      // explicitly use FormulaAugmentor
      print(FormulaAugmentor(fml).sub(PosInExpr(0::0::Nil)))        // x>2
      
      // implicitly use FormulaAugmentor functions on formulas
      import Augmentors._
      print(fml.sub(PosInExpr(0::0::Nil)))        // x>2;
      
      print(fml.sub(PosInExpr(0::1::Nil)))        // x+1<9
      print(fml.sub(PosInExpr(0::1::0::Nil)))     // x+1
      print(fml.sub(PosInExpr(0::1::0::0::Nil)))  // x
      print(fml.sub(PosInExpr(0::1::0::1::Nil)))  // 1
      print(fml.sub(PosInExpr(0::1::1::Nil)))     // 9
      print(fml.sub(PosInExpr(1::1::Nil)))        // x^2>=2
      print(fml.sub(PosInExpr(1::0::Nil)))        // x:=2*x+1; y:=0;
      print(fml.sub(PosInExpr(1::0::0::Nil)))     // x:=2*x+1;
      print(fml.sub(PosInExpr(1::0::1::Nil)))     // y:=0;
      print(fml.sub(PosInExpr(1::0::0::1::Nil)))  // 2*x+1
    See also

    edu.cmu.cs.ls.keymaerax.btactics.Augmentors

    edu.cmu.cs.ls.keymaerax.btactics.Context.splitPos()

    edu.cmu.cs.ls.keymaerax.btactics.Context.replaceAt()

    edu.cmu.cs.ls.keymaerax.btactics.Context.at()

    edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.positionOf()

  67. sealed trait Position extends AnyRef

    Position at which formula and subexpresion ofa a sequent to apply a tactic.

    Position at which formula and subexpresion ofa a sequent to apply a tactic.

    To do

    Position should essentially become a nice type-preserving name for a pair of a SeqPos and a PosInExpr.

    use AntePos and SuccPos directly instead of index etc.

    See also

    edu.cmu.cs.ls.keymaerax.core.SeqPos

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

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

  70. class ReflectiveExpressionBuilderExn extends Exception

    Exceptions raised by the reflective expression builder on unexpected tactics/arguments.

  71. sealed abstract class RenUSubst extends (Expression) ⇒ Expression

    Renaming Uniform Substitution, combining URename and USubst.

    Renaming Uniform Substitution, combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.Augmentors.ProgramAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.btactics.Augmentors.FormulaAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.btactics.Augmentors.TermAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.core.USubst

    edu.cmu.cs.ls.keymaerax.core.URename

  72. case class RepeatTactic(child: BelleExpr, times: Int) extends BelleExpr with Product with Serializable
  73. case class ReplacementBelleContext(t: BelleExpr) extends BelleContext with Product with Serializable
  74. case class SaturateTactic(child: BelleExpr) extends BelleExpr with Product with Serializable
  75. abstract class SchematicUnificationMatch extends BaseMatcher

    Generic schematic unification/matching algorithm for tactics.

    Generic schematic unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher. Defined by recursive unification from compositions.

  76. 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 abbr of the resulting provable which corresponds to having run USubst(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 instantiation inst in the first place.

    abbr

    the abbreviation to instantie, which should be fresh in the Provable

    See also

    NoProverException

    Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017. Example 32.

    ProvableSig.apply(USubst)

  77. case class SeqTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable
  78. abstract class SequentialInterpreter extends Interpreter with Logging

    Sequential interpreter for Bellerophon tactic expressions.

  79. abstract class SingleGoalDependentTactic extends DependentTactic
  80. case class SpoonFeedingInterpreter(rootProofId: Int, startStepIndex: Int, idProvider: (ProvableSig) ⇒ Int, listenerFactory: (Int) ⇒ (String, Int, Int) ⇒ Seq[IOListener], inner: (Seq[IOListener]) ⇒ Interpreter, descend: Int = 0, strict: Boolean = true) 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).

  81. abstract class StringInputTactic extends BuiltInTactic
  82. trait SuccPosition extends Position

    A position guaranteed to identify a succedent position

    A position guaranteed to identify a succedent position

    See also

    SuccPos

  83. class TacticComparator[T <: BelleExpr] extends AnyRef
  84. trait TopAntePosition extends AntePosition with TopPosition

    A top-level anteedent position

  85. trait TopPosition extends Position

    A position guaranteed to identify a top-level position

  86. trait TopSuccPosition extends SuccPosition with TopPosition

    A top-level succedent position

  87. final class USubstAboveURen extends RenUSubst

    Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.

    Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.

    s(RG) |- s(RD)
    -------------- USubst
      RG  |- RD
    -------------- URen
       G  |- D
    Note

    reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.

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

  89. final case class USubstRen(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable

    Renaming Uniform Substitution, simultaneously combining URename and USubst.

    Renaming Uniform Substitution, simultaneously combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution, simultaneously.

    Note

    This implementation performs semantic renaming.

    See also

    MultiRename

    edu.cmu.cs.ls.keymaerax.core.USubst

    edu.cmu.cs.ls.keymaerax.core.URename

  90. case class UnificationException(e1: String, e2: String, info: String = "") extends BelleThrowable with Product with Serializable
  91. class UnificationMatchBase extends SchematicUnificationMatch

    Generic base for unification/matching algorithm for tactics.

    Generic base for unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher.

  92. class UnificationMatchURenAboveUSubst extends Matcher

    Unification/matching algorithm for tactics for URenAboveUSubst.

    Unification/matching algorithm for tactics for URenAboveUSubst. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape.

  93. class UnificationMatchUSubstAboveURen extends Matcher
  94. case class AppliedDependentTwoPositionTactic(t: DependentTwoPositionTactic, p1: Position, p2: Position) extends BelleExpr with Product with Serializable
    Annotations
    @deprecated
    Deprecated
  95. trait BelleType extends AnyRef

    Annotations
    @deprecated
    Deprecated

    remove

    To do

    eisegesis -- simple types

  96. abstract case class DependentTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
    Annotations
    @deprecated
    Deprecated
  97. case class PartialTactic(child: BelleExpr, label: Option[BelleLabel] = None) extends BelleExpr with Product with Serializable

    A partial tactic is allowed to leave its subgoals around as unproved

    A partial tactic is allowed to leave its subgoals around as unproved

    Annotations
    @deprecated
    Deprecated

    (Since version 4.2) Replace with something else -- either assertProved or some sort of branch indicator?

  98. case class ProveAs(lemmaName: String, f: Formula, e: BelleExpr) extends BelleExpr with Product with Serializable
    Annotations
    @deprecated
    Deprecated

    (Since version 4.2) Does not work with useAt, which was the only point. There's also no way to print/parse ProveAs correctly, and scoping is global. So ProveAs should be replaced with something more systematic.

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

  100. case class TheType() extends BelleType with Product with Serializable
    Annotations
    @deprecated
    Deprecated

    remove

Value Members

  1. object AntePosition
  2. object BelleDot extends BelleDot
  3. object BelleExpr
  4. object BelleInterpreter extends Interpreter

    Provides the interpreter for running tactics.

  5. object Find extends Serializable
  6. object Fixed extends Serializable
  7. object IOListeners

    Some tactic listeners.

    Some tactic listeners. Created by smitsch on 9/3/17.

  8. object NonSubstUnificationMatch extends FreshUnificationMatch

    Unify any term for variables in ODEs.

  9. object PosInExpr extends Serializable
  10. object Position
  11. object ReflectiveExpressionBuilder extends Logging

    Constructs a edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr from a tactic name

  12. object RenUSubst
  13. object SuccPosition
  14. object TacticComparator
  15. 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.

  16. object TacticStatistics

    Computes tactic statistics (e.g., size).

  17. 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.AxiomIndex

  18. object USubstRen extends Serializable
  19. object UnificationMatch extends FreshUnificationMatch

    Unification/matching algorithm for tactics.

    Unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape.

Inherited from AnyRef

Inherited from Any

Ungrouped