recfun.mlw 1.23 KB
Newer Older
1
module M
2

3 4
  use import int.Int
  use import module ref.Ref
5

6
  (** Recursive functions *)
7

8
  (** 1. Pure function *)
9

10 11
  let rec f1 (x:int) : int variant { x } =
    { x >= 0 } (if x > 0 then (f1 (x-1)) else x) { result = 0 }
12

13
  (** 2. With effects but no argument *)
14

Andrei Paskevich's avatar
Andrei Paskevich committed
15
  val x : ref int
16

17 18
  let rec f2 (u:unit) : unit variant { !x } =
    { !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
19

20
  (** 3. With effects and a pure argument *)
21

22 23 24 25
  let rec f3 (a:int) : unit variant { a } =
    { a >= 0 }
    if a > 0 then begin x := !x + 1; (f3 (a-1)) end
    { !x = old !x + a }
26

27
  (** 4. With effects and a reference as argument *)
28

29 30 31 32
  let rec f4 (a:ref int) : unit variant { !a } =
    { !a >= 0 }
    if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
    { !x = old !x + old !a }
33

34 35
  (** 5. The acid test:
         partial application of a recursive function with effects *)
36

37 38 39 40
  let rec f5 (a b:ref int) variant { !a } =
    { !a >= 0 }
    if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
    { result = old !a + old !b }
41

42 43
  let test_f5 () =
    { !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
44

45
  end
46 47

(*
48
Local Variables:
49
compile-command: "unset LANG; make -C ../../.. bench/programs/good/recfun"
50
End:
51
*)