From 430143c1ca8856a2b6406d50dff80589bcdafd3f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 24 Jan 2022 15:25:02 +0100
Subject: [PATCH] [wp] Change F_subst signature
---
src/plugins/qed/engine.mli | 4 +++-
src/plugins/qed/export.ml | 4 ++--
src/plugins/qed/export_why3.ml | 2 +-
src/plugins/wp/MemMemory.ml | 19 ++++---------------
src/plugins/wp/MemVal.ml | 8 ++------
src/plugins/wp/ProverWhy3.ml | 3 +--
src/plugins/wp/driver.mll | 5 +----
7 files changed, 14 insertions(+), 31 deletions(-)
diff --git a/src/plugins/qed/engine.mli b/src/plugins/qed/engine.mli
index 65dbd5cad46..7d91ca390d6 100644
--- a/src/plugins/qed/engine.mli
+++ b/src/plugins/qed/engine.mli
@@ -36,7 +36,9 @@ type op =
type link =
| F_call of string (** n-ary function *)
- | F_subst of string (** n-ary function with substitution "foo(%1,%2)" *)
+ | F_subst of string * string (** n-ary function with substitution
+ first value is the link name, second is the
+ substitution (e.g. "foo(%1,%2)") *)
| F_left of string (** 2-ary function left-to-right + *)
| F_right of string (** 2-ary function right-to-left + *)
| F_list of string * string (** n-ary function with (cons,nil) constructors *)
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index c1d37be3920..452b8b472cf 100644
--- a/src/plugins/qed/export.ml
+++ b/src/plugins/qed/export.ml
@@ -65,7 +65,7 @@ let link_name = function
let debug = function
| F_call f | F_left f | F_right f | F_bool_prop(_,f)
- | F_list(f,_) | F_subst f | F_assoc f -> f
+ | F_list(f,_) | F_subst (f, _) | F_assoc f -> f
(* -------------------------------------------------------------------------- *)
(* --- Identifiers --- *)
@@ -451,7 +451,7 @@ struct
fc self#pp_atom x (plist w) xs
in plist (self#callstyle,fc,fn) fmt xs
end
- | F_subst s, _ ->
+ | F_subst (_, s), _ ->
let print = match self#callstyle with
| CallVar | CallVoid -> self#pp_flow
| CallApply -> self#pp_atom in
diff --git a/src/plugins/qed/export_why3.ml b/src/plugins/qed/export_why3.ml
index 6ed4f1b2e7b..2d7b39ce7c3 100644
--- a/src/plugins/qed/export_why3.ml
+++ b/src/plugins/qed/export_why3.ml
@@ -231,7 +231,7 @@ struct
| F_left f, _ -> Plib.pp_fold_apply ~f pretty fmt ts
| F_right f, _ -> Plib.pp_fold_apply_rev ~f pretty fmt (List.rev ts)
| F_assoc op, _ -> Plib.pp_assoc ~op pretty fmt ts
- | F_subst s, _ -> Plib.substitute_list pretty s fmt ts
+ | F_subst (_, s), _ -> Plib.substitute_list pretty s fmt ts
| F_list(fc,fn) , _ ->
let rec plist fc fn fmt = function
| [] -> pp_print_string fmt fn
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index a9c94fe2263..7c4439368ec 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -34,13 +34,9 @@ let library = "memory"
let a_addr = Lang.datatype ~library "addr"
let t_addr = L.Data(a_addr,[])
let f_base = Lang.extern_f ~library ~result:L.Int
- ~link:{why3 = Qed.Engine.F_call "base";
- coq = Qed.Engine.F_subst("(base %1)");
- } "base"
+ ~link:(Qed.Engine.F_subst ("base", "%1.base")) "base"
let f_offset = Lang.extern_f ~library ~result:L.Int
- ~link:{why3 = Qed.Engine.F_call "offset";
- coq = Qed.Engine.F_subst("(offset %1)");
- } "offset"
+ ~link:(Qed.Engine.F_subst ("offset", "%1.offset")) "offset"
let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
let f_global = Lang.extern_f ~library ~result:t_addr ~category:L.Injection "global"
let f_null = Lang.extern_f ~library ~result:t_addr "null"
@@ -58,15 +54,8 @@ let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
-let l_havoc = Qed.Engine.{
- coq = F_call "fhavoc" ;
- why3 = F_call "havoc" ;
- }
-
-let l_set_init = Qed.Engine.{
- coq = F_call "fset_init" ;
- why3 = F_call "set_init" ;
- }
+let l_havoc = Qed.Engine.F_call "havoc"
+let l_set_init = Qed.Engine.F_call "set_init"
let p_valid_rd = Lang.extern_fp ~library "valid_rd"
let p_valid_rw = Lang.extern_fp ~library "valid_rw"
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index b880015256d..f9ce1bc2aee 100644
--- a/src/plugins/wp/MemVal.ml
+++ b/src/plugins/wp/MemVal.ml
@@ -93,13 +93,9 @@ let library = "memory"
let a_addr = Lang.datatype ~library "addr"
let t_addr = Logic.Data(a_addr,[])
let f_base = Lang.extern_f ~library ~result:Logic.Int
- ~link:{why3 = Qed.Engine.F_subst("%1.base");
- coq = Qed.Engine.F_subst("(base %1)");
- } "base"
+ ~link:(Qed.Engine.F_subst ("base", "%1.base")) "base"
let f_offset = Lang.extern_f ~library ~result:Logic.Int
- ~link:{why3 = Qed.Engine.F_subst("%1.offset");
- coq = Qed.Engine.F_subst("(offset %1)");
- } "offset"
+ ~link:(Qed.Engine.F_subst ("offset", "%1.offset")) "offset"
let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
let f_global = Lang.extern_f ~library ~result:t_addr "global"
let f_null = Lang.extern_f ~library ~result:t_addr "null"
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index c0cb6f8e847..a21e48d0d86 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -520,8 +520,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
in
match lfun_name f, expected with
| F_call s, _ -> apply_from_ns' s l sort
- | Qed.Engine.F_subst _, _ ->
- why3_failure "Driver link with subst not yet implemented"
+ | Qed.Engine.F_subst (s, _), _ -> apply_from_ns' s l sort
| Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
let rec aux = function
| [] -> why3_failure "Empty application"
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index 3f297a4ddd5..400780fc71d 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -81,10 +81,7 @@
| `Default -> conv_bal default (name,default)
| `Left -> Qed.Engine.F_left name
| `Right -> Qed.Engine.F_right name
- | `Nary ->
- if Qed.Plib.is_template name
- then Qed.Engine.F_subst name
- else Qed.Engine.F_call name
+ | `Nary -> Qed.Engine.F_call name
}
--
GitLab