diff options
Diffstat (limited to 'ltac')
-rw-r--r-- | ltac/extratactics.ml4 | 115 |
1 files changed, 70 insertions, 45 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index f87aa407d..d53248a04 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -340,6 +340,9 @@ END (**********************************************************************) (* Refine *) +open EConstr +open Vars + let constr_flags = { Pretyping.use_typeclasses = true; Pretyping.use_unif_heuristics = true; @@ -396,8 +399,6 @@ VERNAC COMMAND EXTEND DeriveInversionClear -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] END -open Term - VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] => [ seff na ] @@ -494,7 +495,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity : bool * constr -> obj = +let inTransitivity : bool * Constr.constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); @@ -646,6 +647,7 @@ let hResolve id c occ t = let sigma = Sigma.to_evar_map sigma in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in let env_ids = Termops.ids_of_context env in let c_raw = Detyping.detype true env_ids env sigma c in let t_raw = Detyping.detype true env_ids env sigma t in @@ -659,10 +661,12 @@ let hResolve id c occ t = resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in + let t_constr = EConstr.of_constr t_constr in let sigma = Evd.merge_universe_context sigma ctx in - let t_constr_type = Retyping.get_type_of env sigma (EConstr.of_constr t_constr) in + let t_constr_type = Retyping.get_type_of env sigma t_constr in + let t_constr_type = EConstr.of_constr t_constr_type in let tac = - (change_concl (EConstr.of_constr (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))) + (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) in Sigma.Unsafe.of_pair (tac, sigma) end } @@ -691,12 +695,14 @@ let hget_evar n = let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list concl in + let concl = EConstr.of_constr concl in if List.length evl < n then error "Not enough uninstantiated existential variables."; if n <= 0 then error "Incorrect existential variable index."; let ev = List.nth evl (n-1) in + let ev = (fst ev, Array.map EConstr.of_constr (snd ev)) in let ev_type = existential_type sigma ev in - change_concl (EConstr.of_constr (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))) + change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) end } TACTIC EXTEND hget_evar @@ -719,7 +725,7 @@ let rewrite_except h = Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else - Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (EConstr.mkVar h) false)) + Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) hyps end } @@ -736,18 +742,20 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in + let type_of_a = EConstr.of_constr type_of_a in Tacticals.New.tclTHENLIST - [Tactics.generalize [EConstr.of_constr (mkApp(delayed_force refl_equal, [| type_of_a; a|]))]; + [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], EConstr.of_constr a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in + let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in let c = EConstr.of_constr c in change_concl c end }; - simplest_case (EConstr.of_constr a)] + simplest_case a] end } @@ -770,36 +778,38 @@ let case_eq_intros_rewrite x = ] end } -let rec find_a_destructable_match t = +let rec find_a_destructable_match sigma t = let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in let cl = [cl, (None, None), None], None in let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in - match kind_of_term t with - | Case (_,_,x,_) when closed0 x -> - if isVar x then + match EConstr.kind sigma t with + | Case (_,_,x,_) when closed0 sigma x -> + if isVar sigma x then (* TODO check there is no rel n. *) raise (Found (Tacinterp.eval_tactic dest)) else (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) raise (Found (case_eq_intros_rewrite x)) - | _ -> iter_constr find_a_destructable_match t + | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t let destauto t = - try find_a_destructable_match t; + Proofview.tclEVARMAP >>= fun sigma -> + try find_a_destructable_match sigma t; Tacticals.New.tclZEROMSG (str "No destructable match found") with Found tac -> tac let destauto_in id = Proofview.Goal.nf_enter { enter = begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in + let ctype = EConstr.of_constr ctype in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype end } TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] +| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (EConstr.of_constr (Proofview.Goal.concl gl)) end } ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END @@ -819,21 +829,24 @@ END TACTIC EXTEND constr_eq_nounivs | [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ - if eq_constr_nounivs x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] + Proofview.tclEVARMAP >>= fun sigma -> + let x = EConstr.of_constr x in + let y = EConstr.of_constr y in + if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] END TACTIC EXTEND is_evar -| [ "is_evar" constr(x) ] -> - [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> - match Evarutil.kind_of_term_upto sigma x with - | Evar _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") - end +| [ "is_evar" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with + | Evar _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") ] END +let has_evar sigma c = let rec has_evar x = - match kind_of_term x with + match EConstr.kind sigma x with | Evar _ -> true | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ -> false @@ -852,57 +865,68 @@ and has_evar_array x = Array.exists has_evar x and has_evar_prec (_, ts1, ts2) = Array.exists has_evar ts1 || Array.exists has_evar ts2 +in +has_evar c TACTIC EXTEND has_evar -| [ "has_evar" constr(x) ] -> - [ if has_evar x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") ] +| [ "has_evar" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + if has_evar sigma (EConstr.of_constr x) then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") +] END TACTIC EXTEND is_hyp -| [ "is_var" constr(x) ] -> - [ match kind_of_term x with +| [ "is_var" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Var _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] END TACTIC EXTEND is_fix -| [ "is_fix" constr(x) ] -> - [ match kind_of_term x with +| [ "is_fix" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Fix _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] END;; TACTIC EXTEND is_cofix -| [ "is_cofix" constr(x) ] -> - [ match kind_of_term x with +| [ "is_cofix" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | CoFix _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] END;; TACTIC EXTEND is_ind -| [ "is_ind" constr(x) ] -> - [ match kind_of_term x with +| [ "is_ind" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Ind _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ] END;; TACTIC EXTEND is_constructor -| [ "is_constructor" constr(x) ] -> - [ match kind_of_term x with +| [ "is_constructor" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Construct _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ] END;; TACTIC EXTEND is_proj -| [ "is_proj" constr(x) ] -> - [ match kind_of_term x with +| [ "is_proj" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Proj _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ] END;; TACTIC EXTEND is_const -| [ "is_const" constr(x) ] -> - [ match kind_of_term x with +| [ "is_const" constr(x) ] -> [ + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma (EConstr.of_constr x) with | Const _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ] END;; @@ -1046,8 +1070,9 @@ END let decompose l c = Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let to_ind c = - if isInd c then Univ.out_punivs (destInd c) + if isInd sigma c then Univ.out_punivs (destInd sigma c) else error "not an inductive type" in let l = List.map to_ind l in @@ -1055,7 +1080,7 @@ let decompose l c = end } TACTIC EXTEND decompose -| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l (EConstr.of_constr c) ] +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose (List.map EConstr.of_constr l) (EConstr.of_constr c) ] END (** library/keys *) |