/* This is a literate program.

Preprocessing
=============
The preprocessor has three main functions:

(1) It converts sets and sequences to internal format (currently, sorted lists).
(2) It applies scope rules.
(3) It standardises syntactic variants, e.g., '\<' becomes '>='.

The point about scope rules needs some introductory explanation.  Suppose that 'add1' is defined as '{X->X+1}'.  Then '1!add1!add1 ought to yield 3.  But from the definition of 'add1', one should also be able to write '1!{X->X+1}!{X->X+1}'.  However, a simple interpretation binds all the X's to the same value, resulting in '1!{1->1+1}!{1->1+1}'.  The subexpression '1!{1->1+1}' simplifies to '2', resulting in '2!{1->1+1}' for the whole expression.  Since '{1->1+1}' is not applicable to '2', no result would be found.  Therefore, in this context, the X's must be read as different.  This suggests that a variable should have a scope limited by the enclosing braces.  On the other hand, in a context such as '1!{X->[X-1,X,X+1]}' the result should clearly be '[0,1,2]'.  The rule adopted is that a variable has the scope of the member of the outermost set in which it appears, including all expressions nested within it.

To aid in identifying scopes, the preprocessor uses a 'symbol table', which is list of lists.  Each term of the table represents a scope, and each of a scope's terms gives the translation from an external variable to an internal variable that is valid for that scope.  The first term of the table is for the innermost current scope.

A variable is in scope if either it is defined locally or local to an enclosing term.

 */ in_scope(X,Y,[Locals|_]) :- in_locals(X,Y,Locals),!. /*
 */ in_scope(X,Y,[_|Globals]) :- in_scope(X,Y,Globals),!. /*

Each scope is a list of internal/external pairs.

 */ in_locals(X,Z,[(Y,Z)|_]) :- Y==X,!. /*
 */ in_locals(X,Z,[_|T])     :- in_locals(X,Z,T),!. /*

A variable is preprocessed by translating it into its internal equivalent, if it is already in scope.

 */ preprocess(X,Y,SymTab,SymTab,_) :- var(X),in_scope(X,Y,SymTab),!. /*

An input variable that is not in scope is added to the local symbol table.  It is necessary to use copy_term, otherwise it will remain bound to all other occurences of the same variable in the term.

 */ preprocess(X,Y,[Lcl|Gbl],[[(X,Y)|Lcl]|Gbl],Context):- 
               var(X),!,copy_term(X,Y),display_line(Context),
               write('An undeclared variable was found in an expression.'),nl. /*

 */ display_line(X) :- numbervars(X,1,_),write(X),nl,fail. /*
 */ display_line(_) :- true. /*

The special notations for ranges and shift sequences must be preserved, and caught before they can be confused with ordinary sets.  But before that, we must check that the set or sequence does not consist of a simple variable, which would match anything!

 */ preprocess({H},[H1],SymTab,SymTab,Context):- var(H),!,
               preprocess_term(H,H1,[[]|SymTab],_,Context). /*
 */ preprocess([H],[(1,H1)],SymTab,SymTab,Context):- var(H),!,
               preprocess(H,H1,[[]|SymTab],_,Context). /*
 */ preprocess({M..N},{M1..N1},SymTab,SymTab,Context) :- !,
               preprocess(M,M1,[[]|SymTab],SymTab1,Context),
               preprocess(N,N1,SymTab1,_,Context). /*
 */ preprocess([M..N],[M1..N1],SymTab,SymTab,Context) :- !,
               preprocess(M,M1,[[]|SymTab],SymTab1,Context),
               preprocess(N,N1,SymTab1,_,Context). /*

Sets are represented internally by sorted lists.  Each member of a set creates a new local scope, which is discarded after preprocessing it.

 */ preprocess({},[],SymTab,SymTab,_) :- !. /*
 */ preprocess({H;T},Z,SymTab,SymTab,Context) :- !,
               preprocess_term(H,H1,[[]|SymTab],_,Context),
               preprocess({T},T1,SymTab,_,Context),sort([H1|T1],Z). /*
 */ preprocess({H},[H1],SymTab,SymTab,Context):- !,
               preprocess_term(H,H1,[[]|SymTab],_,Context). /*

Terms are pattern matched to decide if they are generators, constructors or filters.

A variable on its own will almost certainly be already declared.

 */ preprocess_term(X,X1,SymTab,SymTab1,Context) :- var(X),!,
                    preprocess(X,X1,SymTab,SymTab1,Context). /*

A variable with a condition is a filter.

 */ preprocess_term((X:B),(X1:B1),SymTab,SymTab2,Context) :- var(X),!,
                    preprocess_vars(X,X1,SymTab,SymTab1,Context),
                    preprocess(B,B1,SymTab1,SymTab2,Context). /*

Anything with an arrow is a generator.

 */ preprocess_term((X->Y:B),((X1,Y1):B1),SymTab,SymTab3,Context) :- !,
                    preprocess_vars(X,X1,SymTab,SymTab1,Context),
                    preprocess(Y,Y1,SymTab1,SymTab2,Context),
                    preprocess(B,B1,SymTab2,SymTab3,Context). /*
 */ preprocess_term((X->Y),(X1,Y1),SymTab,SymTab2,Context) :- !,
                    preprocess_vars(X,X1,SymTab,SymTab1,Context),
                    preprocess(Y,Y1,SymTab1,SymTab2,Context). /*

The pattern with a condition is a filter.

 */ preprocess_term((X:B),(X1:B1),SymTab,SymTab2,Context) :- !,
                    preprocess_vars(X,X1,SymTab,SymTab1,Context),
                    preprocess(B,B1,SymTab1,SymTab2,Context). /*

Anything else is just a tuple, and should almost certainly include only declared variables.

 */ preprocess_term(X,X1,SymTab,SymTab1,Context) :- 
                    preprocess(X,X1,SymTab,SymTab1,Context). /*

Sequences are represented as sets of pairs and are mappings from 1-n onto their terms.

 */ preprocess([],[],SymTab,SymTab,_) :- !. /*
 */ preprocess([H|T],Z,SymTab,SymTab1,Context):- !,
               preprocess_seq(1,[H|T],Z,SymTab,SymTab1,Context). /*

 */ preprocess_seq(_,[],[],SymTab,SymTab,_)   :- !. /*
 */ preprocess_seq(N,[H|T],[(N,H1)|T1],SymTab,SymTab2,Context):- 
                   preprocess(H,H1,SymTab,SymTab1,Context),
                   N1 is N+1,preprocess_seq(N1,T,T1,SymTab1,SymTab2,Context). /*

Pairs translate to pairs, and '->' is converted to ','.  This takes care of tuples too.

 */ preprocess((X,Y),(X1,Y1),SymTab,SymTab2,Context) :- !,
               preprocess(X,X1,SymTab,SymTab1,Context),
               preprocess(Y,Y1,SymTab1,SymTab2,Context). /*
 */ preprocess(((X->Y)),(X1,Y1),SymTab,SymTab2,Context) :- !,
               preprocess(X,X1,SymTab,SymTab1,Context),
               preprocess(Y,Y1,SymTab1,SymTab2,Context). /*

An atom or integer denotes itself.

 */ preprocess(X,X,SymTab,SymTab,_) :- atomic(X),!. /*

Comparison operators are given special treatment.  Alternative operators need to be converted to a common form.  The predicate 'comparison(C,X,R,Y)' succeeds if C is a comparison, setting X to the left operand, R to the normalised relation, and Y to the right operand.

 */ comparison(C,_,_,_)  :- var(C),!,fail. /*
 */ comparison(X<Y,X,<,Y)  :- !. /*
 */ comparison(X=<Y,X,=<,Y) :- !. /*
 */ comparison(X\>Y,X,=<,Y) :- !. /*
 */ comparison(X>=Y,X,>=,Y) :- !. /*
 */ comparison(X\<Y,X,>=,Y) :- !. /*
 */ comparison(X>Y,X,>,Y)  :- !. /*
 */ comparison(X=Y,X,=,Y)  :- !. /*
 */ comparison(X\=Y,X,\=,Y) :- !. /*
 */ comparison(X subset Y,X,subset,Y) :- !. /*
 */ comparison(X inside Y,X,inside,Y) :- !. /*
 */ comparison(X encloses Y,X,encloses,Y) :- !. /*
 */ comparison(X includes Y,X,includes,Y) :- !. /*
 */ comparison(X disjoint Y,X,disjoint,Y) :- !. /*
 */ comparison(X equal Y,X,equal,Y) :- !. /*
 */ comparison(X unequal Y,X,unequal,Y) :- !. /*

Shorthands such as X<Y<Z must be expanded to X<Y&Y<Z.  After decomposing a comparison, 'preprocess_comparison' is called to check if the right operand is also a comparison.  If it is, it is preprocessed recursively, then linked to the first comparison by '&'.  In any case, the left and right operands of the comparison are preprocessed, then combined with the normalised relation.

 */ preprocess(C,C1,SymTab,SymTab1,Context) :- comparison(C,X,R,Y),!,
               preprocess_comparison(X,R,Y,C1,SymTab,SymTab1,Context). /*

 */ preprocess_comparison(X,R,Y,T1 & T2,SymTab,SymTab3,Context) :- 
                          comparison(Y,X2,_,_),!,
                          preprocess(X,X1,SymTab,SymTab1,Context),
                          preprocess(X2,X3,SymTab1,SymTab2,Context),T1=..[R,X1,X3],
                          preprocess(Y,T2,SymTab2,SymTab3,Context). /*
 */ preprocess_comparison(X,R,Y,T1,SymTab,SymTab2,Context) :- 
                          preprocess(X,X1,SymTab,SymTab1,Context),
                          preprocess(Y,Y1,SymTab1,SymTab2,Context),T1=..[R,X1,Y1]. /*

Any other function is processed by operating on its operands recursively.

 */ preprocess(X,Y,SymTab,SymTab1,Context) :- compound(X),!,
               X =.. [F|A],preprocess_args(A,A1,SymTab,SymTab1,Context),Y =..[F|A1]. /*

 */ preprocess_args([],[],SymTab,SymTab,_). /*
 */ preprocess_args([H|T],[H1|T1],SymTab,SymTab2,Context) :- 
                    preprocess(H,H1,SymTab,SymTab1,Context),
                    preprocess_args(T,T1,SymTab1,SymTab2,Context). /*

If the preprocessor is working correctly, no other case needs to be allowed for.

 */ preprocess(X,X,SymTab,SymTab,Context) :- write('Bug: '),nl,
               write(preprocess(X,X,SymTab,SymTab,Context)),nl. /*

Within 'preprocess_vars' we expect a pattern of tuples of variables, and nothing else.

It is OK if the variable has already been declared locally.

 */ preprocess_vars(X,Y,SymTab,SymTab,_) :- var(X),in_locals(X,Y,SymTab),!. /*

It is bad news if the variable has already been declared globally.

 */ preprocess_vars(X,Y,SymTab,SymTab,Context) :- 
                    var(X),in_scope(X,Y,SymTab),!,display_line(Context),
                    write('An argument is already declared in an enclosing context.'),
                    nl. /*

An input variable that is not in scope is added to the local symbol table.  It is necessary to use copy_term, otherwise it will remain bound to all other occurences of the same variable in the term.

 */ preprocess_vars(X,Y,[Lcl|Gbl],[[(X,Y)|Lcl]|Gbl],_):- var(X),!,copy_term(X,Y). /*

Pairs translate to pairs.  This takes care of tuples too.

 */ preprocess_vars((X,Y),(X1,Y1),SymTab,SymTab2,Context) :- !,
                     preprocess_vars(X,X1,SymTab,SymTab1,Context),
                     preprocess_vars(Y,Y1,SymTab1,SymTab2,Context). /*

An atom or integer denotes itself.

 */ preprocess_vars(X,X,SymTab,SymTab,_) :- atomic(X),!. /*

It is an error for any other function to be present.  It is processed by operating on its operands recursively.  

 */ preprocess_vars(X,Y,SymTab,SymTab1,Context) :- compound(X),!,
                     display_line(Context),X =.. [F|L],write('A '''),write(F),
                     write(''' operation appears in an argument pattern.'),nl,
                     list_to_tuple(L,A),
                     preprocess_vars(A,A1,SymTab,SymTab1,Context),
                     tuple_to_list(A1,L1),Y =..[F|L1]. /*

End of literate program. */
