%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% iG.pl  Interactive Geolog
%%    http://www.csupomona.edu/~jrfisher/www/geolog
%%    jrfisher@csupomona.edu
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- op(1150,xfx,'=>'), 
   op(1200,xfx,axiom), % M. Bezem's annotations
   op(700,xfx,'==='),  % mathematical equality
   op(600,xfx,'#').    % another infix math op
:- dynamic theory/1, focus/1, count/1, fact/2, link/2,
   split/4, connectedReadStream/1, connectedWriteStream/1, 
   history/1.


%% shortcuts
s:-show.  i:-info. c(F):-compile(F).

info:- nl,
   writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 06/17/2007 '), 
   write('%%  interactive Geolog    '), 
   (theory(T) -> write('G:'), writeln(T) | nl),
   writeln('%%   ?- compile(+G).  % Compile Geolog rules in file G.gl(.in) '),
   writeln('%%   ?- show.         % Show ordered rules ...                 '), 
   writeln('%%   ?- iG.           % Start interactive Geolog proof browser ...           '), 
   writeln('%%   ?- info.         % Display this info                      '), 
   writeln('%%   ?- more.         % More info about ?-compile(+G). ?-iG.    '), 
   writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'),
   nl.
:- info. 

more :- 
   writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% '), 
   writeln('%%  For example, if the Prolog working directory contains a file'), 
   writeln('%%  ./in/dpe.in then compile it using ?-compile(''in/dpe'').'), 
   writeln('%%  If the goal ?-iG. reports errors or hangs, close the Java'), 
   writeln('%%  window and try again.  Once the Java GUI is ready click'), 
   writeln('%%  on the "iG?" button for more information about interactions.'), 
   writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% '), 
   nl.


%%%%% COMPILE/SHOW 
compile(Theory) :- 
   in2gl(Theory), %% convert .in file to .gl, if it exists
   %% load and translate a geolog (.gl) file
   retractall(theory(_)), abolish('Geolog_rule'/2), 
   name(Theory,NameList), append(NameList,[46,103,108],A), name(F,A), %%.gl
   %% load user's theory
   init_count, see(F), repeat, read(Geolog), process(Geolog), !, seen,  
   getCount(Count), assertz('Geolog_rule'(Count, '^')),  %% bottom
   assert(theory(Theory)), % new theory
   %% compile
   compile_predicates(['Geolog_rule'/2]), write('%% '), write(F), writeln(' compiled.') .

process(end_of_file) :- !.
process(Geolog) :-  
   transcribe(Geolog,G), % fails if ill formed ...
   writeq(G), write('.'), write(' %'), getCount(Count), writeln(Count), 
   assertz('Geolog_rule'(Count,G)), fail.
 
init_count :- retractall(count(_)), assert(count(1)).
getCount(C) :- retract(count(C)), C1 is C+1, assert(count(C1)).
downCount :- count(0) | (retract(count(C)), C1 is C-1, assert(count(C1)) ).

%% Separate free variables in consequent and add existential quantifiers (X^...).
transcribe((A=>C),(A=>C1)) :- 
   term_variables(A,Universals), 
   alter(C,Universals,C1).

alter((C;D),U,(C2;D1)) :- !,
   copy_term_nat(U^C,U^C1), 
   term_variables(C1,V),
   exclude(V,U,V1),
   prefix(V1,C1,C2),
   alter(D,U,D1).
alter(C,U,C2) :- 
   copy_term_nat(U^C,U^C1), 
   term_variables(C1,V),
   exclude(V,U,V1),
   prefix(V1,C1,C2).

prefix([],E,E).
prefix([V|Vs],E,(V^Es)) :- prefix(Vs,E,Es).

%% exclude variables.
exclude([X|R],Xclude,R1) :- 
   coincident(X,Xclude), !,
   exclude(R,Xclude,R1).
exclude([X|R],Xclude,[X|R1]) :- 
   exclude(R,Xclude,R1).
exclude([],_,[]). 

coincident(X,[Y|_]) :- X == Y.
coincident(X,[_|R]) :- coincident(X,R).

show :- theory(_), !,
        findall([N,R],'Geolog_rule'(N,R),NRs),  
        cascade(NRs).
show :- 
   writeln('There is no compiled theory.').

cascade([[N,R]|More]) :- 
   write(N), write(' '), 
   writeln(R),
   cascade(More).
cascade([]).

%%%%% CONVERT F.in to F.gl %%%%%%%%%%%%%%%%%%%%%%%%
%% if File.in exists, convert it
in2gl(File) :- 
   name(File,NameList), append(NameList,[46,105,110],INL), 
   name(IN,INL), exists_file(IN),
   !, append(NameList,[46,103,108],GLL), name(GL,GLL),
   see(IN), tell(GL), 
   repeat, read(Bez), convert(Bez,Comment,Geolog), record(Comment,Geolog), !, seen, told,
   write('%% '), write(IN), write(' converted to '),writeln(GL).
