cic2acic.mli added

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 63ec81c6c12fa008e8b07f10c73a66600f28775d..5a677d73a1cd89b817ba5900e7fa0eb43215f342 100644 (file)
--- 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 a8f9d6b06709222bac1ebb70eeb97045b5250e65..cd800f906c528a108e7b0fa5e796907c49b37e45 100644 (file)
--- 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 (file)
index 0000000..479a576
--- /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 *)