module two.
import forumlog aux.

type right    list o -> list o -> list o -> o.
type left     list o -> o -> list o -> o.

% This line allows you to trace the progress of the search.
right Delta Atoms Gamma :- write (right Delta Atoms Gamma), nl, fail.

% This line is used to call some of elp's special predicates from
% inside Forum.  See forumlog.mod for specification of the special
% predicate.

right nil (A::nil) nil :- special A, !, A.

right Delta Atoms nil :-
  membNrest B Delta Rest, left  Rest  B Atoms;
  cl B, left  Delta B Atoms;
  qt B, right Delta Atoms (B::nil).

right Delta Atoms (Atom::Gamma) :-
  atomic Atom, right Delta (Atom::Atoms) Gamma.

right Delta Atoms (erase::Gamma).

right Delta Atoms ((B & C)::Gamma) :-
  right Delta Atoms (B::Gamma), right Delta Atoms (C::Gamma).

right Delta Atoms (bottom::Gamma) :-
  right Delta Atoms Gamma.

right Delta Atoms ((B | C)::Gamma) :-
  right Delta Atoms (B::C::Gamma).

right Delta Atoms ((B -o C)::Gamma) :-
  right (B::Delta) Atoms (C::Gamma).

right Delta Atoms ((C o- B)::Gamma) :-
  right (B::Delta) Atoms (C::Gamma).

right Delta Atoms ((B => C)::Gamma) :-
  cl B => right Delta Atoms (C::Gamma).

right Delta Atoms ((pi B)::Gamma) :-
  pi x\(right Delta Atoms ((B x)::Gamma)).

right Delta Atoms ((? B)::Gamma) :-
  qt B => right Delta Atoms Gamma.

% left Delta B Atoms :- write (left Delta B Atoms), nl, fail.

left nil A (A::nil).

left nil A nil :- qt A.

left nil bottom nil.

left Delta (B & C) Atoms :- left Delta B Atoms; left Delta C Atoms.

left nil (? B) nil :- right (B::nil) nil nil.

left Delta (B | C) Atoms :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  left Delta1 B Atoms1, left Delta2 C Atoms2.

left Delta (pi B) Atoms :- left Delta (B T) Atoms.

left Delta (B -o C) Atoms :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  left  Delta2 C Atoms2, right Delta1 Atoms1 (B::nil).

left Delta (C o- B) Atoms :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  left  Delta2 C Atoms2, right Delta1 Atoms1 (B::nil).

left Delta (B => C) Atoms :-
  left  Delta C Atoms, right nil nil (B::nil).