module Expr where 

import Types 
import Subst
import List (sort, nub)
import Maybe (fromJust)


data Binding = Binding String Type 
               deriving (Eq)

instance Show Binding where
  show (Binding n t) = n ++ " :: " ++ show t

bind :: String -> Type -> Binding
bind n t = Binding n t



data Reduction = Reduction Binding Binding Subst Binding



data Expr = Bind Binding | FAppl Expr Expr
            deriving (Show, Eq)

(=:) :: String -> Type -> Expr
n =: t = Bind $ bind n t 
infixr 3 =:

($:) :: Expr -> Expr -> Expr
e1 $: e2 = FAppl e1 e2
infixr 3 $:

(-:) :: Expr -> Expr -> Expr
e1 -: e2 = FAppl e1 e2
infixl 6 -:


efmap :: (Binding -> Binding) -> Expr -> Expr
efmap f (Bind b) = Bind $ f b
efmap f (FAppl e1 e2) = FAppl (efmap f e1) (efmap f e2)


localize :: Expr -> Expr
localize e = efmap (\(Binding n t) -> Binding n $ tfmap (\v -> v ++ ":" ++ n) t) e


normalize :: Expr -> Expr
normalize e = efmap (\(Binding n t) -> Binding n $ tfmap (\v -> fromJust $ lookup v cvars) t) e
  where cvars = zip (evars e) $ map return ['a' .. 'z']
        evars = nub . sort . concatMap (\(Binding n t) -> vars t) . bindings


-- Returns from left to right, perhaps evaluation order would be better?
bindings :: Expr -> [Binding]
bindings (Bind b) = [b]
bindings (FAppl e1 e2) = bindings e1 ++ bindings e2


-- Replace a subexpr by another
replace :: Expr -> Expr -> Expr -> Expr
replace cur find repl | cur == find = repl
replace cur@(Bind b) find repl = cur
replace (FAppl e1 e2) find repl = FAppl (replace e1 find repl) (replace e2 find repl)


replaceRed :: Expr -> Reduction -> Expr
replaceRed cur r@(Reduction b1 b2 s br) = replace cur find repl
  where (find, repl) = (FAppl (Bind b1) (Bind b2), Bind br)


reduce :: Expr -> Maybe Reduction
reduce e@(Bind b) = Nothing
reduce (FAppl (Bind b1@(Binding n (TFunc t1 t2))) (Bind b2@(Binding ns ts))) = Just $ Reduction b1 b2 subst nb
  where nb    = bind (n ++ " " ++ ns) $ apply subst t2
        subst = match t1 ts
reduce (FAppl b@(Bind _) e) = reduce e >>= (\(Reduction b1 b2 s br@(Binding n t)) -> return $ Reduction b1 b2 s (Binding ("(" ++ n ++ ")") t))
reduce (FAppl e b@(Bind _)) = reduce e
reduce (FAppl e1 e2) = reduce e1


reduceAll :: Expr -> Expr
reduceAll e = 
  case reduce e of 
    Nothing -> e
    Just r -> reduceAll . replaceRed e $ r