Commit 0f5f1acf authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] provides global pool in tactical environment

parent 9d26bad8
......@@ -357,13 +357,13 @@ class pane (proverpane : GuiConfig.provers) =
printer#set_target Tactical.Empty ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
| Some(model,sequent,sel) ->
| Some(model,tree,sequent,sel) ->
strategies#connect (Some (self#strategies sequent)) ;
let select (tactic : GuiTactic.tactic) =
let process = self#apply in
let composer = self#compose in
let browser = self#browse in
tactic#select ~process ~composer ~browser sel
tactic#select ~process ~composer ~browser ~tree sel
in
Model.with_model model (List.iter select) tactics ;
let tgt =
......@@ -470,7 +470,7 @@ class pane (proverpane : GuiConfig.provers) =
let sequent = printer#sequent in
let select = printer#selection in
let model = wpo.Wpo.po_model in
self#update_tactics (Some(model,sequent,select)) ;
self#update_tactics (Some(model,proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
......
......@@ -340,6 +340,7 @@ let wfield tac form pp = function
(* -------------------------------------------------------------------------- *)
type edited = {
tree : ProofEngine.tree ;
target : selection ;
browser : (browser -> unit) ;
composer : (composer -> unit) ;
......@@ -388,6 +389,10 @@ class tactic
(* --- Feedback API --- *)
(* -------------------------------------------------------------------------- *)
method pool = match edited with
| None -> assert false
| Some { tree } -> ProofEngine.pool tree
method interactive = self#is_active
method get_title = title
method has_error = error
......@@ -437,8 +442,8 @@ class tactic
method private updated () =
match edited with
| None -> ()
| Some { process ; composer ; browser ; target } ->
self#select ~process ~composer ~browser target
| Some { process ; composer ; browser ; target ; tree } ->
self#select ~process ~composer ~browser ~tree target
method clear =
begin
......@@ -455,9 +460,11 @@ class tactic
try tac#select (self :> feedback) target
with Not_found | Exit -> Not_applicable
method select ~process ~browser ~composer (target : selection) =
method select ~process ~browser ~composer ~tree
(target : selection) =
begin
self#reset_dongle ;
edited <- Some { process ; composer ; browser ; target ; tree } ;
let status = self#status target in
match status , error with
| Not_applicable , _ ->
......@@ -466,12 +473,10 @@ class tactic
self#set_action () ;
| Not_configured , _ | Applicable _ , true ->
self#set_visible true ;
edited <- Some { process ; composer ; browser ; target } ;
self#set_status `DIALOG_WARNING ;
self#set_action () ;
| Applicable proc , false ->
self#set_visible true ;
edited <- Some { process ; composer ; browser ; target } ;
self#set_status `APPLY ;
let callback () = process tac target proc in
self#set_action ~callback () ;
......
......@@ -64,6 +64,7 @@ class tactic : Tactical.t -> (Format.formatter -> Tactical.selection -> unit) ->
process:(tactical -> selection -> process -> unit) ->
browser:(browser -> unit) ->
composer:(composer -> unit) ->
tree:ProofEngine.tree ->
selection -> unit
end
......
......@@ -40,6 +40,7 @@ and script =
type tree = {
main : Wpo.t ; (* Main goal to be proved. *)
mutable pool : Lang.F.pool option ; (* Global pool variable *)
mutable saved : bool ; (* Saved on Disk. *)
mutable gid : int ; (* WPO goal numbering *)
mutable head : node option ; (* the current node *)
......@@ -53,6 +54,7 @@ module PROOFS = Model.StaticGenerator(Wpo.S)
let name = "Wp.ProofEngine.Proofs"
let compile main = {
main ; gid = 0 ;
pool = None ;
head = None ;
root = None ;
saved = false ;
......@@ -73,6 +75,14 @@ let get wpo =
let iter_all f ns = List.iter (fun (_,n) -> f n) ns
let map_all f ns = List.map (fun (k,n) -> k,f n) ns
let pool tree =
match tree.pool with
| Some pool -> pool
| None ->
let _,sequent = Wpo.compute tree.main in
let pool = Lang.new_pool ~vars:(Conditions.vars_seq sequent) () in
tree.pool <- Some pool ; pool
(* -------------------------------------------------------------------------- *)
(* --- Constructors --- *)
(* -------------------------------------------------------------------------- *)
......
......@@ -40,6 +40,7 @@ type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
type current = [ `Main | `Internal of node | `Leaf of int * node ]
type position = [ `Main | `Node of node | `Leaf of int ]
val pool : tree -> Lang.F.pool
val saved : tree -> bool
val set_saved : tree -> bool -> unit
......
......@@ -429,11 +429,12 @@ let configure jtactic sequent =
(* --- Console --- *)
(* -------------------------------------------------------------------------- *)
class console ~title =
class console ~pool ~title =
object
val mutable the_title = title
method pool : Lang.F.pool = pool
method interactive = false
method get_title = the_title
method set_title : 'a. 'a formatter =
......
......@@ -23,7 +23,7 @@
open Tactical
open Conditions
class console : title:string -> Tactical.feedback
class console : pool:Lang.F.pool -> title:string -> Tactical.feedback
type jscript = alternative list
and alternative = private
......
......@@ -78,7 +78,9 @@ let jconfigure (console : #Tactical.feedback) jtactic goal =
end
let jfork tree ?node jtactic =
let console = new ProofScript.console ~title:jtactic.header in
let console = new ProofScript.console
~pool:(ProofEngine.pool tree)
~title:jtactic.header in
try
let anchor = ProofEngine.anchor tree ?node () in
let goal = ProofEngine.goal anchor in
......
......@@ -40,7 +40,9 @@ let configure (console : #Tactical.feedback) strategy =
| _ -> None
let fork tree anchor strategy =
let console = new ProofScript.console ~title:strategy.tactical#title in
let console = new ProofScript.console
~pool:(ProofEngine.pool tree)
~title:strategy.tactical#title in
try
let model = ProofEngine.node_model anchor in
match Model.with_model model (configure console) strategy with
......
......@@ -316,6 +316,7 @@ type 'a formatter = ('a,Format.formatter,unit) format -> 'a
class type feedback =
object
method pool : pool
method interactive : bool
method get_title : string
method has_error : bool
......
......@@ -142,6 +142,9 @@ type 'a formatter = ('a,Format.formatter,unit) format -> 'a
class type feedback =
object
(** Global fresh variable pool *)
method pool : pool
(** Interactive mode.
If [false] the GUI is not activated.
Hence, detailed feedback is not reported to the user. *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment