From 8e495f9616b6c578583e043919a40fdbff8c6b26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 27 Jun 2019 15:37:09 +0200
Subject: [PATCH] [wp+qed] remove lc_bind and lc_open
---
src/plugins/qed/logic.ml | 8 +++++---
src/plugins/qed/term.ml | 36 ++++++++++++++++++-----------------
src/plugins/wp/TacInstance.ml | 2 +-
3 files changed, 25 insertions(+), 21 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 83ed15378f0..829356d7002 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -306,6 +306,11 @@ sig
(** Bind the given variable if it appears free in the term,
or return the term unchanged. *)
+ val e_unbind : var -> lc_term -> term
+ (** Opens the top-most bound variable with a (fresh) variable.
+ Can be only applied on top-most lc-term from `Bind(_,_,_)`,
+ thanks to typing. *)
+
val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
term -> (binder * var) list * term
(** Open all the specified binders (flags default to `true`, so all
@@ -362,9 +367,6 @@ sig
(** {3 Locally Nameless Representation} *)
- val lc_bind : var -> term -> lc_term (** Bind x with top bound variable *)
- val lc_open : var -> lc_term -> term (** Open top bound variable with x *)
-
val lc_empty : term -> bool (** No bound variables *)
val lc_closed : term -> bool (** All bound variables are under their binder *)
val lc_closed_at : int -> term -> bool
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 7448b14d454..ce7a97cd2fc 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2280,23 +2280,6 @@ struct
| _ -> is_eq e
in ignore(exists_case a); !res
- let e_bind q x (e : term) =
- assert (lc_closed e) ;
- let do_bind =
- match q with Forall | Exists -> Vars.mem x e.vars | Lambda -> true in
- if do_bind then
- match let_intro_case q x e with
- | None -> c_bind q (tau_of_var x) (lc_bind x e)
- | Some v -> e_subst_var x v e (* case [let x = v ; e] *)
- else e
-
- let rec bind_xs q xs e =
- match xs with [] -> e | x::xs -> e_bind q x (bind_xs q xs e)
-
- let e_forall = bind_xs Forall
- let e_exists = bind_xs Exists
- let e_lambda = bind_xs Lambda
-
let e_open ~pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
match a.repr with
| Bind _ ->
@@ -2312,8 +2295,27 @@ struct
in walk [] a
| _ -> [],a
+ let e_unbind x (lc : lc_term) : term =
+ assert (not (Vars.mem x lc.vars)); lc_open x lc
+
+ let e_bind q x (e : term) =
+ let do_bind =
+ match q with Forall | Exists -> Vars.mem x e.vars | Lambda -> true in
+ if do_bind then
+ match let_intro_case q x e with
+ | None -> c_bind q (tau_of_var x) (lc_bind x e)
+ | Some v -> e_subst_var x v e (* case [let x = v ; e] *)
+ else e
+
let e_close qs a = List.fold_left (fun b (q,x) -> e_bind q x b) a qs
+ let rec bind_xs q xs e =
+ match xs with [] -> e | x::xs -> e_bind q x (bind_xs q xs e)
+
+ let e_forall = bind_xs Forall
+ let e_exists = bind_xs Exists
+ let e_lambda = bind_xs Lambda
+
(* -------------------------------------------------------------------------- *)
(* --- Iterators --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 42eb158d569..9e5f2c1311c 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -159,7 +159,7 @@ class instance =
let tooltip = fieldname ~range env.index x in
env.feedback#update_field
~tooltip ~range ~enabled:true ~filter:(filter x) fd ;
- let lemma = F.QED.lc_open x phi in
+ let lemma = F.QED.e_unbind x phi in
let bindings,property = self#wrap env lemma fields in
(x,v) :: bindings , property
| _ ->
--
GitLab