1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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: "grammar/grammar.cma" i*)
open Tacexpr;;
open Printer;;
open Pp;;
open Environ;;
open Proof_type;;
open Termops;;
open Ppconstr;;
open Names;;
exception Different
let xmlstream s = xmlescape 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 "\"/>"
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_goal_concl_style_env env typ) ++
str "\"/>"
in
List.fold_left (++) (mt ()) (List.map pr_one metas)
;;
let pr_goal_xml sigma g =
let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
if Decl_mode.try_get_info sigma g = None then
(hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
str "\"/>" ++
(pr_context_xml env)) ++
fnl () ++ str "</goal>")
else
(hov 2 (str "<goal type=\"declarative\">" ++
(pr_context_xml env)) ++
fnl () ++ str "</goal>")
;;
let print_proof_xml () =
Errors.anomaly "Dump Tree command not supported in this version."
VERNAC COMMAND EXTEND DumpTree
[ "Dump" "Tree" ] -> [ print_proof_xml () ]
END
|
