Blame for src/lattice-kernel/lattice_kernel.m

%-----------------------------------------------------------------------------%
% SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
% CLONE_GATE: lattice_kernel_mercury
%
% lattice_kernel.m — Mercury production library
% Deterministic functions + multi-moded relations for the LATTICE kernel:
% lists, Peano, bit full-adder, SMT-stub SAT, path, FSM, interval refine.
% Build: mmc --make lattice_kernel   (needs a main module to link)
%   or compile as a library: mmc --make liblattice_kernel
%-----------------------------------------------------------------------------%

:- module lattice_kernel.
:- interface.

:- import_module bool.
:- import_module list.

% ---- types ----
:- type peano
    --->    z
    ;       s(peano).

:- type bit
    --->    b0
    ;       b1.

:- type smt
    --->    atom(string)
    ;       smt_not(smt)
    ;       smt_and(smt, smt).

:- type node == int.

:- type fsm_state
    --->    s0
    ;       s1.

:- type abs_val
    --->    conc(int)
    ;       top
    ;       interval(int, int).

% ---- lists (relational, reversible) ----
:- pred appendo(list(T), list(T), list(T)).
:- mode appendo(in, in, out) is det.
:- mode appendo(out, out, in) is multi.
:- mode appendo(in, out, in) is semidet.
:- mode appendo(out, in, in) is semidet.

:- pred membero(T, list(T)).
:- mode membero(in, in) is semidet.
:- mode membero(out, in) is nondet.

:- pred rembero(T, list(T), list(T)).
:- mode rembero(in, in, out) is semidet.
:- mode rembero(in, out, in) is nondet.

:- pred reverseo(list(T), list(T)).
:- mode reverseo(in, out) is det.
:- mode reverseo(out, in) is det.

:- pred lengtho(list(T), peano).
:- mode lengtho(in, out) is det.

:- pred distincto(list(T)).
:- mode distincto(in) is semidet.

% ---- Peano ----
:- pred nato(peano).
:- mode nato(in) is det.

:- pred addo(peano, peano, peano).
:- mode addo(in, in, out) is det.
:- mode addo(in, out, in) is semidet.
:- mode addo(out, in, in) is semidet.
:- mode addo(out, out, in) is multi.

:- pred mulo(peano, peano, peano).
:- mode mulo(in, in, out) is det.

:- func add_f(peano, peano) = peano.
:- func mul_f(peano, peano) = peano.

% ---- bits / adder ----
:- pred bit_xoro(bit, bit, bit).
:- mode bit_xoro(in, in, out) is det.
:- mode bit_xoro(in, out, in) is semidet.
:- mode bit_xoro(out, in, in) is semidet.
:- mode bit_xoro(in, in, in) is semidet.
:- mode bit_xoro(out, out, in) is multi.

:- pred bit_ando(bit, bit, bit).
:- mode bit_ando(in, in, out) is det.
:- mode bit_ando(in, in, in) is semidet.

:- pred half_addero(bit, bit, bit, bit).
:- mode half_addero(in, in, out, out) is det.

:- pred full_addero(bit, bit, bit, bit, bit).
:- mode full_addero(in, in, in, out, out) is det.
:- mode full_addero(in, in, in, in, in) is semidet.

:- pred ripple_addero(list(bit), list(bit), bit, list(bit), bit).
:- mode ripple_addero(in, in, in, out, out) is semidet.

% ---- SMT stub + path ----
:- pred smt_sato(smt, bool).
:- mode smt_sato(in, out) is det.
:- mode smt_sato(in, in) is semidet.

:- pred edgeo(node, node, smt).
:- mode edgeo(in, in, out) is nondet.
:- mode edgeo(out, out, out) is multi.
:- mode edgeo(in, out, out) is nondet.

:- pred patho(node, node, list(node), smt).
:- mode patho(in, in, out, out) is nondet.
:- mode patho(out, out, out, out) is nondet.

% ---- FSM / refine ----
:- pred fsmo(fsm_state, bit, fsm_state, bit).
:- mode fsmo(in, in, out, out) is det.
:- mode fsmo(in, in, in, in) is semidet.
:- mode fsmo(out, out, out, out) is multi.

:- pred refineo(abs_val, int).
:- mode refineo(in, in) is semidet.
:- mode refineo(in, out) is nondet.

