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