%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%     FLOPER: Fuzzy LOgic Programming Environment for Research.         %%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%           %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% INTERFACE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%           %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

user_help :- menu.

title :- nl,write('######################################################################'),
	nl,nl,
	write('     ########   ##        #######   ########   ######   ########   '),nl,
	write('     ##         ##        ##   ##   ##    ##   ##       ##    ##   '),nl,
	write('     **         **        **   **   **    **   **       **    **   '),nl,
	write('     *****      **        **   **   ********   ******   ********   '),nl,
	write('     **         **        **   **   **         **       **  **     '),nl,
	write('     oo         oo        oo   oo   oo         oo       oo   oo    '),nl,
	write('     oo         ooooooo   ooooooo   oo         oooooo   oo    oo   '),nl,nl,
	write('    **  Fuzzy  LOgic  Programming  Environment  for  Research  **  '),nl,nl,
	write('    **                          v 2.0                          **  '),nl,
	nl,
	write('ooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo'),nl.

menu :-   nl,nl,write('		*****  PROGRAM    MENU      *******'),nl,  
	write('**  parse  --> Parse/load a fuzzy prolog file (.fpl) 	**'),nl,
	write('**  save   --> Parse/load/save a fuzzy prolog file.  	**'),nl,
	write('**  load   --> Consult a prolog file (.pl). 	    	**'),nl,
	write('**  list   --> Displays the last loaded clauses.     	**'),nl,  
	write('**  clean  --> Clean the database 			**'),nl,nl,

	write('		*****  LATTICE    MENU      *******'),nl,  
	write('**  lat    --> Load a Multi-Adjoint lattice	     	**'),nl,
	write('**  show   --> Show current Multi-Adjoint lattice	**'),nl,
	write('**  ismode --> Select kind of interpretive steps	**'),nl,nl,

	write('		*****  GOAL    MENU    	    *******'),nl,  
	write('**  intro  --> Introduce a new goal (between quotes). 	**'),nl,
	write('**  run    --> Execute a goal completely 		**'),nl,
	write('**  depth  --> Set the maximum level of execution trees **'),nl,
	write('**  leaves --> Interprete a goal                        **'),nl,
	write('**  tree   --> Generate a partial execution tree        **'),nl,nl,

	write('		*****  TRANSFORMATION  MENU *******'),nl, 
	write('%%  pe     -->  Partial evaluation 			%%'),nl,
	write('%%  fu     --> Fold/Unfold Transformations 		%%'),nl,
	write('%%  red    --> Reductants Calculus 			%%'),nl,nl,

	write('---------------------------------------------------------'),nl,nl,

	write('**  stop      --> Stop the execution of the parser. 	**'),nl,
	write('**  quit      --> Exit to desktop.                  	**'),nl,nl,

	write('---------------------------------------------------------'),nl,nl.

shell_synth :- nl,write('>> '), read(Command), (Command=end_of_file;catch(call(Command),_,print_err),!,shell_synth).

print_err :- nl,write('Error...'),nl,!,shell_synth.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PROGRAM MENU OPTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% PARSE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

parse :- write('File to parse: '),read(_File),parser(_File,'tmp_fuzzy-prolog.pl'),nl,list.

parser(Source,Destiny) :- open(Source,read,Stream),to_list(Stream,Text),close(Stream),
		clean(Text,Input),begin(Output,Output9,Input,Errors),
		( Errors>0,!, nl, write('Unable to parse'),nl
		; Errors=0,!,
		open(Destiny,write,Stream2),to_file(Stream2,Output),close(Stream2), 
		open('tmp_fuzzy-inter.pl',write,Stream9),to_file(Stream9,Output9),close(Stream9),
		fpl:consult(Destiny), consult('tmp_fuzzy-inter.pl'),
		retractall(loaded_file_fpl(_)), assert(loaded_file_fpl(Source))).

begin(Output,Output9,Input,E) :- assert(line(1)), assert(last_rule_index(0)), assert(last_var_index(1)), assert(num_errors(0)),
		begin2(Output,Output9,Input),retractall(line(_)),retractall(last_rule_index(_)), retractall(last_var_index(_)),
		retract(num_errors(E)),retractall(num_errors(_)),nl,write(E),write(' errors.'),nl.
begin2(Output,Output9,Input) :- catch(program(Output,Output9,Input,[]),_,(nl,write('Translation failed.'),nl)),!.
begin2(_,_,_) :- nl,write('Translation failed'),nl.

%% Puts the file in a list %%
to_list(Stream,Text) :- get_code(Stream,X),
 (X==9,Text=[' '|Text2],!,to_list(Stream,Text2) % ignore 'tab' and puts a blank 
 ;X\==(-1),name(P,[X]),Text=[P|Text2],!,to_list(Stream,Text2) 
 ;X==(-1),Text=[]). % EOF

%% Returns a char list from a code list.
to_char_list([A|B],[Ca|Cb]):-name(Ca,[A]),to_char_list(B,Cb).
to_char_list([],[]).

%% clean the list
clean(['%'|Text1],Text3) :- clean_simple_comment(Text1,Text2),clean(Text2,Text3). % ignore simple comment
clean(['/','*'|Text1],Text3) :- clean_complex_comment(Text1,Text2),clean(Text2,Text3). % ignore complex comment
clean([X|Text1],[X|Text2]) :- clean(Text1,Text2).
clean([],[]).

clean_simple_comment(['\r'|Text],['\r'|Text]) :- !. % RC  
clean_simple_comment(['\n'|Text],['\n'|Text]) :- !. % New line
clean_simple_comment([_|Text1],Text2) :- clean_simple_comment(Text1,Text2). % Any other symbol
clean_simple_comment([],[]). % sure terminate

clean_complex_comment(['*','/'|Text],Text) :- !.
clean_complex_comment([_|Text1],Text2) :- clean_complex_comment(Text1,Text2). % Any other symbol
clean_complex_comment([],_) :- error('Complex comment must end with \'*/\'.'). 

