]> matita.cs.unibo.it Git - helm.git/blob - components/acic_content/contentPp.ml
Useless code simplified out.
[helm.git] / components / acic_content / contentPp.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (***************************************************************************)
27 (*                                                                         *)
28 (*                            PROJECT HELM                                 *)
29 (*                                                                         *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                     *)
31 (*                              17/06/2003                                 *)
32 (*                                                                         *)
33 (***************************************************************************)
34
35 (* $Id$ *)
36
37 exception ContentPpInternalError;;
38 exception NotEnoughElements;;
39 exception TO_DO
40
41 (* Utility functions *)
42
43
44 let string_of_name =
45  function
46     Some s -> s
47   | None  -> "_"
48 ;;
49
50 (* get_nth l n   returns the nth element of the list l if it exists or *)
51 (* raises NotEnoughElements if l has less than n elements              *)
52 let rec get_nth l n =
53  match (n,l) with
54     (1, he::_) -> he
55   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
56   | (_,_) -> raise NotEnoughElements
57 ;;
58
59 let rec blanks n = 
60   if n = 0 then ""
61   else (" " ^ (blanks (n-1)));; 
62
63 let rec pproof (p: Cic.annterm Content.proof) indent =
64   let module Con = Content in
65   let new_indent =
66     (match p.Con.proof_name with
67        Some s -> 
68          prerr_endline 
69           ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1)
70      | None ->indent) in
71   let new_indent1 = 
72     if (p.Con.proof_context = []) then new_indent
73     else 
74       (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in
75   papply_context p.Con.proof_apply_context new_indent1;
76   pconclude p.Con.proof_conclude new_indent1;
77
78 and pcontext c indent =
79   List.iter (pcontext_element indent) c
80
81 and pcontext_element indent =
82   let module Con = Content in
83   function
84       `Declaration d -> 
85         (match d.Con.dec_name with
86             Some s -> 
87               prerr_endline 
88                ((blanks indent)  
89                  ^ "Assume " ^ s ^ " : " 
90                  ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type)));
91               flush stderr
92           | None ->
93               prerr_endline ((blanks indent) ^ "NO NAME!!"))
94     | `Hypothesis h ->
95          (match h.Con.dec_name with
96             Some s -> 
97               prerr_endline 
98                ((blanks indent)  
99                  ^ "Suppose " ^ s ^ " : " 
100                  ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type)));
101               flush stderr
102           | None ->
103               prerr_endline ((blanks indent) ^ "NO NAME!!"))
104     | `Proof p -> pproof p indent
105     | `Definition d -> 
106          (match d.Con.def_name with
107             Some s -> 
108               prerr_endline 
109                ((blanks indent) ^ "Let " ^ s ^ " = " 
110                 ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term)));
111               flush stderr
112           | None ->
113               prerr_endline ((blanks indent) ^ "NO NAME!!")) 
114     | `Joint ho -> 
115          prerr_endline ((blanks indent) ^ "Joint Def");
116          flush stderr
117
118 and papply_context ac indent = 
119   List.iter(function p -> (pproof p indent)) ac
120
121 and pconclude concl indent =
122   let module Con = Content in
123   prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr;
124   pargs concl.Con.conclude_args indent;
125   match concl.Con.conclude_conclusion with
126      None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr
127     | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr
128
129 and pargs args indent =
130   List.iter (parg indent) args
131
132 and parg indent =
133   let module Con = Content in
134   function
135       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n)
136     | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
137     | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
138     | Con.Term t -> 
139         prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
140     | Con.ArgProof p -> pproof p (indent+1) 
141     | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
142 ;;
143  
144 let print_proof p = pproof p 0;;
145
146 let print_obj (_,_,_,obj) =
147   match obj with 
148     `Decl (_,decl) -> 
149        pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
150   | `Def (_,_,def) -> 
151        pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
152   | `Joint _ as jo -> pcontext_element 0 jo 
153 ;;
154
155
156
157
158