diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 26 | ||||
| -rw-r--r-- | tactics/elim.ml | 143 | ||||
| -rw-r--r-- | tactics/elim.mli | 7 | ||||
| -rw-r--r-- | tactics/equality.ml | 67 | ||||
| -rw-r--r-- | tactics/hints.ml | 59 | ||||
| -rw-r--r-- | tactics/inv.ml | 21 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 134 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 30 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
10 files changed, 219 insertions, 274 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 784322679f..369508c2a3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ccb69cf845..96cbbf0ba8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = { modulo_eta = false; } -let auto_unif_flags ?(allowed_evars = AllowAll) st = +let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st = let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; @@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if cl.cl_strict then let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - AllowFun allowed - else AllowAll - | _ -> AllowAll - with e when CErrors.noncritical e -> AllowAll + Evarsolve.AllowedEvars.from_pred allowed + else Evarsolve.AllowedEvars.all + | _ -> Evarsolve.AllowedEvars.all + with e when CErrors.noncritical e -> Evarsolve.AllowedEvars.all in let tac_of_hint = fun (flags, h) -> @@ -931,12 +931,14 @@ module Search = struct top_sort evm goals else Evar.Set.elements goals in - let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>= + let goalsl = List.map Proofview_monad.with_empty_state goalsl in + let tac = + Proofview.Unsafe.tclNEWGOALS goalsl <*> + tac <*> Proofview.Unsafe.tclGETGOALS >>= fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in let evm = Evd.set_typeclass_evars evm Evar.Set.empty in let evm = Evd.push_future_goals evm in let _, pv = Proofview.init evm [] in - let pv = Proofview.unshelve goalsl pv in try (* Instance may try to call this before a proof is set up! Thus, give_me_the_proof will fail. Beware! *) @@ -947,17 +949,17 @@ module Search = struct * with | Proof_global.NoCurrentProof -> *) Id.of_string "instance", false in - let finish pv' shelved = + let finish pv' = let evm' = Proofview.return pv' in + let shelf = Evd.shelf evm' in assert(Evd.fold_undefined (fun ev _ acc -> - let okev = Evd.mem evm ev || List.mem ev shelved in + let okev = Evd.mem evm ev || List.mem ev shelf in if not okev then Feedback.msg_debug (str "leaking evar " ++ int (Evar.repr ev) ++ spc () ++ pr_ev evm' ev); acc && okev) evm' true); let _, evm' = Evd.pop_future_goals evm' in - let evm' = Evd.shelve_on_future_goals shelved evm' in let nongoals' = Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with | Some ev' -> Evar.Set.add ev acc @@ -968,8 +970,8 @@ module Search = struct let evm' = Evd.set_typeclass_evars evm' nongoals' in Some evm' in - let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in - if Proofview.finished pv' then finish pv' shelved + let (), pv', unsafe, _ = Proofview.apply ~name ~poly env tac pv in + if Proofview.finished pv' then finish pv' else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found diff --git a/tactics/elim.ml b/tactics/elim.ml index 274ebc9f60..49437a2aef 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -10,33 +10,137 @@ open Util open Names +open Constr open Termops open EConstr open Inductiveops open Hipattern open Tacmach.New open Tacticals.New +open Clenv open Tactics open Proofview.Notations +type branch_args = { + branchnum : int; (* the branch number *) + nassums : int; (* number of assumptions/letin to be introduced *) + branchsign : bool list; (* the signature of the branch. + true=assumption, false=let-in *) + branchnames : Tactypes.intro_patterns} + module NamedDecl = Context.Named.Declaration +type elim_kind = Case of bool | Elim + +(* Find the right elimination suffix corresponding to the sort of the goal *) +(* c should be of type A1->.. An->B with B an inductive definition *) +let general_elim_then_using mk_elim + rec_flag allnames tac predicate (ind, u, args) id = + let open Pp in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in + let sigma, elim = match mk_elim with + | Case dep -> + let u = EInstance.kind sigma u in + let (sigma, r) = Indrec.build_case_analysis_scheme env sigma (ind, u) dep sort in + (sigma, EConstr.of_constr r) + | Elim -> + let gr = Indrec.lookup_eliminator env ind sort in + Evd.fresh_global env sigma gr + in + let indclause = mk_clenv_from_env env sigma None (mkVar id, mkApp (mkIndU (ind, u), args)) in + (* applying elimination_scheme just a little modified *) + let elimclause = mk_clenv_from_env env sigma None (elim, Retyping.get_type_of env sigma elim) in + let indmv = + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> CErrors.anomaly (str"elimination.") + in + let pmv = + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with + | Meta p -> p + | _ -> + let name_elim = + match EConstr.kind sigma elim with + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env env sigma elim + | _ -> mt () + in + CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") + in + let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in + let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag (ind, u) in + let brnames = Tacticals.compute_induction_names false branchsigns allnames in + let flags = Unification.elim_flags () in + let elimclause' = + match predicate with + | None -> elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' + in + let after_tac i = + let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); + nassums = List.length branchsigns.(i); + branchnum = i+1; } + in + tac ba + in + let branchtacs = List.init (Array.length branchsigns) after_tac in + Proofview.tclTHEN + (Clenv.res_pf ~flags elimclause') + (Proofview.tclEXTEND [] tclIDTAC branchtacs) + end + +(* computing the case/elim combinators *) + +let make_elim_branch_assumptions ba hyps = + let assums = + try List.rev (List.firstn ba.nassums hyps) + with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in + assums + +let elim_on_ba tac ba = + Proofview.Goal.enter begin fun gl -> + let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in + tac branches + end + +let elimination_then tac id = + let open Declarations in + Proofview.Goal.enter begin fun gl -> + let ((ind, u), t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in + let _, args = decompose_app_vect (Proofview.Goal.sigma gl) t in + let isrec,mkelim = + match (Global.lookup_mind (fst ind)).mind_record with + | NotRecord -> true, Elim + | FakeRecord | PrimRecord _ -> false, Case true + in + general_elim_then_using mkelim isrec None tac None (ind, u, args) id + end + (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = - assert (ba.Tacticals.branchnames == []); - let introElimAssums = tclDO ba.Tacticals.nassums intro in + assert (ba.branchnames == []); + let introElimAssums = tclDO ba.nassums intro in (tclTHEN introElimAssums (elim_on_ba tac ba)) (* Supposed to be called with a non-recursive scheme *) let introCaseAssumsThen with_evars tac ba = - let n1 = List.length ba.Tacticals.branchsign in - let n2 = List.length ba.Tacticals.branchnames in + let n1 = List.length ba.branchsign in + let n2 = List.length ba.branchnames in let (l1,l2),l3 = - if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, [] - else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in + if n1 < n2 then List.chop n1 ba.branchnames, [] + else (ba.branchnames, []), List.make (n1-n2) false in let introCaseAssums = tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in - (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) + (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba)) + +let case_tac dep names tac elim ind c = + let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in + general_elim_then_using (Case dep) false names tac (Some elim) ind c (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate @@ -56,19 +160,16 @@ Another example : Qed. *) -let elimHypThen tac id = - elimination_then tac (mkVar id) - let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = - elimHypThen + elimination_then (introElimAssumsThen (fun bas -> tclTHEN (clear [id]) (tclMAP (general_decompose_on_hyp recognizer) - (ids_of_named_context bas.Tacticals.assums)))) + (ids_of_named_context bas)))) id (* We should add a COMPLETE to be sure that the created hypothesis @@ -76,7 +177,6 @@ and general_decompose_aux recognizer id = (* Best strategies but loss of compatibility *) let tmphyp_name = Id.of_string "_TmpHyp" -let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> @@ -90,14 +190,10 @@ let general_decompose recognizer c = end let head_in indl t gl = - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let ity,_ = - if !up_to_delta - then find_mrectype env sigma t - else extract_mrectype sigma t - in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl + let ity,_ = extract_mrectype sigma t in + List.exists (fun i -> eq_ind (fst i) (fst ity)) indl with Not_found -> false let decompose_these c l = @@ -124,9 +220,6 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c - let induction_trailer abs_i abs_j bargs = tclTHEN (tclDO (abs_j - abs_i) intro) @@ -136,7 +229,7 @@ let induction_trailer abs_i abs_j bargs = let idty = pf_get_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs in let (hyps,_) = List.fold_left @@ -149,7 +242,7 @@ let induction_trailer abs_i abs_j bargs = in let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST - [revert ids; simple_elimination (mkVar id)]) + [revert ids; elimination_then (fun _ -> tclIDTAC) id]) end )) @@ -167,7 +260,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) id))) end let h_double_induction = double_ind diff --git a/tactics/elim.mli b/tactics/elim.mli index e89855a050..01053502e4 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -10,14 +10,13 @@ open Names open EConstr -open Tacticals open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : Tactics.evars_flag -> - (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> - branch_args -> unit Proofview.tactic +val case_tac : bool -> or_and_intro_pattern option -> + (intro_patterns -> named_context -> unit Proofview.tactic) -> + constr -> inductive * EInstance.t * EConstr.t array -> Id.t -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index b4def7bb51..26ae35a79d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -105,7 +105,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause = if Evar.Map.mem evk initial then false else Evar.Set.mem evk (Lazy.force newevars) in - let allowed_evars = AllowFun allowed in + let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in {flags with core_unify_flags = {flags.core_unify_flags with allowed_evars}; merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; @@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; @@ -1013,19 +1013,16 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) +type equality = { + eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); + (* equality data + A : Type, t1 : A, t2 : A *) + eq_clenv : clausenv; + (* clause [M : R A t1 t2] where [R] is the equality from above *) +} let eq_baseid = Id.of_string "e" -let apply_on_clause (f,t) clause = - let sigma = clause.evd in - let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in - let argmv = - (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> user_err (str "Ill-formed clause applicator.")) in - clenv_fchain ~with_univs:false argmv f_clause clause - -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1043,13 +1040,13 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow eqn Sorts.Relevant false_0 in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenv.clenv_value_cast_meta absurd_clause in + (* pf : eq t t1 t2 -> False *) + let pf = EConstr.mkApp (pf, [|clenv_value eq_clause|]) in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = +let discrEq eq = + let { eq_data = (_, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1058,7 +1055,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let info = Exninfo.reify () in tclZEROMSG ~info (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma eq cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1071,9 +1068,10 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in + let eq = { eq_data = (eq, eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) - (tac (eq,eqn,eq_args) eq_clause') + (tac eq) end let onNegatedEquality with_evars tac = @@ -1385,7 +1383,8 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t -let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = +let inject_at_positions env sigma l2r eq posns tac = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1395,11 +1394,12 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda (make_annot e Sorts.Relevant) t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in - let pf = applist(congr,[t;resty;injfun;t1;t2]) in + (* pf : eq t t1 t2 -> eq resty (injfun t1) (injfun t2) *) + let pf = mkApp (congr,[|t; resty; injfun; t1; t2|]) in let sigma, pf_typ = Typing.type_of env sigma pf in - let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = Clenv.clenv_value_cast_meta inj_clause in - let ty = simplify_args env sigma (clenv_type inj_clause) in + let pf_typ = Vars.subst1 mkProp (pi3 @@ destProd sigma pf_typ) in + let pf = mkApp (pf, [| Clenv.clenv_value eq_clause |]) in + let ty = simplify_args env sigma pf_typ in evdref := sigma; Some (pf, ty) with Failure _ -> None @@ -1422,7 +1422,8 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) -let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r eql = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1437,7 +1438,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] -> Proofview.tclZERO NothingToInject | Inr posns -> - inject_at_positions env sigma l2r u eq_clause posns + inject_at_positions env sigma l2r eql posns (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = @@ -1491,17 +1492,18 @@ let simpleInjClause flags with_evars = function let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac eq = + let { eq_data = (_, (_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma eq cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true eq posns (ntac (clenv_value clause)) end @@ -1513,10 +1515,11 @@ let dEq ~keep_proofs with_evars = dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decomp_eq tac data (c, t) = +let intro_decomp_eq tac (eq, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl + let eq = { eq_data = (eq, data); eq_clenv = cl } in + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end let () = declare_intro_decomp_eq intro_decomp_eq diff --git a/tactics/hints.ml b/tactics/hints.ml index db4b23705f..355cea8fa8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -837,7 +837,7 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = db = None; secvars; code = with_uid (Give_exact (c, cty, ctx, poly)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match EConstr.kind sigma cty with | Prod _ -> @@ -862,25 +862,11 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( db = None; secvars; code = with_uid (Res_pf(c,cty,ctx,poly)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then begin - let variables = str (CString.plural nmiss "variable") in - Feedback.msg_info ( - strbrk "The hint " ++ - pr_leconstr_env env sigma' c ++ - strbrk " will only be used by eauto, because applying " ++ - pr_leconstr_env env sigma' c ++ - strbrk " would leave " ++ variables ++ Pp.spc () ++ - Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ - strbrk " as unresolved existential " ++ variables ++ str "." - ) - end; + else (Some hd, { pri; pat = Some pat; name; db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx,poly)); }) - end | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose @@ -916,19 +902,25 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info ~check ~poly ?name cr = +let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = - try Some (f (c, cty, ctx)) with Failure _ -> None in + try + let (_, hint) as ans = f (c, cty, ctx) in + match hint.code.obj with + | ERes_pf _ -> if not eapply then None else Some ans + | _ -> Some ans + with Failure _ -> None + in let ents = List.map_filter try_apply [make_exact_entry env sigma info ~poly ?name; - make_apply_entry env sigma flags info ~poly ?name] + make_apply_entry env sigma hnf info ~poly ?name] in if check && List.is_empty ents then user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ - (if pi1 flags then str"cannot be used as a hint." + (if eapply then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents @@ -937,7 +929,7 @@ let make_resolve_hyp env sigma decl = let hname = NamedDecl.get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false + [make_apply_entry env sigma true empty_hint_info ~poly:false ~name:(PathHints [GlobRef.VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with @@ -1223,9 +1215,28 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,not !Flags.quiet) + make_resolves env sigma (true, hnf) pri ~check:true ~poly ~name:path gr) clist) in + let check (_, hint) = match hint.code.obj with + | ERes_pf (c, cty, ctx, _) -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + | _ -> () + in + let () = if not !Flags.quiet then List.iter check r in let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1375,10 +1386,10 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems + make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems let make_resolves env sigma info ~check ~poly ?name hint = - make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + make_resolves env sigma (true, false) info ~check ~poly ?name hint let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/inv.ml b/tactics/inv.ml index 4b94dd0e72..41899132a6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -409,7 +409,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> - let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in + let (depids,nodepids) = split_dep_and_nodep ba gl in let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with @@ -463,7 +463,7 @@ let raw_inversion inv_kind id status names = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in - let (ind, t) = + let ((ind, u), t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in @@ -474,13 +474,12 @@ let raw_inversion inv_kind id status names = let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in - let (cut_concl,case_tac) = - if status != NoDep && (local_occur_var sigma id concl) then - Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), - case_then_using + let dep = status != NoDep && (local_occur_var sigma id concl) in + let cut_concl = + if dep then + Reductionops.beta_applist sigma (elim_predicate, realargs@[c]) else - Reductionops.beta_applist sigma (elim_predicate, realargs), - case_nodep_then_using + Reductionops.beta_applist sigma (elim_predicate, realargs) in let refined id = let prf = mkApp (mkVar id, args) in @@ -488,13 +487,11 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in + let (_, args) = decompose_app_vect sigma t in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) - [case_tac names - (introCaseAssumsThen false (* ApplyOn not supported by inversion *) - (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c,t); + [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate (ind, u, args) id; onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ec770e2473..fc099f643d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -14,10 +14,8 @@ open Util open Names open Constr open EConstr -open Termops open Declarations open Tacmach -open Clenv open Tactypes module RelDecl = Context.Rel.Declaration @@ -335,18 +333,6 @@ let ifOnHyp pred tac1 tac2 id gl = used to keep track of some information about the ``branches'' of the elimination. *) -type branch_args = { - ity : pinductive; (* the type we were eliminating on *) - branchnum : int; (* the branch number *) - nassums : int; (* number of assumptions/letin to be introduced *) - branchsign : bool list; (* the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -401,15 +387,13 @@ let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns = let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true -let compute_induction_names_gen check_and branchletsigns = function +let compute_induction_names check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] | Some {CAst.loc;v=names} -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns -let compute_induction_names = compute_induction_names_gen true - (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = @@ -844,60 +828,6 @@ module New = struct tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) end - (* Find the right elimination suffix corresponding to the sort of the goal *) - (* c should be of type A1->.. An->B with B an inductive definition *) - let general_elim_then_using mk_elim - rec_flag allnames tac predicate ind (c, t) = - Proofview.Goal.enter begin fun gl -> - let sigma, elim = mk_elim ind gl in - let ind = on_snd (fun u -> EInstance.kind sigma u) ind in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.enter begin fun gl -> - let indclause = mk_clenv_from gl (c, t) in - (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in - let indmv = - match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> anomaly (str"elimination.") - in - let pmv = - let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in - match EConstr.kind elimclause.evd p with - | Meta p -> p - | _ -> - let name_elim = - match EConstr.kind sigma elim with - | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim - | _ -> mt () - in - user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ name_elim ++ str " is unknown.") - in - let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures ~rec_flag ind in - let brnames = compute_induction_names_gen false branchsigns allnames in - let flags = Unification.elim_flags () in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' - in - let after_tac i = - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = List.length branchsigns.(i); - branchnum = i+1; - ity = ind; } - in - tac ba - in - let branchtacs = List.init (Array.length branchsigns) after_tac in - Proofview.tclTHEN - (Clenv.res_pf ~flags elimclause') - (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end - let elimination_sort_of_goal gl = (* Retyping will expand evars anyway. *) let c = Proofview.Goal.concl gl in @@ -912,68 +842,6 @@ module New = struct | None -> elimination_sort_of_goal gl | Some id -> elimination_sort_of_hyp id gl - (* computing the case/elim combinators *) - - let gl_make_elim ind = begin fun gl -> - let env = Proofview.Goal.env gl in - let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in - let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, c) - end - - let gl_make_case_dep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind (project gl) u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let gl_make_case_nodep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind sigma u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let make_elim_branch_assumptions ba hyps = - let assums = - try List.rev (List.firstn ba.nassums hyps) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in - { ba = ba; assums = assums } - - let elim_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let case_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let elimination_then tac c = - Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in - let isrec,mkelim = - match (Global.lookup_mind (fst (fst ind))).mind_record with - | NotRecord -> true,gl_make_elim - | FakeRecord | PrimRecord _ -> false,gl_make_case_dep - in - general_elim_then_using mkelim isrec None tac None ind (c, t) - end - - let case_then_using = - general_elim_then_using gl_make_case_dep false - - let case_nodep_then_using = - general_elim_then_using gl_make_case_nodep false - let pf_constr_of_global ref = Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 48a06e6e1d..bfead34b3b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr open EConstr open Evd open Locus @@ -94,18 +93,6 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = private { - ity : pinductive; (** the type we were eliminating on *) - branchnum : int; (** the branch number *) - nassums : int; (** number of assumptions/letin to be introduced *) - branchsign : bool list; (** the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = private { - ba : branch_args; (** the branch args *) - assums : named_context} (** the list of assumptions introduced *) - (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern *) @@ -122,7 +109,7 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis (** Useful for [as intro_pattern] modifier *) val compute_induction_names : - bool list array -> or_and_intro_pattern option -> intro_patterns array + bool -> bool list array -> or_and_intro_pattern option -> intro_patterns array val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family @@ -249,20 +236,5 @@ module New : sig val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family - val elimination_then : - (branch_args -> unit Proofview.tactic) -> - constr -> unit Proofview.tactic - - val case_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val case_nodep_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 28e841d4ae..d33f3a5062 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function @@ -4394,7 +4394,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in - let names = compute_induction_names branchletsigns names in + let names = compute_induction_names true branchletsigns names in Array.iter (check_name_unicity env toclear []) names; let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) |