%====================================================================
%----This module holds the clauses for shortening all the symbols in
%----a TPTP input set.

%----Written by Geoff Sutcliffe, March, 1993.
%====================================================================
%--------------------------------------------------------------------
%----This makes a short term from the letter and index
make_shortened_atomic__(Letter,Index,Shortened_atomic,New_index):-
    name(Letter,[Letter_ascii]),
    tptpshort_integer_name__(Index,Index_list),
    name(Shortened_atomic,[Letter_ascii|Index_list]),
    New_index is Index + 1.
%--------------------------------------------------------------------
%----Make a short vaiable name (as an atom now)
%----First look if it has been seen before. Need to use == here.
shorten_variable__(Variable,Index,Index,Shortenings,Shortenings,
Shortened_variable):-
    member__(A_variable-Shortened_variable,Shortenings),
    Variable == A_variable,
    !.

shorten_variable__(Variable,Index,New_index,Shortenings,
[Variable-Shortened_variable|Shortenings],Shortened_variable):-
    make_shortened_atomic__('X',Index,Shortened_variable,New_index).
%--------------------------------------------------------------------
%-----Convert from an integer to a list of characters
tptpshort_integer_name__(Integer,Final_string):-
    tptpshort_integer_name__(Integer,[],Final_string).

tptpshort_integer_name__(Integer,String_so_far,[Character|
String_so_far]):-
    Integer < 10,
    !,
    Character is Integer + 48.

tptpshort_integer_name__(Integer,String_so_far,Final_string):-
    Top_half is Integer // 10,
    Bottom_half is Integer mod 10,
    Character is Bottom_half + 48,
    tptpshort_integer_name__(Top_half,[Character|String_so_far],
Final_string).
%----------------------------------------------------------------------
%----Atomic things get shortened here
%----First case is this symbol has been seen before. Have to use ==
%---- to avoid confusion with variable shortenings.
shorten_atomic__(Atomic,_,_,Index,Index,Shortenings,Shortenings,
Shortened_atomic):-
    member__(An_atom-Shortened_atomic,Shortenings),
    Atomic == An_atom,
    !.

%----Constants
shorten_atomic__(Constant,term,0,Index,New_index,Shortenings,
[Constant-Shortened_constant|Shortenings],Shortened_constant):-
    !,
    make_shortened_atomic__(c,Index,Shortened_constant,New_index).

%----Functors
shorten_atomic__(Functor,term,Number_of_arguments,Index,New_index,
Shortenings,[Functor-Shortened_functor|Shortenings],
Shortened_functor):-
    Number_of_arguments > 0,
    !,
    make_shortened_atomic__(f,Index,Shortened_functor,New_index).

%----Predicate symbols
shorten_atomic__(Predicate,atom,_,Index,New_index,Shortenings,
[Predicate-Shortened_predicate|Shortenings],Shortened_predicate):-
    !,
    make_shortened_atomic__(p,Index,Shortened_predicate,New_index).
%--------------------------------------------------------------------
shorten_terms__([],Index,Index,Shortenings,Shortenings,[]):-
    !.

shorten_terms__([First_term|Rest_of_terms],Next_index,New_index,
Shortenings,New_shortenings,[Shortened_first_term|
Rest_of_shortened_terms]):-
    shorten_term__(First_term,term,Next_index,Middle_index,
Shortenings,Middle_shortenings,Shortened_first_term),
    shorten_terms__(Rest_of_terms,Middle_index,New_index,
Middle_shortenings,New_shortenings,Rest_of_shortened_terms).
%--------------------------------------------------------------------
%----Shorten a term, based on the principle symbol shortenings and
%----argument shortenings provided
shorten_term__(Variable,term,Index,New_index,Shortenings,
New_shortenings,Shortened_variable):-
    var(Variable),
    !,
    shorten_variable__(Variable,Index,New_index,Shortenings,
New_shortenings,Shortened_variable).

shorten_term__(Term,Term_type,Next_index,New_index,Shortenings,
New_shortenings,Shortened_term):-
%----Break off the symbol and arguments
    Term =.. [Principle_symbol|Arguments],
    length(Arguments,Number_of_arguments),
%----Shorten the predicate symbol
    shorten_atomic__(Principle_symbol,Term_type,Number_of_arguments,
Next_index,Middle_index,Shortenings,Middle_shortenings,
Shortened_principle_symbol),
%----Shorten the arguments
    shorten_terms__(Arguments,Middle_index,New_index,
Middle_shortenings,New_shortenings,Shortened_arguments),
%----Put it all back together again
    Shortened_term =.. [Shortened_principle_symbol|
Shortened_arguments].
%--------------------------------------------------------------------
%----Convert all the literals' predicate symbols and fcuntors
shorten_literals__([],Index,Index,Shortenings,Shortenings,[]):-
    !.

shorten_literals__([First_literal|Rest_of_literals],Next_index,
New_index,Shortenings,New_shortenings,[Shortened_first_literal|
Rest_of_shortened_literals]):-
%----Strip off the sign
    First_literal =.. [Sign,Atom],
%----Shorten the atom
    shorten_term__(Atom,atom,Next_index,Middle_index,Shortenings,
Middle_shortenings,Shortened_atom),
%----Put back on the sign
    Shortened_first_literal =.. [Sign,Shortened_atom],
%----Do the rest of the literals
    shorten_literals__(Rest_of_literals,Middle_index,New_index,
Middle_shortenings,New_shortenings,Rest_of_shortened_literals).
%--------------------------------------------------------------------
%----Convert all the predicate symbols and functors to short ones
shorten_clauses__([],Clause_index,Clause_index,Index,Index,
Shortenings,Shortenings,[]):-
    !.

shorten_clauses__([input_clause(_Name,Status,Literals)|Rest_of_clauses],
Clause_index,New_clause_index,Next_index,New_index,Shortenings,
New_shortenings,[input_clause(Indexed_name,Status,Shortened_literals)|
Rest_of_shortened_clauses]):-
    make_shortened_atomic__(c,Clause_index,Indexed_name,
Middle_clause_index),
    shorten_literals__(Literals,Next_index,Middle_index,Shortenings,
Middle_shortenings,Shortened_literals),
    shorten_clauses__(Rest_of_clauses,Middle_clause_index,
New_clause_index,Middle_index,New_index,Middle_shortenings,
New_shortenings,Rest_of_shortened_clauses).
%--------------------------------------------------------------------
%----Entry point for these routines
shorten_clauses__(Input_clauses,Shortened_clauses):-
    shorten_clauses__(Input_clauses,1,_,1,_,[],_,Shortened_clauses).
%--------------------------------------------------------------------