in2gl(_).  %% .in file not present

convert(end_of_file,end_of_file,end_of_file).
convert(dom(X),'domain declaration', (true => dom(X))).
convert(P axiom Q : R,(P axiom Q),R).  %% annotation becomes comment 

record(end_of_file,end_of_file) :- told.
record(Anno,Geolog) :- 
   write('%% '), write(Anno),nl,
   writeq(Geolog), writeln('.'), fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ig:-iG.
iG :- 
   theory(T), !,
   name(T,NameList), append(NameList,[46,105,103],A), name(IG,A), %.ig 
   tell(IG), show, told, % write one rule per line
   % start iG
   name('java -cp GeologTree.jar iG ',PreList), 
   %name('java -cp ./ iG ',PreList), 
   append(PreList,A,L1), append(L1,[32,38,32],CommandList),
   name(JAVA,CommandList), 
   writeln(' CLOSE the Java iG window when finished ... '), 
   writeln(' If connection fails, close Java window '), 
   writeln(' and try ?-iG. again ...'), 
   nl,nl,nl,    
   initialize,  
   shell(JAVA),   % onward ...
   wait,          % let Connector start
   %wait(400000),  % stall 
   connect(54321),  
   wait(400000),  % stall before main starts 
   main, !.
iG:- 
   writeln('User needs to first compile a Geolog theory.'),
   writeln('Then start the iG proof browser.').

iG(Theory) :- 
   compile(Theory),
   iG.

%% wait for connector to be ready
wait :- 
   repeat, 
   exists_file('ready').

initialize :- 
   (exists_file('ready') -> delete_file('ready') ; true),
   retractall(focus(_)),
   retractall(fact(_,_)),
   retractall(link(_,_)),
   retractall(history(_)),
   retractall(split(_,_,_,_)),
   assert(history([])), 
   retractall(connectedReadStream(_)),
   retractall(connectedWriteStream(_)),
   assert(focus(0)), 
   assert(fact(0,true)), 
   init_count.

connect(Port) :- 
   tcp_socket(Socket), 
   gethostname(Host),  % local host
   tcp_connect(Socket,Host:Port),
   tcp_open_socket(Socket,INs,OUTs), 
   assert(connectedReadStream(INs)), 
   assert(connectedWriteStream(OUTs)).


wait(0).
wait(N) :- 
   N > 0, 
   N1 is N-1, 
   wait(N1).

