Commit 22ea5f18 authored by Michael Hanus 's avatar Michael Hanus
Browse files

RequiredValue analysis refined with strictness information

parent bd2f8477
......@@ -5,7 +5,7 @@
--- registered in the top part of this module.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version August 2014
--- @version May 2015
--------------------------------------------------------------------
module AnalysisCollection(
......
......@@ -16,12 +16,7 @@ DEPS = Analysis.curry AnalysisCollection.curry AnalysisDependencies.curry \
LoadAnalysis.curry SCC.curry ServerFormats.curry \
ServerFunctions.curry WorkerFunctions.curry \
$(LIBDIR)/Distribution.curry $(LIBDIR)/PropertyFile.curry \
$(METADIR)/FlatCurry.curry \
$(ANADIR)/Deterministic.curry $(ANADIR)/HigherOrder.curry \
$(ANADIR)/Indeterministic.curry $(ANADIR)/RightLinearity.curry \
$(ANADIR)/SolutionCompleteness.curry $(ANADIR)/TotallyDefined.curry \
$(ANADIR)/Demandedness.curry $(ANADIR)/Groundness.curry \
$(ANADIR)/RequiredValues.curry
$(METADIR)/FlatCurry.curry $(ANADIR)/*.curry
.PHONY: all compile install clean uninstall
......
......@@ -9,7 +9,7 @@
--- the argument `True` to compute the result `False`.
---
--- @author Michael Hanus
--- @version October 2014
--- @version May 2015
-----------------------------------------------------------------------------
module RequiredValues(AType(..),showAType,AFType(..),showAFType,lubAType,
......@@ -28,9 +28,11 @@ import Unsafe(trace)
------------------------------------------------------------------------------
-- Our abstract (non-standard) type domain.
-- `Any` represents any value, `Cons c` a value rooted by the constructor `c`,
-- or `Empty` represents no possible value.
data AType = Any | Cons QName | Empty
-- `Any` represents any expression,
-- `AnyC` represents any value (i.e., constructor-rooted term),
-- `Cons c` a value rooted by the constructor `c`, and
-- `Empty` represents no possible value.
data AType = Any | AnyC | Cons QName | Empty
--- Is some abstract type a constructor?
isConsValue :: AType -> Bool
......@@ -40,15 +42,25 @@ isConsValue av = case av of Cons _ -> True
--- Least upper bound of abstract values.
lubAType :: AType -> AType -> AType
lubAType Any _ = Any
lubAType AnyC Any = Any
lubAType AnyC AnyC = AnyC
lubAType AnyC (Cons _) = AnyC
lubAType AnyC Empty = AnyC
lubAType (Cons _) Any = Any
lubAType (Cons c) (Cons d) = if c==d then Cons c else Any
lubAType (Cons _) AnyC = AnyC
lubAType (Cons c) (Cons d) = if c==d then Cons c else AnyC
lubAType (Cons c) Empty = Cons c
lubAType Empty av = av
--- Join two abstract values. The result is `Empty` if they are not compatible.
joinAType :: AType -> AType -> AType
joinAType Any av = av
joinAType AnyC Any = AnyC
joinAType AnyC AnyC = AnyC
joinAType AnyC (Cons c) = Cons c
joinAType AnyC Empty = Empty
joinAType (Cons c) Any = Cons c
joinAType (Cons c) AnyC = Cons c
joinAType (Cons c) (Cons d) = if c==d then Cons c else Empty
joinAType (Cons _) Empty = Empty
joinAType Empty _ = Empty
......@@ -59,7 +71,8 @@ compatibleType t1 t2 = joinAType t1 t2 /= Empty
-- Shows an abstract value.
showAType :: AOutFormat -> AType -> String
showAType _ Any = "any"
showAType _ Any = "any"
showAType _ AnyC = "cons"
showAType _ (Cons (_,n)) = n --q++"."++n
showAType _ Empty = "_|_"
......@@ -125,25 +138,34 @@ analyseReqVal :: ProgInfo [QName] -> FuncDecl -> [(QName,AFType)] -> AFType
analyseReqVal consinfo (Func (m,f) arity _ _ rule) calledfuncs
| m==prelude = maybe (anaresult rule) id (lookup f preludeFuncs)
| otherwise = --trace ("Analyze "++f++"\n"++showCalledFuncs calledfuncs++
-- "\nRESULT: "++showAFType _ anaresult) $
-- "\nRESULT: "++showAFType _ (anaresult rule)) $
anaresult rule
where
anaresult (External _) = AFType [(take arity (repeat Any),Any)]
anaresult (External _) = AFType [(take arity (repeat Any),AnyC)]
anaresult (Rule args rhs) = analyseReqValRule consinfo calledfuncs args rhs
-- add special results for prelude functions here:
preludeFuncs = [("failed",AFType [([],Empty)])]
preludeFuncs = [("failed",AFType [([],Empty)])
,("==",AFType [([AnyC,AnyC],AnyC)])
,("=:=",AFType [([AnyC,AnyC],AnyC)])
,("$",AFType [([AnyC,Any],AnyC)])
,("$!",AFType [([AnyC,AnyC],AnyC)])
,("$!!",AFType [([AnyC,AnyC],AnyC)])
,("$#",AFType [([AnyC,AnyC],AnyC)])
,("$##",AFType [([AnyC,AnyC],AnyC)])
,("compare",AFType [([AnyC,AnyC],AnyC)])
]
analyseReqValRule :: ProgInfo [QName] -> [(QName,AFType)] -> [Int] -> Expr
-> AFType
analyseReqValRule consinfo calledfuncs args rhs =
let initenv = extendEnv [] args
envtypes = reqValExp initenv rhs Any
envtypes = reqValExp initenv rhs AnyC
rtypes = map snd envtypes
in -- If some result is any and another result is a constructor, then
in -- If some result is `AnyC` and another result is a constructor, then
-- analyze again for all constructors as required results
-- in order to get more precise information.
if any (==Any) rtypes && any isConsValue rtypes
if any (==AnyC) rtypes && any isConsValue rtypes
then
let somecons = maybe (error "Internal error")
(\ (Cons c) -> c)
......@@ -152,23 +174,23 @@ analyseReqValRule consinfo calledfuncs args rhs =
consenvtypes = foldr lubEnvTypes []
(map (\rt -> reqValExp initenv rhs rt)
(map Cons (somecons:othercons)))
in AFType (map (\ (env,rtype) -> (map snd env,rtype))
in AFType (map (\ (env,rtype) -> (map snd env, rtype))
(lubAnyEnvTypes (if length othercons >= maxReqValues
then envtypes
else consenvtypes)))
else AFType (map (\ (env,rtype) -> (map snd env,rtype))
else AFType (map (\ (env,rtype) -> (map snd env, rtype))
(lubAnyEnvTypes envtypes))
where
reqValExp env exp reqtype = case exp of
Var v -> [(updateVarInEnv env v reqtype, reqtype)]
Lit _ -> [(env, Any)] -- too many literal constants...
Lit _ -> [(env, AnyC)] -- too many literal constants...
Comb ConsCall c _ -> [(env, Cons c)] -- analysis of arguments superfluous
Comb FuncCall qf funargs ->
if qf==(prelude,"?") && length funargs == 2
then -- use intended definition of Prelude.? for more precise analysis:
reqValExp env (Or (head funargs) (funargs!!1)) reqtype
else
maybe [(env, Any)]
maybe [(env, AnyC)]
(\ftype -> case ftype of
EmptyFunc -> [(env, Empty)] -- no information available
AFType ftypes ->
......@@ -186,7 +208,7 @@ analyseReqValRule consinfo calledfuncs args rhs =
then [(env, Empty)]
else matchingenvs )
(lookup qf calledfuncs)
Comb _ _ _ -> [(env, Any)] -- no reasonable info for partial applications
Comb _ _ _ -> [(env, AnyC)] -- no reasonable info for partial applications
Or e1 e2 -> lubEnvTypes (reqValExp env e1 reqtype)
(reqValExp env e2 reqtype)
Case _ e branches ->
......@@ -212,6 +234,7 @@ analyseReqValRule consinfo calledfuncs args rhs =
-- argument is required to be a constructor:
envForConsArg env (reqtype,exp) =
case reqtype of
AnyC -> [foldr1 lubEnv (map fst (reqValExp env exp AnyC))]
Cons qc -> [foldr1 lubEnv (map fst (reqValExp env exp (Cons qc)))]
_ -> []
......@@ -242,11 +265,11 @@ lubEnvTypes ((env1,t1):ets1) ((env2,t2):ets2)
| t1<t2 = (env1,t1) : lubEnvTypes ets1 ((env2,t2):ets2)
| otherwise = (env2,t2) : lubEnvTypes ((env1,t1):ets1) ets2
--- "lub" the environments of the more specific types to the Any type
--- "lub" the environments of the more specific types to the AnyC type
--- (if present).
lubAnyEnvTypes :: [(AEnv,AType)] -> [(AEnv,AType)]
lubAnyEnvTypes envtypes =
if null envtypes || snd (head envtypes) /= Any
if null envtypes || snd (head envtypes) /= AnyC
then envtypes
else foldr1 lubEnvType envtypes : tail envtypes
......
......@@ -291,11 +291,11 @@ argumentTypesFor (Just EmptyFunc) _ = repeat Any
argumentTypesFor (Just (AFType rtypes)) reqval =
maybe (-- no exactly matching type, look for Any type:
maybe (-- no Any type: if reqtype==Any, try lub of all other types:
if reqval==Any && not (null rtypes)
if (reqval==Any || reqval==AnyC) && not (null rtypes)
then foldr1 lubArgs (map fst rtypes)
else repeat Any)
fst
(find ((==Any) . snd) rtypes))
(find ((`elem` [AnyC,Any]) . snd) rtypes))
fst
(find ((==reqval) . snd) rtypes)
where
......@@ -309,14 +309,14 @@ containsBeqRule (Rule _ rhs) = containsBeqExp rhs
where
-- containsBeq an expression w.r.t. a required value
containsBeqExp exp = case exp of
Var _ -> False
Lit _ -> False
Var _ -> False
Lit _ -> False
Comb _ qf es -> qf == pre "==" || qf == pre "/=" || any containsBeqExp es
Free _ e -> containsBeqExp e
Or e1 e2 -> containsBeqExp e1 || containsBeqExp e2
Typed e _ -> containsBeqExp e
Case _ e bs -> containsBeqExp e || any containsBeqBranch bs
Let bs e -> containsBeqExp e || any containsBeqExp (map snd bs)
Free _ e -> containsBeqExp e
Or e1 e2 -> containsBeqExp e1 || containsBeqExp e2
Typed e _ -> containsBeqExp e
Case _ e bs -> containsBeqExp e || any containsBeqBranch bs
Let bs e -> containsBeqExp e || any containsBeqExp (map snd bs)
containsBeqBranch (Branch _ be) = containsBeqExp be
......@@ -342,13 +342,12 @@ loadPreludeBoolReqValues = do
-- Current relevant Boolean functions of the prelude:
preludeBoolReqValues :: [(QName, AFType)]
preludeBoolReqValues =
[((pre "&&"),(AFType [([Any,Any],(Cons (pre "False"))),
([(Cons (pre "True")),(Cons (pre "True"))],(Cons (pre "True")))]))
,((pre "not"),(AFType [([(Cons (pre "True"))],(Cons (pre "False"))),
([(Cons (pre "False"))],(Cons (pre "True")))]))
,((pre "||"),
(AFType [([(Cons (pre "False")),(Cons (pre "False"))],(Cons (pre "False"))),
([Any,Any],(Cons (pre "True")))]))
,((pre "solve"),(AFType [([(Cons (pre "True"))],(Cons (pre "True")))]))
,((pre "&&>"),(AFType [([(Cons (pre "True")),Any],Any)]))
[(pre "&&", AFType [([Any,Any],false), ([true,true],true)])
,(pre "not", AFType [([true],false), ([false],true)])
,(pre "||", AFType [([false,false],false), ([Any,Any],true)])
,(pre "solve", AFType [([true],true)])
,(pre "&&>", AFType [([true,Any],AnyC)])
]
where
false = Cons (pre "False")
true = Cons (pre "True")
......@@ -32,15 +32,3 @@ BindingOpt: BindingOpt.curry
.PHONY: load
load: BindingOpt.curry
$(REPL) $(REPL_OPTS) :set path $(ANADIRS) :l $<
TESTPROGS = HTML SetFunctions Parser AddTypes CurryStringClassifier Curry2JS
.PHONY: test
test:
$(CLEANCURRY) -r
cd examples && $(TOOL) -f $(TESTPROGS) | tee test.log
cd examples && meld TEST.log test.log
.PHONY: selftest
selftest:
export CURRYPATH=$(ANADIRS) && ./eqopt -f BindingOpt.curry
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment