:- use_module(library(pio)).

parse_cnf(File,Formula) :-
    phrase_from_file(spec(_NumVar,_NumCs,Cs),File),
    clauses_frm(Cs,Formula).

% parse integer excluding sign

integer(I) -->
    digit(D0),
    digits(D),
    { number_codes(I, [D0|D]) }.

digits([D|T]) -->
    digit(D), !,
    digits(T).
digits([]) -->
    "".

digit(D) -->
    [D],
    { code_type(D, digit) }.

:- \+ phrase(integer(_I),`-17`).
:- phrase(integer(_I),`7`).

% auxiliary predicates for parsing

anychar -->
    [C],
    {code_type(C,ascii)}.

anything -->
    "".
anything -->
    anychar,
    anything.

blanks -->
    " ".
blanks -->
    " ",
    blanks.

:- phrase(blanks,` `).

empty_or_blanks -->
    "".
empty_or_blanks -->
    blanks.

new_lines -->
    "".
new_lines -->
    blanks_newline,
    new_lines.

blanks_newline -->
    "", 
    new_line.
blanks_newline -->
    blanks, 
    new_line.

new_line -->
    [C],
    {code_type(C,newline)}.

% spec(NumVar,NumCs,Cs) specifies a clause in CNF format,
% NumVar and NumCs is the number of variables/clauses respectively;
% CS is a list of an integer list representing the clause set


spec(NV,NC,Cs) -->
    comments,
    new_line,
    preamble(NV,NC), 
    blanks_newline,
    clauses(Cs).

comments -->
    "c", !, anything.
comments -->
    "c", !, anything,
    new_line,
    comments.

:- phrase(comments,`c start with comments`).

preamble(NV,NC) -->
    "p", blanks, "cnf", blanks,
    integer(NV), blanks,
    integer(NC).

:- phrase(preamble(NV,NC),`p cnf 5 3`), NV=5, NC=3.

clauses([C]) -->
    clause(C).
clauses([C|Cs]) -->
    clause(C),
    blanks_newline,
    clauses(Cs).

clause([]) -->
    "0".
clause([A|As]) -->
    integer(A),
    blanks,
    clause(As).
clause([neg(A)|As]) -->
    "-", integer(A),
    blanks,
    clause(As).
    
:- phrase(clause(As),`-3 -4 0`), As = [neg(3), neg(4)].
:- phrase(clauses(Cs),`-3 -4 0`), Cs = [[neg(3), neg(4)]].

% spec_formula(NV,NC,Cs,Frm) <- transform list of clauses
% into Smullyan's formula representation

?-op(140,fy,neg).
?-op(160, yfx, [and, or]).
?-op(180, xfy, [imp]).

clauses_frm([C],(Frm)) :-
    clause_frm(C,Frm).
clauses_frm([C|Cs],and(Frm,Frms)) :-
    clause_frm(C,Frm),
    clauses_frm(Cs,Frms).

clause_frm([A],A).
clause_frm([A|As],A or Frm) :-
    clause_frm(As,Frm).

:- clause_frm([neg(3), neg(4)],Frm), Frm = neg 3 or neg 4.
:- Cs = [[1, neg(5), 4], [neg(1), 5, 3, 4], [neg(3), neg(4)]], clauses_frm(Cs,Frm), Frm = 1 or (neg 5 or 4)and(neg 1 or (5 or (3 or 4)) and (neg 3 or neg 4)).
:- phrase_from_file(spec(_NumVar,_NumCs,Cs),'test.cnf'), clauses_frm(Cs,_Frm).
:- parse_cnf('test.cnf',Frm), Frm = 1 or (neg 5 or 4)and(neg 1 or (5 or (3 or 4))and(neg 3 or neg 4)).