% Copyright (C) 1983, Uppsala University. Authors: Jaan Koort, Mats Carlsson.
% Known bugs:
% The predicate 'enumvars' backtracks to make single-occurrence variables
% look like anonymous, this can be slow and you do not always want it.

:-public lispify/0.

lispify :- 
	tell('lmpc4:'), nl,
	abolish(warned,1),
	predicates_to_translate(List_of_p),
	lispify2(List_of_p),
	told, nl.


:-mode lispify2(+).
lispify2([]).
lispify2([ lispify | Y]) :- lispify2(Y).
lispify2([ lm_compile_declarations | Y]) :- lispify2(Y).
lispify2([ lm_top_level_prove(Pred)|Y]) :-
	first_translation(Pred,pred,Pred1),
	enumvars(Pred1,0,_),
	print_for_lisp(['query-once',[quote,Pred1]]), nl, nl,
	lispify2(Y).
lispify2([ X | Y]) :- lispify_pred(X),lispify2(Y). % the default

:-mode lispify_pred(+).
lispify_pred(Pred) :- %This predicate exhausts its search space.
	current_predicate(Pred,H),
	bagof(clause(H,B),clause(H,B),Clauses),
	lisp_clauses(Clauses,Clauses1,Pred1),
	optionpart(H,Clauses1,OptionsClauses),
	print_for_lisp(['define-predicate',Pred1|OptionsClauses]),
	nl, nl, display('.'), fail;
	true.

:-mode optionpart(+,+,-).
optionpart(First,Clauses,
	[[do(write(':options')),[do(write(':argument-list')),O1]]|Clauses]) :-
	functor(First,Pred,N),
	lm_compile_declarations(Pred,O,N),
	first_translation(O,term,O1),!.
optionpart(_,Clauses,Clauses).

:-mode lisp_clauses(+,-,-).
lisp_clauses([],[],_).
lisp_clauses([clause(H,B)|Rest],[do(nl),[Head1|Body1]|Rest1],Name) :-
	first_translation(H,pred,Head1), Head1=[Name|_],
	conjunction_list(B,Body1),
	enumvars([Head1|Body1],0,_),!,
	lisp_clauses(Rest,Rest1,_).

:-mode enumvars(+,+,-).
enumvars('$PVAR'(T),I,I) :- var(T), T=(-1).
enumvars('$PVAR'(T),_,_) :- T==(-1), !, fail.
enumvars('$PVAR'(I),I,J) :- !, J is I+1.
enumvars([A|B],I,K) :- !, enumvars(A,I,J), enumvars(B,J,K).
enumvars(_,I,I).

:-mode append(+,+,-).
append([],X,X).
append([A|X],Y,[A|Z]) :- append(X,Y,Z).

:-mode name_append(+,+,-).
name_append(Prefix,Name,Prefixed) :-
	name(Name,Namelist), append(Prefix,Namelist,PNamelist),
	name(Prefixed,PNamelist).

:-mode warn_mask(+,-).
warn_mask(Pred,PPred) :-
	name_append("defined-",Pred,PPred),
	(warned(Pred), !; assert(warned(Pred)),
	 ttynl, display('The predicate '),
	 display(Pred),	
	 ttynl, display(' is already defined in LM-Prolog, renamed to '),
	 display(PPred)).


:-mode warn_udf(+,-).
warn_udf(F,Translation) :-
	functor(F,Name,Arity),
	(warned(Name/Arity), !;
	 ttynl, display(Name), display('/'), display(Arity), 
	 display(' is undefined in LM-Prolog'),
	 assert(warned(Name/Arity))),
	name_append("undefined-",Name,Newname),
	F=..[_|Args],
	translation([Newname|Args],term,Translation).

:-mode warn_md(+).
warn_md(F) :-
	warned(F), !;
	ttynl, display(F), display(' is implementation dependent'),
	assert(warned(F)).

lpar :- write('(').
rpar :- write(')').

