module forumlog.

%  The logical connectives for Forum.
%% These are divided into three groups.
%% (Some are commented out since they are already present in elp.)
%% (1) Those already present in lambda Prolog.

% type =>                o -> o -> o.    % intuitionistic implication
% type pi                (A -> o) -> o.  % universal quantification
  type -o                o -> o -> o.    % lollipop
  type o-                o -> o -> o.    % reverse lollipop
  type <=                o -> o -> o.    % intuitionistic implication
  infixr -o 1.
  infixl o- 1.
  infixl <= 4.

%% (2) Those new to lambda Prolog

  type erase             o.              % top (additive true)
  type &                 o -> o -> o.    % with (additive and )
  type bottom            o.              % multiplicative false
  type |                 o -> o -> o.    % par (multiplicative or)
  type ?                 o -> o.         % why-not modal
  infixr & 2.
  infixr | 3.

%% (3) Those that can be used in positive occurrences

% type true              o.              % multiplicative true
% type ,                 o -> o -> o.    % tensor (multiplicative and)
% type ;                 o -> o -> o.    % o-plus (additive or)
% type sigma             (A -> o) -> o.  % existential quantification
  type bang              o -> o.         % of-course modal

% Two predicates useful to have here.  Used by the next interpreter.

type cl       o -> o.
type qt       o -> o.

type atomic        o -> o.
type non_atomic    o -> o.

non_atomic (B o- C).
non_atomic (B => C).
non_atomic (B -o C).
non_atomic (B <= C).
non_atomic (B | C).
non_atomic (B & C).
non_atomic (B , C).
non_atomic (B ; C).
non_atomic (? B).
non_atomic (bang B).
non_atomic (pi B).
non_atomic (sigma B).
non_atomic (erase).
non_atomic (bottom).
non_atomic (true).

atomic B :- not (non_atomic B).

% special lambda Prolog predicates are treated here.

type special   o -> o.

special (N is M).
special (X =  Y).
special (write M).
special (writesans S).
special nl.