> {-# OPTIONS_GHC -fglasgow-exts #-}

> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env,
>                       eval_nf_without, eval_nf_limit,
>                       tidyNames) where

> import Ivor.TTCore
> import Ivor.Gadgets
> import Ivor.Constant
> import Ivor.Values

> import Debug.Trace
> import Data.Typeable
> import Control.Monad.State
> import List
> import qualified Data.Map as Map

 data Machine = Machine { term :: (TT Name),
                          mstack :: [TT Name],
                          menv :: [(Name, Binder (TT Name))] }

> eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name
> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing Nothing)
>                              in finalise (Ind res)

> eval_nf :: Gamma Name -> Indexed Name -> Indexed Name
> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing Nothing)
>                            in finalise (Ind res)

 eval_nf gam (Ind tm) = Ind (evaluate True gam tm Nothing Nothing Nothing)

> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
> eval_nf_env env g t
>     = eval_nf (addenv env g) t
>   where addenv [] g = g
>         addenv ((n,B (Let v) ty):xs) (Gam g)
>             = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
>         addenv (_:xs) g = addenv xs g

> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
> eval_nf_without gam tm [] = eval_nf gam tm
> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing Nothing)
>                                       in finalise (Ind res)

> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> 
>                  Maybe [(Name, ([Int], Int))] -> Indexed Name
> eval_nf_limit gam tm [] stat = eval_nf gam tm
> eval_nf_limit gam (Ind tm) ns stat 
>     = -- trace (show (tm, stat)) $
>       let res = makePs (evaluate True gam tm Nothing (Just ns) stat)
>           in finalise (Ind res)

> type SEnv = [(Name, TT Name, TT Name)]
> type StackEntry = (TT Name, SEnv, [(Name, TT Name)])
> type Stack = [StackEntry]

> getEnv i env = (\ (_,_,val) -> val) (traceIndex env i "Evaluator fail")
> sfst (n,_,_) = n
> senv (_,e,_) = e
> stkpats (_,_,p) = p

> allNames :: Stack -> SEnv -> [(Name, TT Name)] -> [Name]
> allNames stk env pats = map sfst env ++ map fst pats ++
>                         concat (map (map sfst) (map senv stk)) ++
>                         concat (map (map fst) (map stkpats stk))

Code			Stack	Env	Result

[[x{global}]]		xs	es	(lookup x), xs, es
[[x{local}]]		xs	es	(es!!x), xs, es
[[f a]]			xs	es	[[f]], a:xs, es
[[\x . e]]		(x:xs)	es	[[e]], xs, (x:es)
[[\x . e]]		[]	es	\x . [[e]], xs, (Lam x: es)
(or leave alone for whnf)
[[let x = t in e]]	xs	es	[[e]], xs, (Let x t: es)

> type EvalState = (Maybe [(Name, Int)], 
>                   Maybe [(Name, ([Int], Int))],
>                   Int)

