From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 19 Jan 2004 11:38:41 +0000 (+0000)
Subject: added Peano module and functions to create natural/real terms
X-Git-Tag: V_0_5_1_3~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bec2787ed93cd8132d25233ebfb3de275c20a47;p=helm.git

added Peano module and functions to create natural/real terms
---

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index 2d4938181..1d7e9285e 100644
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -1,4 +1,6 @@
 
+(** {2 Auxiliary functions} *)
+
 let uri = UriManager.uri_of_string
 
 let const ?(subst = []) uri = Cic.Const (uri, subst)
@@ -6,6 +8,8 @@ let var ?(subst = []) uri = Cic.Var (uri, subst)
 let mutconstruct ?(subst = []) uri typeno consno =
   Cic.MutConstruct (uri, typeno, consno, subst)
 
+(** {2 Helm's objects shorthands} *)
+
 module Logic =
   struct
     let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
@@ -52,3 +56,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
+