%%% substitution for the lambda calculus
%%%
%%% AUTHOR: Gary T. Leavens

%%% #load "abstract_syntax.mod", "substitution.mod".
%%% #query abstract_syntax, substitution.

module substitution.

import abstract_syntax.

type	free_in		string -> term -> o.
%%% ``free_in S M'' succeeds if S is free in M.

type fresh		term -> term -> string -> string -> o.
%%%``fresh M N X Y'' succeeds if Y is an identifier formed from
%%% X that does not occur free in M or N.

type substitute 	term -> string -> term -> term -> o.
%%% ``substitute N X M R'' succeeds if R is the result
%%% of substituting N for the free occurrences of X in M.


free_in X (var X).
free_in X (ap Operator Operand) :-
	free_in X Operator ; free_in X Operand.
free_in X (lambda Y Body) :-
	not(X = Y), 
	free_in X Body.

substitute N X (var X) N :- !.
substitute N X (var Y) (var Y).

substitute N X (ap Operator Operand) (ap Operator' Operand') :-
	substitute N X Operator Operator',
	substitute N X Operand Operand'.

substitute N X (lambda X Body) (lambda X Body) :- !.
substitute N X (lambda Y Body) (lambda Y Body') :-
	(not(free_in Y N) ; not(free_in X Body)),
	!,
	substitute N X Body Body'.
substitute N X (lambda Y Body) (lambda Y' Body') :-
	fresh Body N Y Y',
	substitute (var Y') Y Body Body'',
	substitute N X Body'' Body'.


type	fresh_aux	term -> term -> string -> string -> string -> o.

fresh M N X Y :- fresh_aux M N X "" Y, !.
fresh_aux M N X S Y :-
	Y is X ^ S,  % Y is the concatenation of X and S
	not(free_in Y M),
	not(free_in Y N).
fresh_aux M N X S Y :-
	S2 is S ^ "'",
	fresh_aux M N X S2 Y.