(* 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;