Sub.lam

module Sub 

import Lambda
import LambdaCore
import LamTranslator
import Encode

-- LAMSUB
-- lambda calculus equivalent of sub

lamsub = #y #lamsubrec;

lamsubrec = Lf.Lm.Lvar.Lterm. #lamguard 
				(#pr term (#pr var (#pr m (#pr f #nil))))
				(#pr (#pr #matchvar #varaction) (#pr (#pr #matchapp #appaction) (#pr (#pr #matchlam #lamaction) #nil)));

-- GUARDS
-- general case statement which allows for a boolean expression to
-- be in the pattern expression
-- applies subject (i) to the callback in the sequence (ps)
lamguard = #y (Lf.Li.Lps.((#frst (#car ps)) i) 
			((#scnd (#car ps)) i) 
			(f i (#cdr ps)));

-- ENCODING INFORMATION

-- Lam = 1
-- App = 2
-- Var = 3

-- Variable names in the term are labelled starting with the 
-- number 0

-- EXTRACTORS
-- extracts a value from an encoded "constructor"

-- extracts x of (Var x)
extractv = #scnd;

-- extracts x of (Lam x e)
extractlname = Llam. #frst (#scnd lam);

-- extracts e of (Lam x e)
extractlexp = Llam. #scnd (#scnd lam);

-- extracts e1 of (App e1 e2)
extractaone = Lapp. #frst (#scnd app);

-- extracts e2 of (App e1 e2)
extractatwo = Lapp. #scnd (#scnd app);

-- MATCHERS
-- matching functions expect an encoded term
-- each returns a boolean
matchvar = Lterms. #eq #three (#car (#car terms));
matchlam = Lterms. #eq #one (#car (#car terms));
matchapp = Lterms. #eq #two (#car (#car terms));

-- ACTIONS
-- actions expect a list of the form [term, (Var x), m, f]

-- varaction correlates to
-- sub m (Var x) (Var v)
--	| x == v	= m
--	| x /= v	= (Var v)
varaction = Llist. (#eq (#extractv (#car (#cdr list))) (#extractv (#car list))) 
			(#car (#cdr (#cdr list))) 
			(#car list);

-- lamaction correlates to 
-- sub m (Var x) (Lam v e)
--	| x == v	= (Lam v e)
--	| otherwise	= (Lam v (sub m (Var x) e))
lamaction = Llist. (#eq (#extractv (#car (#cdr list))) (#extractlname (#car list))
			(#car list)
			(#pr #one 
			(#pr (#extractlname (#car list)) 
			((#car (#cdr (#cdr (#cdr list)))) 
			(#car (#cdr (#cdr list))) 
			(#car (#cdr list)) 
			(#extractlexp (#car list))))));

-- appaction correlates to
-- 	(App (sub m (Var x) e1) (sub m (Var x) e2))
appaction = Llist. #pr #two 
		(#pr ((#car (#cdr (#cdr (#cdr list)))) 
		      (#car (#cdr (#cdr list)))
		      (#car (#cdr list))
		      (#extractaone (#car list)))
		     ((#car (#cdr (#cdr (#cdr list))))
		      (#car (#cdr (#cdr list)))
		      (#car (#cdr list))
		      (#extractatwo (#car list))));