From 412f848e681e3c94c635f65638310a13d675449e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Mar 2014 00:03:37 +0100 Subject: Removing generic equality in Syntax plugin. --- plugins/syntax/nat_syntax.ml | 4 ++-- plugins/syntax/numbers_syntax.ml | 18 +++++++++--------- plugins/syntax/string_syntax.ml | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 59180be81..c3dad0a10 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -50,8 +50,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) - | GRef (_,z) when z = glob_O -> zero + | 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 let uninterp_nat p = diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index b8c2b33fd..8e09c974a 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -110,12 +110,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur) - | (GRef (_,b))::l when 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 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 = @@ -199,14 +199,14 @@ let interp_bigN dloc n = let bigint_of_word = let rec get_height rc = match rc with - | GApp (_,GRef(_,c), [_;lft;rght]) when 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 c = zn2z_W0-> zero - | GApp (_,GRef(_,c), [_;lft;rght]) when 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)) @@ -262,8 +262,8 @@ let interp_bigZ dloc n = (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg - | GApp (_, GRef(_,c), [one_arg]) when 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 @@ -294,7 +294,7 @@ let interp_bigQ dloc n = let uninterp_bigQ rc = try match rc with - | GApp (_, GRef(_,c), [one_arg]) when 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 diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c9767a975..54206b453 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -41,11 +41,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | GApp (_,GRef (_,k),[a;s]) when 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 z = force glob_EmptyString -> + | GRef (_,z) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string -- cgit v1.2.3