datatype Bit where
| O
| I
end

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

function well_formed(xs: BitList)
begin
    match xs with
    | Nil => ()
    | Cons(I, Nil) => ()
    | Cons(_, Cons(head, tail)) => well_formed(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 with
    | Nil => Nil
    | Cons(O, ks) => Cons(O, mul(ks, ys))
    | Cons(I, ks) => add(Cons(O, mul(ks, ys)), ys)
    end
end

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

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