:- implementation.

:- import_module int.
:- import_module string.

% ---- lists ----
appendo([], S, S).
appendo([A | D], S, [A | Res]) :-
    appendo(D, S, Res).

membero(X, [X | _]).
membero(X, [_ | D]) :-
    membero(X, D).

rembero(X, [X | D], D).
rembero(X, [A | D], [A | Res]) :-
    A \= X,
    rembero(X, D, Res).

reverseo(L, O) :-
    reverseo_acc(L, [], O).

:- pred reverseo_acc(list(T), list(T), list(T)).
:- mode reverseo_acc(in, in, out) is det.
:- mode reverseo_acc(out, in, in) is det.
reverseo_acc([], Acc, Acc).
reverseo_acc([A | D], Acc, O) :-
    reverseo_acc(D, [A | Acc], O).

lengtho([], z).
lengtho([_ | D], s(N)) :-
    lengtho(D, N).

distincto([]).
distincto([A | D]) :-
    not membero(A, D),
    distincto(D).

% ---- Peano ----
nato(z).
nato(s(P)) :-
    nato(P).

addo(z, Y, Y).
addo(s(X), Y, s(Z)) :-
    addo(X, Y, Z).

mulo(z, _, z).
mulo(s(X), Y, Z) :-
    mulo(X, Y, Z1),
    addo(Y, Z1, Z).

add_f(z, Y) = Y.
add_f(s(X), Y) = s(add_f(X, Y)).

mul_f(z, _) = z.
mul_f(s(X), Y) = add_f(Y, mul_f(X, Y)).

% ---- bits ----
bit_xoro(b0, b0, b0).
bit_xoro(b0, b1, b1).
bit_xoro(b1, b0, b1).
bit_xoro(b1, b1, b0).

bit_ando(b0, b0, b0).
bit_ando(b0, b1, b0).
bit_ando(b1, b0, b0).
bit_ando(b1, b1, b1).

half_addero(X, Y, R, C) :-
    bit_xoro(X, Y, R),
    bit_ando(X, Y, C).

full_addero(Cin, X, Y, R, Cout) :-
    half_addero(X, Y, W, C1),
    half_addero(W, Cin, R, C2),
    bit_xoro(C1, C2, Cout).

ripple_addero([], [], Cin, [], Cin).
ripple_addero([X | Xs], [Y | Ys], Cin, [R | Rs], Cout) :-
    full_addero(Cin, X, Y, R, C1),
    ripple_addero(Xs, Ys, C1, Rs, Cout).

% ---- SMT stub: reject phi /\ ~phi at top-level flatten ----
smt_sato(Phi, Sat) :-
    atoms(Phi, As),
    ( unsat_pair(As) -> Sat = no ; Sat = yes ).

:- pred atoms(smt::in, list(smt)::out) is det.
atoms(smt_and(A, B), Xs) :-
    atoms(A, Xs1),
    atoms(B, Xs2),
    appendo(Xs1, Xs2, Xs).
atoms(smt_not(P), [smt_not(P)]).
atoms(atom(S), [atom(S)]).

:- pred unsat_pair(list(smt)::in) is semidet.
unsat_pair(As) :-
    membero(P, As),
    membero(smt_not(P), As).

edgeo(0, 1, atom("bv_slt_x_y")).
edgeo(1, 2, atom("bv_slt_y_z")).
edgeo(2, 3, atom("bv_sgt_z_x")).
edgeo(3, 1, smt_and(atom("p"), smt_not(atom("q")))).

patho(X, Y, [Y], Phi) :-
    edgeo(X, Y, Phi),
    smt_sato(Phi, yes).
patho(X, Y, [Z | P2], smt_and(E, Phi2)) :-
    edgeo(X, Z, E),
    patho(Z, Y, P2, Phi2),
    not membero(Z, P2),
    smt_sato(smt_and(E, Phi2), yes).

% ---- FSM / refine ----
fsmo(s0, b0, s0, b0).
fsmo(s0, b1, s1, b0).
fsmo(s1, b0, s0, b1).
fsmo(s1, b1, s1, b1).

refineo(conc(C), C).
refineo(top, _).
refineo(interval(Lo, Hi), N) :-
    N >= Lo,
    N =< Hi.

:- end_module lattice_kernel.