Use `Program Instance` instead of `Instance` + refine mode (#261)

CompCert currently uses `Instance` in so-called "refine" mode, where
Coq drops automatically in proof mode if some members of the instance
are missing.

This mode is soon going to be turned off by default, see
https://github.com/coq/coq/pull/9270.

In order to make CompCert robust against this change, this commit
replaces those occurrences of `Instance` that use "refine" mode
with `Program Instance`.

2 files changed, 86 insertions, 64 deletions

diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 036b768b..bfc5daa9 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -1173,14 +1173,12 @@ Unset Implicit Arguments.
 
 (** ** Linking types *)
 
-Instance Linker_types : Linker type := {
+Program Instance Linker_types : Linker type := {
   link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
   linkorder := fun t1 t2 => t1 = t2
 }.
-Proof.
-  auto.
-  intros; congruence.
-  intros. destruct (type_eq x y); inv H. auto.
+Next Obligation.
+  destruct (type_eq x y); inv H. auto.
 Defined.
 
 Global Opaque Linker_types.
@@ -1224,14 +1222,18 @@ Proof.
   assert (x = y) by eauto. subst y. auto.
 Qed.
 
-Instance Linker_composite_defs : Linker (list composite_definition) := {
+Program Instance Linker_composite_defs : Linker (list composite_definition) := {
   link := link_composite_defs;
   linkorder := @List.incl composite_definition
 }.
-Proof.
-- intros; apply incl_refl.
-- intros; red; intros; eauto.
-- intros. apply link_composite_def_inv in H; destruct H as (A & B & C).
+Next Obligation.
+  apply incl_refl.
+Defined.
+Next Obligation.
+  red; intros; eauto.
+Defined.
+Next Obligation.
+  apply link_composite_def_inv in H; destruct H as (A & B & C).
   split; red; intros; apply C; auto.
 Defined.
 
@@ -1406,18 +1408,22 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
   | linkorder_fundef_ext_int: forall f id sg targs tres cc,
       linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
 
-Instance Linker_fundef (F: Type): Linker (fundef F) := {
+Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
   link := link_fundef;
   linkorder := linkorder_fundef
 }.
-Proof.
-- intros; constructor.
-- intros. inv H; inv H0; constructor.
-- intros x y z EQ. destruct x, y; simpl in EQ.
+Next Obligation.
+  constructor.
+Defined.
+Next Obligation.
+  inv H; inv H0; constructor.
+Defined.
+Next Obligation.
+  destruct x, y; simpl in H.
 + discriminate.
-+ destruct e; inv EQ. split; constructor.
-+ destruct e; inv EQ. split; constructor.
-+ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ.
++ destruct e; inv H. split; constructor.
++ destruct e; inv H. split; constructor.
++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv H.
   InvBooleans. subst. split; constructor.
 Defined.
 
@@ -1465,15 +1471,19 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
      linkorder (program_of_program p1) (program_of_program p2)
   /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
 
-Instance Linker_program (F: Type): Linker (program F) := {
+Program Instance Linker_program (F: Type): Linker (program F) := {
   link := link_program;
   linkorder := linkorder_program
 }.
-Proof.
-- intros; split. apply linkorder_refl. auto. 
-- intros. destruct H, H0. split. eapply linkorder_trans; eauto.
+Next Obligation.
+  split. apply linkorder_refl. auto.
+Defined.
+Next Obligation.
+  destruct H, H0. split. eapply linkorder_trans; eauto.
   intros; auto.
-- intros until z. unfold link_program. 
+Defined.
+Next Obligation.
+  revert H. unfold link_program.
   destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate.
   destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate.
   destruct (link_build_composite_env (prog_types x) (prog_types y) typs
diff --git a/common/Linking.v b/common/Linking.v
index eaa95462..ec828ea4 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -59,18 +59,22 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
   | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd
   | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f).
 
-Instance Linker_fundef (F: Type): Linker (fundef F) := {
+Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
   link := link_fundef;
   linkorder := linkorder_fundef
 }.
-Proof.
-- intros; constructor.
-- intros. inv H; inv H0; constructor.
-- intros x y z EQ. destruct x, y; simpl in EQ.
+Next Obligation.
+  constructor.
+Defined.
+Next Obligation.
+  inv H; inv H0; constructor.
+Defined.
+Next Obligation.
+  destruct x, y; simpl in H.
 + discriminate.
-+ destruct e; inv EQ. split; constructor.
-+ destruct e; inv EQ. split; constructor.
-+ destruct (external_function_eq e e0); inv EQ. split; constructor.
++ destruct e; inv H. split; constructor.
++ destruct e; inv H. split; constructor.
++ destruct (external_function_eq e e0); inv H. split; constructor.
 Defined.
 
 Global Opaque Linker_fundef.
@@ -109,16 +113,20 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
       il <> nil -> init_data_list_size il = sz ->
       linkorder_varinit (Init_space sz :: nil) il.
 
-Instance Linker_varinit : Linker (list init_data) := {
+Program Instance Linker_varinit : Linker (list init_data) := {
   link := link_varinit;
   linkorder := linkorder_varinit
 }.
-Proof.
-- intros. constructor.
-- intros. inv H; inv H0; constructor; auto.
+Next Obligation.
+  constructor.
+Defined.
+Next Obligation.
+  inv H; inv H0; constructor; auto.
   congruence.
   simpl. generalize (init_data_list_size_pos z). xomega.
-- unfold link_varinit; intros until z.
+Defined.
+Next Obligation.
+  revert H; unfold link_varinit.
   destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail).
 + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0.
   split; constructor. congruence. auto.
@@ -154,14 +162,18 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P
       linkorder i1 i2 ->
       linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo).
 
-Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
+Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
   link := link_vardef;
   linkorder := linkorder_vardef
 }.
-Proof.
-- intros. destruct x; constructor; apply linkorder_refl.
-- intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto.
-- unfold link_vardef; intros until z.
+Next Obligation.
+  destruct x; constructor; apply linkorder_refl.
+Defined.
+Next Obligation.
+  inv H; inv H0. constructor; eapply linkorder_trans; eauto.
+Defined.
+Next Obligation.
+  revert H; unfold link_vardef.
   destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl.
   destruct (link f1 f2) as [f|] eqn:LF; try discriminate.
   destruct (link i1 i2) as [i|] eqn:LI; try discriminate.
@@ -176,15 +188,10 @@ Global Opaque Linker_vardef.
 
 (** A trivial linker for the trivial var info [unit]. *)
 
-Instance Linker_unit: Linker unit := {
+Program Instance Linker_unit: Linker unit := {
   link := fun x y => Some tt;
   linkorder := fun x y => True
 }.
-Proof.
-- auto.
-- auto.
-- auto.
-Defined.
 
 Global Opaque Linker_unit.
 
@@ -207,18 +214,22 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -
       linkorder v1 v2 ->
       linkorder_def (Gvar v1) (Gvar v2).
 
-Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
+Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
   link := link_def;
   linkorder := linkorder_def
 }.
-Proof.
-- intros. destruct x; constructor; apply linkorder_refl.
-- intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto.
-- unfold link_def; intros.
+Next Obligation.
+  destruct x; constructor; apply linkorder_refl.
+Defined.
+Next Obligation.
+  inv H; inv H0; constructor; eapply linkorder_trans; eauto.
+Defined.
+Next Obligation.
+  unfold link_def; intros.
   destruct x as [f1|v1], y as [f2|v2]; try discriminate.
-+ destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L.
-  split; constructor; tauto.
-+ destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L.
++ simpl in H. destruct (link f1 f2) as [f|] eqn:L. inv H. apply link_linkorder in L.
+  split; constructor; tauto. discriminate.
++ simpl in H; destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L.
   split; constructor; tauto.
 Defined.
 
@@ -320,7 +331,7 @@ Qed.
 
 End LINKER_PROG.
 
-Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
+Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
   link := link_prog;
   linkorder := fun p1 p2 =>
      p1.(prog_main) = p2.(prog_main)
@@ -332,18 +343,19 @@ Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program
      /\ linkorder gd1 gd2
      /\ (~In id p2.(prog_public) -> gd2 = gd1)
 }.
-Proof.
-- intros; split; auto. split. apply incl_refl. intros.
+Next Obligation.
+  split; auto. split. apply incl_refl. intros.
   exists gd1; split; auto. split; auto. apply linkorder_refl.
-
-- intros x y z (A1 & B1 & C1) (A2 & B2 & C2).
+Defined.
+Next Obligation.
   split. congruence. split. red; eauto.
-  intros. exploit C1; eauto. intros (gd2 & P & Q & R).
-  exploit C2; eauto. intros (gd3 & U & X & Y).
+  intros. exploit H4; eauto. intros (gd2 & P & Q & R).
+  exploit H2; eauto. intros (gd3 & U & X & Y).
   exists gd3. split; auto. split. eapply linkorder_trans; eauto.
   intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto.
-
-- intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3).
+Defined.
+Next Obligation.
+  apply link_prog_inv in H. destruct H as (L1 & L2 & L3).
   subst z; simpl. intuition auto.
 + red; intros; apply in_app_iff; auto.
 + rewrite prog_defmap_elements, PTree.gcombine, H by auto.