Source

Example:

// This module implements the Fibonacci function. It also gives a
// solution to the second problem from Project Euler
// (projecteuler.net), viz.,
//
// "Each new term in the Fibonacci sequence is generated by adding the
// previous two terms. By starting with 1 and 2, the first 10 terms
// will be: 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, ...
//
// By considering the terms in the Fibonacci sequence whose values do
// not exceed four million, find the sum of the even-valued terms.
// Answer: 4613732"

val (+) = mod32::+;

// This is a simple but reasonably efficent implementation of the
// Fibonacci function.
val fun fib(x i32) = purify i32 {
  new a = new_i32(0);
  new b = new_i32(1);
  for _ in 0..x {
    val old_a = get a;
    val old_b = get b;
    a := old_b;
    b := old_a + old_b;
  }
  yield(get a);
};

// Test the first few terms of the Fibonacci function.
assert fib(0) = 0 is i32;
assert fib(1) = 1 is i32;
assert fib(2) = 1 is i32;
assert fib(3) = 2 is i32;
assert fib(4) = 3 is i32;
assert fib(5) = 5 is i32;
assert fib(6) = 8 is i32;
assert fib(7) = 13 is i32;
assert fib(8) = 21 is i32;
assert fib(46) = 1836311903 is i32;

// Compile the Fibonacci function.
compile fib(x i32) i32 = block { yield(fib(x)); };
test fib(46) = 1836311903;

// Here is the resulting LLVM listing.
//
// define i32 @fib(i32 %x) {
// entry:
//   br label %begin
//
// begin:                                            ; preds = %loop, %entry
//   %b = phi i32 [ 1, %entry ], [ %1, %loop ]
//   %a = phi i32 [ 0, %entry ], [ %b, %loop ]
//   %range = phi i32 [ 0, %entry ], [ %2, %loop ]
//   %0 = icmp ult i32 %range, %x
//   br i1 %0, label %loop, label %end
//
// loop:                                             ; preds = %begin
//   %1 = add i32 %a, %b
//   %2 = add i32 %range, 1
//   br label %begin
//
// end:                                              ; preds = %begin
//   ret i32 %a
// }


val (<) = mod32::<;
val (==) = mod32::==;
val fun (x bool) && (y bool) = x ? y : false;
val fun (x bool) || (y bool) = x ? true : y;
val fun (x i32) <= (y i32) = x < y || x == y;
val and = mod32::and;

val fun (I interface) ++ (J interface) interface = meth {
  false: I,
  true: J
};
val fun !(x bool) = x ? false : true;

val i_range interface = meth(_ i32) void;
val range type = i_range => void;
val i_break interface = meth(_ i32) bool;
val break type = i_break => bool;

assert catch is
dep(b type) ->
dep(i interface) ->
dep(a type) ->
dep(f b -> i => a) ->
(i ++ (meth(_ b) enum{}) => a) ->
i => a;


val fun breakable(rng range) break =
catch(void)(i_break)(bool)(fun(_) block { yield(false); })(
block {
  for c in rng {
    val x = do call(false@c);
    if !x { val y = do call(true@()); yield(do fun{}(y)); }
  }
  yield(true);
});


// This solution to the second Euler problem is very inefficient and
// doesn't use any properties of the Fibonacci sequence to optimize
// the algorithm.
//
// One natural solution to this problem is to use a while loop, but
// there are currently no plans to implement while loops in IPL, as
// all programs in type theory must be terminating.
//
// A future version of IPL will support range loops with break and
// continue, and, more generally, an efficiently implemented
// throw/catch construct that can be used to break out of (possibly
// nested) loops.
val fun euler2(max i32) = purify i32 {
  new sum = new_i32(0);
  val _ bool = for i in breakable(0..max) {
    val a = fib(i);
    // Count a if a <= max and the lsb of a is unset.
    if a <= max {
      if and(a, 1) == 0 {
        sum := sum + a;
      }
      yield(true);  // continue
    } else {
      yield(false);  // break
    }
  }
  yield(get sum);
};

// Check that we have a correct solution.
assert euler2(4000000) = 4613732 is i32;

// Compile the solution to the second Euler problem.
compile euler2(max i32) i32 = block { yield(euler2(max)); };

// Check that the compiled function works too.
test euler2(4000000) = 4613732;

