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

module substitution.
  
  accumulate abstract_syntax.
  
  %%% ``free_in S M'' succeeds if S is free 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 M R'' succeeds if R is the result
  %%% of substituting N for the free occurrences of X in M.
  substitute N X (var X) N :- !.
  substitute N X (var Y) (var Y).
  
  substitute N X (ap Operator Operand) (ap Operator1 Operand1) :-
  	substitute N X Operator Operator1,
  	substitute N X Operand Operand1.
  
  substitute N X (lambda X Body) (lambda X Body) :- !.
  substitute N X (lambda Y Body) (lambda Y Body1) :-
  	(not(free_in Y N) ; not(free_in X Body)),
  	!,
  	substitute N X Body Body1.
  substitute N X (lambda Y Body) (lambda Y2 Body1) :-
  	fresh Body N Y Y2,
  	substitute (var Y2) Y Body Body2,
  	substitute N X Body2 Body1.
  
  %%%``fresh M N X Y'' succeeds if Y is an identifier formed from
  %%% X that does not occur free in M or N.
  fresh M N X Y :- fresh_aux M N X "" Y, !.
  
  local	fresh_aux	term -> term -> string -> string -> string -> o.
  
  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.