From 1c10b84c0ce5f96a3afd1fc83c738c76070958c3 Mon Sep 17 00:00:00 2001 From: amblaf Date: Tue, 27 Jun 2017 08:38:20 +0200 Subject: Correcting [build_discriminator] to make the test-suite pass --- API/API.mli | 2 +- plugins/cc/cctac.ml | 3 ++- tactics/equality.ml | 62 +++++++++++++++++++++++++++------------------------- tactics/equality.mli | 2 +- 4 files changed, 36 insertions(+), 33 deletions(-) diff --git a/API/API.mli b/API/API.mli index 19726b52f..3905843a5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5233,7 +5233,7 @@ sig val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> - EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.constr -> EConstr.constr val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4934b0750..11d3a6d1f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -231,7 +231,8 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma = project gls in + let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in sigma, mkLambda(Name id,intype,body) diff --git a/tactics/equality.ml b/tactics/equality.ml index d08735582..6274bca9f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -854,7 +854,8 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") + in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in let (mib,mip) = lookup_mind_specif env ind in @@ -876,7 +877,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -921,23 +922,20 @@ let build_selector env sigma dirn c ind special default = let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, mkCase (ci, p, c, Array.of_list brl) + mkCase (ci, p, c, Array.of_list brl) -let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ()) -let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ()) -let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ()) +let build_coq_False () = pf_constr_of_global (build_coq_False ()) +let build_coq_True () = pf_constr_of_global (build_coq_True ()) +let build_coq_I () = pf_constr_of_global (build_coq_I ()) -let rec build_discriminator env sigma dirn c = function +let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - let sigma, true_0 = build_coq_True sigma in - let sigma, false_0 = build_coq_False sigma in build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> - let sigma, false_0 = build_coq_False sigma in let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let sigma, subval = build_discriminator cnum_env sigma dirn newc l in + let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in kont sigma subval (false_0,mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is @@ -980,14 +978,15 @@ let ind_scheme_of_eq lbeq = ConstRef c, eff -let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = - let sigma, i = build_coq_I sigma in - let sigma, absurd_term = build_coq_False sigma in +let discrimination_pf e (t,t1,t2) discriminator lbeq = + build_coq_I () >>= fun i -> + build_coq_False () >>= fun absurd_term -> let eq_elim, eff = ind_scheme_of_eq lbeq in - let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in - let eq_elim = EConstr.of_constr eq_elim in - sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), - eff + Proofview.tclEFFECTS eff <*> + pf_constr_of_global eq_elim >>= fun eq_elim -> + Proofview.tclUNIT + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) + let eq_baseid = Id.of_string "e" @@ -1001,19 +1000,22 @@ let apply_on_clause (f,t) clause = clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = + build_coq_True () >>= fun true_0 -> + build_coq_False () >>= fun false_0 -> let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - let sigma, discriminator = - build_discriminator e_env sigma dirn (mkVar e) cpath in - let sigma,(pf, absurd_term), eff = - discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in - let pf_ty = mkArrow eqn absurd_term in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.tclEFFECTS eff <*> - tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + try + let discriminator = + build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath + in + discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> + let pf_ty = mkArrow eqn absurd_term in + let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in + let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + tclTHENS (assert_after Anonymous absurd_term) + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + with + UserError _ as ex -> Proofview.tclZERO ex let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1299,7 +1301,7 @@ let rec build_injrec env sigma dflt c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in - let sigma, res = kont sigma subval (dfltval,tuplety) in + let res = kont sigma subval (dfltval,tuplety) in sigma, (res, tuplety,dfltval) with UserError _ -> failwith "caught" diff --git a/tactics/equality.mli b/tactics/equality.mli index 421f7c7f5..a4d1c0f9b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> evar_map * constr + constr -> constr -> constr -- cgit v1.2.3