diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-03 10:11:23 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-24 17:38:06 +0100 |
| commit | 1e29e518e62ad88e9c2e2b180beb07434a07cdd7 (patch) | |
| tree | 515e91150bc6db4910daa97ba99611192b01fe2f /common/AST.v | |
| parent | 794ae6fb64e89175b40288369011f4fc51e0ac53 (diff) | |
| download | compcert-kvx-1e29e518e62ad88e9c2e2b180beb07434a07cdd7.tar.gz compcert-kvx-1e29e518e62ad88e9c2e2b180beb07434a07cdd7.zip | |
Record public global definitions via field "prog_public" in AST.program.
For the moment, this field is ignored.
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/common/AST.v b/common/AST.v index 1c46389e..75286bd6 100644 --- a/common/AST.v +++ b/common/AST.v @@ -201,6 +201,8 @@ Record globvar (V: Type) : Type := mkglobvar { (** Whole programs consist of: - a collection of global definitions (name and description); +- a set of public names (the names that are visible outside + this compilation unit); - the name of the ``main'' function that serves as entry point in the program. A global definition is either a global function or a global variable. @@ -218,6 +220,7 @@ Implicit Arguments Gvar [F V]. Record program (F V: Type) : Type := mkprogram { prog_defs: list (ident * globdef F V); + prog_public: list ident; prog_main: ident }. @@ -244,6 +247,7 @@ Definition transform_program_globdef (idg: ident * globdef A V) : ident * globde Definition transform_program (p: program A V) : program B V := mkprogram (List.map transform_program_globdef p.(prog_defs)) + p.(prog_public) p.(prog_main). Lemma transform_program_function: @@ -295,7 +299,8 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end. Definition transform_partial_program2 (p: program A V) : res (program B W) := - do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). + do gl' <- transf_globdefs p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). Lemma transform_partial_program2_function: forall p tp i tf, @@ -363,6 +368,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_program2_public: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -373,7 +386,7 @@ Variable new_main: ident. Definition transform_partial_augment_program (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); - OK(mkprogram (gl' ++ new_globs) new_main). + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). Lemma transform_partial_augment_program_main: forall p tp, @@ -416,6 +429,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_program_public: + forall p tp, + transform_partial_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -480,7 +501,8 @@ Definition match_program (new_globs : list (ident * globdef B W)) (p1: program A V) (p2: program B W) : Prop := (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ p2.(prog_defs) = tglob ++ new_globs) /\ - p2.(prog_main) = new_main. + p2.(prog_main) = new_main /\ + p2.(prog_public) = p1.(prog_public). End MATCH_PROGRAM. |