From a384d0bb61c08c807cc19e329e38ba44e44c3d5c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 31 Jan 2022 09:16:05 +0100
Subject: [PATCH] [wp] Multi select tactic - not available from GUI for now -
TacClear and TacUnfold adapted
---
src/plugins/wp/GuiSequent.ml | 2 +-
src/plugins/wp/ProofScript.ml | 7 ++
src/plugins/wp/TacChoice.ml | 6 +-
src/plugins/wp/TacClear.ml | 89 +++++++++++++++--------
src/plugins/wp/TacCompound.ml | 2 +-
src/plugins/wp/TacNormalForm.ml | 2 +-
src/plugins/wp/TacSplit.ml | 2 +-
src/plugins/wp/TacUnfold.ml | 101 ++++++++++++++++++++++++--
src/plugins/wp/Tactical.ml | 15 +++-
src/plugins/wp/Tactical.mli | 3 +
src/plugins/wp/tests/wp_tip/TacNOP.ml | 1 +
11 files changed, 184 insertions(+), 46 deletions(-)
diff --git a/src/plugins/wp/GuiSequent.ml b/src/plugins/wp/GuiSequent.ml
index fdb29988b39..aaf112abc48 100644
--- a/src/plugins/wp/GuiSequent.ml
+++ b/src/plugins/wp/GuiSequent.ml
@@ -623,7 +623,7 @@ class focused (wtext : Wtext.text) =
method set_target tgt =
match tgt with
- | Tactical.Empty | Tactical.Compose _ ->
+ | Tactical.Empty | Tactical.Compose _ | Tactical.Multi _ ->
begin
pcond#set_target Term ;
plang#clear_target ;
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 3e0bcc83cc2..531175ba1ee 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -97,6 +97,7 @@ let j_step = j_select "clause-step"
let j_ingoal = j_select "inside-goal"
let j_instep = j_select "inside-step"
let j_compose = j_select "compose"
+let j_multi = j_select "multi"
let j_kint = j_select "kint"
let j_range = j_select "range"
let j_id a = "id" , `String a
@@ -136,6 +137,9 @@ let rec json_of_selection = function
`Assoc [ j_instep ; j_at s ; j_kind s ; j_occur n ;
j_term e ; j_pattern m ]
+ | Multi es ->
+ `Assoc (j_multi :: j_args es)
+
and j_args = function
| [] -> []
| es -> ["args" , `List (List.map json_of_selection es)]
@@ -184,6 +188,9 @@ let rec selection_of_json ((hs,g) as s : sequent) js =
let id = j_id js in
let args = j_args js in
Tactical.compose id (List.map (selection_of_json s) args)
+ | "multi" ->
+ let args = j_args js in
+ Tactical.multi @@ List.map (selection_of_json s) args
| "kint" -> Tactical.cint (j_val js)
| "range" -> Tactical.range (j_min js) (j_max js)
| _ -> raise Not_found
diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index 31f3ee05e0c..28ba26f16ae 100644
--- a/src/plugins/wp/TacChoice.ml
+++ b/src/plugins/wp/TacChoice.ml
@@ -45,7 +45,7 @@ class choice =
Applicable (fun (hs,_) -> ["Choice",(hs,F.p_bool q)])
| _ -> Not_applicable
end
- | Empty | Compose _ | Clause _ | Inside(Step _,_) ->
+ | Empty | Compose _ | Clause _ | Inside(Step _,_) | Multi _ ->
Not_applicable
end
@@ -59,7 +59,7 @@ class absurd =
method select _feedback (s : Tactical.selection) =
match s with
- | Empty | Compose _ | Inside _ | Clause(Goal _)
+ | Empty | Compose _ | Inside _ | Clause(Goal _) | Multi _
-> Not_applicable
| Clause(Step s) ->
begin
@@ -85,7 +85,7 @@ class contrapose =
method select _feedback (s : Tactical.selection) =
match s with
- | Empty | Compose _ | Inside _ | Clause(Goal _)
+ | Empty | Compose _ | Inside _ | Clause(Goal _) | Multi _
-> Not_applicable
| Clause(Step s) ->
begin
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index a16fa3aa2f7..fb177fc292b 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -23,6 +23,58 @@
open Tactical
open Conditions
+let condition original p = (* keep original kind of simple condition *)
+ match original.condition with
+ | Type _ -> Type p
+ | Have _ -> Have p
+ | When _ -> When p
+ | Core _ -> Core p
+ | Init _ -> Init p
+ | _ -> assert false
+
+let tactical_step step =
+ Tactical.replace_single ~at:step.id ("Removed", Conditions.Have Lang.F.p_true)
+
+let tactical_inside step remove =
+ let rec collect p =
+ match Lang.F.p_expr p with
+ | And ps -> collect_list ps
+ | _ -> [ p ]
+ and collect_list = function
+ | [] -> []
+ | p :: l -> List.rev_append (List.rev @@ collect p) (collect_list l)
+ in
+ begin match step.condition with
+ | Type p | Have p | When p | Core p | Init p ->
+ let ps = Lang.F.e_props @@ collect p in
+ let ps = List.filter (fun x -> not @@ List.mem x remove) ps in
+ let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and ps in
+ Tactical.replace_single ~at:step.id ("Filtered", cond)
+
+ | _ -> raise Not_found
+ end
+
+module Smap = Qed.Idxmap.Make
+ (struct
+ type t = step
+ let id s = s.id
+ end)
+
+let collect_remove m = function
+ | Inside(Step step, remove) ->
+ let l =
+ try Smap.find step m
+ with Not_found -> []
+ in
+ Smap.add step (remove :: l) m
+ | _ -> raise Not_found
+
+let fold_selection s seq =
+ let m = List.fold_left collect_remove Smap.empty s in
+ "Filtered", Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+
+let process (f: sequent -> string * sequent) s = [ f s ]
+
class clear =
object(_)
inherit Tactical.make ~id:"Wp.clear"
@@ -33,39 +85,14 @@ class clear =
method select _feedback sel =
match sel with
| Clause(Step step) ->
- let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
- Applicable (Tactical.replace ~at:step.id removed)
+ Applicable(process @@ tactical_step step)
| Inside(Step step, remove) ->
- let cond p = (* keep original kind of step *)
- match step.condition with
- | Type _ -> Type p
- | Have _ -> Have p
- | When _ -> When p
- | Core _ -> Core p
- | Init _ -> Init p
- | _ -> assert false (* see above pattern matching *)
- in
- let rec collect p =
- match Lang.F.p_expr p with
- | And ps -> collect_list ps
- | _ -> [ p ]
- and collect_list = function
- | [] -> []
- | p :: l -> List.rev_append (List.rev @@ collect p) (collect_list l)
- in
- begin match step.condition with
- | Type p | Have p | When p | Core p | Init p ->
- let ps = Lang.F.e_props @@ collect p in
- if List.mem remove ps then
- let ps = List.filter (fun x -> x <> remove) ps in
- let cond = cond @@ Lang.F.p_bool @@ Lang.F.e_and ps in
- let filtered = [ "Filtered", cond ] in
- Applicable (Tactical.replace ~at:step.id filtered)
- else
- Not_applicable
-
- | _ -> Not_applicable
+ begin
+ try Applicable(process @@ tactical_inside step [remove])
+ with Not_found -> Not_applicable
end
+ | Multi es ->
+ Applicable (process @@ fold_selection es)
| _ -> Not_applicable
end
diff --git a/src/plugins/wp/TacCompound.ml b/src/plugins/wp/TacCompound.ml
index e4fe08b7833..53c984d681c 100644
--- a/src/plugins/wp/TacCompound.ml
+++ b/src/plugins/wp/TacCompound.ml
@@ -209,7 +209,7 @@ class compound =
| Clause (Step s) -> process_have feedback s
| Clause (Goal p) -> process_goal feedback p
| Inside(_,e) -> process_expand feedback ?at:(Tactical.at s) e
- | Empty | Compose _ -> raise Not_found
+ | Empty | Compose _ | Multi _ -> raise Not_found
in Applicable process
end
diff --git a/src/plugins/wp/TacNormalForm.ml b/src/plugins/wp/TacNormalForm.ml
index f7e78a43906..a3ca166d4d3 100644
--- a/src/plugins/wp/TacNormalForm.ml
+++ b/src/plugins/wp/TacNormalForm.ml
@@ -73,7 +73,7 @@ let match_selection = function
else Some (false, e, f_nf_hyp s e)
| _ -> None
end
- | Inside(_,_) | Compose _ | Empty -> None
+ | Inside(_,_) | Compose _ | Empty | Multi _ -> None
class normal_form =
object
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 1e20d4073b3..20857de0be0 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -187,7 +187,7 @@ class split =
split_cmp at "Split (<)" x y
in
match s with
- | Empty | Compose _ -> Not_applicable
+ | Empty | Compose _ | Multi _ -> Not_applicable
| Inside(_,e) ->
begin
let at = Tactical.at s in
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index fd4f9e3a3b9..e64bfec45f9 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -22,6 +22,7 @@
open Lang
open Tactical
+open Conditions
(* -------------------------------------------------------------------------- *)
(* --- Unfold Definition Tactical --- *)
@@ -48,6 +49,8 @@ let range f es =
(F.p_leq e (F.e_zint b)) in
F.e_prop (F.p_all range es)
+(* Used only for non Multi selection *)
+
let rec applicable ?at e f es = function
| phi::others ->
begin
@@ -61,6 +64,82 @@ let rec applicable ?at e f es = function
| [] ->
Not_applicable
+(* Used only for Multi selection *)
+
+module Smap = Qed.Idxmap.Make
+ (struct
+ type t = step
+ let id s = s.id
+ end)
+
+let condition original p = (* keep original kind of simple condition *)
+ match original.condition with
+ | Type _ -> Type p
+ | Have _ -> Have p
+ | When _ -> When p
+ | Core _ -> Core p
+ | Init _ -> Init p
+ | _ -> assert false
+
+let collect_term_to_unfold (g, m) = function
+ | Inside(Step step, unfold) ->
+ let l =
+ try Smap.find step m
+ with Not_found -> []
+ in
+ g, Smap.add step (unfold :: l) m
+ | Inside (Goal _, unfold) ->
+ begin match g with
+ | None -> Some [ unfold ], m
+ | Some g -> Some (unfold :: g), m
+ end
+ | _ -> raise Not_found
+
+let rec collect_unfold phis m e =
+ match phis with
+ | phi :: others ->
+ begin
+ try
+ match F.repr e with
+ | Qed.Logic.Fun(f,es) -> Lang.F.Tmap.add e (phi f es) m
+ | _ -> raise Not_found
+ with Not_found | Invalid_argument _ -> collect_unfold others m e
+ end
+ | [] -> m
+
+let unfolds_from_list phis es =
+ List.fold_left (collect_unfold phis) Lang.F.Tmap.empty es
+
+let unfolds_from_smap phis m =
+ Smap.map (fun _s es -> unfolds_from_list phis es) m
+
+let tactical_inside step unfolds sequent =
+ if Lang.F.Tmap.is_empty unfolds
+ then raise Not_found
+ else match step.condition with
+ | Type p | Have p | When p | Core p | Init p ->
+ let subst t = Lang.F.Tmap.find t unfolds in
+ let p = condition step @@ Lang.p_subst subst p in
+ snd @@ Tactical.replace_single ~at:step.id ("Unfolded", p) sequent
+ | _ -> raise Not_found
+
+let tactical_goal unfolds (seq, g) =
+ if Lang.F.Tmap.is_empty unfolds
+ then raise Not_found
+ else
+ let subst t = Lang.F.Tmap.find t unfolds in
+ seq, Lang.p_subst subst g
+
+let fold_selection goal_unfolds step_unfolds sequent =
+ "Unfolded multiple selection",
+ let add_goal = match goal_unfolds with
+ | None -> Extlib.id
+ | Some goal_unfolds -> tactical_goal goal_unfolds
+ in
+ add_goal @@ Smap.fold tactical_inside step_unfolds sequent
+
+let process (f: sequent -> string * sequent) s = [ f s ]
+
class unfold =
object
inherit Tactical.make ~id:"Wp.unfold"
@@ -69,13 +148,21 @@ class unfold =
~params:[]
method select _feedback (s : Tactical.selection) =
- let at = Tactical.at s in
- let e = Tactical.selected s in
- match F.repr e with
- | Qed.Logic.Fun(f,es) ->
- applicable ?at e f es [ definition ; range ]
- | _ -> Not_applicable
-
+ let unfoldings = [ definition ; range ] in
+ match s with
+ | Multi es ->
+ let goal, steps =
+ List.fold_left collect_term_to_unfold (None, Smap.empty) es in
+ let goal = Option.map (unfolds_from_list unfoldings) goal in
+ let steps = unfolds_from_smap unfoldings steps in
+ Applicable (process @@ fold_selection goal steps)
+ | s ->
+ let at = Tactical.at s in
+ let e = Tactical.selected s in
+ match F.repr e with
+ | Qed.Logic.Fun(f,es) ->
+ applicable ?at e f es unfoldings
+ | _ -> Not_applicable
end
let tactical = Tactical.export (new unfold)
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 5fcf6a7bc0a..1da597fa8d3 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -79,6 +79,7 @@ type selection =
| Clause of clause
| Inside of clause * term
| Compose of compose
+ | Multi of selection list
and compose =
| Cint of Integer.t
@@ -105,6 +106,7 @@ let selected = function
| Inside(_,t) -> t
| Clause c -> e_prop (head c)
| Compose code -> composed code
+ | Multi _s -> e_true (* For now, do not provide this *)
let get_int_z z =
try Some (Integer.to_int_exn z) with Z.Overflow -> None
@@ -148,6 +150,10 @@ let rec pp_selection fmt = function
Format.fprintf fmt "@[<hov 2>Compose '%s'" id ;
List.iter (fun e -> Format.fprintf fmt "(%a)" pp_selection e) es ;
Format.fprintf fmt "@]"
+ | Multi es ->
+ Format.fprintf fmt "@[<hov 2>Multi-selection" ;
+ List.iter (fun e -> Format.fprintf fmt "(%a)" pp_selection e) es ;
+ Format.fprintf fmt "@]"
let int a = Compose(Cint (Integer.of_int a))
let cint a = Compose(Cint a)
@@ -161,6 +167,8 @@ let compose id es =
| _ -> Compose(Code(e,id,es))
with Not_found -> Empty
+let multi es = Multi es
+
let findhead (s:selection) e =
match s with
| Empty -> None
@@ -172,6 +180,7 @@ let findhead (s:selection) e =
else None
| Compose(Code(v,_,_)) as s ->
if v == e then Some s else None
+ | Multi _ -> None
let rec lookup (s:selection) e q =
match findhead s e with
@@ -334,7 +343,7 @@ class type feedback =
(* -------------------------------------------------------------------------- *)
let at = function
- | Empty | Clause (Goal _) | Inside(Goal _,_) | Compose _ -> None
+ | Empty | Clause (Goal _) | Inside(Goal _,_) | Compose _ | Multi _ -> None
| Clause (Step s) | Inside(Step s,_) -> Some s.id
let mapi f cases =
@@ -357,6 +366,10 @@ let replace ~at cases sequent =
descr , Conditions.replace ~at step sequent)
cases
+let replace_single ~at (descr,cond) sequent =
+ let step = Conditions.(step ~descr cond) in
+ descr , Conditions.replace ~at step sequent
+
let replace_step ~at conditions sequent =
let step =
let s = Conditions.step_at (fst sequent) at in
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index 78159e588ce..f7ea9130bf0 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -41,6 +41,7 @@ type selection =
| Clause of clause
| Inside of clause * term
| Compose of compose
+ | Multi of selection list
and compose = private
| Cint of Integer.t
@@ -51,6 +52,7 @@ val int : int -> selection
val cint : Integer.t -> selection
val range : int -> int -> selection
val compose : string -> selection list -> selection
+val multi : selection list -> selection
val get_int : selection -> int option
val destruct : selection -> selection list
@@ -179,6 +181,7 @@ val at : selection -> int option
val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
val insert : ?at:int -> (string * pred) list -> process
val replace : at:int -> (string * condition) list -> process
+val replace_single : at:int -> string * condition -> sequent -> string * sequent
val replace_step : at:int -> condition list -> process
val split : (string * pred) list -> process
val rewrite : ?at:int -> (string * pred * term * term) list -> process
diff --git a/src/plugins/wp/tests/wp_tip/TacNOP.ml b/src/plugins/wp/tests/wp_tip/TacNOP.ml
index 7b2413cd0a6..a398efe3ac5 100644
--- a/src/plugins/wp/tests/wp_tip/TacNOP.ml
+++ b/src/plugins/wp/tests/wp_tip/TacNOP.ml
@@ -16,6 +16,7 @@ class nop =
match s with
| Empty -> Not_applicable
| Compose _
+ | Multi _
| Inside _
| Clause _ ->
feedback#set_title "NOP" ;
--
GitLab