aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity/guard.v
blob: ceb7835a6b3da5ad2dd674dbf8e8de59d5cfc7c7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
(* Examples to check that the guard condition does not evaluate
   irrelevant subterms *)
(* Expected time < 1.00s *)
Require Import Bool.

Fixpoint slow n :=
 match n with
 | 0 => true
 | S k => andb (slow k) (slow k)
 end.

Timeout 5 Time Fixpoint F n :=
  match n with
  | 0 => 0
  | S k =>
    if slow 100 then F k else 0
  end.

Fixpoint slow2 n :=
 match n with
 | 0 => 0
 | S k => slow2 k + slow2 k
 end.

Timeout 5 Time Fixpoint F' n :=
  match n with
  | 0 => 0
  | S k =>
    if slow2 100 then F' k else 0
  end.