aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--cfrontend/Ctypes.v56
-rw-r--r--common/Linking.v94
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.