added HelmLibraryObjects module

diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend
index 591cea8dfe228a51de3cf22671a1e23a368792ec..3bf9bfedeb6acea2e7a94ecf26b6374591eed470 100644 (file)
--- a/helm/ocaml/cic/.depend
+++ b/helm/ocaml/cic/.depend
@@ -10,3 +10,5 @@ cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi
 cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi 
 cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi 
 cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi 
+helmLibraryObjects.cmo: cic.cmo 
+helmLibraryObjects.cmx: cic.cmx 

diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile
index c18667dc228398a5f3790f04e638d2b7b4ff21a5..1789cd67ee7792208efc06b55789c28e23e42e36 100644 (file)
--- a/helm/ocaml/cic/Makefile
+++ b/helm/ocaml/cic/Makefile
@@ -3,7 +3,7 @@ REQUIRES = helm-urimanager helm-pxp
 PREDICATES =
 
 INTERFACE_FILES = deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli
-IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml)
+IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml) helmLibraryObjects.ml
 EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
 EXTRA_OBJECTS_TO_CLEAN =
 

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
new file mode 100644 (file)
index 0000000..2d49381
--- /dev/null
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -0,0 +1,54 @@
+
+let uri = UriManager.uri_of_string
+
+let const ?(subst = []) uri = Cic.Const (uri, subst)
+let var ?(subst = []) uri = Cic.Var (uri, subst)
+let mutconstruct ?(subst = []) uri typeno consno =
+  Cic.MutConstruct (uri, typeno, consno, subst)
+
+module Logic =
+  struct
+    let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
+    let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
+    let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
+  end
+
+module Logic_Type =
+  struct
+    let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
+    let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
+
+    let refl_eqt = mutconstruct eqt_URI 0 1
+    let sym_eqt = const sym_eqt_URI
+  end
+
+module Datatypes =
+  struct
+    let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
+    let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
+
+    let trueb = mutconstruct bool_URI 0 1
+    let falseb = mutconstruct bool_URI 0 2
+    let zero = mutconstruct nat_URI 0 1
+    let succ = mutconstruct nat_URI 0 2
+  end
+
+module Reals =
+  struct
+    let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
+    let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
+    let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+    let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+    let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
+    let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
+    let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
+
+    let r = const r_URI
+    let rplus = const rplus_URI
+    let rmult = const rmult_URI
+    let ropp = const ropp_URI
+    let r0 = const r0_URI
+    let r1 = const r1_URI
+    let rtheory = const rtheory_URI
+  end
+