Program.hs

module Language.Cap.Interpret.Program (interpret) where

import Language.Cap.Interpret.Parse
import Language.Cap.Debug.Trace

import Data.Map (Map(..))
import qualified Data.Map as M
import Data.Maybe
import Data.List
import System.IO.Unsafe


-- | Substitutions are mappings from variable names to a graph to substitute in.
type Substitution = Map String NodeName

-- | Checks whether a term is simply a variable.
isVariable :: Term -> Bool
isVariable (TVariable _) = True
isVariable _ = False

-- | Fetches the variable name from a variable term.
variableName :: Term -> String
variableName (TVariable x) = x

-- | Constructs a graph for a term using a particular substitution.  No
--   evaluation is performed.
graph :: NodeName -> Term -> Substitution -> Graph
graph n (TAtom x) _ = M.singleton n (Atom x)
graph n (TVariable x) subs =
  M.singleton n (Indirection (fromJust (M.lookup x subs)))
graph n (TApplication (TVariable i) (TVariable j)) subs =
  M.singleton n (Application (fromJust (M.lookup i subs))
                             (fromJust (M.lookup j subs)))
graph n (TApplication (TVariable i) j) subs =
  M.insert n
           (Application (fromJust (M.lookup i subs)) ('a':n))
           (graph ('a':n) j subs)
graph n (TApplication i (TVariable j)) subs =
  M.insert n
           (Application ('f':n) (fromJust (M.lookup j subs)))
           (graph ('f':n) i subs)
graph n (TApplication i j) subs =
  M.insert n
           (Application ('f':n) ('a':n))
           (M.union ig jg)
  where
    ig = graph ('f':n) i subs
    jg = graph ('a':n) j subs

-- | Attempts to match a node in the graph against a pattern.
match :: Graph -> NodeName -> Term -> Maybe Substitution
match t n (TAtom a) =
  case nodeValue t n of
    Just (Atom a') -> if a == a' then Just M.empty
                                 else Nothing
    _              -> Nothing
match t n (TApplication i j) =
  case nodeValue t n of
    Just (Application i' j') ->
      do is <- if isVariable i then Just (M.singleton (variableName i) i')
                               else match t (nodeLast t i') i
         js <- if isVariable j then Just (M.singleton (variableName j) j')
                               else match t (nodeLast t j') j
         return $ M.union is js
    _ -> Nothing

-- | Evaluates the a term based on a given program.  Returns a trace of the
--   completed evaluation
interpret :: Program -> Term -> Graph
interpret p t = compute p (graph "" t (M.fromList []))

-- | Evaluates the program by continuously attempting to match un-reduced
--   computations against rewrite rules.
compute :: Program -> Graph -> Graph
compute p g = if isJust computableNode
                  then compute p (M.union g (graph ('r':redex) term subs))
                  else g
                where
                  computableNode = findRedex p g
                
                  (redex,term,subs) = fromJust computableNode

-- | Attempts to find a reducable expression, and the rewrite rule that it may
--   be reduced with.
findRedex :: Program -> Graph -> Maybe (NodeName,Term,Substitution)
findRedex p g =
  first (tryRules p g)
        [n | n <- nodes,    (not $ isIndirection $ fromJust $ nodeValue g n)
                         && not (('r':n) `elem` nodes)]
  where
    nodes = sortBy outerMostLeftMostFirst $ necessaryNodes g

-- | Finds all nodes that may need to be reduced to complete construction of
--   the trace
necessaryNodes :: Graph -> [NodeName]
necessaryNodes g =
  nub $ necessaryNodes' g ""
  where
    necessaryNodes' :: Graph -> NodeName -> [NodeName]
    necessaryNodes' g n =
      if ('r':n) `elem` allNodes g
        then necessaryNodes' g ('r':n)
        else
          case nodeValue g n of
            Just (Application i j)
              -> n:(necessaryNodes' g i ++ necessaryNodes' g j)
            Just (Atom a)
              -> [n]
            Just (Indirection x)
              -> necessaryNodes' g x

-- | Establishes an outermost leftmost first order on nodes
outerMostLeftMostFirst :: NodeName -> NodeName -> Ordering
outerMostLeftMostFirst x y =
  outerMostLeftMostFirst' (reverse x) (reverse y)
  where
    outerMostLeftMostFirst' [] [] = EQ
    outerMostLeftMostFirst' [] ('r':ys) = GT
    outerMostLeftMostFirst' [] (_:ys) = LT
    outerMostLeftMostFirst' ('r':xs) [] = LT
    outerMostLeftMostFirst' (_:xs) [] = GT
    outerMostLeftMostFirst' ('r':xs) ('r':ys) = outerMostLeftMostFirst' xs ys
    outerMostLeftMostFirst' ('f':xs) ('f':ys) = outerMostLeftMostFirst' xs ys
    outerMostLeftMostFirst' ('a':xs) ('a':ys) = outerMostLeftMostFirst' xs ys
    outerMostLeftMostFirst' ('r':xs) (_:ys) = LT
    outerMostLeftMostFirst' (_:xs) ('r':ys) = GT
    outerMostLeftMostFirst' ('f':xs) ('a':ys) = LT
    outerMostLeftMostFirst' ('a':xs) ('f':ys) = GT

-- | Tries each rewrite rule on a given unreduced application to find out if
--   it's a redex.
tryRules :: Program -> Graph -> NodeName -> Maybe (NodeName,Term,Substitution)
tryRules [] g n = Nothing
tryRules ((Rule pattern term):rs) g n = 
  if isJust subs then Just (n,term,fromJust subs)
                 else tryRules rs g n
  where
    subs = match g n pattern

-- | Finds the first item in a list for which f does not return Nothing.-}
first :: (a -> Maybe b) -> [a] -> Maybe b
first f [] = Nothing
first f (x:xs)
  = if isJust r then r
                else first f xs
    where
      r = f x