copied && added "C" *
Require Import CoqlibC Maps Errors ASTC.
newly added *
Require Export Linking.
Require Import Axioms.
Require Import sflib.
Set Implicit Arguments.
Inductive link_res (
A:
Type):
Type :=
|
empty
|
fail
|
success:
A ->
link_res A.
Arguments empty [
A].
Arguments fail [
A].
Fixpoint link_list_aux X `{
Linker X} (
xs:
list X):
link_res X :=
match xs with
| [] =>
empty
|
x0 ::
tl =>
match link_list_aux tl with
|
empty =>
success x0
|
fail =>
fail
|
success x1 =>
match link x0 x1 with
|
Some x =>
success x
|
None =>
fail
end
end
end.
Definition link_list X `{
Linker X} (
xs:
list X):
option X :=
match link_list_aux xs with
|
empty =>
None
|
success x =>
Some x
|
fail =>
None
end.
Lemma link_list_cons
X `{
Linker X}
hd tl restl res
(
TL:
link_list tl =
Some restl)
(
HD:
link hd restl =
Some res):
<<
LINK:
link_list (
hd ::
tl) =
Some res>> /\ <<
LINKORDER:
Forall (
fun x =>
linkorder x res) (
hd ::
tl)>>.
Proof.
Lemma link_list_linkorder
X `{
Linker X}
xs xs_res
(
LINK:
link_list xs =
Some xs_res):
<<
LINKORDER:
Forall (
fun x =>
linkorder x xs_res)
xs>>.
Proof.
Lemma link_list_cons_inv
X `{
Linker X}
hd tl res
(
LINK:
link_list (
hd ::
tl) =
Some res)
(
LEN:
tl <> []):
exists restl, <<
TL:
link_list tl =
Some restl>> /\ <<
HD:
link hd restl =
Some res>>.
Proof.
Lemma link_list_aux_empty_inv
X `{
Linker X}
xs
(
EMPTY:
link_list_aux xs =
empty):
<<
NIL:
xs = []>>.
Proof.
ginduction xs; ii; ss. des_ifs. Qed.
Lemma link_list_snoc_commut
X `{
Linker X}
x0 x1 x_link xs
(
LINK:
link x0 x1 =
Some x_link):
<<
CMT:
link_list (
xs ++ [
x0 ;
x1]) =
link_list (
xs ++ [
x_link])>>.
Proof.
Lemma match_program_refl
F V
`{
Linker F} `{
Linker V}
(
prog:
AST.program F V):
match_program (
fun _ =>
eq)
eq prog prog.
Proof.
econs;
eauto.
destruct prog;
ss.
ginduction prog_defs;
ii;
ss.
{
econs;
eauto. }
destruct a;
ss.
econs;
eauto.
-
econs;
eauto.
ss.
destruct g;
ss.
+
econs;
eauto.
eapply linkorder_refl.
+
econs;
eauto.
destruct v;
ss.
-
rpapply IHprog_defs;
eauto.
do 2 (
apply Axioms.functional_extensionality;
i;
destruct x;
ss).
apply AxiomsC.prop_ext.
split;
ii;
inv H1;
ss;
clarify;
inv H3;
econs;
ss;
eauto;
econs;
ss;
eauto;
apply linkorder_refl.
Unshelve.
all:
ss.
Qed.
Lemma match_globdef_eq
C F V
`{
Linker C}
ctx:
match_globdef ((
fun _ =>
eq):
C ->
F ->
F ->
Prop)
(
eq:
V ->
V ->
Prop)
ctx =
eq.
Proof.
Local Transparent Linker_def Linker_vardef Linker_varinit.
Lemma link_unit_same
F (
g g0:
globdef F unit) (
gv:
globvar unit) `{
Linker F}
(
LINK:
link g g0 =
Some (
Gvar gv)):
g =
Gvar gv \/
g0 =
Gvar gv.
Proof.
ss.
unfold link_def in *.
des_ifs.
ss.
unfold link_vardef in *.
destruct v;
ss.
des_ifs;
bsimpl;
des;
des_sumbool;
rewrite eqb_true_iff in *.
destruct gvar_info;
ss.
destruct v0;
ss.
destruct gvar_info;
ss.
destruct u;
ss.
unfold link_varinit in *.
des_ifs;
eauto.
Qed.
Local Opaque Linker_def Linker_vardef Linker_varinit.
Definition link_skfundef (
fd1 fd2:
AST.fundef signature) :=
match fd1,
fd2 with
|
Internal _,
Internal _ =>
None
|
External ef1,
External ef2 =>
match ef1,
ef2 with
|
EF_external _ sg1,
EF_external _ sg2 =>
if signature_eq sg1 sg2 then Some (
External ef1)
else None
|
_,
_ =>
if external_function_eq ef1 ef2 then Some (
External ef1)
else None
end
|
Internal f,
External ef =>
match ef with
|
EF_external id sg =>
if signature_eq f sg then Some (
Internal f)
else None
|
_ =>
None
end
|
External ef,
Internal f =>
match ef with
|
EF_external id sg =>
if signature_eq f sg then Some (
Internal f)
else None
|
_ =>
None
end
end.
Inductive linkorder_skfundef:
AST.fundef signature ->
AST.fundef signature ->
Prop :=
|
linkorder_skfundef_refl:
forall fd,
linkorder_skfundef fd fd
|
linkorder_fundef_ext_ext:
forall name0 name1 sg,
linkorder_skfundef (
External (
EF_external name0 sg)) (
External (
EF_external name1 sg))
|
linkorder_skfundef_ext_int:
forall id sg,
linkorder_skfundef (
External (
EF_external id sg)) (
Internal sg).
Program Instance Linker_skfundef:
Linker (
AST.fundef signature) :=
{|
link :=
link_skfundef;
linkorder :=
linkorder_skfundef;
|}.
Next Obligation.
destruct x; econs; eauto. Qed.
Next Obligation.
inv H; inv H0; econs; et. Qed.
Next Obligation.
pose x as X. pose y as Y. destruct x, y; ss; des_ifs; esplits; eauto; try (econs; et).
Qed.