module parser.
import scan, lex, fol, control.

type fullstop          list lex -> o.

fullstop (period::nil).

type make_infix  lex -> form -> form -> form -> o.

make_infix andtok A B (A and B).
make_infix ortok  A B (A or  B).
make_infix imptok A B (A imp B).

type make_quant   lex -> string -> (i -> form) -> form -> o.

make_quant foralltok Var B (forall Var B).
make_quant existstok Var B (exists Var B).

type parse_form        form        -> list lex -> list lex -> o.
type parse_atom        form        -> list lex -> list lex -> o.
type parse_term        i           -> list lex -> list lex -> o.
type parse_term_list   list i      -> list lex -> list lex -> o.
type parse_terms       list i      -> list lex -> list lex -> o.
type parse_tail        list i      -> list lex -> list lex -> o.
type parse_abstraction (i -> form) -> list lex -> list lex -> o.

parse_form A B C :- announce (parse_form A B C).
parse_atom A B C :- announce (parse_atom A B C).
parse_term A B C :- announce (parse_term A B C).
parse_terms A B C :- announce (parse_terms A B C).
parse_term_list A B C :- announce (parse_term_list A B C).

parse_form truth (truthtok::In) In :- !.
parse_form false (falsetok::In) In :- !.

parse_form (neg A) (lparen::negtok::In) Out :- !, 
  parse_form A In (rparen::Out).

parse_form Quant (lparen::Qtok::(tok Var)::In) Out :-
  make_quant Qtok Var B Quant, !, 
  piname Var x\(parse_form (B x) In (rparen::Out)).

parse_form Infix (lparen::In) Out :-
  parse_form A In (Tok::Mid), make_infix Tok A B Infix, !, 
  parse_form B Mid (rparen::Out).  

parse_form Atom In Out :- parse_atom Atom In Out.

parse_atom Atom ((tok Name)::In) In :- !, 
  (print_name_pred Atom Name Args, !, Args = nil;
   print "Parse Error: The token ", print Name,
   print " is not given a print_name_pred.\n", fail).

parse_atom Atom (lparen::(tok Name)::In) Out :-
  (print_name_pred Atom Name Args, !;
   print "Parse Error: The token ", print Name,
   print " is not given a print_name_pred.\n", fail), 
  parse_term_list Args In Out.

parse_term_list nil (rparen::In) In :- !.

parse_term_list (T::Ts) In Out :-
  parse_term T In Mid, parse_term_list Ts Mid Out.

parse_term Term ((tok Name)::In) In :-
  print_name_term Term' Name Args, !, Term = Term', Args = nil.

parse_term Term (lparen::(tok Name)::In) Out :-
  print_name_term Term Name Args, parse_term_list Args In Out.

parse_terms (T::Ts) In Out :- parse_term T In Mid, parse_tail Ts Mid Out.

parse_tail nil In In.
parse_tail Ts (comma::In) Out :- parse_terms Ts In Out.

parse_abstraction Abs Ls nil :- announce (parse_abstraction Abs Ls nil).

parse_abstraction B (lambdatok::tok Name::In) Out :- 
  piname Name x\(parse_form (B x) In Out).

type read_form          string -> form        -> o.
type read_term          string -> i           -> o.
type read_terms         string -> list i      -> o.
type read_term_line     string -> i           -> o.
type read_abstraction   string -> (i -> form) -> o.

read_form String Term :- scan String Ls, parse_form Term Ls nil.

read_term String Term :- scan String Ls, parse_term Term Ls nil.

read_term_line String Term :-
  scan String Ls, parse_term Term Ls Out, fullstop Out.

read_terms String Terms :-
  scan String Ls, parse_terms Terms Ls nil.

read_abstraction String Abs :-
  scan String Ls, parse_abstraction Abs Ls nil.