%% implementation of a parser for PL1
%% Authors: Uwe Reyle / Philipp Cimiano Lavin
%% Date:    18/07/00


%%Start
parse(String,Tree) :-  string_to_list(String,Ascii_list),
                       char2atom(Ascii_list,Formula),
                       formula(Tree,Formula,[]).


%%Formulas


%Atomic formulas
formula(F) --> atom(F).

%Negation
formula(not(F))--> negation, formula(F).

%Connetives
formula(F) --> open_bracket,
               formula(F1),
               connective(Connective),
               formula(F2),
               close_bracket,
               {
                 F=..[Connective,F1,F2]
               }.

%Quantors
formula(F) --> quantor(Quantor),
               var(Variable),
               formula(Fsub),
               {
                 F=..[Quantor,Variable,Fsub]
               }.




%%Atoms

%Predicates with Arity=0
atom(F) --> p([],F).

%Predicates with Arity#0
atom(F) --> p(Arity,Predicate_Name),
            open_bracket,
            termlist(Arity,Termlist),
            close_bracket,
            {
              F=..[Predicate_Name|Termlist]
            }.         




%%Terms


%Variables
term([T]) --> var(T).

%Constants
term([T]) --> f([],T).

%Functions
term([T]) --> f(Arity,Function_Name), 
              open_bracket, 
              termlist(Arity,Termlist), 
              close_bracket,
              {
                T=..[Function_Name|Termlist]
              }.


termlist([_],Termlist) --> term(Termlist).

termlist([_|Rest],Termlist) --> term(Term),
                                comma,
                                termlist(Rest,Rest_Termlist),
                                {
                                  append(Term,Rest_Termlist,Termlist)
                                }.
  



%Negation
negation --> [-].


%Connectives(Lexicon)
connective(and) --> ['&'].
connective(imp)  --> ['>'].
connective(or) --> [v].
connective(eq) --> ['='].


%Quantors(Lexicon)
quantor(forall) --> [f].
quantor(exists) --> [e].


%Brackets & Commas(Lexicon)
open_bracket --> ['('].
close_bracket --> [')'].
comma --> [','].




%Predicates
p([],p)      --> [p].
p([_],q)     --> [q].
p([_,_,_],r) --> [r].

%Constants
f([],a) --> [a].
f([],b) --> [b].

%Functions
f([_],f)   --> [f].
f([_,_],g) --> [g].

%Variables
var(x) --> [x].
var(y) --> [y].
var(z) --> [z].


% append
% concatenates two lists
append([],Liste2,Liste2).
append([First|Rest],Liste2,[First|Res]) :- append(Rest,Liste2,Res).


% char2atom
% converts a list of ascii-symbols into a list of atoms
char2atom([],[]).
char2atom([First|Rest],[First_atom|Rest_atoms]) :- atom_char(First_atom,First),
                                                   char2atom(Rest,Rest_atoms).