From c42b59d779785f32f3270ac8284af413fa4432a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 13 Jul 2016 08:30:50 +0200
Subject: [PATCH] [WP/Tactical] make env available to composer
---
src/plugins/wp/GuiGoal.ml | 73 +++++++++++++++++++----
src/plugins/wp/GuiSequent.ml | 48 +++++++++++----
src/plugins/wp/GuiSequent.mli | 11 +++-
src/plugins/wp/GuiTactic.ml | 10 +++-
src/plugins/wp/Pcond.ml | 17 +++---
src/plugins/wp/qed/src/engine.mli | 1 +
src/plugins/wp/qed/src/export.ml | 3 +-
src/plugins/wp/qed/src/export.mli | 2 +
src/plugins/wp/qed/src/export_whycore.mli | 1 +
9 files changed, 129 insertions(+), 37 deletions(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index d7b4583f70f..c5868a2574a 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -24,7 +24,11 @@ type state =
| Empty
| Proof of ProofEngine.tree
| Forking of ProofEngine.tree * ProofEngine.fork * Task.pool
- | Composer of ProofEngine.tree * GuiTactic.composer
+ | Composer of ProofEngine.tree * GuiTactic.composer * GuiSequent.target
+
+(* -------------------------------------------------------------------------- *)
+(* --- Autofocus Management --- *)
+(* -------------------------------------------------------------------------- *)
type mode = [ `Refresh | `Autofocus | `ViewModel | `ViewAll | `ViewRaw ]
@@ -56,12 +60,55 @@ class autofocus =
end
end
+(* -------------------------------------------------------------------------- *)
+(* --- Composer Panel --- *)
+(* -------------------------------------------------------------------------- *)
+
+class composer (focused : GuiSequent.focused) =
+ object
+
+ val mutable stack = []
+ val mutable update = (fun () -> ())
+
+ method clear = stack <- [ ]
+
+ method connect f = update <- f
+
+ method print (cc : GuiTactic.composer) ~quit fmt =
+ begin
+ let selection = focused#selection in
+ let candidate = match selection with
+ | Tactical.Empty -> cc#get_value
+ | _ -> selection in
+ focused#set_target cc#target ;
+ Format.fprintf fmt "Composer for '%s': %a@."
+ cc#title focused#pp_selection candidate ;
+ Array.iteri
+ (fun i s ->
+ let c = char_of_int (int_of_char 'A' + i) in
+ Format.fprintf fmt "%c: %a@." c focused#pp_selection s
+ ) (Array.of_list stack) ;
+ let select () = cc#set_value selection ; quit () in
+ let clear () = cc#set_value Tactical.Empty ; quit () in
+ focused#button ~title:"Select" ~callback:select fmt ;
+ focused#button ~title:"Clear" ~callback:clear fmt ;
+ focused#button ~title:"Cancel" ~callback:quit fmt ;
+ Format.pp_print_newline fmt () ;
+ end
+
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Goal Panel --- *)
+(* -------------------------------------------------------------------------- *)
+
class pane (proverpane : GuiConfig.provers) =
let icon = new Widget.image GuiProver.no_status in
let status = new Widget.label () in
let text = new Wtext.text () in
let scripter = new GuiProof.printer text in
let printer = new GuiSequent.focused text in
+ let composer = new composer printer in
let layout = new Wutil.layout in
let palette = new Wpalette.panel () in
let delete = new Widget.button
@@ -119,6 +166,7 @@ class pane (proverpane : GuiConfig.provers) =
save_script#connect (fun () -> self#save_script) ;
play_script#connect (fun () -> self#play_script) ;
autofocus#connect self#autofocus ;
+ composer#connect (fun () -> self#update) ;
end
(* ---------------------------------------------------------------------- *)
@@ -128,14 +176,15 @@ class pane (proverpane : GuiConfig.provers) =
method private compose composer =
match state with
| Proof proof ->
- state <- Composer(proof,composer) ;
+ let tgt = printer#unselect in
+ state <- Composer(proof,composer,tgt) ;
self#update
| _ -> ()
method private interrupt cancel =
match state with
| Empty -> ()
- | Proof proof | Composer(proof,_) ->
+ | Proof proof | Composer(proof,_,_) ->
cancel proof ;
printer#reset ;
self#update
@@ -309,7 +358,7 @@ class pane (proverpane : GuiConfig.provers) =
save_script#set_enabled false ;
play_script#set_enabled false ;
end
- | Proof proof | Composer(proof,_) ->
+ | Proof proof | Composer(proof,_,_) ->
begin
let main = ProofEngine.main proof in
let play = ProofSession.exists main in
@@ -330,7 +379,7 @@ class pane (proverpane : GuiConfig.provers) =
forward#set_enabled false ;
status#set_text "No Status" ;
end
- | Proof proof | Forking(proof,_,_) | Composer(proof,_) ->
+ | Proof proof | Forking(proof,_,_) | Composer(proof,_,_) ->
begin
delete#set_enabled true ;
match ProofEngine.status proof with
@@ -406,17 +455,21 @@ class pane (proverpane : GuiConfig.provers) =
text#clear ;
scripter#tree proof ;
text#hrule ;
- text#printf "%a@." printer#pp_goal (ProofEngine.head proof) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
text#hrule ;
scripter#status proof ;
end
- | Composer(proof,composer) ->
+ | Composer(proof,cc,tgt) ->
begin
text#clear ;
- text#printf "Composer" ;
+ let quit () =
+ state <- Proof proof ;
+ printer#restore tgt ;
+ self#update in
+ text#printf "%t@."
+ (printer#goal (ProofEngine.head proof)) ;
text#hrule ;
- printer#set_target composer#target ;
- text#printf "%a@." printer#pp_goal (ProofEngine.head proof) ;
+ text#printf "%t@." (composer#print cc ~quit) ;
end
| Forking _ -> ()
diff --git a/src/plugins/wp/GuiSequent.ml b/src/plugins/wp/GuiSequent.ml
index 053351af452..53b85f53fc9 100644
--- a/src/plugins/wp/GuiSequent.ml
+++ b/src/plugins/wp/GuiSequent.ml
@@ -279,12 +279,6 @@ class plang
method! pp_var fmt x = Format.fprintf fmt "@{<wp:var>%s@}" x
method! pp_flow fmt e = self#wrap super#pp_flow fmt e
method! pp_atom fmt e = self#wrap super#pp_atom fmt e
- method pp_env env fmt e =
- self#scope env
- (fun () ->
- if F.is_prop e
- then self#pp_prop fmt e
- else self#pp_term fmt e)
end
(* -------------------------------------------------------------------------- *)
@@ -377,10 +371,13 @@ class pcond
(* --- Printer --- *)
(* -------------------------------------------------------------------------- *)
+type target = part * F.term option
+
class focused (wtext : Wtext.text) =
let parts : part Wtext.marker = wtext#marker in
let terms : term Wtext.marker = wtext#marker in
let focus : term Wtext.marker = wtext#marker in
+ let button : (unit -> unit) Wtext.marker = wtext#marker in
let target_term : term Wtext.marker = wtext#marker in
let target_part : part Wtext.marker = wtext#marker in
let autofocus = new autofocus in
@@ -411,6 +408,9 @@ class focused (wtext : Wtext.text) =
terms#set_hover [`BACKGROUND "lightblue"] ;
parts#set_hover [`BACKGROUND "lightgreen"] ;
focus#set_style [`BACKGROUND "wheat"] ;
+ button#set_style [`BACKGROUND "grey" ];
+ button#set_hover [`BACKGROUND "orange" ];
+ button#on_click (fun (_,_,cb) -> cb ()) ;
target_part#set_style [`BACKGROUND "orange"] ;
target_term#set_style [`BACKGROUND "orange"] ;
parts#on_click self#on_part ;
@@ -503,6 +503,19 @@ class focused (wtext : Wtext.text) =
| Goal , Some t -> inside Tactical.(Goal (snd sequent)) t
| Step s , Some t -> inside Tactical.(Step s) t
+ method unselect =
+ begin
+ let p = selected_part in selected_part <- Term ;
+ let t = selected_term in selected_term <- None ;
+ p,t
+ end
+
+ method restore (p,t) =
+ begin
+ selected_part <- p ;
+ selected_term <- t ;
+ end
+
method set_target = function
| Tactical.Empty ->
pcond#set_target Term ; plang#clear_target
@@ -553,9 +566,14 @@ class focused (wtext : Wtext.text) =
self#popup ;
end
- method pp_term fmt e = plang#pp_env autofocus#env fmt e
- method pp_pred fmt p = plang#pp_env autofocus#env fmt (F.e_prop p)
- method pp_sequent fmt s =
+ method pp_term fmt e = plang#pp_sort fmt e
+ method pp_pred fmt p = plang#pp_pred fmt p
+
+ method pp_selection fmt = function
+ | Tactical.Empty -> Format.fprintf fmt " - "
+ | sel -> self#pp_term fmt (Tactical.selected sel)
+
+ method sequent s fmt =
sequent <- s ;
if autofocus#set_sequent s then
begin
@@ -563,18 +581,22 @@ class focused (wtext : Wtext.text) =
selected_part <- Term ;
end ;
pcond#pp_esequent autofocus#env fmt s
-
- method pp_goal fmt w =
+
+ method goal w fmt =
let open Wpo in
match w.po_formula with
| GoalCheck _ -> Wpo.pp_goal fmt w
| GoalLemma { VC_Lemma.lemma = { Definitions.l_lemma = p } } ->
let sequent = Conditions.lemma p in
Format.fprintf fmt "@\n@{<wp:clause>Lemma@} %a:@\n" Wpo.pp_title w ;
- self#pp_sequent fmt sequent
+ self#sequent sequent fmt
| GoalAnnot { VC_Annot.goal = goal } ->
let sequent = GOAL.compute_descr goal in
Format.fprintf fmt "@\n@{<wp:clause>Goal@} %a:@\n" Wpo.pp_title w ;
- self#pp_sequent fmt sequent
+ self#sequent sequent fmt
+ method button ~title ~callback fmt =
+ Format.fprintf fmt "[ %a ]"
+ (button#mark callback Format.pp_print_string) title
+
end
diff --git a/src/plugins/wp/GuiSequent.mli b/src/plugins/wp/GuiSequent.mli
index 8d33a22436d..f7a66f9710f 100644
--- a/src/plugins/wp/GuiSequent.mli
+++ b/src/plugins/wp/GuiSequent.mli
@@ -28,6 +28,8 @@ type 'a printer = 'a Qed.Plib.printer
(* --- Sequent Pretty-Printer --- *)
(* -------------------------------------------------------------------------- *)
+type target
+
class focused : Wtext.text ->
object
method reset : unit
@@ -37,6 +39,8 @@ class focused : Wtext.text ->
method set_state_mode : bool -> unit
method selected : unit
+ method unselect : target
+ method restore : target -> unit
method on_selection : (unit -> unit) -> unit
method selection : Tactical.selection
@@ -47,6 +51,9 @@ class focused : Wtext.text ->
method pp_term : term printer
method pp_pred : pred printer
- method pp_goal : Wpo.t printer
- method pp_sequent : Conditions.sequent printer
+ method pp_selection : Tactical.selection printer
+ method goal : Wpo.t -> Format.formatter -> unit
+ method sequent : Conditions.sequent -> Format.formatter -> unit
+ method button : title:string -> callback:(unit -> unit) ->
+ Format.formatter -> unit
end
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 43d124e9fe6..92c641f153d 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -43,6 +43,7 @@ class type wfield =
object
method field : wfield
method reset : unit
+ method select : selection -> unit
method connect : (unit -> unit) -> unit
method compose : (composer -> unit) -> unit
method update :
@@ -62,6 +63,7 @@ class checkbox
method field = (self :> wfield)
method reset = button#set s.value
method connect = button#on_event
+ method select (_ : selection) = ()
method compose (_ : composer -> unit) = ()
method update ?enabled ?title ?tooltip id =
if id = Tactical.ident field then
@@ -90,6 +92,7 @@ class spinner
method field = (self :> wfield)
method reset = spin#set s.value
method connect = spin#on_event
+ method select (_ : selection) = ()
method compose (_ : composer -> unit) = ()
method update ?enabled ?title ?tooltip id =
if id = Tactical.ident field then
@@ -104,9 +107,9 @@ class mkcomposer
(tac : Tactical.t) (form : Wpane.form) (field : selection field)
(pp : Format.formatter -> Lang.F.term -> unit) =
let s = Tactical.signature field in
- let head = new Widget.label ~style:`Label ~align:`Right () in
+ let head = new Widget.label ~style:`Label ~align:`Left () in
let edit = new Widget.button ~icon:`EDIT ~tooltip:s.descr () in
- let hbox = Wbox.(hbox [ f head ; w edit ]) in
+ let hbox = Wbox.(hbox [ f head ; w ~padding:8 edit ]) in
object(self)
initializer
begin
@@ -137,6 +140,7 @@ class mkcomposer
method field = (self :> wfield)
method reset = ()
method connect f = demon <- demon @ [f]
+ method select tgt = target <- tgt
method compose f = edit#connect (fun () -> f self#composer)
method update ?enabled ?title ?tooltip id =
if id = Tactical.ident field then
@@ -169,6 +173,7 @@ class ['a] selector
method field = (self :> wfield)
method reset = combo#set default
method connect = combo#on_event
+ method select (_ : selection) = ()
method compose (_ : composer -> unit) = ()
method update ?enabled ?title ?tooltip id =
if id = Tactical.ident field then
@@ -283,6 +288,7 @@ class tactic (tac : tactical) (pp : Format.formatter -> Lang.F.term -> unit) =
method select ~process ~compose (sel : selection) =
begin
self#reset_dongle ;
+ List.iter (fun fd -> fd#select sel) fields ;
let status =
try tac#select (self :> feedback) sel
with Not_found | Exit -> Not_applicable
diff --git a/src/plugins/wp/Pcond.ml b/src/plugins/wp/Pcond.ml
index 1a00f4dd70f..7d023370b9e 100644
--- a/src/plugins/wp/Pcond.ml
+++ b/src/plugins/wp/Pcond.ml
@@ -272,15 +272,13 @@ class engine (lang : #Plang.engine) =
Conditions.iter (self#mark marks) hs ;
Format.fprintf fmt "@[<hv 0>" ;
List.iter (append (self#define env) fmt) (F.defs marks) ;
- lang#scope env
- begin fun () ->
- if not (Conditions.is_empty hs) then
- begin
- self#pp_block ~clause:"Assume" fmt hs ;
- Format.pp_print_newline fmt () ;
- end ;
- self#pp_goal fmt goal ;
+ lang#set_env env ;
+ if not (Conditions.is_empty hs) then
+ begin
+ self#pp_block ~clause:"Assume" fmt hs ;
+ Format.pp_print_newline fmt () ;
end ;
+ self#pp_goal fmt goal ;
Format.fprintf fmt "@]@."
method pp_goal fmt goal =
@@ -294,7 +292,8 @@ class engine (lang : #Plang.engine) =
lang#global (self#dump fmt seq)
method pp_esequent env fmt seq =
- lang#scope env (self#dump fmt seq)
+ lang#set_env env ;
+ self#dump fmt seq ()
(* --- Scope Management --- *)
diff --git a/src/plugins/wp/qed/src/engine.mli b/src/plugins/wp/qed/src/engine.mli
index 1b28c351e7c..460870f40be 100644
--- a/src/plugins/wp/qed/src/engine.mli
+++ b/src/plugins/wp/qed/src/engine.mli
@@ -112,6 +112,7 @@ class type virtual ['z,'adt,'field,'logic,'tau,'var,'term,'env] engine =
(** {3 Global and Local Environment} *)
method env : 'env (** Returns a fresh copy of the current environment. *)
+ method set_env : 'env -> unit (** Set environment. *)
method lookup : 'term -> scope (** Term scope in the current environment. *)
method scope : 'env -> (unit -> unit) -> unit
(** Calls the continuation in the provided environment.
diff --git a/src/plugins/wp/qed/src/export.ml b/src/plugins/wp/qed/src/export.ml
index d46b5b28585..55ff0ed335d 100644
--- a/src/plugins/wp/qed/src/export.ml
+++ b/src/plugins/wp/qed/src/export.ml
@@ -267,6 +267,7 @@ struct
method lookup t : scope = Env.lookup alloc t
method env = copy_alloc alloc
+ method set_env env = alloc <- env
method marks =
let env = alloc (* NOT a fresh copy *) in
let shared = Env.shared env in
@@ -274,7 +275,7 @@ struct
let subterms = self#subterms in
let marks = T.marks ~shared ~shareable ~subterms () in
env , marks
-
+
method scope env (job : unit -> unit) =
let stack = alloc in
alloc <- env ;
diff --git a/src/plugins/wp/qed/src/export.mli b/src/plugins/wp/qed/src/export.mli
index 9264bd3c348..def7c488a03 100644
--- a/src/plugins/wp/qed/src/export.mli
+++ b/src/plugins/wp/qed/src/export.mli
@@ -63,8 +63,10 @@ sig
method virtual link : Fun.t -> link
method env : Env.t (** A safe copy of the environment *)
+ method set_env : Env.t -> unit (** Set the environment *)
method marks : Env.t * T.marks (** The current environment with empty marks *)
method lookup : term -> scope
+ method set_env : Env.t -> unit
method scope : Env.t -> (unit -> unit) -> unit
method local : (unit -> unit) -> unit
method global : (unit -> unit) -> unit
diff --git a/src/plugins/wp/qed/src/export_whycore.mli b/src/plugins/wp/qed/src/export_whycore.mli
index c2a52087463..d55e068c0b2 100644
--- a/src/plugins/wp/qed/src/export_whycore.mli
+++ b/src/plugins/wp/qed/src/export_whycore.mli
@@ -48,6 +48,7 @@ sig
method virtual link : Fun.t -> link
method env : Env.t
+ method set_env : Env.t -> unit
method marks : Env.t * T.marks
method lookup : t -> scope
method scope : Env.t -> (unit -> unit) -> unit
--
GitLab