(* $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)));
-(* DisambiguateChoices.add_num_choice
+ ("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
HelmLibraryObjects.build_bin_pos num ]
else
assert false))
-*)