Type Members

1.  case class Assertion(kind: String, _formula: Expr) extends Group with Product with Serializable

   formula can have free variables

2.  sealed trait AssumingDecl extends AnyRef

   a declaration in the assumptions of a theory, essentially formal parameters of axiom flavor and some auxiliary declarations

   a declaration in the assumptions of a theory, essentially formal parameters of axiom flavor and some auxiliary declarations

   This is the same as Decl except for also allowing assumptions (= axioms).

3.  case class ChainedDecl(named: NamedDecl, chain_p: Boolean, semi_colon_p: Boolean) extends Group with Product with Serializable

   like NamedDecl but may be chained

4.  sealed trait Decl extends AssumingDecl

   a declaration in the body of theory

5.  case class DeclaredType(_declared: Type, _internal: Type) extends Group with Product with Serializable

6.  sealed trait Expr extends Object with assignment_arg
7.  sealed trait FormalParameter extends AnyRef

   a declaration in the list of parameters of a theory declaration

   a declaration in the list of parameters of a theory declaration

   This is essentially a subtype of Decl, but the Decl counterparts are general.

8.  case class InlineDatatypeBody(named: NamedDecl, arg_formals: List[bindings], _constructors: List[constructor]) extends Group with Product with Serializable

   an ADT-like datatype declared inside a theory, see also TopDatatypeBody

9.  trait Judgement extends Decl

   named theorem-flavor statement in the meta-logic

10.  trait Module extends AnyRef

    toplevel declarations

11.  case class NamedDecl(id: String, place: String, decl_formals: List[FormalParameter]) extends Group with Product with Serializable

    common parts of a named declaration in a theory

12.  case class NonEmptiness(nonempty_p: Boolean, contains: Option[Expr]) extends Group with Product with Serializable
13.  sealed trait Object extends AnyRef

    PVS objects are theories, types, and expressions

14.  case class OptNamedDecl(id: Option[String], place: String, formals: List[FormalParameter], semi_colon_p: Boolean) extends Group with Product with Serializable

    formal parameters only allowed if optional id is given

15.  sealed trait TheoryExpr extends Object

    the only theory expressions are references (names) however, those subsume instantiation of parameters and declarations

16.  case class TopDatatypeBody(named: NamedDecl, theory_formals: List[FormalParameter], importings: List[importing], _constructors: List[constructor]) extends Group with Product with Serializable

    an ADT-like datatype declared at toplevel, see also InlineDatatypeBody

    an ADT-like datatype declared at toplevel, see also InlineDatatypeBody

    for historical reasons, imports can occur separately in addition to within formals although that is redundant

17.  sealed trait Type extends Object with domain

    PVS types

18.  case class UnnamedDecl(place: String, chain_p: Boolean, semi_colon_p: Boolean) extends Group with Product with Serializable

    common parts of an unnamed declaration in a theory

19.  case class accessor(named: NamedDecl, _type: Type) extends Product with Serializable
20.  case class application(place: String, _fun: Expr, _arg: Expr, infix: Boolean) extends Expr with Product with Serializable

    function application

21.  case class application_judgement(named: OptNamedDecl, _name: name_expr, arg_formals: List[bindings], tp: DeclaredType) extends Judgement with Product with Serializable

    p: |- name(arg_formals) : A

22.  case class assignment(place: String, assignment_args: List[assignment_arg], _expr: Expr) extends update_assignment with Product with Serializable
23.  sealed trait assignment_arg extends AnyRef

24.  case class assumption(named: ChainedDecl, assertion: Assertion) extends AssumingDecl with Product with Serializable

    a: F for a formula F (semantically, an axiom in the list of formal parameters, becomes tcc when instantiating the theory)

25.  case class auto_rewrite(unnamed: UnnamedDecl, key: String, kind: String, _rewrite_name: List[rewrite_name]) extends Decl with Product with Serializable

    name of a formula that is loaded as a conditional rewrite rule

26.  case class axiom_decl(named: ChainedDecl, assertion: Assertion) extends Decl with Product with Serializable

    a: F for a formula F

27.  case class binding(id: String, named: ChainedDecl, _type: Type) extends domain with Product with Serializable
28.  case class bindings(_bindings: List[binding]) extends Product with Serializable

    list of variable bindings

29.  case class cases_expr(place: String, _expr: Expr, _selections: List[selection]) extends Expr with Product with Serializable

    one-level pattern matching of an expression against a list of cases

