-
Notifications
You must be signed in to change notification settings - Fork 398
/
Control.lean
55 lines (47 loc) · 1.5 KB
/
Control.lean
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Control.Basic
import Init.Data.Nat.Basic
namespace Nat
universe u v
@[inline] def forM {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
let rec @[specialize] loop
| 0 => pure ()
| i+1 => do f (n-i-1); loop i
loop n
@[inline] def forRevM {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
let rec @[specialize] loop
| 0 => pure ()
| i+1 => do f i; loop i
loop n
@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
let rec @[specialize] loop
| 0, a => pure a
| i+1, a => f (n-i-1) a >>= loop i
loop n init
@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
let rec @[specialize] loop
| 0, a => pure a
| i+1, a => f i a >>= loop i
loop n init
@[inline] def allM {m} [Monad m] (n : Nat) (p : Nat → m Bool) : m Bool :=
let rec @[specialize] loop
| 0 => pure true
| i+1 => do
match (← p (n-i-1)) with
| true => loop i
| false => pure false
loop n
@[inline] def anyM {m} [Monad m] (n : Nat) (p : Nat → m Bool) : m Bool :=
let rec @[specialize] loop
| 0 => pure false
| i+1 => do
match (← p (n-i-1)) with
| true => pure true
| false => loop i
loop n
end Nat