Trace.hs

module Language.Cap.Debug.Trace
       (Graph,NodeInfo(..),NodeName
       ,numNodes,numApps,numReductions
       ,nodeLast,nodeHead,nodeHeads,nodeArgs,nodeValue,isApplication
       ,isIndirection,nodeContents,nodeResult,allNodes,allApplications
       ,dispReduction)
       where

import Language.Cap.Interpret.Pretty
import qualified Language.Cap.Interpret.Pretty as P (pretty)

import Data.Map (Map(..))
import qualified Data.Map as M

import Data.Maybe
import Data.List

{- | A type synonym for the graph - it simply maps node names onto info about
     the node.
-}
type Graph = Map NodeName NodeInfo

-- | Stores information about any given node in the trace.
data NodeInfo = Application NodeName NodeName
              | Atom String
              | Indirection NodeName
                deriving (Show,Read)

-- | Checks whether a given node is an application node.
isApplication :: NodeInfo -> Bool
isApplication (Application _ _) = True
isApplication _ = False

-- | Checks whether a given node is an indirection node.
isIndirection :: NodeInfo -> Bool
isIndirection (Indirection _) = True
isIndirection _ = False

{- | Node names are just strings (of rs, as and fs at the moment).  Node names
     are stored in reverse order thus if the theory paper describes a node as
     \"rarf\" it will be stored as \"frar\".
-}
type NodeName = String

-- | Counts the number of nodes in any given trace.
numNodes :: Graph -> Int
numNodes n = M.size n

-- | Counts the number of application nodes in any given trace.
numApps :: Graph -> Int
numApps n = M.size (M.filter isApplication n)

-- | Counts the number of reduction arrows in any given trace.
numReductions :: Graph -> Int
numReductions n =
  M.size (M.filterWithKey keyEndsWithR n)
  where
    -- | Checks whether the node is the direct result of a reduction.
    keyEndsWithR ('r':xs) _ = True
    keyEndsWithR _ _ = False

{- | The final node in a sequence of reductions starting at a node m.
     The purpose of this function is to find the most evaluated point for m.
-}
nodeLast :: Graph -> NodeName -> NodeName
nodeLast g m =
  case nodeValue g ('r':m) of
    Just n -> nodeLast g ('r':m)
    _      -> case nodeValue g m of
                Just (Indirection n) -> nodeLast g n
                _                    -> m

{- | The head of the term at node m, head(G,m) where G is a graph and m is
     a node in g.
-}
nodeHead :: Graph -> NodeName -> NodeName
nodeHead g m =
  case nodeValue g m of
    Just (Application i j) -> nodeHead g (nodeLast g i)
    Just a@(Atom x)        -> m

nodeHeads :: Graph -> NodeName -> [NodeName]
nodeHeads g m =
  case nodeValue g m of
    Just (Application i j) -> m:nodeHeads g (nodeLast g i)
    Just (Atom x)          -> [m]

{- | The arguments of the application at node m.  Note that the arguments of the
     application are a sequence of nodes.
-}
nodeArgs :: Graph -> NodeName -> [NodeName]
nodeArgs g m =
  case nodeValue g m of
    Just (Application i j) -> nodeArgs g (nodeLast g i) ++ [j]
    _                      -> []

{- | Returns the value held at a specific node
-}
nodeValue :: Graph -> NodeName -> Maybe NodeInfo
nodeValue g m = M.lookup m g

{- | Gives a printable version of the node m in graph G.
-}
nodeContents :: Graph -> NodeName -> PrettyTerm
nodeContents g m =
  case nodeValue g m of
    Just (Application i j) -> PApplication (nodeContents g i) (nodeContents g j)
    Just (Atom a)          -> PAtom a
    Just (Indirection x)   -> nodeContents g x
    Nothing                -> PAtom ""

nodeResult :: Graph -> NodeName -> PrettyTerm
nodeResult g m =
  case nodeValue g (nodeLast g m) of
    Just (Application i j) -> PApplication (nodeResult g i) (nodeResult g j)
    Just (Atom a)          -> PAtom a
    Just (Indirection x)   -> nodeResult g x
    Nothing                -> PAtom ""

{- | Gives a list of all nodes in the trace.
-}
allNodes :: Graph -> [NodeName]
allNodes g = M.keys g

{- | Gives a list of all nodes that are applications
-}
allApplications :: Graph -> [NodeName]
allApplications g = filter (isApplication . fromJust . nodeValue g) (allNodes g)

-- | Display a full reduction.
dispReduction :: Graph -> NodeName -> String
dispReduction g n =    P.pretty (nodeContents g n)
                    ++ " = "
                    ++ P.pretty (nodeResult g n)