fix: elim/v handles eliminator from Derive Inversion (issue #2)

Also:
- fix elim trying to saturate too much and not raising the expected exn
- fix fill_occ_pattern when occ is {-}, it used to lose the
  instantiation obtained by matching the term

5 files changed, 101 insertions, 42 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index fc895a5..e82272e 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -3381,7 +3381,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
         (Reductionops.whd_betadeltaiota env sigma) ty in
       match kind_of_type ty with
       | ProdType _ -> loop ty args sigma n
-      | _ -> anomaly "saturate did not find enough products"
+      | _ -> raise NotEnoughProducts
   in
    loop ty [] sigma m
 
@@ -3904,7 +3904,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    pp(lazy(str"matching: " ++ pp_pattern p));
+    pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in
     pp(lazy(str"     got: " ++ pr_constr c));
@@ -3924,6 +3924,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
        with e when Errors.noncritical e -> p in
   (* finds the eliminator applies it to evars and c saturated as needed  *)
   (* obtaining "elim ??? (c ???)". pred is the higher order evar         *)
+  (* cty is None when the user writes _ (hence we can't make a pattern *)
   let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl =
     match elim with
     | Some elim ->
@@ -3934,7 +3935,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in
-      None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
+      let cty, gl =
+        if Option.is_empty oc then None, gl
+        else
+          let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
+          let pc = match c_gen with
+            | Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+            | _ -> mkTpat gl c in
+          Some(c, c_ty, pc), gl in
+      cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
     | None ->
       let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
       let ((kn, i) as ind, _ as indu), unfolded_c_ty =
@@ -3964,7 +3973,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
   pp(lazy(str"elim= "++ pr_constr_pat elim));
-  pp(lazy(str"elimty= "++ pr_constr elimty));
+  pp(lazy(str"elimty= "++ pr_constr_pat elimty));
   let inf_deps_r = match kind_of_type elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -3973,11 +3982,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in
       let gl' = f c c_ty gl in
       Some (c, c_ty, gl, gl')
-    with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in
-  let elim_is_dep, gl = match cty with
-    | None -> true, gl
+    with
+    | NotEnoughProducts -> None
+    | e when Errors.noncritical e -> loop (n+1) in loop 0 in
+  (* 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
+    | 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 = pf_type_of gl arg in
@@ -3988,21 +4003,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
     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 = pf_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 (str"Unable to apply the eliminator to the term"++
-      spc()++pr_constr c++spc()++str"or to unify it's type with"++
-      pr_constr inf_arg_ty) in
-  pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep));
+        errorstrm (str"Unable to apply the eliminator to the term"++
+          spc()++pr_constr c++spc()++str"or to unify it's type with"++
+          pr_constr inf_arg_ty) in
+  pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pf_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,_) = pp_pattern p in
+  let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in
   let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
@@ -4018,12 +4034,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c));
+          pp(lazy(str"adding inf pattern " ++ pr_constr_pat c));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm (str "Too many dependent abstractions") in
-    let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with
-    | `EConstr _, _, None -> anomaly "Simple welim with no term"
+    let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
+    | `EConstr _, _, None -> anomaly "Simple elim with no term"
     | _, false, _ -> deps, [], inf_deps_r
     | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r
     | _, true, Some (c, _, pc) ->
@@ -4083,7 +4099,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
           apply_type new_concl [erefl], gl in
-        let rel = k + if elim_is_dep then 1 else 0 in
+        let rel = k + if c_is_head_p then 1 else 0 in
         let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in
         let concl = mkArrow src (lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index b697050..aa44fec 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -776,7 +776,7 @@ let rec uniquize = function
   let sigma, _, ({up_f = pf; up_a = pa} as u) =
     if all_instances then assert_done_multires upat_that_matched
     else List.hd (snd(assert_done upat_that_matched)) in
-  pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma));
+(*   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *)
   if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
   let pn = Array.length pa in
