%======================================================================
%----This module holds the clauses for reading input sets in TPTP 
%----format. This code has to be executed in the parent directory of 
%----the Problems and Axioms directories, due to the references to 
%----axiom files in the problem files.

%----Written by Geoff Sutcliffe, July, 1992.
%======================================================================
%----This specifies the parent directory of the TPTP Problems and Axioms
%----directories. To work from the current directory, use '.' here.
tptp_directory__('~/TPTP').
%---------------------------------------------------------------------
%----Make a completed path name from the TPTP directory and the
%----supplied file name
%----If there is a leading /, then do nothing.
tptp_path_name__(File_name,File_name):-
    name(File_name,[47|_]),
    !.

%----If there is a leading ~, then do nothing.
tptp_path_name__(File_name,File_name):-
    name(File_name,[126|_]),
    !.

%----If no leading /, then put the TPTP directory on front
tptp_path_name__(File_name,Path_name):-
    name(File_name,File_name_list),
    tptp_directory__(Directory),
    name(Directory,Directory_list),
    append__(Directory_list,[47|File_name_list],Path_name_list),
    name(Path_name,Path_name_list).
%---------------------------------------------------------------------
%----Determine what to do with the term read.
%----Input clauses are returned in a list
filter_for_clauses__(input_clause(Name,Status,Literals),Dictionary,
[input_clause(Name,Status,Literals)],Dictionary):-
    !.
    
%----Include directive cause recursive call to the top level to read
%----the included file.
filter_for_clauses__(include(File_name),_,Input_clauses,Dictionary):-
    !,
    read_input_clauses_from_file__(File_name,Input_clauses,_,
Dictionary).
    
filter_for_clauses__(Term,_,[],[]):-
    write('Input term '),
    write(Term),
    write(' ignored'),
    nl.
%---------------------------------------------------------------------
%----This pulls apart the dictionary and instantiates the variables
%----with their names.
%----Special case of numbervars, simply call it
instantiate_variables_from_dictionary__([numbervars=Term|
Rest_of_list]):-
    !,
    numbervars(Term,0,_),
    instantiate_variables_from_dictionary__(Rest_of_list).

%----If a variable then that's the end of the dictionary branch.
instantiate_variables_from_dictionary__([]):-
    !.

%----Otherwise instantiate this node and do sub-dictionaries
instantiate_variables_from_dictionary__([Name=Name|Rest_of_list]):-
    instantiate_variables_from_dictionary__(Rest_of_list).
%----------------------------------------------------------------------
%----Convert a SICStus dictionary into a list of variable-name pairs
make_dictionary_from_SICStus_dictionary__(SICStus_dictionary,[]):-
    var(SICStus_dictionary),
    !.

make_dictionary_from_SICStus_dictionary__(dic(NameList,[Variable|_],
Smaller_SICStus_dictionary,Larger_SICStus_dictionary),
[Name=Variable|Rest_of_dictionary]):-
    name(Name,NameList),
    make_dictionary_from_SICStus_dictionary__(Smaller_SICStus_dictionary,
Smaller_dictionary),
    make_dictionary_from_SICStus_dictionary__(Larger_SICStus_dictionary,
Larger_dictionary),
    append__(Smaller_dictionary,Larger_dictionary,Rest_of_dictionary).
%----------------------------------------------------------------------
%----This is the entry point for reading
%----The naive read that does not preserve variable names
%----Set the dictionary to a special flag for later instantiating.
realRead(Term,Dictionary):-
    read(Term),
    Dictionary = [numbervars=Term].

%----The Quintus top level read
%realRead(Term,Dictionary):-
%    read_term([variable_names(Dictionary)],Term).

%----The SISCtus 0.7 top level read
%realRead(Term,Dictionary):-
%   'SYSCALL'(read_top_level(Term,SICStus_dictionary)),
%   make_dictionary_from_SICStus_dictionary__(SICStus_dictionary,
%Dictionary).

%----The SICStus 2.1 top level read. 
%realRead(Term,Dictionary):-
%    current_input(Input_stream),
%    prolog:read_top_level(Input_stream,Term,SICStus_dictionary),
%    make_dictionary_from_SICStus_dictionary__(SICStus_dictionary,
%Dictionary).
%----------------------------------------------------------------------
%----Read in cluases from current input device, until eof
read_input_clauses__(Input_clauses,Dictionary):-
%----Need to deal with skolem_functor facts here, if and when I add
%----the equality stuff again
    realRead(Prolog_term,Term_dictionary),
    \+ (Prolog_term == end_of_file),
    !,
%----Check if an include, and return all clauses resulting
    filter_for_clauses__(Prolog_term,Term_dictionary,Input_clause_list,
Clause_dictionary),
    read_input_clauses__(Rest_of_clauses,Rest_of_dictionary),
    append__(Input_clause_list,Rest_of_clauses,Input_clauses),
    append__(Clause_dictionary,Rest_of_dictionary,Dictionary).

read_input_clauses__([],[]).
%----------------------------------------------------------------------
%----Read input clauses from a file, doing includes too
read_input_clauses_from_file__(File_name,Input_clauses,Problem_name,
Dictionary):-
    seeing(Current_input),
    tptp_path_name__(File_name,Path_name),
    see(Path_name),
    read_input_clauses__(Input_clauses,Dictionary),
%----Cut, so that later errors do not try to read more input clauses
    !,
    seen,
    see(Current_input),
%----Make problem name from file name
    basename__(File_name,'.p',Problem_name).
%--------------------------------------------------------------------
