% trs2dfg(InFile,OutFile) << Infile >> Outfile <-- succeeds if TRS format is transformed into DFG format

:- use_module(library(pio)).
?-op(140,fy, [+, -]).

%trs2dfg(TRS,DFG) <-- succeeds if TRS is the content of a TRS file and DFG
%                     is the output in DFG format				

trs2dfg(InFile,OutFile) :-
    phrase_from_file(spec(Vars,Es),InFile),
    equations_functions(Vars,Es,Fs),
    generate_dfg(Vars,Fs,Es,OutFile).

% member/3 <-- member for difference lists,
% checks that X is not contained in Ys
% not efficient

member(X,Xs,Ys) :-
	nonvar(Xs),
	var(Ys),
	Xs = [X|_].
member(X,Xs,Ys) :-
	nonvar(Xs),
	nonvar(Ys),
	Xs = [X|_],
	Ys \= [X|_].
member(X,Xs,Ys) :-
	nonvar(Xs),
	Xs = [_|Xs1],
	member(X,Xs1,Ys).

:- member(a,[a|Xs],Xs).
:- \+ member(b,[a,b],[b]).
:- member(a,[b,a],[]).

% equations_functions(Vars,Es,Fs) <--

equations_functions(Vars,Es,Fs) :-
    equations_functions(Es,Vars,[],Fs).

equations_functions([],_Vars,Fs,Fs).
equations_functions([equal(Term1,Term2)|Es],Vars,Fs0,Fs) :-
    term_functions(Term1,Vars,Fs0,Fs1),
    term_functions(Term2,Vars,Fs1,Fs2),
    equations_functions(Es,Vars,Fs2,Fs).

term_functions(Var,Vars,Fs,Fs) :-
    member(Var,Vars).
term_functions(Term,Vars,Fs0,Fs) :-
    \+ member(Term,Vars),
    Term =.. [F|Args],
    length(Args,N),
    \+ member((F,N),Fs0),
    append(Fs0,[(F,N)],Fs1),
    terms_functions(Args,Vars,Fs1,Fs).
term_functions(Term,Vars,Fs0,Fs) :-
    \+ member(Term,Vars),
    Term =.. [F|Args],
    length(Args,N),
    member((F,N),Fs0),    
    terms_functions(Args,Vars,Fs0,Fs).

terms_functions([],_Vars,Fs,Fs).
terms_functions([T|Ts],Vars,Fs0,Fs) :-
    term_functions(T,Vars,Fs0,Fs1),
    terms_functions(Ts,Vars,Fs1,Fs).


%generate_dfg(ES,DFG) <-- transforms equational system ES = es(Vars,Equations) 
%                         to DFG syntax

generate_dfg(Vars,Fs,Es,OutFile) :-
    open(OutFile,write,FD,[]),
    begin_problem(FD),
    preamble(FD),
    symbols(FD,Fs),
    axioms(FD,Vars,Es),
    settings(FD),
    end_problem(FD),
    close(FD).


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

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

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

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

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(Vs,Es) <-- (Vs,Es) is a representation of an equational system consisting of
%               a list of variables and a list of equations

spec(Vars,Equations) --> 
    other_decl,
    new_lines,
    "(", var_decl(Vars), empty_or_blanks, ")",
    new_lines,
    other_decl,
    new_lines,
    "(", rules_decl(Equations), 
    blanks_newline, 
    ")",
    new_lines,
    other_decl,
    new_lines.

var_decl(Vars) -->
    "VAR", blanks,
    vars(Vars).

vars([V]) --> 
    var(V).
vars([V|Vs]) -->
    var(V),
    blanks,
    vars(Vs).

var(V) -->
    id(Cs),
    {atom_codes(V,Cs)}.

% id(Cs) <-- id are non-empty sequences of characters except space, '(', ')', '"' and ','

id([C]) --> 
    [C],
    {tpdb_char(C)}.