30.  case class codatatype(body: TopDatatypeBody) extends Module with Product with Serializable

    a top-level datatype with greatest fixed point semantics

31.  case class coercion_expr(place: String, _of: Expr, _to: Type) extends Expr with Product with Serializable

    (a :: A), coerce a to A, which must be compatible with the type of a

32.  case class coind_decl(named: NamedDecl, arg_formals: List[bindings], tp: DeclaredType, _body: Expr) extends Decl with Product with Serializable

    coinductive definition

33.  case class cond(_if: Expr, _then: Expr) extends Product with Serializable

    if -> then (case in a condition expression)

34.  case class cond_expr(place: String, conditions: List[cond]) extends Expr with Product with Serializable

    condition expression, i.e., if-expression with multiple cases (checked for disjointness and exhaustiveness)

35.  case class const_decl(named: ChainedDecl, arg_formals: List[bindings], tp: DeclaredType, _def: Option[Expr]) extends Decl with Product with Serializable

    c(G) : A [= t]

36.  case class constructor(named: NamedDecl, ordnum: Int, accessors: List[accessor], recognizer: String, subtype_id: Option[String]) extends Product with Serializable

    constructor of an inductive data type

    constructor of an inductive data type

    ordnum

    constructors are numbered consecutively for convenience

37.  case class conversion_decl(unnamed: UnnamedDecl, kind: String, _expr: Expr) extends Decl with Product with Serializable

    conversion f (makes f an implicit conversion)

38.  case class cotuple_type(place: String, _arguments: List[Type]) extends Type with Product with Serializable

    A1 + ...

    A1 + ... + An

39.  case class datatype(body: TopDatatypeBody) extends Module with Product with Serializable

    a top-level datatype with least fixed point semantics

40.  case class declref(href: String) extends Product with Serializable

    attempt to represent pointers a xlinks; changed to integer-index in list of overloaded id in that theory

41.  case class def_decl(named: ChainedDecl, arg_formals: List[bindings], tp: DeclaredType, _def: Expr, _measure: Option[Expr], _order: Option[Expr]) extends Decl with Product with Serializable

    c(G) : A [= t] where c is a recursive function

42.  sealed trait domain extends AnyRef

    A domain is a type, possibly binding a variable

    A domain is a type, possibly binding a variable

    Its two cases unify the simple and dependent cases of product and function types

    The only way to create dependent types is via predicate subtypes (including declared ones).

43.  case class enumtype_decl(named: NamedDecl, enum_elts: List[id]) extends Decl with Product with Serializable
44.  case class exists_expr(place: String, bindings: List[binding], _body: Expr) extends Expr with Product with Serializable

    existential quantifier

45.  case class exporting(place: String, exporting_kind: String, exporting_names_: exporting_names, exporting_but_names_: exporting_names, exporting_theory_names: List[theory_name]) extends Product with Serializable
46.  case class exporting_names(name: List[name]) extends Group with Product with Serializable
47.  case class expr_as_type(place: String, _expr: Expr, _type: Option[Type]) extends Type with Product with Serializable

    (p): type, for a predicate p: _type = a => bool; _

48.  case class expr_judgement(named: OptNamedDecl, bindings: List[binding], _expr: Expr, tp: DeclaredType) extends Judgement with Product with Serializable

    p: |- t: A (some limitations on t)

49.  case class field_appl_expr(place: String, id: String, _expr: Expr) extends Expr with Product with Serializable

    named projection from a record

50.  case class field_assign(place: String, id: String) extends assignment_arg with Product with Serializable
51.  case class field_decl(named: NamedDecl, _type: Type) extends Product with Serializable
52.  case class forall_expr(place: String, bindings: List[binding], _body: Expr) extends Expr with Product with Serializable

    universal quantifier

53.  case class formal_const_decl(named: ChainedDecl, tp: DeclaredType) extends FormalParameter with Product with Serializable

    typed constant -- c:A for a type A

54.  case class formal_subtype_decl(named: ChainedDecl, ne: NonEmptiness, _sup: Type, _pred: const_decl) extends FormalParameter with Product with Serializable

    type with given supertype -- a TYPE FROM A for a type A

55.  case class formal_theory_decl(named: ChainedDecl, _name: theory_name) extends FormalParameter with Product with Serializable

    model of a theory -- m: T for a theory T

56.  case class formal_type_decl(named: ChainedDecl, ne: NonEmptiness) extends FormalParameter with Product with Serializable

    type -- a TYPE

