From 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Mar 2013 16:51:42 +0000 Subject: 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 --- lib/Coqlib.v | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index f58a894..b936b9b 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: -- cgit v1.2.3