summaryrefslogtreecommitdiff
path: root/plugins/cc/ccalgo.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r--plugins/cc/ccalgo.ml99
1 files changed, 68 insertions, 31 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 3c40cfb9..1c021eee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
@@ -30,6 +28,7 @@ let debug f x =
let _=
let gdopt=
{ optsync=true;
+ optdepr=false;
optname="Congruence Verbose";
optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
@@ -105,6 +104,26 @@ type term=
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
+let rec term_equal t1 t2 =
+ match t1, t2 with
+ | Symb c1, Symb c2 -> eq_constr c1 c2
+ | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
+ | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+ | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
+ | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
+ Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
+ i1 = i2 && j1 = j2 && eq_constructor c1 c2
+ | _ -> t1 = t2
+
+open Hashtbl_alt.Combine
+
+let rec hash_term = function
+ | Symb c -> combine 1 (hash_constr c)
+ | Product (s1, s2) -> combine3 2 (Hashtbl.hash s1) (Hashtbl.hash s2)
+ | Eps i -> combine 3 (Hashtbl.hash i)
+ | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
+ | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (Hashtbl.hash c) i j
+
type ccpattern =
PApp of term * ccpattern list (* arguments are reversed *)
| PVar of int
@@ -172,13 +191,32 @@ type node =
vertex:vertex;
term:term}
+module Constrhash = Hashtbl.Make
+ (struct type t = constr
+ let equal = eq_constr
+ let hash = hash_constr
+ end)
+module Typehash = Constrhash
+
+module Termhash = Hashtbl.Make
+ (struct type t = term
+ let equal = term_equal
+ let hash = hash_term
+ end)
+
+module Identhash = Hashtbl.Make
+ (struct type t = identifier
+ let equal = Pervasives.(=)
+ let hash = Hashtbl.hash
+ end)
+
type forest=
{mutable max_size:int;
mutable size:int;
mutable map: node array;
- axioms: (constr,term*term) Hashtbl.t;
+ axioms: (term*term) Constrhash.t;
mutable epsilons: pa_constructor list;
- syms:(term,int) Hashtbl.t}
+ syms: int Termhash.t}
type state =
{uf: forest;
@@ -189,10 +227,10 @@ type state =
mutable diseq: disequality list;
mutable quant: quant_eq list;
mutable pa_classes: Intset.t;
- q_history: (identifier,int array) Hashtbl.t;
+ q_history: (int array) Identhash.t;
mutable rew_depth:int;
mutable changed:bool;
- by_type: (types,Intset.t) Hashtbl.t;
+ by_type: Intset.t Typehash.t;
mutable gls:Proof_type.goal Tacmach.sigma}
let dummy_node =
@@ -207,8 +245,8 @@ let empty depth gls:state =
size=0;
map=Array.create init_size dummy_node;
epsilons=[];
- axioms=Hashtbl.create init_size;
- syms=Hashtbl.create init_size};
+ axioms=Constrhash.create init_size;
+ syms=Termhash.create init_size};
terms=Intset.empty;
combine=Queue.create ();
marks=Queue.create ();
@@ -216,9 +254,9 @@ let empty depth gls:state =
diseq=[];
quant=[];
pa_classes=Intset.empty;
- q_history=Hashtbl.create init_size;
+ q_history=Identhash.create init_size;
rew_depth=depth;
- by_type=Hashtbl.create init_size;
+ by_type=Constrhash.create init_size;
changed=false;
gls=gls}
@@ -366,7 +404,8 @@ let rec canonize_name c =
let build_subst uf subst =
Array.map (fun i ->
try term uf i
- with _ -> anomaly "incomplete matching") subst
+ with e when Errors.noncritical e ->
+ anomaly "incomplete matching") subst
let rec inst_pattern subst = function
PVar i ->
@@ -384,7 +423,7 @@ let pr_term t = str "[" ++
let rec add_term state t=
let uf=state.uf in
- try Hashtbl.find uf.syms t with
+ try Termhash.find uf.syms t with
Not_found ->
let b=next uf in
let typ = pf_type_of state.gls (constr_of_term t) in
@@ -430,10 +469,10 @@ let rec add_term state t=
term=t}
in
uf.map.(b)<-new_node;
- Hashtbl.add uf.syms t b;
- Hashtbl.replace state.by_type typ
+ Termhash.add uf.syms t b;
+ Typehash.replace state.by_type typ
(Intset.add b
- (try Hashtbl.find state.by_type typ with
+ (try Typehash.find state.by_type typ with
Not_found -> Intset.empty));
b
@@ -441,7 +480,7 @@ let add_equality state c s t=
let i = add_term state s in
let j = add_term state t in
Queue.add {lhs=i;rhs=j;rule=Axiom(c,false)} state.combine;
- Hashtbl.add state.uf.axioms c (s,t)
+ Constrhash.add state.uf.axioms c (s,t)
let add_disequality state from s t =
let i = add_term state s in
@@ -461,7 +500,7 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
let is_redundant state id args =
try
let norm_args = Array.map (find state.uf) args in
- let prev_args = Hashtbl.find_all state.q_history id in
+ let prev_args = Identhash.find_all state.q_history id in
List.exists
(fun old_args ->
Util.array_for_all2 (fun i j -> i = find state.uf j)
@@ -476,7 +515,7 @@ let add_inst state (inst,int_subst) =
debug msgnl (str "discarding redundant (dis)equality")
else
begin
- Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
+ Identhash.add state.q_history inst.qe_hyp_id int_subst;
let subst = build_subst (forest state) int_subst in
let prfhead= mkVar inst.qe_hyp_id in
let args = Array.map constr_of_term subst in
@@ -532,9 +571,9 @@ let union state i1 i2 eq=
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
- Hashtbl.replace state.by_type r1.class_type
+ Constrhash.replace state.by_type r1.class_type
(Intset.remove i1
- (try Hashtbl.find state.by_type r1.class_type with
+ (try Constrhash.find state.by_type r1.class_type with
Not_found -> Intset.empty));
let f= Intset.union r1.fathers r2.fathers in
r2.weight<-Intset.cardinal f;
@@ -691,11 +730,9 @@ let __eps__ = id_of_string "_eps_"
let new_state_var typ state =
let id = pf_get_new_id __eps__ state.gls in
- state.gls<-
- {state.gls with it =
- {state.gls.it with evar_hyps =
- Environ.push_named_context_val (id,None,typ)
- state.gls.it.evar_hyps}};
+ let {it=gl ; sigma=sigma} = state.gls in
+ let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
+ state.gls<- gls;
id
let complete_one_class state i=
@@ -763,14 +800,14 @@ let rec do_match state res pb_stack =
else (* mismatch for non-linear variable in pattern *) ()
| PApp (f,[]) ->
begin
- try let j=Hashtbl.find uf.syms f in
+ try let j=Termhash.find uf.syms f in
if find uf j =cl then
Stack.push {mp with mp_stack=remains} pb_stack
with Not_found -> ()
end
| PApp(f, ((last_arg::rem_args) as args)) ->
try
- let j=Hashtbl.find uf.syms f in
+ let j=Termhash.find uf.syms f in
let paf={fsym=j;fnargs=List.length args} in
let rep=get_representative uf cl in
let good_terms = PafMap.find paf rep.functions in
@@ -788,7 +825,7 @@ let rec do_match state res pb_stack =
let paf_of_patt syms = function
PVar _ -> invalid_arg "paf_of_patt: pattern is trivial"
| PApp (f,args) ->
- {fsym=Hashtbl.find syms f;
+ {fsym=Termhash.find syms f;
fnargs=List.length args}
let init_pb_stack state =
@@ -810,7 +847,7 @@ let init_pb_stack state =
| Trivial typ ->
begin
try
- Hashtbl.find state.by_type typ
+ Typehash.find state.by_type typ
with Not_found -> Intset.empty
end in
Intset.iter (fun i ->
@@ -833,7 +870,7 @@ let init_pb_stack state =
| Trivial typ ->
begin
try
- Hashtbl.find state.by_type typ
+ Typehash.find state.by_type typ
with Not_found -> Intset.empty
end in
Intset.iter (fun i ->
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-12 10:33:06 +0000