%% The final list (with prolog code) is written into a file.
to_file(File,[X|Text]) :- 
  (number(X),name(X,[K|J]),char_code(T,K),put_char(File,T),(empty(J),to_file(File,Text);aux_to_file(File,J),to_file(File,Text)) % If a number is read, it is converted into a char so we can it write in the file. If it has more than one digit, 'aux_to_file' is called so that the number can be written. %    
     ;put_char(File,X),to_file(File,Text)),!.
to_file(_,[]).
empty([]).

%% 'List' contains the remaining digits's ASCII codes   
aux_to_file(File,List) :- nth_(1,List,First,Tail),char_code(T,First),put_char(File,T),aux_to_file(File,Tail). 
aux_to_file(_,[]).

%% SAVE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

save :- write('File to parse: '),read(_File), write('Save to: '),read(Save),
	parser(_File,Save).

%% LOAD %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

load :- write('File to load: '),read(_File),fpl:consult(_File),retractall(loaded_file_pl(_)),assert(loaded_file_pl(_File)).

%% LIST %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

list :- try((loaded_file_pl(PL), list_pl(PL)),(write('No loaded files'),nl)),
	try((loaded_file_fpl(FPL), list_fpl(FPL)),write('No parsed files')),nl.

list_pl(P):- nl, write('LOADED FILES CODE:'), nl,nl, list(P).
list_fpl(P):- nl, write('ORIGINAL FUZZY-PROLOG CODE:'), nl,nl, list(P),
		nl,write('GENERATED PROLOG CODE:'),nl,nl,list('tmp_fuzzy-prolog.pl').

list(F) :- open(F,read,Stream),to_list(Stream,List),clean(List,Text),print_list(Text),nl,close(Stream).
print_list([]).
print_list([C|T]) :- (C == 'end_of_file'
		     ;write(C),print_list(T)).

%% CLEAN %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

clean :- floper_default, assert(loaded_file_lat('num.lat')),wipe_module(fpl).

%% STOP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

stop :- retractall(floper_depth(_)), retractall(floper_goal(_)), retractall(floper_ismode(_)),
	retractall(loaded_file_fpl(_)),retractall(loaded_file_pl(_)),retractall(loaded_file_lat(_)),
	wipe_module(fpl), wipe_module(lat).

%% QUIT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

quit :- stop, del_file('tmp_fuzzy-prolog.pl'),del_file('tmp_fuzzy-inter.pl'), wipe_module(user).

del_file(F) :- exists_file(F), !, delete_file(F).
del_file(_).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LAT MENU OPTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% LAT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

lat :- try(loaded_file_lat(L),(assert(loaded_file_lat(null)),L=null)),
	write('Current lattice: '), write(L),nl,
	write('Introduce new lattice: '), read(N), wipe_module(lat),
	lat:consult(N), lat_test, retractall(loaded_file_lat(_)),assert(loaded_file_lat(N)),nl.

lat_test:- nl, (current_predicate(lat:member/1), write('member/1 OK') ; write('WARNING: member/1 is not defined')),
	nl, (current_predicate(lat:bot/1),    write('bot/1 OK')    ; write('WARNING: bot/1 is not defined')),
	nl, (current_predicate(lat:top/1),    write('top/1 OK')    ; write('WARNING: top/1 is not defined')),
	nl, (current_predicate(lat:leq/2),    write('leq/2 OK')    ; write('WARNING: leq/2 is not defined')),
	nl, (current_predicate(lat:members/1),write('Finite lattice') ; write('Infinite lattice')).

%% SHOW %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

show :- nl, try((loaded_file_lat(LAT), list_lat(LAT)),write('No loaded lattices')).
list_lat(LAT) :- nl, write('MULTI-ADJOINT LATTICE:'), nl, list(LAT).

%% ISMODE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

ismode :- try(floper_ismode(O),(assert(floper_ismode(m)),O=m)), write('Current mode: '), write(O), nl, write('Introduce new mode (l=large, m=medium, s=small): '),
	read(X), (valid_ismode(X),!, retractall(floper_ismode(_)),assert(floper_ismode(X)), nl ;
	write(X), write(' is not a valid interpretive mode'), nl).
valid_ismode(s).
valid_ismode(m).
valid_ismode(l).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GOAL MENU OPTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% INTRO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

intro :- write('Current goal: '), try(floper_goal(G_old),G_old='p(X)'), write(G_old),nl,
	write('Introduce new Goal: '), read(Goal), retractall(floper_goal(_)),assert(floper_goal(Goal)).

%% RUN %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

run :-  floper_goal(Goal),(Goal == 'empty', write('There is no goal introduced yet!!!!!');
	term2char(Goal,List),clear_run,
	assert(line(1)), assert(last_var_index(1)), assert(num_errors(0)),
	catch(body(Fuz_goal0,_,['T',r,u,t,h,'_',d,e,g,r,e,e,')'],P,List,[]),_,(clear_run,!,false)),
	clear_run, appendc(Fuz_goal0,P,Fuz_goal), to_string(Fuz_goal,Code_goal,_),append(Code_goal,".",Code),
	read_term_from_chars(Code,Fin_goal,[variable_names(V),singletons(_)]), run2(Fin_goal,V)).
run2(Fin_goal,V) :- on_exception(_,setof(V,fpl:Fin_goal,Sol),(write('There is no solution.'),Sol=[])),print_exe(Sol),!.
run2(_) :- write('There is no solution.').

%% Retract parsing information
clear_run :- retractall(line(_)),retractall(last_var_index(_)),retractall(num_errors(_)).

%% Returns a List and a Code_list from an Atom.---> [b,o,d,y] ---> [98,111,100,99] ---> body
to_string(List,Code_list,Atom) :-aux(List,Code_list), name(Atom,Code_list).
aux([],[]).
aux([H|T],[H1|T1]):-name(H,[H1]),aux(T,T1). 

%%%% Prints each solution in a new line, without temporal variables.
print_exe([]).
print_exe([H|T]) :- write(H),nl,print_exe(T).