id([C|Cs]) -->
    [C],
    {tpdb_char(C)},
    id(Cs).

tpdb_char(C) :-
    code_type(C,ascii),
    \+ member(C,[32,34,40,41]).

rules_decl(Equations) -->
    "RULES", 
    blanks_newline,
    rules(Equations).

rules([E]) -->
    empty_or_blanks,
    rule(E).
rules([E|Es]) -->
    empty_or_blanks, 
    rule(E),
    blanks_newline,
    rules(Es).

rule(equal(Term1,Term2)) -->
    term(Term1), 
    blanks, "->", blanks, 
    term(Term2).
rule(equal(Term1,Term2)) -->
    term(Term1), 
    blanks, "->", blanks_newline, 
    term(Term2).

% special symbols *, + , -, /, ,
contains_special_symbols(Cs) :-
    member(42,Cs) ;
    member(43,Cs) ;
    member(44,Cs) ;
    member(45,Cs) ;
    member(46,Cs) ;
    member(47,Cs) ;
    member(64,Cs).


symbol(Id) -->
    id(Cs),
    {
	\+ contains_special_symbols(Cs),
	atom_codes(Id,Cs)
    }.
symbol(times) -->
    "*".
symbol(plus) -->
    "+".
symbol(minus) -->
    "-".
symbol(quot) -->
    "/".
symbol(app) -->
    "@".
symbol(dot) -->
    ".".

term(Id) -->
    symbol(Id).
term(Id) -->
    symbol(Id), "(", ")".
term(Term) -->
    symbol(Id), 
    "(", termlist(Ts), ")",
    {
	Term =.. [Id|Ts]
    }.

termlist([Term]) -->
    term(Term).
termlist([T|Ts]) -->
    term(T), 
    ",", empty_or_blanks,
    termlist(Ts).

other_decl -->
    "".
other_decl -->
    "(", other_decl_aux, ")".
other_decl -->
    "(", other_decl_aux,
    blanks_newline,
    ")".

other_decl_aux -->
    "THEORY", blanks, anything.
other_decl_aux -->
    "STRATEGY", blanks, anything.
other_decl_aux -->
    "COMMENT", blanks, anything.
other_decl_aux -->
    "from", blanks, anything.

begin_problem(FD) :-
    format(FD,'begin_problem(Generated).~n~n',[]).

preamble(FD) :-
    format(FD,'list_of_descriptions.~n',[]),   
    format(FD,'name({* generated *}).~n',[]),
    format(FD,'author({* Georg Moser *}).~n',[]),
    format(FD,'status(satisfiable).~n',[]),
    format(FD,'description({* generated *}).~n',[]),
    format(FD,'end_of_list.~n~n',[]).

symbols(FD,Fs) :-
    format(FD,'list_of_symbols.~n',[]),
    format(FD,'        functions~w. ~n',[Fs]),
    format(FD,'end_of_list.~n~n',[]).

axioms(FD,Vars,Es) :-
    format(FD,'list_of_formulae(axioms).~n',[]),
    equations(FD,Vars,Es),
    format(FD,'end_of_list.~n~n',[]).

equations(_FD,_Vars,[]).
equations(FD,Vars,[E|Es]) :-
    format(FD,'        formula(forall(~w,~w)).~n',[Vars,E]),
    equations(FD,Vars,Es).

settings(FD) :-
    format(FD,'list_of_settings(SPASS).~n',[]),
    format(FD,'{*~n',[]),
    format(FD,'set_flag(DocProof,1).~n',[]),
    format(FD,'*}~n',[]),
    format(FD,'end_of_list.~n~n',[]).

end_problem(FD) :-
    format(FD,'end_problem.',[]).

    
:- phrase(rule(E),"p1(x,0()) -> x"), phrase(vars(Vars),"x y z"), equations_functions([E],Vars,[],Fs), Fs = [(p1,2),('0',0)].