diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-16 16:51:42 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-16 16:51:42 +0000 |
commit | 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 (patch) | |
tree | 166a21d507612d60db40737333ddec5003fc81aa /lib/Coqlib.v | |
parent | e44df4563f1cb893ab25b2a8b25d5b83095205be (diff) | |
download | compcert-707b6a1ae9660b13cf6f68c7c0ce74017f5981c5.tar.gz compcert-707b6a1ae9660b13cf6f68c7c0ce74017f5981c5.zip |
Assorted changes to reduce stack and heap requirements when compiling very big functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index f58a894d..b936b9b2 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -854,6 +854,54 @@ Proof. exists (a0 :: l1); exists l2; intuition. simpl; congruence. Qed. +(** Folding a function over a list *) + +Section LIST_FOLD. + +Variables A B: Type. +Variable f: A -> B -> B. + +(** This is exactly [List.fold_left] from Coq's standard library, + with [f] taking arguments in a different order. *) + +Fixpoint list_fold_left (accu: B) (l: list A) : B := + match l with nil => accu | x :: l' => list_fold_left (f x accu) l' end. + +(** This is exactly [List.fold_right] from Coq's standard library, + except that it runs in constant stack space. *) + +Definition list_fold_right (l: list A) (base: B) : B := + list_fold_left base (List.rev' l). + +Remark list_fold_left_app: + forall l1 l2 accu, + list_fold_left accu (l1 ++ l2) = list_fold_left (list_fold_left accu l1) l2. +Proof. + induction l1; simpl; intros. + auto. + rewrite IHl1. auto. +Qed. + +Lemma list_fold_right_eq: + forall l base, + list_fold_right l base = + match l with nil => base | x :: l' => f x (list_fold_right l' base) end. +Proof. + unfold list_fold_right; intros. + destruct l. + auto. + unfold rev'. rewrite <- ! rev_alt. simpl. + rewrite list_fold_left_app. simpl. auto. +Qed. + +Lemma list_fold_right_spec: + forall l base, list_fold_right l base = List.fold_right f base l. +Proof. + induction l; simpl; intros; rewrite list_fold_right_eq; congruence. +Qed. + +End LIST_FOLD. + (** Properties of list membership. *) Lemma in_cns: |