prune-lang 0.2.3

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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

datatype Bit where
| O
| I
end

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

datatype BitInt where
| Pos(BitList)
| Zero
| Neg(BitList)
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 list_add_1(xs: BitList) -> BitList
begin
    match xs with
    | Cons(O, tail) => Cons(I, tail)
    | Cons(I, tail) => Cons(O, list_add_1(tail))
    | Nil => Cons(O, Nil)
    end
end

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

function list_mul(xs: BitList, ys: BitList) -> BitList
begin
    match (xs, ys) with
    | (Nil, Nil) => Nil
    | (Cons(_, _), Nil) => xs
    | (Nil, Cons(_, _)) => ys
    | (Cons(x_head, x_tail), Cons(y_head, y_tail)) =>
        let new_tail = list_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, list_add(x_tail, Cons(O, new_tail)))
        // (2m + 1)(2n) = 4mn + 2n
        | (I, O) => Cons(O, list_add(y_tail, Cons(O, new_tail)))
        // (2m + 1)(2n + 1) = 4mn + 2(m + n) + 1
        | (I, I) => Cons(I, list_add(list_add(x_tail, y_tail), Cons(O, new_tail)))
        end
    end
end

function list_sub(xs: BitList, ys: BitList) -> BitInt
begin
    fresh zs;
    alternative
    // xs + (-ys) = (+zs) ===> ys + zs = xs
    | guard xs = full_adder_n(O, ys, zs); Pos(zs)
    // xs + (-ys) = (-zs) ===> (-xs) + ys = zs ===> xs + zs = ys
    | guard ys = full_adder_n(O, xs, zs); Neg(zs)
    // xs + (-ys) = 0 ===> xs = ys
    | guard xs = ys; Zero
    end
end

function add(x: BitInt, y: BitInt) -> BitInt
begin
    match (x, y) with
    | (Pos(xs), Pos(ys)) => Pos(full_adder_n(O, xs, ys))
    | (Pos(xs), Zero) => Pos(xs)
    | (Pos(xs), Neg(ys)) => list_sub(xs, ys)
    | (Zero, ys) => ys
    | (Neg(xs), Pos(ys)) => list_sub(ys, xs)
    | (Neg(xs), Zero) => Neg(xs)
    | (Neg(xs), Neg(ys)) => Neg(full_adder_n(O, xs, ys))
    end 
end

function mul(x: BitInt, y: BitInt) -> BitInt
begin
    match (x, y) with
    | (Pos(xs), Pos(ys)) => Pos(list_mul(xs, ys))
    | (Pos(_xs), Zero) => Zero
    | (Pos(xs), Neg(ys)) => Neg(list_mul(xs, ys))
    | (Zero, _) => Zero
    | (Neg(xs), Pos(ys)) => Neg(list_mul(xs, ys))
    | (Neg(_xs), Zero) => Zero
    | (Neg(xs), Neg(ys)) => Pos(list_mul(xs, ys))
    end 
end

function pythagorean_triple(x: BitInt, y: BitInt, z: BitInt)
begin
    let Pos(_) = x;
    let Pos(_) = y;
    let Pos(_) = z;
    guard add(mul(x, x), mul(y, y)) = mul(z, z);
end

query pythagorean_triple(depth_step=20, depth_limit=500, answer_limit=10)