57.  case class formula_decl(named: ChainedDecl, assertion: Assertion) extends Decl with Product with Serializable

    a: F for a formula F (has proof, which is not exported)

58.  case class function_type(place: String, _from: domain, _to: Type) extends Type with Product with Serializable

    A -> B or (x:A) -> B

59.  case class id(_id: String) extends Product with Serializable
60.  case class if_expr(place: String, _if: Expr, _then: Expr, _else: Expr) extends Expr with Product with Serializable

    if-then-else expression

61.  case class importing(unnamed: UnnamedDecl, _name: theory_name) extends Decl with FormalParameter with Product with Serializable

    include T, can occur in formal parameters without semantic change in case parameters already need included declarations

62.  case class ind_decl(named: NamedDecl, arg_formals: List[bindings], tp: DeclaredType, _body: Expr) extends Decl with Product with Serializable

    inductive definition

63.  case class inline_codatatype(body: InlineDatatypeBody) extends Decl with Product with Serializable

    an inline ADT with greatest fixed point semantics

64.  case class inline_datatype(body: InlineDatatypeBody) extends Decl with Product with Serializable

    an inline ADT with least fixed point semantics

65.  case class lambda_expr(place: String, bindings: List[binding], _body: Expr) extends Expr with Product with Serializable

    lambda abstraction

66.  case class let_binding(named: ChainedDecl, _type: Type, _expr: Expr) extends Product with Serializable
67.  case class let_expr(place: String, let_bindings: List[let_binding], _body: Expr) extends Expr with Product with Serializable

    let expression

68.  case class lib_decl(id: String, unnamed: UnnamedDecl, library: String) extends Decl with Product with Serializable

    assigns a short name to a library (= folder)

69.  case class list_expr(place: String, _arguments: List[Expr]) extends Expr with Product with Serializable

    list

70.  case class macro_decl(named: ChainedDecl, arg_formals: List[bindings], tp: DeclaredType, _def: Option[Expr]) extends Decl with Product with Serializable

    defined constant that is always expanded

71.  case class maplet(place: String, assignment_args: List[assignment_arg], _expr: Expr) extends update_assignment with Product with Serializable
72.  sealed trait mapping extends AnyRef

    superclass of instantiations and renaming when forming theories

73.  case class mapping_rename(mapping_rhs: name, mapping_lhs: Object) extends mapping with Product with Serializable

    c ~> c'

74.  case class mapping_subst(mapping_rhs: name, mapping_lhs: Object) extends mapping with Product with Serializable

    c := c'

75.  case class name(id: String, theory_id: String, library_id: String, mappings: List[mapping], target: Option[theory_name], actuals: List[Object], dactuals: List[Object]) extends Group with Product with Serializable

    user-provided reference to a symbol

    user-provided reference to a symbol

    id

    theory name

    library_id

    library (in particular, as declared by lib_decl)

    mappings

    instantiations/renaming for

    target

    abbreviation for substituting a set of names at once by the declarations of the same local name in a different theory

    actuals

    instantiations for the formal parameters (positional, full)

76.  case class name_expr(place: String, name: name, _type: Option[Type], _resolution: resolution) extends Expr with Product with Serializable

    reference to a declared name

    reference to a declared name

    name

    the user-provided reference

    _type

    the type disambiguating overloading (can be computed from resolution)

77.  case class name_judgement(named: OptNamedDecl, _name: name_expr, tp: DeclaredType) extends Judgement with Product with Serializable

    p: |- name: A (special case of expr_judgement)

78.  case class number_expr(place: String, _num: BigInt) extends Expr with Product with Serializable

    number literal

79.  case class number_judgement(named: OptNamedDecl, _number: number_expr, tp: DeclaredType) extends Judgement with Product with Serializable

    p: |- number: A (special case of expr_judgement)

80.  case class proj_appl_expr(place: String, _expr: Expr, index: Int) extends Expr with Product with Serializable

    n-th projection applied to an argument

81.  case class proj_assign(place: String, _index: Int) extends assignment_arg with Product with Serializable
82.  case class proj_expr(place: String, _index: Int) extends Expr with Product with Serializable

    n-th projection (as a polymorphic function, turned into lambda with fresh type variable by type checker)

83.  case class pvs_file(_modules: List[Module]) extends Product with Serializable

    a pvs file containing some modules

84.  case class rational_expr(place: String, _s: String) extends Expr with Product with Serializable

    rational literal

85.  case class record_expr(place: String, _assignments: List[assignment]) extends Expr with Product with Serializable

    record

