import System.IO (hFlush, stdout)
import System.IO.Unsafe 
data Lter = Var String | Abs Lter Lter | App Lter Lter
--data DeB = Place Integer | DAbs DeB | DApp DeB DeB


dbugp :: Lter -> String
dbugp term = case term of 
	Var string -> string
	Abs n m    -> "Abs (" ++ (dbugp n) ++ ") (" ++ (dbugp m) ++ ")"
	App n m    -> "App (" ++ (dbugp n) ++ ") (" ++ (dbugp m) ++ ")"

unCurrySugar = True

instance Show Lter where 
	show (Var varstr) = varstr
	show (Abs n m) = if unCurrySugar then (showUncurriedAbs n m True)++")" else
							"(\\"++ (show n) ++ "." ++ (show m) ++ ")"
	--show (App n m) = "(" ++ (show n) ++ " "++ (show m) ++ ")"
	show (App n m) =case m of
		App _ _ ->(show n) ++ " ("++ (show m) ++ ")"  
		_ -> (show n) ++ " " ++ (show m)

showUncurriedAbs :: Lter -> Lter -> Bool -> String
showUncurriedAbs var expr firstcall = 
	if firstcall then 
		case expr of 
			Var varstr -> "(\\" ++ (show var) ++ "." ++ varstr 
			appterm@(App n m) -> "(\\" ++ (show var) ++ "." ++ (show appterm)
			Abs n m -> "(\\" ++ (show var) ++ (showUncurriedAbs n m False)
	else
		case expr of  
			Var varstr -> " " ++ (show var) ++ "." ++ varstr
			appterm@(App n m) -> " " ++ (show var) ++ "." ++ (show appterm)
			Abs n m -> " " ++ (show var) ++ (showUncurriedAbs n m False)

parseString instr
	| isVar strin = Var strin
	| isAbs strin = foldr Abs 
		(Abs (Var (last splitAbsParams)) (parseString (last splitAbs)))
		(map Var (init splitAbsParams))
	| isApp strin = foldl App (head splitApp) (tail splitApp)
	| otherwise = Var "SOMETHING WENT WRONG"
		where	
			strin = (trimSpaces .stripClosingBrackets . trimSpaces) instr
			splitApp = map parseString (splitByBreakChar strin ' ')
			splitAbs = splitByBreakChar (tail strin) '.'
			splitAbsParams = splitByBreakChar (head splitAbs) ' '


