AltErgoLib.Typed
Typed AST
This module defines a typed AST, used to represent typed terms before they are hashconsed.
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
.
type tconstant =
Typed constants.
type oplogic =
| OPand | (* conjunction *) |
| OPor | (* disjunction *) |
| OPxor | (* exclusive disjunction *) |
| OPimp | (* implication *) |
| OPnot | (* negation *) |
| OPiff | (* equivalence *) |
| OPif | (* conditional branching *) |
Logic operators.
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.why *) |
| TTinInterval of 'a atterm * Symbols.bound * Symbols.bound | (* Represent floating point intervals (used for triggers in Floating point arithmetic theory). |
| 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 |
| 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 |
| TAfalse | (* The |
| 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. |
| 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.
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 *) |
Typed formulas.
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.
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.
Assuming a name generated by fresh_hypothesis_name
, answers whether the name design a local hypothesis ?
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. |
| TFunction_def of Loc.t * string * (string * Ty.t) list * Ty.t * 'a atform | (* Predicate definition. |
| TTypeDecl of Loc.t * Ty.t | (* New type declaration. |
Typed declarations.
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.
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