-- SIMPLY TYPED LAMBDA CALCULUS TYPECHECKING & REDUCTIONS

-- *******************  data types for simply typed lambda calculus [church]  ********************* --

type TermVar	= String
type TermType	= String

data Lterm		= 	Variable TermVar		-- x 
			|	Application Lterm Lterm		-- M N 
			|	Abstraction TermVar Ltype Lterm	-- lambda x:t.M
	deriving (Show, Read, Eq) 
data Ltype		= SimpleType TermType 		-- t
			| FunctionType Ltype Ltype 	-- t->t'
	deriving (Show, Read, Eq) 

type Bentry  	= (TermVar, Ltype) 
type Basis	= [Bentry]

-- ****************  typeof function: type checker for simply typed lambda calculus  ************** --

typeof :: Basis -> Lterm -> Maybe Ltype
-- simple variable type
typeof basis (Variable var) =
			lookup var basis 
-- application type
typeof basis (Application m n) = 
			case typeof basis m of
				Nothing 			-> Nothing
				Just (SimpleType x)	 	-> Nothing
				Just (FunctionType x y) 	-> 
						if typeof basis n == Just x then 
							Just y
						else 
							Nothing
-- abstraction type
typeof basis (Abstraction x t y) =
			case typeof ((x,t) : basis) y of
				Nothing		-> Nothing
				Just z		-> Just (FunctionType t z)

-- ***********************  ->b reductions for simply typed lambda calculus  ********************** --

-- free variables
free :: Lterm -> [TermVar]
free (Variable x) 		= [x]
free (Application l1 l2) 	= (free l1) ++ (free l2)
free (Abstraction x t y)	= [a | a<-free y, a /= x]
--					filter (\z -> z /= x) (free y) 

newPar :: TermVar->[TermVar]->TermVar
newPar par x 			= if ([a | a<-x, a==par] == []) then
				-- if not (par `elem` x) then
					par
				  else 
				  	newPar (par ++ "'") x
					
newVar :: TermVar->[TermVar]->Lterm
newVar par x = Variable (newPar par x)
				  	

-- subst expr1, var, expr2 --> expr means in lambda calculus: expr1[var ::= expr2]
subst :: Lterm->TermVar->Lterm->Lterm
subst (Variable x) x1 as = if x==x1 then as else Variable x
subst (Application l1 l2) par as = Application (subst l1 par as) (subst l2 par as)
subst (Abstraction x t y) par as = 
			if (x `elem` free as) then
--				let z = newPar x (free as ++ free y)
--				in Abstraction z t (subst (subst y x (Variable z)) par as)
				Abstraction (newPar x (free as ++ free y)) t (subst (subst y x (newVar x (free as ++ free y))) par as)
			else
				Abstraction x t (subst y par as)


-- ->b reductions based on substitution
reduce1 :: Lterm->Lterm
reduce1 (Application (Abstraction x t y) l) = subst y x l

-- others reduce to themselves

reduce1 (Application l1 l2) = 
		Application (reduce1 l1) (reduce1 l2)

reduce1 (Abstraction x t y) = 
	Abstraction x t (reduce1 y)

reduce1 x = x

reduce :: Lterm -> Lterm
reduce l =
		let l' = reduce1 l
		in if l == l' then
			l
		   else 
			reduce l'


sqrt :: Int -> Int
sqrt n = let f :: Int -> Int 
             f y = if (y*y <= n) && (y+1)*(y+1) > n then
                      y
		   else 
		      f (y+1)
         in f 0