%% DEPTH %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

depth :- retract(floper_depth(D_old)),write('Current depth: '),write(D_old),nl,
	write('Introduce new depth: '), read(Depth), assert(floper_depth(Depth)).

%% TREE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

tree :- retractall(varcont(_)),assert(varcont(0)), floper_depth(D), floper_ismode(I), floper_goal(Goal),
	(Goal == 'empty', write('There is no goal introduced yet!!!!!');
	term2char(Goal,List),clear_run,
	assert(line(1)), assert(last_var_index(1)), assert(num_errors(0)),
	catch(body(_,Fuz_goal,_,_,List,[]),_,(clear_run,!,false)),
	clear_run, to_string(Fuz_goal,Code_goal,_),append(Code_goal,".",Code),
	read_from_chars(Code,Fin_goal),
	write('R0'),print_state(state(Fin_goal,[])),nl, tree2(D,I,state(Fin_goal,[]),1)), retract(varcont(_)).

tree2(D,I,S,N):- D>N, step(I,S,F,R), tree3(D,I,F,R,N),fail.
tree2(_,_,_,_).

tree3(D,_,_,_,D).
tree3(D,I,F,R,N) :- D>N, indent(N), write(R), print_state(F),nl, M is N+1, tree2(D,I,F,M).

indent(0):- !.
indent(N):- write('    '), M is N-1, indent(M).

%% LEAVES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

leaves :- retractall(varcont(_)),assert(varcont(0)), floper_depth(D), floper_goal(Goal),
	(Goal == 'empty', write('There is no goal introduced yet!!!!!');
	term2char(Goal,List),clear_run,
	assert(line(1)), assert(last_var_index(1)), assert(num_errors(0)),
	catch(body(_,Fuz_goal,_,_,List,[]),_,(clear_run,!,false)),
	clear_run, to_string(Fuz_goal,Code_goal,_),append(Code_goal,".",Code),
	read_from_chars(Code,Fin_goal),nl,leaves2(D,state(Fin_goal,[]),0)).

leaves2(D,S,N):- D>N, step('l',S,F,_), leaves3(D,F,N), fail.
leaves2(_,S,_):- \+(step('l',S,_,_)),print_state(S),nl.
leaves2(_,_,_).

leaves3(D,_,D).
leaves3(D,F,N) :- D>N, M is N+1, leaves2(D,F,M).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                             %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% TRANSFORMATION MENU OPTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                             %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Partial evaluation
pe :- write('Sorry, this option is not implemented yet!!!'),nl.

%% Fold/unfold transformation
fu :- write('Sorry, this option is not implemented yet!!!'),nl.

%% Reductant calculus
red :- write('Sorry, this option is not implemented yet!!!'),nl.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PARSER %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% A program is a set of sentences and declarations which can also begin with blanks. If there is an error, the option 'error' is chosen. %%

error(S) :- 	try(line(L),(assert(line(0)),L=0)), write('Line: '), write(L), write('. Error: \''), write(S),
		write('\' expected'),nl,retract(num_errors(E)),E2 is E+1, assert(num_errors(E2)).
new_line :- 	retract(line(N)), M is N+1, assert(line(M)).
new_var(R) :-	retract(last_var_index(N)), M is N+1, assert(last_var_index(M)),
		(N=0,R=['T','V',0]; N>0,name(N,Mn),to_char_list(Mn,X),R=['_','T','V'|X]).
reset_var :-	retract(last_var_index(_)), assert(last_var_index(1)).
new_rule(X) :-	retract(last_rule_index(N)),M is N+1,assert(last_rule_index(M)),
				name(M,Mn),to_char_list(Mn,X).
term2char(T,C) :- write_to_chars(T,N), to_char_list(N,C).

%% appendc: appends two strings with a colon.
appendc([],X,X).
appendc(X,[],X).
appendc(X,Y,Z):-append(X,[','|Y],Z).

wait(X,_) --> [X],!.
wait(X,S) --> {error(S),!}, wait2(X).
wait2(X) --> [X],!.
wait2(X) --> [A], {\+(A='.'),(A='\n',new_line;true)},!, wait2(X).
wait2(_) --> [].

blank --> [' '], blanks.
blank --> ['\r'], {new_line}, blanks.
blank --> ['\n'], {new_line}, blanks.
blank --> ['\t'], blanks.
blanks --> blank.
blanks --> [].

%% program

program(H,L) --> blanks, rules(H,L).

rules(Ph,Pl) --> declarations(D), rules(Ph2,Pl), {append(D,['\n'|Ph2],Ph)}.
rules(Ph,Pl) --> rule(Rh,Rl), rules(Ph2,Pl2), {append(Rh,Ph2,Ph), append(Rl,Pl2,Pl)}.
rules([],[]) --> [].

declarations(Expr) --> ['$'],!,allbut('$',Expr),wait('$','$'),blanks.

allbut(C,Id) --> allbut2(C,Id),!.
allbut2(C,['\r'|Id]) --> ['\r'],!,{new_line}, allbut2(C,Id).
allbut2(C,['\n'|Id]) --> ['\n'],!,{new_line}, allbut2(C,Id).
allbut2(C,['\\',X|Id]) --> ['\\',X],!, allbut2(C,Id).
allbut2(C,[X|Id]) --> [X], {\+(X = C)},allbut2(C,Id).
allbut2(_,[]) --> [].

%% Numbers (integer and float)
int(Z) --> [X],int1(Y),{number(X),append([X],Y,Z)}.
int1(Z) --> [X],int1(Y),{number(X),append([X],Y,Z)},!.
int1([]) --> [].
num(X,[n,u,m,'('|Y]) --> int(A), num2(B), {append(A,B,X), append(X,[')'],Y)}.
num2(['.'|X]) --> ['.'], int(X).
num2([]) --> [].

%% A variable begins with capital letter, and then whatever
variable([X|Y], [v,a,r,'(','\'',X|Z0]) --> [X],var1(Y),{(letter_may(X);member(X,['_'])),append(Y,['\'',')'],Z0)}.
var1(Z) --> [X],var1(Y),{(letter(X);number(X);member(X,['-','_'])),append([X],Y,Z)}.
var1([]) --> [].

