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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
(************************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(* *)
(* Copyright (C) 2000-2004, HELM Team. *)
(* http://helm.cs.unibo.it *)
(************************************************************************)
let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
let std_ppcmds_to_string s =
Pp.msg_with Format.str_formatter s;
Format.flush_str_formatter ()
;;
let idref_of_id id = "v" ^ id;;
(* Transform a constr to an Xml.token Stream.t *)
(* env is a named context *)
(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *)
let constr_to_xml obj sigma env =
let ids_to_terms = Hashtbl.create 503 in
let constr_to_ids = Acic.CicHash.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
(* named_context holds section variables and local variables *)
let named_context = Environ.named_context env in
(* real_named_context holds only the section variables *)
let real_named_context = Environ.named_context (Global.env ()) in
(* named_context' holds only the local variables *)
let named_context' =
List.filter (function n -> not (List.mem n real_named_context)) named_context
in
let idrefs =
List.map
(function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in
let rel_context = Sign.push_named_to_rel_context named_context' [] in
let rel_env =
Environ.push_rel_context rel_context
(Environ.reset_with_named_context
(Environ.val_of_named_context real_named_context) env) in
let obj' =
Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
let seed = ref 0 in
try
let annobj =
Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env
idrefs sigma (Unshare.unshare obj') None
in
Acic2Xml.print_term ids_to_inner_sorts annobj
with e ->
Util.anomaly
("Problem during the conversion of constr into XML: " ^
Printexc.to_string e)
(* CSC: debugging stuff
Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
Pp.ppnl (Pp.str "ENVIRONMENT:") ;
Pp.ppnl (Printer.pr_context_of rel_env) ;
Pp.ppnl (Pp.str "TERM:") ;
Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
Pp.ppnl (Pp.str "RAW-TERM:") ;
Pp.ppnl (Printer.pr_lconstr obj') ;
Xml.xml_empty "MISSING TERM" [] (*; raise e*)
*)
;;
let first_word s =
try let i = String.index s ' ' in
String.sub s 0 i
with _ -> s
;;
let string_of_prim_rule x = match x with
| Proof_type.Intro _-> "Intro"
| Proof_type.Cut _ -> "Cut"
| Proof_type.FixRule _ -> "FixRule"
| Proof_type.Cofix _ -> "Cofix"
| Proof_type.Refine _ -> "Refine"
| Proof_type.Convert_concl _ -> "Convert_concl"
| Proof_type.Convert_hyp _->"Convert_hyp"
| Proof_type.Thin _ -> "Thin"
| Proof_type.ThinBody _-> "ThinBody"
| Proof_type.Move (_,_,_) -> "Move"
| Proof_type.Order _ -> "Order"
| Proof_type.Rename (_,_) -> "Rename"
| Proof_type.Change_evars -> "Change_evars"
let
print_proof_tree curi sigma pf proof_tree_to_constr
proof_tree_to_flattened_proof_tree constr_to_ids
=
let module PT = Proof_type in
let module L = Logic in
let module X = Xml in
let module T = Tacexpr in
let ids_of_node node =
let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
(*
let constr =
try
Proof2aproof.ProofTreeHash.find proof_tree_to_constr node
with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated
no lambda-term: ") (Refiner.print_script true (Evd.empty)
(Global.named_context ()) node)) ; assert false (* Closed bug, should not
happen any more *)
in
*)
try
Some (Acic.CicHash.find constr_to_ids constr)
with _ ->
Pp.ppnl (Pp.(++) (Pp.str
"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
(Printer.pr_lconstr constr)) ;
None
in
let rec aux node old_hyps =
let of_attribute =
match ids_of_node node with
None -> []
| Some id -> ["of",id]
in
match node with
{PT.ref=Some(PT.Prim tactic_expr,nodes)} ->
let tac = string_of_prim_rule tactic_expr in
let of_attribute = ("name",tac)::of_attribute in
if nodes = [] then
X.xml_empty "Prim" of_attribute
else
X.xml_nempty "Prim" of_attribute
(List.fold_left
(fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
| {PT.goal=goal;
PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
(* [hidden_proof] is the proof of the tactic; *)
(* [nodes] are the proof of the subgoals generated by the tactic; *)
(* [flat_proof] if the proof-tree obtained substituting [nodes] *)
(* for the holes in [hidden_proof] *)
let flat_proof =
Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
in begin
match tactic_expr with
| T.TacArg (T.Tacexp _) ->
(* We don't need to keep the level of abstraction introduced at *)
(* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
aux flat_proof old_hyps
| _ ->
(****** la tactique employee *)
let prtac = Pptactic.pr_tactic (Global.env()) in
let tac = std_ppcmds_to_string (prtac tactic_expr) in
let tacname= first_word tac in
let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
(****** le but *)
let {Evd.evar_concl=concl;
Evd.evar_hyps=hyps}=goal in
let env = Global.env_of_context hyps in
let xgoal =
X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
let rec build_hyps =
function
| [] -> xgoal
| (id,c,tid)::hyps1 ->
let id' = Names.string_of_id id in
[< build_hyps hyps1;
(X.xml_nempty "Hypothesis"
["id",idref_of_id id' ; "name",id']
(constr_to_xml tid sigma env))
>] in
let old_names = List.map (fun (id,c,tid)->id) old_hyps in
let nhyps = Environ.named_context_of_val hyps in
let new_hyps =
List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
X.xml_nempty "Tactic" of_attribute
[<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
end
| {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
Util.anomaly "Not Implemented"
| {PT.ref=Some(PT.Daimon,_)} ->
X.xml_empty "Hidden_open_goal" of_attribute
| {PT.ref=None;PT.goal=goal} ->
X.xml_empty "Open_goal" of_attribute
in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n");
X.xml_nempty "ProofTree" ["of",curi] (aux pf [])
>]
;;
(* Hook registration *)
(* CSC: debranched since it is bugged
Xmlcommand.set_print_proof_tree print_proof_tree;;
*)
|