:-mode print_for_lisp(+).
print_for_lisp(do(G)) :- call(G), !.
print_for_lisp([quote,X]) :- put("'"), print_for_lisp(X), !.
print_for_lisp([]) :- write('()'), !.
print_for_lisp([X|Y]) :-
	lpar, print_for_lisp(X), print_for_lisp_rest(Y), rpar, !.
print_for_lisp('$PVAR'(-1)) :- put("?"), !.
print_for_lisp('$PVAR'(X)) :- put("?"), print_for_lisp(X), !.
print_for_lisp(S) :- integer(S), write(S); name(S,T), mput0(S,T), !.

:-mode print_for_lisp_rest(+).
print_for_lisp_rest([]) :- !.
print_for_lisp_rest([X|Y]) :-
	tab(1), print_for_lisp(X), print_for_lisp_rest(Y), !.
print_for_lisp_rest(X) :- write(' . '), print_for_lisp(X), !.

:-mode slashp(+).
slashp([A|_]) :- memb(A," /|#(),.;:`'""").
slashp([_|X]) :- slashp(X).

:-mode mput0(+,+).
%Heuristic: if needs slashification, we print a string,
%unless length=1, in which case we print a slashified character.
mput0(_,[A]) :- slashp([A]), !, put("/"), put(A).
mput0(_,X) :- slashp(X), !, put(""""), mput1(X), put("""").
mput0(Name,[Q|R]) :- memb(Q,"?"), !, put("?"), write(Name).
mput0(Name,_) :- write(Name).

:-mode mput1(+).
mput1([A|B]) :- memb(A,"/;"""), !, put("/"), put(A), mput1(B).
mput1([A|B]) :- !, put(A), mput1(B).
mput1([]).

:-mode conjunction_list(+,-).
conjunction_list(true,[]) :- !.
conjunction_list((A,B),[A1|B1]) :- !,
	first_translation(A,pred,A1), conjunction_list(B,B1).
conjunction_list(A,[A1]) :- first_translation(A,pred,A1).

:-mode disjunction_list(+,-).
disjunction_list(fail,[]) :- !.
disjunction_list((A;B),[A1|B1]) :- !,
	first_translation(A,pred,A1), disjunction_list(B,B1).
disjunction_list(A,[A1]) :- first_translation(A,pred,A1).

:-mode cases_list(+,-).
cases_list((P->Q;R->S),[Case1,Case2]) :-
	first_translation((P->Q),pred,[cases,Case1]),
	first_translation((R->S),pred,[cases,Case2]).
cases_list((P->Q;R),[Thiscase|Rest]) :-
	first_translation((P->Q),pred,[cases,Thiscase]),
	(cases_list(R,Rest); first_translation(R,pred,R2), Rest=[[[true],R2]]).

:-mode quantified(+,-,-).
quantified(Formula,EveryQ,Inner) :-
	fq(Formula,SomeQ,Inner),
	(setof(A,free_for(A,SomeQ,Inner),EveryQ); EveryQ=[]).

:-mode fq(+,-,-).
fq(A^B,[A|R],P):-fq(B,R,P).
fq(A,[],A).

:-mode free_for(-,+,+).
free_for(X,SomeQ,X) :-
	X='$PVAR'(_), !, (memb(X,SomeQ), !, fail; true).
free_for(X,SomeQ,Y) :-
	nonvar(Y), !, Y=..Y1, memb(Y2,Y1), free_for(X,SomeQ,Y2).

:-mode memb(?,+).
memb(X,[X|L]).
memb(X,[_|L]) :- memb(X,L).

:-mode assertion(+,-).
assertion((P:-Q),[[P]|Q1]) :- atom(P), conjunction_list(Q,Q1).
assertion((P:-Q),[P1|Q1]) :- translation(P,term,P1), conjunction_list(Q,Q1).
assertion(P,P1) :- assertion((P:-true),P1).

:-mode arith_translation(+,-).
%the second argument of is/2.
arith_translation('$PVAR'(X),'$PVAR'(X)) :- !.
arith_translation(B,B1) :- translation(B,arith,B1).

:-mode first_translation(+,+,-).
first_translation(X,Y,Z) :- translation(X,Y,Z), !.

:-mode translation(+,+,-).
translation(X,arith,[quote,X]) :- X='$PVAR'(_).
translation(X,arith,X) :- atom(X).
translation([X|_],arith,X) :- integer(X).
translation(X,term,X) :- atom(X).
translation([A|B],term,[A1|B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(X,_,X) :- integer(X); X='$PVAR'(_).
translation(consult(A),pred,[load,A1]) :- translation(A,term,A1).
translation(reconsult(A),pred,[load,A1]) :- translation(A,term,A1).
translation([F|Fs],pred,[map,load,L]) :- translation([F|Fs],term,L).
translation(see(X),pred,T) :- warn_udf(see(X),T).
translation(seeing(X),pred,T) :- warn_udf(seeing(X),T).
translation(seen,pred,T) :- warn_udf(seen,T).
translation(tell(X),pred,T) :- warn_udf(tell(X),T).
translation(telling(X),pred,T) :- warn_udf(telling(X),T).
translation(told,pred,T) :- warn_udf(told,T).
translation(write(A),pred,[format,t,do(write('"~a"')),A1]) :- %really standard-output
	translation(A,term,A1).
translation(writeq(A),pred,[format,t,do(write('"~n"')),A1]) :- %really standard-output
	translation(A,term,A1).
translation(nl,pred,[tyo,do(write('#\return'))]).
translation(display(A),pred,[format,t,do(write('"~n"')),A1]) :-
	translation(A,term,A1).
translation(ttynl,pred,[tyo,do(write('#\return')),t]).
translation(ttyflush,pred,[true]).
translation(ttyget0(A),pred,[tyi,A1,t]) :-
	warn_md('ttyget0/1'), translation(A,term,A1).
translation(ttyget(A),pred,
	['prove-once',[repeat],[tyi,A1,t],['not-=',A1,do(write('#/ '))]]) :-
	translation(A,term,A1), warn_md('ttyget/1').
translation(ttyskip(A),pred,
	['prove-once',[repeat],[tyi,A1,t]]) :-
	translation(A,term,A1), warn_md('ttyskip/1').
translation(ttyput(A),pred,[tyo,A1,t]) :-
	translation(A,term,A1), warn_md('ttyput/1').
translation(get0(A),pred,[tyi,A1]) :-
	translation(A,term,A1), warn_md('get0/1').
translation(get(A),pred,
	['prove-once',[repeat],[tyi,A1],['not-=',A1,do(write('#/ '))]]) :-
	translation(A,term,A1), warn_md('get/1').
translation(skip(A),pred,
	['prove-once',[repeat],[tyi,A1]]) :-
	translation(A,term,A1), warn_md('skip/1').
translation(put(A),pred,[tyo,A1]) :- translation(A,term,A1), warn_md('put/1').
translation(tab(A),pred,[format,t,do(write('"~VX"')),A1]) :-
	translation(A,term,A1).
translation(read(A),pred,[read,A1]) :- translation(A,term,A1).
translation(putatom(X),pred,T) :- warn_udf(putatom(X),T).
translation(close(X),pred,T) :- warn_udf(close(X),T).
translation(fileerrors,pred,T) :- warn_udf(fileerrors,T).
translation(nofileerrors,pred,T) :- warn_udf(nofileerrors,T).
translation(rename(X,Y),pred,T) :- warn_udf(rename(X,Y),T).
translation(A is B,pred,['lisp-value',A1,B1,do(write(':dont-invoke'))]) :-
	translation(A,term,A1), arith_translation(B,B1).
translation(A+B,arith,[+,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A-B,arith,[-,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A*B,arith,[*,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A/B,arith,[/,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A mod B,arith,[\,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(-A,arith,[-,A1]) :- translation(A,arith,A1).
translation(A /\ B,arith,[logand,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A \/ B,arith,[logior,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(\(A),arith,[lognot,A1]) :- translation(A,arith,A1).
translation(A << B,arith,[lsh,A1,B1]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A >> B,arith,[lsh,A1,[-,B1]]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(!(A),arith,[\,A1,do(write('#o1000000'))]) :-
	warn_md('!/1'), translation(A,arith,A1).
translation($(A),pred,
	[-,[\,[+,A1,do(write('#o400000'))],do(write('#o1000000'))],do(write('#o400000'))]) :-
	warn_md('$/1'), translation(A,arith,A1).
translation(true,pred,[true]).
translation(fail,pred,[fail]).
translation((A,B),pred,[and|Conj]) :- conjunction_list((A,B),Conj).
translation((P->Q;R),pred,[cases|Cases]) :- cases_list((P->Q;R),Cases).
translation((A;B),pred,[or|Disj]) :- disjunction_list((A;B),Disj).
translation(length(A,B),pred,[length,B1,A1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(!,pred,[cut]).
translation(\+ A,pred,['cannot-prove',A1]) :-
	translation(A,pred,A1).
translation((A->B),pred,[cases,[['prove-once',A1],B1]]) :-
	translation(A,pred,A1), translation(B,pred,B1).
translation(abort,pred,T) :- warn_udf(abort,T).
translation(log,pred,T) :- warn_udf(log,T).
translation(nolog,pred,T) :- warn_udf(nolog,T).
translation(compare(X,Y,Z),pred,[compare,X1,Y1,Z1]) :-
	translation(X,term,X1), translation(Y,term,Y1), translation(Z,term,Z1).
translation(X @> Y,pred,T) :- warn_udf(X @> Y,T).
translation(X @< Y,pred,T) :- warn_udf(X @< Y,T).
translation(X @>= Y,pred,T) :- warn_udf(X @>= Y,T).
translation(X @=< Y,pred,T) :- warn_udf(X @=< Y,T).
translation(X>Y,pred,[>,X1,Y1]) :-
	translation(X,term,X1), translation(Y,term,Y1).
translation(X<Y,pred,[<,X1,Y1]) :-
	translation(X,term,X1), translation(Y,term,Y1).
translation(X=Y,pred,[=,X1,Y1]) :-
	translation(X,term,X1), translation(Y,term,Y1).
translation(A=:=B,pred,
	['lisp-predicate',[=,A1,B1],do(write(':dont-invoke'))]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A=\=B,pred,
	['lisp-predicate',[not,[=,A1,B1]],do(write(':dont-invoke'))]) :-
	translation(A,arith,A1), translation(B,arith,B1).
translation(A=<B,pred,['<=',A1,B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(A>=B,pred,['>=',A1,B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(A==B,pred,[identical,A1,B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(A\==B,pred,['not-identical',A1,B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(sort(X,Y),pred,T) :- warn_udf(sort(X,Y),T).
translation(keysort(X,Y),pred,T) :- warn_udf(keysort(X,Y),T).
translation(var(A),pred,[variable,A1]) :- translation(A,term,A1).
translation(nonvar(A),pred,['not-variable',A1]) :- translation(A,term,A1).
translation(atom(A),pred,[symbol,A1]) :- translation(A,term,A1).
translation(integer(A),pred,[number,A1]) :- translation(A,term,A1).
translation(functor(A,B,C),pred,
	    [and,[=,A1,[B1|'$PVAR'(U)]],[length,C1,'$PVAR'(U)]]) :-
	warn_md('functor/3'),
	translation(A,term,A1),
	translation(B,term,B1),
	translation(C,term,C1).
translation(arg(A,B,C),pred,[nth,C1,A1,B1]) :-
	translation(A,term,A1),
	translation(B,term,B1),
	translation(C,term,C1).
translation(A=..B,pred,[=,A1,B1]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(name(A,B),pred,[exploden,B1,A1]) :- 
	translation(A,term,A1), translation(B,term,B1), warn_md('name/2').
translation(clause(A,B),pred,[clause,[A1|B1]]) :-
	translation(A,term,A1), translation(B,term,B1).
translation(clause(X,Y,Z),pred,T) :- warn_udf(clause(X,Y,Z),T).
translation(listing,pred,['print-definition','$PVAR'(_)]).
translation(listing(A),pred,['print-definition',A1]) :- translation(A,term,A1).
translation(setof(A,B,C),pred,['quantified-set-of',C1,Q,A1,B2]) :-
	translation(A,term,A1),
	translation(C,term,C1),
	quantified(B,Q,B1),
	translation(B1,pred,B2).
translation(bagof(A,B,C),pred,['quantified-bag-of',C1,Q,A1,B2]) :-
	translation(A,term,A1),
	translation(C,term,C1),
	quantified(B,Q,B1),
	translation(B1,pred,B2).
translation(assert(A),pred,[assert,A1]) :- assertion(A,A1).
translation(asserta(X,Y),pred,T) :- warn_udf(asserta(X,Y),T).
translation(asserta(A),pred,[asserta,A1]) :- assertion(A,A1).
translation(assertz(X,Y),pred,T) :- warn_udf(assertz(X,Y),T).
translation(assertz(A),pred,[assertz,A1]) :- assertion(A,A1).
translation(assert(X,Y),pred,T) :- warn_udf(assert(X,Y),T).
translation(retract(A),pred,[retract,A1]) :- assertion(A,A1).
translation(abolish(A,_),pred,['retract-all',A1]) :- translation(A,term,A1).
translation(numbervars(X,Y,Z),pred,T) :- warn_udf(numbervars(X,Y,Z),T).
translation(ancestors(X),pred,T) :- warn_udf(ancestors(X),T).
translation(subgoal_of(X),pred,T) :- warn_udf(subgoal_of(X),T).
translation(current_atom(X),pred,T) :- warn_udf(current_atom(X),T).
translation(current_functor(X,Y),pred,T) :- warn_udf(current_functor(X,Y),T).
translation(current_predicate(N,_),pred,[predicator,N1]) :-
	translation(N,term,N1), warn_md('current_predicate/2').
translation(compile(F),pred,[map,'compile-file',F1]) :- translation(F,term,F1).
translation(incore(G),pred,[call,G1]) :- translation(G,pred,G1).
translation(call(G),pred,[call,G1]) :- translation(G,pred,G1).
translation(_^G,pred,[call,G1]) :- translation(G,pred,G1).
translation(revive(X,Y),pred,T) :- warn_udf(revive(X,Y),T).
translation(recorded(X,Y,Z),pred,T) :- warn_udf(recorded(X,Y,Z),T).
translation(recorda(X,Y,Z),pred,T) :- warn_udf(recorda(X,Y,Z),T).
translation(recordz(X,Y,Z),pred,T) :- warn_udf(recordz(X,Y,Z),T).
translation(erase(X),pred,T) :- warn_udf(erase(X),T).
translation(instance(X,Y),pred,T) :- warn_udf(instance(X,Y),T).
translation('NOLC',pred,T) :- warn_udf('NOLC',T).
translation('LC',pred,T) :- warn_udf('LC',T).
translation(prompt(X,Y),pred,T) :- warn_udf(prompt(X,Y),T).
translation(current_op(X,Y,Z),pred,T) :- warn_udf(current_op(X,Y,Z),T).
translation(op(X,Y,Z),pred,T) :- warn_udf(op(X,Y,Z),T).
translation(break,pred,T) :- warn_udf(break,T).
translation(save(X),pred,T) :- warn_udf(save(X),T).
translation(core_image,pred,T) :- warn_udf(core_image,T).
translation(restore(X),pred,T) :- warn_udf(restore(X),T).
translation(maxdepth(X),pred,T) :- warn_udf(maxdepth(X),T).
translation(depth(X),pred,T) :- warn_udf(depth(X),T).
translation(gcguide(X),pred,T) :- warn_udf(gcguide(X),T).
translation(gc,pred,T) :- warn_udf(gc,T).
translation(nogc,pred,T) :- warn_udf(nogc,T).
translation(trimcore,pred,T) :- warn_udf(trimcore,T).
translation(statistics,pred,T) :- warn_udf(statistics,T).
translation(statistics(X,Y),pred,T) :- warn_udf(statistics(X,Y),T).
translation(debug,pred,T) :- warn_udf(debug,T).
translation(nodebug,pred,T) :- warn_udf(nodebug,T).
translation(trace,pred,T) :- warn_udf(trace,T).
translation(leash(X),pred,T) :- warn_udf(leash(X),T).
translation(spy(X),pred,T) :- warn_udf(spy(X),T).
translation(nospy(X),pred,T) :- warn_udf(nospy(X),T).
translation(debugging,pred,T) :- warn_udf(debugging,T).
translation(expand_term(X,Y),pred,T) :- warn_udf(expand_term(X,Y),T).
translation(phrase(X,Y),pred,T) :- warn_udf(phrase(X,Y),T).
translation(portray(X),pred,T) :- warn_udf(portray(X),T).
translation(version,pred,T) :- warn_udf(version,T).
translation(version(X),pred,T) :- warn_udf(version(X),T).
translation(plsys(X),pred,T) :- warn_udf(plsys(X),T).
translation(reinitialise,pred,T) :- warn_udf(reinitialise,T).
translation(tmpcor(A,B,C),pred,T) :- warn_udf(tmpcor(A,B,C),T).
translation(run(A,B),pred,T) :- warn_udf(run(A,B),T).
translation(X,pred,T) :-
	X=..[F|Args], lm(F), warn_mask(F,F1), translation([F1|Args],term,T).
translation(X,_,X2) :- X=..X1, translation(X1,term,X2). %the default

:-mode lm(+).
lm(<). lm(=). lm(>). lm('add-world'). lm('all-worlds'). lm(and). lm(append). 
lm(apropos). lm('argument-list'). lm(assert). lm(asserta). lm(assertz). 
lm(assume). lm('bag-of'). lm('set-of'). lm(call). 
lm('can-prove'). lm('cannot-prove'). lm(cases). lm(infinite). lm(finite). 
lm('circularity-mode'). lm(clause). lm(clauses). lm(compile). lm(cut). 
lm('define-predicate'). lm(definition). lm('defined-in-world'). 
lm('delayed-value-mode'). lm(demos). lm('desctroy-world'). lm(difference). 
lm(documentation). lm(either). lm(exploden). lm(fail). lm(false). lm(format). 
lm('generate-name'). lm('generate-symbol'). lm('global-read'). lm(ground). 
lm(identical). lm(if). lm(interrupts). lm(intersection). lm('lazy-bag-of'). 
lm('lazy-set-of'). lm(load). lm('make-true'). lm(map). lm(member). lm(meter). 
lm('not-='). lm('not-identical'). lm('not-variable'). lm(number). 
lm('open-file'). lm(option). lm(or). lm(predicator). lm(print). 
lm('print-definition'). lm(product). lm('protected-worlds'). lm('prove-once'). 
lm('quantified-bag-of'). lm('quantified-set-of'). lm(quotient). lm(read). 
lm(remove). lm('remove-definition'). lm('remove-world'). lm('retract-all'). 
lm(retract). lm('destroy-world'). 
lm(reverse). lm(rules). lm(same). lm('save-world'). lm(substitute). lm(sum). 
lm(symbol). lm(time). lm('time-and-print'). lm(trace). lm(true). lm(tyi). 
lm(tyo). lm(type). lm(union). lm(universe). lm(untrace). lm('untrace-query'). 
lm('unwind-protect'). lm(variable). lm(variables). lm('who-state'). lm(with). 
lm('with-world'). lm('without-world'). lm('y-or-n'). 
lm(delete). lm(not). lm('compile-file').