[wp] goal printer debug

src/plugins/wp/GuiSequent.ml

@@ -341,7 +341,7 @@ class pcond
     (focus : step_selection)
     (plang : Pcond.state) =
   object(self)
-    inherit Pcond.sequence plang as super
+    inherit Pcond.seqengine plang as super
 
     (* All displayed entries *)
     val mutable domain = Vars.empty

src/plugins/wp/Pcond.ml

@@ -333,7 +333,7 @@ class engine (lang : #Plang.engine) =
 
 let is_nop = function None -> true | Some(_,upd) -> Bag.is_empty upd
 
-class sequence (lang : #state) =
+class seqengine (lang : #state) =
   object(self)
     inherit engine lang as super
 
@@ -440,7 +440,7 @@ class sequence (lang : #state) =
 
 let engine () =
   if Wp_parameters.has_dkey dkey_state then
-    ( new sequence (new state) :> engine )
+    ( new seqengine (new state) :> engine )
   else
     new engine (new Plang.engine)
 
@@ -449,15 +449,18 @@ let pretty fmt seq =
 
 let () = Conditions.pretty := pretty
 
-let sequence ?(clause="Sequence") fmt seq =
+let dump_sequence ?(clause="Sequence") ?goal fmt seq =
   let plang = new Plang.engine in
   let pcond = new engine plang in
   plang#global
-    (fun () ->
-       Vars.iter (fun x -> ignore (plang#bind x)) (Conditions.vars_hyp seq) ;
-       pcond#pp_sequence ~clause fmt seq)
+    begin fun () ->
+      pcond#pp_block ~clause fmt seq ;
+      match goal with
+      | None -> ()
+      | Some g -> Format.fprintf fmt "@ @[<hov 2>Prove %a@]" plang#pp_pred g
+    end
 
-let bundle ?clause fmt bundle =
-  sequence ?clause fmt (Conditions.bundle bundle)
+let dump_bundle ?clause ?goal fmt bundle =
+  dump_sequence ?clause ?goal fmt (Conditions.bundle bundle)
 
-let dump = bundle ~clause:"Bundle"
+let dump = dump_bundle ?goal:None ~clause:"Bundle"

src/plugins/wp/Pcond.mli

@@ -23,16 +23,18 @@
 open Qed.Plib
 open Conditions
 
+open Lang.F
+
 (** {2 All-in-one printers} *)
 
-val dump : bundle printer
-val bundle : ?clause:string -> bundle printer
-val sequence : ?clause:string -> sequence printer
 val pretty : sequent printer
 
+val dump : bundle printer
+val dump_bundle : ?clause:string -> ?goal:pred -> bundle printer
+val dump_sequence : ?clause:string -> ?goal:pred -> sequence printer
+
 (** {2 Low-level API} *)
 
-open Lang.F
 type env = Plang.Env.t
 
 val alloc_hyp : Plang.pool -> (var -> unit) -> sequence -> unit
@@ -103,7 +105,7 @@ class state :
     method pp_value : Format.formatter -> term -> unit
   end
 
-class sequence : #state ->
+class seqengine : #state ->
   object
     inherit engine
     method set_sequence : Conditions.sequence -> unit

src/plugins/wp/cfgDump.ml

@@ -121,6 +121,7 @@ struct
   let add_assigns env (pid,_) k =
     let u = node () in
     Format.fprintf !out "  %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+    Format.fprintf !out "  %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
     merge env u k
 
   let use_assigns _env _stmt region d k =
@@ -215,7 +216,9 @@ struct
             (fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
                 Printer.pp_predicate p) pre
       end ;
-    ignore pre ; merge env u k
+    ignore pre ;
+    Format.fprintf !out "  %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+    merge env u k
 
   let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
     let u_post = List.fold_right (add_hyp env) post p_post in

src/plugins/wp/cfgWP.ml

@@ -101,6 +101,10 @@ struct
   struct
     type t = effect
     let compare e1 e2 = P.compare e1.e_pid e2.e_pid
+    let pretty fmt e =
+      Format.fprintf fmt "@[<hov 2>EFFECT %a:@ %a@]"
+        P.pretty e.e_pid (Cvalues.pp_region M.pretty) e.e_region
+    [@@ warning "-32"]
   end
 
   module G = Qed.Collection.Make(TARGET)
@@ -140,9 +144,8 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   let pp_vc fmt vc =
-    Format.fprintf fmt "%a@ @[<hov 2>Prove %a@]"
-      Pcond.dump vc.hyps
-      F.pp_pred vc.goal
+    Format.fprintf fmt "%a"
+      (Pcond.dump_bundle ~clause:"Context" ~goal:vc.goal) vc.hyps
 
   let pp_vcs fmt vcs =
     let k = ref 0 in

src/plugins/wp/wpPropId.ml

@@ -230,7 +230,7 @@ let compare_prop_id pid1 pid2 =
     else
       Stdlib.compare pid1.p_part pid2.p_part
 
-module PropId =
+module PropIdRaw =
   Datatype.Make_with_collections(
   struct
     type t = prop_id
@@ -356,7 +356,7 @@ end = struct
     in normalize_basename basename
 
 
-  module UniquifyPropId = NameUniquify(PropId)(struct
+  module UniquifyPropId = NameUniquify(PropIdRaw)(struct
       let name = "WpProperty"
       let basename = get_prop_id_basename
     end)
@@ -435,7 +435,7 @@ struct
         if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
           Printf.sprintf "%s_part%06d" basename (succ k)
 
-  module Uniquify2 = NameUniquify(PropId)(struct
+  module Uniquify2 = NameUniquify(PropIdRaw)(struct
       let name = "Wp.WpPropId.Names2."
       let basename = get_prop_id_basename
     end)
@@ -573,6 +573,16 @@ end
 
 let pretty_local = Pretty.pp_local
 
+(* -------------------------------------------------------------------------- *)
+(* --- Datatype                                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+module PropId =
+struct
+  include PropIdRaw
+  let pretty = pp_propid
+end
+
 (* -------------------------------------------------------------------------- *)
 (* --- Hints                                                              --- *)
 (* -------------------------------------------------------------------------- *)