Relicense under the Sovereign Leviathan covenant; remove MIT and Apache

055a27e verified 27 days ago

6.28 kB

%-----------------------------------------------------------------------------%
% 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.

	%-----------------------------------------------------------------------------%
	% 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.