X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fnumber_notation.ml;h=c41a9aab091034a8f81610b914721fc66b0c1ff3;hb=4e51145c79bf8c5c8d42442f74b2c63ff68141ed;hp=9dece04ecda69100013d0f04c265b5b93ef8c7bf;hpb=623cbb7a784ce2d983608ee4a44bf386dfe01bbc;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 9dece04ec..c41a9aab0 100644
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -25,27 +25,48 @@
 
 (* $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",
-      (fun _ num _ -> LibraryObjects.build_nat (int_of_string num)));
+    ("natural number", `Num_interp interp_natural_number);
   DisambiguateChoices.add_num_choice
     ("Coq natural number",
-      (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
+      `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
   DisambiguateChoices.add_num_choice
     ("real number",
-      (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
+      `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num)));
   DisambiguateChoices.add_num_choice
     ("binary positive number",
-      (fun _ num _ ->
+      `Num_interp (fun num ->
         let num = int_of_string num in
-        if num = 0 then
-          raise (DisambiguateTypes.Invalid_choice (None, lazy "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
     ("binary integer number",
-      (fun _ num _ ->
+      `Num_interp (fun num ->
         let num = int_of_string num in
         if num = 0 then
           HelmLibraryObjects.BinInt.z0