helm/ocaml/cic_omdoc/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 exception ContentPpInternalError;;
  36 exception NotEnoughElements;;
  37 exception TO_DO
  38
  39 (* Utility functions *)
  40
  41
  42 let string_of_name =
  43  function
  44     Some s -> s
  45   | None  -> "_"
  46 ;;
  47
  48 (* get_nth l n   returns the nth element of the list l if it exists or *)
  49 (* raises NotEnoughElements if l has less than n elements              *)
  50 let rec get_nth l n =
  51  match (n,l) with
  52     (1, he::_) -> he
  53   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
  54   | (_,_) -> raise NotEnoughElements
  55 ;;
  56
  57 let rec blanks n =
  58   if n = 0 then ""
  59   else (" " ^ (blanks (n-1)));;
  60
  61 let rec pproof (p: Cic.annterm Content.proof) indent =
  62   let module Con = Content in
  63   let new_indent =
  64     (match p.Con.proof_name with
  65        Some s ->
  66          prerr_endline
  67           ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1)
  68      | None ->indent) in
  69   let new_indent1 =
  70     if (p.Con.proof_context = []) then new_indent
  71     else
  72       (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in
  73   papply_context p.Con.proof_apply_context new_indent1;
  74   pconclude p.Con.proof_conclude new_indent1;
  75
  76 and pcontext c indent =
  77   List.iter (pcontext_element indent) c
  78
  79 and pcontext_element indent =
  80   let module Con = Content in
  81   function
  82       `Declaration d ->
  83         (match d.Con.dec_name with
  84             Some s ->
  85               prerr_endline
  86                ((blanks indent)
  87                  ^ "Assume " ^ s ^ " : "
  88                  ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type)));
  89               flush stderr
  90           | None ->
  91               prerr_endline ((blanks indent) ^ "NO NAME!!"))
  92     | `Hypothesis h ->
  93          (match h.Con.dec_name with
  94             Some s ->
  95               prerr_endline
  96                ((blanks indent)
  97                  ^ "Suppose " ^ s ^ " : "
  98                  ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type)));
  99               flush stderr
 100           | None ->
 101               prerr_endline ((blanks indent) ^ "NO NAME!!"))
 102     | `Proof p -> pproof p indent
 103     | `Definition d ->
 104          (match d.Con.def_name with
 105             Some s ->
 106               prerr_endline
 107                ((blanks indent) ^ "Let " ^ s ^ " = "
 108                 ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term)));
 109               flush stderr
 110           | None ->
 111               prerr_endline ((blanks indent) ^ "NO NAME!!"))
 112     | `Joint ho ->
 113          prerr_endline ((blanks indent) ^ "Joint Def");
 114          flush stderr
 115
 116 and papply_context ac indent =
 117   List.iter(function p -> (pproof p indent)) ac
 118
 119 and pconclude concl indent =
 120   let module Con = Content in
 121   prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr;
 122   pargs concl.Con.conclude_args indent;
 123   match concl.Con.conclude_conclusion with
 124      None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr
 125     | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr
 126
 127 and pargs args indent =
 128   List.iter (parg indent) args
 129
 130 and parg indent =
 131   let module Con = Content in
 132   function
 133       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n)
 134     | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
 135     | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
 136     | Con.Term t ->
 137         prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
 138     | Con.ArgProof p -> pproof p (indent+1)
 139     | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
 140 ;;
 141
 142 let print_proof p = pproof p 0;;
 143
 144 let print_obj (_,_,_,obj) =
 145   match obj with
 146     `Decl (_,decl) ->
 147        pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
 148   | `Def (_,_,def) ->
 149        pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
 150   | `Joint _ as jo -> pcontext_element 0 jo
 151 ;;
 152
 153
 154
 155
 156