% module:   syntax.pl
% date:     January 6, 2005, HAPPY NEW YEAR
% author:   Douglas M. Auclair (DMA)

% copyright (c) 2005, Cotillion Group, Inc. All rights reserved.

% synopsis: Some syntactic shorthand for logic expressions and set
%           theory.

:- module(syntax, [
	(<-)/2,
	try/1, try/3, sinon/2, sinon/4,
	(\/)/2, (/\)/2, (~)/1,
	(<=)/2, (<=>)/2, (=>)/2
]).

% The following meta_predicate/1 declarations allow us to essay proofs
% without the combersomely prepended module specifications.

:- meta_predicate sinon(:, :).
:- meta_predicate sinon(:, :, +, -).
:- meta_predicate try(:).
:- meta_predicate try(:, +, -).
:- meta_predicate ~(:).
:- meta_predicate /\(:, :).
:- meta_predicate \/(:, :).
:- meta_predicate <=(:, :).
:- meta_predicate <=>(:, :).
:- meta_predicate =>(:, :).

:- op(200,  yfx, <-).
:- op(200,   fx, try).
:- op(500,  yfx, \/).
:- op(500,  yfx, /\).
:- op(900,   fy, ~).
:- op(920,  xfy, <= ).
:- op(920,  xfy,  =>).
:- op(920,  xfy, <=>).
:- op(1100, xfy, sinon).

% modified: December 2, 2005, DMA
% changed:  Corrected syntax of meta_predicate/1, as Quintus pukes on
%           using (*) as argument descriptor.

% modified: November 18, 2005, DMA
% changed:  Converted the top-level file back to a module (so it's
%	    now in 'modular form', as it were ... teehee, math jokes
%	    crack me up); renamed back to syntax.pl

% modified: November 16, 2005, DMA
% changed:  Converted this file back to a top-level (not module) file;
%           moved all set syntax to this file, as well.  Removed
%           member check for <-.  Renamed this file from 'syntax.pl'
%           to 'logic_syntax.pl'

% modified: February 16, 2005, DMA
% changed:  Reencapsulated this file as a module; using modules must
%           now explicitly declare a called predicate's module.

% modified: January 7, 2005, DMA
% changed:  Removed module declaration, as call(G) becomes confused,
%           added <-/2.

% sinon/[2,4] permits two proofs to be essayed consecutively -- it's
% very much in the syntactic/semantic vein of ';'/[2,4], except that
% the order is deterministic for sinon/[2,4] (fr: 'if not') whereas
% 'GoalA; GoalB'/[2,4]'s order is not by nature fixed (I've observed
% situations where GoalB, usually the more general case, being
% executed first, leading to unintented results).

sinon(TryThisFirst, OtherwiseTryThis) :-
  TryThisFirst -> true; OtherwiseTryThis.
sinon(TryThisFirst, OtherwiseTryThis) -->
  TryThisFirst -> []; OtherwiseTryThis.

% try/[1,3] is really a derivative sinon/[2,4]: (try X) = (X sinon true).
% 'try Goal' calls Goal and simply succeeds, even if goal fails,
% preventing (some would say: 'subverting') bactracking over an
% establish proof branch.

try X :- X -> true; true.
try X --> X -> []; [].

% Ever try to explain why \+/1 ('for every') means 'not' and not look
% stupid while 'explaining' the concept?  It's very, very hard,
% especially given the somewhat different meaning of \+ in mathematics
% ... so, as a face-saving measure I propose the following reasonable
% alternative: ~/1.

~ X :- \+ call(X).
%    would a DCG version of '~Goal' make any sense?

% Some more mathematics:

A /\ B :- A, B.
A \/ B :- A ; B.

%    Try, e.g., (X = 5) \/ (X = 7).  Now wasn't that fun?

X <- [X|_].
X <- [_|List] :- X <- List.

Goal1 <=  Goal2 :- ~(Goal2 /\ ~(Goal1)).
Goal1 <=> Goal2 :- (Goal1 => Goal2) /\ (Goal1 <= Goal2).
Goal1  => Goal2 :- ~(Goal1 /\ ~(Goal2)).

% so, given the above, what holds about L1 and L2 if:
%    X <- L1 <=> X <- L2.