summaryrefslogtreecommitdiff
path: root/contrib/cc/ccalgo.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cc/ccalgo.ml')
-rw-r--r--contrib/cc/ccalgo.ml307
1 files changed, 207 insertions, 100 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index 8bdae54b..e67797e4 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccalgo.ml 10579 2008-02-21 13:54:00Z corbinea $ *)
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
@@ -16,13 +16,16 @@ open Pp
open Goptions
open Names
open Term
+open Tacmach
+open Evd
+open Proof_type
let init_size=5
let cc_verbose=ref false
-let debug msg (stdpp:std_ppcmds) =
- if !cc_verbose then msg stdpp
+let debug f x =
+ if !cc_verbose then f x
let _=
let gdopt=
@@ -97,7 +100,8 @@ type cinfo=
type term=
Symb of constr
- | Eps
+ | Product of sorts_family * sorts_family
+ | Eps of identifier
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -122,14 +126,19 @@ type equality = rule eq
type disequality = from eq
+type patt_kind =
+ Normal
+ | Trivial of types
+ | Creates_variables
+
type quant_eq =
{qe_hyp_id: identifier;
qe_pol: bool;
qe_nvars:int;
qe_lhs: ccpattern;
- qe_lhs_valid:bool;
+ qe_lhs_valid:patt_kind;
qe_rhs: ccpattern;
- qe_rhs_valid:bool}
+ qe_rhs_valid:patt_kind}
let swap eq : equality =
let swap_rule=match eq.rule with
@@ -145,10 +154,11 @@ type inductive_status =
| Total of (int * pa_constructor)
type representative=
- {mutable nfathers:int;
+ {mutable weight:int;
mutable lfathers:Intset.t;
mutable fathers:Intset.t;
mutable inductive_status: inductive_status;
+ class_type : Term.types;
mutable functions: Intset.t PafMap.t;
mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
@@ -179,9 +189,11 @@ type state =
mutable diseq: disequality list;
mutable quant: quant_eq list;
mutable pa_classes: Intset.t;
- q_history: (constr,unit) Hashtbl.t;
+ q_history: (identifier,int array) Hashtbl.t;
mutable rew_depth:int;
- mutable changed:bool}
+ mutable changed:bool;
+ by_type: (types,Intset.t) Hashtbl.t;
+ mutable gls:Proof_type.goal Tacmach.sigma}
let dummy_node =
{clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
@@ -189,7 +201,7 @@ let dummy_node =
vertex=Leaf;
term=Symb (mkRel min_int)}
-let empty depth:state =
+let empty depth gls:state =
{uf=
{max_size=init_size;
size=0;
@@ -206,7 +218,9 @@ let empty depth:state =
pa_classes=Intset.empty;
q_history=Hashtbl.create init_size;
rew_depth=depth;
- changed=false}
+ by_type=Hashtbl.create init_size;
+ changed=false;
+ gls=gls}
let forest state = state.uf
@@ -233,7 +247,7 @@ let get_constructor_info uf i=
| _ -> anomaly "get_constructor: not a constructor"
let size uf i=
- (get_representative uf i).nfathers
+ (get_representative uf i).weight
let axioms uf = uf.axioms
@@ -241,13 +255,13 @@ let epsilons uf = uf.epsilons
let add_lfather uf i t=
let r=get_representative uf i in
- r.nfathers<-r.nfathers+1;
+ r.weight<-r.weight+1;
r.lfathers<-Intset.add t r.lfathers;
r.fathers <-Intset.add t r.fathers
let add_rfather uf i t=
let r=get_representative uf i in
- r.nfathers<-r.nfathers+1;
+ r.weight<-r.weight+1;
r.fathers <-Intset.add t r.fathers
exception Discriminable of int * pa_constructor * int * pa_constructor
@@ -295,19 +309,29 @@ let next uf=
uf.size<-nsize;
size
-let new_representative ()=
- {nfathers=0;
+let new_representative typ =
+ {weight=0;
lfathers=Intset.empty;
fathers=Intset.empty;
inductive_status=Unknown;
+ class_type=typ;
functions=PafMap.empty;
constructors=PacMap.empty}
(* rebuild a constr from an applicative term *)
+let _A_ = Name (id_of_string "A")
+let _B_ = Name (id_of_string "A")
+let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
+
+let cc_product s1 s2 =
+ mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
+ mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
+
let rec constr_of_term = function
Symb s->s
- | Eps -> anomaly "epsilon constant has no value"
+ | Product(s1,s2) -> cc_product s1 s2
+ | Eps id -> mkVar id
| Constructor cinfo -> mkConstruct cinfo.ci_constr
| Appli (s1,s2)->
make_app [(constr_of_term s2)] s1
@@ -330,24 +354,31 @@ let rec inst_pattern subst = function
(fun spat f -> Appli (f,inst_pattern subst spat))
args t
+let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
+ Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
+
+let pr_term t = str "[" ++
+ Termops.print_constr (constr_of_term t) ++ str "]"
+
let rec add_term state t=
let uf=state.uf in
try Hashtbl.find uf.syms t with
Not_found ->
let b=next uf in
+ let typ = pf_type_of state.gls (constr_of_term t) in
let new_node=
match t with
- Symb _ ->
+ Symb _ | Product (_,_) ->
let paf =
{fsym=b;
fnargs=0} in
Queue.add (b,Fmark paf) state.marks;
- {clas= Rep (new_representative ());
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Leaf;
term= t}
- | Eps ->
- {clas= Rep (new_representative ());
+ | Eps id ->
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Leaf;
term= t}
@@ -356,7 +387,7 @@ let rec add_term state t=
add_lfather uf (find uf i1) b;
add_rfather uf (find uf i2) b;
state.terms<-Intset.add b state.terms;
- {clas= Rep (new_representative ());
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Node(i1,i2);
term= t}
@@ -370,13 +401,17 @@ let rec add_term state t=
arity= cinfo.ci_arity;
args=[]} in
Queue.add (b,Cmark pac) state.marks;
- {clas=Rep (new_representative ());
+ {clas=Rep (new_representative typ);
cpath= -1;
vertex=Leaf;
term=t}
in
uf.map.(b)<-new_node;
Hashtbl.add uf.syms t b;
+ Hashtbl.replace state.by_type typ
+ (Intset.add b
+ (try Hashtbl.find state.by_type typ with
+ Not_found -> Intset.empty));
b
let add_equality state c s t=
@@ -400,32 +435,53 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
qe_rhs= patt2;
qe_rhs_valid=valid2}::state.quant
+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
+ List.exists
+ (fun old_args ->
+ Util.array_for_all2 (fun i j -> i = find state.uf j)
+ norm_args old_args)
+ prev_args
+ with Not_found -> false
+
let add_inst state (inst,int_subst) =
- if state.rew_depth > 0 then
- 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
- let _ = array_rev args in (* highest deBruijn index first *)
- let prf= mkApp(prfhead,args) in
- try Hashtbl.find state.q_history prf
- with Not_found ->
- (* this instance is new, we can go on *)
- let s = inst_pattern subst inst.qe_lhs
- and t = inst_pattern subst inst.qe_rhs in
- state.changed<-true;
- state.rew_depth<-pred state.rew_depth;
- if inst.qe_pol then
- begin
- debug msgnl
- (str "adding new equality, depth="++ int state.rew_depth);
- add_equality state prf s t
- end
- else
- begin
- debug msgnl (str "adding new disequality, depth="++
- int state.rew_depth);
- add_disequality state (Hyp prf) s t
- end
+ check_for_interrupt ();
+ if state.rew_depth > 0 then
+ if is_redundant state inst.qe_hyp_id int_subst then
+ debug msgnl (str "discarding redundant (dis)equality")
+ else
+ begin
+ Hashtbl.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
+ let _ = array_rev args in (* highest deBruijn index first *)
+ let prf= mkApp(prfhead,args) in
+ let s = inst_pattern subst inst.qe_lhs
+ and t = inst_pattern subst inst.qe_rhs in
+ state.changed<-true;
+ state.rew_depth<-pred state.rew_depth;
+ if inst.qe_pol then
+ begin
+ debug (fun () ->
+ msgnl
+ (str "Adding new equality, depth="++ int state.rew_depth);
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+ add_equality state prf s t
+ end
+ else
+ begin
+ debug (fun () ->
+ msgnl
+ (str "Adding new disequality, depth="++ int state.rew_depth);
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+ add_disequality state (Hyp prf) s t
+ end
+ end
let link uf i j eq = (* links i -> j *)
let node=uf.map.(i) in
@@ -448,12 +504,17 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug msgnl (str "Linking " ++ int i1 ++ str " and " ++ int i2 ++ str ".");
+ debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
+ str " and " ++ pr_idx_term state i2 ++ str ".")) ();
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
+ (Intset.remove i1
+ (try Hashtbl.find state.by_type r1.class_type with
+ Not_found -> Intset.empty));
let f= Intset.union r1.fathers r2.fathers in
- r2.nfathers<-Intset.cardinal f;
+ r2.weight<-Intset.cardinal f;
r2.fathers<-f;
r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
ST.delete_set state.sigtable r1.fathers;
@@ -483,8 +544,9 @@ let union state i1 i2 eq=
| _,_ -> ()
let merge eq state = (* merge and no-merge *)
- debug msgnl
- (str "Merging " ++ int eq.lhs ++ str " and " ++ int eq.rhs ++ str ".");
+ debug (fun () -> msgnl
+ (str "Merging " ++ pr_idx_term state eq.lhs ++
+ str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
let uf=state.uf in
let i=find uf eq.lhs
and j=find uf eq.rhs in
@@ -495,8 +557,8 @@ let merge eq state = (* merge and no-merge *)
union state j i (swap eq)
let update t state = (* update 1 and 2 *)
- debug msgnl
- (str "Updating term " ++ int t ++ str ".");
+ debug (fun () -> msgnl
+ (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
@@ -556,8 +618,8 @@ let process_constructor_mark t i rep pac state =
end
let process_mark t m state =
- debug msgnl
- (str "Processing mark for term " ++ int t ++ str ".");
+ debug (fun () -> msgnl
+ (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -573,9 +635,9 @@ let check_disequalities state =
let uf=state.uf in
let rec check_aux = function
dis::q ->
- debug msg
- (str "Checking if " ++ int dis.lhs ++ str " = " ++
- int dis.rhs ++ str " ... ");
+ debug (fun () -> msg
+ (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+ pr_idx_term state dis.rhs ++ str " ... ")) ();
if find uf dis.lhs=find uf dis.rhs then
begin debug msgnl (str "Yes");Some dis end
else
@@ -601,16 +663,35 @@ let one_step state =
update t state;
true
with Not_found -> false
-
+
+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}};
+ id
let complete_one_class state i=
match (get_representative state.uf i).inductive_status with
Partial pac ->
- let rec app t n =
+ let rec app t typ n =
if n<=0 then t else
- app (Appli(t,Eps)) (n-1) in
+ let _,etyp,rest= destProd typ in
+ let id = new_state_var etyp state in
+ app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+ let _c = pf_type_of state.gls
+ (constr_of_term (term state.uf pac.cnode)) in
+ let _args =
+ List.map (fun i -> constr_of_term (term state.uf i))
+ pac.args in
+ let typ = prod_applist _c (List.rev _args) in
+ let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
- ignore (add_term state (app (term state.uf i) pac.arity))
+ ignore (add_term state ct)
| _ -> anomaly "wrong incomplete class"
let complete state =
@@ -624,18 +705,18 @@ type matching_problem =
let make_fun_table state =
let uf= state.uf in
let funtab=ref PafMap.empty in
- for cl=0 to pred uf.size do
- match uf.map.(cl).clas with
- Rep rep ->
- PafMap.iter
- (fun paf _ ->
- let elem =
- try PafMap.find paf !funtab
- with Not_found -> Intset.empty in
- funtab:= PafMap.add paf (Intset.add cl elem) !funtab)
- rep.functions
- | _ -> ()
- done;
+ Array.iteri
+ (fun i inode -> if i < uf.size then
+ match inode.clas with
+ Rep rep ->
+ PafMap.iter
+ (fun paf _ ->
+ let elem =
+ try PafMap.find paf !funtab
+ with Not_found -> Intset.empty in
+ funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+ rep.functions
+ | _ -> ()) state.uf.map;
!funtab
@@ -656,6 +737,7 @@ let rec do_match state res pb_stack =
else
if mp.mp_subst.(pred i) = cl then
Stack.push {mp with mp_stack=remains} pb_stack
+ else (* mismatch for non-linear variable in pattern *) ()
| PApp (f,[]) ->
begin
try let j=Hashtbl.find uf.syms f in
@@ -665,19 +747,19 @@ let rec do_match state res pb_stack =
end
| PApp(f, ((last_arg::rem_args) as args)) ->
try
- let j=Hashtbl.find uf.syms f in
+ let j=Hashtbl.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
let aux i =
- let (s,t) = ST.rev_query i state.sigtable in
+ let (s,t) = signature state.uf i in
Stack.push
{mp with
mp_subst=Array.copy mp.mp_subst;
mp_stack=
(PApp(f,rem_args),s) ::
(last_arg,t) :: remains} pb_stack in
- Intset.iter aux good_terms
+ Intset.iter aux good_terms
with Not_found -> ()
let paf_of_patt syms = function
@@ -692,28 +774,50 @@ let init_pb_stack state =
let funtab = make_fun_table state in
let aux inst =
begin
- if inst.qe_lhs_valid then
- try
- let paf= paf_of_patt syms inst.qe_lhs in
- let good_classes = PafMap.find paf funtab in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
- mp_inst=inst;
- mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
- with Not_found -> ()
+ let good_classes =
+ match inst.qe_lhs_valid with
+ Creates_variables -> Intset.empty
+ | Normal ->
+ begin
+ try
+ let paf= paf_of_patt syms inst.qe_lhs in
+ PafMap.find paf funtab
+ with Not_found -> Intset.empty
+ end
+ | Trivial typ ->
+ begin
+ try
+ Hashtbl.find state.by_type typ
+ with Not_found -> Intset.empty
+ end in
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
+ mp_inst=inst;
+ mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
end;
begin
- if inst.qe_rhs_valid then
- try
- let paf= paf_of_patt syms inst.qe_rhs in
- let good_classes = PafMap.find paf funtab in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
- mp_inst=inst;
- mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
- with Not_found -> ()
+ let good_classes =
+ match inst.qe_rhs_valid with
+ Creates_variables -> Intset.empty
+ | Normal ->
+ begin
+ try
+ let paf= paf_of_patt syms inst.qe_rhs in
+ PafMap.find paf funtab
+ with Not_found -> Intset.empty
+ end
+ | Trivial typ ->
+ begin
+ try
+ Hashtbl.find state.by_type typ
+ with Not_found -> Intset.empty
+ end in
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
+ mp_inst=inst;
+ mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
end in
List.iter aux state.quant;
pb_stack
@@ -724,7 +828,8 @@ let find_instances state =
let _ =
debug msgnl (str "Running E-matching algorithm ... ");
try
- while true do
+ while true do
+ check_for_interrupt ();
do_match state res pb_stack
done;
anomaly "get out of here !"
@@ -734,7 +839,9 @@ let find_instances state =
let rec execute first_run state =
debug msgnl (str "Executing ... ");
try
- while one_step state do ()
+ while
+ check_for_interrupt ();
+ one_step state do ()
done;
match check_disequalities state with
None ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 19:33:50 +0000