|
definition:
|
processWorkList :: Eq a => ADom a -> (SemEq a->SemEq a->Bool) -> Bool -> [Rule]
-> [(String,[a])] -> WorkSemInt a -> IO (SemInt a)
processWorkList _ _ _ _ [] finals =
-- transform the final semantic into the usual format:
return (concatMap (\ (f,feqs) -> map (\ (args,res,_) -> Eq f args res) feqs)
(Table.toList finals))
processWorkList adom@(ADom abottom avar acons matchterms _ _ applyprim)
lessSpecificEq withprint trs wl@((fc,eargs) : working) finals = do
if withprint
then putStr (" W" ++ show (length wl) ++
"/F" ++ show (length (Table.toList finals)))
else return ()
let fcRules = let rules = funcRules fc trs
in if null rules
then error ("Rules of operation '"++fc++"' not found!")
else rules
(newwss,newfeqss) = maybe (unzip (map applyRule fcRules))
(\ares -> ([],[[(eargs,ares,[])]]))
(applyprim fc eargs)
(newws,newfeqs) = (concat newwss, concat newfeqss)
betterCalls = filter isBetterCall newws
betterEquations = filter hasBetterResult
(if null newfeqs
then [(eargs,abottom,[])] -- no matching rule
else newfeqs)
bestEquations = filter (\e-> not (any (\ei->ei/=e && leqEqDep e ei)
betterEquations))
betterEquations
activatedEqs =
if null bestEquations
then []
else concatMap (\ (f,feqs) -> concatMap (\ (args,_,deps) ->
if fc `elem` deps then [(f,args)] else []) feqs)
(Table.toList finals)
--putStrLn ("WORKING:" ++
-- showSemInt adom (map (\ (f,args)->Eq f args abottom) wl))
--putStrLn ("FINAL:" ++ showSemInt adom
-- (concatMap (\ (f,feqs) -> map (\ (args,res,_) -> Eq f args res) feqs)
-- (Table.toList finals)))
--putStrLn ("Function: " ++ fc)
--putStrLn ("BETTER: " ++ show betterEquations)
--putStrLn ("BEST : " ++ show bestEquations)
--putStrLn ("BETTER: " ++ show betterFuncs)
--putStrLn ("ACTIVE: " ++ show activatedEqs)
processWorkList adom lessSpecificEq withprint trs
(foldr insertIfBetterCall working
(betterCalls ++ activatedEqs))
(foldr insertBetterIntoRemaining finals bestEquations)
where
-- insert better (dependency) equations and delete all less specific ones:
insertBetterIntoRemaining bettereq wsem =
let oldfceqs = fEqsOfWorkSem fc wsem
in Table.update fc
(bettereq : filter (\oldeq -> not (leqEq oldeq bettereq)) oldfceqs)
wsem
-- insert given abstract call if there does not already exist one
-- which is more specific than this one; if the call is inserted,
-- all less specific calls are removed
--insertIfBetterCall :: (String,[a]) -> [(String,[a])] -> [(String,[a])]
insertIfBetterCall eq wlist =
if any (leqCall eq) wlist
then wlist
else eq : filter (\e -> not (leqCall e eq)) wlist
where
leqCall (f,args) (f',args') =
lessSpecificEq (Eq f args abottom) (Eq f' args' abottom)
-- is a given abstract call more specific than all equations
-- in the current final interpretation?
--isBetterCall :: (String,[a]) -> Bool
isBetterCall (f,args) =
not (any (\ (args',_,_) ->
lessSpecificEq (Eq f args abottom) (Eq f args' abottom))
(fEqsOfWorkSem f finals))
-- is a given equation for function fc a better approximation than
-- anything in the current final equations,
-- i.e., if there does not already exist one final equation which has
-- an identical left-hand side but a more specific result than this one
hasBetterResult eq = not (any (leqEq eq) (fEqsOfWorkSem fc finals))
-- compare given equation: left-hand sides and right-hand sides
-- in leq relation on terms?
leqEq (args,r,_) (args',r',_) =
lessSpecificEq (Eq fc args r) (Eq fc args' r')
-- compare given equation and their dependencies:
-- left- and right-hand sides in leq relation on terms and dependencies
-- subsumed?
leqEqDep (args,r,ds) (args',r',ds') =
lessSpecificEq (Eq fc args r) (Eq fc args' r') && all (`elem` ds') ds
applyRule (largs,rhs) =
maybe ([],[])
(\s -> (concatMap (newCall s) (fSubterms rhs),
map (\ri -> (eargs,ri,depFuncs))
(evalInt s finals rhs)))
(matchterms largs eargs)
where
depFuncs = funcsInTerm rhs
newCall s (f,args) = map (\iargs->(f,iargs))
(extendListMap (evalInt s finals) args)
-- abstract evaluation of a term w.r.t. a substitution and interpretation
--evalInt :: Sub a -> WorkSemInt a -> Term -> [a]
evalInt sub _ (Var v) = [maybe (avar v) id (lookup v sub)]
evalInt sub eqs (Func Cons c args) =
map (acons c) (extendListMap (evalInt sub eqs) args)
evalInt sub eqs (Func Def f args) =
let evalargs = extendListMap (evalInt sub eqs) args
results = concatMap (\ (argsi,r,_) ->
if any (\evargs->evargs==argsi) evalargs
then [r]
else [])
(fEqsOfWorkSem f eqs)
in if null results then [abottom] else results
|
|
iotype:
|
{(_,_,_,_,_,{[]},_) |-> _ || (_,{ADom},_,_,_,{:},_) |-> _}
|