From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 10:12:12 +0000 (+0000) Subject: Dead code/files removed. X-Git-Tag: V_0_1_2_1~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18ab6500105671c07f65430be5c899732fc101c3;p=helm.git Dead code/files removed. --- diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index 2dd0a2f31..ff75618f8 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -37,19 +37,6 @@ val string_of_sort: sort_kind -> string val sort_of_string: string -> sort_kind val sort_of_sort: Cic.sort -> sort_kind -val acic_of_cic_context' : - int ref -> (* seed *) - (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) - (Cic.id, sort_kind) Hashtbl.t -> (* ids_to_inner_sorts *) - (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) - Cic.metasenv -> (* metasenv *) - Cic.context -> (* context *) - Cic.id list -> (* idrefs *) - Cic.term -> (* term *) - Cic.term option -> (* expected type *) - Cic.annterm (* annotated term *) - val acic_object_of_cic_object : ?eta_fix: bool -> (* perform eta_fixing; default: true*) Cic.obj -> (* object *) diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 3669f5d7e..4a8977aa7 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -17,7 +17,6 @@ INTERFACE_FILES = \ sequent2pres.mli \ domMisc.mli \ xml2Gdome.mli \ - sequentPp.mli \ applyTransformation.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml deleted file mode 100644 index e7b3151ea..000000000 --- a/helm/ocaml/cic_transformations/sequentPp.ml +++ /dev/null @@ -1,118 +0,0 @@ -(* Copyright (C) 2000-2002, 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/. - *) - -module TextualPp = - struct - (* It also returns the pretty-printing context! *) - let print_context ctx = - let print_name = - function - Cic.Name n -> n - | Cic.Anonymous -> "_" - in - List.fold_right - (fun i (output,context) -> - let (newoutput,context') = - match i with - Some (n,Cic.Decl t) -> - print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context - | Some (n,Cic.Def (t,None)) -> - print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context - | None -> - "_ ?= _\n", None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - in - output^newoutput,context' - ) ctx ("",[]) - ;; - - exception NotImplemented;; - - let print_sequent (metano,context,goal) = - "\n" ^ - let (output,pretty_printer_context_of_context) = print_context context in - output ^ - "---------------------- ?" ^ string_of_int metano ^ "\n" ^ - CicPp.pp goal pretty_printer_context_of_context - ;; - end -;; - -module XmlPp = - struct - let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";; - - let print_sequent metasenv (metano,context,goal) = - let module X = Xml in - let ids_to_terms = Hashtbl.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let ids_to_hypotheses = Hashtbl.create 11 in - let hypotheses_seed = ref 0 in - let sequent_id = "i0" in - let seed = ref 1 in (* 'i0' is used for the whole sequent *) - let acic_of_cic_context = - Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types metasenv - in - let final_s,_,final_idrefs = - (List.fold_right - (fun binding (s,context,idrefs) -> - let hid = "h" ^ string_of_int !hypotheses_seed in - Hashtbl.add ids_to_hypotheses hid binding ; - incr hypotheses_seed ; - match binding with - (Some (n,(Cic.Def (t,None) as b)) as entry) - | (Some (n,(Cic.Decl t as b)) as entry) -> - let acic = acic_of_cic_context context idrefs t None in - [< s ; - X.xml_nempty - (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def") - [None,"name",(match n with Cic.Name n -> n | _ -> assert false); - None,"id",hid] - (Cic2Xml.print_term ~ids_to_inner_sorts acic) - >], (entry::context), (hid::idrefs) - | None -> - (* Invariant: "" is never looked up *) - [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context ([<>],[],[]) - ) - in - let acic = acic_of_cic_context context final_idrefs goal None in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n"); - X.xml_nempty "Sequent" - [None,"no",string_of_int metano;None,"id",sequent_id] - [< final_s ; - Xml.xml_nempty "Goal" [] - (Cic2Xml.print_term ~ids_to_inner_sorts acic) - >] - >], - ids_to_terms,ids_to_father_ids,ids_to_hypotheses - ;; - end -;; diff --git a/helm/ocaml/cic_transformations/sequentPp.mli b/helm/ocaml/cic_transformations/sequentPp.mli deleted file mode 100644 index 61f843fe8..000000000 --- a/helm/ocaml/cic_transformations/sequentPp.mli +++ /dev/null @@ -1,42 +0,0 @@ -(* Copyright (C) 2000-2002, 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/. - *) - -module TextualPp : - sig - val print_context : - (Cic.name * Cic.context_entry) option list -> - string * Cic.name option list - exception NotImplemented - val print_sequent : - int * (Cic.name * Cic.context_entry) option list * Cic.term -> string - end -module XmlPp : - sig - val print_sequent : - Cic.metasenv -> - int * Cic.context * Cic.term -> - Xml.token Stream.t * (Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t - end