%% Letter definition
letter(X):-letter_min(X);letter_may(X).
letter_min(X):-name(X,[N]),97=<N,N=<122.
letter_may(X):-name(X,[N]),65=<N,N=<90.

%% An identifier begins with a lower-case letter.
identifier(Z) --> [X],var1(Y),blanks,{letter_min(X),append([X],Y,Z)}.
identifier(['\''|Z]) --> ['\''],!,allbut('\'',A),wait('\'','\''),blanks,{append(A,['\''],Z)}.

%% rule
rule(H,L) --> head(Hh,Hl,Hv), rule2(I,Bh,Bl,Bv,Bp), td(T), blanks, wait('.', '.'),blanks,
		{constr_rule(Hh,Hl,Hv,I,Bh,Bl,Bv,Bp,T,H,L)}.
rule2(I,Bh,Bl,Bv,Bp) --> ['<'],!, idImplication(I), body(Bh,Bl,Bv,Bp),blanks.
rule2([],[],[],[],[]) --> blanks.

constr_rule(Hh,Hl,Hv,_,[],[],[],[],[],Ch,Cl) :- !, new_rule(N),
	lat:top(T), term2char(T,Hv),append(Hh,[')','.','\n'],Ch), append(Hv,[')',')','.','\n'],A0),
	append(Hl,[')',',',i,m,p,l,'(',e,m,p,t,y,')',',',b,o,d,y,'(',e,m,p,t,y,')',',',t,d,'('|A0],A1),
	append(N,[',',h,e,a,d,'('|A1],A2),Cl=[r,u,l,e,'('|A2].
constr_rule(Hh,Hl,Hv,_,Bh,[],[],_,[],Ch,Cl) :- !, new_rule(N),
	lat:top(T), term2char(T,Hv),append(Bh,['.','\n'],Z0),append(Hh,[')',':','-'|Z0],Ch),append(Hv,[')',')','.','\n'],A0),
	append(Hl,[')',',',i,m,p,l,'(',e,m,p,t,y,')',',',b,o,d,y,'(',e,m,p,t,y,')',',',t,d,'('|A0],A1),
	append(N,[',',h,e,a,d,'('|A1],A2),Cl=[r,u,l,e,'('|A2].	

constr_rule(Hh,Hl,Hv,_,[],[],[],[],Hv,Ch,Cl) :- !, new_rule(N),
	append(Hh,[')','.','\n'],Ch), append(Hv,[')',')','.','\n'],A0),
	append(Hl,[')',',',i,m,p,l,'(',e,m,p,t,y,')',',',b,o,d,y,'(',e,m,p,t,y,')',',',t,d,'('|A0],A1),
	append(N,[',',h,e,a,d,'('|A1],A2),Cl=[r,u,l,e,'('|A2].
constr_rule(Hh,Hl,Hv,_,Bh,[],[],_,Hv,Ch,Cl) :- !, new_rule(N),
	append(Bh,['.','\n'],Z0),append(Hh,[')',':','-'|Z0],Ch),append(Hv,[')',')','.','\n'],A0),
	append(Hl,[')',',',i,m,p,l,'(',e,m,p,t,y,')',',',b,o,d,y,'(',e,m,p,t,y,')',',',t,d,'('|A0],A1),
	append(N,[',',h,e,a,d,'('|A1],A2),Cl=[r,u,l,e,'('|A2].	

constr_rule(Hh,Hl,Hv,I,Bh,Bl,Bv,Bp,[],Ch,Cl) :- !, new_rule(N),
	lat:top(T), term2char(T,Tt), (Bp=[],A0=['.','\n'];\+(Bp=[]),append([','|Bp],['.','\n'],A0)),
	Hv=['T','V',0,')'],Bv=Hv, append(Bh,A0,A1), append(Hh,[':','-'|A1],Ch),
	append(Tt,[')',')','.','\n'],Z0),append(Bl,[')',',',t,d,'('|Z0],Z1),append(I,[')',',',b,o,d,y,'('|Z1],Z2),
	append(Hl,[')',',',i,m,p,l,'('|Z2],Z3),append(N,[',',h,e,a,d,'('|Z3],Z4),Cl=[r,u,l,e,'('|Z4].
constr_rule(Hh,Hl,Hv,I,Bh,Bl,Bv,Bp,T,Ch,Cl) :- !, new_rule(N),
	(Bp=[],A0=['.','\n'];\+(Bp=[]),append([','|Bp],['.','\n'],A0)),
	Hv=['T','V',0,')'],new_var(Bv), append(Bv,[',','T','V',0,')'|A0],A1),
	append(T,[','|A1],A2),append(I,['('|A2],A3),append(Bh,[')',',',l,a,t,':',a,n,d,'_'|A3],A4), append(Hh,[':','-'|A4],Ch),
	append(T,[')',')','.','\n'],Z0),append(Bl,[')',',',t,d,'('|Z0],Z1),append(I,[')',',',b,o,d,y,'('|Z1],Z2),
	append(Hl,[')',',',i,m,p,l,'('|Z2],Z3),append(N,[',',h,e,a,d,'('|Z3],Z4),Cl=[r,u,l,e,'('|Z4].

%% head
head(H,L,V) --> {reset_var}, idCompoundA(H,L,V),blanks,!.

%% idImplication
idImplication(I) --> identifier(I), blanks, !.
idImplication(I) --> wait('-','implication label'), blanks, {arbitrary_implication(I)}.
arbitrary_implication(I) :- arbitrary_connective([a,n,d,'_'],I).

%% td
td(H) --> [w,i,t,h],!, blank, td2(H),
	{to_string(H,C,_),append(C,".",C1),read_from_chars(C1,E),try(lat:member(E),error('member of lattice'))}.
