From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 37 ++++++++----------------------------- 1 file changed, 8 insertions(+), 29 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 9f734670..2f319d0c 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -214,39 +214,15 @@ Qed. (** * Properties of the translation functions *) -Lemma map_partial_names: - forall (A B: Type) (f: A -> res B) - (l: list (ident * A)) (tl: list (ident * B)), - map_partial prefix_var_name f l = OK tl -> - List.map (@fst ident B) tl = List.map (@fst ident A) l. -Proof. - induction l; simpl. - intros. inversion H. reflexivity. - intro tl. destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence. - inv H0. simpl. decEq. auto. -Qed. - -Lemma map_partial_append: - forall (A B: Type) (f: A -> res B) - (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)), - map_partial prefix_var_name f l1 = OK tl1 -> - map_partial prefix_var_name f l2 = OK tl2 -> - map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2). -Proof. - induction l1; intros until tl2; simpl. - intros. inversion H. simpl; auto. - destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence. - inv H0. rewrite (IHl1 _ _ _ H H1). auto. -Qed. - Lemma transl_vars_names: forall vars tvars, transl_vars vars = OK tvars -> List.map variable_name tvars = var_names vars. Proof. - exact (map_partial_names _ _ var_kind_of_type). + induction vars; simpl; intros. + monadInv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + simpl. decEq; auto. Qed. Lemma transl_names_norepet: @@ -268,7 +244,10 @@ Lemma transl_vars_append: transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). Proof. - exact (map_partial_append _ _ var_kind_of_type). + induction l1; simpl; intros. + inv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + erewrite IHl1; eauto. simpl. auto. Qed. Lemma transl_fn_variables: -- cgit