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