prune-lang 0.2.1

Prune is a constraint logic programming language with branching heuristic.
Documentation 
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

datatype Bit where
| O
| I
end

datatype BitList where
| Nil
| Cons(Bit, BitList)
end

function well_formed_sign(xs: BitList) -> Bit
begin
    match xs with
    | Nil => O
    | Cons(I, Nil) => I
    | Cons(_, Cons(head, tail)) => well_formed_sign(Cons(head, tail))
    end
end

// adder (ci, x, y) -> (z, co)
function full_adder_1(ci: Bit, x: Bit, y: Bit) -> (Bit, Bit) 
begin
    match (ci, x, y) with
    | (O, O, O) => (O, O)
    | (I, O, O) => (I, O)
    | (O, I, O) => (I, O)
    | (I, I, O) => (O, I)
    | (O, O, I) => (I, O)
    | (I, O, I) => (O, I)
    | (O, I, I) => (O, I)
    | (I, I, I) => (I, I)
    end
end

function full_adder_n(ci: Bit, xs: BitList, ys: BitList) -> BitList
begin
    match (xs, ys) with
    | (Nil, Nil) => match ci with
        | O => Nil
        | I => Cons(I, Nil)
        end
    | (Cons(x_head, x_tail), Nil) => 
        let (z, co) = full_adder_1(ci, x_head, O);
        Cons(z, full_adder_n(co, x_tail, Nil))
    | (Nil, Cons(y_head, y_tail)) => 
        let (z, co) = full_adder_1(ci, O, y_head);
        Cons(z, full_adder_n(co, Nil, y_tail))
    | (Cons(x_head, x_tail), Cons(y_head, y_tail)) =>
        let (z, co) = full_adder_1(ci, x_head, y_head);
        Cons(z, full_adder_n(co, x_tail, y_tail))
    end
end

function add(xs: BitList, ys: BitList) -> BitList
begin
    full_adder_n(O, xs, ys)
end

function mul(xs: BitList, ys: BitList) -> BitList
begin
    match (xs, ys) with
    | (Nil, Nil) => Nil
    | (Cons(_, _), Nil) => Nil
    | (Nil, Cons(_, _)) => Nil
    | (Cons(x_head, x_tail), Cons(y_head, y_tail)) =>
        let new_tail = mul(x_tail, y_tail);
        match (x_head, y_head) with
        // (2m)(2n) = 4mn
        | (O, O) => Cons(O, Cons(O, new_tail))
        // (2m)(2n + 1) = 4mn + 2m
        | (O, I) => Cons(O, add(x_tail, Cons(O, new_tail)))
        // (2m + 1)(2n) = 4mn + 2n
        | (I, O) => Cons(O, add(y_tail, Cons(O, new_tail)))
        // (2m + 1)(2n + 1) = 4mn + 2(m + n) + 1
        | (I, I) => Cons(I, add(add(x_tail, y_tail), Cons(O, new_tail)))
        end
    end
end

function pythagorean_triple(xs: BitList, ys: BitList, zs: BitList)
begin
    guard well_formed_sign(xs) = I;
    guard well_formed_sign(ys) = I;
    guard add(mul(xs, xs), mul(ys, ys)) = mul(zs, zs);
end

query pythagorean_triple(depth_step=20, depth_limit=200, answer_limit=1)