+++ /dev/null
-(* 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;;
-
-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
-;;
-
-
-
-
-
projects / helm.git / blobdiff