aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 11:16:35 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 11:16:35 +0200
commitf2fec63025d933f56dabf114a51720b1aae626c1 (patch)
tree7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/syntax
parent28f8da9489463b166391416de86420c15976522f (diff)
parent94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff)
Merge PR#402: Uniform attribute handling in interfaces
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/ascii_syntax.ml20
-rw-r--r--plugins/syntax/nat_syntax.ml19
-rw-r--r--plugins/syntax/numbers_syntax.ml100
-rw-r--r--plugins/syntax/r_syntax.ml38
-rw-r--r--plugins/syntax/string_syntax.ml16
-rw-r--r--plugins/syntax/z_syntax.ml85
6 files changed, 141 insertions, 137 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index ed8cc6ab0..e7eea0284 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,34 +37,34 @@ let glob_Ascii = lazy (make_reference "Ascii")
open Lazy
-let interp_ascii dloc p =
+let interp_ascii ?loc p =
let rec aux n p =
if Int.equal n 0 then [] else
let mp = p mod 2 in
- GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
+ (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
:: (aux (n-1) (p/2)) in
- GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
+ CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
-let interp_ascii_string dloc s =
+let interp_ascii_string ?loc s =
let p =
if Int.equal (String.length s) 1 then int_of_char s.[0]
else
if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
then int_of_string s
else
- user_err ~loc:dloc ~hdr:"interp_ascii_string"
+ user_err ?loc ~hdr:"interp_ascii_string"
(str "Expects a single character or a three-digits ascii code.") in
- interp_ascii dloc p
+ interp_ascii ?loc p
let uninterp_ascii r =
let rec uninterp_bool_list n = function
| [] when Int.equal n 0 -> 0
- | GRef (_,k,_)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l)
- | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
+ | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l)
+ | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
| _ -> raise Non_closed_ascii in
try
let aux = function
- | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+ | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
| _ -> raise Non_closed_ascii in
Some (aux r)
with
@@ -80,4 +80,4 @@ let _ =
Notation.declare_string_interpreter "char_scope"
(ascii_path,ascii_module)
interp_ascii_string
- ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true)
+ ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index ab262fea7..9a4cd6c25 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -33,21 +33,21 @@ 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 = CAst.make ?loc @@ GRef (glob_O, None) in
+ let ref_S = CAst.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 (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
else
acc
in
mk_nat ref_O n
end
else
- user_err ~hdr:"nat_of_int"
+ user_err ?loc ~hdr:"nat_of_int"
(str "Cannot interpret a negative number as a number of type nat")
(************************************************************************)
@@ -55,10 +55,11 @@ let nat_of_int dloc n =
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 = CAst.with_val (function
+ | GApp ({ CAst.v = 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
| _ -> raise Non_closed_number
+ ) x
let uninterp_nat p =
try
@@ -73,4 +74,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)
+ ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index a25ddb062..e23852bf8 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -86,10 +86,10 @@ exception Non_closed
(* parses a *non-negative* integer (from bigint.ml) into an int31
wraps modulo 2^31 *)
-let int31_of_pos_bigint dloc n =
- let ref_construct = GRef (dloc, int31_construct, None) in
- let ref_0 = GRef (dloc, int31_0, None) in
- let ref_1 = GRef (dloc, int31_1, None) in
+let int31_of_pos_bigint ?loc n =
+ let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in
+ let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in
+ let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in
let rec args counter n =
if counter <= 0 then
[]
@@ -97,16 +97,16 @@ let int31_of_pos_bigint dloc n =
let (q,r) = div2_with_rest n in
(if r then ref_1 else ref_0)::(args (counter-1) q)
in
- GApp (dloc, ref_construct, List.rev (args 31 n))
+ CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n))
-let error_negative dloc =
- CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
+let error_negative ?loc =
+ CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
-let interp_int31 dloc n =
+let interp_int31 ?loc n =
if is_pos_or_zero n then
- int31_of_pos_bigint dloc n
+ int31_of_pos_bigint ?loc n
else
- error_negative dloc
+ error_negative ?loc
(* Pretty prints an int31 *)
@@ -114,12 +114,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> cur
- | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
- | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
+ | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+ | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
| _ -> raise Non_closed
in
function
- | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero
+ | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -132,7 +132,7 @@ let uninterp_int31 i =
let _ = Notation.declare_numeral_interpreter int31_scope
(int31_path, int31_module)
interp_int31
- ([GRef (Loc.ghost, int31_construct, None)],
+ ([CAst.make @@ GRef (int31_construct, None)],
uninterp_int31,
true)
@@ -162,40 +162,40 @@ let height bi =
in hght 0 base
(* n must be a non-negative integer (from bigint.ml) *)
-let word_of_pos_bigint dloc hght n =
- let ref_W0 = GRef (dloc, zn2z_W0, None) in
- let ref_WW = GRef (dloc, zn2z_WW, None) in
+let word_of_pos_bigint ?loc hght n =
+ let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in
+ let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in
let rec decomp hgt n =
if hgt <= 0 then
- int31_of_pos_bigint dloc n
+ int31_of_pos_bigint ?loc n
else if equal n zero then
- GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
+ CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
else
let (h,l) = split_at hgt n in
- GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
+ CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
decomp (hgt-1) h;
decomp (hgt-1) l])
in
decomp hght n
-let bigN_of_pos_bigint dloc n =
+let bigN_of_pos_bigint ?loc n =
let h = height n in
- let ref_constructor = GRef (dloc, bigN_constructor h, None) in
- let word = word_of_pos_bigint dloc h n in
+ let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in
+ let word = word_of_pos_bigint ?loc h n in
let args =
if h < n_inlined then [word]
- else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
+ else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word]
in
- GApp (dloc, ref_constructor, args)
+ CAst.make ?loc @@ GApp (ref_constructor, args)
-let bigN_error_negative dloc =
- CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
+let bigN_error_negative ?loc =
+ CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
-let interp_bigN dloc n =
+let interp_bigN ?loc n =
if is_pos_or_zero n then
- bigN_of_pos_bigint dloc n
+ bigN_of_pos_bigint ?loc n
else
- bigN_error_negative dloc
+ bigN_error_negative ?loc
(* Pretty prints a bigN *)
@@ -203,14 +203,14 @@ let interp_bigN dloc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW ->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW ->
1+max (get_height lft) (get_height rght)
| _ -> 0
in
let rec transform hght rc =
match rc with
- | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero
- | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW->
let new_hght = hght-1 in
add (mult (rank new_hght)
(transform new_hght lft))
@@ -223,8 +223,8 @@ let bigint_of_word =
let bigint_of_bigN rc =
match rc with
- | GApp (_,_,[one_arg]) -> bigint_of_word one_arg
- | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
+ | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg
+ | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg
| _ -> raise Non_closed
let uninterp_bigN rc =
@@ -240,7 +240,7 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
if i < n_inlined+1 then
- GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1))
+ (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1))
else
[]
in
@@ -256,18 +256,18 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
(*** Parsing for bigZ in digital notation ***)
-let interp_bigZ dloc n =
- let ref_pos = GRef (dloc, bigZ_pos, None) in
- let ref_neg = GRef (dloc, bigZ_neg, None) in
+let interp_bigZ ?loc n =
+ let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in
+ let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in
if is_pos_or_zero n then
- GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
+ CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
else
- GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
+ CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
- | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg ->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_neg ->
let opp_val = bigint_of_bigN one_arg in
if equal opp_val zero then
raise Non_closed
@@ -286,19 +286,19 @@ let uninterp_bigZ rc =
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
- ([GRef (Loc.ghost, bigZ_pos, None);
- GRef (Loc.ghost, bigZ_neg, None)],
+ ([CAst.make @@ GRef (bigZ_pos, None);
+ CAst.make @@ GRef (bigZ_neg, None)],
uninterp_bigZ,
true)
(*** Parsing for bigQ in digital notation ***)
-let interp_bigQ dloc n =
- let ref_z = GRef (dloc, bigQ_z, None) in
- GApp (dloc, ref_z, [interp_bigZ dloc n])
+let interp_bigQ ?loc n =
+ let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in
+ CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
let uninterp_bigQ rc =
try match rc with
- | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z ->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [one_arg]) } when eq_gr c bigQ_z ->
Some (bigint_of_bigZ one_arg)
| _ -> None (* we don't pretty-print yet fractions *)
with Non_closed -> None
@@ -307,5 +307,5 @@ let uninterp_bigQ rc =
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ,
+ ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ,
true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 8f065f528..7ce066c59 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -41,14 +41,14 @@ 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 = CAst.make @@ GRef (glob_xI, None) in
+ let ref_xH = CAst.make @@ GRef (glob_xH, None) in
+ let ref_xO = CAst.make @@ 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) -> CAst.make @@ GApp (ref_xO,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
@@ -58,9 +58,9 @@ let pos_of_bignat dloc x =
(**********************************************************************)
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
+ | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+ | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one
| _ -> raise Non_closed_number
(**********************************************************************)
@@ -77,22 +77,22 @@ 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])
+ CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
else
- GRef (dloc, glob_ZERO, None)
+ CAst.make @@ 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
+ | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+ | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+ | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero
| _ -> raise Non_closed_number
(**********************************************************************)
@@ -107,15 +107,15 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id)
let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
-let r_of_int dloc z =
- GApp (dloc, GRef(dloc,glob_IZR,None), [z_of_int dloc z])
+let r_of_int ?loc z =
+ CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
(**********************************************************************)
(* Printing R via scopes *)
(**********************************************************************)
let bigint_of_r = function
- | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR ->
+ | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR ->
bigint_of_z a
| _ -> raise Non_closed_number
@@ -128,6 +128,6 @@ let uninterp_r p =
let _ = Notation.declare_numeral_interpreter "R_scope"
(r_path,["Coq";"Reals";"Rdefinitions"])
r_of_int
- ([GRef (Loc.ghost,glob_IZR,None)],
+ ([CAst.make @@ GRef (glob_IZR, None)],
uninterp_r,
false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index de0fa77ef..b7f13b040 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -33,23 +33,23 @@ let glob_EmptyString = lazy (make_reference "EmptyString")
open Lazy
-let interp_string dloc s =
+let interp_string ?loc s =
let le = String.length s in
let rec aux n =
- if n = le then GRef (dloc, force glob_EmptyString, None) else
- GApp (dloc,GRef (dloc, force glob_String, None),
- [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
+ if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+ CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None),
+ [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
in aux 0
let uninterp_string r =
try
let b = Buffer.create 16 in
let rec aux = function
- | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) ->
+ | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) ->
(match uninterp_ascii a with
| Some c -> Buffer.add_char b (Char.chr c); aux s
| _ -> raise Non_closed_string)
- | GRef (_,z,_) when eq_gr z (force glob_EmptyString) ->
+ | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
Some (Buffer.contents b)
| _ ->
raise Non_closed_string
@@ -61,6 +61,6 @@ let _ =
Notation.declare_string_interpreter "string_scope"
(string_path,["Coq";"Strings";"String"])
interp_string
- ([GRef (Loc.ghost,static_glob_String,None);
- GRef (Loc.ghost,static_glob_EmptyString,None)],
+ ([CAst.make @@ GRef (static_glob_String,None);
+ CAst.make @@ GRef (static_glob_EmptyString,None)],
uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index b7b5fb8a5..479448e06 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -44,35 +44,36 @@ 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 = CAst.make ?loc @@ GRef (glob_xI, None) in
+ let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in
+ let ref_xO = CAst.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) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> CAst.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 ~hdr:"interp_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 rec bignat_of_pos x = CAst.with_val (function
+ | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+ | GApp ({ CAst.v = 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
| _ -> raise Non_closed_number
+ ) x
let uninterp_positive p =
try
@@ -87,9 +88,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)],
+ ([CAst.make @@ GRef (glob_xI, None);
+ CAst.make @@ GRef (glob_xO, None);
+ CAst.make @@ GRef (glob_xH, None)],
uninterp_positive,
true)
@@ -106,27 +107,28 @@ 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 = CAst.make ?loc @@
if not (Bigint.equal n zero) then
- GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n])
+ GApp(CAst.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 ~hdr:"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 = CAst.with_val (function
+ | GApp ({ CAst.v = 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
| _ -> raise Non_closed_number
+ )
let uninterp_n p =
try Some (bignat_of_n p)
@@ -138,8 +140,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)],
+ ([CAst.make @@ GRef (glob_N0, None);
+ CAst.make @@ GRef (glob_Npos, None)],
uninterp_n,
true)
@@ -157,23 +159,24 @@ 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])
+ CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
else
- GRef (dloc, glob_ZERO, None)
+ CAst.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 = CAst.with_val (function
+ | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+ | GApp ({ CAst.v = 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
| _ -> raise Non_closed_number
+ )
let uninterp_z p =
try
@@ -186,8 +189,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)],
+ ([CAst.make @@ GRef (glob_ZERO, None);
+ CAst.make @@ GRef (glob_POS, None);
+ CAst.make @@ GRef (glob_NEG, None)],
uninterp_z,
true)