(********************************************************************)
(*                                                                  *)
(*  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

   b) on integers, e.g.

   35 + 7 -> 42

   c) on projections of pairs and of other ADTs, e.g

   fst (x,y) -> x

   cdr (Cons x y) -> y

   d) on defined function symbols, e.g.

   function sqr (x:int) = x * x

   sqr 4 -> 4 * 4 -> 16

   sqr x -> x * x

   e) (TODO?) on booleans, e.g.

   True xor False -> True

   f) (TODO?) on reals, e.g.

   1.0 + 2.5 -> 3.5

   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

   then

   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

   forall ... t1 = t2

   or

   forall ... f1 <-> f2

   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 *)
open Why3

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
[@@deriving show]

type builtin_value =
  | Eval of Why3.Term.term
  | Value of value
[@@deriving show]

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