From 0558b653dd111f2da19d3d0285d84348ad652150 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 24 Sep 2018 17:36:27 +0200
Subject: [PATCH] Reduce memory consumption of Why3.
This decreases the memory consumption by 10% on multiprecision/add.mlw.
---
src/transform/apply.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/transform/apply.ml b/src/transform/apply.ml
index 07cf91e60..ebab34178 100644
--- a/src/transform/apply.ml
+++ b/src/transform/apply.ml
@@ -296,7 +296,7 @@ let rewrite_list opt rev with_terms hl h1 =
(* Used to find the equality we are rewriting on *)
(* TODO here should fold with a boolean stating if we found equality yet to
not go through all possible hypotheses *)
- fold_decl (fun d (acclp,accterm) ->
+ fold_decl (fun d ((acclp,accterm) as acc) ->
match d.d_node with
| Dprop (Paxiom, pr, t) when Ident.id_equal pr.pr_name h.pr_name ->
let lp, lv, f = intros t in
@@ -311,10 +311,10 @@ let rewrite_list opt rev with_terms hl h1 =
let new_lp, new_term =
if opt
then try replace_subst lp lv t1 t2 with_terms accterm
- with Arg_trans _ -> (acclp, accterm)
+ with Arg_trans _ -> acc
else replace_subst lp lv t1 t2 with_terms accterm in
new_lp@acclp, new_term
- | _ -> (acclp, accterm)) (lp, term) in
+ | _ -> acc) (lp, term) in
let do_all = List.fold_left (fun acc h -> Trans.bind acc (do_h h)) found_term hl in
(* Pass the premises as new goals. Replace the former toberewritten
hypothesis to the new rewritten one *)
--
GitLab