diff options
Diffstat (limited to 'plugins/syntax/z_syntax.ml')
-rw-r--r-- | plugins/syntax/z_syntax.ml | 56 |
1 files changed, 28 insertions, 28 deletions
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) |