added some code to print the praamodulation proofs with a graph

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1bc87f8c54fd6e235b903a405e6422b7486ba62e..fcb4586cb4d8b2e0ecb2e1831797f11a2ef49605 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -1234,3 +1234,104 @@ let pp_proofterm t =
   pp_proofterm (Some (Cic.Name "Hypothesis")) t []
 ;;
 
+let initial_nameset_list = [
+ "x"; "y"; "z"; "t"; "u"; "v"; "a"; "b"; "c"; "d"; 
+ "e"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; 
+]
+
+module S = Set.Make(String)
+
+let initial_nameset = List.fold_right S.add initial_nameset_list S.empty, [];;
+
+let freshname (nameset, subst) term = 
+  let m = CicUtil.metas_of_term term in
+  let nameset, subst = 
+    List.fold_left 
+      (fun (set,rc) (m,_) -> 
+        if List.mem_assoc m rc then set,rc else
+        let name = S.choose set in
+        let set = S.remove name set in
+        set, 
+        (m,Cic.Const(UriManager.uri_of_string 
+             ("cic:/"^name^".con"),[]))::rc)
+      (nameset,subst) m
+  in
+  let term = 
+   ProofEngineReduction.replace
+    ~equality:(fun i t -> match t with Cic.Meta (j,_) -> i=j| _ -> false) 
+    ~what:(List.map fst subst) 
+    ~with_what:(List.map snd subst) ~where:term
+  in
+  (nameset, subst), term
+;;
+
+let remove_names_in_context (set,subst) names =
+  List.fold_left
+    (fun s n -> 
+      match n with Some (Cic.Name n) -> S.remove n s | _ -> s) 
+    set names, subst
+;;
+
+let string_of_id2 (id_to_eq,_) names nameset id = 
+  if id = 0 then "" else 
+  try
+    let (_,_,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let nameset, l = freshname nameset l in
+    let nameset, r = freshname nameset r in
+    Printf.sprintf "%s = %s" (CicPp.pp l names) (CicPp.pp r names)
+  with
+      Not_found -> assert false
+;;
+
+let draw_proof bag names goal_proof proof id =
+  let b = Buffer.create 100 in
+  let fmt = Format.formatter_of_buffer b in 
+  let sint = string_of_int in
+  let fst3 (x,_,_) = x in
+  let visited = ref [] in
+  let nameset = remove_names_in_context initial_nameset names in
+  let rec fact id = function
+    | Exact t -> 
+        if not (List.mem id !visited) then
+          begin
+          visited := id :: !visited;
+          let nameset, t = freshname nameset t in
+          let t = CicPp.pp t names in
+          GraphvizPp.Dot.node (sint id) 
+          ~attrs:["label",t^":"^string_of_id2 bag names nameset id;
+          "shape","rectangle"] fmt;
+          end
+    | Step (_,(_,id1,(_,id2),_)) ->
+        GraphvizPp.Dot.edge (sint id) (sint id1) fmt;
+        GraphvizPp.Dot.edge (sint id) (sint id2) fmt;
+        let p1,_,_ = proof_of_id bag id1 in
+        let p2,_,_ = proof_of_id bag id2 in
+        fact id1 p1;
+        fact id2 p2;
+        if not (List.mem id !visited); then
+          begin
+          visited := id :: !visited;
+          GraphvizPp.Dot.node (sint id) 
+          ~attrs:["label",sint id^":"^string_of_id2 bag names nameset id;
+                  "shape","ellipse"] fmt
+          end
+  in
+  let sleft acc (_,_,id,_,_) =
+    if acc != 0 then GraphvizPp.Dot.edge (sint acc) (sint id) fmt;
+    fact id (fst3 (proof_of_id bag id));
+    id
+  in
+  GraphvizPp.Dot.header ~node_attrs:["fontsize","10"; ] fmt;
+  ignore(List.fold_left sleft id goal_proof);
+  GraphvizPp.Dot.trailer fmt;
+  let oc = open_out "/tmp/matita_paramod.dot" in
+  Buffer.output_buffer oc b;
+  close_out oc;
+  prerr_endline "dot!";
+  ignore(Unix.system 
+    "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot"
+(* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *)
+  );
+  ignore(Unix.system "gv /tmp/matita_paramod.eps");
+;;
+

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 3bc9e4309c4d5ecd8302f74b1aea773bb48b2d47..a8dec96f937ce74835bf6a1a5e027808b18ec117 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -46,6 +46,10 @@ val pp_proof:
   (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
     Cic.term -> string
 
+val draw_proof:
+  equality_bag ->
+  (Cic.name option) list -> goal_proof -> proof -> int -> unit
+
 val pp_proofterm: Cic.term -> string
     
 val mk_equality :

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 30561bf07b5df933fecb0da1e3efef1be1539207..ff58512ea9d1f47c429d6f0f6b412fc5c96b4165 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1343,6 +1343,7 @@ let build_proof
         eq_uri goalproof initial type_of_goal side_effects
         context proof_menv  
   in
+(*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
   let real_menv =  fix_metasenv (proof_menv@metasenv) in
   let real_menv,goal_proof =