summaryrefslogtreecommitdiff
path: root/plugins/syntax/z_syntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/z_syntax.ml')
-rw-r--r--plugins/syntax/z_syntax.ml107
1 files changed, 58 insertions, 49 deletions
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 60803a36..d5300e47 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* 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) *)
(************************************************************************)
open Pp
@@ -44,37 +46,42 @@ let glob_xI = ConstructRef path_of_xI
let glob_xO = ConstructRef path_of_xO
let glob_xH = ConstructRef path_of_xH
-let pos_of_bignat dloc x =
- let ref_xI = GRef (dloc, glob_xI, None) in
- let ref_xH = GRef (dloc, glob_xH, None) in
- let ref_xO = GRef (dloc, glob_xO, None) in
+let pos_of_bignat ?loc x =
+ let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
+ let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
+ let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
let rec pos_of x =
match div2_with_rest x with
- | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
- | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
+ | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
-let error_non_positive dloc =
- user_err_loc (dloc, "interp_positive",
- str "Only strictly positive numbers in type \"positive\".")
+let error_non_positive ?loc =
+ user_err ?loc ~hdr:"interp_positive"
+ (str "Only strictly positive numbers in type \"positive\".")
-let interp_positive dloc n =
- if is_strictly_pos n then pos_of_bignat dloc n
- else error_non_positive dloc
+let interp_positive ?loc n =
+ if is_strictly_pos n then pos_of_bignat ?loc n
+ else error_non_positive ?loc
(**********************************************************************)
(* Printing positive via scopes *)
(**********************************************************************)
-let rec bignat_of_pos = function
- | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
- | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
- | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
+let rec bignat_of_pos x = DAst.with_val (function
+ | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+ | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
| _ -> raise Non_closed_number
+ ) x
-let uninterp_positive p =
+let uninterp_positive (AnyGlobConstr p) =
try
Some (bignat_of_pos p)
with Non_closed_number ->
@@ -87,9 +94,9 @@ let uninterp_positive p =
let _ = Notation.declare_numeral_interpreter "positive_scope"
(positive_path,binnums)
interp_positive
- ([GRef (Loc.ghost, glob_xI, None);
- GRef (Loc.ghost, glob_xO, None);
- GRef (Loc.ghost, glob_xH, None)],
+ ([DAst.make @@ GRef (glob_xI, None);
+ DAst.make @@ GRef (glob_xO, None);
+ DAst.make @@ GRef (glob_xH, None)],
uninterp_positive,
true)
@@ -106,29 +113,30 @@ let glob_Npos = ConstructRef path_of_Npos
let n_path = make_path binnums "N"
-let n_of_binnat dloc pos_or_neg n =
+let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
if not (Bigint.equal n zero) then
- GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n])
+ GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
else
- GRef (dloc, glob_N0, None)
+ GRef(glob_N0, None)
-let error_negative dloc =
- user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
+let error_negative ?loc =
+ user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
-let n_of_int dloc n =
- if is_pos_or_zero n then n_of_binnat dloc true n
- else error_negative dloc
+let n_of_int ?loc n =
+ if is_pos_or_zero n then n_of_binnat ?loc true n
+ else error_negative ?loc
(**********************************************************************)
(* Printing N via scopes *)
(**********************************************************************)
-let bignat_of_n = function
- | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
- | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+let bignat_of_n n = DAst.with_val (function
+ | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
+ | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
| _ -> raise Non_closed_number
+ ) n
-let uninterp_n p =
+let uninterp_n (AnyGlobConstr p) =
try Some (bignat_of_n p)
with Non_closed_number -> None
@@ -138,8 +146,8 @@ let uninterp_n p =
let _ = Notation.declare_numeral_interpreter "N_scope"
(n_path,binnums)
n_of_int
- ([GRef (Loc.ghost, glob_N0, None);
- GRef (Loc.ghost, glob_Npos, None)],
+ ([DAst.make @@ GRef (glob_N0, None);
+ DAst.make @@ GRef (glob_Npos, None)],
uninterp_n,
true)
@@ -157,25 +165,26 @@ let glob_ZERO = ConstructRef path_of_ZERO
let glob_POS = ConstructRef path_of_POS
let glob_NEG = ConstructRef path_of_NEG
-let z_of_int dloc n =
+let z_of_int ?loc n =
if not (Bigint.equal n zero) then
let sgn, n =
if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
- GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n])
+ DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
else
- GRef (dloc, glob_ZERO, None)
+ DAst.make ?loc @@ GRef(glob_ZERO, None)
(**********************************************************************)
(* Printing Z via scopes *)
(**********************************************************************)
-let bigint_of_z = function
- | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
- | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
- | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+let bigint_of_z z = DAst.with_val (function
+ | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
+ | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
+ | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
| _ -> raise Non_closed_number
+ ) z
-let uninterp_z p =
+let uninterp_z (AnyGlobConstr p) =
try
Some (bigint_of_z p)
with Non_closed_number -> None
@@ -186,8 +195,8 @@ let uninterp_z p =
let _ = Notation.declare_numeral_interpreter "Z_scope"
(z_path,binnums)
z_of_int
- ([GRef (Loc.ghost, glob_ZERO, None);
- GRef (Loc.ghost, glob_POS, None);
- GRef (Loc.ghost, glob_NEG, None)],
+ ([DAst.make @@ GRef (glob_ZERO, None);
+ DAst.make @@ GRef (glob_POS, None);
+ DAst.make @@ GRef (glob_NEG, None)],
uninterp_z,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 21:17:05 +0000