Commit ae8cee50 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Analysis for recursive types added

parent 64b5ae9a
Higher-order constructor analysis
---------------------------------
This analysis is a simple analysis for data constructors.
It associates to each data constructor a flag indicating
whether some argument contains functions.
Higher-order property analysis
------------------------------
This analysis analyzes the higher-order status of an operation,
i.e., it shows whether an operation is first order or
it is higher-order since has functional arguments or results
or processes data structures with functional components.
This analysis analyzes the higher-order status of an operation.
It classifies an operations as higher-order since if it
has functional arguments or results, or or it processes
data structures with functional components.
Analyzing types occurring in values
-----------------------------------
The `TypesInValues` analysis is a type analysis which assigns
to each data type defined in a program the list of data types
(type constructors) which might occur in value arguments of this type.
For instance, no type constructors are associated to `Bool`
since Boolean values have no arguments.
The type constructor `[]` is associated to the `[]` since a list
occurs in the second argument of a non-empty list.
Thus, this analysis can be used to check for recursive types:
if a type constructor is associated to itself, the type is recursive,
i.e., can have values of arbitrary size.
For instance, consider the following type declarations:
data List a = Empty | Cons a (List a)
data Tree a = Leaf | Node (List (Tree a))
Then this analysis computes the following information:
List : List
Tree : List, Tree
Hence, both types are recursive.
......@@ -44,6 +44,7 @@ import RootReplaced
import SolutionCompleteness
import Termination
import TotallyDefined
import TypeUsage
--------------------------------------------------------------------
--- Each analysis used in our tool must be registered in this list
......@@ -75,6 +76,7 @@ registeredAnalysis =
,cassAnalysis "Root cyclic replacements" rootCyclicAnalysis showRootCyclic
,cassAnalysis "Root replacements" rootReplAnalysis showRootRepl
,cassAnalysis "Terminating operations" terminationAnalysis showTermination
,cassAnalysis "Types in values" typesInValuesAnalysis showTypeNames
]
......
------------------------------------------------------------------------
--- Analysis of properties related to the usage and occurrences of types.
---
--- @author Michael Hanus
--- @version February 2017
------------------------------------------------------------------------
module TypeUsage(showTypeNames,typesInValuesAnalysis) where
import Analysis
import FlatCurry.Types
import List(intercalate)
------------------------------------------------------------------------
-- This analysis associates to each type the types which might occur
-- in values of this type. If a type occurs in its associated types,
-- it is a recursive type.
typesInValuesAnalysis :: Analysis [QName]
typesInValuesAnalysis =
dependencyTypeAnalysis "TypesInValues" [] typesInTypeDecl
-- Show a list of type constructor names as a string.
showTypeNames :: AOutFormat -> [QName] -> String
showTypeNames _ tcs = intercalate ", " $ map (\ (mn,fn) -> mn ++ "." ++ fn) tcs
typesInTypeDecl :: TypeDecl -> [(QName,[QName])] -> [QName]
typesInTypeDecl (Type _ _ _ conDecls) usedtypes =
foldr join [] $ map typesInConsDecl conDecls
where
typesInConsDecl (Cons _ _ _ typeExprs) =
foldr join [] $ map (typesInTypeExpr usedtypes) typeExprs
typesInTypeDecl (TypeSyn _ _ _ typeExpr) usedtypes =
typesInTypeExpr usedtypes typeExpr
-- Computes all type constructors occurring in a type expression.
typesInTypeExpr :: [(QName,[QName])] -> TypeExpr -> [QName]
typesInTypeExpr _ (TVar _) = []
typesInTypeExpr usedtypes (FuncType t1 t2) =
join (typesInTypeExpr usedtypes t1) (typesInTypeExpr usedtypes t2)
typesInTypeExpr usedtypes (TCons tc texps) =
foldr join (join [tc] (maybe [] id (lookup tc usedtypes)))
(map (typesInTypeExpr usedtypes) texps)
join :: [QName] -> [QName] -> [QName]
join tcs1 tcs2 = foldr insert tcs2 tcs1
where
insert x [] = [x]
insert x (y:ys) | x == y = y : ys
| x < y = x : y : ys
| otherwise = y : insert x ys
-----------------------------------------------------------------------
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