Module AltErgoLib.Typed

Annotations

type ('a, 'b) annoted = {
c : 'a;
annot : 'b;
}

An annoted structure. Usually used to annotate terms.

val new_id : unit -> int

Generate a new, fresh integer (useful for annotations).

val mk : ?⁠annot:int -> 'a -> ('a, int) annoted

Create an annoted value with the given annotation. If no annotation is given, a fresh annotation is generated using new_id.

Terms and formulas

type tconstant =
| Tint of string

An integer constant.

| Treal of Num.num

Real constant.

| Tbitv of string

Bitvector constant.

| Ttrue

The true boolean (or proposition ?)

| Tfalse

The false boolean

| Tvoid

The only value of type unit

Typed constants.

type oplogic =
| OPand

conjunction

| OPor

disjunction

| OPxor

exclusive disjunction

| OPimp

implication

| OPnot

negation

| OPiff

equivalence

| OPif

conditional branching

Logic operators.

type pattern =
| Constr of {
name : Hstring.t;
args : (Var.t * Hstring.t * Ty.t) list;
}
| Var of Var.t
type 'a tterm = {
tt_ty : Ty.t;

type of the term

tt_desc : 'a tt_desc;

term descriptor

}

Typed terms. Polymorphic in the annotation: an 'a tterm is a term annoted with values of type 'a.

and 'a atterm = ('a tterm'a) annoted

type alias for annoted typed terms.

and 'a tt_desc =
| TTconst of tconstant

Term constant

| TTvar of Symbols.t

Term variables

| TTinfix of 'a atterm * Symbols.t * 'a atterm

Infix symbol application

| TTprefix of Symbols.t * 'a atterm

Prefix symbol application

| TTapp of Symbols.t * 'a atterm list

Arbitrary symbol application

| TTmapsTo of Var.t * 'a atterm

Used in semantic triggers for floating point arithmetic. See sources/preludes/fpa-theory-2017-01-04-16h00.ae

| TTinInterval of 'a atterm * Symbols.bound * Symbols.bound

Represent floating point intervals (used for triggers in Floating point arithmetic theory). TTinInterval (lower, l_strict, t, upper, u_strict) is a constraint stating that term t is in the interval lower, upper, and that the lower (resp. upper) bound is strict iff l_strict (resp. u_strict) is true.

| TTget of 'a atterm * 'a atterm

Get operation on arrays

| TTset of 'a atterm * 'a atterm * 'a atterm

Set operation on arrays

| TTextract of 'a atterm * 'a atterm * 'a atterm

Extract a sub-bitvector

| TTconcat of 'a atterm * 'a atterm
| TTdot of 'a atterm * Hstring.t

Field access on structs/records

| TTrecord of (Hstring.t * 'a atterm) list

Record creation.

| TTlet of (Symbols.t * 'a atterm) list * 'a atterm

Let-bindings. Accept a list of mutually recursive le-bindings.

| TTnamed of Hstring.t * 'a atterm

Attach a label to a term.

| TTite of 'a atform * 'a atterm * 'a atterm

Conditional branching, of the form TTite (condition, then_branch, else_branch).

| TTproject of bool * 'a atterm * Hstring.t

Field (conditional) access on ADTs. The boolean is true when the projection is 'guarded' and cannot be simplified (because functions are total)

| TTmatch of 'a atterm * (pattern * 'a atterm) list

pattern matching on ADTs

| TTform of 'a atform

formulas inside terms: simple way to add them without making a lot of changes

Typed terms descriptors.

and 'a atatom = ('a tatom'a) annoted

Type alias for annoted typed atoms.

and 'a tatom =
| TAtrue

The true atom

| TAfalse

The false atom

| TAeq of 'a atterm list

Equality of a set of typed terms.

| TAdistinct of 'a atterm list

Disequality. All terms in the set are pairwise distinct.

| TAneq of 'a atterm list

Equality negation: at least two elements in the list are not equal.

| TAle of 'a atterm list

Arithmetic ordering: lesser or equal. Chained on lists of terms.

| TAlt of 'a atterm list

Strict arithmetic ordering: less than. Chained on lists of terms.

| TApred of 'a atterm * bool

Term predicate, negated if the boolean is true. TApred (t, negated) is satisfied iff t <=> not negated

| TTisConstr of 'a atterm * Hstring.t

Test if the given term's head symbol is identitical to the provided ADT consturctor

and 'a quant_form = {
qf_bvars : (Symbols.t * Ty.t) list;

Variables that are quantified by this formula.

qf_upvars : (Symbols.t * Ty.t) list;

Free variables that occur in the formula.

qf_triggers : ('a atterm list * bool) list;

Triggers associated wiht the formula. For each trigger, the boolean specifies whether the trigger was given in the input file (compared to inferred).

qf_hyp : 'a atform list;

Hypotheses of axioms with semantic triggers in FPA theory. Typically, these hypotheses reduce to TRUE after instantiation

qf_form : 'a atform;

The quantified formula.

}

Quantified formulas.

and 'a atform = ('a tform'a) annoted

Type alias for typed annoted formulas.

and 'a tform =
| TFatom of 'a atatom

Atomic formula.

| TFop of oplogic * 'a atform list

Application of logical operators.

| TFforall of 'a quant_form

Universal quantification.

| TFexists of 'a quant_form

Existencial quantification.

| TFlet of (Symbols.t * Ty.t) list * (Symbols.t * 'a tlet_kind) list * 'a atform

Let binding. TODO: what is in the first list ?

| TFnamed of Hstring.t * 'a atform

Attach a name to a formula.

| TFmatch of 'a atterm * (pattern * 'a atform) list

pattern matching on ADTs

and 'a tlet_kind =
| TletTerm of 'a atterm

Term let-binding

| TletForm of 'a atform

Formula let-binding

The different kinds of let-bindings, whether they bind terms or formulas.

Declarations

type 'a rwt_rule = {
rwt_vars : (Symbols.t * Ty.t) list;

Variables of the rewrite rule

rwt_left : 'a;

Left side of the rewrite rule (aka pattern).

rwt_right : 'a;

Right side of the rewrite rule.

}

