diff options
| -rwxr-xr-x | dev/tools/backport-pr.sh | 30 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 64 | ||||
| -rw-r--r-- | test-suite/ssr/elim_noquant.v | 29 |
3 files changed, 88 insertions, 35 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 9864fd4d69..1ec8251f66 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -30,13 +30,15 @@ while [[ $# -gt 0 ]]; do esac done -if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then +MASTER=origin/master + +if ! git log $MASTER --grep "Merge PR #$PRNUM" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." exit 1 fi -SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?") -git log master --grep "Merge PR #${PRNUM}" --format="%GG" +SIGNATURE_STATUS=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%G?") +git log $MASTER --grep "Merge PR #$PRNUM" --format="%GG" if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then echo read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r @@ -47,10 +49,18 @@ if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then fi BRANCH=backport-pr-${PRNUM} -RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../') -MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/') +RANGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%P" | sed 's/ /../') +MESSAGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%s" | sed 's/Merge/Backport/') -if git checkout -b "${BRANCH}"; then +if [[ "$(git rev-parse --abbrev-ref HEAD)" == "$BRANCH" ]]; then + + if ! git cherry-pick --continue; then + echo "Please fix the conflicts, then relaunch the script." + exit 1 + fi + git checkout - + +elif git checkout -b "$BRANCH"; then if ! git cherry-pick -x "${RANGE}"; then if [[ "$NO_CONFLICTS" == "true" ]]; then @@ -61,12 +71,8 @@ if git checkout -b "${BRANCH}"; then git branch -d "$BRANCH" exit 1 fi - echo "Please fix the conflicts, then exit." - bash - while ! git cherry-pick --continue; do - echo "Please fix the conflicts, then exit." - bash - done + echo "Please fix the conflicts, then relaunch the script." + exit 1 fi git checkout - 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/test-suite/ssr/elim_noquant.v b/test-suite/ssr/elim_noquant.v new file mode 100644 index 0000000000..e6662203e9 --- /dev/null +++ b/test-suite/ssr/elim_noquant.v @@ -0,0 +1,29 @@ +Require Import ssreflect. + + +Axiom app : forall T, list T -> list T -> list T. +Arguments app {_}. +Infix "++" := app. + +Lemma test (aT rT : Type) + (pmap : (aT -> option rT) -> list aT -> list rT) + (perm_eq : list rT -> list rT -> Prop) + (f : aT -> option rT) + (g : rT -> aT) + (s t : list aT) + (E : forall T : list aT -> Type, + (forall s1 s2 s3 : list aT, + T (s1 ++ s2 ++ s3) -> T (s2 ++ s1 ++ s3)) -> + T s -> T t) : + perm_eq (pmap f s) (pmap f t). +Proof. +elim/E: (t). +Admitted. + + +Lemma test2 (a b : nat) : a = b -> b = 1. +Proof. +elim. +match goal with |- a = 1 => idtac end. +Admitted. + |