% Copyright (C) 1983, Uppsala University. Authors: Jaan Koort, Mats Carlsson.
% Known bugs:
% Variable names that happen to be declared as operators can't be read in 
% 'NOLC' mode.  You have to enclose them in parentheses in the input file 
% of this program.

:-public devar/0,winst/2.
devar:-  asserta(predicates_to_translate([])),
         asserta(lc_mode(true)),
         tell('lmpc3:'),
         read_process(J,[]),
         ttynl,
         close('lmpc1:'),
         close('lmpc2:'),
	 winst(predicates_to_translate(J),predicates_to_translate(J)),
         told,
         seen.

read_mode(X) :- lc_mode(true), !, read_lc(X); read_nolc(X).

read_nolc(X) :- 'NOLC', read(Y), expand_term(Y,X).

read_lc(X) :- 'LC', read(Y), expand_term(Y,X).

read_process -->
	{see('lmpc1:'), read_mode(X), see('lmpc2:'), read_nolc(Y)},
	({X=end_of_file}; process(X,Y), !, read_process).

:-mode process(+,+,?,?).
process((:-op(X,Y,Z)),_) --> !,{op(X,Y,Z)}.
process((:-public(G)),_) --> !.
process((:-compactcode),_) --> !.
process((:-fastcode),_) --> !.
process((:-mode X,Y),_) --> process((:- mode X),_), process((:- mode Y),_).
process((:-mode G),_) -->
	!, {G=..[F|A], length(A,L), repasterisk(A,D),
	winst(lm_compile_declarations(F,D,L),lm_compile_declarations(F,D,L))},
	warnq(F).
process((:-'NOLC'),_) --> {retract(lc_mode(_)),assert(lc_mode(false)),!}.
process((:-'LC'),_) --> {retract(lc_mode(_)),assert(lc_mode(true)),!}.
process((:-Query),_) --> !,[lm_top_level_prove(Query)].
process(X,Y) --> {winst(X,Y), soft_functor(X,F)}, traceq(F).		

traceq(F) --> {traced(F), !};
	      {display(F), ttynl, assert(traced(F))}, [F].

warnq(F) --> {declared(F), !,
	      display('%More than one mode declaration of '),
	      display(F), ttynl};
	     {assert(declared(F))}.

soft_functor((:-(X,_)),F) :- !,soft_functor(X,F).
soft_functor(X,F) :- functor(X,F,_).

:-mode repasterisk(+,-).
repasterisk([],[]).
repasterisk([?|R],['*'|T]) :- !,repasterisk(R,T).
repasterisk([X|R],[X|T]) :- repasterisk(R,T).

winst(T,U) :- winst1(T,U), put("."), nl, nl.

winst1(X,Y) :- var(X), var(Y), !, writeq('$PVAR'(Y)).
winst1(X,Y) :- var(X), !, winst1('$PVAR'(Y),'$PVAR'(Y)).
winst1((mode),(mode)) :- !, write('(mode)').
winst1((public),(public)) :- !, write('(public)').
winst1({X},{X}) :- !, put("{"), winst1(X,X), put("}").
winst1(X,X) :- atomic(X), !, writeq(X).
winst1(X,Y) :- functor(X,F,N), writeq(F), winst2(0,N,X,Y,"(").

winst2(N,E,T,U,[C]) :-
	N<E, M is N+1, arg(M,T,X), arg(M,U,Y),
	put(C), winst1(X,Y), winst2(M,E,T,U,",").
winst2(E,E,_,_,_) :- put(")").