Packages

case class Context(s: Statement) extends Product with Serializable

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Context
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Context(s: Statement)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def --(other: Context): Context

    Compute the "difference" between two contexts.

    Compute the "difference" between two contexts. A "difference" only exists if the underlying statement of other is a "prefix" of this, and consists of statements in this which remain after deleting the prefix other. When this is a branching proof (e.g. Switch), we consider other a prefix even if other is currently proving some branch of the switch. An exception is thrown if the difference does not exist.

  4. def :+(other: Statement): Context

    Add s to the "end" of the context.

  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. def add(x: Ident, fml: Formula): Context

    Add an assumption to the context

  7. def asElaborationContext: Context

    Clone this context with the elaboration flag set

  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def bakePhi: Context
  10. def clone(): Context

    Copy this context to provide persistent interface

    Copy this context to provide persistent interface

    Definition Classes
    Context → AnyRef
  11. def contains(id: Ident): Boolean

    Does the context contain a fact named id?

  12. def deletePhi: Context
  13. def elabFunctionETF(node: ASTNode): ExpressionTraversalFunction
  14. def elaborateFunctions(pt: ProofTerm, node: ASTNode): ProofTerm
  15. def elaborateFunctions(e: Expression, node: ASTNode): Expression
  16. def elaborateFunctions(prog: Program, node: ASTNode): Program
  17. def elaborateFunctions(fml: Formula, node: ASTNode): Formula
  18. def elaborateFunctions(f: Term, node: ASTNode): Term

    Elaborate user-defined functions in an expression

  19. def elaborateStable(pt: ProofTerm): ProofTerm
  20. def elaborateStable(e: Expression): Expression
  21. def elaborateStable(f: Term): Term
  22. def elaborateStable(f: Formula): Formula

    Final elaboration step used in proof-checker.

  23. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  25. def findAll(cq: ContextQuery): ContextResult
  26. def fresh(ident: String = ghostVar): Ident

    returns

    A proof variable name which is not bound in the context.

  27. def get(id: Ident, wantProgramVar: Boolean = false, isSound: Boolean = true): Option[Formula]
  28. def getAssignments(x: Variable): List[Formula]

    Return all assignments which mention any variant of "x"

  29. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  30. def getFor: Option[For]
  31. def getHere(id: Ident, wantProgramVar: Boolean = false): Option[Formula]
  32. def getMentions(x: Variable): List[Formula]
  33. def ghost(f: Formula): Context

    Bind the next ghost variable to formula f

  34. def inferGuardDelta(asrt: Assert): Term
  35. def isElaborationContext: Boolean

    Does this context represent an elaboration pass?

  36. def isEmpty: Boolean
  37. def isGhost: Boolean

    Are we checking a statement which appears as a forward ghost?

  38. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  39. def isInverseGhost: Boolean

    Are we checking a statement which appears as an inverse ghost?

  40. def lastBlock: Block

    Used in proof statements such as ProveODE which have not only implicit assumptions but which need to consider immediately preceding assignments.

    Used in proof statements such as ProveODE which have not only implicit assumptions but which need to consider immediately preceding assignments. The lastBlock can include straight-line assignments and facts, which may appear ghosted or unghosted.

  41. def lastBlockSmall: Block
  42. def lastFact: Option[(IdentPat, Formula, Formula)]

    The most recently proven fact in a context.

    The most recently proven fact in a context. Fact is returned as (ident, unelaboratedFml, elaboratedFml)

  43. def lastFacts: List[(IdentPat, Formula, Formula)]
  44. def location: Option[Int]

    Recover the "current" line and column number using the position information of the underlying statement

  45. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  46. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  47. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  48. var outer: Context
  49. def programSignature: Map[ProgramConst, Program]

    The set of program symbols defined in a statement.

    The set of program symbols defined in a statement. This includes symbols which are defined under a branch or under a binder.

  50. def rawLastFact: Option[(IdentPat, Formula)]
  51. def reapply(s: Statement): Context

    Convert input s to a context, but remember the metadata from this context

  52. val s: Statement
  53. def searchAll(cq: ContextQuery, tabooProgramVars: Set[Variable], tabooFactVars: Set[Ident]): ContextResult

    Look up definitions of a proof variable, starting with the most recent.

    Look up definitions of a proof variable, starting with the most recent. tabooProgramVars are for soundness, tabooFactVars are to avoid duplicate lookup results

  54. def sideEffect(s: Statement): Unit
  55. def signature: Map[Function, LetSym]

    The set of function symbols defined in a statement.

    The set of function symbols defined in a statement. This includes symbols which are defined under a branch or under a binder.

  56. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  57. def unify(pat: Expression): Option[(Option[Ident], Formula)]

    Return first fact that unifies with a pattern, if any.

  58. def unifyAll(pat: Expression): ContextResult

    return all facts that unify with a given pattern

  59. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  60. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  61. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  62. def withGhost: Context

    Clone this context but indicate that we are checking a ghost statement

  63. def withInverseGhost: Context

    Clone this context but indicate that we are checking an inverse ghost statement

  64. def withOuter: Context

    Remember the current context as the outer context before a recursive traversal

  65. def withoutGhost: Context

    Clone this context but indicate that we are checking a normal statement

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped