summaryrefslogtreecommitdiff
path: root/theories/Lists/StreamMemo.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Lists/StreamMemo.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Lists/StreamMemo.v')
-rw-r--r--theories/Lists/StreamMemo.v48
1 files changed, 24 insertions, 24 deletions
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index bdbe0ecc..d906cfa4 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -11,8 +11,8 @@ Require Import Streams.
(** * Memoization *)
-(** Successive outputs of a given function [f] are stored in
- a stream in order to avoid duplicated computations. *)
+(** Successive outputs of a given function [f] are stored in
+ a stream in order to avoid duplicated computations. *)
Section MemoFunction.
@@ -24,8 +24,8 @@ CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).
Definition memo_list := memo_make 0.
Fixpoint memo_get (n:nat) (l:Stream A) : A :=
- match n with
- | O => hd l
+ match n with
+ | O => hd l
| S n1 => memo_get n1 (tl l)
end.
@@ -49,7 +49,7 @@ Variable g: A -> A.
Hypothesis Hg_correct: forall n, f (S n) = g (f n).
CoFixpoint imemo_make (fn:A) : Stream A :=
- let fn1 := g fn in
+ let fn1 := g fn in
Cons fn1 (imemo_make fn1).
Definition imemo_list := let f0 := f 0 in
@@ -68,7 +68,7 @@ Qed.
End MemoFunction.
-(** For a dependent function, the previous solution is
+(** For a dependent function, the previous solution is
reused thanks to a temporarly hiding of the dependency
in a "container" [memo_val]. *)
@@ -80,7 +80,7 @@ Variable f: forall n, A n.
Inductive memo_val: Type :=
memo_mval: forall n, A n -> memo_val.
-Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
+Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
match n, m return {n = m} + {True} with
| 0, 0 =>left True (refl_equal 0)
| 0, S m1 => right (0 = S m1) I
@@ -88,7 +88,7 @@ Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
| S n1, S m1 =>
match is_eq n1 m1 with
| left H => left True (f_equal S H)
- | right _ => right (S n1 = S m1) I
+ | right _ => right (S n1 = S m1) I
end
end.
@@ -97,7 +97,7 @@ match v with
| memo_mval m x =>
match is_eq n m with
| left H =>
- match H in (@eq _ _ y) return (A y -> A n) with
+ match H in (eq _ y) return (A y -> A n) with
| refl_equal => fun v1 : A n => v1
end
| right _ => fun _ : A m => f n
@@ -134,7 +134,7 @@ Variable g: forall n, A n -> A (S n).
Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
-Let mg v := match v with
+Let mg v := match v with
memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
Definition dimemo_list := imemo_list _ mf mg.
@@ -166,13 +166,13 @@ End DependentMemoFunction.
Require Import ZArith.
Open Scope Z_scope.
-Fixpoint tfact (n: nat) :=
- match n with
- | O => 1
- | S n1 => Z_of_nat n * tfact n1
+Fixpoint tfact (n: nat) :=
+ match n with
+ | O => 1
+ | S n1 => Z_of_nat n * tfact n1
end.
-Definition lfact_list :=
+Definition lfact_list :=
dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)).
Definition lfact n := dmemo_get _ tfact n lfact_list.
@@ -183,18 +183,18 @@ intros n; unfold lfact, lfact_list.
rewrite dimemo_get_correct; auto.
Qed.
-Fixpoint nop p :=
+Fixpoint nop p :=
match p with
- | xH => 0
- | xI p1 => nop p1
- | xO p1 => nop p1
+ | xH => 0
+ | xI p1 => nop p1
+ | xO p1 => nop p1
end.
-Fixpoint test z :=
+Fixpoint test z :=
match z with
- | Z0 => 0
- | Zpos p1 => nop p1
- | Zneg p1 => nop p1
+ | Z0 => 0
+ | Zpos p1 => nop p1
+ | Zneg p1 => nop p1
end.
Time Eval vm_compute in test (lfact 2000).
@@ -202,4 +202,4 @@ Time Eval vm_compute in test (lfact 2000).
Time Eval vm_compute in test (lfact 1500).
Time Eval vm_compute in (lfact 1500).
*)
-
+