diff options
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 38 |
1 files changed, 23 insertions, 15 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index a9eb126b..ad8b54d4 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,11 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) + (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "nat_syntax_plugin" let () = Mltop.add_known_module __coq_plugin_name @@ -33,34 +36,39 @@ let warn_large_nat = strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed).") -let nat_of_int dloc n = +let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = GRef (dloc, glob_O, None) in - let ref_S = GRef (dloc, glob_S, None) in + let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in mk_nat ref_O n end else - user_err_loc (dloc, "nat_of_int", - str "Cannot interpret a negative number as a number of type nat") + user_err ?loc ~hdr:"nat_of_int" + (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) (* Printing via scopes *) exception Non_closed_number -let rec int_of_nat = function - | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) - | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero +let rec int_of_nat x = DAst.with_val (function + | GApp (r, [a]) -> + begin match DAst.get r with + | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end + | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number + ) x -let uninterp_nat p = +let uninterp_nat (AnyGlobConstr p) = try Some (int_of_nat p) with @@ -73,4 +81,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) + ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) |