% -*- Mode: Prolog -*-
% SPDX-FileCopyrightText: 2026  Jonas Smedegaard <dr@jones.dk
% SPDX-License-Identifier: GPL-3.0-or-later
%
% Tableau-rules expansion of a propositional formula.
%
%% Usage, with REPL or non-interactively:
%% swipl -q formulator.prolog
%% swipl -g 'QUERY.' -t halt. formulator.prolog
%% gprolog --consult-file formulator.prolog
%% gprolog --query-goal "consult('formulator.prolog'), QUERY, halt"
%%
%% QUERY examples with expected response (indented):
%% complete([not(not(q))])
%%   Complete tableau: [[q]]
%% complete([not(and(p,and(not(not(q)),q)))])
%%   Complete tableau: [[not(p),not(q),not(q)]]

% log messages to console
info(String) :- format('~w~n', [String]).
info(String, Term) :- format('~w: ~w~n', [String, Term]).
warn(String) :- format('Warning: ~w~n', [String]).
warn(String, Term) :- format('Warning: ~w: ~w~n', [String, Term]).

%% first_item(Item, List)
%
% Item is the first item of List if List is non-empty
first_item([Item|_], Item).

%% distribute(Formula, TableauIn, TableauOut)
%
% TableauOut is TableauIn with Formula prepended to each branch
distribute(_, [], []).
distribute(Formula, [Rest|TableauIn], [[Formula|Rest]|TableauOut]) :-
    distribute(Formula, TableauIn, TableauOut).

%% well_formed_formula(Formula)
%
% True when Formula is a valid propositional formula
well_formed_formula(Formula) :-
    atom(Formula).
well_formed_formula(Formula) :-
    compound_formula(Formula).

%% well_formed(FormulaBranch)
%
% True when FormulaBranch is a list of well-formed formulas
well_formed([]).
well_formed([Formula|Rest]) :-
    well_formed_formula(Formula),
    well_formed(Rest).

%% compound_formula(Formula)
%
% True when Formula is a compound propositional formula
compound_formula(not(Formula)) :-
    well_formed_formula(Formula).
compound_formula(and(Formula1, Formula2)) :-
    well_formed_formula(Formula1),
    well_formed_formula(Formula2).

%% expand_branch(Formula, Branch, BranchExpanded)
%
% BranchExpanded is Branch with Formula expanded and prepended
expand_branch(Formula, Branch, BranchExpanded) :-
    expand([Branch], Branches),           % reuses expand/2 for branches
    distribute(Formula, Branches, BranchExpanded).

%% has_expansion_rule(Formula)
%
% True when Formula is handled by a specific expansion rule
has_expansion_rule(not(not(_))).
has_expansion_rule(and(_,_)).
has_expansion_rule(not(and(_,_))).

%% expand(TableauIn, TableauOut)
%
% TableauOut is TableauIn with branches expanded
expand([], []).
expand([[]|TableauIn], [[]|TableauOut]) :-
    expand(TableauIn, TableauOut).

% TableauOut is TableauIn with first formula of first branch expanded
expand([[Formula|Branch]|Rest], TableauOut) :-
    \+ has_expansion_rule(Formula), % omit separately handled expansions
    expand_branch(Formula, Branch, Expanded),
    expand(Rest, ExpandedRest),
    append(Expanded, ExpandedRest, TableauOut).

% Expansion by double negation
expand([[not(not(Formula))|Branch]|Rest], TableauOut) :-
    expand([[Formula|Branch]|Rest], TableauOut).

% Expansion by conjunction
expand([[and(Formula1, Formula2)|Branch]|Rest], Tableau) :-
    expand([[Formula1, Formula2|Branch]|Rest], Tableau).

% Expansion by nonconjunction
expand([[not(and(Formula1, Formula2))|Branch]|Rest], Tableau) :-
    expand([[not(Formula1), not(Formula2)|Branch]|Rest], Tableau).

complete(FormulaBranch) :-
    well_formed(FormulaBranch),
    expand([FormulaBranch], Tableau),
    info('Complete tableau', Tableau).

% FIXME: needs to drop contradicting branches before checking if empty
open(FormulaBranch) :-
    expand(FormulaBranch, Tableau),
    first_item(_, Tableau),
    info('Tableau is open');
    warn('Tableau is closed'), false.

% TODO
%sound(FormulaBranch) :-
%    well_formed(FormulaBranch),
%    expand([FormulaBranch], Tableau),
%    member(OpenBranch, Tableau),
%    info('Formula is sound (i.e. satisfiable)');
%    warn('Formula is unsound (i.e. not satisfiable)'), false.

%% testsuite for SWI Prolog
%
% Usage: swipl -g run_tests. -t halt. formulator.prolog
:- if(current_prolog_flag(dialect, swi)).
:- begin_tests(lists).
test(well_formed_atomic, [nondet]) :-
    well_formed_formula(q).
test(unwell_formed_nothing, [nondet]) :-
    \+ well_formed_formula([]).
test(unwell_formed_connective, [nondet]) :-
    \+ well_formed_formula(non(q)).
test(well_formed_compound, [nondet]) :-
    well_formed_formula(not(not(q))).
test(unwell_formed_compound, [nondet]) :-
    \+ well_formed_formula(and(not(q))).
test(not, [nondet]) :-
    expand([[not(not(q))]], [[q]]).
test(not_not, [nondet]) :-
    expand(
        [[p, not(not(q)), r], [p,not(not(q)), not(not(not(q))), r], [s]],
        [[p, q, r], [p, q, not(q), r], [s]]
    ).
test(and, [nondet]) :-
    expand([[and(p, q)]], [[p, q]]).
test(not_and, [nondet]) :-
    expand(
        [[p, not(not(and(s, q))), and(and(not(q), p), s), r], [s]],
        [[p, s, q, not(q), p, s, r], [s]]
    ).
:- endif.