/*  %% creates more problems
connect :- 
   repeat, 
   catch(connect(54321),_, (writeln('.'),fail)).

*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"

%% oldest tree ancestor computed first
ancestor(I,J) :- link(P,J),  ancestor(I,P) | link(I,J).

%% match antecedent or consequent against facts
match((F;R),I) :- match(F,I) | match(R,I).
match((_^L),I) :- match(L,I).
match((L,M),I) :- !, match(L,I), match(M,I).
match(L,I) :- ancestor(A,I), fact(A,L).
match(L,I) :- fact(I,L).

applicable((A=>C),I) :- match(A,I), \+match(C,I).
applicable('^',_).  % never actually applied!

% focus on leaf
main :- 
   focus(0),
   count(C), C > 1, % done actually
   inform(rule,0,'PROOF'),   %%%%%%%????????
   \+choice(0), !, ask_done.
main :- 
   focus(I),  
   ( fact(I,goal) | fact(I,false) ), !, 
   inform(disable,'X','X'),  % <=(undo) or =>(ascend) 
   ask_leaf.
% focus at branch point
main :- 
   focus(I), 
   split(I,N,_,R), !,  % got here using ascend
   suffix(N,S), concat_atom([N,S,' choice ...'],Message),
   inform(disable,'X','X'),  % <=(undo) or =>(descend)
   inform(rule,R,Message),  % <=(undo) or =>(descend)
   ask_split.
% focus on inference node
main :- 
   focus(I), 
   find_rule(I).  % applicable rule

%% find applicable rule(s) at current focus
find_rule(I) :-   
   repeat,
   (I=0 -> inform(disable,'<=','<=') ; true),  
   'Geolog_rule'(N,R), 
   applicable(R,I), 
   ask(N,R).

ask_done :-   %% can only undo ...
   inquire(_), 
   descend, main. 

ask_leaf :- 
   % User will say "undo" or "infer"
   inquire(X), 
   (X=='stop' -> stop ; 
      X=='undo' -> undo, main ; 
        X=='infer' -> ascend, main ; 
          stop).
ask_split :- 
   % User will say "undo" or "infer"
   inquire(X), 
   (X=='stop' -> stop ; 
      X=='undo' -> descend, main ; 
        X=='infer' -> continue, main ; 
          stop).

ask(N,R) :-
   inform(rule,N,R), 
   inquire(X), % user's response  
   (X=='stop' -> stop ;                
      X=='undo' -> undo, main ;     
        X=='block' -> fail ;        
          X=='infer' -> expand(N,R), main ; 
            stop).  

stop :- 
   connectedReadStream(RS), close(RS),
   connectedWriteStream(WS),close(WS).  % 

expand(N,R) :-  
   focus(F), 
   inform(inference,F,(N,R)),  % Need N
   R = (_=>C), 
   (C = (C1;_C2) -> 
       (extend(C1,[],H), updateHistory(H), assert(split(F,2,C,N))) 
          ; 
       (extend(C,[],H), updateHistory(H))  ), 
   focus(F1), inform(focus,F1,F1). 
   
extend(V^B,L,H) :- !, gensym('sk',V), extend(B,L,H). % Skolem eigenvariable
extend((C,D),L,H) :- !, extend(C,L,H1), extend(D,H1,H).
extend(Fact,L,H) :- 
   retract(focus(F)), 
   getCount(C),           inform(count,C,C),
   asserta(link(F,C)),    inform(link,F,C),   %%>>> N.B. asserta
   assert(fact(C,Fact)),  inform(fact,C,Fact),
   H=[C|L],
   assert(focus(C)).

continue :- 
   focus(F), 
   retract(split(F,N,C,R)),
   N1 is N+1, % next disjunct
   assert(split(F,N1,C,R)), 
   nthOR(C,N,Cn),
   extend(Cn,[],H), 
   updateHistory(H), 
   focus(F1), inform(focus,F1,F1).
   
%% nth or (-;-;-;-;-;...)  1-based
nthOR(A,1,C) :- !,
   A = (A1;_) -> C = A1 ; C=A.
nthOR((_;B),N,C) :- 
   N1 is N-1, 
   nthOR(B,N1,C).
   
updateHistory(H) :- 
   retract(history(Past)), 
   assert(history([H|Past])).

undo :- 
   focus(F), 
   count(C), 
   F =:= C-1, !,  % else next clause
   retract(history([Last|Former])), 
   undo(Last), 
   assert(history(Former)), 
   adjust,
   focus(F1), inform(focus,F1,F1).  % split(-,-,-,-)
undo :- descend.  % undo ascend, 

adjust :- 
   focus(F), 
   retract(split(F,N,C,R)), !,
   N1 is N-1, 
   (N1 > 1 ->
      assert(split(F,N1,C,R))   % same inference
         ; 
      inform(remove_inference,F,F)).  % no inference
adjust.

undo([]).
undo([I|R]) :- 
   downCount,
   retract(fact(I,_)),   inform(remove_fact,I,I),
   retract(link(J,I)),   inform(remove_link,J,I),
   retract(focus(_)),
   assert(focus(J)),     inform(focus,J,J),
   undo(R).
   
%% ascend focus until choice succeeds
ascend :- focus(F), choice(F), !, inform(focus,F,F).
ascend :- 
   focus(0), !,      % cannot go higher in tree
   inform(focus,0,0), 
   %%inform(disable,'<=','<='),  
   inform(disable,'X','X'),  
   inform(disable,'=>','=>').
ascend :- 
   retract(focus(F)), 
   link(P,F), 
   assert(focus(P)), 
   ascend.   % keep going

%% Is F a split node with a choice remaining?
%% When fails, means either not split node or no choice remains.
choice(F) :- 
   split(F,K,Choices,_),
   width(Choices,W),  
   K =< W.

%% width of choices (# of disjuncts)
width((_;R),B1) :- !, width(R,B), B1 is B+1.
width(_,1).

%% descend to leaf
descend :- 
   focus(F),
   \+link(F,_), !,
   inform(focus,F,F).
descend :- 
   retract(focus(F)), 
   link(F,C), 
   assert(focus(C)), 
   descend. 

%% inform Connector using triples -#-#-
%% fact#n#f
%% link#i#j
%% inference#i#inf
%% disable#t#t
%% rule#n#r 
%% focus#f#f        SIGNAL TO REPAINT TREE
%% remove_fact#n#-
%% remove_link#i#j
%% remove_inference#i#-

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

inform(inference,B,(C,D)) :-  !, % case of inference 
   connectedWriteStream(WS), 
   write(WS,inference), write(WS,'#'),
   write(WS,B), write(WS,'#'),
   write(WS,'rule '), write(WS,C), write(WS,': '), write(WS,D), 
   nl(WS), flush_output(WS).

inform(A,B,C) :-
   connectedWriteStream(WS), 
   write(WS,A), write(WS,'#'),
   write(WS,B), write(WS,'#'),
   write(WS,C), nl(WS), flush_output(WS).

inquire(I) :-
   connectedReadStream(RS), 
   read(RS,I), 
   write(user,I), nl(user).

suffix(1,'st'):-!.
suffix(2,'nd'):-!.
suffix(3,'rd'):-!.
suffix(_,'th').

/* DEBUG */
%inform(A,B,C) :- write(A),write('#'),write(B),write('#'),writeln(C).  
%% inquire regarding <=(undo), X(block), =>(infer)
%%inquire(X) :- read(X).
look :- listing([focus,count,fact,link,split,history]).