From b3e0c913f34e42e067a5142352df7a407aa70dcd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 4 Jan 2022 12:52:00 +0100
Subject: [PATCH] [wp] Removes legacy pid
---
src/plugins/wp/ProofEngine.ml | 1 -
src/plugins/wp/ProofSession.ml | 1 -
src/plugins/wp/ProverCoq.ml | 7 +--
src/plugins/wp/cfgWP.ml | 7 +--
src/plugins/wp/proof.ml | 18 ++----
src/plugins/wp/proof.mli | 4 +-
src/plugins/wp/tests/wp/stmtcompiler_test.ml | 2 +-
.../wp/tests/wp/stmtcompiler_test_rela.ml | 2 -
src/plugins/wp/wpPropId.ml | 63 -------------------
src/plugins/wp/wpPropId.mli | 1 -
src/plugins/wp/wpo.ml | 2 -
src/plugins/wp/wpo.mli | 1 -
12 files changed, 11 insertions(+), 98 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index fc339fef85e..ff5c98207f2 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -307,7 +307,6 @@ let mk_goal t ~title ~part ~axioms sequent =
let sid = Printf.sprintf "%s-%d" t.main.Wpo.po_sid id in
Wpo.({
po_gid = gid ;
- po_leg = "" ; (* no use for legacy name *)
po_sid = sid ;
po_name = Printf.sprintf "%s (%s)" title part ;
po_idx = t.main.po_idx ;
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 106f45f28e3..2839d1012fc 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -43,7 +43,6 @@ let legacies wpo =
[
jsonfile dscript wpo.po_gid ;
jsonfile dmodel wpo.po_gid ;
- jsonfile dmodel wpo.po_leg ;
]
let get wpo =
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 5519ecdb256..75a1361e434 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -525,7 +525,6 @@ open Wpo
type coq_wpo = {
cw_pid : WpPropId.prop_id ;
cw_gid : string ;
- cw_leg : string ;
cw_goal : string ; (* filename for goal without proof *)
cw_script : string ; (* filename for goal with proof script *)
cw_headers : string list ; (* filename for libraries *)
@@ -558,7 +557,7 @@ let rec try_hints w = function
let try_prove w =
begin
- match Proof.script_for ~pid:w.cw_pid ~gid:w.cw_gid ~legacy:w.cw_leg with
+ match Proof.script_for ~pid:w.cw_pid ~gid:w.cw_gid with
| Some (script,closing) ->
Wp_parameters.feedback ~ontty "[Coq] Goal %s : Saved script" w.cw_gid ;
try_script w script closing
@@ -572,7 +571,7 @@ let try_prove w =
let try_coqide w =
let script,closing =
- Proof.script_for_ide ~pid:w.cw_pid ~gid:w.cw_gid ~legacy:w.cw_leg in
+ Proof.script_for_ide ~pid:w.cw_pid ~gid:w.cw_gid in
make_script w script closing ;
(new runcoq w.cw_includes w.cw_script)#coqide >>= fun st ->
if st = 0 then
@@ -632,7 +631,6 @@ let prove_session ~mode w =
let prove_prop wpo ~mode ~axioms ~prop =
let pid = wpo.po_pid in
let gid = wpo.po_gid in
- let leg = wpo.po_leg in
let model = wpo.po_model in
let context = Wpo.get_context wpo in
let script = DISK.file_goal ~pid ~model ~prover:NativeCoq in
@@ -642,7 +640,6 @@ let prove_prop wpo ~mode ~axioms ~prop =
prove_session ~mode {
cw_pid = pid ;
cw_gid = gid ;
- cw_leg = leg ;
cw_goal = goal ;
cw_script = script ;
cw_headers = headers ;
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 1bece5f01ae..2ce1303333b 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1498,7 +1498,6 @@ struct
po_pid = pid ;
po_sid = "" ;
po_gid = "" ;
- po_leg = "" ;
po_name = "" ;
po_idx = index ;
po_formula = GoalAnnot vcq ;
@@ -1557,12 +1556,10 @@ struct
WpPropId.split_bag
begin fun po_pid wpo ->
let po_sid = WpPropId.get_propid po_pid in
- let po_leg = WpPropId.get_legacy po_pid in
let po_gid = Printf.sprintf "%s_%s" mid po_sid in
- let po_leg = Printf.sprintf "%s_%s" mid po_leg in
let po_name = Pretty_utils.to_string WpPropId.pretty_local pid in
let wpo =
- { wpo with po_pid ; po_sid ; po_gid ; po_leg ; po_name }
+ { wpo with po_pid ; po_sid ; po_gid ; po_name }
in
Wpo.add wpo ;
collection := Bag.append !collection wpo ;
@@ -1589,11 +1586,9 @@ struct
| LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
let mid = WpContext.MODEL.id model in
let sid = WpPropId.get_propid id in
- let leg = WpPropId.get_legacy id in
let wpo = {
Wpo.po_model = model ;
Wpo.po_gid = Printf.sprintf "%s_%s" mid sid ;
- Wpo.po_leg = Printf.sprintf "%s_%s" mid leg ;
Wpo.po_sid = sid ;
Wpo.po_name = Printf.sprintf "Lemma '%s'" l.lem_name ;
Wpo.po_idx = index ;
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
index f7f06f01564..f9d54288e6a 100644
--- a/src/plugins/wp/proof.ml
+++ b/src/plugins/wp/proof.ml
@@ -205,19 +205,11 @@ let loadscripts () =
end
end
-let find_script_for_goal ~gid ~legacy =
+let find_script_for_goal ~gid =
loadscripts () ;
try
let _,proof,qed = Hashtbl.find scriptbase gid in
Some(proof,qed)
- with Not_found ->
- try
- let (_,proof,qed) as entry = Hashtbl.find scriptbase legacy in
- Wp_parameters.feedback "Upgrading Coq script for '%s'" gid ;
- Hashtbl.add scriptbase gid entry ;
- Hashtbl.remove scriptbase legacy ;
- needsave := true ;
- Some(proof,qed)
with Not_found ->
None
@@ -276,8 +268,8 @@ let add_script_for ~gid hints proof =
(* --- Prover API --- *)
(* -------------------------------------------------------------------------- *)
-let script_for ~pid ~gid ~legacy =
- let found = find_script_for_goal ~gid ~legacy in
+let script_for ~pid ~gid =
+ let found = find_script_for_goal ~gid in
( if found <> None then
let required,hints = WpPropId.prop_id_keys pid in
let all = List.merge String.compare required hints in
@@ -301,8 +293,8 @@ let hints_for ~pid =
else default
else default
-let script_for_ide ~pid ~gid ~legacy =
- match find_script_for_goal ~gid ~legacy with
+let script_for_ide ~pid ~gid =
+ match find_script_for_goal ~gid with
| Some script -> script
| None ->
let required,hints = WpPropId.prop_id_keys pid in
diff --git a/src/plugins/wp/proof.mli b/src/plugins/wp/proof.mli
index 17b88dd6f51..8fb4c7f14a7 100644
--- a/src/plugins/wp/proof.mli
+++ b/src/plugins/wp/proof.mli
@@ -43,6 +43,6 @@ val savescripts : unit -> unit
(** If necessary, dump the scripts database into the file
specified by [-wp-script f]. *)
-val script_for : pid:prop_id -> gid:string -> legacy:string -> (string * string) option
-val script_for_ide : pid:prop_id -> gid:string -> legacy:string -> string * string
+val script_for : pid:prop_id -> gid:string -> (string * string) option
+val script_for_ide : pid:prop_id -> gid:string -> string * string
val hints_for : pid:prop_id -> (string * string * string) list
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index e104a2e5c46..0cc749a809c 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -50,7 +50,7 @@ let run () =
effect = None;
} in
let po = Wpo.{
- po_gid = ""; po_sid = ""; po_name = ""; po_leg = "";
+ po_gid = ""; po_sid = ""; po_name = "";
po_idx = Function(kf, None); po_model = model;
po_pid = prop_id;
po_formula = Wpo.GoalAnnot vc_annot;
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 9770e9b4295..12849805c20 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -58,7 +58,6 @@ let run () =
let annot = Logic_const.new_code_annotation (AAssert ([],pred)) in
let po = Wpo.{
po_gid = "";
- po_leg = "";
po_sid = "";
po_name = "";
po_idx = Function(kf, None);
@@ -73,7 +72,6 @@ let run () =
| h :: _ ->
inter_po := Wpo.{
po_gid = "";
- po_leg = "";
po_sid = "";
po_name = "";
po_idx = Function(kf, None);
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 8071f178960..6bb11c8b687 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -328,66 +328,6 @@ struct
end
-module LegacyNames :
-sig
- val get_prop_id_name: prop_id -> string
-end = struct
-
- let base_id_prop_txt = Property.LegacyNames.get_prop_name_id
-
- let basename_of_prop_id p =
- match p.p_kind , p.p_prop with
- | PKEstablished , p -> base_id_prop_txt p ^ "_established"
- | PKPreserved , p -> base_id_prop_txt p ^ "_preserved"
- | PKVarDecr , p -> base_id_prop_txt p ^ "_decrease"
- | PKVarPos , p -> base_id_prop_txt p ^ "_positive"
- | PKVarRel , p -> base_id_prop_txt p ^ "_relation"
- | PKAFctOut , p -> base_id_prop_txt p ^ "_normal"
- | PKAFctExit , p -> base_id_prop_txt p ^ "_exit"
- | PKPre(_kf,stmt,pre) , _ ->
- let kf_name_of_stmt =
- Kernel_function.get_name
- (Kernel_function.find_englobing_kf stmt)
- in Printf.sprintf "%s_call_%s" kf_name_of_stmt (base_id_prop_txt pre)
- | _ , p ->
- base_id_prop_txt p
-
-
- (** function used to normalize basename *)
- let normalize_basename s =
- (* truncates basename in order to limit length of file name *)
- let max_len = Wp_parameters.TruncPropIdFileName.get () in
- if max_len > 0 && String.length s > max_len then
- if max_len > 3 then (String.sub s 0 (max_len-3)) ^ "___"
- else String.sub s 0 max_len
- else s
-
- (** returns the normalized basename of the property. *)
- let get_prop_id_basename p =
- let basename = basename_of_prop_id p in
- let basename = match p.p_part with
- | None -> basename
- | Some(k,n) ->
- if n < 10 then Printf.sprintf "%s_part%d" basename (succ k) else
- if n < 100 then Printf.sprintf "%s_part%02d" basename (succ k) else
- if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
- Printf.sprintf "%s_part%06d" basename (succ k)
- in normalize_basename basename
-
-
- module UniquifyPropId = NameUniquify(PropIdRaw)(struct
- let name = "WpProperty"
- let basename = get_prop_id_basename
- end)
-
-
- (** returns a unique name identifying the property.
- This name is built from the basename of the property. *)
- let get_prop_id_name pid =
- UniquifyPropId.unique_basename pid
-
-end
-
(* -------------------------------------------------------------------------- *)
(* --- Naming Properties --- *)
(* -------------------------------------------------------------------------- *)
@@ -471,9 +411,6 @@ end
(* --- Naming Accessors --- *)
(* -------------------------------------------------------------------------- *)
-let get_legacy = LegacyNames.get_prop_id_name
-(** Legacy property PO name *)
-
let get_propid = Names.get_prop_id_name
(** Name related to a property PO *)
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 469a8ee011d..d56bc1a6251 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -79,7 +79,6 @@ val ident_names : string list -> string list
val prop_id_keys : prop_id -> string list * string list (* required , hints *)
val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
-val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
val user_pred_names: toplevel_predicate -> string list
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index d94196679bf..699646cfaa8 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -378,7 +378,6 @@ type formula =
type po = t and t = {
po_gid : string ; (* goal identifier *)
- po_leg : string ; (* legacy goal identifier *)
po_sid : string ; (* goal short identifier (without model) *)
po_name : string ; (* goal informal name *)
po_idx : index ; (* goal index *)
@@ -456,7 +455,6 @@ module S =
po_pid = List.hd WpPropId.PropId.reprs;
po_sid = "";
po_gid = "";
- po_leg = "";
po_model = WpContext.MODEL.repr ;
po_name = "dummy";
po_formula = GoalAnnot VC_Annot.repr ;
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 580b6469497..763b485f663 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -104,7 +104,6 @@ type formula =
type po = t and t = {
po_gid : string ; (** goal identifier *)
- po_leg : string ; (** legacy goal identifier *)
po_sid : string ; (** goal short identifier (without model) *)
po_name : string ; (** goal informal name *)
po_idx : index ; (** goal index *)
--
GitLab