Module `AltErgoLib.Typed`Source

Typed AST

This module defines a typed AST, used to represent typed terms before they are hashconsed.

Annotations

Sourcetype ('a, 'b) annoted = {

c : 'a;
annot : 'b;

}

An annoted structure. Usually used to annotate terms.

Sourceval new_id : unit -> int

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

Sourceval 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

Sourcetype 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.

Sourcetype oplogic =

| OPand
(*
conjunction
*)
| OPor
(*
disjunction
*)
| OPxor
(*
exclusive disjunction
*)
| OPimp
(*
implication
*)
| OPnot
(*
negation
*)
| OPiff
(*
equivalence
*)
| OPif
(*
conditional branching
*)

Logic operators.

Sourcetype pattern =

| Constr of {
1. name : Hstring.t;
2. args : (Var.t * Hstring.t * Ty.t) list;
}
| Var of Var.t

Sourcetype '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.

Sourceand 'a atterm = ('a tterm, 'a) annoted

type alias for annoted typed terms.

Sourceand '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.why
*)
| 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.

Sourceand 'a atatom = ('a tatom, 'a) annoted

Type alias for annoted typed atoms.

Sourceand '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 tterm, 'a) annoted * Hstring.t
(*
Test if the given term's head symbol is identitical to the provided ADT consturctor
*)

Typed atoms.

Sourceand '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.

Sourceand 'a atform = ('a tform, 'a) annoted

Type alias for typed annoted formulas.

Sourceand '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
*)

Typed formulas.

Sourceand '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

Sourcetype '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.

Sourcetype 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.

Sourceval fresh_hypothesis_name : goal_sort -> string

create a fresh hypothesis name given a goal sort.

Sourceval is_local_hyp : string -> bool

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

Sourceval is_global_hyp : string -> bool

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

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

Sourcetype 'a atdecl = ('a tdecl, 'a) annoted

Type alias for annoted typed declarations.

Sourceand '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.
*)

Typed declarations.

Printing

Sourceval print_term : Format.formatter -> _ atterm -> unit

Print annoted typed terms. Ignore the annotations.

Sourceval print_formula : Format.formatter -> _ atform -> unit

Print annoted typed formulas; Ignores the annotations.

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

Print a list of bound typed variables.

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

Print a list of triggers.

Sourceval print_goal_sort : Format.formatter -> goal_sort -> unit

Print a goal sort

Source

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

Print a rewrite rule

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alt-ergo-lib/AltErgoLib/Typed/index.html

Module `AltErgoLib.Typed`Source

Annotations

Terms and formulas

Declarations

Printing

package alt-ergo-lib

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alt-ergo-lib/AltErgoLib/Typed/index.html

Module AltErgoLib.TypedSource

Annotations

Terms and formulas

Declarations

Printing

Module `AltErgoLib.Typed`Source