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