diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/cc/ccalgo.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/cc/ccalgo.ml')
-rw-r--r-- | contrib/cc/ccalgo.ml | 357 |
1 files changed, 357 insertions, 0 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml new file mode 100644 index 00000000..e73a6221 --- /dev/null +++ b/contrib/cc/ccalgo.ml @@ -0,0 +1,357 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: ccalgo.ml,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *) + +(* This file implements the basic congruence-closure algorithm by *) +(* Downey,Sethi and Tarjan. *) + +open Util +open Names +open Term + +let init_size=251 + +type pa_constructor= + {head_constr: int; + arity:int; + nhyps:int; + args:int list; + term_head:int} + + +module PacMap=Map.Make(struct type t=int*int let compare=compare end) + +type term= + Symb of constr + | Appli of term*term + | Constructor of constructor*int*int (* constructor arity+ nhyps *) + +type rule= + Congruence + | Axiom of identifier + | Injection of int*int*int*int (* terms+head+arg position *) + +type equality = {lhs:int;rhs:int;rule:rule} + +let swap eq= + let swap_rule=match eq.rule with + Congruence -> Congruence + | Injection (i,j,c,a) -> Injection (j,i,c,a) + | Axiom id -> anomaly "no symmetry for axioms" + in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule} + +(* Signature table *) + +module ST=struct + + (* l: sign -> term r: term -> sign *) + + type t = {toterm:(int*int,int) Hashtbl.t; + tosign:(int,int*int) Hashtbl.t} + + let empty ()= + {toterm=Hashtbl.create init_size; + tosign=Hashtbl.create init_size} + + let enter t sign st= + if Hashtbl.mem st.toterm sign then + anomaly "enter: signature already entered" + else + Hashtbl.replace st.toterm sign t; + Hashtbl.replace st.tosign t sign + + let query sign st=Hashtbl.find st.toterm sign + + let delete t st= + try let sign=Hashtbl.find st.tosign t in + Hashtbl.remove st.toterm sign; + Hashtbl.remove st.tosign t + with + Not_found -> () + + let rec delete_list l st= + match l with + []->() + | t::q -> delete t st;delete_list q st + +end + +(* Basic Union-Find algo w/o path compression *) + +module UF = struct + +module IndMap=Map.Make(struct type t=inductive let compare=compare end) + + type representative= + {mutable nfathers:int; + mutable fathers:int list; + mutable constructors:pa_constructor PacMap.t; + mutable inductives:(int * int) IndMap.t} + + type cl = Rep of representative| Eqto of int*equality + + type vertex = Leaf| Node of (int*int) + + type node = + {clas:cl; + vertex:vertex; + term:term; + mutable node_constr: int PacMap.t} + + type t={mutable size:int; + map:(int,node) Hashtbl.t; + syms:(term,int) Hashtbl.t; + sigtable:ST.t} + + let empty ():t={size=0; + map=Hashtbl.create init_size; + syms=Hashtbl.create init_size; + sigtable=ST.empty ()} + + let rec find uf i= + match (Hashtbl.find uf.map i).clas with + Rep _ -> i + | Eqto (j,_) ->find uf j + + let get_representative uf i= + let node=Hashtbl.find uf.map i in + match node.clas with + Rep r ->r + | _ -> anomaly "get_representative: not a representative" + + let get_constructor uf i= + match (Hashtbl.find uf.map i).term with + Constructor (cstr,_,_)->cstr + | _ -> anomaly "get_constructor: not a constructor" + + + let fathers uf i= + (get_representative uf i).fathers + + let size uf i= + (get_representative uf i).nfathers + + let add_father uf i t= + let r=get_representative uf i in + r.nfathers<-r.nfathers+1; + r.fathers<-t::r.fathers + + let pac_map uf i= + (get_representative uf i).constructors + + let pac_arity uf i sg= + (PacMap.find sg (get_representative uf i).constructors).arity + + let add_node_pac uf i sg j= + let node=Hashtbl.find uf.map i in + if not (PacMap.mem sg node.node_constr) then + node.node_constr<-PacMap.add sg j node.node_constr + + let mem_node_pac uf i sg= + PacMap.find sg (Hashtbl.find uf.map i).node_constr + + exception Discriminable of int * int * int * int * t + + let add_pacs uf i pacs = + let rep=get_representative uf i in + let pending=ref [] and combine=ref [] in + let add_pac sg pac= + try + let opac=PacMap.find sg rep.constructors in + if (snd sg)>0 then () else + let tk=pac.term_head + and tl=opac.term_head in + let rec f n lk ll q= + if n > 0 then match (lk,ll) with + k::qk,l::ql-> + let eq= + {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)} + in f (n-1) qk ql (eq::q) + | _-> anomaly + "add_pacs : weird error in injection subterms merge" + else q in + combine:=f pac.nhyps pac.args opac.args !combine + with Not_found -> (* Still Unknown Constructor *) + rep.constructors <- PacMap.add sg pac rep.constructors; + pending:= + (fathers uf (find uf pac.term_head)) @rep.fathers@ !pending; + let (c,a)=sg in + if a=0 then + let (ind,_)=get_constructor uf c in + try + let th2,hc2=IndMap.find ind rep.inductives in + raise (Discriminable (pac.term_head,c,th2,hc2,uf)) + with Not_found -> + rep.inductives<- + IndMap.add ind (pac.term_head,c) rep.inductives in + PacMap.iter add_pac pacs; + !pending,!combine + + let term uf i=(Hashtbl.find uf.map i).term + + let subterms uf i= + match (Hashtbl.find uf.map i).vertex with + Node(j,k) -> (j,k) + | _ -> anomaly "subterms: not a node" + + let signature uf i= + let j,k=subterms uf i in (find uf j,find uf k) + + let nodes uf= (* cherche les noeuds binaires *) + Hashtbl.fold + (fun i node l-> + match node.vertex with + Node (_,_)->i::l + | _ ->l) uf.map [] + + let next uf= + let n=uf.size in uf.size<-n+1; n + + let new_representative pm im= + {nfathers=0; + fathers=[]; + constructors=pm; + inductives=im} + + let rec add uf t= + try Hashtbl.find uf.syms t with + Not_found -> + let b=next uf in + let new_node= + match t with + Symb s -> + {clas=Rep (new_representative PacMap.empty IndMap.empty); + vertex=Leaf;term=t;node_constr=PacMap.empty} + | Appli (t1,t2) -> + let i1=add uf t1 and i2=add uf t2 in + add_father uf (find uf i1) b; + add_father uf (find uf i2) b; + {clas=Rep (new_representative PacMap.empty IndMap.empty); + vertex=Node(i1,i2);term=t;node_constr=PacMap.empty} + | Constructor (c,a,n) -> + let pacs= + PacMap.add (b,a) + {head_constr=b;arity=a;nhyps=n;args=[];term_head=b} + PacMap.empty in + let inds= + if a=0 then + let (ind,_)=c in + IndMap.add ind (b,b) IndMap.empty + else IndMap.empty in + {clas=Rep (new_representative pacs inds); + vertex=Leaf;term=t;node_constr=PacMap.empty} + in + Hashtbl.add uf.map b new_node; + Hashtbl.add uf.syms t b; + b + + let link uf i j eq= (* links i -> j *) + let node=Hashtbl.find uf.map i in + Hashtbl.replace uf.map i {node with clas=Eqto (j,eq)} + + let union uf i1 i2 eq= + let r1= get_representative uf i1 + and r2= get_representative uf i2 in + link uf i1 i2 eq; + r2.nfathers<-r1.nfathers+r2.nfathers; + r2.fathers<-r1.fathers@r2.fathers; + add_pacs uf i2 r1.constructors + + let rec down_path uf i l= + match (Hashtbl.find uf.map i).clas with + Eqto(j,t)->down_path uf j (((i,j),t)::l) + | Rep _ ->l + + let rec min_path=function + ([],l2)->([],l2) + | (l1,[])->(l1,[]) + | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) + | cpl -> cpl + + let join_path uf i j= + assert (find uf i=find uf j); + min_path (down_path uf i [],down_path uf j []) + +end + +let rec combine_rec uf=function + []->[] + | t::pending-> + let combine=combine_rec uf pending in + let s=UF.signature uf t in + let u=snd (UF.subterms uf t) in + let f (c,a) pac pacs= + if a=0 then pacs else + let sg=(c,a-1) in + UF.add_node_pac uf t sg pac.term_head; + PacMap.add sg {pac with args=u::pac.args;term_head=t} pacs + in + let pacs=PacMap.fold f (UF.pac_map uf (fst s)) PacMap.empty in + let i=UF.find uf t in + let (p,c)=UF.add_pacs uf i pacs in + let combine2=(combine_rec uf p)@c@combine in + try {lhs=t;rhs=ST.query s uf.UF.sigtable;rule=Congruence}::combine2 with + Not_found-> + ST.enter t s uf.UF.sigtable;combine2 + +let rec process_rec uf=function + []->[] + | eq::combine-> + let pending=process_rec uf combine in + let i=UF.find uf eq.lhs + and j=UF.find uf eq.rhs in + if i=j then + pending + else + if (UF.size uf i)<(UF.size uf j) then + let l=UF.fathers uf i in + let (p,c)=UF.union uf i j eq in + let _ =ST.delete_list l uf.UF.sigtable in + let inj_pending=process_rec uf c in + inj_pending@p@l@pending + else + let l=UF.fathers uf j in + let (p,c)=UF.union uf j i (swap eq) in + let _ =ST.delete_list l uf.UF.sigtable in + let inj_pending=process_rec uf c in + inj_pending@p@l@pending + +let rec cc_rec uf=function + []->() + | pending-> + let combine=combine_rec uf pending in + let pending0=process_rec uf combine in + cc_rec uf pending0 + +let cc uf=cc_rec uf (UF.nodes uf) + +let rec make_uf=function + []->UF.empty () + | (ax,(t1,t2))::q-> + let uf=make_uf q in + let i1=UF.add uf t1 in + let i2=UF.add uf t2 in + let j1=UF.find uf i1 and j2=UF.find uf i2 in + if j1=j2 then uf else + let (_,inj_combine)= + UF.union uf j1 j2 {lhs=i1;rhs=i2;rule=Axiom ax} in + let _ = process_rec uf inj_combine in uf + +let add_one_diseq uf (t1,t2)=(UF.add uf t1,UF.add uf t2) + +let add_disaxioms uf disaxioms= + let f (id,cpl)=(id,add_one_diseq uf cpl) in + List.map f disaxioms + +let check_equal uf (i1,i2) = UF.find uf i1 = UF.find uf i2 + +let find_contradiction uf diseq = + List.find (fun (id,cpl) -> check_equal uf cpl) diseq + + |