diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 463 |
1 files changed, 250 insertions, 213 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 60d42916..7110e5b2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,49 +1,39 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - (* This file is the interface between the c-c algorithm and Coq *) open Evd -open Proof_type open Names -open Libnames -open Nameops open Inductiveops open Declarations open Term +open Vars open Tacmach open Tactics -open Tacticals open Typing open Ccalgo -open Tacinterp open Ccproof open Pp +open Errors open Util -open Format - -let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) - -let _f_equal = constant ["Init";"Logic"] "f_equal" - -let _eq_rect = constant ["Init";"Logic"] "eq_rect" - -let _refl_equal = constant ["Init";"Logic"] "eq_refl" -let _sym_eq = constant ["Init";"Logic"] "eq_sym" +let reference dir s = Coqlib.gen_reference "CC" dir s -let _trans_eq = constant ["Init";"Logic"] "eq_trans" - -let _eq = constant ["Init";"Logic"] "eq" - -let _False = constant ["Init";"Logic"] "False" +let _f_equal = reference ["Init";"Logic"] "f_equal" +let _eq_rect = reference ["Init";"Logic"] "eq_rect" +let _refl_equal = reference ["Init";"Logic"] "eq_refl" +let _sym_eq = reference ["Init";"Logic"] "eq_sym" +let _trans_eq = reference ["Init";"Logic"] "eq_trans" +let _eq = reference ["Init";"Logic"] "eq" +let _False = reference ["Init";"Logic"] "False" +let _True = reference ["Init";"Logic"] "True" +let _I = reference ["Init";"Logic"] "I" let whd env= let infos=Closure.create_clos_infos Closure.betaiotazeta env in @@ -55,7 +45,8 @@ let whd_delta env= (* decompose member of equality in an applicative format *) -let sf_of env sigma c = family_of_sort (sort_of env sigma c) +(** FIXME: evar leak *) +let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c) let rec decompose_term env sigma t= match kind_of_term (whd env t) with @@ -70,32 +61,37 @@ let rec decompose_term env sigma t= Appli(Appli(Product (sort_a,sort_b) , decompose_term env sigma a), decompose_term env sigma b) - | Construct c-> - let (mind,i_ind),i_con = c in + | Construct c -> + let (((mind,i_ind),i_con),u)= c in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in - Constructor {ci_constr= (canon_ind,i_con); + let nargs=constructor_nallargs_env env (canon_ind,i_con) in + Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} | Ind c -> - let mind,i_ind = c in + let (mind,i_ind),u = c in let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) - | Const c -> + let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u))) + | Const (c,u) -> let canon_const = constant_of_kn (canonical_con c) in - (Symb (mkConst canon_const)) + (Symb (mkConstU (canon_const,u))) + | Proj (p, c) -> + let canon_const kn = constant_of_kn (canonical_con kn) in + let p' = Projection.map canon_const p in + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) +open Globnames 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 + if is_global _eq f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -107,9 +103,9 @@ let rec pattern_of_constr env sigma c = App (f,args)-> let pf = decompose_term env sigma f in let pargs,lrels = List.split - (array_map_to_list (pattern_of_constr env sigma) 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 Int.Set.union Int.Set.empty lrels | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> let b = Termops.pop _b in let pa,sa = pattern_of_constr env sigma a in @@ -117,11 +113,11 @@ let rec pattern_of_constr env sigma c = 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 + [pa;pb]),(Int.Set.union sa sb) + | Rel i -> PVar i,Int.Set.singleton i | _ -> let pf = decompose_term env sigma c in - PApp (pf,[]),Intset.empty + PApp (pf,[]),Int.Set.empty let non_trivial = function PVar _ -> false @@ -129,23 +125,21 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= - try destApp (whd_delta env term) - with e when Errors.noncritical e -> raise Not_found - in - if eq_constr f (Lazy.force _eq) && (Array.length args)=3 + try destApp (whd_delta env term) with DestKO -> raise Not_found in + if is_global _eq f && Int.equal (Array.length args) 3 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 + if not (Int.equal (Int.Set.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 + if not (Int.equal (Int.Set.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 + if valid1 != Creates_variables + || valid2 != Creates_variables then nrels,valid1,patt1,valid2,patt2 else raise Not_found else raise Not_found @@ -153,7 +147,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -165,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with | Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -182,7 +176,7 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) -let rec make_prb gls depth additionnal_terms = +let make_prb gls depth additionnal_terms = let env=pf_env gls in let sigma=sig_sig gls in let state = empty depth gls in @@ -213,9 +207,9 @@ let rec make_prb gls depth additionnal_terms = 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 (Goal.V82.hyps gls.sigma gls.it)); + end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); begin - match atom_of_constr env sigma (pf_concl gls) with + match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter @@ -226,226 +220,256 @@ let rec make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) -let build_projection intype outtype (cstr:constructor) special default gls= +let build_projection intype outtype (cstr:pconstructor) special default gls= let env=pf_env gls in - let (h,argv) = - try destApp intype with - Invalid_argument _ -> (intype,[||]) in - let ind=destInd h in - let types=Inductiveops.arities_of_constructors env ind in + let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in + let ind,u=destInd h in + let types=Inductiveops.arities_of_constructors env (ind,u) in let lp=Array.length types in - let ci=pred (snd cstr) in + let ci=pred (snd(fst cstr)) in let branch i= - let ti=Term.prod_appvect types.(i) argv in + let ti= prod_appvect types.(i) argv in let rc=fst (decompose_prod_assum ti) in let head= - if i=ci then special else default in + if Int.equal i ci then special else default in it_mkLambda_or_LetIn head rc in let branches=Array.init lp branch in let casee=mkRel 1 in let pred=mkLambda(Anonymous,intype,outtype) 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 + let id=pf_get_new_id (Id.of_string "t") gls in mkLambda(Name id,intype,body) (* generate an adhoc tactic following the proof tree *) let _M =mkMeta -let rec proof_tac p gls = +let app_global f args k = + Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_app_global f args k = + Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_refine c = Proofview.V82.tactic (refine c) + +let rec proof_tac p : unit Proofview.tactic = + Proofview.Goal.nf_enter begin fun gl -> + let type_of t = Tacmach.New.pf_type_of gl t in + try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> exact_check c gls + Ax c -> exact_check c | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + let typ = (* Termops.refresh_universes *) type_of l in + new_app_global _sym_eq [|typ;r;l;c|] exact_check | Refl t -> let lr = constr_of_term t in - let typ = Termops.refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + let typ = (* Termops.refresh_universes *) type_of lr in + new_app_global _refl_equal [|typ;constr_of_term t|] exact_check | 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 = Termops.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 + let typ = (* Termops.refresh_universes *) (type_of t2) in + let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs 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 = Termops.refresh_universes (pf_type_of gls tf1) in - let typx = Termops.refresh_universes (pf_type_of gls tx1) in - let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in - let id = pf_get_new_id (id_of_string "f") gls in + let typf = (* Termops.refresh_universes *)(type_of tf1) in + let typx = (* Termops.refresh_universes *) (type_of tx1) in + let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in + let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl 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 + app_global _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 + app_global _f_equal + [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = - mkApp(Lazy.force _trans_eq, + app_global _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - tclTHENS (refine prf) - [tclTHEN (refine lemma1) (proof_tac p1); - tclFIRST - [tclTHEN (refine lemma2) (proof_tac p2); + mkApp(tf2,[|tx2|]);_M 2;_M 3|] in + Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + Tacticals.New.tclFIRST + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; - fun gls -> - errorlabstrm "Congruence" + Proofview.tclZERO (UserError ("Congruence" , (Pp.str - "I don't know how to handle dependent equality")]] gls + "I don't know how to handle dependent equality")))]] | Inject (prf,cstr,nargs,argind) -> 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 = Termops.refresh_universes (pf_type_of gls ti) in - let outtype = Termops.refresh_universes (pf_type_of gls default) in + let intype = (* Termops.refresh_universes *) (type_of ti) in + let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in - let proj=build_projection intype outtype cstr special default gls in + let proj = + Tacmach.New.of_old (build_projection intype outtype cstr special default) gl + in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - tclTHEN (refine injt) (proof_tac prf) gls + app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end -let refute_tac c t1 t2 p gls = +let refute_tac c t1 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = Termops.refresh_universes (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 intype = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + in + let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; simplest_elim false_t] gls + Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; simplest_elim false_t] + end -let convert_to_goal_tac c t1 t2 p gls = +let refine_exact_check c gl = + let evm, _ = pf_apply e_type_of gl c in + Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl + +let convert_to_goal_tac c t1 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = Termops.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 + let sort = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + in + let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in + let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=mkApp (Lazy.force _eq_rect, - [|sort;tt1;identity;c;tt2;mkVar e|]) in - tclTHENS (assert_tac (Name e) neweq) - [proof_tac p;exact_check endt] gls + let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + Tacticals.New.tclTHENS (neweq (assert_before (Name e))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + end -let convert_to_hyp_tac c1 t1 c2 t2 p gls = +let convert_to_hyp_tac c1 t1 c2 t2 p = + Proofview.Goal.nf_enter begin fun gl -> let tt2=constr_of_term t2 in - let h=pf_get_new_id (id_of_string "H") gls in + let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (assert_tac (Name h) tt2) + Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; - simplest_elim false_t] 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 = Termops.refresh_universes (pf_type_of gls t1) in - let concl=pf_concl gls in - let outsort = mkType (Termops.new_univ ()) in - let xid=pf_get_new_id (id_of_string "X") gls in - let tid=pf_get_new_id (id_of_string "t") gls in - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - let trivial=pf_type_of gls identity in - let outtype = mkType (Termops.new_univ ()) in - let pred=mkLambda(Name xid,outtype,mkRel 1) in - let hid=pf_get_new_id (id_of_string "Heq") gls in - let proj=build_projection intype outtype cstr trivial concl gls in - let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p;exact_check endt] gls + simplest_elim false_t] + end + +let discriminate_tac (cstr,u as cstru) p = + Proofview.Goal.nf_enter begin fun gl -> + let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let intype = + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + in + let concl = Proofview.Goal.concl gl in + (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) + (* let outsort = mkSort outsort in *) + let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) + (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) + let identity = Universes.constr_of_global _I in + (* let trivial=pf_type_of gls identity in *) + let trivial = Universes.constr_of_global _True in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let outtype = mkSort outtype in + let pred=mkLambda(Name xid,outtype,mkRel 1) in + let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in + let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in + let injt=app_global _f_equal + [|intype;outtype;proj;t1;t2;mkVar hid|] in + let endt k = + injt (fun injt -> + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in + let neweq=new_app_global _eq [|intype;t1;t2|] in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) + (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + end (* wrap everything *) let build_term_to_complete uf meta pac = let cinfo = get_constructor_info uf pac.cnode 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 dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in - applistc (mkConstruct cinfo.ci_constr) all_args - -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 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 - let uf=forest state in + applistc (mkConstructU cinfo.ci_constr) all_args + +let cc_tactic depth additionnal_terms = + Proofview.Goal.nf_enter begin fun gl -> + Coqlib.check_required_library Coqlib.logic_module_name; + let _ = debug (Pp.str "Reading subgoal ...") in + let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in + let _ = debug (Pp.str "Problem built, solving ...") in + let sol = execute true state in + let _ = debug (Pp.str "Computation completed.") in + let uf=forest state in match sol with - None -> tclFAIL 0 (str "congruence failed") gls - | Some reason -> - debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); - match reason with - Discrimination (i,ipac,j,jpac) -> - let p=build_proof uf (`Discr (i,ipac,j,jpac)) in - let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac cstr p gls - | Incomplete -> - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in - Pp.msgnl - (Pp.str "Goal is solvable by congruence but \ + None -> Tacticals.New.tclFAIL 0 (str "congruence failed") + | Some reason -> + debug (Pp.str "Goal solved, generating proof ..."); + match reason with + Discrimination (i,ipac,j,jpac) -> + let p=build_proof uf (`Discr (i,ipac,j,jpac)) in + let cstr=(get_constructor_info uf ipac.cnode).ci_constr in + discriminate_tac cstr p + | Incomplete -> + let env = Proofview.Goal.env gl in + let metacnt = ref 0 in + let newmeta _ = incr metacnt; _M !metacnt in + let terms_to_complete = + List.map + (build_term_to_complete uf newmeta) + (epsilons uf) in + Pp.msg_info + (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msgnl - (Pp.str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ - prlist_with_sep - (fun () -> str ")" ++ pr_spc () ++ str "(") - (Termops.print_constr_env (pf_env gls)) - terms_to_complete ++ - str ")\"," - end); - Pp.msgnl - (Pp.str " replacing metavariables by arbitrary terms."); - tclFAIL 0 (str "Incomplete") gls - | Contradiction dis -> - let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in - let ta=term uf dis.lhs and tb=term uf dis.rhs in - match dis.rule with - Goal -> proof_tac p gls - | Hyp id -> refute_tac id ta tb p gls - | HeqG id -> - convert_to_goal_tac id ta tb p gls - | HeqnH (ida,idb) -> - convert_to_hyp_tac ida ta idb tb p gls - + Pp.msg_info + (Pp.str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ spc () ++ str "(") + (Termops.print_constr_env env) + terms_to_complete ++ + str ")\"," + end ++ + Pp.str " replacing metavariables by arbitrary terms."); + Tacticals.New.tclFAIL 0 (str "Incomplete") + | Contradiction dis -> + let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in + let ta=term uf dis.lhs and tb=term uf dis.rhs in + match dis.rule with + Goal -> proof_tac p + | Hyp id -> refute_tac id ta tb p + | HeqG id -> + convert_to_goal_tac id ta tb p + | HeqnH (ida,idb) -> + convert_to_hyp_tac ida ta idb tb p + end 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 + Tacticals.New.tclORELSE + (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) + (Proofview.V82.tactic cc_fail) (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent to a "simple apply refl_equal" *) -let simple_reflexivity () = apply (Lazy.force _refl_equal) - (* The [f_equal] tactic. It mimics the use of lemmas [f_equal], [f_equal2], etc. @@ -453,22 +477,35 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal) the fact that congruence is called internally. *) -let f_equal gl = - let cut_eq c1 c2 = - let ty = Termops.refresh_universes (pf_type_of gl c1) in - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_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 f_equal = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let type_of = Tacmach.New.pf_type_of gl in + let cut_eq c1 c2 = + try (* type_of can raise an exception *) + let ty = (* Termops.refresh_universes *) (type_of c1) in + if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () + else + Tacticals.New.tclTRY (Tacticals.New.tclTHEN + ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + in + Proofview.tclORELSE + begin match kind_of_term concl with + | App (r,[|_;t;t'|]) when Globnames.is_global _eq r -> + begin match kind_of_term t, kind_of_term t' with + | App (f,v), App (f',v') when Int.equal (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 + if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 []) + else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) + in cuts (Array.length v - 1) + | _ -> Proofview.tclUNIT () + end + | _ -> Proofview.tclUNIT () + end + begin function (e, info) -> match e with + | Type_errors.TypeError _ -> Proofview.tclUNIT () + | e -> Proofview.tclZERO ~info e + end + end |