From 82466efd82082c6101d1c2c0c217f681b37160e8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 May 2002 10:10:54 +0000 Subject: [PATCH] cic2acic.mli added --- helm/gTopLevel/.depend | 6 +++-- helm/gTopLevel/Makefile | 4 +-- helm/gTopLevel/cic2acic.mli | 51 +++++++++++++++++++++++++++++++++++++ 3 files changed, 57 insertions(+), 4 deletions(-) create mode 100644 helm/gTopLevel/cic2acic.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 63ec81c6c..5a677d73a 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,12 +1,14 @@ proofEngine.cmo: proofEngineReduction.cmo proofEngine.cmx: proofEngineReduction.cmx +cic2acic.cmo: cic2acic.cmi +cic2acic.cmx: cic2acic.cmi logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx -sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo +sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx mquery.cmo: mquery.cmi mquery.cmx: mquery.cmi -gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo mquery.cmi \ +gTopLevel.cmo: cic2Xml.cmo cic2acic.cmi logicalOperations.cmo mquery.cmi \ proofEngine.cmo sequentPp.cmo xml2Gdome.cmo gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx mquery.cmx \ proofEngine.cmx sequentPp.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index a8f9d6b06..cd800f906 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -14,8 +14,8 @@ all: gTopLevel opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ - cic2acic.ml logicalOperations.ml sequentPp.ml mquery.mli mquery.ml \ - gTopLevel.ml + cic2acic.ml cic2acic.mli logicalOperations.ml sequentPp.ml \ + mquery.mli mquery.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli new file mode 100644 index 000000000..479a5760c --- /dev/null +++ b/helm/gTopLevel/cic2acic.mli @@ -0,0 +1,51 @@ +(* 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/. + *) + +exception NotImplemented +exception NotEnoughElements +exception NameExpected +exception Found of (Cic.name * Cic.context_entry) list +exception NotImplemented + +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, string) Hashtbl.t -> (* ids_to_inner_sorts *) + (Cic.id, Cic.annterm) Hashtbl.t -> (* ids_to_inner_types *) + Cic.metasenv -> (* metasenv *) + Cic.context -> (* context *) + Cic.term -> (* term *) + Cic.annterm (* annotated term *) + +val acic_object_of_cic_object : + Cic.obj -> (* object *) + Cic.annobj * (* annotated object *) + (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic.annterm) Hashtbl.t * (* ids_to_inner_types *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) + (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) -- 2.39.2