diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /plugins/cc/ccalgo.ml | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r-- | plugins/cc/ccalgo.ml | 98 |
1 files changed, 68 insertions, 30 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 3c40cfb9..e3d27f71 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-2010 *) (* \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} @@ -384,7 +422,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 +468,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 +479,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 +499,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 +514,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 +570,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 +729,11 @@ 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 new_hyps = + Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in + let gls = Goal.V82.new_goal_with sigma gl new_hyps in + state.gls<- gls; id let complete_one_class state i= @@ -763,14 +801,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 +826,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 +848,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 +871,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 -> |