trimSpaces' :: String -> String
trimSpaces' [] = []
trimSpaces' [x] = if x == ' ' then [] else [x]
trimSpaces' (n:xs)	
	| n == '\\' && head xs == ' ' = '.':(trimSpaces' $ tail xs)
	| n == '.' && head xs == ' ' = '.':(trimSpaces' $ tail xs)
	| n == ' ' && head xs == ' ' = trimSpaces' xs
	| otherwise =  n:(trimSpaces' xs)
trimSpaces x = trimSpaces' (dropWhile (==' ') x)

listSlice :: [a] -> Int -> Int -> [a]
listSlice a start end = drop (start) (take (end) a)

getAppParambreaks :: String -> Integer -> [Integer] -> Integer  -> Char -> [Integer]
getAppParambreaks [] bOffset listofBreaks index breakChar = (reverse listofBreaks)
getAppParambreaks (x:xs) bOffset listofBreaks index breakChar
	| x == '(' = getAppParambreaks xs (bOffset+1) listofBreaks (index+1) breakChar
	| x == ')' = getAppParambreaks xs (bOffset-1) listofBreaks (index+1) breakChar
	| x == breakChar && bOffset == 0 = getAppParambreaks xs 0 (index:listofBreaks) (index+1) breakChar
	| otherwise = getAppParambreaks xs bOffset listofBreaks (index+1) breakChar

splitByBreaks' :: String -> [Integer] -> [String] -> String -> Integer -> [String]
splitByBreaks' [] listofBreaks endList working index = reverse (working:endList)
splitByBreaks' (x:xs) listofBreaks endList working index
	| index `elem` listofBreaks = splitByBreaks' xs listofBreaks (working:endList) "" (index+1)
	| otherwise = splitByBreaks' xs listofBreaks endList (working ++ [x]) (index+1)

splitByBreaks :: String -> [Integer] ->  [String]
splitByBreaks instr listofBreaks = splitByBreaks' instr listofBreaks [] "" 0

splitByBreakChar :: String -> Char -> [String]
splitByBreakChar instr breakChar = splitByBreaks instr breaks
		where breaks = getAppParambreaks instr 0 [] 0 breakChar

isVar :: String -> Bool
isVar ('\\':xs) = False
isVar instr = if ((' ' `elem` instr) || ('(' `elem` instr) || 
	(')' `elem` instr)) then False else True

isAbs :: String -> Bool
isAbs (x:xs) = x == '\\'

isApp' :: String -> Integer -> Bool
isApp' [] outerBracketOffSet = False
isApp' (x:xs) outerBracketOffSet = -- If outerbracketOffSet>0 then we're inside a bracket
	case x of                      --  and that is a whole other level (\x.f x) is not an
		'(' -> isApp' xs (outerBracketOffSet+1)
		')' -> isApp' xs (outerBracketOffSet-1)
		' ' -> if outerBracketOffSet == 0 then True else isApp' xs (outerBracketOffSet)
		_ -> isApp' xs outerBracketOffSet
isApp instr = isApp' instr 0

stripClosingBrackets :: String -> String -- if instr is "(<validexpr>)"
stripClosingBrackets instr = if ((head instr) =='(') && (last instr == ')') 
	&& validBrackets stripped then (stripClosingBrackets stripped) else instr
		where stripped =  drop 1 (take ((length instr)-1) instr)


validBrackets' :: String -> Integer -> Bool
validBrackets' [] x = x == 0
validBrackets' (x:xs) outerBracketOffSet = if outerBracketOffSet<0 then False else
	 case x of                      
		'(' -> validBrackets' xs (outerBracketOffSet+1)
		')' -> validBrackets' xs (outerBracketOffSet-1)
		_ -> validBrackets' xs outerBracketOffSet
validBrackets instr = validBrackets' instr 0





{--rmDups :: Eq a => [a] -> [a]
rmDups [] = []
rmDups (x:xs) 
	| x `elem` xs = rmDups xs
	| otherwise = x:(rmDups xs) --}
rmDups a = a
freeVars :: Lter -> [String]
freeVars term = case term of 
	Var varstr -> [varstr]
	Abs var expr -> rmDups (removeAll (show var) (freeVars expr))
		where removeAll el lis = [n | n <- lis, n /= el]
	App n m -> rmDups ((freeVars n) ++ (freeVars m))

allVars :: Lter -> [String]
allVars term = case term of 
	Var varstr -> [varstr]
	Abs var expr -> rmDups ( (allVars var) ++ (allVars expr) )
	App n m -> rmDups ( (allVars n) ++ (allVars m) ) 


findNewVar :: [String] -> String
findNewVar varlist =
	if tryAlphaBet /= [] then (head tryAlphaBet)
	else head ["x"++ (show n) | n <- [0..], not (("x"++ (show n)) `elem` varlist)]
		where tryAlphaBet = [[x] | x <- ['a'..'z'], not ([x] `elem` varlist)]
	
subst' term var substitute origAllVars = 
	case term of
	(Var p) -> if p == varstring then substitute else term
		where 
			Var varstring = var
	(App n m) -> App (subst' n var substitute origAllVars) (subst' m var substitute origAllVars)
	(Abs x expr) -> 
		if xstring == varstring then 
			term
		else (
			if not (xstring `elem` (freeVars substitute)) then 
				Abs x (subst' expr var substitute origAllVars)
			else 
				let newArrStr = findNewVar origAllVars
				in Abs (Var newArrStr) (subst' (subst' expr x (Var newArrStr) (newArrStr:origAllVars)) var substitute (newArrStr:origAllVars))
		) where 
			Var xstring = x
			Var varstring = var


subst term var substitute = subst' term var substitute ((allVars term) ++ (allVars) var ++ (allVars substitute))

reduce' :: Lter -> [String] -> [Lter] -> Lter -- normal order
reduce' term origAllVars prevTerms = case term of 
	Var vars -> term
	Abs n m  -> carryOnReducing 
		(Abs (reduce' n origAllVars []) (reduce' m origAllVars []) ) prevTerms origAllVars 
	App f x  -> case f of
		Var vark -> carryOnReducing 
			(App f (reduce' x  origAllVars [])) prevTerms origAllVars
		App k p -> carryOnReducing
			(App (reduce' f origAllVars []) (reduce' x origAllVars [])) prevTerms origAllVars
		Abs var func -> 
			let substituted = subst' func var x origAllVars in
			carryOnReducing substituted prevTerms (origAllVars ++ allVars substituted)

carryOnReducing :: Lter -> [Lter] -> [String] -> Lter
carryOnReducing newTerm prevTerms origAllVars = 
	if not (null [n | n <- prevTerms, alphaEq newTerm n]) then 
		newTerm
	else reduce' newTerm  origAllVars (newTerm:prevTerms) 

	

{--alphaEq :: Lter -> Lter -> Bool
alphaEq t1 t2 = case t1 of 
	App v1 f1 -> 
		case t2 of 
			App v2 f2 -> (alphaEq v1 v2) && (alphaEq f1 f2)
			_ -> False
	Var varstr ->
		case t2 of
			Var varstr2 -> varstr == varstr2
			_ -> False
	Abs d1 f1 ->
		case t2 of -- \d1.f1 = \d2.f2 <=> f1[d1:=z] = f2[d2:=z]
			Abs d2 f2 -> let newVarStr = findNewVar ((allVars t1) ++ (allVars t2)) in
				alphaEq (subst f1 d1 (Var newVarStr)) (subst f2 d2 (Var newVarStr))
			_ -> False
--}


--This is very broken - cant handle free variables
alphaEq' n m nvars mvars = case n of
	App n1 n2 -> case m of
		App m1 m2 -> (alphaEq' n1 m1 nvars mvars) && (alphaEq' n2 m2 nvars mvars)
		_ -> False
	Abs n1 n2 -> case m of
		Abs m1 m2 -> (alphaEq' n2 m2 (n1s:nvars) (m1s:mvars)) where Var m1s = m1
		_ -> False
			
		where Var n1s = n1

	Var ns -> case m of
		Var ms -> firstinN == firstinM where firstinM = findFirstIndexOf mvars ms
		_ -> False
			
		where firstinN = findFirstIndexOf nvars ns
				

alphaEq n m = alphaEq' n m [] []
findFirstIndexOf :: [String] -> String -> Int 
{--findFirstIndexOf xvars var= if not (null listOfIndexes) then head listOfIndexes else -1
	where listOfIndexes = [index | (index, xvarstring) <- zip [0..] xvars, xvarstring == var ]
--}
findFirstIndexOf' :: [String] -> String -> Int -> Int
findFirstIndexOf' [] var index = -1
findFirstIndexOf' (x:xs) var index = if x==var then index else findFirstIndexOf' xs var (index+1)

findFirstIndexOf varlist var = findFirstIndexOf' varlist var 0
reduce :: Lter -> Lter
reduce term = reduce' term (allVars term) []

genNum num =Abs (Var "f") (Abs (Var "x") ((iterate (App (Var "f")) (Var "x"))!! (num)))


readAsCNumApp :: String -> String -> Lter -> Integer
readAsCNumApp fname xname func = case func of
	App j k -> 
		if jstring /= fname then -1 
		else 
			if restInt /= -1 then 1+restInt
			else -1
		where
			Var jstring = j
			restInt = (readAsCNumApp fname xname k)

	Var k -> if k == xname then 0 else -1
	_ -> -1

readAsCNum :: Lter -> String
readAsCNum term = case term of
	Abs f j -> case j of
		Abs x func -> 
			if parsedApp == -1 then "Not a Church Numeral" else show parsedApp
				where parsedApp = readAsCNumApp (show f) (show x) func
		_ -> "Not a Church Numeral"
	_ -> "Not a Church numeral"

readAndSubstitute instr macroes = substFold lamterm macroes
	where
		lamterm = parseString instr

parseCommand macroes = do
	putStr ">>> "
	hFlush stdout
	lineStr <- getLine 
	let 
		splitted = (splitByBreakChar  lineStr ':')
		macName = trimSpaces ( head splitted)
		macTerm = trimSpaces (drop 1 (last splitted))
		lamterm = parseString lineStr
		substdterm =  substFold lamterm macroes
		fileName = (drop ((length ":loadFile ")) lineStr)
	if lineStr == "" then do return ()
	else
		if ':' == (head lineStr) then
			if (take (length ":readAsCNum") lineStr ) == ":readAsCNum" then do
				putStrLn $ readAsCNum (readAndSubstitute (drop ((length ":readAsCNum")) lineStr) macroes)
				parseCommand macroes
			else
			if (take (length ":loadFile") lineStr) == ":loadFile" then do 
				
				putStrLn $ "Loaded file" ++ fileName
				parseCommand ((readMacroFile fileName) ++ macroes )
			else parseCommand macroes
		else
				if ':' `elem` lineStr then
					parseCommand (addToMacroes (macName, readAndSubstitute macTerm macroes) macroes)
					--((macName, parseString macTerm):macroes)
				else do
					putStrLn . show $ (reduce substdterm)
					parseCommand macroes

addToMacroes :: (String, Lter) -> [(String, Lter)] -> [(String, Lter)]
addToMacroes macro [] = [macro]
addToMacroes macro@(macName,macTerm) (x@(omacName,omacTerm):xs) =
	if macName == omacName then addToMacroes macro xs
	else (x:(addToMacroes macro xs))

substFold' lamterm [] origMacs = if not (null macsInlamterm) 
	then substFold' lamterm macsInlamterm origMacs 
	else lamterm
	where macsInlamterm = 
		[mac | lamtermstring <- allVars lamterm, mac@(macString,_) <- origMacs, lamtermstring == macString]
substFold' lamterm ((macName,macTerm):macroes) origMacs = 
	substFold' (subst lamterm (parseString macName) macTerm) macroes origMacs


substFold lamterm macroes = substFold' lamterm usedMacs macroes
	where usedMacs = [mac | 
		lamtermvar <- allVars lamterm, mac@(macString,_) <- macroes, lamtermvar == macString]


readMacroFile :: String -> [(String,Lter)]
readMacroFile filename = readMacroLines (lines (unsafePerformIO . readFile $ filename))

readMacroLines :: [String] -> [(String,Lter)]
readMacroLines [] = []
readMacroLines (xline:xs) = (lineToMacro xline) ++ (readMacroLines xs)


lineToMacro :: String -> [(String,Lter)]
lineToMacro line = if ':' `elem` line then [(macName, parseString macTerm)] else []
	where
		splitted = (splitByBreakChar  line ':')
		macName = trimSpaces ( head splitted)
		macTerm = trimSpaces (drop 1 (last splitted))

main = do
	parseCommand (readMacroFile "macrolist.txt")
{-
main = do
	let test =" (\\u.u)"
	--putStrLn . dbugp $ test
	putStrLn . show $ parseString test
-}
{-main = do
		let x = Var "x"
		let y= Var "y"
		let f = Var "f"
		let n = Var "n"
		let m = Var "m"
		let z= Var "z"
		let one = Abs f (Abs x (App f x))
		let two = Abs f (Abs x (App f (App f x)))
		let e = App (Abs x (App y z)) (App (App n f) x)
		let nter = App (App n f) x
		let add = Abs m (Abs n (Abs f (Abs x 
			(App (App m f) nter)
			)))
		let mult = Abs m (Abs n (Abs f (App m (App n f))))
		let suc =Abs n (Abs f (Abs x ( App f (App (App n f) x))))
		let test = App (App mult (genNum 5)) two
		let test2 = App (Abs x (App x n)) (Abs y y)
		let test3 = parseString "\\m n f x.m f (n f x)"
		--putStrLn . show $ Abs (Var "u") (Var "u")
		putStrLn . show  $ trimSpaces "\\t n f x. t f (n f x)"
		putStrLn . show $ alphaEq add test3
-}
