From 574fc624a3203a0b5791d8527b1fb30896734eb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 21 Sep 2022 15:57:19 +0200
Subject: [PATCH] [interpretation] Copy module reduction_engine from Why3.
---
src/interpretation.ml | 49 ++
src/interpretation.mli | 30 +
src/main.ml | 51 +-
src/reduction_engine.ml | 1495 ++++++++++++++++++++++++++++++++++++++
src/reduction_engine.mli | 133 ++++
src/verification.ml | 30 +-
src/verification.mli | 17 +-
tests/interpretation.t | 13 +
8 files changed, 1790 insertions(+), 28 deletions(-)
create mode 100644 src/interpretation.ml
create mode 100644 src/interpretation.mli
create mode 100644 src/reduction_engine.ml
create mode 100644 src/reduction_engine.mli
create mode 100644 tests/interpretation.t
diff --git a/src/interpretation.ml b/src/interpretation.ml
new file mode 100644
index 0000000..bcfb697
--- /dev/null
+++ b/src/interpretation.ml
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Why3
+open Base
+
+let interpret_task env task =
+ let f = Task.task_goal_fmla task in
+ let engine =
+ Reduction_engine.create
+ {
+ compute_defs = false;
+ compute_builtin = true;
+ compute_def_set = Term.Sls.empty;
+ compute_max_quantifier_domain = 0;
+ }
+ env Ident.Mid.empty
+ in
+ let f = Reduction_engine.normalize ~limit:1000 engine Term.Mvs.empty f in
+ Fmt.pr "%a : %a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term f
+
+let interpret ?debug ?format ~loadpath s =
+ let env, _config, mstr_theory =
+ Verification.open_file ?debug ?format ~loadpath s
+ in
+ Wstdlib.Mstr.iter
+ (fun _ theory ->
+ List.iter (Task.split_theory theory None None) ~f:(fun task ->
+ interpret_task env task))
+ mstr_theory
diff --git a/src/interpretation.mli b/src/interpretation.mli
new file mode 100644
index 0000000..68649f2
--- /dev/null
+++ b/src/interpretation.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Base
+
+val interpret :
+ ?debug:bool ->
+ ?format:string ->
+ loadpath:string list ->
+ Verification.File.t ->
+ unit
diff --git a/src/main.ml b/src/main.ml
index 00b42e0..c0034ca 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -204,6 +204,10 @@ let verify_json ?memlimit ?timelimit ?outfile json =
~f:(record_verification_result jin.id verification_result)
| _ -> failwith "Unexpected more than one theory from a JSON file"
+let interpret format loadpath files =
+ let debug = log_level_is_debug () in
+ List.iter ~f:(Interpretation.interpret ~debug ?format ~loadpath) files
+
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Execution of command '%s'" cmdname);
cmd ()
@@ -257,6 +261,20 @@ let timelimit =
Arg.(
value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+ let loadpath =
+ let doc = "Additional loadpath." in
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+
+ let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+
+ let files =
+ let doc = "File to verify." in
+ let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
+ Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
+
+
let verify_cmd =
let cmdname = "verify" in
let info =
@@ -265,14 +283,6 @@ let verify_cmd =
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
- let loadpath =
- let doc = "Additional loadpath." in
- Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
- in
- let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
- in
let prover =
let all_provers = Prover.list_available () in
let doc =
@@ -297,11 +307,6 @@ let verify_cmd =
let doc = "Dataset $(docv) (CSV format only)." in
Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
in
- let files =
- let doc = "File to verify." in
- let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
- Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
- in
let term =
Term.(
const
@@ -355,6 +360,24 @@ let verify_json_cmd =
in
Cmd.v info term
+let interpret_cmd =
+ let cmdname = "interpret" in
+ let doc =
+ "Interpret the goal and print the strategy that will be executed."
+ in
+ let info =
+ Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
+ ~doc
+ ~man:[ `S Manpage.s_description; `P doc ]
+ in
+ let term =
+ Term.(
+ const (fun format loadpath files _ ->
+ exec_cmd cmdname (fun () -> interpret format loadpath files))
+ $ format $ loadpath $ files $ setup_logs)
+ in
+ Cmd.v info term
+
let default_info =
let doc =
"A platform for characterizing the safety and robustness of artificial \
@@ -389,7 +412,7 @@ let () =
let () =
try
Cmd.group ~default:default_cmd default_info
- [ config_cmd; verify_cmd; verify_json_cmd ]
+ [ config_cmd; verify_cmd; verify_json_cmd; interpret_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
with exn when not (log_level_is_debug ()) ->
Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
new file mode 100644
index 0000000..e2f8783
--- /dev/null
+++ b/src/reduction_engine.ml
@@ -0,0 +1,1495 @@
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2022 -- 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. *)
+(* *)
+(********************************************************************)
+
+open Why3
+open Term
+
+[@@@ ocaml.warning "-9"]
+
+(* {2 Values} *)
+
+type value =
+ | Term of term (* invariant: is in normal form *)
+ | Int of BigInt.t
+ | Real of Number.real_value
+
+let v_attr_copy orig v =
+ match v with
+ | Int _ -> v
+ | Real _ -> v
+ | Term t -> Term (t_attr_copy orig t)
+
+let term_of_value v =
+ let open Number in
+ match v with
+ | Term t -> t
+ | Int n -> t_int_const n
+ | Real { rv_sig = s; rv_pow2 = pow2; rv_pow5 = pow5 } -> t_real_const ~pow2 ~pow5 s
+
+exception NotNum
+
+let big_int_of_const c =
+ match c with
+ | Constant.ConstInt i -> i.Number.il_int
+ | Constant.ConstReal _ -> assert false
+ | Constant.ConstStr _ -> assert false
+
+let big_int_of_value v =
+ match v with
+ | Int n -> n
+ | Real _ -> assert false
+ | Term { t_node = Tconst c } -> big_int_of_const c
+ | Term _ -> raise NotNum
+
+let real_of_const c =
+ match c with
+ | Constant.ConstReal r -> r.Number.rl_real
+ | Constant.ConstInt _ -> assert false
+ | Constant.ConstStr _ -> assert false
+
+let real_of_value v =
+ match v with
+ | Real r -> r
+ | Int _ -> assert false
+ | Term { t_node = Tconst c } -> real_of_const c
+ | Term _ -> raise NotNum
+
+(* {2 Builtin symbols} *)
+
+let builtins = Hls.create 17
+
+(* all builtin functions *)
+
+exception Undetermined
+
+let to_bool b = if b then t_true else t_false
+
+let _t_app_value ls l ty =
+ Term (t_app ls (List.map term_of_value l) ty)
+
+let is_zero v =
+ try BigInt.eq (big_int_of_value v) BigInt.zero
+ with NotNum -> false
+
+let is_one v =
+ try BigInt.eq (big_int_of_value v) BigInt.one
+ with NotNum -> false
+
+let eval_int_op op simpl ls l ty =
+ match l with
+ | [t1 ; t2] ->
+ begin
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Int (op n1 n2)
+ with NotNum | Division_by_zero ->
+ simpl ls t1 t2 ty
+ end
+ | _ -> assert false
+
+let simpl_add _ls t1 t2 _ty =
+ if is_zero t1 then t2 else
+ if is_zero t2 then t1 else
+ raise Undetermined
+
+let simpl_sub _ls t1 t2 _ty =
+ if is_zero t2 then t1 else
+ raise Undetermined
+
+let simpl_mul _ls t1 t2 _ty =
+ if is_zero t1 then t1 else
+ if is_zero t2 then t2 else
+ if is_one t1 then t2 else
+ if is_one t2 then t1 else
+ raise Undetermined
+
+let simpl_div _ls t1 t2 _ty =
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1 then t1 else
+ if is_one t2 then t1 else
+ raise Undetermined
+
+let simpl_mod _ls t1 t2 _ty =
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1 then t1 else
+ if is_one t2 then Int (BigInt.zero) else
+ raise Undetermined
+
+let simpl_minmax _ls v1 v2 _ty =
+ match v1,v2 with
+ | Term t1, Term t2 ->
+ if t_equal t1 t2 then v1 else
+ raise Undetermined
+ | _ ->
+ raise Undetermined
+
+let eval_int_rel op _ls l _ty =
+ match l with
+ | [t1 ; t2] ->
+ begin
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Term (to_bool (op n1 n2))
+ with NotNum | Division_by_zero ->
+ raise Undetermined
+ (* t_app_value ls l ty *)
+ end
+ | _ -> assert false
+
+let eval_int_uop op _ls l _ty =
+ match l with
+ | [t1] ->
+ begin
+ try
+ let n1 = big_int_of_value t1 in Int (op n1)
+ with NotNum | Division_by_zero ->
+ raise Undetermined
+ (* t_app_value ls l ty *)
+ end
+ | _ -> assert false
+
+let real_align ~pow2 ~pow5 r =
+ let open Number in
+ let { rv_sig = s; rv_pow2 = p2; rv_pow5 = p5 } = r in
+ let s = BigInt.mul s (BigInt.pow_int_pos_bigint 2 (BigInt.sub p2 pow2)) in
+ let s = BigInt.mul s (BigInt.pow_int_pos_bigint 5 (BigInt.sub p5 pow5)) in
+ s
+
+let eval_real_op op simpl ls l ty =
+ match l with
+ | [t1; t2] ->
+ begin
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ Real (op n1 n2)
+ with NotNum ->
+ simpl ls t1 t2 ty
+ end
+ | _ -> assert false
+
+let eval_real_uop op _ls l _ty =
+ match l with
+ | [t1] ->
+ begin
+ try
+ let n1 = real_of_value t1 in
+ Real (op n1)
+ with NotNum ->
+ raise Undetermined
+ end
+ | _ -> assert false
+
+let eval_real_rel op _ls l _ty =
+ let open Number in
+ match l with
+ | [t1 ; t2] ->
+ begin
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ let s1, s2 =
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = n1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = n2 in
+ if BigInt.sign s1 <> BigInt.sign s2 then s1,s2
+ else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 n1 in
+ let s2 = real_align ~pow2 ~pow5 n2 in
+ s1, s2 in
+ Term (to_bool (op s1 s2))
+ with NotNum ->
+ raise Undetermined
+ (* t_app_value ls l ty *)
+ end
+ | _ -> assert false
+
+let real_0 = Number.real_value BigInt.zero
+let real_1 = Number.real_value BigInt.one
+
+let is_real t r =
+ try Number.compare_real (real_of_value t) r = 0
+ with NotNum -> false
+
+let real_opp r =
+ let open Number in
+ let { rv_sig = s; rv_pow2 = pow2; rv_pow5 = pow5 } = r in
+ real_value ~pow2 ~pow5 (BigInt.minus s)
+
+let real_add r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.eq s1 BigInt.zero then r2 else
+ if BigInt.eq s2 BigInt.zero then r1 else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 r1 in
+ let s2 = real_align ~pow2 ~pow5 r2 in
+ real_value ~pow2 ~pow5 (BigInt.add s1 s2)
+
+let real_sub r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.eq s2 BigInt.zero then r1 else
+ if BigInt.eq s1 BigInt.zero then real_value ~pow2:p22 ~pow5:p52 (BigInt.minus s2) else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 r1 in
+ let s2 = real_align ~pow2 ~pow5 r2 in
+ real_value ~pow2 ~pow5 (BigInt.sub s1 s2)
+
+let real_mul r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ let s = BigInt.mul s1 s2 in
+ let pow2 = BigInt.add p21 p22 in
+ let pow5 = BigInt.add p51 p52 in
+ real_value ~pow2 ~pow5 s
+
+let simpl_real_add _ls t1 t2 _ty =
+ if is_real t1 real_0 then t2 else
+ if is_real t2 real_0 then t1 else
+ raise Undetermined
+
+let simpl_real_sub _ls t1 t2 _ty =
+ if is_real t2 real_0 then t1 else
+ raise Undetermined
+
+let simpl_real_mul _ls t1 t2 _ty =
+ if is_real t1 real_0 then t1 else
+ if is_real t2 real_0 then t2 else
+ if is_real t1 real_1 then t2 else
+ if is_real t2 real_1 then t1 else
+ raise Undetermined
+
+let real_pow r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.le s1 BigInt.zero then
+ raise Undetermined
+ else if BigInt.lt p22 BigInt.zero || BigInt.lt p52 BigInt.zero then
+ raise NotNum
+ else
+ let s1 = try BigInt.to_int s1 with Failure _ -> raise NotNum in
+ let s2 = BigInt.mul s2 (BigInt.pow_int_pos_bigint 2 p22) in
+ let s2 = BigInt.mul s2 (BigInt.pow_int_pos_bigint 5 p52) in
+ let s =
+ if s1 = 1 then BigInt.one
+ else if BigInt.lt s2 BigInt.zero then raise NotNum
+ else BigInt.pow_int_pos_bigint s1 s2 in
+ let pow2 = BigInt.mul p21 s2 in
+ let pow5 = BigInt.mul p51 s2 in
+ Number.real_value ~pow2 ~pow5 s
+
+let simpl_real_pow _ls t1 _t2 _ty =
+ if is_real t1 real_1 then t1 else
+ raise Undetermined
+
+let real_from_int _ls l _ty =
+ match l with
+ | [t] ->
+ begin
+ try
+ let n = big_int_of_value t in
+ Real (Number.real_value n)
+ with NotNum ->
+ raise Undetermined
+ end
+ | _ -> assert false
+
+let built_in_theories =
+ [
+(*
+ ["bool"],"Bool", [],
+ [ "True", None, eval_true ;
+ "False", None, eval_false ;
+ ] ;
+*)
+ ["int"],"Int", [],
+ [ Ident.op_infix "+", None, eval_int_op BigInt.add simpl_add;
+ Ident.op_infix "-", None, eval_int_op BigInt.sub simpl_sub;
+ Ident.op_infix "*", None, eval_int_op BigInt.mul simpl_mul;
+ Ident.op_prefix "-", None, eval_int_uop BigInt.minus;
+ Ident.op_infix "<", None, eval_int_rel BigInt.lt;
+ Ident.op_infix "<=", None, eval_int_rel BigInt.le;
+ Ident.op_infix ">", None, eval_int_rel BigInt.gt;
+ Ident.op_infix ">=", None, eval_int_rel BigInt.ge;
+ ] ;
+ ["int"],"MinMax", [],
+ [ "min", None, eval_int_op BigInt.min simpl_minmax;
+ "max", None, eval_int_op BigInt.max simpl_minmax;
+ ] ;
+ ["int"],"ComputerDivision", [],
+ [ "div", None, eval_int_op BigInt.computer_div simpl_div;
+ "mod", None, eval_int_op BigInt.computer_mod simpl_mod;
+ ] ;
+ ["int"],"EuclideanDivision", [],
+ [ "div", None, eval_int_op BigInt.euclidean_div simpl_div;
+ "mod", None, eval_int_op BigInt.euclidean_mod simpl_mod;
+ ] ;
+ ["real"], "Real", [],
+ [ Ident.op_prefix "-", None, eval_real_uop real_opp;
+ Ident.op_infix "+", None, eval_real_op real_add simpl_real_add;
+ Ident.op_infix "-", None, eval_real_op real_sub simpl_real_sub;
+ Ident.op_infix "*", None, eval_real_op real_mul simpl_real_mul;
+ Ident.op_infix "<", None, eval_real_rel BigInt.lt;
+ Ident.op_infix "<=", None, eval_real_rel BigInt.le;
+ Ident.op_infix ">", None, eval_real_rel BigInt.gt;
+ Ident.op_infix ">=", None, eval_real_rel BigInt.ge ] ;
+ ["real"], "FromInt", [],
+ [ "from_int", None, real_from_int ] ;
+ ["real"], "PowerReal", [],
+ [ "pow", None, eval_real_op real_pow simpl_real_pow ] ;
+(*
+ ["map"],"Map", ["map", builtin_map_type],
+ [ "const", Some ls_map_const, eval_map_const;
+ "get", Some ls_map_get, eval_map_get;
+ "set", Some ls_map_set, eval_map_set;
+ ] ;
+*)
+ ]
+
+let add_builtin_th env (l,n,t,d) =
+ let th = Env.read_theory env l n in
+ List.iter
+ (fun (id,r) ->
+ let ts = Theory.ns_find_ts th.Theory.th_export [id] in
+ r ts)
+ t;
+ List.iter
+ (fun (id,r,f) ->
+ let ls = Theory.ns_find_ls th.Theory.th_export [id] in
+ Hls.add builtins ls f;
+ match r with
+ | None -> ()
+ | Some r -> r := ls)
+ d
+
+let get_builtins env =
+ Hls.clear builtins;
+ List.iter (add_builtin_th env) built_in_theories
+
+
+
+(* {2 the reduction machine} *)
+
+
+type rule = Svs.t * term list * term
+
+type params =
+ { compute_defs : bool;
+ compute_builtin : bool;
+ compute_def_set : Term.Sls.t;
+ compute_max_quantifier_domain : int;
+ }
+
+type engine =
+ { known_map : Decl.decl Ident.Mid.t;
+ rules : rule list Mls.t;
+ params : params;
+ ls_lt : lsymbol; (* The lsymbol for [int.Int.(<)] *)
+ }
+
+
+(* OBSOLETE COMMENT
+
+ A configuration is a pair (t,s) where t is a stack of terms and s is a
+ stack of function symbols.
+
+ A configuration ([t1;..;tn],[f1;..;fk]) represents a whole term, its
+ model, as defined recursively by
+
+ model([t],[]) = t
+
+ model(t1::..::tn::t,f::s) = model(f(t1,..,tn)::t,s)
+ where f is of arity n
+
+ A given term can be "exploded" into a configuration by reversing the
+ rules above
+
+ During reduction, the terms in the first stack are kept in normal
+ form (value). The normalization process can be defined as the repeated
+ application of the following rules.
+
+ ([t],[]) --> t // t is in normal form
+
+ if f(t1,..,tn) is not a redex then
+ (t1::..::tn::t,f::s) --> (f(t1,..,tn)::t,s)
+
+ if f(t1,..,tn) is a redex l sigma for a rule l -> r then
+ (t1::..::tn::t,f::s) --> (subst(sigma) @ t,explode(r) @ s)
+
+
+
+
+*)
+
+type substitution = term Mvs.t
+
+type cont =
+| Kapp of lsymbol * Ty.ty option
+| Kif of term * term * substitution
+| Klet of vsymbol * term * substitution
+| Kcase of term_branch list * substitution
+| Keps of vsymbol
+| Kquant of quant * vsymbol list * trigger
+| Kbinop of binop
+| Knot
+| Keval of term * substitution
+
+type config = {
+ value_stack : value list;
+ cont_stack : (cont * term) list;
+ (* second term is the original term, for attribute and loc copy *)
+}
+
+
+(* This global variable is used to approximate a count of the elementary
+ simplifications that are done during normalization. This is used for
+ transformation step. *)
+let rec_step_limit = ref 0
+
+exception NoMatch of (term * term * term option) option
+exception NoMatchpat of (pattern * pattern) option
+
+let rec pattern_renaming (bound_vars, mt) p1 p2 =
+ match p1.pat_node, p2.pat_node with
+ | Pwild, Pwild ->
+ (bound_vars, mt)
+ | Pvar v1, Pvar v2 ->
+ begin
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ (bound_vars, mt)
+ with
+ | Ty.TypeMismatch _ ->
+ raise (NoMatchpat (Some (p1, p2)))
+ end
+ | Papp (ls1, tl1), Papp (ls2, tl2) when ls_equal ls1 ls2 ->
+ List.fold_left2 pattern_renaming (bound_vars, mt) tl1 tl2
+ | Por (p1a, p1b), Por (p2a, p2b) ->
+ let (bound_vars, mt) =
+ pattern_renaming (bound_vars, mt) p1a p2a in
+ pattern_renaming (bound_vars, mt) p1b p2b
+ | Pas (p1, v1), Pas (p2, v2) ->
+ begin
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ pattern_renaming (bound_vars, mt) p1 p2
+ with
+ | Ty.TypeMismatch _ ->
+ raise (NoMatchpat (Some (p1, p2)))
+ end
+ | _ -> raise (NoMatchpat (Some (p1, p2)))
+
+let first_order_matching (vars : Svs.t) (largs : term list)
+ (args : term list) : Ty.ty Ty.Mtv.t * substitution =
+ let rec loop bound_vars ((mt,mv) as sigma) largs args =
+ match largs,args with
+ | [],[] -> sigma
+ | t1::r1, t2::r2 ->
+ begin
+(*
+ Format.eprintf "matching terms %a and %a...@."
+ Pretty.print_term t1 Pretty.print_term t2;
+*)
+ match t1.t_node with
+ | Tvar vs when Svs.mem vs vars ->
+ begin
+ try let t = Mvs.find vs mv in
+ if t_equal t t2 then
+ loop bound_vars sigma r1 r2
+ else
+ raise (NoMatch (Some (t1, t2, Some t)))
+ with Not_found ->
+ try
+ let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
+ let fv2 = t_vars t2 in
+ if Mvs.is_empty (Mvs.set_inter bound_vars fv2) then
+ loop bound_vars (ts,Mvs.add vs t2 mv) r1 r2
+ else
+ raise (NoMatch (Some (t1, t2, None)))
+ with Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tapp(ls1,args1) ->
+ begin
+ match t2.t_node with
+ | Tapp(ls2,args2) when ls_equal ls1 ls2 ->
+ let mt, mv = loop bound_vars sigma
+ (List.rev_append args1 r1)
+ (List.rev_append args2 r2) in
+ begin
+ try Ty.oty_match mt t1.t_ty t2.t_ty, mv
+ with Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ end
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tquant (q1, bv1) ->
+ begin
+ match t2.t_node with
+ | Tquant (q2, bv2) when q1 = q2 ->
+ let (vl1, _tl1, term1) = t_open_quant bv1 in
+ let (vl2, _tl2, term2) = t_open_quant bv2 in
+ let (bound_vars, term1, mt) =
+ try List.fold_left2 (fun (bound_vars, term1, mt) e1 e2 ->
+ let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
+ let bound_vars = Mvs.add e2 e1 bound_vars in
+ (bound_vars,term1, mt)) (bound_vars,term1, mt) vl1 vl2
+ with Invalid_argument _ | Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1,t2,None)))
+ in
+ loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tbinop (b1, t1_l, t1_r) ->
+ begin
+ match t2.t_node with
+ | Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
+ loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tif (t11, t12, t13) ->
+ begin
+ match t2.t_node with
+ | Tif (t21, t22, t23) ->
+ loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
+ (t21 :: t22 :: t23 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tlet (td1, tb1) ->
+ begin
+ match t2.t_node with
+ | Tlet (td2, tb2) ->
+ let (v1, tl1) = t_open_bound tb1 in
+ let (v2, tl2) = t_open_bound tb2 in
+ let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1,t2, None))) in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
+ | _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tcase (ts1, tbl1) ->
+ begin
+ match t2.t_node with
+ | Tcase (ts2, tbl2) ->
+ begin try
+ let (bound_vars, mt, l1, l2) =
+ List.fold_left2 (fun (bound_vars, mt, l1, l2) tb1 tb2 ->
+ let (p1, tb1) = t_open_branch tb1 in
+ let (p2, tb2) = t_open_branch tb2 in
+ let bound_vars, mt = pattern_renaming (bound_vars, mt) p1 p2 in
+ (bound_vars,mt, tb1 :: l1, tb2 :: l2)
+ ) (bound_vars,mt, ts1 :: r1, ts2 :: r2) tbl1 tbl2 in
+ loop bound_vars (mt,mv) l1 l2
+ with Invalid_argument _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ end
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Teps tb1 ->
+ begin
+ match t2.t_node with
+ | Teps tb2 ->
+ let (v1, td1) = t_open_bound tb1 in
+ let (v2, td2) = t_open_bound tb2 in
+ let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1,t2,None))) in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+
+ | Tnot t1 ->
+ begin
+ match t2.t_node with
+ | Tnot t2 ->
+ loop bound_vars sigma (t1 :: r1) (t2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | Tvar v1 ->
+ begin match t2.t_node with
+ | Tvar v2 ->
+ begin try
+ if vs_equal v1 (Mvs.find v2 bound_vars) then
+ loop bound_vars sigma r1 r2
+ else
+ raise (NoMatch (Some (t1, t2, None)))
+ with
+ Not_found -> assert false
+ end
+ | _ -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
+ loop bound_vars sigma r1 r2
+ | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2, None)))
+ end
+ | _ -> raise (NoMatch None)
+ in
+ loop Mvs.empty (Ty.Mtv.empty, Mvs.empty) largs args
+
+exception Irreducible
+
+let one_step_reduce engine ls args =
+ try
+ let rules = Mls.find ls engine.rules in
+ let rec loop rules =
+ match rules with
+ | [] -> raise Irreducible
+ | (vars,largs,rhs)::rem ->
+ begin
+ try
+ let sigma = first_order_matching vars largs args in
+ sigma,rhs
+ with NoMatch _ ->
+ loop rem
+ end
+ in loop rules
+ with Not_found ->
+ raise Irreducible
+
+let rec matching ((mt,mv) as sigma) t p =
+ match p.pat_node with
+ | Pwild -> sigma
+ | Pvar v -> (mt,Mvs.add v t mv)
+ | Por(p1,p2) ->
+ begin
+ try matching sigma t p1
+ with NoMatch _ -> matching sigma t p2
+ end
+ | Pas(p,v) -> matching (mt,Mvs.add v t mv) t p
+ | Papp(ls1,pl) ->
+ match t.t_node with
+ | Tapp(ls2,tl) ->
+ if ls_equal ls1 ls2 then
+ List.fold_left2 matching sigma tl pl
+ else
+ if ls2.ls_constr > 0 then raise (NoMatch None)
+ else raise Undetermined
+ | _ -> raise Undetermined
+
+
+let rec extract_first n acc l =
+ if n = 0 then acc,l else
+ match l with
+ | x :: r ->
+ extract_first (n-1) (x::acc) r
+ | [] -> assert false
+
+(** If [t1] matches [i1 < vs] or [i1 <= vs] and [t2] matches [vs < i2] or
+ [vs <= i2], then return the bounds [i1(+1), vs, i2(-1)]. The +1/-1 shift the
+ bounds for strict unequalities operators to obtain inclusive bounds. *)
+let bounds ls_lt t1 t2 =
+ let lt order = function (* match [i < vs] or [vs < i], return [i, vs] *)
+ | {t_node= Tapp (ls, [t1; t2])} when ls_equal ls ls_lt -> (
+ assert Ty.(ty_equal (t_type t1) ty_int && ty_equal (t_type t2) ty_int);
+ match order t1 t2 with
+ | {t_node= Tconst (Constant.ConstInt {Number.il_int= i})},
+ {t_node= Tvar vs} ->
+ i, vs
+ | _ -> raise Exit )
+ | _ -> raise Exit in
+ let eq order = function (* match [i = vs] or [vs = i], return [i, vs] *)
+ | {t_node= Tapp (ls, [t1; t2])}
+ when ls_equal ls Term.ps_equ
+ && Ty.ty_equal (t_type t1) Ty.ty_int
+ && Ty.ty_equal (t_type t2) Ty.ty_int -> (
+ match order t1 t2 with
+ | {t_node= Tconst (Constant.ConstInt {Number.il_int= i})},
+ {t_node= Tvar vs} when Ty.ty_equal vs.vs_ty Ty.ty_int ->
+ i, vs
+ | _ -> raise Exit )
+ | _ -> raise Exit in
+ let le order = function (* match [i <= vs] or [vs <= i], return [i, vs] *)
+ | {t_node= Tbinop (Tor, t1, t2)} ->
+ let i, vs = lt order t1 in
+ let i', vs' = eq order t2 in
+ if not (BigInt.eq i i' && vs_equal vs vs') then raise Exit;
+ i, vs
+ | _ -> raise Exit in
+ let bound order shift t = (* match [i op vs] or [vs op i], op is [<] or [<=] *)
+ try le order t with Exit ->
+ let i, vs = lt order t in
+ shift i, vs in
+ let i1, vs = bound (fun t1 t2 -> t1, t2) BigInt.succ t1 in
+ let i2, vs' = bound (fun t1 t2 -> t2, t1) BigInt.pred t2 in
+ if not (vs_equal vs vs') then raise Exit;
+ i1, vs, i2
+
+(** [reduce_bounded_quant ls_lt limit t sigma st rem] detects a bounded
+ quantification and reduces it to conjunction:
+
+ forall v. a < v < b. t(v)
+ --> f(a+1) /\ ... /\ f(b-1)
+
+ @param ls_lt lsymbol for [int.Int.(<)]
+
+ @param limit Reduce if the difference between upper and lower bound is at
+ most [limit].
+
+ TODO:
+ - expand to bounded quantifications on range values
+ - compatiblity with reverse direction (forall i. b > i > a -> t)
+ - detect SPARK-style [forall i. if a < i /\ i < b then t else true] *)
+let reduce_bounded_quant ls_lt limit t sigma st rem =
+ match st, rem with (* st = a < vs < b :: _; rem = -> :: forall vs :: _ *)
+ | Term {t_node= Tbinop (Tand, t1, t2)} :: st,
+ ((Kbinop Timplies, _) :: (Kquant (Tforall as quant, [vs], _), _) :: rem |
+ (Kbinop Tand, _) :: (Kquant (Texists as quant, [vs], _), _) :: rem)
+ when Ty.ty_equal vs.vs_ty Ty.ty_int ->
+ let t_empty, binop = match quant with
+ | Tforall -> t_true, Tand
+ | Texists -> t_false, Tor in
+ let a, vs', b = bounds ls_lt t1 t2 in
+ if not (vs_equal vs vs') then raise Exit;
+ if BigInt.(gt (sub b a) (of_int limit)) then raise Exit;
+ if BigInt.gt a b then (* empty range *)
+ {value_stack= Term t_empty :: st; cont_stack= rem}
+ else
+ let rec loop rem i =
+ if BigInt.lt i a then
+ rem
+ else
+ let t_i = t_const (Constant.int_const i) Ty.ty_int in
+ let rem = (* conjunction for all i > a *)
+ if BigInt.gt i a then (Kbinop binop, t_true) :: rem else rem in
+ let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
+ loop rem (BigInt.pred i) in
+ {value_stack= st; cont_stack= loop rem b}
+ | _ -> raise Exit
+
+let rec reduce engine c =
+ match c.value_stack, c.cont_stack with
+ | _, [] -> assert false
+ | st, (Keval (t,sigma),orig) :: rem -> (
+ let limit = engine.params.compute_max_quantifier_domain in
+ try reduce_bounded_quant engine.ls_lt limit t sigma st rem with Exit ->
+ reduce_eval engine st t ~orig sigma rem )
+ | [], (Kif _, _) :: _ -> assert false
+ | v :: st, (Kif(t2,t3,sigma), orig) :: rem ->
+ begin
+ match v with
+ | Term { t_node = Ttrue } ->
+ incr(rec_step_limit);
+ { value_stack = st ;
+ cont_stack = (Keval(t2,sigma),t_attr_copy orig t2) :: rem }
+ | Term { t_node = Tfalse } ->
+ incr(rec_step_limit);
+ { value_stack = st ;
+ cont_stack = (Keval(t3,sigma),t_attr_copy orig t3) :: rem }
+ | Term t1 -> begin
+ match t1.t_node , t2.t_node , t3.t_node with
+ | Tapp (ls,[b0;{ t_node = Tapp (ls1,_) }]) , Tapp(ls2,_) , Tapp(ls3,_)
+ when ls_equal ls ps_equ && ls_equal ls1 fs_bool_true &&
+ ls_equal ls2 fs_bool_true && ls_equal ls3 fs_bool_false ->
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig b0) :: st;
+ cont_stack = rem }
+ | _ ->
+ { value_stack =
+ Term
+ (t_attr_copy orig
+ (t_if t1 (t_subst sigma t2) (t_subst sigma t3))) :: st;
+ cont_stack = rem;
+ }
+ end
+ | (Int _ | Real _) -> assert false (* would be ill-typed *)
+ end
+ | [], (Klet _, _) :: _ -> assert false
+ | t1 :: st, (Klet(v,t2,sigma), orig) :: rem ->
+ incr(rec_step_limit);
+ let t1 = term_of_value t1 in
+ { value_stack = st;
+ cont_stack =
+ (Keval(t2, Mvs.add v t1 sigma), t_attr_copy orig t2) :: rem;
+ }
+ | [], (Kcase _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Kcase _, _) :: _ -> assert false
+ | (Term t1) :: st, (Kcase(tbl,sigma), orig) :: rem ->
+ reduce_match st t1 ~orig tbl sigma rem
+ | ([] | [_] | (Int _ | Real _) :: _ | Term _ :: (Int _ | Real _) :: _),
+ (Kbinop _, _) :: _ -> assert false
+ | (Term t1) :: (Term t2) :: st, (Kbinop op, orig) :: rem ->
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig (t_binary_simp op t2 t1)) :: st;
+ cont_stack = rem;
+ }
+ | [], (Knot,_) :: _ -> assert false
+ | (Int _ | Real _) :: _ , (Knot,_) :: _ -> assert false
+ | (Term t) :: st, (Knot, orig) :: rem ->
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig (t_not_simp t)) :: st;
+ cont_stack = rem;
+ }
+ | st, (Kapp(ls,ty), orig) :: rem ->
+ reduce_app engine st ~orig ls ty rem
+ | [], (Keps _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _ , (Keps _, _) :: _ -> assert false
+ | Term t :: st, (Keps v, orig) :: rem ->
+ { value_stack = Term (t_attr_copy orig (t_eps_close v t)) :: st;
+ cont_stack = rem;
+ }
+ | [], (Kquant _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Kquant _, _) :: _ -> assert false
+ | Term t :: st, (Kquant(q,vl,tr), orig) :: rem ->
+ { value_stack = Term (t_attr_copy orig (t_quant_close_simp q vl tr t)) :: st;
+ cont_stack = rem;
+ }
+
+and reduce_match st u ~orig tbl sigma cont =
+ let rec iter tbl =
+ match tbl with
+ | [] -> assert false (* pattern matching not exhaustive *)
+ | b::rem ->
+ let p,t = t_open_branch b in
+ try
+ let (mt',mv') = matching (Ty.Mtv.empty,sigma) u p in
+(*
+ Format.eprintf "Pattern-matching succeeded:@\nmt' = @[";
+ Ty.Mtv.iter
+ (fun tv ty -> Format.eprintf "%a -> %a,"
+ Pretty.print_tv tv Pretty.print_ty ty)
+ mt';
+ Format.eprintf "@]@\n";
+ Format.eprintf "mv' = @[";
+ Mvs.iter
+ (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t)
+ mv';
+ Format.eprintf "@]@.";
+ Format.eprintf "branch before inst: %a@." Pretty.print_term t;
+*)
+ let mv'',t = t_subst_types mt' mv' t in
+(*
+ Format.eprintf "branch after types inst: %a@." Pretty.print_term t;
+ Format.eprintf "mv'' = @[";
+ Mvs.iter
+ (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t)
+ mv'';
+ Format.eprintf "@]@.";
+*)
+ incr(rec_step_limit);
+ { value_stack = st;
+ cont_stack = (Keval(t,mv''), t_attr_copy orig t) :: cont;
+ }
+ with NoMatch _ -> iter rem
+ in
+ try iter tbl with Undetermined ->
+ let dmy = t_var (create_vsymbol (Ident.id_fresh "__dmy") (t_type u)) in
+ let tbls = match t_subst sigma (t_case dmy tbl) with
+ | { t_node = Tcase (_,tbls) } -> tbls
+ | _ -> assert false
+ in
+ { value_stack =
+ Term (t_attr_copy orig (t_case u tbls)) :: st;
+ cont_stack = cont;
+ }
+
+
+and reduce_eval eng st t ~orig sigma rem =
+ let orig = t_attr_copy orig t in
+ match t.t_node with
+ | Tvar v ->
+ begin
+ match Ident.Mid.find v.vs_name eng.known_map with
+ | Decl.{d_node = Dlogic dl} ->
+ incr rec_step_limit ;
+ let _, ls_defn = List.find (fun (ls, _) -> String.equal ls.ls_name.Ident.id_string v.vs_name.Ident.id_string) dl in
+ let vs, t = Decl.open_ls_defn ls_defn in
+ let aux vs t =
+ (* Create ε fc. λ vs. fc @ vs = t to make the value from
+ known_map compatible to reduce_func_app *)
+ let ty = Opt.get t.t_ty in
+ let app_ty = Ty.ty_func vs.vs_ty ty in
+ let fc = create_vsymbol (Ident.id_fresh "fc") app_ty in
+ t_eps
+ (t_close_bound fc
+ (t_quant Tforall
+ (t_close_quant [vs] []
+ (t_app ps_equ
+ [t_app fs_func_app [t_var fc; t_var vs] (Some ty); t]
+ None)))) in
+ let t = List.fold_right aux vs t in
+ {value_stack = Term t :: st; cont_stack = rem}
+ | _ -> assert false
+ | exception Not_found ->
+ match Mvs.find v sigma with
+ | t ->
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig t) :: st ;
+ cont_stack = rem;
+ }
+ | exception Not_found ->
+ (* this may happen, e.g when computing below a quantified formula *)
+ (* Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
+ assert false *)
+ { value_stack = Term orig :: st ;
+ cont_stack = rem;
+ }
+ end
+ | Tif(t1,t2,t3) ->
+ { value_stack = st;
+ cont_stack = (Keval(t1,sigma),t1) :: (Kif(t2,t3,sigma),orig) :: rem;
+ }
+ | Tlet(t1,tb) ->
+ let v,t2 = t_open_bound tb in
+ { value_stack = st ;
+ cont_stack = (Keval(t1,sigma),t1) :: (Klet(v,t2,sigma),orig) :: rem }
+ | Tcase(t1,tbl) ->
+ { value_stack = st;
+ cont_stack = (Keval(t1,sigma),t1) :: (Kcase(tbl,sigma),orig) :: rem }
+ | Tbinop(op,t1,t2) ->
+ { value_stack = st;
+ cont_stack =
+ (Keval(t1,sigma),t1) ::
+ (Keval(t2,sigma),t2) :: (Kbinop op, orig) :: rem;
+ }
+ | Tnot t1 ->
+ { value_stack = st;
+ cont_stack = (Keval(t1,sigma),t1) :: (Knot,orig) :: rem;
+ }
+ | Teps tb ->
+ let v,t1 = t_open_bound tb in
+ { value_stack = st ;
+ cont_stack = (Keval(t1,sigma),t1) :: (Keps v,orig) :: rem;
+ }
+ | Tquant(q,tq) ->
+ let vl,tr,t1 = t_open_quant tq in
+ { value_stack = st;
+ cont_stack = (Keval(t1,sigma),t1) :: (Kquant(q,vl,tr),orig) :: rem;
+ }
+ | Tapp(ls,tl) ->
+ let args = List.rev_map (fun t -> (Keval(t,sigma),t)) tl in
+ { value_stack = st;
+ cont_stack = List.rev_append args ((Kapp(ls,t.t_ty),orig) :: rem);
+ }
+ | Ttrue | Tfalse | Tconst _ ->
+ { value_stack = Term orig :: st;
+ cont_stack = rem;
+ }
+
+and reduce_app engine st ls ~orig ty rem_cont =
+ if ls_equal ls ps_equ then
+ match st with
+ | t2 :: t1 :: rem_st ->
+ begin
+ try
+ reduce_equ ~orig rem_st t1 t2 rem_cont
+ with Undetermined ->
+ reduce_app_no_equ engine st ls ~orig ty rem_cont
+ end
+ | _ -> assert false
+ else
+ if ls_equal ls fs_func_app then
+ match st with
+ | t2 :: t1 :: rem_st ->
+ begin
+ try
+ reduce_func_app ~orig ty rem_st t1 t2 rem_cont
+ with Undetermined ->
+ reduce_app_no_equ engine st ls ~orig ty rem_cont
+ end
+ | _ -> assert false
+ else
+ reduce_app_no_equ engine st ls ~orig ty rem_cont
+
+and reduce_func_app ~orig _ty rem_st t1 t2 rem_cont =
+ (* attempt to decompile t1 under the form
+ (epsilon fc. forall x. fc @ x = body)
+ that is equivalent to \x.body *)
+ match t1 with
+ | Term { t_node = Teps tb } ->
+ let fc,t = Term.t_open_bound tb in
+ begin match t.t_node with
+ | Tquant(Tforall,tq) ->
+ let vl,trig,t = t_open_quant tq in
+ let process lhs body equ elim =
+ let rvl = List.rev vl in
+ let rec remove_var lhs rvh rvt = match lhs.t_node with
+ | Tapp (ls2,[lhs1;{t_node = Tvar v1} as arg])
+ when ls_equal ls2 fs_func_app && vs_equal v1 rvh ->
+ begin
+ match rvt , lhs1 with
+ | rvh::rvt , _ ->
+ let lhs1 , fc2 = remove_var lhs1 rvh rvt in
+ let lhs2 = t_app ls2 [lhs1;arg] lhs.t_ty in
+ t_attr_copy lhs lhs2 , fc2
+ | [] , { t_node = Tvar fc1 } when vs_equal fc1 fc ->
+ let fcn = fc.vs_name in
+ let fc2 = Ident.id_derive fcn.Ident.id_string fcn in
+ let fc2 = create_vsymbol fc2 (t_type lhs) in
+ t_attr_copy lhs (t_var fc2) , fc2
+ | _ -> raise Undetermined
+ end
+ | _ -> raise Undetermined
+ in
+ begin
+ match rvl with
+ | rvh :: rvt -> let lhs , fc2 = remove_var lhs rvh rvt in
+ let (vh,vl) = match vl with
+ | [] -> assert false
+ | vh::vl -> (vh,vl)
+ in
+ let t2 = term_of_value t2 in
+ begin
+ match vl with
+ | [] -> elim body vh t2
+ | _ ->
+ let eq = equ lhs body in
+ let tq = t_quant Tforall (t_close_quant vl trig eq) in
+ let body = t_attr_copy t (t_eps_close fc2 tq) in
+ { value_stack = rem_st;
+ cont_stack =
+ (Keval(body,Mvs.add vh t2 Mvs.empty),
+ t_attr_copy orig body) :: rem_cont;
+ }
+ end
+ | _ -> raise Undetermined
+ end
+ in
+ begin
+ match t.t_node with
+ | Tapp (ls1,[lhs;body]) when ls_equal ls1 ps_equ ->
+ let equ lhs body = t_attr_copy t (t_app ps_equ [lhs;body] None) in
+ let elim body vh t2 = {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval(body,Mvs.add vh t2 Mvs.empty),
+ t_attr_copy orig body) :: rem_cont;
+ } in
+ process lhs body equ elim
+ | Tbinop (Tiff,
+ ({t_node=Tapp (ls1,[lhs;tr])} as teq),
+ body)
+ when ls_equal ls1 ps_equ && t_equal tr t_bool_true ->
+ let equ lhs body =
+ let lhs = t_attr_copy teq (t_app ps_equ [lhs;tr] None) in
+ t_attr_copy t (t_binary Tiff lhs body) in
+ let elim body vh t2 =
+ let body = t_if body t_bool_true t_bool_false in
+ { value_stack = rem_st;
+ cont_stack =
+ (Keval(body,Mvs.add vh t2 Mvs.empty),
+ t_attr_copy orig body) :: rem_cont } in
+ process lhs body equ elim
+ | _ -> raise Undetermined
+ end
+ | _ -> raise Undetermined
+ end
+ | _ -> raise Undetermined
+
+and reduce_app_no_equ engine st ls ~orig ty rem_cont =
+ let arity = List.length ls.ls_args in
+ let args,rem_st = extract_first arity [] st in
+ try
+ let f = Hls.find builtins ls in
+ let v = f ls args ty in
+ { value_stack = (v_attr_copy orig v) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ with Not_found | Undetermined ->
+ let args = List.map term_of_value args in
+ match Ident.Mid.find ls.ls_name engine.known_map with
+ | exception Not_found ->
+ Format.eprintf "Reduction engine, ident not found: %s@."
+ ls.ls_name.Ident.id_string ;
+ { value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ | d ->
+ let rewrite () =
+ (* try a rewrite rule *)
+ try
+(*
+ Format.eprintf "try a rewrite rule on %a@." Pretty.print_ls ls;
+*)
+ let (mt,mv),rhs = one_step_reduce engine ls args in
+(*
+ Format.eprintf "rhs = %a@." Pretty.print_term rhs;
+ Format.eprintf "sigma = ";
+ Mvs.iter
+ (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t)
+ (snd sigma);
+ Format.eprintf "@.";
+ Format.eprintf "try a type match: %a and %a@."
+ (Pp.print_option Pretty.print_ty) ty
+ (Pp.print_option Pretty.print_ty) rhs.t_ty;
+*)
+(*
+ let type_subst = Ty.oty_match Ty.Mtv.empty rhs.t_ty ty in
+ Format.eprintf "subst of rhs: ";
+ Ty.Mtv.iter
+ (fun tv ty -> Format.eprintf "%a -> %a,"
+ Pretty.print_tv tv Pretty.print_ty ty)
+ type_subst;
+ Format.eprintf "@.";
+ let rhs = t_ty_subst type_subst Mvs.empty rhs in
+ let sigma =
+ Mvs.map (t_ty_subst type_subst Mvs.empty) sigma
+ in
+ Format.eprintf "rhs = %a@." Pretty.print_term rhs;
+ Format.eprintf "sigma = ";
+ Mvs.iter
+ (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t)
+ sigma;
+ Format.eprintf "@.";
+*)
+ let mv,rhs = t_subst_types mt mv rhs in
+ incr(rec_step_limit);
+ { value_stack = rem_st;
+ cont_stack = (Keval(rhs,mv),orig) :: rem_cont;
+ }
+ with Irreducible ->
+ { value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ in
+ match d.Decl.d_node with
+ | Decl.Dtype _ | Decl.Dprop _ -> assert false
+ | Decl.Dlogic dl ->
+ (* regular definition *)
+ let d = List.assq ls dl in
+ if engine.params.compute_defs ||
+ Term.Sls.mem ls engine.params.compute_def_set
+ then begin
+ let vl,e = Decl.open_ls_defn d in
+ let add (mt,mv) x y =
+ Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv
+ in
+ let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl args in
+ let mt = Ty.oty_match mt e.t_ty ty in
+ let mv,e = t_subst_types mt mv e in
+ { value_stack = rem_st;
+ cont_stack = (Keval(e,mv),orig) :: rem_cont;
+ }
+ end else rewrite ()
+ | Decl.Dparam _ | Decl.Dind _ ->
+ rewrite ()
+ | Decl.Ddata dl ->
+ (* constructor or projection *)
+ begin try match args with
+ | [ { t_node = Tapp(ls1,tl1) } ] ->
+ (* if ls is a projection and ls1 is a constructor,
+ we should compute that projection *)
+ let rec iter dl =
+ match dl with
+ | [] -> raise Exit
+ | (_,csl) :: rem ->
+ let rec iter2 csl =
+ match csl with
+ | [] -> iter rem
+ | (cs,prs) :: rem2 ->
+ if ls_equal cs ls1
+ then
+ (* we found the right constructor *)
+ let rec iter3 prs tl1 =
+ match prs,tl1 with
+ | (Some pr)::prs, t::tl1 ->
+ if ls_equal ls pr
+ then (* projection found! *)
+ { value_stack =
+ (Term (t_attr_copy orig t)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ else
+ iter3 prs tl1
+ | None::prs, _::tl1 ->
+ iter3 prs tl1
+ | _ -> raise Exit
+ in iter3 prs tl1
+ else iter2 rem2
+ in iter2 csl
+ in iter dl
+ | _ -> raise Exit
+ with Exit -> rewrite () end
+
+
+and reduce_equ (* engine *) ~orig st v1 v2 cont =
+(*
+ try
+*)
+ match v1,v2 with
+ | Int n1, Int n2 ->
+ let b = to_bool (BigInt.eq n1 n2) in
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig b) :: st;
+ cont_stack = cont;
+ }
+ | Real r1, Real r2 ->
+ let b = to_bool (Number.compare_real r1 r2 = 0) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st;
+ cont_stack = cont;
+ }
+ | Int n, Term {t_node = Tconst c} | Term {t_node = Tconst c}, Int n ->
+ begin
+ try
+ let n' = big_int_of_const c in
+ let b = to_bool (BigInt.eq n n') in
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig b) :: st;
+ cont_stack = cont;
+ }
+ with NotNum -> raise Undetermined
+ end
+ | Real r, Term {t_node = Tconst c} | Term {t_node = Tconst c}, Real r ->
+ begin
+ try
+ let r' = real_of_const c in
+ let b = to_bool (Number.compare_real r r' = 0) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st;
+ cont_stack = cont;
+ }
+ with NotNum -> raise Undetermined
+ end
+ | Real _, Term _ | Term _, Real _ -> raise Undetermined
+ | Int _, Term _ | Term _, Int _ -> raise Undetermined
+ | Int _, Real _ | Real _, Int _ -> assert false
+ | Term t1, Term t2 -> reduce_term_equ ~orig st t1 t2 cont
+(*
+ with Undetermined ->
+ { value_stack = Term (t_equ (term_of_value v1) (term_of_value v2)) :: st;
+ cont_stack = cont;
+ }
+*)
+
+and reduce_term_equ ~orig st t1 t2 cont =
+ if t_equal t1 t2 then
+ let () = incr(rec_step_limit) in
+ { value_stack = Term (t_attr_copy orig t_true) :: st;
+ cont_stack = cont;
+ }
+ else
+ match (t1.t_node,t2.t_node) with
+ | Tconst c1, Tconst c2 ->
+ begin
+ match c1,c2 with
+ | Constant.ConstInt i1, Constant.ConstInt i2 ->
+ let b =
+ BigInt.eq i1.Number.il_int i2.Number.il_int
+ in
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig (to_bool b)) :: st;
+ cont_stack = cont;
+ }
+ | _ -> raise Undetermined
+ end
+ | Tapp(ls1,tl1), Tapp(ls2,tl2) when ls1.ls_constr > 0 && ls2.ls_constr > 0 ->
+ if ls_equal ls1 ls2 then
+ let rec aux sigma t tyl l1 l2 =
+ match tyl,l1,l2 with
+ | [],[],[] -> sigma,t
+ | ty::tyl, t1::tl1, t2::tl2 ->
+ let v1 = create_vsymbol (Ident.id_fresh "") ty in
+ let v2 = create_vsymbol (Ident.id_fresh "") ty in
+ aux
+ (Mvs.add v1 t1 (Mvs.add v2 t2 sigma))
+ (t_and_simp (t_equ (t_var v1) (t_var v2)) t)
+ tyl tl1 tl2
+ | _ -> assert false
+ in
+ let sigma,t =
+ aux Mvs.empty t_true ls1.ls_args tl1 tl2
+ in
+ let () = incr(rec_step_limit) in
+ { value_stack = st;
+ cont_stack = (Keval(t,sigma),orig) :: cont;
+ }
+ else
+ { value_stack = Term (t_attr_copy orig t_false) :: st;
+ cont_stack = cont;
+ }
+ | Tif (b,{ t_node = Tapp(ls1,_) },{ t_node = Tapp(ls2,_) }) , Tapp(ls3,_)
+ when ls_equal ls3 fs_bool_true && ls_equal ls1 fs_bool_true &&
+ ls_equal ls2 fs_bool_false ->
+ incr(rec_step_limit);
+ { value_stack = Term (t_attr_copy orig b) :: st;
+ cont_stack = cont }
+ | _ -> raise Undetermined
+
+
+
+let rec reconstruct c =
+ match c.value_stack, c.cont_stack with
+ | [Term t], [] -> t
+ | _, [] -> assert false
+ | _, (k,orig) :: rem ->
+ let t, st =
+ match c.value_stack, k with
+ | st, Keval (t,sigma) -> (t_subst sigma t), st
+ | [], Kif _ -> assert false
+ | v :: st, Kif(t2,t3,sigma) ->
+ (t_if (term_of_value v) (t_subst sigma t2) (t_subst sigma t3)), st
+ | [], Klet _ -> assert false
+ | t1 :: st, Klet(v,t2,sigma) ->
+ (t_let_close v (term_of_value t1) (t_subst sigma t2)), st
+ | [], Kcase _ -> assert false
+ | v :: st, Kcase(tbl,sigma) ->
+ (t_subst sigma (t_case (term_of_value v) tbl)), st
+ | ([] | [_]), Kbinop _ -> assert false
+ | t1 :: t2 :: st, Kbinop op ->
+ (t_binary_simp op (term_of_value t2) (term_of_value t1)), st
+ | [], Knot -> assert false
+ | t :: st, Knot -> (t_not (term_of_value t)), st
+ | st, Kapp(ls,ty) ->
+ let args,rem_st = extract_first (List.length ls.ls_args) [] st in
+ let args = List.map term_of_value args in
+ (t_app ls args ty), rem_st
+ | [], Keps _ -> assert false
+ | t :: st, Keps v -> (t_eps_close v (term_of_value t)), st
+ | [], Kquant _ -> assert false
+ | t :: st, Kquant(q,vl,tr) ->
+ (t_quant_close_simp q vl tr (term_of_value t)), st
+ in
+ reconstruct {
+ value_stack = (Term (t_attr_copy orig t)) :: st;
+ cont_stack = rem;
+ }
+
+
+(** iterated reductions *)
+
+let normalize ?step_limit ~limit engine sigma t0 =
+ rec_step_limit := 0;
+ let rec many_steps c n =
+ match c.value_stack, c.cont_stack with
+ | [Term t], [] -> t
+ | _, [] -> assert false
+ | _ ->
+ if n = limit then
+ begin
+ let t1 = reconstruct c in
+ (* Loc.warning "reduction of term %a takes more than %d steps, aborted at %a.@."
+ * Pretty.print_term t0 limit Pretty.print_term t1; *)
+ t1
+ end
+ else begin
+ match step_limit with
+ | None ->
+ let c = reduce engine c in
+ many_steps c (n+1)
+ | Some step_limit ->
+ if !rec_step_limit >= step_limit then
+ reconstruct c
+ else
+ let c = reduce engine c in
+ many_steps c (n+1)
+ end
+ in
+ let c = { value_stack = [];
+ cont_stack = [Keval(t0,sigma),t0] ;
+ }
+ in
+ many_steps c 0
+
+(* the rewrite engine *)
+
+let create p env km =
+ if p.compute_builtin
+ then get_builtins env
+ else Hls.clear builtins;
+ let th = Env.read_theory env ["int"] "Int" in
+ let ls_lt = Theory.ns_find_ls th.Theory.th_export [Ident.op_infix "<"] in
+ { known_map = km ;
+ rules = Mls.empty;
+ params = p;
+ ls_lt;
+ }
+
+exception NotARewriteRule of string
+
+let extract_rule _km t =
+(*
+ let check_ls ls =
+ try let _ = Hls.find builtins ls in
+ raise (NotARewriteRule "root of lhs of rule must not be a built-in symbol")
+ with Not_found ->
+ let d = Ident.Mid.find ls.ls_name km in
+ match d.Decl.d_node with
+ | Decl.Dtype _ | Decl.Dprop _ -> assert false
+ | Decl.Dlogic _ ->
+ raise (NotARewriteRule "root of lhs of rule must not be defined symbol")
+ | Decl.Ddata _ ->
+ raise (NotARewriteRule "root of lhs of rule must not be a constructor nor a projection")
+ | Decl.Dparam _ | Decl.Dind _ -> ()
+ in
+*)
+
+ let check_vars acc t1 t2 =
+ (* check that quantified variables all appear in the lefthand side
+ (quantified variables not appearing could be removed and those appearing
+ on right hand side cannot be guessed during rewriting). *)
+ let vars_lhs = t_vars t1 in
+ if Svs.exists (fun vs -> not (Mvs.mem vs vars_lhs)) acc
+ then raise (NotARewriteRule "lhs should contain all variables");
+ (* check the same with type variables *)
+ if not
+ (Ty.Stv.subset
+ (t_ty_freevars Ty.Stv.empty t2) (t_ty_freevars Ty.Stv.empty t2))
+ then raise (NotARewriteRule "lhs should contain all type variables")
+
+ in
+ let rec aux acc t =
+ match t.t_node with
+ | Tquant(Tforall,q) ->
+ let vs,_,t = t_open_quant q in
+ aux (List.fold_left (fun acc v -> Svs.add v acc) acc vs) t
+ | Tbinop(Tiff,t1,t2) ->
+ begin
+ match t1.t_node with
+ | Tapp(ls,args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ acc,ls,args,t2
+ | _ -> raise
+ (NotARewriteRule "lhs of <-> should be a predicate symbol")
+ end
+ | Tapp(ls,[t1;t2]) when ls == ps_equ ->
+ begin
+ match t1.t_node with
+ | Tapp(ls,args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ acc,ls,args,t2
+ | _ -> raise
+ (NotARewriteRule "lhs of = should be a function symbol")
+ end
+ | _ -> raise
+ (NotARewriteRule "rule should be of the form forall ... t1 = t2 or f1 <-> f2")
+ in
+ aux Svs.empty t
+
+
+let add_rule t e =
+ let vars,ls,args,r = extract_rule e.known_map t in
+ let rules =
+ try Mls.find ls e.rules
+ with Not_found -> []
+ in
+ {e with rules =
+ Mls.add ls ((vars,args,r)::rules) e.rules}
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
new file mode 100644
index 0000000..282ee55
--- /dev/null
+++ b/src/reduction_engine.mli
@@ -0,0 +1,133 @@
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2022 -- 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 engine
+(** abstract type for reduction engines *)
+
+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 *)
+
+val create : params -> Env.env -> Decl.decl Ident.Mid.t -> 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 -> engine -> 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 -> 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
diff --git a/src/verification.ml b/src/verification.ml
index 8fe43e4..1a7162e 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -274,10 +274,25 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
let id = Task.task_goal task in
{ id; prover_answer; additional_info }
-let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
- prover ?prover_altern file =
+let open_file ?(debug = false) ?format ~loadpath file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env ~debug loadpath in
+ let mstr_theory =
+ match file with
+ | File.Stdin ->
+ Env.(read_channel ?format base_language env "stdin" Caml.stdin)
+ | File file ->
+ let mlw_files, _ = Env.(read_file ?format base_language env file) in
+ mlw_files
+ | JSON jin ->
+ let th = JSON.theory_of_input env jin in
+ Wstdlib.Mstr.singleton th.th_name.id_string th
+ in
+ (env, config, mstr_theory)
+
+let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
+ ?prover_altern file =
+ let env, config, mstr_theory = open_file ?debug ?format ~loadpath file in
let main = Whyconf.get_main config in
let limit =
let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
@@ -292,17 +307,6 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
Call_provers.limit_mem = memlimit;
}
in
- let mstr_theory =
- match file with
- | File.Stdin ->
- Env.(read_channel ?format base_language env "stdin" Caml.stdin)
- | File file ->
- let mlw_files, _ = Env.(read_file ?format base_language env file) in
- mlw_files
- | JSON jin ->
- let th = JSON.theory_of_input env jin in
- Wstdlib.Mstr.singleton th.th_name.id_string th
- in
let config_prover =
let altern =
let default =
diff --git a/src/verification.mli b/src/verification.mli
index 8dc3939..0dabf96 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -23,7 +23,10 @@
open Why3
module File : sig
- type t
+ type t = private
+ | Stdin
+ | File of string
+ | JSON of JSON.input
val of_json_input : JSON.input -> (t, string) result
val of_string : string -> (t, string) result
@@ -71,3 +74,15 @@ val verify :
@return
for each theory, an [answer] for each goal of the theory, respecting the
order of appearance. *)
+
+val open_file :
+ ?debug:bool ->
+ ?format:string ->
+ loadpath:string list ->
+ File.t ->
+ Env.env * Whyconf.config * Theory.theory Wstdlib.Mstr.t
+(** [open_file ?debug ?format ~loadpath file] just opens the given file.
+
+ @param debug when set, enables debug information.
+ @param format is the [file] format.
+ @param loadpath is the additional loadpath. *)
diff --git a/tests/interpretation.t b/tests/interpretation.t
new file mode 100644
index 0000000..0b75c82
--- /dev/null
+++ b/tests/interpretation.t
@@ -0,0 +1,13 @@
+Test verify
+ $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
+ > theory T
+ > use int.Int
+ >
+ > goal G1: 1+1=2
+ >
+ > goal G2: 1+1=3
+ >
+ > end
+ > EOF
+ G1 : true
+ G2 : false
--
GitLab