module PCF where
import LUB
import Exp

data NForm =
	Hnf Int [Exp] | Abst Exp |
	Con Int | Pr NForm | Su NForm | Test NForm Exp Exp deriving Show

normalize :: Exp -> Maybe NForm
normalize e = norm [] e

norm :: [Exp] -> Exp -> Maybe NForm
norm [] Zero = return (Con 0)
norm _ Zero = Nothing
norm xs (Succ t) = norm xs t >>= su
norm xs (Pred t) = norm xs t >>= pr
norm xs (Fix t) = norm xs (subst0 (Fix t) t)
norm xs (App f a) = norm (a:xs) f
norm [] (Lam t) = return(Abst t)
norm (x:xs) (Lam t) = norm xs (subst0 x t)
norm [] (If0 c t e) =
	normalize c >>= (\nf->
		case nf of
			Con 0 -> normalize t
			Con k -> normalize e
			Abst _ -> Nothing
			z -> return (Test z t e))
norm (x:xs) (If0 c t e) =
	norm xs (If0 c (App t x)(App e x))
norm xs (Var k) = return (Hnf k xs)


su (Con x) = return (Con (x+1))
su (Abst _) = Nothing
su x = return (Su x)
pr (Con x) = return (Con (prednat x))
pr (Abst _) = Nothing
pr x = return (Pr x)

prednat n = if n==0 then 0 else (n-1)

evaltoint :: (SelfEmbed a,IntEmbed a) => [a] -> NForm -> Int
evaltoint xs t = a_to_int(evalNF xs t)

evalExp :: (SelfEmbed a,IntEmbed a) => [a] -> Exp -> a
evalExp xs e = evalNF xs (unwrap $ normalize e)

evalNF :: (SelfEmbed a,IntEmbed a) => [a] -> NForm -> a
evalNF xs (Con n) = int_to_a n
evalNF xs (Pr e) = liftInt prednat (evalNF xs e)
evalNF xs (Su e) = liftInt (+1) (evalNF xs e)
evalNF xs (Test c t e) =
    case evaltoint xs c of
        0 -> evalExp xs t
        _ -> evalExp xs e
evalNF xs (Abst e) = lambd(\a->evalExp(a:xs)e)
evalNF xs (Hnf n es) = applyargs (xs!!n) [evalExp xs e|e<-es]

applyargs :: SelfEmbed a => a -> [a] -> a
applyargs v [] = v
applyargs v (e:es) = applyargs (apply v e) es

unwrap (Just x) = x
unwrap Nothing = error "type violation"

liftInt :: IntEmbed a => (Int->Int) -> (a->a)
liftInt = a_to_int --> int_to_a

class Run t where interpret :: Exp -> t
instance Run Int where interpret = evalExp []

instance (LUB a b c,Full c d) => Run(a->b) where
    interpret e a = (p1.p2)(evalExp [(e2.e1) a] (expand e))
                    where e1 = embed :: a->c
                          e2 = embed :: c->d
                          p2 = project :: d->c
                          p1 = project :: c->b

binary :: Exp -> Int -> Int -> Int
binary e a b = interpret e a b

unary :: Exp -> Int -> Int
unary e a = interpret e a

importBinary :: Exp -> (Int->Int->Int) -> Int -> Int
importBinary e a b = interpret e a b

importBinary1 :: Exp -> (Int->Int->Int)  -> Int
importBinary1 e a = interpret e a

importBinary2 :: Exp -> (Int->Int->Int) -> Int -> Int -> Int
importBinary2 e a b c = interpret e a b c
{- e.g. importBinary2 factSchema (*) 1 7 -}

importUnary0 :: Exp -> (Int->Int) -> Int
importUnary0 e f = interpret e f

importUnary1 :: Exp -> (Int->Int) -> Int -> Int
importUnary1 e f n = interpret e f n
importUnary1b :: Exp -> Int -> (Int->Int) -> Int
importUnary1b e f n = interpret e f n

importUnary2 :: Exp -> (Int->Int) -> (Int->Int) ->Int
importUnary2 e f g = interpret e f g