// The compiled version of euler2 is rather interesting.
//
//
// define i32 @euler2(i32 %max) {
// entry:
//   %0 = icmp sgt i32 %max, 2
//   br i1 %0, label %merge37, label %false38
//
// merge37:                                          ; preds = %false38, %entry
//   %merge40 = phi i32 [ %phitmp, %false38 ], [ 2, %entry ]
//   %1 = icmp sgt i32 %max, 8
//   %2 = icmp eq i32 %max, 8
//   %. = select i1 %1, i1 true, i1 %2
//   %3 = or i32 %merge40, 8
//   %local_cell.6 = select i1 %., i32 %3, i32 %merge40
//   %4 = icmp sgt i32 %max, 34
//   %5 = icmp eq i32 %max, 34
//   %.793 = select i1 %4, i1 true, i1 %5
//   %6 = add i32 %local_cell.6, 34
//   %local_cell.9 = select i1 %.793, i32 %6, i32 %local_cell.6
//   %7 = icmp sgt i32 %max, 144
//   %8 = icmp eq i32 %max, 144
//   %.794 = select i1 %7, i1 true, i1 %8
//   %9 = add i32 %local_cell.9, 144
//   %local_cell.12 = select i1 %.794, i32 %9, i32 %local_cell.9
//   %10 = icmp sgt i32 %max, 610
//   %11 = icmp eq i32 %max, 610
//   %.795 = select i1 %10, i1 true, i1 %11
//   %12 = add i32 %local_cell.12, 610
//   %local_cell.15 = select i1 %.795, i32 %12, i32 %local_cell.12
//   %13 = icmp sgt i32 %max, 2584
//   %14 = icmp eq i32 %max, 2584
//   %.796 = select i1 %13, i1 true, i1 %14
//   %15 = add i32 %local_cell.15, 2584
//   %local_cell.18 = select i1 %.796, i32 %15, i32 %local_cell.15
//   %16 = icmp sgt i32 %max, 10946
//   %17 = icmp eq i32 %max, 10946
//   %.797 = select i1 %16, i1 true, i1 %17
//   %18 = add i32 %local_cell.18, 10946
//   %local_cell.21 = select i1 %.797, i32 %18, i32 %local_cell.18
//   %19 = icmp sgt i32 %max, 46368
//   %20 = icmp eq i32 %max, 46368
//   %.798 = select i1 %19, i1 true, i1 %20
//   %21 = add i32 %local_cell.21, 46368
//   %local_cell.24 = select i1 %.798, i32 %21, i32 %local_cell.21
//   %22 = icmp sgt i32 %max, 196418
//   %23 = icmp eq i32 %max, 196418
//   %.799 = select i1 %22, i1 true, i1 %23
//   %24 = add i32 %local_cell.24, 196418
//   %local_cell.27 = select i1 %.799, i32 %24, i32 %local_cell.24
//   %25 = icmp sgt i32 %max, 832040
//   %26 = icmp eq i32 %max, 832040
//   %.800 = select i1 %25, i1 true, i1 %26
//   %27 = add i32 %local_cell.27, 832040
//   %local_cell.30 = select i1 %.800, i32 %27, i32 %local_cell.27
//   %28 = icmp sgt i32 %max, 3524578
//   %29 = icmp eq i32 %max, 3524578
//   %.801 = select i1 %28, i1 true, i1 %29
//   %30 = add i32 %local_cell.30, 3524578
//   %local_cell.33 = select i1 %.801, i32 %30, i32 %local_cell.30
//   %31 = icmp sgt i32 %max, 14930352
//   %32 = icmp eq i32 %max, 14930352
//   %.802 = select i1 %31, i1 true, i1 %32
//   %33 = add i32 %local_cell.33, 14930352
//   %local_cell.36 = select i1 %.802, i32 %33, i32 %local_cell.33
//   %34 = icmp sgt i32 %max, 63245986
//   %35 = icmp eq i32 %max, 63245986
//   %.803 = select i1 %34, i1 true, i1 %35
//   %36 = add i32 %local_cell.36, 63245986
//   %local_cell.39 = select i1 %.803, i32 %36, i32 %local_cell.36
//   %37 = icmp sgt i32 %max, 267914296
//   %38 = icmp eq i32 %max, 267914296
//   %.804 = select i1 %37, i1 true, i1 %38
//   %39 = add i32 %local_cell.39, 267914296
//   %local_cell.42 = select i1 %.804, i32 %39, i32 %local_cell.39
//   %40 = icmp sgt i32 %max, 1134903170
//   %41 = icmp eq i32 %max, 1134903170
//   %.805 = select i1 %40, i1 true, i1 %41
//   %42 = add i32 %local_cell.42, 1134903170
//   %local_cell.45 = select i1 %.805, i32 %42, i32 %local_cell.42
//   ret i32 %local_cell.45
//
// false38:                                          ; preds = %entry
//   %43 = icmp eq i32 %max, 2
//   %phitmp = select i1 %43, i32 2, i32 0
//   br label %merge37
// }


Tags: language  

Last modified 16 December 2024