td([]) --> [].
td2(H) --> idCompoundT(H,_), !.
td2(H) --> num(H,_), !.
%% td2(H) --> string(H,_).
td2(H) --> list(H,_), !.

%% idCompound
idCompoundT(A,B) --> identifier(I),!, idCompound2(H,L,N), {N=0,A=I,append(I,[')'],B0),B=[c,o,n,'('|B0]
			; N>0, append(H,[')'],A0), append(I,['('|A0],A),
			append(L,[')'],Al0), term2char(N,NN), append(NN,[')',','|Al0],Al1),append(I,[','|Al1],Al2),
			B=[t,e,r,m,'(',f,u,n,'('|Al2]}.
%% NUEVO
idCompoundA([],[t,d,'('|H2],H) --> td2(H), {to_string(H,C,_),append(C,".",C1),read_from_chars(C1,E),try(lat:member(E),fail),
			append(H,[')'],H2)}.
idCompoundA(A,B,V) --> identifier(I),!, idCompound2(H,L,N),
			{(N=0, append(I,['('|V],A), append(I,[',',0,')',',','[',']',')'],Al2)
			; N>0, append(H,[','|V],A1), append(I,['('|A1],A),
			append(L,[')'],Al0), term2char(N,NN), append(NN,[')',','|Al0],Al1),append(I,[','|Al1],Al2)),
			B=[a,t,o,m,'(',p,r,e,d,'('|Al2]}.
idCompound2(H,['['|L],M) --> ['('],!, blanks, wait_term(Th,Tl), blanks, idCompound3(Ch,Cl,N), blanks, wait(')',')'),blanks,
			{M is N+1, append(Th,Ch,H), append(Cl,[']'],Cl0), append(Tl,Cl0,L)}.
idCompound2([],['[',']'],0) --> [].
idCompound3([','|H],[','|L],M) --> [','],!, blanks, term(Th,Tl), blanks, idCompound3(Ch,Cl,N), {M is N+1,
			append(Th,Ch,H),append(Tl,Cl,L)}.
idCompound3([],[],0) --> [].

%% term
term(Th,Tl) --> idCompoundT(Th,Tl),blanks.
term(Th,Tl) --> num(Th,Tl),blanks.
%% term(Th,Tl) --> string(Th,Tl),blanks.
term(Th,Tl) --> variable(Th,Tl),blanks.
term(Th,Tl) --> list(Th,Tl),blanks.

wait_term(H,L) --> term(H,L).
wait_term([],[]) --> blanks, {error('term')}.

%% list
list(['['|H],L) --> ['['],!, blanks, list2(H2,L), wait(']',']'), blanks,{append(H2,[']'],H)}.
list2(H,[t,e,r,m,'(',f,u,n,'(','\'','.','\'',',',2,')',',','['|L]) --> term(Fh,Fl), list3(Sh,Sl),
	{append(Fh,Sh,H), append(Sl,[']',')'],A),append(Fl,[','|A],L)}.
list2([],[c,o,n,'(','[',']',')']) --> blanks.
list3([','|H],[t,e,r,m,'(',f,u,n,'(','\'','.','\'',',',2,')',',','['|L]) --> [','],!, blanks, wait_term(Fh,Fl),list3(Sh,Sl),
	{append(Fh,Sh,H), append(Sl,[']',')'],A),append(Fl,[','|A],L)}.
list3(['|'|H],L) --> ['|'],!, blanks, term(H,L),blanks.
list3([],[c,o,n,'(','[',']',')']) --> blanks.

%% Prolog code
pcode(H) --> ['{'],!, allbut('}',H1), wait('}','}'), blanks, pcode(H2), {(H2=[],!,H=H1;append(H1,[','|H2],H))}.
pcode([]) --> blanks.

%% body
body(H,L,V,P) --> pcode(P1), body_x(H1,L,V,P), {appendc(P1,H1,H)}.
body_x(H1,L,V,P) --> body1(H1,L,V,P).
body_x([],[],[],[]) --> [].

body0(H,L,V,P) --> pcode(P1), body1(H1,L,V,P), {(P1=[],H=H1,!; H1=[], H=P1,!; append(P1,[','|H1],H))}.
wait_body0(H,L,V,P) --> body0(H,L,V,P).
wait_body0([],[],[],[]) --> [], {error('formula')}.

body1(H,L,V,P3) --> body2(H1,L1,V1,P0), blanks, pcode(Ps), body3(H2,L2,V2,T,C), blanks, pcode(P2),
	{appendc(P0,Ps,P1), constr_body(H1,L1,V1,P1,H2,L2,V2,T,C,P2,H,L,V,P3)}.

constr_body(H,L,V,P1,[],[],[],[],[],P2,H,L,V,P3):-appendc(P1,P2,P3).
constr_body(H1,L1,V1,P1,H2,L2,V2,T,C,P2,H,L,V,[]):-
	new_var(V1),append(V2,[','|V],A2),append(V1,[','|A2],A3),append(C,['('|A3],A4),append(T,A4,A5),
	appendc(P2,[l,a,t,':'|A5],A6),appendc(H2,A6,A7),appendc(P1,A7,A8),append(H1,[')',','|A8],H),
	append(L2,[']',')'],B0),append(L1,[','|B0],B1),append(C,[',',2,',','['|B1],B2),
	append(Ts,['_'],T),append(Ts,['('|B2],L).
%% NUEVO
constr_body(H1,L1,V1,P1,H2,L2,V2,T,C,P2,H,L,V,[]):-
	append(V2,[','|V],A2),append(V1,[','|A2],A3),append(C,['('|A3],A4),append(T,A4,A5),
	appendc(P2,[l,a,t,':'|A5],A6),appendc(H2,A6,A7),appendc(P1,A7,H),
	append(L2,[']',')'],B0),append(L1,[','|B0],B1),append(C,[',',2,',','['|B1],B2),
	append(Ts,['_'],T),append(Ts,['('|B2],L).

