test branch

[helm.git] / helm / ocaml / acic_content / contentPp.ml

diff --git a/helm/ocaml/acic_content/contentPp.ml b/helm/ocaml/acic_content/contentPp.ml
new file mode 100644 (file)
index 0000000..ca89fad
--- /dev/null
+++ b/helm/ocaml/acic_content/contentPp.ml
@@ -0,0 +1,158 @@
+(* 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                                 *)
+(*                                                                         *)
+(***************************************************************************)
+
+(* $Id$ *)
+
+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 
+;;
+
+
+
+
+