1 files changed, 152 insertions, 0 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
new file mode 100644
index 00000000..9419ba59
--- /dev/null
+++ b/plugins/xml/dumptree.ml4
@@ -0,0 +1,152 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module provides the "Dump Tree" command that allows dumping the
+    current state of the proof stree in XML format *)
+
+(** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+open Tacexpr;;
+open Decl_mode;;
+open Printer;;
+open Pp;;
+open Environ;;
+open Format;;
+open Proof_type;;
+open Evd;;
+open Termops;;
+open Ppconstr;;
+open Names;;
+
+exception Different
+
+let xmlstream s =
+  (* In XML we want to print the whole stream so we can force the evaluation *)
+  Stream.of_list (List.map xmlescape (Stream.npeek max_int s))
+;;
+
+let thin_sign osign sign =
+  Sign.fold_named_context
+    (fun (id,c,ty as d) sign ->
+       try
+        if Sign.lookup_named id osign = (id,c,ty) then sign
+         else raise Different
+       with Not_found | Different -> Environ.push_named_context_val d sign)
+    sign ~init:Environ.empty_named_context_val
+;;
+
+let pr_tactic_xml = function
+  | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
+  | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>"
+;;
+
+let pr_proof_instr_xml instr =
+  Ppdecl_proof.pr_proof_instr (Global.env()) instr
+;;
+
+let pr_rule_xml pr = function
+  | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>"
+  | Nested(cmpd, subtree) ->
+      hov 2 (str "<cmpdrule>" ++ fnl () ++
+        begin match cmpd with
+          Tactic (texp, _) -> pr_tactic_xml texp
+        | Proof_instr (_,instr) -> pr_proof_instr_xml instr
+        end ++ fnl ()
+        ++ pr subtree
+      ) ++ fnl () ++ str "</cmpdrule>"
+  | Daimon -> str "<daimon/>"
+  | Decl_proof _ -> str "<proof/>"
+(*  | Change_evars -> str "<chgevars/>"*)
+;;
+
+let pr_var_decl_xml env (id,c,typ) =
+  let ptyp = print_constr_env env typ in
+  match c with
+  | None ->
+      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>")
+  | Some c ->
+      (* Force evaluation *)
+      let pb = print_constr_env env c in
+      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++
+         xmlstream pb ++ str "\"/>")
+;;
+
+let pr_rel_decl_xml env (na,c,typ) =
+  let pbody = match c with
+    | None -> mt ()
+    | Some c ->
+	(* Force evaluation *)
+	let pb = print_constr_env env c in
+	  (str" body=\"" ++ xmlstream pb ++ str "\"") in
+  let ptyp = print_constr_env env typ in
+  let pid =
+    match na with
+    | Anonymous -> mt ()
+    | Name id -> str " id=\"" ++ pr_id id ++ str "\""
+  in
+  (str "<hyp" ++ pid ++ str " type=\"" ++ xmlstream ptyp ++ str "\"" ++ pbody ++ str "/>")
+;;
+
+let pr_context_xml env =
+  let sign_env =
+    fold_named_context
+      (fun env d pp -> pp ++ pr_var_decl_xml env d)
+      env ~init:(mt ())
+  in
+  let db_env =
+    fold_rel_context
+      (fun env d pp -> pp ++ pr_rel_decl_xml env d)
+      env ~init:(mt ())
+  in
+  (sign_env ++ db_env)
+;;
+
+let pr_subgoal_metas_xml metas env=
+  let pr_one (meta, typ) =
+    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++
+      str "\"/>"
+  in
+  List.fold_left (++) (mt ()) (List.map pr_one metas)
+;;
+
+let pr_goal_xml g =
+  let env = try evar_unfiltered_env g with _ -> empty_env in
+  if g.evar_extra = None then
+    (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
+    xmlstream (pr_ltype_env_at_top env g.evar_concl) ++
+    str "\"/>" ++
+    (pr_context_xml env)) ++
+    fnl () ++ str "</goal>")
+  else
+    (hov 2 (str "<goal type=\"declarative\">" ++
+    (pr_context_xml env)) ++
+    fnl () ++ str "</goal>")
+;;
+
+let rec print_proof_xml sigma osign pf =
+  let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
+  let hyps' = thin_sign osign hyps in
+  match pf.ref with
+    | None -> hov 2 (str "<tree>" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "</tree>"
+    | Some(r,spfl) ->
+        hov 2 (str "<tree>" ++ fnl () ++
+        (pr_goal_xml {pf.goal with evar_hyps=hyps'}) ++ fnl () ++ (pr_rule_xml (print_proof_xml sigma osign) r) ++
+        (List.fold_left (fun x y -> x ++ fnl () ++ y) (mt ()) (List.map (print_proof_xml sigma hyps) spfl))) ++ fnl () ++ str "</tree>"
+;;
+
+let print_proof_xml () =
+  let pp = print_proof_xml Evd.empty Sign.empty_named_context
+      (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ())))
+  in
+  msgnl pp
+;;
+
+VERNAC COMMAND EXTEND DumpTree
+  [ "Dump" "Tree" ] -> [ print_proof_xml () ]
+END