From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/RTLgen.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 3da961c6..49d79fb2 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -27,7 +27,7 @@ Open Local Scope string_scope. (** * Translation environments and state *) -(** The translation functions are parameterized by the following +(** The translation functions are parameterized by the following compile-time environment, which maps CminorSel local variables and let-bound variables to RTL registers. The mapping for local variables is computed from the CminorSel variable declarations at the beginning of @@ -78,7 +78,7 @@ Lemma state_incr_trans: forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. Proof. intros. inv H; inv H0. apply state_incr_intro. - apply Ple_trans with (st_nextnode s2); assumption. + apply Ple_trans with (st_nextnode s2); assumption. apply Ple_trans with (st_nextreg s2); assumption. intros. generalize (H3 pc) (H5 pc). intuition congruence. Qed. @@ -93,7 +93,7 @@ Qed. to modify the global state. These luxuries are not available in Coq, however. Instead, we use a monadic encoding of the translation: translation functions take the current global state as argument, - and return either [Error msg] to denote an error, + and return either [Error msg] to denote an error, or [OK r s incr] to denote success. [s] is the modified state, [r] the result value of the translation function. and [incr] a proof that the final state is in the [state_incr] relation with the @@ -198,7 +198,7 @@ Definition add_instr (i: instruction) : mon node := fun s => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) + (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) (add_instr_wf s i)) (add_instr_incr s i). @@ -306,7 +306,7 @@ Definition add_var (map: mapping) (name: ident) : mon (reg * mapping) := ret (r, mkmapping (PTree.set name r map.(map_vars)) map.(map_letvars)). -Fixpoint add_vars (map: mapping) (names: list ident) +Fixpoint add_vars (map: mapping) (names: list ident) {struct names} : mon (list reg * mapping) := match names with | nil => ret (nil, map) @@ -339,7 +339,7 @@ Definition find_letvar (map: mapping) (idx: nat) : mon reg := fresh temporary register. Exception: if [a] is a let-bound variable or a local variable, we return the RTL register associated with that variable instead. Returning a fresh temporary in all cases - would be semantically correct, but would generate less efficient + would be semantically correct, but would generate less efficient RTL code. *) Definition alloc_reg (map: mapping) (a: expr) : mon reg := -- cgit