added HelmLibraryObjects module

[helm.git] / helm / ocaml / cic / helmLibraryObjects.ml

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
+