From 0e225553a2ee1c39e0f070edb6528d109dd878ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Sep 2018 22:23:39 +0200
Subject: Fixing #4612 (anomaly with Scheme called on unsupported inductive
 type).

We raise a normal error instead of an anomaly.

This fixes also #2550, #8492.

Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
---
 test-suite/bugs/closed/4612.v |  7 +++++++
 vernac/auto_ind_decl.ml       | 44 ++++++++++++++++++++++---------------------
 vernac/auto_ind_decl.mli      |  1 +
 vernac/indschemes.ml          |  8 +++++++-
 4 files changed, 38 insertions(+), 22 deletions(-)
 create mode 100644 test-suite/bugs/closed/4612.v

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/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 3bf3925b4b..25ec1a68b4 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -59,6 +59,7 @@ exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
+exception ConstructorWithNonParametricInductiveType of inductive
 
 let constr_of_global g = lazy (UnivGen.constr_of_global g)
 
@@ -361,10 +362,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,16 +374,18 @@ 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*)
+    | 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 mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+        let mp,dir,lbl = Constant.repr3 cst 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")
         )))
       )
+    | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
+
   in
   Proofview.Goal.enter begin fun gl ->
     let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
@@ -409,8 +412,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
@@ -423,10 +426,10 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
 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 +438,15 @@ 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
+    | 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 mp,dir,lbl = Constant.repr3 cst 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")
         )))
-      )
+    | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
   in
 
   let rec aux l1 l2 =
@@ -456,7 +458,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 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 +482,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..8ecc09b7d1 100644
--- a/vernac/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
@@ -27,6 +27,7 @@ exception ParameterWithoutEquality of GlobRef.t
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
+exception ConstructorWithNonParametricInductiveType of inductive
 
 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..4c41ea657a 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,11 @@ let try_declare_scheme what f internal names kn =
     | NoDecidabilityCoInductive ->
          alarm what internal
            (str "Scheme Equality is only for inductive types.")
+    | 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)
-- 
cgit v1.2.3


From 82a3fb5d5c0d0c5660effec59f3800ee5e8a125d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Sep 2018 22:47:36 +0200
Subject: Fixing #4859 (anomaly with Scheme called on inductive type with
 indices).

We raise a normal error instead of an anomaly.
---
 test-suite/bugs/closed/4859.v | 7 +++++++
 vernac/auto_ind_decl.ml       | 6 ++++++
 vernac/auto_ind_decl.mli      | 1 +
 vernac/indschemes.ml          | 3 +++
 4 files changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/4859.v

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/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 25ec1a68b4..ca1d36cb69 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -60,6 +60,7 @@ 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)
 
@@ -121,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 =
@@ -134,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
diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli
index 8ecc09b7d1..647ff3d8d6 100644
--- a/vernac/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
@@ -28,6 +28,7 @@ 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 4c41ea657a..0a74a8cc4a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -177,6 +177,9 @@ 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." ++
-- 
cgit v1.2.3


From f30996a89a31a1a54ab481f752e5febb8a8ac0ed Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 12:59:28 +0200
Subject: Fixing a typo in a comment.

---
 test-suite/success/SchemeEquality.v | 7 +++++++
 vernac/auto_ind_decl.ml             | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/success/SchemeEquality.v

diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
new file mode 100644
index 0000000000..00e84bff38
--- /dev/null
+++ b/test-suite/success/SchemeEquality.v
@@ -0,0 +1,7 @@
+(* Examples of use of Scheme Equality *)
+
+Module A.
+Definition N := nat.
+Inductive list := nil | cons : N -> list -> list.
+Scheme Equality for list.
+End A.
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ca1d36cb69..a9bf3f42c4 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -428,7 +428,7 @@ 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
-- 
cgit v1.2.3


From 3dd31e9f94f09ec898ceb309082f147f3f40b1f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 12:59:48 +0200
Subject: Fixing a Scheme Equality anomaly with constants bound to inductive.

---
 vernac/auto_ind_decl.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index a9bf3f42c4..2013f19dc5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -348,13 +348,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.
@@ -397,7 +394,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     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
@@ -464,7 +461,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
-- 
cgit v1.2.3


From 9afe18c3190bb0210e03bf40f3af101a7c5604da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 13:32:08 +0200
Subject: Scheme Equality: support for working in a context of Parameters.

It was working in very specific context of section variables. We make
it work similarly in the same kind of specific context of
Parameters. See test file SchemeEquality.v for the expected form. See
discussion at PR #8509.
---
 test-suite/success/SchemeEquality.v | 22 ++++++++++++++++++++++
 vernac/auto_ind_decl.ml             | 15 ++++++++++++---
 2 files changed, 34 insertions(+), 3 deletions(-)

diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v
index 00e84bff38..85d5c3e123 100644
--- a/test-suite/success/SchemeEquality.v
+++ b/test-suite/success/SchemeEquality.v
@@ -5,3 +5,25 @@ 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 2013f19dc5..eb51d2341a 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -200,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)
@@ -232,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")
-- 
cgit v1.2.3


From 4865687c8c5641170080a47c72ee26c75eece49d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Sep 2018 14:30:47 +0200
Subject: Using Constant.change_label (better level of abstraction to build
 kernel names).

---
 vernac/auto_ind_decl.ml | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index eb51d2341a..dee7541d37 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -389,13 +389,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     | 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 mp,dir,lbl = Constant.repr3 cst 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")
-        )))
-      )
+        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
@@ -453,11 +449,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     | 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 mp,dir,lbl = Constant.repr3 cst 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")
-        )))
+        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
 
-- 
cgit v1.2.3