X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FcontentPp.ml;fp=helm%2Focaml%2Fcic_omdoc%2FcontentPp.ml;h=0000000000000000000000000000000000000000;hp=3967c621668818fbb68b8e48fcd3e2bbc96e0b32;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
deleted file mode 100644
index 3967c6216..000000000
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ /dev/null
@@ -1,156 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(***************************************************************************)
-(*                                                                         *)
-(*                            PROJECT HELM                                 *)
-(*                                                                         *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                     *)
-(*                              17/06/2003                                 *)
-(*                                                                         *)
-(***************************************************************************)
-
-exception ContentPpInternalError;;
-exception NotEnoughElements;;
-exception TO_DO
-
-(* Utility functions *)
-
-
-let string_of_name =
- function
-    Some s -> s
-  | None  -> "_"
-;;
-
-(* get_nth l n   returns the nth element of the list l if it exists or *)
-(* raises NotEnoughElements if l has less than n elements              *)
-let rec get_nth l n =
- match (n,l) with
-    (1, he::_) -> he
-  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise NotEnoughElements
-;;
-
-let rec blanks n = 
-  if n = 0 then ""
-  else (" " ^ (blanks (n-1)));; 
-
-let rec pproof (p: Cic.annterm Content.proof) indent =
-  let module Con = Content in
-  let new_indent =
-    (match p.Con.proof_name with
-       Some s -> 
-         prerr_endline 
-          ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1)
-     | None ->indent) in
-  let new_indent1 = 
-    if (p.Con.proof_context = []) then new_indent
-    else 
-      (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in
-  papply_context p.Con.proof_apply_context new_indent1;
-  pconclude p.Con.proof_conclude new_indent1;
-
-and pcontext c indent =
-  List.iter (pcontext_element indent) c
-
-and pcontext_element indent =
-  let module Con = Content in
-  function
-      `Declaration d -> 
-        (match d.Con.dec_name with
-            Some s -> 
-              prerr_endline 
-               ((blanks indent)  
-                 ^ "Assume " ^ s ^ " : " 
-                 ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type)));
-              flush stderr
-          | None ->
-              prerr_endline ((blanks indent) ^ "NO NAME!!"))
-    | `Hypothesis h ->
-         (match h.Con.dec_name with
-            Some s -> 
-              prerr_endline 
-               ((blanks indent)  
-                 ^ "Suppose " ^ s ^ " : " 
-                 ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type)));
-              flush stderr
-          | None ->
-              prerr_endline ((blanks indent) ^ "NO NAME!!"))
-    | `Proof p -> pproof p indent
-    | `Definition d -> 
-         (match d.Con.def_name with
-            Some s -> 
-              prerr_endline 
-               ((blanks indent) ^ "Let " ^ s ^ " = " 
-                ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term)));
-              flush stderr
-          | None ->
-              prerr_endline ((blanks indent) ^ "NO NAME!!")) 
-    | `Joint ho -> 
-         prerr_endline ((blanks indent) ^ "Joint Def");
-         flush stderr
-
-and papply_context ac indent = 
-  List.iter(function p -> (pproof p indent)) ac
-
-and pconclude concl indent =
-  let module Con = Content in
-  prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr;
-  pargs concl.Con.conclude_args indent;
-  match concl.Con.conclude_conclusion with
-     None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr
-    | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr
-
-and pargs args indent =
-  List.iter (parg indent) args
-
-and parg indent =
-  let module Con = Content in
-  function
-      Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n)
-    | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
-    | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
-    | Con.Term t -> 
-        prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
-    | Con.ArgProof p -> pproof p (indent+1) 
-    | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
-;;
- 
-let print_proof p = pproof p 0;;
-
-let print_obj (_,_,_,obj) =
-  match obj with 
-    `Decl (_,decl) -> 
-       pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
-  | `Def (_,_,def) -> 
-       pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
-  | `Joint _ as jo -> pcontext_element 0 jo 
-;;
-
-
-
-
-