split into two major parts:

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

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index 2d493818129f8814d9feaddc6f96458dfbddaf89..af781edc8fb8cd7ca8bd08fc997c3a1bdd4b818f 100644 (file)
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -1,3 +1,4 @@
+(** {2 Auxiliary functions} *)
 
 let uri = UriManager.uri_of_string
 
@@ -5,6 +6,49 @@ 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)
+let mutind ?(subst = []) uri typeno = Cic.MutInd (uri, typeno, subst)
+
+let indtyuri_of_uri uri =
+  let index_sharp =  String.index uri '#' in
+  let index_num = index_sharp + 3 in
+  (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+   int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
+
+let indconuri_of_uri uri =
+  let index_sharp =  String.index uri '#' in
+  let index_div = String.rindex uri '/' in
+  let index_con = index_div + 1 in
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+    int_of_string
+      (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
+    int_of_string
+      (String.sub uri index_con (String.length uri - index_con)))
+
+let term_of_uri uri =
+  let s = UriManager.string_of_uri uri in
+  try
+  (* Constant *)
+  (* TODO explicit substitutions? *)
+  let len = String.length s in
+  let sub = String.sub s (len -4) 4 in
+  if sub = ".con" then
+    const uri
+  else if sub = ".var" then
+    var uri
+  else
+    (try
+      (* Inductive Type *)
+      let (uri, typeno) = indtyuri_of_uri s in
+      mutind uri typeno
+     with
+      | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
+          (* Constructor of an Inductive Type *)
+          let (uri, typeno, consno) = indconuri_of_uri s in
+          mutconstruct uri typeno consno)
+ with
+ | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)
+
+(** {2 Helm's objects shorthands} *)
 
 module Logic =
   struct
@@ -52,3 +96,36 @@ module Reals =
     let rtheory = const rtheory_URI
   end
 
+module Peano =
+  struct
+    let plus_URI = uri "cic:/Coq/Init/Peano/plus.con"
+    let mult_URI = uri "cic:/Coq/Init/Peano/mult.con"
+    let pred_URI = uri "cic:/Coq/Init/Peano/pred.con"
+
+    let plus = const plus_URI
+    let mult = const mult_URI
+    let pred = const pred_URI
+  end
+
+(** {2 Helpers for creating common terms}
+ *  (e.g. numbers)} *)
+
+exception NegativeInteger
+
+let build_nat n =
+  if n < 0 then raise NegativeInteger;
+  let rec aux = function
+    | 0 -> Datatypes.zero
+    | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ]
+  in
+  aux n
+
+let build_real n =
+  if n < 0 then raise NegativeInteger;
+  let rec aux = function
+    | 0 -> Reals.r0
+    | 1 -> Reals.r1 (* to avoid trailing "+ 0" *)
+    | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ]
+  in
+  aux n
+