Phase d'optimisation: comparaison d'instances d'un type énuméré

Lié à #21 (closed)

Une comparaison ressemble à ça:

component compare[N : Int]

    i_a : bN
    i_b : bN
    o_c : bit

o_c = i_a ^ i_b == 0

Sachant qu'un XOR2 ça fait 4 NAND2, que la comparaison à 0 est gros NOR. On a donc environ 5×N NAND2eq.

Si x is ** implique que sémantiquement x == y renvoie ?, alors on peut utiliser le comparateur suivant.

OnlyOnes et OnlyZeroes sont calculés pour chaque bit en regardant la diversité de ce bit dans les variants en ignorant les x, voir exemple OneHot à la fin.

component enum_compare[
    N : Int,
    OnlyOnes : N * Bool,
    OnlyZeroes : N * Bool,
]

    i_a : bN
    i_b : bN
    o_c : bit

let only : bN
    [@I]
        = i_a[I] && i_b[I] If OnlyOnes[I]
        = !(i_a[I] || i_b[I]) If OnlyZeroes[I]
        = False

Val Both : N * Bool
    [@I] = !(OnlyOnes[I] || OnlyZeroes[I])


let both : bN
    [@I]
        = !(i_a[I] ^ i_b[I]) If Both[I]
        = True

o_c = (only != 0) && (both == ~0)

On retombe sur la même chose pour un encodage entiers. Pour un encodage OneHot, on aurait OnlyOnes[@I] = True et OnlyZeroes[@I] = False donc par propagation des constantes on obtiendrait un circuit avec:

N AND2 et une comparaison à 0 soit environ 2×N NAND2eq.

Une telle phase d'optimisation pourrait être facultative. On pourrait toujours forcer localement la comparaison complète avec quelque chose comme x as b == y as b, si l'encodage est défini.