From 172ed0c8c5c66f22b17e07de792da41c3d925b77 Mon Sep 17 00:00:00 2001 From: puech Date: Fri, 29 Jul 2011 14:30:31 +0000 Subject: Ring: replaced various generic = on constr by eq_constr, destructors etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14375 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/ring/ring.ml | 44 +++++++++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 19 deletions(-) (limited to 'plugins/ring') diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 6dd2a0c6e..9a252dfb7 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -135,7 +135,7 @@ let mkLApp(fc,v) = mkApp(Lazy.force fc, v) module OperSet = Set.Make (struct type t = global_reference - let compare = (Pervasives.compare : t->t->int) + let compare = (RefOrdered.compare : t->t->int) end) type morph = @@ -377,8 +377,14 @@ Builds *) +module Constrhash = Hashtbl.Make + (struct type t = constr + let equal = eq_constr + let hash = hash_constr + end) + let build_spolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) (* aux creates the spolynom p by a recursive destructuration of c @@ -392,14 +398,14 @@ let build_spolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SPconst, [|th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -434,7 +440,7 @@ Builds *) let build_polynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -455,14 +461,14 @@ let build_polynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_Pconst, [|th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -498,7 +504,7 @@ Builds *) let build_aspolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) (* aux creates the aspolynom p by a recursive destructuration of c @@ -512,13 +518,13 @@ let build_aspolynom gl th lc = | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -552,7 +558,7 @@ Builds *) let build_apolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -572,14 +578,14 @@ let build_apolynom gl th lc = | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_APvar, [| path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -613,7 +619,7 @@ Builds *) let build_setpolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -634,14 +640,14 @@ let build_setpolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SetPconst, [| th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -680,7 +686,7 @@ Builds *) let build_setspolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -692,14 +698,14 @@ let build_setspolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SetSPconst, [| th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in -- cgit v1.2.3