blob: f94044160e20bd56bfacbb6d75a85e631d26da72 (
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
|
open import Pervasives
type M 's 'a = 's -> ('a * 's)
val return : forall 's 'a. 'a -> M 's 'a
let return a = fun s -> (a,s)
val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b
let bind m f s = let (a,s') = m s in f a s'
let (>>=) = bind
let (>>) m n = m >>= fun _ -> n
val foreach_inc : forall 's 'vars. (nat * nat * nat) -> (nat -> 'vars -> M 's 'vars) ->
'vars -> M 's 'vars
let rec foreach_inc (i,stop,by) body vars =
if i <= stop
then (body i vars >>= fun vars -> foreach_inc (i + by,stop,by) body vars)
else return vars
val foreach_dec : forall 's 'vars. (nat * nat * nat) -> (nat -> 'vars -> M 's 'vars) ->
'vars -> M 's 'vars
let rec foreach_dec (i,stop,by) body vars =
if i >= stop
then (body i vars >>= fun vars -> foreach_dec (i - by,stop,by) body vars)
else return vars
|
