Packages

trait Interpreter extends AnyRef

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

Linear Supertypes
AnyRef, Any
Known Subclasses
BelleBaseInterpreter, BelleInterpreter, ConcurrentInterpreter, ExhaustiveSequentialInterpreter, LazySequentialInterpreter, SequentialInterpreter, SpoonFeedingInterpreter
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Interpreter
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def apply(expr: BelleExpr, v: BelleValue): BelleValue

    Returns the result of applying tactic expr to the proof value v (usually a provable).

    Returns the result of applying tactic expr to the proof value v (usually a provable). Interpreter must be started before executing tactics.

  2. abstract def isDead: Boolean

    Indicates whether the interpreter is still operational.

    Indicates whether the interpreter is still operational. A dead interpreter refuses to run tactics.

  3. abstract def kill(): Unit

    Stops the interpreter and kills all its tactic executions.

  4. abstract def listeners: Seq[IOListener]

    Registered listeners.

  5. abstract def start(): Unit

    Starts the interpreter.

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def applySubDerivation(original: ProvableSig, n: Int, subderivation: ProvableSig, subst: USubst): (Boolean, ProvableSig)

    Replaces the nth subgoal of original with the remaining subgoals of subderivation.

    Replaces the nth subgoal of original with the remaining subgoals of subderivation.

    original

    A Provable whose nth subgoal is equal to the conclusion of subderivation (modulo substitution).

    n

    The numerical index of the subgoal of original to rewrite (Seqs are zero-indexed)

    subderivation

    The provable to replace the original subgoal.

    returns

    A tuple of: * Indicator whether original and subderivation were merged. * A new provable that is identical to original, except that the nth subgoal is replaced with the remaining subgoals of subderivation.

    Attributes
    protected
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def assertConclusionsMatchModuloConstification(parent: ProvableSig, sub: ProvableSig, subst: USubst): Unit

    Assert that the conclusion of provable sub matches the conclusion of provable parent either verbatim or modulo constification renaming that is assumed to be applied in the future.

    Assert that the conclusion of provable sub matches the conclusion of provable parent either verbatim or modulo constification renaming that is assumed to be applied in the future.

    Attributes
    protected
  7. def assertSubMatchesModuloConstification(parent: ProvableSig, sub: ProvableSig, n: Int, subst: USubst): Unit

    Assert that the conclusion of provable sub matches the subgoal n of provable parent either verbatim or modulo constification renaming that is assumed to be applied in the future.

    Assert that the conclusion of provable sub matches the subgoal n of provable parent either verbatim or modulo constification renaming that is assumed to be applied in the future. Constification renaming requires parent to have exactly one single subgoal.

    Attributes
    protected
  8. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  9. def collectSubst(goal: Sequent, have: Sequent, haveIsProved: Boolean, defs: Declaration): USubst

    Collects substitutions (of defs) that are needed to make have fit goal.

    Collects substitutions (of defs) that are needed to make have fit goal.

    Attributes
    protected
  10. def collectSubst(goal: ProvableSig, i: Int, sub: ProvableSig): USubst

    Collects substitutions (of defs) that are needed to make sub fit the i-th subgoal of goal.

    Collects substitutions (of defs) that are needed to make sub fit the i-th subgoal of goal.

    Attributes
    protected
  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  13. def exhaustiveSubst(p: ProvableSig, s: USubst): ProvableSig

    Applies substitutions s to provable p exhaustively.

    Applies substitutions s to provable p exhaustively.

    Attributes
    protected
  14. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  15. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. lazy val nilNames: List[String]

    Names of nil tactics.

    Names of nil tactics.

    Attributes
    protected
  20. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. def progress(prev: BelleValue, curr: BelleValue): Boolean

    Compares provables ignoring labels.

    Compares provables ignoring labels.

    Attributes
    protected
  23. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  24. def toString(): String
    Definition Classes
    AnyRef → Any
  25. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped