From 5e6145c871eea1e94566b252b4bfc4cd752f42d5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 23 Oct 2013 22:17:07 +0000 Subject: cList: set-as-list functions are now with an explicit comparison git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/glob_term_to_relation.ml | 5 ++- plugins/funind/recdef.ml | 2 +- plugins/omega/omega.ml | 51 ++++++++++++++------------ plugins/romega/refl_omega.ml | 12 ++++-- 5 files changed, 40 insertions(+), 32 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 13816d1db..95aaf4518 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1587,7 +1587,7 @@ let prove_principle_for_gen Elim.h_decompose_and (mkVar hid); (fun g -> let new_hyps = pf_ids_of_hyps g in - tcc_list := List.rev (List.subtract new_hyps (hid::hyps)); + tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps)); if List.is_empty !tcc_list then begin diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 2cc203ed5..91ea714c1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -90,7 +90,7 @@ let combine_results in (* and then we flatten the map *) { result = List.concat pre_result; - to_avoid = List.union res1.to_avoid res2.to_avoid + to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid } @@ -711,7 +711,8 @@ and build_entry_lc_from_case env funname make_discr { result = List.concat (List.map (fun r -> r.result) results); to_avoid = - List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results + List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid) + [] results } and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 22e82035b..96a60424c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1276,7 +1276,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (Elim.h_decompose_and (mkVar hid)) (fun g -> let ids' = pf_ids_of_hyps g in - lid := List.rev (List.subtract ids' ids); + lid := List.rev (List.subtract Id.equal ids' ids); if List.is_empty !lid then lid := [hid]; tclIDTAC g ) diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 60887b451..cf1a7e6db 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -19,6 +19,7 @@ module type INT = sig type bigint + val equal : bigint -> bigint -> bool val less_than : bigint -> bigint -> bool val add : bigint -> bigint -> bigint val sub : bigint -> bigint -> bigint @@ -32,26 +33,26 @@ end let debug = ref false -module MakeOmegaSolver (Int:INT) = struct - -type bigint = Int.bigint -let (?) x y = Int.less_than y x -let (>=?) x y = Int.less_than y x || x = y -let (=?) = (=) -let (+) = Int.add -let (-) = Int.sub -let ( * ) = Int.mult -let (/) x y = fst (Int.euclid x y) -let (mod) x y = snd (Int.euclid x y) -let zero = Int.zero -let one = Int.one +module MakeOmegaSolver (I:INT) = struct + +type bigint = I.bigint +let (=?) = I.equal +let (?) x y = I.less_than y x +let (>=?) x y = I.less_than y x || x = y +let (+) = I.add +let (-) = I.sub +let ( * ) = I.mult +let (/) x y = fst (I.euclid x y) +let (mod) x y = snd (I.euclid x y) +let zero = I.zero +let one = I.one let two = one + one -let negone = Int.neg one -let abs x = if Int.less_than x zero then Int.neg x else x -let string_of_bigint = Int.to_string -let neg = Int.neg +let negone = I.neg one +let abs x = if I.less_than x zero then I.neg x else x +let string_of_bigint = I.to_string +let neg = I.neg (* To ensure that polymorphic (<) is not used mistakenly on big integers *) (* Warning: do not use (=) either on big int *) @@ -697,14 +698,16 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = | [] -> failwith "solve" in let s1,s2 = List.partition (fun (_,_,decomp,_) -> sign decomp) systems in - let s1' = - List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s1 in - let s2' = - List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s2 in + let remove_int (dep,ro,dc,pa) = + (Util.List.except Int.equal id dep,ro,dc,pa) + in + let s1' = List.map remove_int s1 in + let s2' = List.map remove_int s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in let (eq,id1,id2) = List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union relie1 relie2 + [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], + eq.id :: Util.List.union Int.equal relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) in let act,relie_on = solve all_solutions in diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 635fc366f..752fa4598 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -921,7 +921,7 @@ let add_stated_equations env tree = let rec get_eclatement env = function i :: r -> let l = try (get_equation env i).e_depends with Not_found -> [] in - List.union (List.rev l) (get_eclatement env r) + List.union Pervasives.(=) (List.rev l) (get_eclatement env r) | [] -> [] let select_smaller l = @@ -1207,12 +1207,16 @@ let resolution env full_reified_goal systems_list = (* recupere explicitement ces equations *) let equations = List.map (get_equation env) useful_equa_id in let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in - let l_hyps = id_concl :: List.remove id_concl l_hyps' in + let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in let useful_hyps = - List.map (fun id -> List.assoc id full_reified_goal) l_hyps in + List.map + (fun id -> List.assoc_f Names.Id.equal id full_reified_goal) l_hyps + in let useful_vars = let really_useful_vars = vars_of_equations equations in - let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in + let concl_vars = + vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal) + in really_useful_vars @@ concl_vars in (* variables a introduire *) -- cgit v1.2.3