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/romega/refl_omega.ml | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e8a72c055..635fc366f 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -38,6 +38,10 @@ type direction = Left of int | Right of int type occ_step = O_left | O_right | O_mono type occ_path = occ_step list +let occ_step_eq s1 s2 = match s1, s2 with +| O_left, O_left | O_right, O_right | O_mono, O_mono -> true +| _ -> false + (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) type occurence = {o_hyp : Names.Id.t; o_path : occ_path} @@ -209,7 +213,7 @@ let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars let unintern_omega env id = let rec loop = function [] -> failwith "unintern" - | ((t,j)::l) -> if id = j then t else loop l in + | ((t,j)::l) -> if Int.equal id j then t else loop l in loop env.om_vars (* \subsection{Gestion des environnements de variable pour la réflexion} @@ -484,8 +488,8 @@ let shuffle_path k1 e1 k2 e2 = let rec loop = function (({c=c1;v=v1}::l1) as l1'), (({c=c2;v=v2}::l2) as l2') -> - if v1 = v2 then - if k1*c1 + k2 * c2 = zero then ( + if Int.equal v1 v2 then + if Bigint.equal (k1 * c1 + k2 * c2) zero then ( Lazy.force coq_f_cancel :: loop (l1,l2)) else ( Lazy.force coq_f_equal :: loop (l1,l2) ) @@ -563,7 +567,7 @@ let reduce_factor = function let rec condense env = function Oplus(f1,(Oplus(f2,r) as t)) -> - if weight env f1 = weight env f2 then begin + if Int.equal (weight env f1) (weight env f2) then begin let shrink_tac,t = shrink_pair f1 f2 in let assoc_tac = Lazy.force coq_c_plus_assoc_l in let tac_list,t' = condense env (Oplus(t,r)) in @@ -577,7 +581,7 @@ let rec condense env = function let tac,f1' = reduce_factor f1 in [do_left (do_list tac)],Oplus(f1',Oint n) | Oplus(f1,f2) -> - if weight env f1 = weight env f2 then begin + if Int.equal (weight env f1) (weight env f2) then begin let tac_shrink,t = shrink_pair f1 f2 in let tac,t' = condense env t in tac_shrink :: tac,t' @@ -595,12 +599,12 @@ let rec condense env = function (* \subsection{Elimination des zéros} *) let rec clear_zero = function - Oplus(Omult(Oatom v,Oint n),r) when n=zero -> + Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero -> let tac',t = clear_zero r in Lazy.force coq_c_red5 :: tac',t | Oplus(f,r) -> let tac,t = clear_zero r in - (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t) + (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t) | t -> [],t;; (* \subsection{Transformation des hypothèses} *) @@ -1014,10 +1018,10 @@ let rec solve_with_constraints all_solutions path = let find_path {o_hyp=id;o_path=p} env = let rec loop_path = function ([],l) -> Some l - | (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2) + | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2) | _ -> None in let rec loop_id i = function - CCHyp{o_hyp=id';o_path=p'} :: l when id = id' -> + CCHyp{o_hyp=id';o_path=p'} :: l when Names.Id.equal id id' -> begin match loop_path (p',p) with Some r -> i,r | None -> loop_id (succ i) l @@ -1260,7 +1264,7 @@ let resolution env full_reified_goal systems_list = let i = List.index0 e.e_origin.o_hyp l_hyps in (* PL: it seems that additionnally introduced hyps are in the way during normalization, hence this index shifting... *) - if i=0 then 0 else Pervasives.(+) i (List.length to_introduce) + if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) in app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in let normalization_trace = -- cgit v1.2.3