%% MODIFICADO (NUEVO)
body2(H,L,V,[]) --> connective(T,C), wait('(','('), blanks, body0(Bh,Bl,Bv,Bp), blanks, body4(B4h,B4l,B4v,N), blanks, wait(')',')'),
	{(new_var(Bv2),append(Bv2,[')'],Bv);Bv2=Bv),appendc(Bh,Bp,B), append(B4v,[','|V],A1), append(Bv2,A1,A2),append(C,['('|A2],A3),
	append(T,A3,A4), appendc(B,B4h,Waw), appendc(Waw,[l,a,t,':'|A4],H), M is N+1, append(B4l,[']',')'],Al0),
	append(Bl,Al0,Al1),term2char(M,Mc),append(Mc,[',','['|Al1],Al2),append(C,[','|Al2],Al3),
	append(Ts,['_'],T),append(Ts,['('|Al3],L)}.
body2(H,L,V,P) --> ['('], blanks, body0(H,L,V,P), blanks, wait(')',')').
body2(H,L,V,[]) --> atom(H,L,V).

%% MODIFICADO (NUEVO)
body3(H,L,V,T,C) --> connective(T,C), wait_body0(H1,L,V1,P), {(new_var(V),append(V,[')'],V1);V=V1),appendc(H1,P,H)}.
body3([],[],[],[],[]) --> [].

%% BORRAR (NUEVO)
% body4(H,[','|L],[','|V],M) --> [','], blanks, wait_body0(H1,L1,V1,P1), blanks, body4(Hs,Ls,Vn,N),
%	{M is N+1, new_var(V1), appendc(H1,P1,H2), append(V1,Vn,V), append(Hs,[')'],Hs2),append(H2,Hs2,H), append(L1,Ls,L)}.

%% MODIFICADO (NUEVO)
body4(H,[','|L],[','|V],M) --> [','], blanks, wait_body0(H1,L1,V1,P1), blanks, body4(Hs,Ls,Vn,N),
	{M is N+1, appendc(H1,P1,H2), (new_var(V1),!,append(H2,[')'],H3);H3=H2), append(V1,Vn,V),appendc(H3,Hs,H), append(L1,Ls,L)}.
body4([],[],[],0) --> [].

%% atom
%% atom(H,L,V) --> term(Th,Tl), atom2(Sh,Tl,L,V), {append(Th,Sh,H)}.
%% atom2(H,L0,L,V) --> ['='], 
atom(H,L,V) --> idCompoundA(H,L,V), {!, \+(H=[w,i,t,h,'('|_])}. %% Se impide confusión con 'with'.

%% connective
connective(T,C) --> conType(T),!, idConnective(T,C), blanks.
conType([a,n,d,'_']) --> ['&'].
conType([a,g,r,'_']) --> ['@'].
conType([o,r,'_']) --> ['|'].

%% idConnective
idConnective(_,C) --> identifier(C).
idConnective(T,C) --> [], {arbitrary_connective(T,C)}.
arbitrary_connective(T,C) :- current_predicate(lat:P/_), name(P,Pn),to_char_list(Pn,Pr),append(T,C,Pr).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% EXECUTION TREE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% step(estado inicial, estado final, info)
step(_,state(Q,S),state(Q2,S2),Info)  :- select_atom(Q,A,Q_,Q_v),!,step_AS(state(Q,S),A,Q_,Q_v,state(Q2,S2),Info).
step(l,state(td(_),_),_,_):- !,fail.
step(l,state(Q,S),state(Q2,S2),result):- is_derivation(state(Q,S),state(Q2,S2)),!.
step(m,state(Q,S),state(Q2,S2),Info)  :- select_expression(Q,A,Q_,Q_v),step_IS(state(Q,S),A,Q_,Q_v,state(Q2,S2),Info),!.
step(s,state(Q,S),state(Q2,S2),Info)  :- select_expression(Q,A,Q_,Q_v),step_SIS(state(Q,S),A,Q_,Q_v,state(Q2,S2),Info),!.

%% step_?(Estado inicial S, átomo A seleccionado de S, S con una variable V en lugar de A, V, Estado final F, información)
step_AS(state(_,S),atom(pred(P,A),V1),Q_,Q_v,state(Q2,SZ),R):- 
	rule(Nr,head(atom(pred(P,A),V2)),impl(I),body(B),td(Nu)), retract(varcont(Vc)),Vc1 is Vc+1,assert(varcont(Vc1)),
	rename(V2,V2_),rename(B,B_), mgu_l(V1,V2_,[],Z),(B=empty,Q_v=td(Nu);\+(B=empty),Q_v=and(I,2,[td(Nu),B_])),
	subs(Q_,Z,Q2), subs(S,Z,S0),append(Z,S0,SZ), name(Nr,NrN), append("R",NrN,Rn), name(R,Rn).
step_AS(_,atom(pred(P,A),V1),_,_,_,_):- rule(_,head(atom(pred(P,A),V2)),_,_,_),
	retract(varcont(Vc)),Vc1 is Vc+1,assert(varcont(Vc1)),rename(V2,V2_),mgu_l(V1,V2_,[],_),!,fail.
step_AS(state(_,S),_,Q_,Q_v,state(Q2,SZ),'R0'):- lat:bot(B), Q_v=td(B), subs(Q_,Z,Q2), subs(S,Z,SZ).

step_IS(state(_,S),E,Q_,td(Q_v),state(Q_,S),is) :- E=..[T,L,_,V], applow(T,L,Fn),
	str2td(V,V2),append(V2,[Q_v],V3),A=..[Fn|V3],lat:A.

%% is_derivation(Estado inicial S, Estado final)
is_derivation(state(Q,S),F):- select_expression(Q,A,Q_,Q_v),!,
	step_IS(state(Q,S),A,Q_,Q_v,State2,_),is_derivation(State2,F).
is_derivation(F,F).

