From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 14:23:53 +0100 Subject: [location] Switch glob_constr to Loc.located --- plugins/syntax/ascii_syntax.ml | 14 +++---- plugins/syntax/nat_syntax.ml | 17 ++++---- plugins/syntax/numbers_syntax.ml | 84 ++++++++++++++++++++-------------------- plugins/syntax/r_syntax.ml | 32 +++++++-------- plugins/syntax/string_syntax.ml | 16 ++++---- plugins/syntax/z_syntax.ml | 56 +++++++++++++-------------- 6 files changed, 110 insertions(+), 109 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index ed8cc6ab0..dc0b87793 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,13 +37,13 @@ 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) + (Loc.tag ~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) + Loc.tag ~loc @@ GApp (Loc.tag ~loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string dloc s = let p = @@ -59,12 +59,12 @@ let interp_ascii_string dloc s = 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) + | (_, 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) | _ -> 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 + | _, GApp ((_, 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) + ([Loc.tag @@ 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..90d643b7f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -33,14 +33,14 @@ 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 = Loc.tag ~loc @@ GRef (glob_O, None) in + let ref_S = Loc.tag ~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 (Loc.tag ~loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -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 = Loc.with_unloc (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 | _ -> 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) + ([Loc.tag @@ GRef (glob_S,None); Loc.tag @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index a25ddb062..8876d464a 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 = Loc.tag ~loc @@ GRef (int31_construct, None) in + let ref_0 = Loc.tag ~loc @@ GRef (int31_0, None) in + let ref_1 = Loc.tag ~loc @@ GRef (int31_1, None) in let rec args counter n = if counter <= 0 then [] @@ -97,7 +97,7 @@ 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)) + Loc.tag ~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.") @@ -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)) + | (_, 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)) | _ -> raise Non_closed in function - | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero + | _, GApp ((_, 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)], + ([Loc.tag @@ GRef (int31_construct, None)], uninterp_int31, true) @@ -162,34 +162,34 @@ 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 = Loc.tag ~loc @@ GRef (zn2z_W0, None) in + let ref_WW = Loc.tag ~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)]) + Loc.tag ~loc @@ GApp (ref_W0, [Loc.tag ~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); + Loc.tag ~loc @@ GApp (ref_WW, [Loc.tag ~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 = Loc.tag ~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) + Loc.tag ~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 = if is_pos_or_zero n then @@ -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 -> + | _, GApp ((_, 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-> + | _, GApp ((_, GRef(c,_)),_) when eq_gr c zn2z_W0-> zero + | _, GApp ((_, 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 + | _, GApp (_,[one_arg]) -> bigint_of_word one_arg + | _, 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)) + (Loc.tag @@ 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 = Loc.tag ~loc @@ GRef (bigZ_pos, None) in + let ref_neg = Loc.tag ~loc @@ GRef (bigZ_neg, None) in if is_pos_or_zero n then - GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) + Loc.tag ~loc @@ GApp (ref_pos, [bigN_of_pos_bigint loc n]) else - GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) + Loc.tag ~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 -> + | _, 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 -> 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)], + ([Loc.tag @@ GRef (bigZ_pos, None); + Loc.tag @@ 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 = Loc.tag ~loc @@ GRef (bigQ_z, None) in + Loc.tag ~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 -> + | _, GApp ((_, 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, + ([Loc.tag @@ GRef (bigQ_z, None)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 8f065f528..1af3f6c5b 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -42,13 +42,13 @@ 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 ref_xI = Loc.tag @@ GRef (glob_xI, None) in + let ref_xH = Loc.tag @@ GRef (glob_xH, None) in + let ref_xO = Loc.tag @@ 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) -> Loc.tag @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> Loc.tag @@ 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 + | _, 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 | _ -> raise Non_closed_number (**********************************************************************) @@ -81,18 +81,18 @@ let z_of_int dloc 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]) + Loc.tag @@ GApp(Loc.tag @@ GRef (sgn,None), [pos_of_bignat dloc n]) else - GRef (dloc, glob_ZERO, None) + Loc.tag @@ 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 + | _, 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 | _ -> raise Non_closed_number (**********************************************************************) @@ -108,14 +108,14 @@ 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]) + Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int dloc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) let bigint_of_r = function - | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR -> + | _, GApp ((_, 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)], + ([Loc.tag @@ GRef (glob_IZR,None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index de0fa77ef..539670722 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 Loc.tag ~loc @@ GRef (force glob_EmptyString, None) else + Loc.tag ~loc @@ GApp (Loc.tag ~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) -> + | _, GApp ((_, 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) -> + | _, 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)], + ([Loc.tag @@ GRef (static_glob_String,None); + Loc.tag @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index b7b5fb8a5..a00525f91 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -44,14 +44,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 = Loc.tag ~loc @@ GRef (glob_xI, None) in + let ref_xH = Loc.tag ~loc @@ GRef (glob_xH, None) in + let ref_xO = Loc.tag ~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) -> Loc.tag ~loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> Loc.tag ~loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -69,9 +69,9 @@ let interp_positive dloc n = (**********************************************************************) 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 + | _, 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 | _ -> raise Non_closed_number let uninterp_positive p = @@ -87,9 +87,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)], + ([Loc.tag @@ GRef (glob_xI, None); + Loc.tag @@ GRef (glob_xO, None); + Loc.tag @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -106,11 +106,11 @@ 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 = Loc.tag ~loc @@ if not (Bigint.equal n zero) then - GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n]) + GApp(Loc.tag @@ 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\".") @@ -124,8 +124,8 @@ let n_of_int dloc n = (**********************************************************************) 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 + | _, 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 | _ -> raise Non_closed_number let uninterp_n p = @@ -138,8 +138,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)], + ([Loc.tag @@ GRef (glob_N0, None); + Loc.tag @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -157,22 +157,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]) + Loc.tag ~loc @@ GApp(Loc.tag ~loc @@ GRef(sgn,None), [pos_of_bignat loc n]) else - GRef (dloc, glob_ZERO, None) + Loc.tag ~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 + | _, 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 | _ -> raise Non_closed_number let uninterp_z p = @@ -186,8 +186,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)], + ([Loc.tag @@ GRef (glob_ZERO, None); + Loc.tag @@ GRef (glob_POS, None); + Loc.tag @@ GRef (glob_NEG, None)], uninterp_z, true) -- cgit v1.2.3