> evaluate :: Bool -> -- under binders? 'False' gives WHNF
>             Gamma Name -> TT Name -> 
>             Maybe [Name] ->  -- Names not to reduce
>             Maybe [(Name, Int)] -> -- Names to reduce a maximum number
>             Maybe [(Name, ([Int], Int))] -> -- Names and list of static args
>             TT Name
> evaluate open gam tm jns maxns statics = -- trace ("EVALUATING: " ++ debugTT tm) $ 
>                                  let res = evalState (eval (True, True) tm [] [] []) (maxns, statics, 0)
>                                      in {- trace ("RESULT: " ++ debugTT res) -}
>                                         res
>   where
>     eval :: (Bool, Bool) -> TT Name -> Stack -> SEnv -> 
>             [(Name, TT Name)] -> State EvalState (TT Name)
>     eval nms@(ev,top) tm stk env pats = -- trace (show (tm, stk, env, pats)) $
>           {-# SCC "eval" #-} do eval' nms tm stk env pats
>                                {- if (ev && top && null stk && tm'/=tm)
>                                   then eval nms tm' [] env pats
>                                   else return tm' -}
>                                

>     eval' (everything, top) (P x) xs env pats 
>         = {-# SCC "evalptop" #-} do
>              (mns, sts, tmp) <- {-# SCC "evalpget" #-} get
>              let (use, mns', sts') = {-# SCC "evalpif" #-}
>                      if (everything || top)
>                         then {-# SCC "usename" #-} usename x jns mns (sts, (xs, pats))
>                         else (False, mns, sts)
>              {-# SCC "evalPput" #-} put (mns', sts, tmp)
>              -- when (not nms) (trace ("Not using " ++ show x) (return ()))
>              case {-# SCC "evalPlookup" #-} lookup x pats of
>                 Nothing -> if use && (everything || top)
>                                 then {-# SCC "evalptop" #-} evalP (everything, top) x (lookupval x gam) xs env pats
>                                 else {-# SCC "evalptop" #-} evalP (everything, top) x Nothing xs env pats
>                 Just val -> eval (everything, False) val xs env (removep x pats)
>        where removep n [] = []
>              removep n ((x,t):xs) | n==x = removep n xs
>                                   | otherwise = (x,t):(removep n xs)
>     eval' nms@(ev,_) (V i) xs env pats 
>              = {-# SCC "evalVtoplevel" #-}
>                if (length env>i) 
>                   then eval nms (getEnv i env) xs env pats
>                   else unload ev (V i) xs pats env -- blocked, so unload
>     eval' nms (App f a) xs env pats 
>        = do -- a' <- eval a [] env pats
>             eval nms f ((a, env, pats):xs) env pats
>     eval' nms (Bind n (B Lambda ty) (Sc sc)) xs env pats
>        = do ty' <- eval nms ty [] env pats
>             {-# SCC "evalscope" #-} evalScope nms Lambda n ty' sc xs env pats
>     eval' nms (Bind n (B Pi ty) (Sc sc)) xs env pats
>        = do ty' <- eval nms ty [] env pats
>             {-# SCC "evalscope" #-} evalScope nms Pi n ty' sc xs env pats
>            -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env
>     eval' nms (Bind n (B (Let val) ty) (Sc sc)) xs env pats 
>        = do val' <- eval nms val [] env pats
>             ty' <- eval nms ty [] env pats
>             eval nms sc xs ((n,ty',val'):env) pats
>     eval' nms@(ev,_) (Bind n (B bt ty) (Sc sc)) xs env pats
>        = do ty' <- eval nms ty [] env pats
>             unload ev (Bind n (B bt ty') (Sc sc)) [] pats env
>     eval' (ev,_) x stk env pats = unload ev x stk pats env

>     evalP (ev, top) n (Just v) xs env pats 
>        = {-# SCC "evalP" #-} case v of
>             Fun opts (Ind v) -> eval (ev, False) v xs env pats
>             PatternDef p@(PMFun arity _) _ _ pc -> 
>                 do ans <- {-# SCC "pmatchc" #-} pmatchC (ev, top) n pc xs env pats
>                    -- ans <- pmatch (ev, top) n p xs env pats
>                    return ans
>             PrimOp _ f -> do xs' <- mapM (\(x, xenv, xpats) -> eval (ev, False) x [] xenv xpats) xs
>                              case f xs' of
>                                Nothing -> unload ev (P n) xs pats env
>                                Just v -> eval (ev, False) v [] env pats
>             _ -> unload ev (P n) xs pats env
>     evalP (ev,top) n Nothing xs env pats = {-# SCC "evalP" #-} unload ev (P n) xs pats env -- blocked, so unload stack

>     evalScope nms b n ty sc stk@((x,xenv,xpats):xs) env pats 
>              = do let n' = uniqify' n (allNames stk env pats)
>                   x' <- eval nms x [] xenv xpats
>                   eval nms sc xs ((n',ty,x'):env) pats
>     evalScope nms@(ev,_) b n ty sc [] env pats
>       | open = do let n' = uniqify' n (allNames [] env pats)
>                   (mns, sts, tmp) <- get
>                   let tmpname = MN ("E",tmp) -- uniqify' (MN ("E", length env)) (allNames [] env pats) -- (MN ("E", length env))
>                   put (mns, sts, tmp+1)
>                   sc' <- eval nms sc [] ((n',ty,P tmpname):env) pats
>                   let newsc = pToV tmpname sc'
>                   u' <- unload ev (Bind n' (B b ty) newsc) [] pats env
>                   --trace ("SCOPE: " ++ show (sc, newsc, env, debugTT u', debugTT (buildenv env u'))) $ 
>                   return $ buildenv env u'
>       | otherwise 
>          = do let n' = uniqify' n (allNames [] env pats)
>               u' <-  unload ev (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf
>               return $ buildenv env u'
>     unload ev x [] pats env 
>                = {-# SCC "unload" #-} return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
>     unload ev x ((a, aenv, apats):as) pats env 
>                = {-# SCC "unload" #-}
>                  do a' <- eval (ev, False) a [] aenv apats
>                     unload ev (App x a') as pats env
>
>     uniqify' u@(UN n) ns = {-# SCC "uniqify'" #-} uniqify (MN (n,0)) ns
>     uniqify' n ns = {-# SCC "uniqify'" #-} uniqify n ns

>     evalStk ev ((a, aenv, apats):as) 
>         = do a' <- eval (ev, True) a [] aenv apats
>              as' <- evalStk ev as
>              return (a':as')
>     evalStk ev [] = return []

>     evalArgs ev ((n, Left (a, aenv, apats)):as) 
>         = do a' <- eval (ev, True) a [] aenv apats
>              as' <- evalArgs ev as
>              return ((n,a'):as')
>     evalArgs ev ((n,Right a'):as) 
>         = do as' <- evalArgs ev as
>              return ((n,a'):as')
>     evalArgs ev [] = return []

     usename x _ mns (sts, (stk, pats)) 
          | Just (static, arity) <- lookup x sts 
              = useDyn x mns static arity stk pats

>     usename x Nothing Nothing (sts, _) = (True, Nothing, sts)
>     usename x _ (Just ys) (sts, _) 
>                 = case lookup x ys of
>                      Just 0 -> (False, Just ys, sts)
>                      Just n -> (True, Just (update x (n-1) ys), sts)
>                      _ -> (True, Just ys, sts)
>     usename x (Just xs) m (sts, _) = (not (elem x xs), m, sts)

     useDyn x mns static arity stk pats =

>     update x v [] = []
>     update x v ((k,_):xs) | x == k = ((x,v):xs)
>     update x v (kv:xs) = kv : update x v xs

>     buildenv [] t = t
>     buildenv ((n,ty,tm):xs) t 
>                 = buildenv xs (subst tm (Sc t))
>     --            = buildenv xs (Bind n (B (Let tm) ty) (Sc t))

>     bindRHS [] rhs = rhs
>     bindRHS ((x,t):xs) rhs = bindRHS xs $ substName x t (Sc rhs)

>     renameRHS pbinds rhs env stk = rrhs [] [] (nub pbinds) rhs where
>       rrhs namemap pbinds' [] rhs = {-trace ("BEFORE " ++ show (rhs, pbinds, pbinds')) $ -}
>                                     (pbinds', substNames namemap rhs)
>       rrhs namemap pbinds ((n,t):ns) rhs
>          = let n' = uniqify' (UN (show n)) (map sfst env ++ 
>                                             map fst pbinds ++ map fst ns ++ 
>                                             concat (map (map sfst) (map senv stk)) ++ 
>                                             concat (map (map fst) (map stkpats stk))) in
>                rrhs ((n,P n'):namemap) ((n',t):pbinds) ns rhs

     substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs
     substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs))

>     pmatch (False, False) n _ xs env pats 
>            = unload False (P n) xs pats env
>     pmatch (ev, top) n (PMFun i clauses) xs env pats = matchtrace (show n) xs $ 
>         do (mns, statics, tmp) <- get
>            let static = fmap (lookup n) statics
>            let rcs = reqCons clauses
>            {- xs' <- zipWithM (\(x, xenv, xpats) reqcon -> 
>                     do x' <- if reqcon then eval (False, True) x [] xenv pats
>                                        else return x     
>                        return (x', xenv, xpats)) xs rcs -}
>            old <- get -- HACK! If it fails, restore old state
>            cm <- matches clauses xs env pats
>            case cm of
>              Nothing -> do put old
>                            unload ev (P n) xs pats env
>              Just (rhs, pbinds, stk) -> 
>                do rhsin <- case static of
>                     -- Just (Just staticargs) -> 
>                        -- do -- mkNewDef n staticargs xs
>                        --    trace ("STATIC: " ++ show (n, staticargs, (map (\(x,y,z) -> x) xs))) $ return rhs 
>                     _ -> return rhs
>                   let rhs' = bindRHS pbinds rhsin 
>                   rhstrace (show n) rhs' []
>                           $ eval (ev, False) rhs' stk env []

>     reqCons [] = repeat False
>     reqCons ((Sch pats _ _):ss) = zipWith (||) (reqCons ss) (rc pats)
>     rc [] = []
>     rc ((PCon _ _ _ _):ps) = True:(rc ps)
>     rc ((PConst _):ps) = True:(rc ps)
>     rc (_:ps) = False:(rc ps)

Careful with matching against catch all cases. If one clause *might* match,
but doesn't because an argument is not in canonical form, then we're stuck,
so better not look further!

>     matches [] xs env pats = return Nothing
>     matches (c:cs) xs env pats
>        = do cm <- match c xs env pats
>             case cm of
>               (Just v, _) -> return $ Just v
>               (Nothing, False) -> matches cs xs env pats
>               (Nothing, True) -> return Nothing -- Stuck due to variable

>     match :: Scheme Name -> Stack -> SEnv -> 
>              [(Name, TT Name)] ->
>              State EvalState 
>                    (Maybe (TT Name, [(Name, TT Name)], Stack), Bool)
>     match (Sch pats _ rhs) xs env patvars 
>               = do r <- matchargs pats xs rhs env patvars []
>                    return r

>     matchargs [] xs (Ind rhs) env patvars pv' 
>                   = return $ (Just (rhs, pv', xs), False)
>     matchargs (p:ps) ((x, xenv, xpats):xs) rhs env patvars pv'
>       = do old <- get
>            x' <- {- trace ("against " ++ show x) $ -} eval (False, True) x [] xenv xpats
>            xm <- matchPat p x' xenv xpats pv' old
>            case xm of
>              (Just patvars', _) -> matchargs ps xs rhs env patvars patvars'

FIXME: We should only get stuck if we have a variable matching against
a pattern (i.e. we've got a potential match) *and* all the rest of the
arguments are matches or potential matches.

If any of the remaining arguments definitely fail to match, we're not
stuck.

>              (Nothing, False) -> do put old
>                                     return (Nothing, False)
>              (Nothing, True) ->
>                  do rest <- matchargs ps xs rhs env patvars pv'
>                     case rest of
>                       (Nothing, False) -> return (Nothing, False)
>                       _ -> return (Nothing, True)

                do xnms' <- eval True x [] xenv xpats
                   trace ("Fully evalled " ++ show (x,xnms')) $ case matchPat p x' pv' of
                     Just patvars' -> matchargs ps xs rhs env patvars patvars'
                     Nothing -> return Nothing

>     matchargs _ _ _ _ _ _ = return (Nothing, False)

>     matchPat PTerm x _ _ patvars old = return $ (Just patvars, False)
>     matchPat (PVar n) x _ _ patvars old
>         = return $ (Just ((n,x):patvars), False) -- (filter (\ (x,y) -> x/=n) patvars))
>     matchPat (PConst t) x xenv xpats patvars old
>              = do x' <- eval (True, True) x [] [] []
>                   case x' of
>                     Const t' -> case cast t of
>                                   Just tc -> 
>                                      if (tc == t') then return $ (Just patvars, False)
>                                                    else return (Nothing, False)
>                     _ -> return (Nothing, False)
>     matchPat pc@(PCon t _ _ args) x xenv xpats patvars old
>              = do -- old <- get
>                   x' <- eval (False, True) x [] xenv xpats
>                   case getConArgs x' [] of
>                     Just (tag, cargs) ->
>                        if (tag == t) then matchPats args cargs patvars
>                                      else return (Nothing, False)
>                     _ -> do put old
>                             x' <- eval (True, True) x [] xenv xpats
>                             case getConArgs x' [] of
>                               Just (tag, cargs) ->
>                                 if (tag == t) then matchPats args cargs patvars
>                                               else return (Nothing, False)

>                               _ -> return (Nothing, True)
>         where matchPats [] [] patvars = return $ (Just patvars, False)
>               matchPats (a:as) (b:bs) patvars
>                   = do vs' <- matchPat a b xenv xpats patvars old
>                        case vs' of
>                          (Just pats, _) -> matchPats as bs pats
>                          x -> return x
>               matchPats _ _ _ = return (Nothing, False)
>     matchPat _ _ _ _ _ _ = return (Nothing, False)

>     getConArgs (Con t _ _) args = Just (t, args)
>     getConArgs (App f a) args = getConArgs f (a:args)
>     getConArgs _ _ = Nothing


Substitution using compiled matches

>     pmatchC top n (args, pc) xs env pats
>         | length xs >= length args
>             = -- trace (show (n, map (\ (x,_,_) -> x) (take arity xs))) $
>               do let stk = take (length args) xs
>                  let rest = drop (length args) xs
>                  -- FIXME: make this lazy so interp fact works again!
>                  -- then lose the annoying extra params
>                  -- then PE might start working, and put the magic here.
>                  argvals' <- {-# SCC "evalstk" #-} evalStk True stk
>                  old <- get
>                  m <- pmSubst n env (zip args (map Right argvals')) pc -- argvals') pc
>                  case m of
>                    Just t -> eval (True,True) t rest env pats
>                    Nothing -> do put old
>                                  unload True (P n) xs pats env
>         | otherwise = unload True (P n) xs pats env

>     substArgNames :: [(Name, Either StackEntry (TT Name))] ->
>                      TT Name -> State EvalState (TT Name)
>     substArgNames args e = do stk' <- evalArgs True (filter (occ e) args)
>                               return $ substNames stk' e

>     occ e (n,_) = n `elem` getNames (Sc e)
>     right (n, Right x) = (n, x)
>     isRight (n, Right _) = True
>     isRight (n, Left _) = False

>     pmSubst :: Name -> SEnv -> -- Name useful for debugging
>                [(Name, Either StackEntry (TT Name))] -> -- function arguments, value
>                TSimpleCase Name -> -- compiled match
>                State EvalState (Maybe (TT Name))
>     pmSubst n env args (TTm rhs) 
>         = do rhs' <- {-# SCC "pmsubstnames" #-} substArgNames args rhs
>              return $ Just rhs'
>     pmSubst n env args TErrorCase = return $ Nothing
>     pmSubst n env args TImpossible = return $ Nothing
>     pmSubst n env args (TSCase scr cases)
>         = case scr of
>             P n -> do (e' , args') <- alookup [] n args
>                       pmSubstCases e' cases args'
>             e -> do e' <- substArgNames args e
>                     e' <- eval (True, True) e' [] env []
>                     pmSubstCases e' cases args
>       where alookup acc n ((x,arg@(Left (a, aenv, apats))):args) 
>                     | n == x = do e' <- eval (False, True) a [] aenv apats
>                                   return (e', acc ++ (x, Right e'):args)
>             alookup acc n ((x,Right e'):args) 
>                     | n == x = return (e', acc ++ (x, Right e'):args)
>             alookup acc n (a:args) = alookup (acc ++ [a]) n args

>             pmSubstCases e [] args = return Nothing
>             pmSubstCases e (c:cs) args 
>                          = do t <- pmCase e c args
>                               case t of
>                                  (Just t', _) -> return (Just t')
>                                  (Nothing, False) -> pmSubstCases e cs args
>                                  _ -> return Nothing

Matching will either succeed, fail (but not be stuck), or realise it's stuck

>             pmCase e (TDefault rhs) args = do v <- pmSubst n env args rhs
>                                               return (v, False)
>             pmCase e (TAlt con t cargs sc) args
>              | Just (t', cargs') <- getConArgs e []
>                 = if (t==t' && length cargs == length cargs')
>                      then do v <- pmSubst n env 
>                                     (args ++ zip cargs (map Right cargs')) sc
>                              return (v, False)
>                      else return (Nothing, False)
>              | otherwise = return (Nothing, True)
>             pmCase (Const e) (TConstAlt c sc) args
>                    = case cast e of
>                        Just e' -> if (e'==c) 
>                           then do v <- pmSubst n env args sc
>                                   return (v, False)
>                           else return (Nothing, False)
>                        Nothing -> return (Nothing, False)
>             pmCase _ _ _ = return (Nothing, True)

> traceIf t s x = if t then (trace s x) else x

> eval_nfEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
> eval_nfEnv env g t
>     = eval_nf (addenv env g) t
>   where addenv [] g = g
>         addenv ((n,B (Let v) ty):xs) (Gam g)
>             = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
>         addenv (_:xs) g = addenv xs g

Turn MN to UN, if they are unique, so that they look nicer.

> tidyNames :: Indexed Name -> Indexed Name
> tidyNames (Ind tm) = Ind (tidy' [] tm)
>   where tidy' ns (Bind (MN (n,i)) (B b t) (Sc tm)) = 
>             let n' = uniqify (UN n) ns in
>                 Bind n' (B b (tidy' ns t)) (Sc (tidy' (n':ns) tm))
>         tidy' ns (Bind x (B b t) (Sc tm)) 
>               = Bind x (B b (tidy' ns t)) (Sc (tidy' (x:ns) tm))
>         tidy' ns (App f a) = App (tidy' ns f) (tidy' ns a)
>         tidy' ns x = x

Various tracing facilities for spying on specific cases

> tracefns = []

> matchtrace n xs =
>    if (n `elem` tracefns)
>        then trace ("Matching " ++ n ++ " " ++ show (map (\(x,y,z) -> x) xs))
>        else id

> rhstrace :: String -> TT Name -> [(Name, TT Name)] -> a -> a
> rhstrace n rhs pbinds =
>    if (n `elem` tracefns)
>       then trace ("Returned " ++ n ++ " => " ++ show rhs ++ "\n" ++
>                               showb pbinds)
>       else id
>   where showb [] = ""
>         showb (m:xs) = "  " ++ show m ++ "\n" ++ showb xs