aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrelim.ml64
-rw-r--r--plugins/ssr/ssrequality.ml17
-rw-r--r--plugins/ssr/ssripats.ml20
3 files changed, 64 insertions, 37 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 3fc05437da..94f7d24242 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -255,31 +255,49 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
(* Here we try to understand if the main pattern/term the user gave is
* the first pattern to be matched (i.e. if elimty ends in P t1 .. tn,
* weather tn is the t the user wrote in 'elim: t' *)
- let c_is_head_p, gl = match cty with
+ let c_is_head_p, gl =
+ match cty with
| None -> true, gl (* The user wrote elim: _ *)
| Some (c, c_ty, _) ->
- let res =
- (* we try to see if c unifies with the last arg of elim *)
- if elim_is_dep then None else
- let arg = List.assoc (n_elim_args - 1) elim_args in
- let gl, arg_ty = pfe_type_of gl arg in
- match saturate_until gl c c_ty (fun c c_ty gl ->
- pf_unify_HO (pf_unify_HO gl c_ty arg_ty) arg c) with
- | Some (c, _, _, gl) -> Some (false, gl)
- | None -> None in
- match res with
- | Some x -> x
- | None ->
- (* we try to see if c unifies with the last inferred pattern *)
- let inf_arg = List.hd inf_deps_r in
- let gl, inf_arg_ty = pfe_type_of gl inf_arg in
- match saturate_until gl c c_ty (fun _ c_ty gl ->
- pf_unify_HO gl c_ty inf_arg_ty) with
- | Some (c, _, _,gl) -> true, gl
- | None ->
- errorstrm Pp.(str"Unable to apply the eliminator to the term"++
- spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
- pr_econstr_env env (project gl) inf_arg_ty) in
+ let rec first = function
+ | [] ->
+ errorstrm Pp.(str"Unable to apply the eliminator to the term"++
+ spc()++pr_econstr_env env (project gl) c++spc())
+ | x :: rest ->
+ match x () with
+ | None -> first rest
+ | Some (b,gl) -> b, gl
+ in
+ (* Unify two terms if their heads are not applied unif variables, eg
+ * not (?P x). The idea is to rule out cases where the problem is too
+ * vague to drive the current heuristics. *)
+ let pf_unify_HO_rigid gl a b =
+ let is_applied_evar x = match EConstr.kind (project gl) x with
+ | App(x,_) -> EConstr.isEvar (project gl) x
+ | _ -> false in
+ if is_applied_evar a || is_applied_evar b then
+ raise Evarconv.(UnableToUnify(project gl,
+ Pretype_errors.ProblemBeyondCapabilities))
+ else pf_unify_HO gl a b in
+ let try_c_last_arg () =
+ (* we try to see if c unifies with the last arg of elim *)
+ if elim_is_dep then None else
+ let arg = List.assoc (n_elim_args - 1) elim_args in
+ let gl, arg_ty = pfe_type_of gl arg in
+ match saturate_until gl c c_ty (fun c c_ty gl ->
+ pf_unify_HO (pf_unify_HO_rigid gl c_ty arg_ty) arg c) with
+ | Some (c, _, _, gl) -> Some (false, gl)
+ | None -> None in
+ let try_c_last_pattern () =
+ (* we try to see if c unifies with the last inferred pattern *)
+ if inf_deps_r = [] then None else
+ let inf_arg = List.hd inf_deps_r in
+ let gl, inf_arg_ty = pfe_type_of gl inf_arg in
+ match saturate_until gl c c_ty (fun _ c_ty gl ->
+ pf_unify_HO_rigid gl c_ty inf_arg_ty) with
+ | Some (c, _, _,gl) -> Some(true, gl)
+ | None -> None in
+ first [try_c_last_arg;try_c_last_pattern] in
ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
let gl, predty = pfe_type_of gl pred in
(* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 15480c7a45..902098c8ce 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -325,7 +325,7 @@ let rec strip_prod_assum c = match Constr.kind c with
let rule_id = mk_internal_id "rewrite rule"
-exception PRtype_error
+exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
(* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
@@ -351,7 +351,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
(* We check the proof is well typed *)
let sigma, proof_ty =
- try Typing.type_of env sigma proof with _ -> raise PRtype_error in
+ try Typing.type_of env sigma proof with
+ | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
+ | e when CErrors.noncritical e -> raise (PRtype_error None)
+ in
ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
try refine_with
~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
@@ -423,13 +426,17 @@ let rwcltac cl rdx dir sr gl =
in
let cvtac' _ =
try cvtac gl with
- | PRtype_error ->
+ | PRtype_error e ->
+ let error = Option.cata (fun (env, sigma, te) ->
+ Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
+ (Pp.mt ()) e in
if occur_existential (project gl) (Tacmach.pf_concl gl)
- then errorstrm Pp.(str "Rewriting impacts evars")
+ then errorstrm Pp.(str "Rewriting impacts evars" ++ error)
else errorstrm Pp.(str "Dependent type error in rewrite of "
++ pr_constr_env (pf_env gl) (project gl)
(Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant)
- (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
+ (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))
+ ++ error)
in
tclTHEN cvtac' rwtac gl
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index e9fe1f3e48..3481b25c8b 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -369,18 +369,20 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
end end
(*** [=> [: id]] ************************************************************)
-[@@@ocaml.warning "-3"]
let mk_abstract_id =
let open Coqlib in
let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
-begin fun () ->
+begin fun env sigma ->
+ let sigma, zero = EConstr.fresh_global env sigma (lib_ref "num.nat.O") in
+ let sigma, succ = EConstr.fresh_global env sigma (lib_ref "num.nat.S") in
let rec nat_of_n n =
- if n = 0 then EConstr.mkConstruct path_of_O
- else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in
- incr ssr_abstract_id; nat_of_n !ssr_abstract_id
+ if n = 0 then zero
+ else EConstr.mkApp (succ, [|nat_of_n (n-1)|]) in
+ incr ssr_abstract_id;
+ sigma, nat_of_n !ssr_abstract_id
end
-let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
+let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
let env, concl = Goal.(env gl, concl gl) in
let step = begin fun sigma ->
let (sigma, (abstract_proof, abstract_ty)) =
@@ -389,8 +391,8 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
let (sigma, lock) = Evarutil.new_evar env sigma ablock in
let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
- let abstract_ty =
- EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
+ let (sigma, abstract_id) = mk_abstract_id env sigma in
+ let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
let sigma, m = Evarutil.new_evar env sigma abstract_ty in
sigma, (m, abstract_ty) in
let sigma, kont =
@@ -409,7 +411,7 @@ end
let tclMK_ABSTRACT_VARS ids =
List.fold_right (fun id tac ->
- Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
+ Tacticals.New.tclTHENFIRST (tclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
(* Debugging *)
let tclLOG p t =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:30:53 +0000