86.  case class record_type(place: String, _fields: List[field_decl]) extends Type with Product with Serializable

    {f1:A1, ..., fn: An}

87.  case class resolution(_theory: theory_name, index: Int) extends Product with Serializable

    internal resolution of an overloaded declaration (including formal parameters) of a theory

    internal resolution of an overloaded declaration (including formal parameters) of a theory

    index

    the position in the list of overloaded declarations in that theory, starting from 0

88.  case class rewrite_name(place: String, kind: Option[String], name: name, _res: Option[resolution], _spec: Option[rewrite_name_spec]) extends Product with Serializable

    reference to a formula that is to be used in rewriting

89.  case class rewrite_name_spec() extends Product with Serializable

    user-provided information for disambiguation in a rewrite_name

90.  case class selection(place: String, _cons: name_expr, bindings: List[binding], _expr: Expr) extends Product with Serializable

    case in a case expression -- cons(bindings) : _expr

91.  case class set_expr(place: String, bindings: List[binding], _body: Expr) extends Expr with Product with Serializable

    equal to lambda, convenience for using predicates as (expression-level) sets

92.  case class setsubtype(place: String, _type: Type, _by: Expr) extends Type with Product with Serializable

    predicate subtype -- A|F, e.g., A | lambda x:A|F

93.  case class string_expr(place: String, _str: String) extends Expr with Product with Serializable

    string literal

94.  case class subtype_judgement(named: OptNamedDecl, sub: DeclaredType, sup: DeclaredType) extends Judgement with Product with Serializable

    p: |- A <: B

95.  case class table_expr(place: String) extends Expr with Product with Serializable

    table expressions, similar to 2-dimensional arrays

96.  case class tcc_decl(named: ChainedDecl, assertion: Assertion) extends Decl with Product with Serializable

    a: F for a formula (for a proof obligation, prepended to a declaration by the type checker)

97.  case class theory(named: NamedDecl, theory_formals: List[FormalParameter], assuming: List[AssumingDecl], exporting_: Option[exporting], _decls: List[Decl]) extends Module with Product with Serializable
98.  case class theory_decl(named: ChainedDecl, _domain: theory_name) extends Decl with Product with Serializable

    named import (parameters, instantiations, and renamings are part of the name); rnc to be revisited

99.  case class theory_name(place: String, id: String, library_id: String, mappings: List[mapping], target: Option[theory_name], actuals: List[Object], dactuals: List[Object]) extends TheoryExpr with Product with Serializable

    user-provided reference to a module

    user-provided reference to a module

    id

    theory name

    library_id

    library (in particular, as declared by lib_decl)

    mappings

    instantiations/renaming for

100.  case class tuple_expr(place: String, _arguments: List[Expr]) extends Expr with Product with Serializable

     tuple

101.  case class tuple_type(place: String, _domains: List[domain]) extends Type with Product with Serializable

     flexary, possibly dependent product -- e.g., A1 * (x2:A2) * ...

     flexary, possibly dependent product -- e.g., A1 * (x2:A2) * ... * An

102.  case class type_application(place: String, _type: type_name, _arguments: List[Expr]) extends Type with Product with Serializable

     a(args)

103.  case class type_decl(named: ChainedDecl, nonempty_p: Boolean) extends Decl with Product with Serializable

     a TYPE (may be asserted to be non-empty

104.  case class type_def_decl(named: NamedDecl, ne: NonEmptiness, arg_formals: List[bindings], df: DeclaredType) extends Decl with Product with Serializable

     a(arg_formals) TYPE = A (defined types may be dependent)

105.  case class type_extension(place: String, _type: Type, _by: Type) extends Type with Product with Serializable
106.  case class type_from_decl(named: ChainedDecl, nonempty_p: Boolean, tp: DeclaredType) extends Decl with Product with Serializable

     a TYPE FROM A (a is subtype of A)

107.  case class type_name(place: String, name: name, _res: Option[resolution]) extends Type with Product with Serializable

     a

108.  sealed trait update_assignment extends AnyRef
109.  case class update_expr(place: String, _exp: Expr, assignments: List[update_assignment]) extends Expr with Product with Serializable

     change value in a tuple, record, or function

110.  case class var_decl(id: String, unnamed: UnnamedDecl, tp: DeclaredType) extends Decl with Product with Serializable

     x: A (declares type of future variables)

111.  case class varname_expr(place: String, id: String, _type: Type) extends Expr with Product with Serializable