/*************************************************************************

         name: semconHelpers.pl
      version: July 2003
  description: Helper Predicates for semantic construction
      authors: Aljoscha Burchardt, Stephan Walter

*************************************************************************/

:- module(semconHelpers,[compose/3,substitute/4,vars2atoms/1,resetVars/0,readLine/1]).
:- [comsemOperators].


/*========================================================================
   Compose predicate argument structure
========================================================================*/

compose(Term,Symbol,ArgList):-
    Term =.. [Symbol|ArgList].


/*========================================================================
   Substitution Predicates
========================================================================*/

substitute(Term,Var,Exp,Result):- 
   Exp==Var, !, Result=Term.
substitute(_Term,_Var,Exp,Result):- 
   \+ compound(Exp), !, Result=Exp.
substitute(Term,Var,Formula,Result):-
   compose(Formula,Functor,[Exp,F]),
   member(Functor,[lambda,forall,exists]), !, 
   (
    Exp==Var, !, 
    Result=Formula
   ; 
    substitute(Term,Var,F,R),
    compose(Result,Functor,[Exp,R])
   ).
substitute(Term,Var,Formula,Result):-
   compose(Formula,Functor,ArgList),
   substituteList(Term,Var,ArgList,ResultList),
   compose(Result,Functor,ResultList).

substituteList(_Term,_Var,[],[]).
substituteList(Term,Var,[Exp|Others],[Result|ResultOthers]):-
   substitute(Term,Var,Exp,Result),
   substituteList(Term,Var,Others,ResultOthers).


/*========================================================================
   New Variables
========================================================================*/

%% First-order variables, they are represented as PROLOG constants.
%% var would overwrite in-built Prolog var/1, so we assert them as  fovar(x),fovar(y)...

resetVars :-
	retractall(fovar(_)),
	retractall(varcount(_)),
	assert(varcount(0)).

:- resetVars.


%% new variables v1, v2...
newvar(Sym) :-
	inc(varcount,N),
	int_to_atom(N,A),
	concat_atom([v,A],Sym),
	assert(fovar(Sym)).


/*========================================================================
   Make (var-)atoms out of all Prolog variables of a term.
========================================================================*/

vars2atoms(T) :-
	free_variables(T,Vars),
	vars2atomsRec(Vars).

vars2atomsRec([]).

vars2atomsRec([H|T]) :-
	newvar(H),
	vars2atomsRec(T).


vars2atomsList([]).

vars2atomsList([H|T]) :-
	vars2atoms(H),
	vars2atomsList(T).


/*========================================================================
   A Little Helper
========================================================================*/

inc(Counter,New) :-
	C =.. [Counter,Old],
	retract(C),
	New is Old + 1,
	NewC =.. [Counter,New],
	assert(NewC).


/*========================================================================

   Read Predicates
   ---------------

readLine(-WordList)
   Outputs a prompt, reads a sequence of characters from the standard
   input and converts this to WordList, a list of strings. Punctuation 
   is stripped.

readWords(-WordList)
   Reads in a sequence of characters, until a return is registered, 
   and converts this to WordList a list of strings. 

readWord(+Char,-Chars,?State)
   Read a word coded as Chars (a list of ascii values), starting 
   with with ascii value Char, and determine the State of input
   (`ended' = end of line, `notended' = not end of line).
   Blanks and full stops split words, a return ends a line.

checkWords(+OldWordList,-NewWordList)
   Check if all words are unquoted atoms, if not convert them 
   into atoms.

convertWord(+OldWord,-NewWord)
   OldWord and NewWord are words represented as lists of ascii values.
   Converts upper into lower case characters, and eliminates
   non-alphabetic characters.

========================================================================*/

readLine(WordList):-
   nl, write('> '),
   readWords(Words),
   checkWords(Words,WordList).

readWords([Word|Rest]):-
   get0(Char),
   readWord(Char,Chars,State),
   name(Word,Chars),
   readRest(Rest,State).

readRest([],ended).
readRest(Rest,notended):-
   readWords(Rest).

readWord(32,[],notended):-!.     %%% blank
readWord(46,[],notended):-!.     %%% full stop
readWord(10,[],ended):-!.        %%% return
readWord(Code,[Code|Rest],State):-
   get0(Char),
   readWord(Char,Rest,State).

checkWords([],[]):- !.
checkWords([''|Rest1],Rest2):-
   checkWords(Rest1,Rest2).
checkWords([Atom|Rest1],[Atom2|Rest2]):-
   name(Atom,Word1),
   convertWord(Word1,Word2),
   name(Atom2,Word2),
   checkWords(Rest1,Rest2).

convertWord([],[]):- !.
convertWord([Capital|Rest1],[Small|Rest2]):-
   Capital > 64, Capital < 91, !,
   Small is Capital + 32,
   convertWord(Rest1,Rest2).
convertWord([Weird|Rest1],Rest2):-
   (Weird < 97; Weird > 122), !,
   convertWord(Rest1,Rest2).
convertWord([Char|Rest1],[Char|Rest2]):-
   convertWord(Rest1,Rest2).