- libraryObjects: new default "natural numbers" with the uri of nat.

[helm.git] / helm / software / components / cic_disambiguation / number_notation.ml

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 06099dcfe20a5aa02ab46be5b22835e517b514d6..c41a9aab091034a8f81610b914721fc66b0c1ff3 100644 (file)
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -25,10 +25,31 @@
 
 (* $Id$ *)
 
+module C   = Cic
+module Obj = LibraryObjects
+module DT  = DisambiguateTypes
+
+let error msg =
+   raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
+
+let build_nat o s str =
+   let n = int_of_string str in
+   if n < 0 then error (str ^ " is not a valid natural number number") else
+   let rec aux n = if n = 0 then o () else s (aux (pred n)) in
+   aux n
+
+let interp_natural_number num =
+   let nat_URI = match Obj.nat_URI () with
+      | Some uri -> uri
+      | None     -> error "no default natural numbers"
+   in
+   let o () = C.MutConstruct (nat_URI,0,1,[]) in
+   let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in
+   build_nat o s num
+
 let _ =
   DisambiguateChoices.add_num_choice
-    ("natural number",
-      `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num)));
+    ("natural number", `Num_interp interp_natural_number);
   DisambiguateChoices.add_num_choice
     ("Coq natural number",
       `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
@@ -39,8 +60,8 @@ let _ =
     ("binary positive number",
       `Num_interp (fun num ->
         let num = int_of_string num in
-        if num = 0 then
-          raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
+        if num = 0 then 
+          error "0 is not a valid positive number"
         else
           HelmLibraryObjects.build_bin_pos num));
   DisambiguateChoices.add_num_choice