# Module `AltErgoLib.Typed`

### Annotations

### 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 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 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 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

### 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).

`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