module pf

import StdEnv
import Data.List

:: Expr
	= Lambda Ident Expr
	| Ident Ident
	| Literal Literal
	| (@) infixl Expr Expr

:: Literal
	= LitInt Int
	| LitBool Bool

:: Ident :== String

hasIdent :: Ident Expr -> Bool
hasIdent id (Ident n) = id == n
hasIdent id (Literal _) = False
hasIdent id (Lambda n e) = id <> n && hasIdent id e
hasIdent id (f @ x) = hasIdent id f || hasIdent id x

print :: Expr -> String
print e = foldl (+++) "" (pr False e [])
where
	pr :: Bool Expr [String] -> [String]
	pr p l=:(Lambda _ _) st =
		[if p "(\\" "\\":intersperse " " vars] ++
		[" -> ":pr False rhs [if p ")" "":st]]
	where
		(vars,rhs) = getLambdas l

		getLambdas :: Expr -> ([Ident], Expr)
		getLambdas (Lambda x rhs) = let (is,e) = getLambdas rhs in ([x:is],e)
		getLambdas e = ([], e)

	pr _ (Ident id)  st = [id:st]
	pr _ (Literal l) st = pLit l st
	pr p (f @ x)     st = [if p "(" "":pr False f [" ":pr True x [if p ")" "":st]]]

	pLit :: Literal [String] -> [String]
	pLit (LitInt i)  st = [toString i:st]
	pLit (LitBool b) st = [toString b:st]

optim :: Expr -> Expr
optim (Lambda id e)
| hasIdent id e = case optim e of
	Ident id` -> if (id == id`) (Ident "id") (Ident "const" @ e)
	e=:(f @ x) -> optim (optApp e)
	e -> Lambda id e
| otherwise = Ident "const" @ optim e
where
	optApp :: Expr -> Expr
	optApp (f @ x)
	| hasIdent id f && hasIdent id x = Ident "ap" @ Lambda id f @ Lambda id x
	| otherwise = case moveOutside id (f @ x) of
		a=:(f @ Ident id`) -> if (id == id`) f (Ident "const" @ a)
		a                  -> Ident "const" @ a
optim (Ident "flip" @ Ident "ap" @ Ident "id") = Ident "join"
optim (f @ x) = optim f @ optim x
optim e = e

moveOutside :: Ident Expr -> Expr
moveOutside _ (Ident id) = Ident id
moveOutside _ (Literal l) = Literal l
moveOutside id (f @ x)
| hasIdent id f && hasIdent id x = abort "moveOutside on @ with id in both sides"
| hasIdent id f = case moveOutside id f of
	Ident id -> Ident "flip" @ Ident "id" @ x @ Ident id
	g @ Ident id -> Ident "flip" @ g @ x @ Ident id
| hasIdent id x = case moveOutside id x of
	e=:(Ident id) -> f @ e
	g @ e=:(Ident id) -> Ident "(o)" @ f @ g @ e
moveOutside _ (Lambda x e) = Lambda x e // TODO

Start = map do
	[ Lambda "x" (Literal (LitInt 5))
	, Lambda "x" (Ident "x")
	, Lambda "x" (Ident "y")
	, Lambda "x" (Lambda "y" (Ident "x"))
	, Lambda "x" (Lambda "y" (Ident "y"))
	, Lambda "x" (Lambda "y" (Literal (LitInt 37)))
	, Lambda "x" (Lambda "y" (Lambda "z" (Ident "x")))
	, Lambda "x" (Lambda "y" (Lambda "z" (Ident "y")))
	, Lambda "x" (Lambda "y" (Lambda "z" (Ident "z")))
	, Lambda "x" (Lambda "y" (Lambda "z" (Literal (LitInt 37))))
	, Lambda "x" (Lambda "y" (Ident "x" @ Ident "y"))
	, Lambda "x" (Lambda "y" (Ident "y" @ Ident "x"))
	, Lambda "x" (Lambda "y" (Ident "y" @ Literal (LitInt 10)))
	, Lambda "f" (Lambda "a" (Lambda "b" (Lambda "c" (Lambda "d" (Ident "f" @ Ident "b" @ Ident "c" @ Ident "d" @ Ident "a")))))
	, Lambda "f" (Lambda "x" (Ident "f" @ Ident "x" @ Ident "x"))
	]
where
	do e = (print e, " ==> ", print (optim e), "\n")