step_SIS(state(_,S),E,Q_,Q_v,state(Q_,S),Info) :- E=..[T,L,_,V], applow(T,L,Fn),str2td(V,V2), append(V2,[X],V3),A=..[Fn|V3],
	try(clause(lat:A,Body),(nl,write('ERROR: '),write(A),write(' is not a dynamic predicate.'),nl,!,fail) ),
	( validForm(Body),assert(tsnum(nv(0))), assert(ts([])),tsInsert(V2),tsExtract(Body,X,Q_v),
	  retractall(ts(_)),retractall(tsnum(_)), (Q_v=td(_),!,Info=sis2; Info=sis1)
	; append(V2,[Rt],Po), Y=..[Fn|Po],lat:Y, Q_v=td(Rt), Info=sis2).

%% validForm(Prolog Body): 'true' if the parameter is vaid for sis1
validForm((A,B)):- !,A=..[P|_], name(P,Pn), to_string(Ps,Pn,_), validForm2(Ps), validForm(B).
validForm(A):- A=..[P|_], name(P,Pn), to_string(Ps,Pn,_), validForm2(Ps).
validForm2(X):-append([a,n,d,'_'],_,X).
validForm2(X):-append([a,g,r,'_'],_,X).
validForm2(X):-append([p,r,i,'_'],_,X).
validForm2(X):-append([o,r,'_'],_,X).

%% tsInsert(list) : insert the list in the table of symbols ts
tsInsert([]).
tsInsert([A|C]):- retract(ts(X)), assert(ts([var(A,td(A))|X])), tsInsert(C).	%% Parameters

%% tsExtract(Body,Variable,Result): extracts in R the Bariable from the Body and the table of symbols.
tsExtract((A,B),U,R):- !, tsExtract2(A), tsExtract(B,U,R).
tsExtract(A,U,R):- tsExtract2(A), ts_search(U,R).
tsExtract2(A):- !, A=..[P|L], rev(L,[U|Param]),retract(tsnum(U)), U=nv(NUM), NUM1 is NUM+1, assert(tsnum(nv(NUM1))),
	rev(Param,L2), length(Param,Num), applow(C,N,P), ts_searchmap(L2,TdParam), retract(ts(Ts)),
	Term=..[C,N,Num,TdParam], assert(ts([var(U,Term)|Ts])).

%% applow(A,B,A_B)
applow(C,X,Z):-var(Z),!,name(C,Cc), to_string(Cl,Cc,_), name(X,Xc), to_string(Xl,Xc,_), append(Cl,['_'|Xl],F), to_string(F,_,Z).
applow(C,X,Z):-name(Z,Zn),to_string(Zs,Zn,_), append(Cs,['_'|Xs],Zs), to_string(Cs,Cn,_),name(C,Cn), to_string(Xs,Xn,_),name(X,Xn).

ts_searchmap([A|B],[As|Bs]):- ts_search(A,As), ts_searchmap(B,Bs).
ts_searchmap([],[]).
ts_search(A,B):- ts(Ts), ts_search2(A,B,Ts).
ts_search2(A,B,[var(A,B)|_]):- !.
ts_search2(A,B,[_|L]):-ts_search2(A,B,L).
ts_search2(A,td(A),[]):- lat:member(A),!.
ts_search2(A,td(X),[]):- lat:bot(X), nl, write(A), write(' is not a member of the loaded lattice'),nl.

%% str2td: [td(0.3),td(1)] --> [0.3,1]
str2td([],[]).
str2td([td(X)|Y],[X|Y0]):-str2td(Y,Y0).

%% select_atom(objetivo S,átomo A de S,S con una variable S_v en lugar de A,S_v)
select_atom(atom(P,V),atom(P,V),W,W).
select_atom(and(C,A,L),X,and(C,A,L_),V):- select_atom_2(L,X,L_,V).
select_atom(agr(C,A,L),X,agr(C,A,L_),V):- select_atom_2(L,X,L_,V).
select_atom(or(C,A,L) ,X,or(C,A,L_) ,V):- select_atom_2(L,X,L_,V).
select_atom(pri(C,A,L),X,pri(C,A,L_),V):- select_atom_2(L,X,L_,V).
select_atom_2([A|B],X,[A_|B],A_v):-select_atom(A,X,A_,A_v),!.
select_atom_2([A|B],X,[A|B_],A_v):-select_atom_2(B,X,B_,A_v).

%% select_expression(objetivo S,expresión E de S,S con una variable S_v en lugar de E,S_v)
select_expression(and(C,A,L),and(C,A,L),V, V):- all_td(L),!.
select_expression(and(C,A,L),X,and(C,A,L_),V):- select_expression_2(L,X,L_,V).
select_expression(agr(C,A,L),agr(C,A,L),V, V):- all_td(L),!.
select_expression(agr(C,A,L),X,agr(C,A,L_),V):- select_expression_2(L,X,L_,V).
select_expression(or(C,A,L), or(C,A,L), V, V):- all_td(L),!.
select_expression(or(C,A,L), X,or(C,A,L_), V):- select_expression_2(L,X,L_,V).
select_expression(pri(C,A,L),pri(C,A,L),V, V):- all_td(L),!.
select_expression(pri(C,A,L),X,pri(C,A,L_),V):- select_expression_2(L,X,L_,V).
select_expression_2([A|B],X,[A_|B],A_v):-select_expression(A,X,A_,A_v),!.
select_expression_2([A|B],X,[A|B_],A_v):-select_expression_2(B,X,B_,A_v).

%% all_td(list of expressions): true if all parameters are truth degrees
all_td([]).
all_td([td(_)|S]):-all_td(S).

%% mgu(Expression 1, Expression 2, substitution)
mgu(atom(pred(P,A),L),atom(pred(P,A),L_),S):- mgu_l(L,L_,[],S).

mgu_l(L,L,X,X).
mgu_l(L, S, Z, R):-
	d_pair_l(L,S,pair(var(X),Y)), subs(Z,[pair(X,Y)],Z_), subs(L,[pair(X,Y)],L_), subs(S,[pair(X,Y)],S_),
	mgu_l(L_,S_,[pair(X,Y)|Z_],R),!.
mgu_l([],[],X,X).

