Packages

object Session

Implementation of proof sessions via the cats free monad. See http://typelevel.org/cats/datatypes/freemonad.html.

Source
Session.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Session
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type Session[A] = Free[SessionCommand, A]
  2. sealed trait SessionCommand[A] extends AnyRef

    Trait for individual session commands.

    Trait for individual session commands.

    A

    The return type of the command.

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def ask(input: SExpression): Free[SessionCommand, SExpression]

    Submits an SExpression and receives one in return.

  6. def assert(formulas: List[Formula]): Session[Unit]

    Asserts a list of formulas.

  7. def assert(f: Formula, label: String): Free[SessionCommand, Unit]

    Asserts a formula with a label.

  8. def assert(f: Formula): Free[SessionCommand, Unit]

    Asserts a formula.

  9. def checkSat: Session[Either[SExpression, Boolean]]

    Checks whether the current set of declarations and assertions is satisfiable.

  10. def checkUnsat: Session[Either[SExpression, Boolean]]

    Checks whether the current set of declarations and assertions is not satisfiable.

  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  12. def declareFun(fun: Const): Free[SessionCommand, Unit]

    Declares a function.

  13. def declareSort(sort: TBase): Free[SessionCommand, Unit]

    Declares a sort.

  14. def declareSymbolsIn(expressions: Expr*)(implicit d: DummyImplicit): Session[Unit]

    Declares all symbols (sorts and functions) in a list of Exprs.

  15. def declareSymbolsIn(expressions: IterableOnce[Expr]): Session[Unit]

    Declares all symbols (sorts and functions) in a list of Exprs.

  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  18. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  23. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  24. def pop: Free[SessionCommand, Unit]

    Pops the stack, eliminating all assertions and declarations since the last push.

  25. def pure[T](t: T): Session[T]
  26. def push: Free[SessionCommand, Unit]

    Pushes the current assertions and declarations on the stack.

  27. def setLogic(logic: String): Free[SessionCommand, Unit]

    Sets the logic to be used for the session.

  28. def setOption(option: String, args: String*): Free[SessionCommand, Unit]

    Sets an option to a value.

  29. def skip: Session[Unit]
  30. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  31. def tell(input: SExpression): Free[SessionCommand, Unit]

    Submits an SExpression without a return.

  32. def toString(): String
    Definition Classes
    AnyRef → Any
  33. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  34. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  35. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  36. def when(p: Boolean)(s: Session[Unit]): Session[Unit]
  37. def withScope[A](f: Session[A]): Session[A]

    Pushes the stack, then runs f, then pops the stack.

  38. def wrap[A](before: Session[Unit], f: Session[A], after: Session[Unit]): Session[A]

    Encloses the session f between before and after.

  39. object Runners

    Contains various functions for interpreting a value of type Session.

    Contains various functions for interpreting a value of type Session.

    A "runner" contains a natural transformation from SessionCommand to Id; i.e. a function that can transform any SessionCommand[A] to an Id[A] (= A).

    Given such a transformation comp: SessionCommand ~> Id, you can use it to interpret a session program p via p.foldMap(comp).

  40. object SessionCommand

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped