Newer
Older
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** A reduction engine for Why3 terms *)
(* terms are normalized with respect to
1) built-in computation rules
a) on propositional connectives, e.g.
f /\ true -> f
35 + 7 -> 42
c) on projections of pairs and of other ADTs, e.g
d) on defined function symbols, e.g.
function sqr (x:int) = x * x
e) (TODO?) on booleans, e.g.
f) (TODO?) on reals, e.g.
2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if
function dot : t -> t -> t axiom assoc: forall x y z, dot (dot x y) z = dot x
(dot y z) meta "rewrite" assoc
dot (dot a b) (dot c d) -> dot a (dot b (dot c d))
axioms used as rewrite rules must be either of the form
where the root symbol of t1 (resp. f1) is a non-interpreted function symbol
(resp. non-interpreted predicate symbol)
rewriting is done from left to right *)
type 'a engine
(** abstract type for reduction engines *)
val user_env : 'a engine -> 'a
type params = {
compute_defs : bool;
compute_builtin : bool;
compute_def_set : Term.Sls.t;
compute_max_quantifier_domain : int;
}
(** Configuration of the engine. . [compute_defs]: if set to true, automatically
compute symbols using known definitions. Otherwise, only symbols in
[compute_def_set] will be computed. . [compute_builtin]: if set to true,
compute builtin functions. . [compute_max_quantifier_domain]: maximum domain
size for the reduction of bounded quantifications *)
type value =
| Term of Why3.Term.term (* invariant: is in normal form *)
| Int of BigInt.t
| Real of Number.real_value
type builtin_value =
| Eval of Why3.Term.term
| Value of value
type 'a builtin =
'a engine -> Why3.Term.lsymbol -> value list -> Ty.ty option -> builtin_value
type 'a built_in_theories =
Env.pathname
* string
* (string * (Ty.tysymbol -> unit)) list
* (string list * Why3.Term.lsymbol ref option * 'a builtin) list
type bounded_quant_result = {
new_quant : Term.vsymbol list;
substitutions : Term.term list;
}
type 'a bounded_quant =
'a engine -> Term.vsymbol -> cond:Term.term -> bounded_quant_result option
val create :
?bounded_quant:'a bounded_quant ->
?builtins:(Why3.Term.lsymbol * 'a builtin) list ->
params ->
Env.env ->
Decl.decl Ident.Mid.t ->
'a ->
'a built_in_theories list ->
'a engine
(** [create env known_map] creates a reduction engine with . builtins theories
(int.Int, etc.) extracted from [env] . known declarations from [known_map] .
empty set of rewrite rules *)
exception NotARewriteRule of string
val add_rule : Term.term -> 'a engine -> 'a engine
(** [add_rule t e] turns [t] into a new rewrite rule and returns the new engine.
raise NotARewriteRule if [t] cannot be seen as a rewrite rule according to
the general rules given above. *)
val normalize :
?step_limit:int ->
limit:int ->
'a engine ->
Term.term Term.Mvs.t ->
Term.term ->
Term.term
(** [normalize e sigma t] normalizes the term [t] with respect to the engine [e]
with an initial variable environment [sigma].
parameter [limit] provides a maximum number of steps for execution. When
limit is reached, the partially reduced term is returned. parameter
[step_limit] provides a maximum number of steps on reductions that would
change the term even after reconstruction. *)
open Term
exception NoMatch of (term * term * term option) option
(** [NoMatch (t1, t2, t3)] Cannot match [t1] with [t2]. If [t3] exists then [t1]
is already matched with [t3]. *)
exception NoMatchpat of (pattern * pattern) option
type substitution = term Mvs.t
val first_order_matching :
Svs.t -> term list -> term list -> Ty.ty Ty.Mtv.t * substitution