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