d_pair(X,X,[]):- !.
d_pair(var(V),X,pair(var(V),X)):- !.
d_pair(X,var(V),pair(var(V),X)):- !.
d_pair(term(fun(F,A),L),term(fun(F,A),S),P) :- d_pair_l(L,S,P),!.
d_pair_l([],[],[]):- !.
d_pair_l([A|As],[B|Bs],S):- d_pair(A,B,S1), (S1=[],!,d_pair_l(As,Bs,S);S=S1).

%% subs(Initial, Substitution, Final)
subs(X,[],X):- !.
subs([],_,[]):- !.
subs([pair(V,Vs)|L],S,[pair(V,Vs_)|L_]) :- subs(Vs,S,Vs_), subs(L,S,L_),!.
subs([A|As],S,[B|Bs]):-subs(A,S,B),subs(As,S,Bs),!.
subs(atom(P,L),S,atom(P,L_)):- subs(L,S,L_),!.
subs(and(A,N,L),S,and(A,N,L_)):- subs(L,S,L_),!.
subs(agr(A,N,L),S,agr(A,N,L_)):- subs(L,S,L_),!.
subs(or(A,N,L), S,or(A,N,L_)) :- subs(L,S,L_),!.
subs(pri(A,N,L),S,pri(A,N,L_)):- subs(L,S,L_),!.
subs(empty, _, empty):- !.
subs(con(C), _, con(C)):- !.
subs(num(C), _, num(C)):- !.
subs(td(C), _, td(C)):- !.
subs(term(F,L),S,term(F,L_)):- subs(L,S,L_),!.
subs(var(V), [pair(V,E)|_], E):- !.
subs(var(V), [_|S], E):- !, subs(var(V),S,E),!.

%% rename(parameters, renamed parameters)
rename([],[]).
rename([A|As],[B|Bs]):- rename(A,B), rename(As,Bs).
rename(var(A),var(B)):- !,name(A,N),varcont(I),name(I,Ni),append(N,Ni,R),name(B,R).
rename(empty,empty).
rename(con(A),con(A)).
rename(num(A),num(A)).
rename(td(A),td(A)).
rename(atom(P,L),atom(P,L2)):- rename(L,L2).
rename(term(F,L),term(F,L2)):- rename(L,L2).
rename(and(A,B,L),and(A,B,L2)):- rename(L,L2).
rename(or(A,B,L), or(A,B,L2)) :- rename(L,L2).
rename(agr(A,B,L),agr(A,B,L2)):- rename(L,L2).
rename(pri(A,B,L),pri(A,B,L2)):- rename(L,L2).

%% print_state(state(Q,S))
print_state(state(Q,S)):- write(' < '), prints(Q), write(', {'), prints_subs(S), write('} >'), !.
prints(and(Label,A,List)):- write('&'),write(Label),prints2(A,List).
prints(or(Label,A,List)) :- write('|'),write(Label),prints2(A,List).
prints(agr(Label,A,List)):- write('@'),write(Label),prints2(A,List).
prints(pri(Label,A,List)):- write('#'),write(Label),prints2(A,List).
prints(atom(pred(P,A),List)):- write(P), prints2(A,List).
prints(con(C)):- write(C).
prints(var(C)):- write(C).
prints(num(C)):- write(C).
prints(td(C)):- write(C).
prints(term(fun('.',2),[H,B])):- write('['),prints(H), prints_list(B), write(']').
prints(term(fun(F,A),List)):- \+(F='.'), write(F), prints2(A,List).
prints([]).
prints(pair(A,B)):- write(A),write('/'),prints(B).

prints_subs([]).
prints_subs([A|B]):-prints(A),prints3(B).

prints2(0,_):- !.
prints2(_,[A|B]):-write('('),prints(A),prints3(B),write(')').

prints3([]).
prints3([A|B]):- write(','),prints(A),prints3(B).

prints_list(term(fun('.',2),[H,B])):- write(','), prints(H), prints_list(B).
prints_list(con([])).
prints_list(X):- write('|'),prints(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% AUXILIARY PREDICATES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% try(dangerous block, exception): obtain a floper value with no errors
try(X,F):-(catch(X,_,F),!;F).

%% nth element
nth_(1,[E|L],E,L).
nth_(N,[E|L],X,[E|R]) :- N>0, M is N-1, nth_(M,L,X,R).

%% wipe_module(M): erase a module M
wipe_module(M) :- 
        (   current_predicate(M:P/A), 
            (\+(current_predicate(license:P/A)) %Evitamos que coja '=', '<', etc..., que aparecen como predicados de 'license'
            ; fail
            ),
            abolish(M:P,A), 
            fail 
        ;   true 
        ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% SETUP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% reverse a list.
rev(L1,L2):- rev(L1,L2,[]).
rev([],L,L).
rev([H|T],L,S):- rev(T,L,[H|S]).

changedir(D):- getdir(D,Dir),catch(chdir(Dir),_,write('SICStus')).
getdir(D,Dir):- name(D,L),rev(L,R),eraseLastPart(R,Rdir),rev(Rdir,Ldir),name(Dir,Ldir).
eraseLastPart([47|L],[47|L]):- !.
eraseLastPart([_|L],R):- eraseLastPart(L,R).

floper_default:- retractall(floper_depth(_)), retractall(floper_goal(_)), retractall(floper_ismode(_)),
	retractall(loaded_file_fpl(_)),retractall(loaded_file_pl(_)),retractall(loaded_file_lat(_)),
	assert(floper_depth(12)), assert(floper_goal('p(X)')), assert(floper_ismode('m')).

?-prolog_load_context(source,Name),write('Name: '),write(Name),nl,nl,changedir(Name), floper_default,
  use_module(library(lists)), %% This package defines operations on lists.
  use_module(library(system)), %% This package contains utilities for invoking services from the operating system.
  use_module(library(charsio)), %% This package defines I/O predicates that read from, or write to, a code-list.
  lat:consult('num.lat'), 	%% Default Lattice
  assert(loaded_file_lat('num.lat')),
  title,menu,shell_synth.