Rewrite rules. Polymorphic to allow for different representation of terms.

type goal_sort =
| Cut

Introduce a cut in a goal. Once the cut proved, it's added as a hypothesis.

| Check

Check if some intermediate assertion is prouvable

| Thm

The goal to be proved

Goal sort. Used in typed declarations.

val fresh_hypothesis_name : goal_sort -> string

create a fresh hypothesis name given a goal sort.

val is_local_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, answers whether the name design a local hypothesis ?

val is_global_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, does the name design a global hypothesis ?

type tlogic_type =
| TPredicate of Ty.t list

Predicate type declarations

| TFunction of Ty.t list * Ty.t

Function type declarations

Type declarations. Specifies the list of argument types, as well as the return type for functions (predicate implicitly returns a proposition, so there is no need for an explicit return type).

type 'a atdecl = ('a tdecl'a) annoted

Type alias for annoted typed declarations.

and 'a tdecl =
| TTheory of Loc.t * string * Util.theories_extensions * 'a atdecl list

Theory declarations. The list of declarations in a Theory may only contain Axioms.

| TAxiom of Loc.t * string * Util.axiom_kind * 'a atform

New axiom that can be used in proofs.

| TRewriting of Loc.t * string * 'a atterm rwt_rule list

New rewrite rule that can be used.

| TGoal of Loc.t * goal_sort * string * 'a atform

New goal to prove.

| TLogic of Loc.t * string list * tlogic_type

Function (or predicate) type declaration.

| TPredicate_def of Loc.t * string * (string * Ty.t) list * 'a atform

Predicate definition. TPredicate_def (loc, name, vars, body) defines a predicate fun vars => body.

| TFunction_def of Loc.t * string * (string * Ty.t) list * Ty.t * 'a atform

Predicate definition. TPredicate_def (loc, name, vars, ret, body) defines a function fun vars => body, where body has type ret.

| TTypeDecl of Loc.t * Ty.t

New type declaration. TTypeDecl (loc, vars, t, body) declares a type t, with parameters vars, and with contents body. This new type may either be abstract, a record type, or an enumeration.

| TPush of Loc.t * int

push (loc,n) pushs n new assertions levels onto the assertion stack

| TPop of Loc.t * int

pop (loc,n) pops n assertions levels from the assertion stack

Printing
val print_term : Stdlib.Format.formatter -> _ atterm -> unit

Print annoted typed terms. Ignore the annotations.

val print_formula : Stdlib.Format.formatter -> _ atform -> unit

Print annoted typed formulas; Ignores the annotations.

val print_binders : Stdlib.Format.formatter -> (Symbols.t * Ty.t) list -> unit

Print a list of bound typed variables.

val print_triggers : Stdlib.Format.formatter -> ('a atterm list * bool) list -> unit

Print a list of triggers.

val print_goal_sort : Stdlib.Format.formatter -> goal_sort -> unit

Print a goal sort

val print_rwt : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a rwt_rule -> unit

Print a rewrite rule