@@ -846,7 +846,7 @@ let pr_pattern_aux pr_constr = function
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p
+  pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
@@ -1192,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
-  let find_R, conclude = let r = ref None in
-    (fun env c _ h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context);
-                     mkRel (h'+h-1)),
+  let do_make_rel, occ =
+    if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in
+  let find_R, conclude =
+    let r = ref None in
+    (fun env c _ h' ->
+       do_once r (fun () -> c, Evd.empty_evar_universe_context);
+       if do_make_rel then mkRel (h'+h-1) else c),
     (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in
   let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in
   let e = conclude cl in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 9452aa2..d0a430a 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -3375,7 +3375,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
         (Reductionops.whd_betadeltaiota env sigma) ty in
       match kind_of_type ty with
       | ProdType _ -> loop ty args sigma n
-      | _ -> anomaly "saturate did not find enough products"
+      | _ -> raise NotEnoughProducts
   in
    loop ty [] sigma m
 
@@ -3898,7 +3898,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    pp(lazy(str"matching: " ++ pp_pattern p));
+    pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in
     pp(lazy(str"     got: " ++ pr_constr c));
@@ -3918,6 +3918,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
        with e when Errors.noncritical e -> p in
   (* finds the eliminator applies it to evars and c saturated as needed  *)
   (* obtaining "elim ??? (c ???)". pred is the higher order evar         *)
+  (* cty is None when the user writes _ (hence we can't make a pattern *)
   let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl =
     match elim with
     | Some elim ->
@@ -3928,7 +3929,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in
-      None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
+      let cty, gl =
+        if Option.is_empty oc then None, gl
+        else
+          let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
+          let pc = match c_gen with
+            | Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+            | _ -> mkTpat gl c in
+          Some(c, c_ty, pc), gl in
+      cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
     | None ->
       let c = Option.get oc in let gl, c_ty = pf_type_of gl c in
       let ((kn, i) as ind, _ as indu), unfolded_c_ty =
@@ -3958,7 +3967,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
   pp(lazy(str"elim= "++ pr_constr_pat elim));
-  pp(lazy(str"elimty= "++ pr_constr elimty));
+  pp(lazy(str"elimty= "++ pr_constr_pat elimty));
   let inf_deps_r = match kind_of_type elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -3967,11 +3976,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in
       let gl' = f c c_ty gl in
       Some (c, c_ty, gl, gl')
-    with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in
-  let elim_is_dep, gl = match cty with
-    | None -> true, gl
+    with
+    | NotEnoughProducts -> None
+    | e when Errors.noncritical e -> loop (n+1) in loop 0 in
+  (* 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
+    | 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 = pf_type_of gl arg in
@@ -3982,21 +3997,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
     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 = pf_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 (str"Unable to apply the eliminator to the term"++
-      spc()++pr_constr c++spc()++str"or to unify it's type with"++
-      pr_constr inf_arg_ty) in
-  pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep));
+        errorstrm (str"Unable to apply the eliminator to the term"++
+          spc()++pr_constr c++spc()++str"or to unify it's type with"++
+          pr_constr inf_arg_ty) in
+  pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pf_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,_) = pp_pattern p in
+  let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in
   let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
@@ -4012,12 +4028,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c));
+          pp(lazy(str"adding inf pattern " ++ pr_constr_pat c));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm (str "Too many dependent abstractions") in
-    let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with
-    | `EConstr _, _, None -> anomaly "Simple welim with no term"
+    let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with
+    | `EConstr _, _, None -> anomaly "Simple elim with no term"
     | _, false, _ -> deps, [], inf_deps_r
     | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r
     | _, true, Some (c, _, pc) ->
@@ -4077,7 +4093,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
           apply_type new_concl [erefl], gl in
-        let rel = k + if elim_is_dep then 1 else 0 in
+        let rel = k + if c_is_head_p then 1 else 0 in
         let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in
         let concl = mkArrow src (lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index 7a58c61..74f42f6 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -776,7 +776,7 @@ let rec uniquize = function
   let sigma, _, ({up_f = pf; up_a = pa} as u) =
     if all_instances then assert_done_multires upat_that_matched
     else List.hd (snd(assert_done upat_that_matched)) in
-  pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma));
+(*   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *)
   if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
   let pn = Array.length pa in
@@ -846,7 +846,7 @@ let pr_pattern_aux pr_constr = function
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p
+  pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
@@ -1192,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
-  let find_R, conclude = let r = ref None in
-    (fun env c _ h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context);
-                     mkRel (h'+h-1)),
+  let do_make_rel, occ =
+    if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in
+  let find_R, conclude =
+    let r = ref None in
+    (fun env c _ h' ->
+       do_once r (fun () -> c, Evd.empty_evar_universe_context);
+       if do_make_rel then mkRel (h'+h-1) else c),
     (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in
   let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in
   let e = conclude cl in
diff --git a/mathcomp/ssrtest/derive_inversion.v b/mathcomp/ssrtest/derive_inversion.v
new file mode 100644
index 0000000..71257d8
--- /dev/null
+++ b/mathcomp/ssrtest/derive_inversion.v
@@ -0,0 +1,19 @@
+Require Import ssreflect ssrbool.
+
+Set Implicit Arguments.
+
+  Inductive wf T : bool -> option T -> Type :=
+  | wf_f : wf false None
+  | wf_t : forall x, wf true (Some x).
+
+  Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop.
+
+  Lemma Problem T b (o : option T) :
+    wf b o ->
+    match b with
+    | true  => exists x, o = Some x
+    | false => o = None
+    end.
+  Proof.
+  by case: b; elim/wf_inv=>//;case: o=>// a *; exists a.
+  Qed.