← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/xml/proofTree2Xml.ml4

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/xml/proofTree2Xml.ml4
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 
6
(*         *   University of Bologna                                    *)
 
7
(************************************************************************)
 
8
(*          This file is distributed under the terms of the             *)
 
9
(*           GNU Lesser General Public License Version 2.1              *)
 
10
(*                                                                      *)
 
11
(*                 Copyright (C) 2000-2004, HELM Team.                  *)
 
12
(*                       http://helm.cs.unibo.it                        *)
 
13
(************************************************************************)
 
14
 
 
15
let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
 
16
 
 
17
let std_ppcmds_to_string s =
 
18
   Pp.msg_with Format.str_formatter s;
 
19
   Format.flush_str_formatter ()
 
20
;;
 
21
 
 
22
let idref_of_id id = "v" ^ id;;
 
23
 
 
24
(* Transform a constr to an Xml.token Stream.t *)
 
25
(* env is a named context                      *)
 
26
(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *)
 
27
let constr_to_xml obj sigma env =
 
28
  let ids_to_terms = Hashtbl.create 503 in
 
29
  let constr_to_ids = Acic.CicHash.create 503 in
 
30
  let ids_to_father_ids = Hashtbl.create 503 in
 
31
  let ids_to_inner_sorts = Hashtbl.create 503 in
 
32
  let ids_to_inner_types = Hashtbl.create 503 in
 
33
 
 
34
  (* named_context holds section variables and local variables *)
 
35
  let named_context = Environ.named_context env  in
 
36
  (* real_named_context holds only the section variables *)
 
37
  let real_named_context = Environ.named_context (Global.env ()) in
 
38
  (* named_context' holds only the local variables *)
 
39
  let named_context' =
 
40
   List.filter (function n -> not (List.mem n real_named_context)) named_context
 
41
  in
 
42
  let idrefs =
 
43
   List.map
 
44
    (function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in
 
45
  let rel_context = Sign.push_named_to_rel_context named_context' [] in
 
46
  let rel_env =
 
47
   Environ.push_rel_context rel_context
 
48
    (Environ.reset_with_named_context 
 
49
        (Environ.val_of_named_context real_named_context) env) in
 
50
  let obj' =
 
51
   Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
 
52
  let seed = ref 0 in
 
53
   try
 
54
    let annobj =
 
55
     Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
 
56
      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env
 
57
      idrefs sigma (Unshare.unshare obj') None
 
58
    in
 
59
     Acic2Xml.print_term ids_to_inner_sorts annobj
 
60
   with e ->
 
61
    Util.anomaly
 
62
     ("Problem during the conversion of constr into XML: " ^
 
63
      Printexc.to_string e)
 
64
(* CSC: debugging stuff
 
65
Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
 
66
Pp.ppnl (Pp.str "ENVIRONMENT:") ;
 
67
Pp.ppnl (Printer.pr_context_of rel_env) ;
 
68
Pp.ppnl (Pp.str "TERM:") ;
 
69
Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
 
70
Pp.ppnl (Pp.str "RAW-TERM:") ;
 
71
Pp.ppnl (Printer.pr_lconstr obj') ;
 
72
Xml.xml_empty "MISSING TERM" [] (*; raise e*)
 
73
*)
 
74
;;
 
75
 
 
76
let first_word s =
 
77
   try let i = String.index s ' ' in
 
78
       String.sub s 0 i
 
79
   with _ -> s
 
80
;;
 
81
 
 
82
let string_of_prim_rule x = match x with
 
83
  | Proof_type.Intro _-> "Intro"
 
84
  | Proof_type.Cut _ -> "Cut"
 
85
  | Proof_type.FixRule _ -> "FixRule"
 
86
  | Proof_type.Cofix _ -> "Cofix"
 
87
  | Proof_type.Refine _ -> "Refine"
 
88
  | Proof_type.Convert_concl _ -> "Convert_concl"
 
89
  | Proof_type.Convert_hyp _->"Convert_hyp"
 
90
  | Proof_type.Thin _ -> "Thin"
 
91
  | Proof_type.ThinBody _-> "ThinBody"
 
92
  | Proof_type.Move (_,_,_) -> "Move"
 
93
  | Proof_type.Order _ -> "Order"
 
94
  | Proof_type.Rename (_,_) -> "Rename"
 
95
  | Proof_type.Change_evars -> "Change_evars"
 
96
 
 
97
let
 
98
 print_proof_tree curi sigma pf proof_tree_to_constr
 
99
  proof_tree_to_flattened_proof_tree constr_to_ids
 
100
=
 
101
 let module PT = Proof_type in
 
102
 let module L = Logic in
 
103
 let module X = Xml in
 
104
 let module T = Tacexpr in
 
105
  let ids_of_node node =
 
106
   let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
 
107
(*
 
108
let constr =
 
109
 try
 
110
    Proof2aproof.ProofTreeHash.find proof_tree_to_constr node
 
111
 with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated
 
112
no lambda-term: ") (Refiner.print_script true (Evd.empty)
 
113
(Global.named_context ()) node)) ; assert false (* Closed bug, should not
 
114
happen any more *)
 
115
in
 
116
*)
 
117
   try
 
118
    Some (Acic.CicHash.find constr_to_ids constr)
 
119
   with _ ->
 
120
Pp.ppnl (Pp.(++) (Pp.str
 
121
"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
 
122
(Printer.pr_lconstr constr)) ;
 
123
    None
 
124
  in
 
125
  let rec aux node old_hyps =
 
126
   let of_attribute =
 
127
    match ids_of_node node with
 
128
       None -> []
 
129
     | Some id -> ["of",id]
 
130
   in
 
131
    match node with
 
132
       {PT.ref=Some(PT.Prim tactic_expr,nodes)} ->
 
133
         let tac = string_of_prim_rule tactic_expr in
 
134
         let of_attribute = ("name",tac)::of_attribute in
 
135
          if nodes = [] then
 
136
           X.xml_empty "Prim" of_attribute
 
137
          else
 
138
           X.xml_nempty "Prim" of_attribute
 
139
            (List.fold_left
 
140
              (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
141
 
 
142
     | {PT.goal=goal;
 
143
        PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
 
144
         (* [hidden_proof] is the proof of the tactic;                     *)
 
145
         (* [nodes] are the proof of the subgoals generated by the tactic; *)
 
146
         (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
 
147
         (*  for the holes in [hidden_proof]                               *)
 
148
        let flat_proof =
 
149
         Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
 
150
        in begin
 
151
        match tactic_expr with
 
152
        | T.TacArg (T.Tacexp _) -> 
 
153
            (* We don't need to keep the level of abstraction introduced at *)
 
154
            (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
 
155
            aux flat_proof old_hyps
 
156
        | _ ->
 
157
         (****** la tactique employee *)
 
158
         let prtac = Pptactic.pr_tactic (Global.env()) in
 
159
         let tac = std_ppcmds_to_string (prtac tactic_expr) in
 
160
         let tacname= first_word tac in
 
161
         let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
 
162
 
 
163
         (****** le but *)
 
164
         let {Evd.evar_concl=concl;
 
165
              Evd.evar_hyps=hyps}=goal in
 
166
 
 
167
         let env = Global.env_of_context hyps in
 
168
 
 
169
         let xgoal =
 
170
          X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
 
171
 
 
172
         let rec build_hyps =
 
173
          function
 
174
           | [] -> xgoal
 
175
           | (id,c,tid)::hyps1 ->
 
176
              let id' = Names.string_of_id id in
 
177
               [< build_hyps hyps1;
 
178
                  (X.xml_nempty "Hypothesis"
 
179
                    ["id",idref_of_id id' ; "name",id']
 
180
                    (constr_to_xml tid sigma env))
 
181
               >] in
 
182
         let old_names = List.map (fun (id,c,tid)->id) old_hyps in
 
183
         let nhyps = Environ.named_context_of_val hyps in
 
184
         let new_hyps =
 
185
          List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
 
186
 
 
187
         X.xml_nempty "Tactic" of_attribute
 
188
          [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
 
189
        end
 
190
 
 
191
     | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
 
192
         Util.anomaly "Not Implemented" 
 
193
 
 
194
     | {PT.ref=Some(PT.Daimon,_)} ->
 
195
         X.xml_empty "Hidden_open_goal" of_attribute
 
196
 
 
197
     | {PT.ref=None;PT.goal=goal} ->
 
198
         X.xml_empty "Open_goal" of_attribute
 
199
  in
 
200
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
201
      X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n");
 
202
      X.xml_nempty "ProofTree" ["of",curi] (aux pf [])
 
203
   >]
 
204
;;
 
205
 
 
206
 
 
207
(* Hook registration *)
 
208
(* CSC: debranched since it is bugged
 
209
Xmlcommand.set_print_proof_tree print_proof_tree;;
 
210
*)