diff options
Diffstat (limited to 'contrib/xml/dumptree.ml4')
| -rw-r--r-- | contrib/xml/dumptree.ml4 | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/contrib/xml/dumptree.ml4 b/contrib/xml/dumptree.ml4 new file mode 100644 index 00000000..407f86b3 --- /dev/null +++ b/contrib/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_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 |