Merge PR #8509: Fix numerous anomalies with Scheme Equality

6 files changed, 105 insertions, 43 deletions

diff --git a/test-suite/bugs/closed/4612.v b/test-suite/bugs/closed/4612.v
new file mode 100644
index 0000000000..ce95f26acc
--- /dev/null
+++ b/test-suite/bugs/closed/4612.v
@@ -0,0 +1,7 @@
+(* While waiting for support, check at least that it does not raise an anomaly *)
+
+Inductive ctype :=
+| Struct: list ctype -> ctype
+| Bot : ctype.
+
+Fail Scheme Equality for ctype.
diff --git a/test-suite/bugs/closed/4859.v b/test-suite/bugs/closed/4859.v
new file mode 100644
index 0000000000..7be0bedcfc
--- /dev/null
+++ b/test-suite/bugs/closed/4859.v
@@ -0,0 +1,7 @@
+(* Not supported but check at least that it does not raise an anomaly *)
+
+Inductive Fin{n : nat} : Set :=
+| F1{i : nat}{e : n = S i}
+| FS{i : nat}(f : @ Fin i){e : n = S i}.
+
+Fail Scheme Equality for Fin.
diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
new file mode 100644
index 0000000000..85d5c3e123
--- /dev/null
+++ b/test-suite/success/SchemeEquality.v
@@ -0,0 +1,29 @@
+(* Examples of use of Scheme Equality *)
+
+Module A.
+Definition N := nat.
+Inductive list := nil | cons : N -> list -> list.
+Scheme Equality for list.
+End A.
+
+Module B.
+  Section A.
+    Context A (eq_A:A->A->bool)
+            (A_bl : forall x y, eq_A x y = true -> x = y)
+            (A_lb : forall x y, x = y -> eq_A x y = true).
+    Inductive I := C : A -> I.
+    Scheme Equality for I.
+  End A.
+End B.
+
+Module C.
+  Parameter A : Type.
+  Parameter eq_A : A->A->bool.
+  Parameter A_bl : forall x y, eq_A x y = true -> x = y.
+  Parameter A_lb : forall x y, x = y -> eq_A x y = true.
+  Hint Resolve A_bl A_lb : core.
+  Inductive I := C : A -> I.
+  Scheme Equality for I.
+  Inductive J := D : list A -> J.
+  Scheme Equality for J.
+End C.
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 3bf3925b4b..dee7541d37 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -59,6 +59,8 @@ exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
+exception ConstructorWithNonParametricInductiveType of inductive
+exception DecidabilityIndicesNotSupported
 
 let constr_of_global g = lazy (UnivGen.constr_of_global g)
 
@@ -120,6 +122,10 @@ let check_bool_is_defined () =
   try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
+let check_no_indices mib =
+  if Array.exists (fun mip -> mip.mind_nrealargs <> 0) mib.mind_packets then
+    raise DecidabilityIndicesNotSupported
+
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
 let build_beq_scheme mode kn =
@@ -133,6 +139,7 @@ let build_beq_scheme mode kn =
   (* number of params in the type *)
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
+  check_no_indices mib;
   (* params context divided *)
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
@@ -193,6 +200,7 @@ let build_beq_scheme mode kn =
         match Constr.kind c with
         | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
         | Var x ->
+          (* Support for working in a context with "eq_x : x -> x -> bool" *)
           let eid = Id.of_string ("eq_"^(Id.to_string x)) in
           let () =
             try ignore (Environ.lookup_named eid env)
@@ -225,9 +233,17 @@ let build_beq_scheme mode kn =
         | Lambda _-> raise (EqUnknown "abstraction")
         | LetIn _ -> raise (EqUnknown "let-in")
         | Const (kn, u) ->
-	    (match Environ.constant_opt_value_in env (kn, u) with
-	      | None -> raise (ParameterWithoutEquality (ConstRef kn))
-              | Some c -> aux (Term.applist (c,a)))
+             (match Environ.constant_opt_value_in env (kn, u) with
+              | Some c -> aux (Term.applist (c,a))
+              | None ->
+                 (* Support for working in a context with "eq_x : x -> x -> bool" *)
+                 (* Needs Hints, see test suite *)
+                 let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in
+                 let kneq = Constant.change_label kn eq_lbl in
+                 try let _ = Environ.constant_opt_value_in env (kneq, u) in
+                   Term.applist (mkConst kneq,a),
+                   Safe_typing.empty_private_constants
+                 with Not_found -> raise (ParameterWithoutEquality (ConstRef kn)))
         | Proj _ -> raise (EqUnknown "projection")
         | Construct _ -> raise (EqUnknown "constructor")
         | Case _ -> raise (EqUnknown "match")
@@ -341,13 +357,10 @@ let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
 (* This function tryies to get the [inductive] between a constr
   the constr should be Ind i or App(Ind i,[|args|])
 *)
-let destruct_ind sigma c =
+let destruct_ind env sigma c =
   let open EConstr in
