From df406886a252faeef80c55af41fdfdb8fcb9b912 Mon Sep 17 00:00:00 2001
From: Nathan Koskas de Diego <nathan.koskasdediego@cea.fr>
Date: Fri, 25 Mar 2022 18:18:39 +0100
Subject: [PATCH] [qed] optimization of Qed.Term.bind
---
src/plugins/qed/term.ml | 25 ++++++++++---------------
1 file changed, 10 insertions(+), 15 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 77ad2323425..935f3729c9f 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2301,6 +2301,15 @@ struct
let filter sigma e =
Subst.filter sigma e || not (Bvars.is_empty e.bind)
+ let bind_qxs qxs e =
+ let qxs = List.filter (function
+ | Lambda, _ -> true
+ | Forall, x | Exists, x -> Vars.mem x e.vars
+ ) qxs in
+ let xs = List.map (fun (_q, x) -> x) qxs in
+ let e = lc_close_xs xs e in
+ List.fold_right (fun (q, x) e -> c_bind q (tau_of_var x) e) qxs e
+
let rec subst sigma alpha e =
if filter sigma e then
incache (Subst.cache sigma) sigma alpha e
@@ -2336,21 +2345,7 @@ struct
let alpha = Intmap.add k (e_var x) alpha in
let qs = (q,x) :: qs in
bind sigma alpha qs a
- | _ ->
- (* HERE:
- This final binding of variables could be parallelized
- if Bvars is precise enough *)
- List.fold_left
- (fun e (q,x) ->
- if Vars.mem x e.vars then
- let t = tau_of_var x in
- (* HERE:
- possible to insert a recursive call to let-intro
- it will use a new instance of e_subst_var that
- will work on a different sigma *)
- c_bind q t (lc_close x e)
- else e
- ) (subst sigma alpha e) qs
+ | _ -> bind_qxs qs (subst sigma alpha e)
and apply sigma beta f vs =
match f.repr, vs with
--
GitLab