diff options
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/ccalgo.ml | 378 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.mli | 55 | ||||
| -rw-r--r-- | contrib/cc/ccproof.ml | 7 | ||||
| -rw-r--r-- | contrib/cc/ccproof.mli | 9 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml | 148 | ||||
| -rw-r--r-- | contrib/cc/cctac.mli | 6 | ||||
| -rw-r--r-- | contrib/cc/g_congruence.ml4 | 16 |
7 files changed, 487 insertions, 132 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml index 3e2d11a2..8bdae54b 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 7298 2005-08-17 12:56:38Z corbinea $ *) +(* $Id: ccalgo.ml 9151 2006-09-19 13:32:22Z corbinea $ *) (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) @@ -55,6 +55,8 @@ module ST=struct Hashtbl.replace st.tosign t sign let query sign st=Hashtbl.find st.toterm sign + + let rev_query term st=Hashtbl.find st.tosign term let delete st t= try let sign=Hashtbl.find st.tosign t in @@ -72,10 +74,22 @@ type pa_constructor= arity : int; args : int list} +type pa_fun= + {fsym:int; + fnargs:int} + +type pa_mark= + Fmark of pa_fun + | Cmark of pa_constructor + module PacMap=Map.Make(struct type t=pa_constructor let compare=Pervasives.compare end) +module PafMap=Map.Make(struct + type t=pa_fun + let compare=Pervasives.compare end) + type cinfo= {ci_constr: constructor; (* inductive type *) ci_arity: int; (* # args *) @@ -87,16 +101,20 @@ type term= | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) +type ccpattern = + PApp of term * ccpattern list (* arguments are reversed *) + | PVar of int + type rule= Congruence - | Axiom of identifier * bool + | Axiom of constr * bool | Injection of int * pa_constructor * int * pa_constructor * int type from= Goal - | Hyp of identifier - | HeqG of identifier - | HeqnH of identifier * identifier + | Hyp of constr + | HeqG of constr + | HeqnH of constr * constr type 'a eq = {lhs:int;rhs:int;rule:'a} @@ -104,6 +122,15 @@ type equality = rule eq type disequality = from eq +type quant_eq = + {qe_hyp_id: identifier; + qe_pol: bool; + qe_nvars:int; + qe_lhs: ccpattern; + qe_lhs_valid:bool; + qe_rhs: ccpattern; + qe_rhs_valid:bool} + let swap eq : equality = let swap_rule=match eq.rule with Congruence -> Congruence @@ -122,6 +149,7 @@ type representative= mutable lfathers:Intset.t; mutable fathers:Intset.t; mutable inductive_status: inductive_status; + mutable functions: Intset.t PafMap.t; mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -138,7 +166,7 @@ type forest= {mutable max_size:int; mutable size:int; mutable map: node array; - axioms: (identifier,term*term) Hashtbl.t; + axioms: (constr,term*term) Hashtbl.t; mutable epsilons: pa_constructor list; syms:(term,int) Hashtbl.t} @@ -147,9 +175,13 @@ type state = sigtable:ST.t; mutable terms: Intset.t; combine: equality Queue.t; - marks: (int * pa_constructor) Queue.t; + marks: (int * pa_mark) Queue.t; mutable diseq: disequality list; - mutable pa_classes: Intset.t} + mutable quant: quant_eq list; + mutable pa_classes: Intset.t; + q_history: (constr,unit) Hashtbl.t; + mutable rew_depth:int; + mutable changed:bool} let dummy_node = {clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence}); @@ -157,7 +189,7 @@ let dummy_node = vertex=Leaf; term=Symb (mkRel min_int)} -let empty ():state = +let empty depth:state = {uf= {max_size=init_size; size=0; @@ -170,7 +202,11 @@ let empty ():state = marks=Queue.create (); sigtable=ST.empty (); diseq=[]; - pa_classes=Intset.empty} + quant=[]; + pa_classes=Intset.empty; + q_history=Hashtbl.create init_size; + rew_depth=depth; + changed=false} let forest state = state.uf @@ -221,11 +257,19 @@ let append_pac t p = let tail_pac p= {p with arity=succ p.arity;args=List.tl p.args} + +let fsucc paf = + {paf with fnargs=succ paf.fnargs} let add_pac rep pac t = if not (PacMap.mem pac rep.constructors) then rep.constructors<-PacMap.add pac t rep.constructors +let add_paf rep paf t = + let already = + try PafMap.find paf rep.functions with Not_found -> Intset.empty in + rep.functions<- PafMap.add paf (Intset.add t already) rep.functions + let term uf i=uf.map.(i).term let subterms uf i= @@ -256,8 +300,36 @@ let new_representative ()= lfathers=Intset.empty; fathers=Intset.empty; inductive_status=Unknown; + functions=PafMap.empty; constructors=PacMap.empty} +(* rebuild a constr from an applicative term *) + +let rec constr_of_term = function + Symb s->s + | Eps -> anomaly "epsilon constant has no value" + | Constructor cinfo -> mkConstruct cinfo.ci_constr + | Appli (s1,s2)-> + make_app [(constr_of_term s2)] s1 +and make_app l=function + Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 + | other -> applistc (constr_of_term other) l + +(* rebuild a term from a pattern and a substitution *) + +let build_subst uf subst = + Array.map (fun i -> + try term uf i + with _ -> anomaly "incomplete matching") subst + +let rec inst_pattern subst = function + PVar i -> + subst.(pred i) + | PApp (t, args) -> + List.fold_right + (fun spat f -> Appli (f,inst_pattern subst spat)) + args t + let rec add_term state t= let uf=state.uf in try Hashtbl.find uf.syms t with @@ -265,7 +337,16 @@ let rec add_term state t= let b=next uf in let new_node= match t with - Symb _ | Eps -> + Symb _ -> + let paf = + {fsym=b; + fnargs=0} in + Queue.add (b,Fmark paf) state.marks; + {clas= Rep (new_representative ()); + cpath= -1; + vertex= Leaf; + term= t} + | Eps -> {clas= Rep (new_representative ()); cpath= -1; vertex= Leaf; @@ -280,11 +361,15 @@ let rec add_term state t= vertex= Node(i1,i2); term= t} | Constructor cinfo -> + let paf = + {fsym=b; + fnargs=0} in + Queue.add (b,Fmark paf) state.marks; let pac = {cnode= b; arity= cinfo.ci_arity; args=[]} in - Queue.add (b,pac) state.marks; + Queue.add (b,Cmark pac) state.marks; {clas=Rep (new_representative ()); cpath= -1; vertex=Leaf; @@ -294,17 +379,54 @@ let rec add_term state t= Hashtbl.add uf.syms t b; b -let add_equality state id s t= +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(id,false)} state.combine; - Hashtbl.add state.uf.axioms id (s,t) + Queue.add {lhs=i;rhs=j;rule=Axiom(c,false)} state.combine; + Hashtbl.add state.uf.axioms c (s,t) let add_disequality state from s t = let i = add_term state s in let j = add_term state t in state.diseq<-{lhs=i;rhs=j;rule=from}::state.diseq +let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) = + state.quant<- + {qe_hyp_id= id; + qe_pol= pol; + qe_nvars=nvars; + qe_lhs= patt1; + qe_lhs_valid=valid1; + qe_rhs= patt2; + qe_rhs_valid=valid2}::state.quant + +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 + let link uf i j eq = (* links i -> j *) let node=uf.map.(i) in node.clas<-Eqto (j,eq); @@ -336,7 +458,13 @@ let union state i1 i2 eq= r2.lfathers<-Intset.union r1.lfathers r2.lfathers; ST.delete_set state.sigtable r1.fathers; state.terms<-Intset.union state.terms r1.fathers; - PacMap.iter (fun pac b -> Queue.add (b,pac) state.marks) r1.constructors; + PacMap.iter + (fun pac b -> Queue.add (b,Cmark pac) state.marks) + r1.constructors; + PafMap.iter + (fun paf -> Intset.iter + (fun b -> Queue.add (b,Fmark paf) state.marks)) + r1.functions; match r1.inductive_status,r2.inductive_status with Unknown,_ -> () | Partial pac,Unknown -> @@ -351,7 +479,7 @@ let union state i1 i2 eq= state.pa_classes<-Intset.remove i2 state.pa_classes; r2.inductive_status<-Partial_applied | Total cpl,Unknown -> r2.inductive_status<-Total cpl; - | Total cpl,Total _ -> Queue.add cpl state.marks + | Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks | _,_ -> () let merge eq state = (* merge and no-merge *) @@ -380,19 +508,22 @@ let update t state = (* update 1 and 2 *) | _ -> () end; PacMap.iter - (fun pac _ -> Queue.add (t,append_pac v pac) state.marks) + (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks) rep.constructors; + PafMap.iter + (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks) + rep.functions; try let s = ST.query sign state.sigtable in Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine with Not_found -> ST.enter t sign state.sigtable -let process_mark t pac state = - debug msgnl - (str "Processing mark for term " ++ int t ++ str "."); - let i=find state.uf t in - let rep=get_representative state.uf i in +let process_function_mark t rep paf state = + add_paf rep paf t; + state.terms<-Intset.union rep.lfathers state.terms + +let process_constructor_mark t i rep pac state = match rep.inductive_status with Total (s,opac) -> if pac.cnode <> opac.cnode then (* Conflict *) @@ -424,6 +555,15 @@ let process_mark t pac state = state.pa_classes<- Intset.add i state.pa_classes end +let process_mark t m state = + debug msgnl + (str "Processing mark for term " ++ int t ++ str "."); + let i=find state.uf t in + let rep=get_representative state.uf i in + match m with + Fmark paf -> process_function_mark t rep paf state + | Cmark pac -> process_constructor_mark t i rep pac state + type explanation = Discrimination of (int*pa_constructor*int*pa_constructor) | Contradiction of disequality @@ -447,15 +587,21 @@ let check_disequalities state = let one_step state = try let eq = Queue.take state.combine in - merge eq state + merge eq state; + true with Queue.Empty -> try let (t,m) = Queue.take state.marks in - process_mark t m state + process_mark t m state; + true with Queue.Empty -> + try let t = Intset.choose state.terms in state.terms<-Intset.remove t state.terms; - update t state + update t state; + true + with Not_found -> false + let complete_one_class state i= match (get_representative state.uf i).inductive_status with @@ -470,38 +616,162 @@ let complete_one_class state i= let complete state = Intset.iter (complete_one_class state) state.pa_classes +type matching_problem = +{mp_subst : int array; + mp_inst : quant_eq; + mp_stack : (ccpattern*int) list } + +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; + !funtab + + +let rec do_match state res pb_stack = + let mp=Stack.pop pb_stack in + match mp.mp_stack with + [] -> + res:= (mp.mp_inst,mp.mp_subst) :: !res + | (patt,cl)::remains -> + let uf=state.uf in + match patt with + PVar i -> + if mp.mp_subst.(pred i)<0 then + begin + mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *) + Stack.push {mp with mp_stack=remains} pb_stack + end + else + if mp.mp_subst.(pred i) = cl then + Stack.push {mp with mp_stack=remains} pb_stack + | PApp (f,[]) -> + begin + try let j=Hashtbl.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 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 + 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 + with Not_found -> () + +let paf_of_patt syms = function + PVar _ -> invalid_arg "paf_of_patt: pattern is trivial" + | PApp (f,args) -> + {fsym=Hashtbl.find syms f; + fnargs=List.length args} + +let init_pb_stack state = + let syms= state.uf.syms in + let pb_stack = Stack.create () in + 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 -> () + 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 -> () + end in + List.iter aux state.quant; + pb_stack + +let find_instances state = + let pb_stack= init_pb_stack state in + let res =ref [] in + let _ = + debug msgnl (str "Running E-matching algorithm ... "); + try + while true do + do_match state res pb_stack + done; + anomaly "get out of here !" + with Stack.Empty -> () in + !res + let rec execute first_run state = debug msgnl (str "Executing ... "); try - while true do - one_step state + while one_step state do () done; - anomaly "keep out of here" - with - Discriminable(s,spac,t,tpac) -> - Some - begin - if first_run then - Discrimination (s,spac,t,tpac) - else - Incomplete - end - | Not_found -> - match check_disequalities state with - None -> - if not(Intset.is_empty state.pa_classes) then - begin - debug msgnl - (str "First run was incomplete, completing ... "); - complete state; - execute false state - end - else None - | Some dis -> Some - begin - if first_run then - Contradiction dis + match check_disequalities state with + None -> + if not(Intset.is_empty state.pa_classes) then + begin + debug msgnl (str "First run was incomplete, completing ... "); + complete state; + execute false state + end + else + if state.rew_depth>0 then + let l=find_instances state in + List.iter (add_inst state) l; + if state.changed then + begin + state.changed <- false; + execute true state + end else - Incomplete + begin + debug msgnl (str "Out of instances ... "); + None + end + else + begin + debug msgnl (str "Out of depth ... "); + None end + | Some dis -> Some + begin + if first_run then Contradiction dis + else Incomplete + end + with Discriminable(s,spac,t,tpac) -> Some + begin + if first_run then Discrimination (s,spac,t,tpac) + else Incomplete + end + diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli index 74132811..05a5c4d1 100644 --- a/contrib/cc/ccalgo.mli +++ b/contrib/cc/ccalgo.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.mli 7298 2005-08-17 12:56:38Z corbinea $ *) +(* $Id: ccalgo.mli 9151 2006-09-19 13:32:22Z corbinea $ *) open Util open Term @@ -23,6 +23,10 @@ type term = | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) +type ccpattern = + PApp of term * ccpattern list + | PVar of int + type pa_constructor = { cnode : int; arity : int; @@ -36,14 +40,14 @@ type state type rule= Congruence - | Axiom of identifier * bool + | Axiom of constr * bool | Injection of int * pa_constructor * int * pa_constructor * int type from= Goal - | Hyp of identifier - | HeqG of identifier - | HeqnH of identifier * identifier + | Hyp of constr + | HeqG of constr + | HeqnH of constr*constr type 'a eq = {lhs:int;rhs:int;rule:'a} @@ -56,22 +60,28 @@ type explanation = | Contradiction of disequality | Incomplete +val constr_of_term : term -> constr + val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit val forest : state -> forest -val axioms : forest -> (identifier, term * term) Hashtbl.t +val axioms : forest -> (constr, term * term) Hashtbl.t val epsilons : forest -> pa_constructor list -val empty : unit -> state +val empty : int -> state val add_term : state -> term -> int -val add_equality : state -> identifier -> term -> term -> unit +val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit +val add_quant : state -> identifier -> bool -> + int * bool * ccpattern * bool * ccpattern -> unit + + val tail_pac : pa_constructor -> pa_constructor val find : forest -> int -> int @@ -87,6 +97,35 @@ val subterms : forest -> int -> int * int val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list +type quant_eq= + {qe_hyp_id: identifier; + qe_pol: bool; + qe_nvars:int; + qe_lhs: ccpattern; + qe_lhs_valid:bool; + qe_rhs: ccpattern; + qe_rhs_valid:bool} + + +type pa_fun= + {fsym:int; + fnargs:int} + +type matching_problem + +module PafMap: Map.S with type key = pa_fun + +val make_fun_table : state -> Intset.t PafMap.t + +val do_match : state -> + (quant_eq * int array) list ref -> matching_problem Stack.t -> unit + +val init_pb_stack : state -> matching_problem Stack.t + +val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun + +val find_instances : state -> (quant_eq * int array) list + val execute : bool -> state -> explanation option diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index 1200dc2e..1ffa347a 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -6,18 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.ml 7298 2005-08-17 12:56:38Z corbinea $ *) +(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open Util open Names +open Term open Ccalgo type proof= - Ax of identifier - | SymAx of identifier + Ax of constr + | SymAx of constr | Refl of term | Trans of proof*proof | Congr of proof*proof diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli index 18c745bf..abdd6fea 100644 --- a/contrib/cc/ccproof.mli +++ b/contrib/cc/ccproof.mli @@ -6,14 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.mli 7298 2005-08-17 12:56:38Z corbinea $ *) +(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *) open Ccalgo open Names +open Term type proof = - Ax of identifier - | SymAx of identifier + Ax of constr + | SymAx of constr | Refl of term | Trans of proof * proof | Congr of proof * proof @@ -25,6 +26,6 @@ val build_proof : | `Prove of int * int ] -> proof val type_proof : - (identifier, (term * term)) Hashtbl.t -> proof -> term * term + (constr, (term * term)) Hashtbl.t -> proof -> term * term diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 4a719f38..ea8aceeb 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 7909 2006-01-21 11:09:18Z herbelin $ *) +(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -63,7 +63,7 @@ let rec decompose_term env t= Constructor {ci_constr=c; ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} - | _ ->(Symb t) + | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) @@ -79,34 +79,72 @@ let atom_of_constr env term = else `Other (decompose_term env term) | _ -> `Other (decompose_term env term) -let rec litteral_of_constr env term= +let rec pattern_of_constr env c = + match kind_of_term (whd env c) with + App (f,args)-> + let pf = decompose_term env f in + let pargs,lrels = List.split + (array_map_to_list (pattern_of_constr env) args) in + PApp (pf,List.rev pargs), + List.fold_left Intset.union Intset.empty lrels + | Rel i -> PVar i,Intset.singleton i + | _ -> + let pf = decompose_term env c in + PApp (pf,[]),Intset.empty + +let non_trivial = function + PVar _ -> false + | _ -> true + +let patterns_of_constr env nrels term= + let f,args= + try destApp (whd_delta env term) with _ -> raise Not_found in + if eq_constr f (Lazy.force _eq) && (Array.length args)=3 + then + let patt1,rels1 = pattern_of_constr env args.(1) + and patt2,rels2 = pattern_of_constr env args.(2) in + let valid1 = (Intset.cardinal rels1 = nrels && non_trivial patt1) + and valid2 = (Intset.cardinal rels2 = nrels && non_trivial patt2) in + if valid1 || valid2 then + nrels,valid1,patt1,valid2,patt2 + else raise Not_found + else raise Not_found + +let rec quantified_atom_of_constr env nrels term = match kind_of_term (whd_delta env term) with Prod (_,atom,ff) -> if eq_constr ff (Lazy.force _False) then + let patts=patterns_of_constr env nrels atom in + `Nrule patts + else + quantified_atom_of_constr env (succ nrels) ff + | _ -> + let patts=patterns_of_constr env nrels term in + `Rule patts + +let litteral_of_constr env term= + match kind_of_term (whd_delta env term) with + | Prod (_,atom,ff) -> + if eq_constr ff (Lazy.force _False) then match (atom_of_constr env atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) - else - `Other (decompose_term env term) - | _ -> atom_of_constr env term + else + begin + try + quantified_atom_of_constr env 1 ff + with Not_found -> + `Other (decompose_term env term) + end + | _ -> + atom_of_constr env term -(* rebuild a term from applicative format *) - -let rec make_term = function - Symb s->s - | Eps -> anomaly "epsilon constant has no value" - | Constructor cinfo -> mkConstruct cinfo.ci_constr - | Appli (s1,s2)-> - make_app [(make_term s2)] s1 -and make_app l=function - Appli (s1,s2)->make_app ((make_term s2)::l) s1 - | other -> applistc (make_term other) l (* store all equalities from the context *) -let rec make_prb gls additionnal_terms = +let rec make_prb gls depth additionnal_terms = let env=pf_env gls in - let state = empty () in + let state = empty depth in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter @@ -116,21 +154,24 @@ let rec make_prb gls additionnal_terms = List.iter (fun (id,_,e) -> begin + let cid=mkVar id in match litteral_of_constr env e with - `Eq (t,a,b) -> add_equality state id a b - | `Neq (t,a,b) -> add_disequality state (Hyp id) a b + `Eq (t,a,b) -> add_equality state cid a b + | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> List.iter - (fun (idn,nh) -> - add_disequality state (HeqnH (id,idn)) ph nh) + (fun (cidn,nh) -> + add_disequality state (HeqnH (cid,cidn)) ph nh) !neg_hyps; - pos_hyps:=(id,ph):: !pos_hyps + pos_hyps:=(cid,ph):: !pos_hyps | `Nother nh -> List.iter - (fun (idp,ph) -> - add_disequality state (HeqnH (idp,id)) ph nh) + (fun (cidp,ph) -> + add_disequality state (HeqnH (cidp,cid)) ph nh) !pos_hyps; - neg_hyps:=(id,nh):: !neg_hyps + neg_hyps:=(cid,nh):: !neg_hyps + | `Rule patts -> add_quant state id true patts + | `Nrule patts -> add_quant state id false patts end) (Environ.named_context_of_val gls.it.evar_hyps); begin match atom_of_constr env gls.it.evar_concl with @@ -170,18 +211,18 @@ let build_projection intype outtype (cstr:constructor) special default gls= (* generate an adhoc tactic following the proof tree *) let rec proof_tac axioms=function - Ax id->exact_check (mkVar id) - | SymAx id->tclTHEN symmetry (exact_check (mkVar id)) - | Refl t->reflexivity - | Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in + Ax c -> exact_check c + | SymAx c -> tclTHEN symmetry (exact_check c) + | Refl t -> reflexivity + | Trans (p1,p2)->let t=(constr_of_term (snd (type_proof axioms p1))) in (tclTHENS (transitivity t) [(proof_tac axioms p1);(proof_tac axioms p2)]) | Congr (p1,p2)-> fun gls-> let (f1,f2)=(type_proof axioms p1) and (x1,x2)=(type_proof axioms p2) in - let tf1=make_term f1 and tx1=make_term x1 - and tf2=make_term f2 and tx2=make_term x2 in + let tf1=constr_of_term f1 and tx1=constr_of_term x1 + and tf2=constr_of_term f2 and tx2=constr_of_term x2 in let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1 and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in let id=pf_get_new_id (id_of_string "f") gls in @@ -204,52 +245,52 @@ let rec proof_tac axioms=function (fun gls -> let ti,tj=type_proof axioms prf in let ai,aj=type_proof axioms gprf in - let cti=make_term ti in - let ctj=make_term tj in - let cai=make_term ai in + let cti=constr_of_term ti in + let ctj=constr_of_term tj in + let cai=constr_of_term ai in let intype=pf_type_of gls cti in let outtype=pf_type_of gls cai in let special=mkRel (1+nargs-argind) in - let default=make_term ai in + let default=constr_of_term ai in let proj=build_projection intype outtype cstr special default gls in let injt= mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in tclTHEN (apply injt) (proof_tac axioms prf) gls) -let refute_tac axioms id t1 t2 p gls = - let tt1=make_term t1 and tt2=make_term t2 in +let refute_tac axioms c t1 t2 p gls = + let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype=pf_type_of gls tt1 in let neweq= mkApp(Lazy.force _eq, [|intype;tt1;tt2|]) in let hid=pf_get_new_id (id_of_string "Heq") gls in - let false_t=mkApp (mkVar id,[|mkVar hid|]) in + let false_t=mkApp (c,[|mkVar hid|]) in tclTHENS (true_cut (Name hid) neweq) [proof_tac axioms p; simplest_elim false_t] gls -let convert_to_goal_tac axioms id t1 t2 p gls = - let tt1=make_term t1 and tt2=make_term t2 in +let convert_to_goal_tac axioms c t1 t2 p gls = + let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort=pf_type_of gls tt2 in let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in let e=pf_get_new_id (id_of_string "e") gls in let x=pf_get_new_id (id_of_string "X") gls in let identity=mkLambda (Name x,sort,mkRel 1) in let endt=mkApp (Lazy.force _eq_rect, - [|sort;tt1;identity;mkVar id;tt2;mkVar e|]) in + [|sort;tt1;identity;c;tt2;mkVar e|]) in tclTHENS (true_cut (Name e) neweq) [proof_tac axioms p;exact_check endt] gls -let convert_to_hyp_tac axioms id1 t1 id2 t2 p gls = - let tt2=make_term t2 in +let convert_to_hyp_tac axioms c1 t1 c2 t2 p gls = + let tt2=constr_of_term t2 in let h=pf_get_new_id (id_of_string "H") gls in - let false_t=mkApp (mkVar id2,[|mkVar h|]) in + let false_t=mkApp (c2,[|mkVar h|]) in tclTHENS (true_cut (Name h) tt2) - [convert_to_goal_tac axioms id1 t1 t2 p; + [convert_to_goal_tac axioms c1 t1 t2 p; simplest_elim false_t] gls let discriminate_tac axioms cstr p gls = let t1,t2=type_proof axioms p in - let tt1=make_term t1 and tt2=make_term t2 in + let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype=pf_type_of gls tt1 in let concl=pf_concl gls in let outsort=mkType (new_univ ()) in @@ -273,15 +314,15 @@ let discriminate_tac axioms cstr p gls = let build_term_to_complete uf meta pac = let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> make_term (term uf i)) pac.args in + let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in let dummy_args = List.rev (list_tabulate meta pac.arity) in let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args -let cc_tactic additionnal_terms gls= +let cc_tactic depth additionnal_terms gls= Coqlib.check_required_library ["Coq";"Init";"Logic"]; let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in - let state = make_prb gls additionnal_terms in + let state = make_prb gls depth additionnal_terms in let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in let sol = execute true state in let _ = debug Pp.msgnl (Pp.str "Computation completed.") in @@ -334,3 +375,8 @@ let cc_tactic additionnal_terms gls= let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") + +let congruence_tac depth l = + tclORELSE + (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) + cc_fail diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli index 6082beb6..97fa4d77 100644 --- a/contrib/cc/cctac.mli +++ b/contrib/cc/cctac.mli @@ -6,11 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cctac.mli 7298 2005-08-17 12:56:38Z corbinea $ *) +(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *) open Term open Proof_type -val cc_tactic : constr list -> tactic +val cc_tactic : int -> constr list -> tactic val cc_fail : tactic + +val congruence_tac : int -> constr list -> tactic diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 index 0bdf7608..693aebb4 100644 --- a/contrib/cc/g_congruence.ml4 +++ b/contrib/cc/g_congruence.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_congruence.ml4 7734 2005-12-26 14:06:51Z herbelin $ *) +(* $Id: g_congruence.ml4 9151 2006-09-19 13:32:22Z corbinea $ *) open Cctac open Tactics @@ -17,13 +17,9 @@ open Tacticals (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic [])) - cc_fail ] -END - -TACTIC EXTEND cc_with - [ "congruence" "with" ne_constr_list(l) ] -> [ tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic l)) - cc_fail] + [ "congruence" ] -> [ congruence_tac 0 [] ] + |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] + |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 0 l ] + |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> + [ congruence_tac n l ] END |