How to build a Gray-code generator in Picat?

Encouraged by the knowledge I've gained from the answer to my previous post, I aim to generate Gray-codes of given length. The procedure hamming seems to work correctly, however, the Picat system finds no solution. Where's the mistake here?

import cp.
main => gray(2).

gray(CodeLen) =>
    CodeNr is 2**CodeLen,
    Codes = new_array(CodeNr, CodeLen),
    Codes :: 0..1,

    foreach(CodeNr1 in 1..CodeNr)
        CodeNr2 = cond(CodeNr1 == CodeNr, 1, CodeNr1 + 1),
        hamming(Codes[CodeNr1], Codes[CodeNr2], 0, H), 
        H #= 1 
        % the Hamming distance between 2 consecutive codes is 1
    end,

    solve(Codes),
    printf("%w\n", Codes).

hamming([], [], A, H) ?=> H #= A.
hamming([H1|T1], [H2|T2], A, H) ?=> 
    H1 #!= H2,
    A1 #= A + 1,
    hamming(T1, T2, A1, H).
hamming([H1|T1], [H2|T2], A, H) ?=> 
    H1 #= H2,
    A1 #= A + 0,
    hamming(T1, T2, A1, H).

The reason that the model don't print anything is that you are using list constructs ([H|T]) on the array matrix Code which is not allowed. You have to convert the rows of the matrix (which are arrays) to lists. This can be done in two ways:

1. Convert the array matrix Code matrix to a list matrix with array_matrix_to_list_matrix() (requires that the util package is loaded):

import util.

% ....

gray(CodeLen) =>
    CodeNr is 2**CodeLen,
    Codes = new_array(CodeNr, CodeLen).array_matrix_to_list_matrix, % <--
    Codes :: 0..1,
    % ....

2. Convert the array parameters in the call to hamming/4 to lists with theto_list() function. E.g.:

    % ...
    foreach(CodeNr1 in 1..CodeNr)
        CodeNr2 = cond(CodeNr1 == CodeNr, 1, CodeNr1 + 1),
        % hamming(Codes[CodeNr1], Codes[CodeNr2], 0, H), % Original
        hamming(Codes[CodeNr1].to_list, Codes[CodeNr2].to_list, 0, H), % <---        
        H #= 1 
        % the Hamming distance between 2 consecutive codes is 1
    end,
    % ...

Update.

Here's a constraint model that solves the problem of generating different rows that was indicated in the comment. It uses a simpler version of hamming_distance by just counting the number of different bits with sum. Also, for symmetry, I require that the first and last row also have a Hamming distance of 1. (This was in the original code.)

To require different rows, the constraint to_num/3 is used to converts a number to digits in an array (given a base, here 2). These numbers (which must be distinct) are in the CodesNum list.

import cp,util.
main =>
   go.

go ?=>
  gray(5),
  nl,
  % fail,
  nl.
go => true.

% First solution for N=2..10
go2 ?=>
  foreach(N in 2..10)
    println(n=N),
    if time(gray(N)) then
      true
    else
      println(nope)
    end,
    nl
  end,
  nl.
go2 => true.


gray(CodeLen) =>
    CodeNr is 2**CodeLen,
    println(codeNr=CodeNr),
    Codes = new_array(CodeNr, CodeLen).array_matrix_to_list_matrix,
    Codes :: 0..1,
    CodesNum = new_list(CodeNr), % array -> integer
    CodesNum :: 0..CodeNr,

    
    foreach(CodeNr1 in 1..CodeNr)
        to_num(Codes[CodeNr1],2,CodesNum[CodeNr1]),
        CodeNr2 = cond(CodeNr1 == CodeNr, 1, CodeNr1 + 1),
        hamming_distance(Codes[CodeNr1], Codes[CodeNr2], 1),
    end,
    % around the corner
    % hamming_distance(Codes[1], Codes[CodeNr],1),
            
    all_different(CodesNum),
    CodesNum[1] #= 0, % symmetry breaking
    Vars = CodesNum ++ Codes.vars,
    solve($[ff,updown],Vars),
    printf("%w\n", Codes),
    println(codesNum=CodesNum),nl.

% Hamming distance of As and Bs
hamming_distance(As, Bs,Diff) =>
   Diff #= sum([(A #!= B) : {A,B} in zip(As,Bs)]).

% Convert Num to/from a list of digits in List (base Base)
to_num(List, Base, Num) =>
        Len = length(List),
        Num #= sum([List[I]*Base**(Len-I) : I in 1..Len]).

to_num(List, Num) =>
       to_num(List, 10, Num).

It solves N=4 in 0s:

n = 4
codeNr = 16
[[0,0,0,0],[1,0,0,0],[1,1,0,0],[1,1,1,0],[1,1,1,1],[1,1,0,1],[1,0,0,1],[1,0,1,1],[1,0,1,0],[0,0,1,0],[0,1,1,0],[0,1,1,1],[0,0,1,1],[0,0,0,1],[0,1,0,1],[0,1,0,0]]
codesNum = [0,8,12,14,15,13,9,11,10,2,6,7,3,1,5,4]

CPU time 0.0 seconds.

The model solves N=2..7 (first solution) quite fast, but it struggles with N=8, and I don't have the time to test different search heuristics to make it faster.

Here's some another approach for solving the gray code but without constraint modelling and it's much faster: http://hakank.org/picat/gray_code.pi

Update2 Here's a much faster version of hamming/4. It use a reification (boolean) variable B to check if H1 and H2 are different and can then be used as the value to add to A0.

hamming2([], [], A, A).
hamming2([H1|T1], [H2|T2], A0, H) :-
    B :: 0..1,
    H1 #!= H2 #<=> B #= 1,
    A1 #= A0 + B,
    hamming2(T1, T2, A1, H).