From 3ac8c62dc65ac256d1ce1a138ad1e9d0c85e72ad Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 26 Jun 2019 14:05:40 +0200
Subject: [PATCH] [wp] replaces lc_open by e_open into Conditions.ml
---
src/plugins/wp/Conditions.ml | 38 ++++++++++++++++++++++--------------
1 file changed, 23 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index a0e859f8d20..0db4c196dcd 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -410,20 +410,22 @@ let prenex_intro p =
let rec walk hs xs p =
match F.p_expr p with
| Imply(h,p) -> walk (h::hs) xs p
- | Bind(Forall,tau,p) -> bind hs xs tau p
+ | Bind(Forall,_,_) -> bind hs xs p
| _ ->
if hs = [] then raise Exit ;
F.p_forall (List.rev xs) (F.p_hyps (List.concat hs) p)
(* invariant: result <-> forall hs xs (\tau.bind) *)
- and bind hs xs tau bind =
- let x = Lang.freshvar tau in
- let p = F.p_bool (F.QED.lc_open x bind) in
- walk hs (x::xs) p
+ and bind hs xs p =
+ let pool = Lang.get_pool () in
+ let ctx,t = e_open ~pool ~forall:true
+ ~exists:false ~lambda:false (e_prop p) in
+ let xs = List.fold_left (fun xs (_,x) -> x::xs) xs (List.rev ctx) in
+ walk hs xs (F.p_bool t)
(* invariant: result <-> p *)
and crawl p =
match F.p_expr p with
| Imply(h,p) -> F.p_hyps h (crawl p)
- | Bind(Forall,tau,p) -> bind [] [] tau p
+ | Bind(Forall,_,_) -> bind [] [] p
| _ -> raise Exit
in crawl p
with Exit -> p
@@ -436,9 +438,11 @@ let rec exist_intro p =
let open Qed.Logic in
match F.p_expr p with
| And ps -> F.p_all exist_intro ps
- | Bind(Exists,tau,p) ->
- let x = Lang.freshvar tau in
- exist_intro (F.p_bool (F.QED.lc_open x p))
+ | Bind(Exists,_,_) ->
+ let pool = Lang.get_pool () in
+ let _,t = e_open ~pool ~exists:true
+ ~forall:false ~lambda:false (e_prop p) in
+ exist_intro (F.p_bool t)
| _ ->
if Wp_parameters.Prenex.get ()
then prenex_intro p
@@ -450,9 +454,11 @@ let rec exist_intros = function
let open Qed.Logic in
match F.p_expr p with
| And ps -> exist_intros (ps@hs)
- | Bind(Exists,tau,p) ->
- let x = Lang.freshvar tau in
- exist_intros ((F.p_bool (F.QED.lc_open x p))::hs)
+ | Bind(Exists,_,_) ->
+ let pool = Lang.get_pool () in
+ let _,t = F.QED.e_open ~pool ~exists:true
+ ~forall:false ~lambda:false (e_prop p) in
+ exist_intros ((F.p_bool t)::hs)
| _ -> p::(exist_intros hs)
end
@@ -463,9 +469,11 @@ let rec exist_intros = function
let rec forall_intro p =
let open Qed.Logic in
match F.p_expr p with
- | Bind(Forall,tau,p) ->
- let x = Lang.freshvar tau in
- forall_intro (F.p_bool (F.QED.lc_open x p))
+ | Bind(Forall,_,_) ->
+ let pool = Lang.get_pool () in
+ let _,t = F.QED.e_open ~pool ~forall:true
+ ~exists:false ~lambda:false (e_prop p) in
+ forall_intro (F.p_bool t)
| Imply(hs,p) ->
let hs = exist_intros hs in
let hs = List.map (fun p -> step (Have p)) hs in
--
GitLab