diff options
Diffstat (limited to 'contrib/cc/cctac.ml')
-rw-r--r-- | contrib/cc/cctac.ml | 148 |
1 files changed, 97 insertions, 51 deletions
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 |