diff options
Diffstat (limited to 'contrib/cc')
-rw-r--r-- | contrib/cc/ccalgo.ml | 307 | ||||
-rw-r--r-- | contrib/cc/ccalgo.mli | 19 | ||||
-rw-r--r-- | contrib/cc/ccproof.ml | 2 | ||||
-rw-r--r-- | contrib/cc/ccproof.mli | 2 | ||||
-rw-r--r-- | contrib/cc/cctac.ml | 145 | ||||
-rw-r--r-- | contrib/cc/cctac.mli | 4 | ||||
-rw-r--r-- | contrib/cc/g_congruence.ml4 | 10 |
7 files changed, 330 insertions, 159 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 -> diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli index 05a5c4d1..cdc0065e 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 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccalgo.mli 10579 2008-02-21 13:54:00Z corbinea $ *) open Util open Term @@ -19,10 +19,16 @@ 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 *) +type patt_kind = + Normal + | Trivial of types + | Creates_variables + type ccpattern = PApp of term * ccpattern list | PVar of int @@ -70,7 +76,7 @@ val axioms : forest -> (constr, term * term) Hashtbl.t val epsilons : forest -> pa_constructor list -val empty : int -> state +val empty : int -> Proof_type.goal Tacmach.sigma -> state val add_term : state -> term -> int @@ -79,8 +85,7 @@ 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 - + int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -102,9 +107,9 @@ type quant_eq= 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} type pa_fun= diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index d336f599..a459b18f 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *) +(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli index 572b2c53..0eb97efe 100644 --- a/contrib/cc/ccproof.mli +++ b/contrib/cc/ccproof.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *) +(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *) open Ccalgo open Names diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index dc0dec0e..871d7521 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *) +(* $Id: cctac.ml 10670 2008-03-14 19:30:48Z letouzey $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -24,6 +24,7 @@ open Termops open Tacmach open Tactics open Tacticals +open Typing open Ccalgo open Tacinterp open Ccproof @@ -49,6 +50,8 @@ let _False = constant ["Init";"Logic"] "False" (* decompose member of equality in an applicative format *) +let sf_of env sigma c = family_of_sort (destSort (type_of env sigma c)) + let whd env= let infos=Closure.create_clos_infos Closure.betaiotazeta env in (fun t -> Closure.whd_val infos (Closure.inject t)) @@ -57,12 +60,19 @@ let whd_delta env= let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let rec decompose_term env t= +let rec decompose_term env sigma t= match kind_of_term (whd env t) with App (f,args)-> - let tf=decompose_term env f in - let targs=Array.map (decompose_term env) args in + let tf=decompose_term env sigma f in + let targs=Array.map (decompose_term env sigma) args in Array.fold_left (fun s t->Appli (s,t)) tf targs + | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> + let b = pop _b in + let sort_b = sf_of env sigma b in + let sort_a = sf_of env sigma a in + Appli(Appli(Product (sort_a,sort_b) , + decompose_term env sigma a), + decompose_term env sigma b) | Construct c-> let (oib,_)=Global.lookup_inductive (fst c) in let nargs=mis_constructor_nargs_env env c in @@ -73,95 +83,111 @@ let rec decompose_term env t= (* decompose equality in members and type *) -let atom_of_constr env term = +let atom_of_constr env sigma term = let wh = (whd_delta env term) in let kot = kind_of_term wh in match kot with App (f,args)-> if eq_constr f (Lazy.force _eq) && (Array.length args)=3 then `Eq (args.(0), - decompose_term env args.(1), - decompose_term env args.(2)) - else `Other (decompose_term env term) - | _ -> `Other (decompose_term env term) + decompose_term env sigma args.(1), + decompose_term env sigma args.(2)) + else `Other (decompose_term env sigma term) + | _ -> `Other (decompose_term env sigma term) -let rec pattern_of_constr env c = +let rec pattern_of_constr env sigma c = match kind_of_term (whd env c) with App (f,args)-> - let pf = decompose_term env f in + let pf = decompose_term env sigma f in let pargs,lrels = List.split - (array_map_to_list (pattern_of_constr env) args) in + (array_map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), - List.fold_left Intset.union Intset.empty lrels + List.fold_left Intset.union Intset.empty lrels + | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> + let b =pop _b in + let pa,sa = pattern_of_constr env sigma a in + let pb,sb = pattern_of_constr env sigma (pop b) in + let sort_b = sf_of env sigma b in + let sort_a = sf_of env sigma a in + PApp(Product (sort_a,sort_b), + [pa;pb]),(Intset.union sa sb) | Rel i -> PVar i,Intset.singleton i | _ -> - let pf = decompose_term env c in + let pf = decompose_term env sigma c in PApp (pf,[]),Intset.empty let non_trivial = function PVar _ -> false | _ -> true -let patterns_of_constr env nrels term= +let patterns_of_constr env sigma 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 + let patt1,rels1 = pattern_of_constr env sigma args.(1) + and patt2,rels2 = pattern_of_constr env sigma args.(2) in + let valid1 = + if Intset.cardinal rels1 <> nrels then Creates_variables + else if non_trivial patt1 then Normal + else Trivial args.(0) + and valid2 = + if Intset.cardinal rels2 <> nrels then Creates_variables + else if non_trivial patt2 then Normal + else Trivial args.(0) in + if valid1 <> Creates_variables + || valid2 <> Creates_variables then nrels,valid1,patt1,valid2,patt2 else raise Not_found else raise Not_found -let rec quantified_atom_of_constr env nrels term = +let rec quantified_atom_of_constr env sigma 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 + let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr env (succ nrels) ff + quantified_atom_of_constr env sigma (succ nrels) ff | _ -> - let patts=patterns_of_constr env nrels term in + let patts=patterns_of_constr env sigma nrels term in `Rule patts -let litteral_of_constr env term= +let litteral_of_constr env sigma 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 + match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) else begin try - quantified_atom_of_constr env 1 ff + quantified_atom_of_constr env sigma 1 ff with Not_found -> - `Other (decompose_term env term) + `Other (decompose_term env sigma term) end | _ -> - atom_of_constr env term + atom_of_constr env sigma term (* store all equalities from the context *) let rec make_prb gls depth additionnal_terms = let env=pf_env gls in - let state = empty depth in + let sigma=sig_sig gls in + let state = empty depth gls in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter (fun c -> - let t = decompose_term env c in + let t = decompose_term env sigma c in ignore (add_term state t)) additionnal_terms; List.iter (fun (id,_,e) -> begin let cid=mkVar id in - match litteral_of_constr env e with + match litteral_of_constr env sigma e with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> @@ -180,7 +206,7 @@ let rec make_prb gls depth additionnal_terms = | `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 + match atom_of_constr env sigma gls.it.evar_concl with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter @@ -209,7 +235,7 @@ let build_projection intype outtype (cstr:constructor) special default gls= let branches=Array.init lp branch in let casee=mkRel 1 in let pred=mkLambda(Anonymous,intype,outtype) in - let case_info=make_default_case_info (pf_env gls) RegularStyle ind in + let case_info=make_case_info (pf_env gls) ind RegularStyle in let body= mkCase(case_info, pred, casee, branches) in let id=pf_get_new_id (id_of_string "t") gls in mkLambda(Name id,intype,body) @@ -224,19 +250,19 @@ let rec proof_tac p gls = | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = pf_type_of gls l in + let typ = refresh_universes (pf_type_of gls l) in exact_check (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls | Refl t -> let lr = constr_of_term t in - let typ = pf_type_of gls lr in + let typ = refresh_universes (pf_type_of gls lr) in exact_check (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - let typ = pf_type_of gls t2 in + let typ = refresh_universes (pf_type_of gls t2) in let prf = mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls @@ -245,16 +271,17 @@ let rec proof_tac p gls = and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - let typf = pf_type_of gls tf1 in - let typx = pf_type_of gls tx1 in - let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in + let typf = refresh_universes (pf_type_of gls tf1) in + let typx = refresh_universes (pf_type_of gls tx1) in + let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in let id = pf_get_new_id (id_of_string "f") gls in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = mkApp(Lazy.force _f_equal, [|typf;typfx;appx1;tf1;tf2;_M 1|]) in let lemma2= - mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in + mkApp(Lazy.force _f_equal, + [|typx;typfx;tf2;tx1;tx2;_M 1|]) in let prf = mkApp(Lazy.force _trans_eq, [|typfx; @@ -274,8 +301,8 @@ let rec proof_tac p gls = let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype=pf_type_of gls ti in - let outtype=pf_type_of gls default in + let intype=refresh_universes (pf_type_of gls ti) in + let outtype=refresh_universes (pf_type_of gls default) in let special=mkRel (1+nargs-argind) in let proj=build_projection intype outtype cstr special default gls in let injt= @@ -284,7 +311,7 @@ let rec proof_tac p gls = let refute_tac 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 intype=refresh_universes (pf_type_of gls tt1) in let neweq= mkApp(Lazy.force _eq, [|intype;tt1;tt2|]) in @@ -295,7 +322,7 @@ let refute_tac c t1 t2 p gls = let convert_to_goal_tac 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 sort=refresh_universes (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 @@ -315,7 +342,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls = let discriminate_tac cstr p gls = let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype=pf_type_of gls t1 in + let intype=refresh_universes (pf_type_of gls t1) in let concl=pf_concl gls in let outsort=mkType (new_univ ()) in let xid=pf_get_new_id (id_of_string "X") gls in @@ -403,3 +430,29 @@ let congruence_tac depth l = tclORELSE (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) cc_fail + +(* The [f_equal] tactic. + + It mimics the use of lemmas [f_equal], [f_equal2], etc. + This isn't particularly related with congruence, apart from + the fact that congruence is called internally. +*) + +let f_equal gl = + let cut_eq c1 c2 = + let ty = refresh_universes (pf_type_of gl c1) in + tclTHENTRY + (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) reflexivity + in + try match kind_of_term (pf_concl gl) with + | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> + begin match kind_of_term t, kind_of_term t' with + | App (f,v), App (f',v') when Array.length v = Array.length v' -> + let rec cuts i = + if i < 0 then tclTRY (congruence_tac 1000 []) + else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) + in cuts (Array.length v - 1) gl + | _ -> tclIDTAC gl + end + | _ -> tclIDTAC gl + with Type_errors.TypeError _ -> tclIDTAC gl diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli index ffc4b9c4..57ad0558 100644 --- a/contrib/cc/cctac.mli +++ b/contrib/cc/cctac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *) +(* $Id: cctac.mli 10637 2008-03-07 23:52:56Z letouzey $ *) open Term open Proof_type @@ -18,3 +18,5 @@ val cc_tactic : int -> constr list -> tactic val cc_fail : tactic val congruence_tac : int -> constr list -> tactic + +val f_equal : tactic diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 index 693aebb4..9877e6fc 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 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: g_congruence.ml4 10637 2008-03-07 23:52:56Z letouzey $ *) open Cctac open Tactics @@ -17,9 +17,13 @@ open Tacticals (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 0 [] ] + [ "congruence" ] -> [ congruence_tac 1000 [] ] |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 0 l ] + |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> [ congruence_tac n l ] END + +TACTIC EXTEND f_equal + [ "f_equal" ] -> [ f_equal ] +END |