aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml432
1 files changed, 244 insertions, 188 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0864048f9..897285f25 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -42,6 +42,7 @@ open Eqschemes
open Locus
open Locusops
open Misctypes
+open Proofview.Notations
(* Options *)
@@ -131,7 +132,7 @@ let make_flags frzevars sigma flags clause =
let side_tac tac sidetac =
match sidetac with
| None -> tac
- | Some sidetac -> tclTHENSFIRSTn tac [|tclIDTAC|] sidetac
+ | Some sidetac -> Tacticals.New.tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac
let instantiate_lemma_all frzevars env gl c ty l l2r concl =
let eqclause = Clenv.make_clenv_binding gl (c,ty) l in
@@ -198,42 +199,52 @@ let rewrite_elim_in with_evars frzevars id c e gl =
(elimination_in_clause_scheme with_evars ~flags id) c e gl
(* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars frzevars cls rew elim =
+let general_elim_clause with_evars frzevars cls rew elim gl =
try
(match cls with
| None ->
(* was tclWEAK_PROGRESS which only fails for tactics generating one
subgoal and did not fail for useless conditional rewritings generating
an extra condition *)
- tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
- | Some id -> rewrite_elim_in with_evars frzevars id rew elim)
+ tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim) gl
+ | Some id -> rewrite_elim_in with_evars frzevars id rew elim gl)
with Pretype_errors.PretypeError (env,evd,
Pretype_errors.NoOccurrenceFound (c', _)) ->
raise (Pretype_errors.PretypeError
(env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
-let general_elim_clause with_evars frzevars tac cls c t l l2r elim gl =
+let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
let all, firstonly, tac =
match tac with
| None -> false, false, None
| Some (tac, Naive) -> false, false, Some tac
- | Some (tac, FirstSolved) -> true, true, Some (tclCOMPLETE tac)
- | Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac)
+ | Some (tac, FirstSolved) -> true, true, Some (Tacticals.New.tclCOMPLETE tac)
+ | Some (tac, AllMatches) -> true, false, Some (Tacticals.New.tclCOMPLETE tac)
in
let cs =
- (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
- (pf_env gl) gl c t l l2r
- (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id)
+ Goal.env >- fun env ->
+ Goal.concl >- fun concl ->
+ Tacmach.New.of_old (
+ (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
+ env ) >- fun instantiate_lemma ->
+ let typ =
+ match cls with None -> Goal.return concl | Some id -> Tacmach.New.pf_get_hyp_typ id
+ in
+ typ >- fun typ ->
+ Goal.return (instantiate_lemma c t l l2r typ)
in
let try_clause c =
side_tac
- (tclTHEN
- (Refiner.tclEVARS c.evd)
- (general_elim_clause with_evars frzevars cls c elim)) tac
+ (Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (Refiner.tclEVARS c.evd))
+ (Proofview.V82.tactic (general_elim_clause with_evars frzevars cls c elim)))
+ tac
in
+ cs >>- fun cs ->
if firstonly then
- tclFIRST (List.map try_clause cs) gl
- else tclMAP try_clause cs gl
+ Tacticals.New.tclFIRST (List.map try_clause cs)
+ else
+ Tacticals.New.tclMAP try_clause cs
(* The next function decides in particular whether to try a regular
rewrite or a generalized rewrite.
@@ -282,12 +293,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
begin
try
let _ = Global.lookup_constant c1' in
- mkConst c1', gl
+ mkConst c1', Declareops.no_seff
with Not_found ->
let rwr_thm = Label.to_string l' in
error ("Cannot find rewrite principle "^rwr_thm^".")
end
- | _ -> pr1, gl
+ | _ -> pr1, Declareops.no_seff
end
| _ ->
(* cannot occur since we checked that we are in presence of
@@ -309,22 +320,23 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
match kind_of_term hdcncl with
| Ind ind ->
let c, eff = find_scheme scheme_name ind in
- let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
- mkConst c, gl
+ mkConst c , eff
| _ -> assert false
-let type_of_clause gl = function
- | None -> pf_concl gl
- | Some id -> pf_get_hyp_typ gl id
+let type_of_clause = function
+ | None -> Goal.concl
+ | Some id -> Tacmach.New.pf_get_hyp_typ id
-let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok gl hdcncl =
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
- let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
- let elim, gl = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+ type_of_clause cls >>- fun type_of_cls ->
+ let dep = dep_proof_ok && dep_fun c type_of_cls in
+ Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) >>- fun (elim,effs) ->
+ Proofview.V82.tactic (Tactics.emit_side_effects effs) <*>
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
- {elimindex = None; elimbody = (elim,NoBindings)} gl
+ {elimindex = None; elimbody = (elim,NoBindings)}
let adjust_rewriting_direction args lft2rgt =
match args with
@@ -343,35 +355,42 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
(* Main function for dispatching which kind of rewriting it is about *)
let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
- ((c,l) : constr with_bindings) with_evars gl =
+ ((c,l) : constr with_bindings) with_evars =
if occs != AllOccurrences then (
- rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
+ rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- let env = pf_env gl in
- let sigma = project gl in
+ Goal.env >>- fun env ->
+ Goal.defs >>- fun sigma ->
let ctype = get_type_of env sigma c in
let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
match match_with_equality_type t with
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
- l with_evars frzevars dep_proof_ok gl hdcncl
+ l with_evars frzevars dep_proof_ok hdcncl
| None ->
- try
- rewrite_side_tac (Hook.get forward_general_rewrite_clause cls
- lft2rgt occs (c,l) ~new_goals:[]) tac gl
- with e when Errors.noncritical e ->
- (* Try to see if there's an equality hidden *)
- let e = Errors.push e in
- let env' = push_rel_context rels env in
- let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
- match match_with_equality_type t' with
- | Some (hdcncl,args) ->
+ Proofview.tclORELSE
+ begin
+ rewrite_side_tac (Hook.get forward_general_rewrite_clause cls
+ lft2rgt occs (c,l) ~new_goals:[]) tac
+ end
+ begin function
+ | e ->
+ (* Try to see if there's an equality hidden *)
+ (* spiwack: [Errors.push] here is unlikely to do
+ what it's intended to, or anything meaningful for
+ that matter. *)
+ let e = Errors.push e in
+ let env' = push_rel_context rels env in
+ let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+ match match_with_equality_type t' with
+ | Some (hdcncl,args) ->
let lft2rgt = adjust_rewriting_direction args lft2rgt in
- leibniz_rewrite_ebindings_clause cls lft2rgt tac c
- (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl hdcncl
- | None -> raise e
- (* error "The provided term does not end with an equality or a declared rewrite relation." *)
+ leibniz_rewrite_ebindings_clause cls lft2rgt tac c
+ (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
+ | None -> Proofview.tclZERO e
+ (* error "The provided term does not end with an equality or a declared rewrite relation." *)
+ end
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
@@ -406,35 +425,38 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
(* If a precise list of locations is given, success is mandatory for
each of these locations. *)
let rec do_hyps = function
- | [] -> tclIDTAC
+ | [] -> Proofview.tclUNIT ()
| ((occs,id),_) :: l ->
- tclTHENFIRST
+ Tacticals.New.tclTHENFIRST
(general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
(do_hyps l)
in
if cl.concl_occs == NoOccurrences then do_hyps l else
- tclTHENFIRST
- (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
- (do_hyps l)
+ Tacticals.New.tclTHENFIRST
+ (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
+ (do_hyps l)
| None ->
(* Otherwise, if we are told to rewrite in all hypothesis via the
syntax "* |-", we fail iff all the different rewrites fail *)
let rec do_hyps_atleastonce = function
- | [] -> (fun gl -> error "Nothing to rewrite.")
+ | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite."))
| id :: l ->
- tclIFTHENTRYELSEMUST
+ Tacticals.New.tclIFTHENTRYELSEMUST
(general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
(do_hyps_atleastonce l)
in
- let do_hyps gl =
+ let do_hyps =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids =
let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
- Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c (pf_ids_of_hyps gl)
- in do_hyps_atleastonce ids gl
+ Tacmach.New.pf_ids_of_hyps >- fun ids_of_hyps ->
+ Goal.return (Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps)
+ in
+ ids >>- fun ids ->
+ do_hyps_atleastonce ids
in
if cl.concl_occs == NoOccurrences then do_hyps else
- tclIFTHENTRYELSEMUST
+ Tacticals.New.tclIFTHENTRYELSEMUST
(general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
do_hyps
@@ -442,22 +464,24 @@ type delayed_open_constr_with_bindings =
env -> evar_map -> evar_map * constr with_bindings
let general_multi_multi_rewrite with_evars l cl tac =
- let do1 l2r f gl =
- let sigma,c = f (pf_env gl) (project gl) in
- Refiner.tclWITHHOLES with_evars
- (general_multi_rewrite l2r with_evars ?tac c) sigma cl gl in
+ let do1 l2r f =
+ Goal.env >>- fun env ->
+ Goal.defs >>- fun sigma ->
+ let sigma,c = f env sigma in
+ Tacticals.New.tclWITHHOLES with_evars
+ (general_multi_rewrite l2r with_evars ?tac c) sigma cl in
let rec doN l2r c = function
- | Precisely n when n <= 0 -> tclIDTAC
+ | Precisely n when n <= 0 -> Proofview.tclUNIT ()
| Precisely 1 -> do1 l2r c
- | Precisely n -> tclTHENFIRST (do1 l2r c) (doN l2r c (Precisely (n-1)))
- | RepeatStar -> tclREPEAT_MAIN (do1 l2r c)
- | RepeatPlus -> tclTHENFIRST (do1 l2r c) (doN l2r c RepeatStar)
- | UpTo n when n<=0 -> tclIDTAC
- | UpTo n -> tclTHENFIRST (tclTRY (do1 l2r c)) (doN l2r c (UpTo (n-1)))
+ | Precisely n -> Tacticals.New.tclTHENFIRST (do1 l2r c) (doN l2r c (Precisely (n-1)))
+ | RepeatStar -> Tacticals.New.tclREPEAT_MAIN (do1 l2r c)
+ | RepeatPlus -> Tacticals.New.tclTHENFIRST (do1 l2r c) (doN l2r c RepeatStar)
+ | UpTo n when n<=0 -> Proofview.tclUNIT ()
+ | UpTo n -> Tacticals.New.tclTHENFIRST (Tacticals.New.tclTRY (do1 l2r c)) (doN l2r c (UpTo (n-1)))
in
let rec loop = function
- | [] -> tclIDTAC
- | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
+ | [] -> Proofview.tclUNIT ()
+ | (l2r,m,c)::l -> Tacticals.New.tclTHENFIRST (doN l2r c m) (loop l)
in loop l
let rewriteLR = general_rewrite true AllOccurrences true true
@@ -471,43 +495,45 @@ let rewriteRL = general_rewrite false AllOccurrences true true
tac : Used to prove the equality c1 = c2
gl : goal *)
-let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
+let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
let try_prove_eq =
match try_prove_eq_opt with
- | None -> tclIDTAC
- | Some tac -> tclCOMPLETE tac
+ | None -> Proofview.tclUNIT ()
+ | Some tac -> Tacticals.New.tclCOMPLETE tac
in
- let t1 = pf_apply get_type_of gl c1
- and t2 = pf_apply get_type_of gl c2 in
- if unsafe || (pf_conv_x gl t1 t2) then
+ Tacmach.New.pf_apply get_type_of >>- fun get_type_of ->
+ let t1 = get_type_of c1
+ and t2 = get_type_of c2 in
+ Tacmach.New.pf_apply is_conv >>- fun is_conv ->
+ if unsafe || (is_conv t1 t2) then
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
let eq = applist (e, [t1;c1;c2]) in
- tclTHENS (assert_as false None eq)
- [onLastHypId (fun id ->
- tclTHEN
- (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
- (clear [id]));
- tclFIRST
- [assumption;
- tclTHEN (apply sym) assumption;
+ Tacticals.New.tclTHENS (assert_as false None eq)
+ [Tacticals.New.onLastHypId (fun id ->
+ Tacticals.New.tclTHEN
+ (Tacticals.New.tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
+ (Proofview.V82.tactic (clear [id])));
+ Tacticals.New.tclFIRST
+ [Proofview.V82.tactic assumption;
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) (Proofview.V82.tactic assumption);
try_prove_eq
]
- ] gl
+ ]
else
- error "Terms do not have convertible types."
+ Tacticals.New.tclFAIL 0 (str"Terms do not have convertible types.")
-let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
+let replace c2 c1 = multi_replace onConcl c2 c1 false None
-let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl
+let replace_in id c2 c1 = multi_replace (onHyp id) c2 c1 false None
-let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl
+let replace_by c2 c1 tac = multi_replace onConcl c2 c1 false (Some tac)
-let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl
+let replace_in_by id c2 c1 tac = multi_replace (onHyp id) c2 c1 false (Some tac)
-let replace_in_clause_maybe_by c2 c1 cl tac_opt gl =
- multi_replace cl c2 c1 false tac_opt gl
+let replace_in_clause_maybe_by c2 c1 cl tac_opt =
+ multi_replace cl c2 c1 false tac_opt
(* End of Eduardo's code. The rest of this file could be improved
using the functions match_with_equation, etc that I defined
@@ -760,13 +786,13 @@ let rec build_discriminator sigma env dirn c sort = function
Goal ~ c _ 0 0 = c _ 0 1. intro. discriminate H.
*)
-let gen_absurdity id gl =
- if is_empty_type (pf_get_hyp_typ gl id)
+let gen_absurdity id =
+ Tacmach.New.pf_get_hyp_typ id >>- fun hyp_typ ->
+ if is_empty_type hyp_typ
then
- simplest_elim (mkVar id) gl
+ simplest_elim (mkVar id)
else
- errorlabstrm "Equality.gen_absurdity"
- (str "Not the negation of an equality.")
+ Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
(* Precondition: eq is leibniz equality
@@ -804,7 +830,7 @@ let apply_on_clause (f,t) clause =
| _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
clenv_fchain argmv f_clause clause
-let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
let discriminator =
@@ -814,40 +840,48 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
let pf_ty = mkArrow eqn absurd_term in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = clenv_value_cast_meta absurd_clause in
- let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
- tclTHENS (cut_intro absurd_term)
- [onLastHypId gen_absurdity; refine pf] gl
+ Proofview.V82.tactic (Tactics.emit_side_effects eff) <*>
+ Tacticals.New.tclTHENS (cut_intro absurd_term)
+ [Tacticals.New.onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
-let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
+let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- let env = pf_env gls in
+ Goal.env >>- fun env ->
+ Goal.concl >>- fun concl ->
match find_positions env sigma t1 t2 with
| Inr _ ->
- errorlabstrm "discr" (str"Not a discriminable equality.")
+ Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
| Inl (cpath, (_,dirn), _) ->
- let sort = pf_apply get_type_of gls (pf_concl gls) in
- discr_positions env sigma u eq_clause cpath dirn sort gls
-
-let onEquality with_evars tac (c,lbindc) gls =
- let t = pf_type_of gls c in
- let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
- let eq_clause = make_clenv_binding gls (c,t') lbindc in
+ Tacmach.New.pf_apply get_type_of >>- fun get_type_of ->
+ let sort = get_type_of concl in
+ discr_positions env sigma u eq_clause cpath dirn sort
+
+let onEquality with_evars tac (c,lbindc) =
+ Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+ Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
+ let t = type_of c in
+ let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
+ Tacmach.New.of_old make_clenv_binding >>- fun make_clenv_binding ->
+ let eq_clause = make_clenv_binding (c,t') lbindc in
let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
let eqn = clenv_type eq_clause' in
- let eq,eq_args = find_this_eq_data_decompose gls eqn in
- tclTHEN
- (Refiner.tclEVARS eq_clause'.evd)
- (tac (eq,eqn,eq_args) eq_clause') gls
-
-let onNegatedEquality with_evars tac gls =
- let ccl = pf_concl gls in
- match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
+ Tacmach.New.of_old find_this_eq_data_decompose >>- fun find_this_eq_data_decompose ->
+ let eq,eq_args = find_this_eq_data_decompose eqn in
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
+ (tac (eq,eqn,eq_args) eq_clause')
+
+let onNegatedEquality with_evars tac =
+ Goal.concl >>- fun ccl ->
+ Goal.env >>- fun env ->
+ Goal.defs >>- fun sigma ->
+ match kind_of_term (hnf_constr env sigma ccl) with
| Prod (_,t,u) when is_empty_type u ->
- tclTHEN introf
- (onLastHypId (fun id ->
- onEquality with_evars tac (mkVar id,NoBindings))) gls
+ Tacticals.New.tclTHEN introf
+ (Tacticals.New.onLastHypId (fun id ->
+ onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
- errorlabstrm "" (str "Not a negated primitive equality.")
+ Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
let discrSimpleClause with_evars = function
| None -> onNegatedEquality with_evars discrEq
@@ -855,19 +889,19 @@ let discrSimpleClause with_evars = function
let discr with_evars = onEquality with_evars discrEq
-let discrClause with_evars = onClause (discrSimpleClause with_evars)
+let discrClause with_evars = Tacticals.New.onClause (discrSimpleClause with_evars)
let discrEverywhere with_evars =
(*
tclORELSE
*)
(if discr_do_intro () then
- (tclTHEN
- (tclREPEAT introf)
- (Tacticals.tryAllHyps
- (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclREPEAT introf)
+ (Tacticals.New.tryAllHyps
+ (fun id -> Tacticals.New.tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
- Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars))
+ Tacticals.New.tryAllHypsAndConcl (discrSimpleClause with_evars))
(* (fun gls ->
errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
*)
@@ -875,8 +909,8 @@ let discr_tac with_evars = function
| None -> discrEverywhere with_evars
| Some c -> onInductionArg (discr with_evars) c
-let discrConcl gls = discrClause false onConcl gls
-let discrHyp id gls = discrClause false (onHyp id) gls
+let discrConcl = discrClause false onConcl
+let discrHyp id = discrClause false (onHyp id)
(* returns the sigma type (sigS, sigT) with the respective
constructor depending on the sort *)
@@ -1131,12 +1165,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
in
let injectors = List.map_filter filter posns in
if List.is_empty injectors then
- errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
- tclTHEN
- (tclMAP
- (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
- (if l2r then List.rev injectors else injectors))
- (tac (List.length injectors))
+ Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
+ else
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (tclMAP
+ (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+ (if l2r then List.rev injectors else injectors)))
+ (tac (List.length injectors))
exception Not_dep_pair
@@ -1170,29 +1205,31 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[tclIDTAC; tclTHEN (apply (
mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
- )) (Auto.trivial [] [])
+ )) (Proofview.V82.of_tactic (Auto.trivial [] []))
] gl
(* not a dep eq or no decidable type found *)
end
else raise Not_dep_pair
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause gl =
+let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
match find_positions env sigma t1 t2 with
| Inl _ ->
- errorlabstrm "Inj"
- (str"Not a projectable equality but a discriminable one.")
+ Proofview.tclZERO (Errors.UserError ("Inj",str"Not a projectable equality but a discriminable one."))
| Inr [] ->
- errorlabstrm "Equality.inj"
- (str"Nothing to do, it is an equality between convertible terms.")
+ Proofview.tclZERO (Errors.UserError ("Equality.inj",str"Nothing to do, it is an equality between convertible terms."))
| Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
- errorlabstrm "Equality.inj" (str"Nothing to inject.")
+ Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
| Inr posns ->
- try inject_if_homogenous_dependent_pair env sigma u gl
- with Not_dep_pair as e | e when Errors.noncritical e ->
- inject_at_positions env sigma l2r u eq_clause posns
- (tac (clenv_value eq_clause)) gl
+ Proofview.tclORELSE
+ begin Proofview.V82.tactic (inject_if_homogenous_dependent_pair env sigma u) end
+ begin function
+ | Not_dep_pair as e |e when Errors.noncritical e ->
+ inject_at_positions env sigma l2r u eq_clause posns
+ (tac (clenv_value eq_clause))
+ | reraise -> Proofview.tclZERO reraise
+ end
let postInjEqTac ipats c n =
match ipats with
@@ -1207,14 +1244,14 @@ let postInjEqTac ipats c n =
else ipats in
tclTHEN
(clear_tac)
- (intros_pattern MoveLast ipats)
+ (Proofview.V82.of_tactic (intros_pattern MoveLast ipats))
| None -> tclIDTAC
let injEq ipats =
let l2r =
if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
in
- injEqThen (postInjEqTac ipats) l2r
+ injEqThen (fun c i -> Proofview.V82.tactic (postInjEqTac ipats c i)) l2r
let inj ipats with_evars = onEquality with_evars (injEq ipats)
@@ -1222,27 +1259,27 @@ let injClause ipats with_evars = function
| None -> onNegatedEquality with_evars (injEq ipats)
| Some c -> onInductionArg (inj ipats with_evars) c
-let injConcl gls = injClause None false None gls
-let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls
-
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
- let sort = pf_apply get_type_of gls (pf_concl gls) in
- let sigma = clause.evd in
- let env = pf_env gls in
- match find_positions env sigma t1 t2 with
- | Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u clause cpath dirn sort gls
- | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
- ntac (clenv_value clause) 0 gls
+let injConcl = injClause None false None
+let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
+
+let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
+ Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>- fun sort ->
+ let sigma = clause.evd in
+ Goal.env >>- fun env ->
+ match find_positions env sigma t1 t2 with
+ | Inl (cpath, (_,dirn), _) ->
+ discr_positions env sigma u clause cpath dirn sort
+ | 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
- (ntac (clenv_value clause)) gls
+ (ntac (clenv_value clause))
let dEqThen with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen ntac)
| Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
-let dEq with_evars = dEqThen with_evars (fun c x -> tclIDTAC)
+let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ())
let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac))
@@ -1266,7 +1303,7 @@ let swapEquandsInConcl gls =
let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
(* find substitution scheme *)
- let eq_elim, gls = find_elim lbeq.eq (Some false) false None None gls in
+ let eq_elim, effs = find_elim lbeq.eq (Some false) false None None gls in
(* build substitution predicate *)
let p = lambda_create (pf_env gls) (t,body) in
(* apply substitution scheme *)
@@ -1471,16 +1508,20 @@ let is_eq_x gl x (id,_,c) =
(* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
erase hyp and x; proceed by generalizing all dep hyps *)
-let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
+let subst_one dep_proof_ok x (hyp,rhs,dir) =
+ Goal.env >>- fun env ->
+ Goal.hyps >>- fun hyps ->
+ Goal.concl >>- fun concl ->
+ let hyps = Environ.named_context_of_val hyps in
(* The set of hypotheses using x *)
let depdecls =
let test (id,_,c as dcl) =
- if not (Id.equal id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl
+ if not (Id.equal id hyp) && occur_var_in_decl env x dcl then Some dcl
else None in
- List.rev (List.map_filter test (pf_hyps gl)) in
+ List.rev (List.map_filter test hyps) in
let dephyps = List.map (fun (id,_,_) -> id) depdecls in
(* Decides if x appears in conclusion *)
- let depconcl = occur_var (pf_env gl) x (pf_concl gl) in
+ let depconcl = occur_var env x concl in
(* The set of non-defined hypothesis: they must be abstracted,
rewritten and reintroduced *)
let abshyps =
@@ -1496,28 +1537,32 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
(Some (replace_term (mkVar x) rhs htyp)) nowhere
in
let need_rewrite = not (List.is_empty dephyps) || depconcl in
- tclTHENLIST
+ Tacticals.New.tclTHENLIST
((if need_rewrite then
- [generalize abshyps;
+ [Proofview.V82.tactic (generalize abshyps);
general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
- thin dephyps;
- tclMAP introtac depdecls]
+ Proofview.V82.tactic (thin dephyps);
+ (Tacticals.New.tclMAP introtac depdecls)]
else
- [tclIDTAC]) @
- [tclTRY (clear [x;hyp])]) gl
+ [Proofview.tclUNIT ()]) @
+ [Proofview.V82.tactic (tclTRY (clear [x;hyp]))])
(* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
-let subst_one_var dep_proof_ok x gl =
- let hyps = pf_hyps gl in
- let (_,xval,_) = pf_get_hyp gl x in
+(* arnaud: il va y avoir un bug là-dedans. Le try ne se déclenche pas
+ au bon endroit. Il faut convertir test en une Proofview.tactic
+ pour la gestion des exceptions. *)
+let subst_one_var dep_proof_ok x =
+ Goal.hyps >>- fun hyps ->
+ let hyps = Environ.named_context_of_val hyps in
+ Tacmach.New.pf_get_hyp x >>- fun (_,xval,_) ->
(* If x has a body, simply replace x with body and clear x *)
- if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) gl else
+ if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else
(* x is a variable: *)
let varx = mkVar x in
(* Find a non-recursive definition for x *)
- let (hyp,rhs,dir) =
+ let found gl =
try
let test hyp _ = is_eq_x gl varx hyp in
Context.fold_named_context test ~init:() hyps;
@@ -1525,10 +1570,11 @@ let subst_one_var dep_proof_ok x gl =
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
str".")
with FoundHyp res -> res in
- subst_one dep_proof_ok x (hyp,rhs,dir) gl
+ Tacmach.New.of_old found >>- fun (hyp,rhs,dir) ->
+ subst_one dep_proof_ok x (hyp,rhs,dir)
let subst_gen dep_proof_ok ids =
- tclTHEN tclNORMEVAR (tclMAP (subst_one_var dep_proof_ok) ids)
+ Tacticals.New.tclTHEN (Proofview.V82.tactic tclNORMEVAR) (Tacticals.New.tclMAP (subst_one_var dep_proof_ok) ids)
(* For every x, look for an hypothesis hyp of the form "x=rhs" or "rhs=x",
rewrite it everywhere, and erase hyp and x; proceed by generalizing
@@ -1547,10 +1593,12 @@ let default_subst_tactic_flags () =
else
{ only_leibniz = true; rewrite_dependent_proof = false }
-let subst_all ?(flags=default_subst_tactic_flags ()) gl =
+(* arnaud: encore des erreurs potentiels avec ces try/with *)
+let subst_all ?(flags=default_subst_tactic_flags ()) =
+ Tacmach.New.of_old find_eq_data_decompose >>- fun find_eq_data_decompose ->
let test (_,c) =
try
- let lbeq,(_,x,y) = find_eq_data_decompose gl c in
+ let lbeq,(_,x,y) = find_eq_data_decompose c in
if flags.only_leibniz then restrict_to_eq_and_identity lbeq.eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if eq_constr x y then failwith "caught";
@@ -1559,9 +1607,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) gl =
with PatternMatchingFailure -> failwith "caught"
in
let test p = try Some (test p) with Failure _ -> None in
- let ids = List.map_filter test (pf_hyps_types gl) in
+ Tacmach.New.pf_hyps_types >>- fun hyps ->
+ let ids = List.map_filter test hyps in
let ids = List.uniquize ids in
- subst_gen flags.rewrite_dependent_proof ids gl
+ subst_gen flags.rewrite_dependent_proof ids
(* Rewrite the first assumption for which the condition faildir does not fail
and gives the direction of the rewrite *)
@@ -1586,18 +1635,25 @@ let cond_eq_term c t gl =
else failwith "not convertible"
with PatternMatchingFailure -> failwith "not an equality"
-let rewrite_multi_assumption_cond cond_eq_term cl gl =
+let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t)
+let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
+let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t)
+
+(* arnaud: toujours des histoires de try/with *)
+let rewrite_multi_assumption_cond cond_eq_term cl =
let rec arec = function
| [] -> error "No such assumption."
| (id,_,t) ::rest ->
begin
try
- let dir = cond_eq_term t gl in
- general_multi_rewrite dir false (mkVar id,NoBindings) cl gl
+ cond_eq_term t >>- fun dir ->
+ general_multi_rewrite dir false (mkVar id,NoBindings) cl
with | Failure _ | UserError _ -> arec rest
end
in
- arec (pf_hyps gl)
+ Goal.hyps >>- fun hyps ->
+ let hyps = Environ.named_context_of_val hyps in
+ arec hyps
let replace_multi_term dir_opt c =
let cond_eq_fun =