|
definition:
|
transformInt :: Eq a => ADom a -> (SemEq a -> SemInt a -> SemInt a)
-> [Rule] -> SemInt a -> SemInt a -> SemInt a
transformInt (ADom abottom avar acons matchterms _ _ applyprim)
insertsem trs mains int =
foldr insertsem mains
(concatMap (\ (Eq fi argsi _) ->
maybe (concatMap (applyRule fi argsi) (fRules fi))
(\ares -> [Eq fi argsi ares])
(applyprim fi argsi))
int)
where
fRules f = let rules = funcRules f trs
in if null rules
then error ("Rules of operation '"++f++"' not found!")
else rules
applyRule fi argsi (largs,rhs) =
maybe []
(\s -> map (Eq fi argsi) (evalInt s int rhs)
++ concatMap (newSemEq s) (fSubterms rhs))
(matchterms largs argsi)
newSemEq s (f,args) =
map (\iargs -> Eq f iargs abottom) (extendListMap (evalInt s int) args)
-- abstract evaluation of a term w.r.t. a given substitution
-- and interpretation
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
in abottom :
concatMap (\ (Eq fi argsi r) ->
if any (\eargs->fi==f && eargs==argsi) evalargs then [r] else [])
eqs
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
------------------------------------------------------------------------------
-- Transformation on (abstract) interpretations:
-- (transformInt adom insertsem trs mains int)
-- adom : abstract domain
-- insertsem : operation to insert new semantic equation into an interpretation
-- trs : term rewriting system
-- mains : main calls (start interpretation)
-- int : interpretation to be transformed
-- result: transformed interpretation
|
|
failfree:
|
(_, _, _, _, _, _)
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{ADom},_,_,_,_) |-> _}
|
|
name:
|
transformInt
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Prelude.Eq a => ADom a -> (SemEq a -> [SemEq a] -> [SemEq a]) -> [TRS.Rule]
-> [SemEq a] -> [SemEq a] -> [SemEq a]
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|