From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/syntax/ascii_syntax.ml | 16 ++++++++-------- plugins/syntax/r_syntax.ml | 24 ++++++++++++------------ plugins/syntax/z_syntax.ml | 22 +++++++++++----------- 3 files changed, 31 insertions(+), 31 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 180d15009..790e1970b 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -35,17 +35,17 @@ open Lazy let interp_ascii dloc p = let rec aux n p = - if n = 0 then [] else + if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,if mp = 0 then glob_false else glob_true) + GRef (dloc,if Int.equal mp 0 then glob_false else glob_true) :: (aux (n-1) (p/2)) in GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p) let interp_ascii_string dloc s = let p = - if String.length s = 1 then int_of_char s.[0] + if Int.equal (String.length s) 1 then int_of_char s.[0] else - if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] + 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,"interp_ascii_string", @@ -54,13 +54,13 @@ let interp_ascii_string dloc s = let uninterp_ascii r = let rec uninterp_bool_list n = function - | [] when n = 0 -> 0 - | GRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) + | [] 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) | _ -> raise Non_closed_ascii in try let aux = function - | GApp (_,GRef (_,k),l) when 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 diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index efbd140ee..545f205db 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -55,7 +55,7 @@ let r_of_posint dloc n = let (q,r) = div2_with_rest n in let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in - if n <> zero then r_of_pos n else GRef(dloc,glob_R0) + if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0) let r_of_int dloc z = if is_strictly_neg z then @@ -72,34 +72,34 @@ let bignat_of_r = let rec bignat_of_pos = function (* 1+1 *) | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) - when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two + when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two (* 1+(1+1) *) | GApp (_,GRef (_,p1), [GRef (_,o1); GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) - when p1 = glob_Rplus && p2 = glob_Rplus && - o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three + when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && + Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three (* (1+1)*b *) - | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult -> - if bignat_of_pos a <> two then raise Non_closed_number; + | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult -> + if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) - when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1 -> - if bignat_of_pos a <> two then raise Non_closed_number; + when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> + if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number in let bignat_of_r = function - | GRef (_,a) when a = glob_R0 -> zero - | GRef (_,a) when a = glob_R1 -> one + | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero + | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | GApp (_,GRef (_,o), [a]) when o = glob_Ropp -> + | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp -> let n = bignat_of_r a in - if n = zero then raise Non_closed_number; + if Bigint.equal n zero then raise Non_closed_number; neg n | a -> bignat_of_r a diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index e5e4e9331..67e54c017 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -47,7 +47,7 @@ let pos_of_bignat dloc x = let rec pos_of x = match div2_with_rest x with | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) - | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -65,9 +65,9 @@ let interp_positive dloc n = (**********************************************************************) let rec bignat_of_pos = function - | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) - | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (_, a) when 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 = @@ -103,7 +103,7 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" let n_of_binnat dloc pos_or_neg n = - if n <> zero then + if not (Bigint.equal n zero) then GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n]) else GRef (dloc, glob_N0) @@ -120,8 +120,8 @@ let n_of_int dloc n = (**********************************************************************) let bignat_of_n = function - | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a - | GRef (_, a) when 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 = @@ -154,7 +154,7 @@ let glob_POS = ConstructRef path_of_POS let glob_NEG = ConstructRef path_of_NEG let z_of_int dloc n = - if n <> zero then + 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), [pos_of_bignat dloc n]) @@ -166,9 +166,9 @@ let z_of_int dloc n = (**********************************************************************) let bigint_of_z = function - | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a - | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (_, a) when 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 = -- cgit v1.2.3