-    try let u,v =  destApp sigma c in
-          let indc = destInd sigma u in
-            indc,v
-    with DestKO -> let indc = destInd sigma c in
-            indc,[||]
+  let (c,v) = Reductionops.whd_all_stack env sigma c in
+  destInd sigma c, Array.of_list v
 
 (*
   In the following, avoid is the list of names to avoid.
@@ -361,10 +374,10 @@ so from Ai we can find the correct eq_Ai bl_ai or lb_ai
 let do_replace_lb mode lb_scheme_key aavoid narg p q =
   let open EConstr in
   let avoid = Array.of_list aavoid in
-  let do_arg sigma v offset =
-  try
+  let do_arg sigma hd v offset =
+    match kind sigma v with
+    | Var s ->
     let x = narg*offset in
-    let s = destVar sigma v in
     let n = Array.length avoid in
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -373,22 +386,20 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
                    (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
-  with e when CErrors.noncritical e ->
-      (* if this happen then the args have to be already declared as a
-              Parameter*)
-      (
-        let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
-          mkConst (Constant.make3 mp dir (Label.make (
-          if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
-                       else ((Label.to_string lbl)^"_lb")
-        )))
-      )
+    | Const (cst,_) ->
+      (* Works in specific situations where the args have to be already declared as a
+         Parameter (see example "J" in test file SchemeEquality.v) *)
+        let lbl = Label.to_string (Constant.label cst) in
+        let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_lb") in
+        mkConst (Constant.change_label cst (Label.make newlbl))
+    | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
+
   in
   Proofview.Goal.enter begin fun gl ->
     let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
     let sigma = Tacmach.New.project gl in
     let env = Tacmach.New.pf_env gl in
-    let u,v = destruct_ind sigma type_of_pq
+    let u,v = destruct_ind env sigma type_of_pq
     in let lb_type_of_p =
         try
           let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
@@ -409,8 +420,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
        Proofview.tclEVARMAP >>= fun sigma ->
        let lb_args = Array.append (Array.append
                           v
-                          (Array.Smart.map (fun x -> do_arg sigma x 1) v))
-                          (Array.Smart.map (fun x -> do_arg sigma x 2) v)
+                          (Array.Smart.map (fun x -> do_arg sigma u x 1) v))
+                          (Array.Smart.map (fun x -> do_arg sigma u x 2) v)
         in let app =  if Array.is_empty lb_args
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
            in
@@ -419,14 +430,14 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
              Equality.replace p q ; apply app ; Auto.default_auto]
   end
 
-(* used in the bool -> leib side *)
+(* used in the bool -> leb side *)
 let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let open EConstr in
   let avoid = Array.of_list aavoid in
-  let do_arg sigma v offset =
-  try
+  let do_arg sigma hd v offset =
+    match kind sigma v with
+    | Var s ->
     let x = narg*offset in
-    let s = destVar sigma v in
     let n = Array.length avoid in
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -435,16 +446,13 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                    (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
-  with e when CErrors.noncritical e ->
-      (* if this happen then the args have to be already declared as a
-         Parameter*)
-      (
-        let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
-          mkConst (Constant.make3 mp dir (Label.make (
-          if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
-                       else ((Label.to_string lbl)^"_bl")
-        )))
-      )
+    | Const (cst,_) ->
+      (* Works in specific situations where the args have to be already declared as a
+         Parameter (see example "J" in test file SchemeEquality.v) *)
+        let lbl = Label.to_string (Constant.label cst) in
+        let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_bl") in
+        mkConst (Constant.change_label cst (Label.make newlbl))
+    | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
   in
 
   let rec aux l1 l2 =
@@ -456,7 +464,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         let env = Tacmach.New.pf_env gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
         else (
-          let u,v = try  destruct_ind sigma tt1
+          let u,v = try destruct_ind env sigma tt1
           (* trick so that the good sequence is returned*)
                 with e when CErrors.noncritical e -> indu,[||]
           in if eq_ind (fst u) ind
@@ -480,8 +488,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                in let bl_args =
                         Array.append (Array.append
                           v
-                          (Array.Smart.map (fun x -> do_arg sigma x 1) v))
-                          (Array.Smart.map (fun x -> do_arg sigma x 2) v )
+                          (Array.Smart.map (fun x -> do_arg sigma u x 1) v))
+                          (Array.Smart.map (fun x -> do_arg sigma u x 2) v )
                 in
                 let app =  if Array.is_empty bl_args
                            then bl_t1 else mkApp (bl_t1,bl_args)
diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli
index 11f26c7c36..647ff3d8d6 100644
--- a/vernac/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
@@ -27,6 +27,8 @@ exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
+exception ConstructorWithNonParametricInductiveType of inductive
+exception DecidabilityIndicesNotSupported
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e86e108772..0a74a8cc4a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -142,7 +142,8 @@ let try_declare_scheme what f internal names kn =
   try f internal names kn
   with e ->
   let e = CErrors.push e in
-  let msg = match fst e with
+  let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
+  let msg = match extract_exn (fst e) with
     | ParameterWithoutEquality cst ->
 	alarm what internal
 	  (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
@@ -176,6 +177,14 @@ let try_declare_scheme what f internal names kn =
     | NoDecidabilityCoInductive ->
          alarm what internal
            (str "Scheme Equality is only for inductive types.")
+    | DecidabilityIndicesNotSupported ->
+         alarm what internal
+           (str "Inductive types with annotations not supported.")
+    | ConstructorWithNonParametricInductiveType ind ->
+         alarm what internal
+           (strbrk "Unsupported constructor with an argument whose type is a non-parametric inductive type." ++
+            strbrk " Type " ++ quote (Printer.pr_inductive (Global.env()) ind) ++
+            str " is applied to an argument which is not a variable.")
     | e when CErrors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ CErrors.print e)