helm/ocaml/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