Analysis_DFOL.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterModule : $Header$
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDescription : Static analysis for first-order logic with dependent types (DFOL)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterLicense : GPLv2 or higher
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterMaintainer : k.sojakova@jacobs-university.de
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterStability : experimental
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPortability : portable
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basicAnalysis -- static analysis of basic specifications
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , symbAnalysis -- static analysis for symbols lists
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , symbMapAnalysis -- static analysis for symbol map lists
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Common.Result as Result
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Common.AS_Annotation as Anno
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Data.Set as Set
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnellimport qualified Data.Map as Map
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell-- BASIC SPEC ANALYSIS
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil MaddenbasicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey Result.Result (BASIC_SPEC, ExtSign Sign Symbol, [Anno.Named FORMULA])
26304a2a091af368cfc16c977bcce6d17195360aTom RumseybasicAnalysis (bs, sig, _) =
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey then Result.Result diag Nothing
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey else Result.Result [] $ Just (bs, ExtSign newSig declaredSyms, formulae)
997d6667b8c483bf582a231b1b24f84fbe6c8390Neil Madden where Diagn diag1 newSig = makeSig bs sig
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey Diagn diag2 formulae = makeFormulas bs newSig
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey declaredSyms = Set.map Symbol
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey $ Set.difference (getSymbols newSig) (getSymbols sig)
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey diag = diag1 ++ diag2
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey-- SIGNATURES
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey-- make a new signature out of a basic spec and an input signature
26304a2a091af368cfc16c977bcce6d17195360aTom RumseymakeSig :: BASIC_SPEC -> Sign -> DIAGN Sign
26304a2a091af368cfc16c977bcce6d17195360aTom RumseymakeSig (Basic_spec items) sig = addItemsToSig items sig
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey-- adds a list of annotated basic items to an input signature
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosteraddItemsToSig :: [Anno.Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
3cfef899c650ea8fa23c64ad5a66b8986bf77bb2Tom RumseyaddItemsToSig [] sig = Diagn [] sig
72450cb9c2ca854c6d3479832c2738196c1d3282Robert WapshottaddItemsToSig (i:is) sig =
72450cb9c2ca854c6d3479832c2738196c1d3282Robert Wapshott (Anno.Annoted (Axiom_item _) _ _ _) -> addItemsToSig is sig
3cfef899c650ea8fa23c64ad5a66b8986bf77bb2Tom Rumsey (Anno.Annoted (Decl_item d) _ _ _) ->
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell then Diagn diag sig
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell else addItemsToSig is newSig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster where Diagn diag newSig = addDeclToSig d sig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- adds a declaration to an existing signature
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosteraddDeclToSig :: DECL -> Sign -> DIAGN Sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosteraddDeclToSig dec sig = if valid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then Diagn [] $ addSymbolDecl dec sig
01a939641aeb0a095851921879620c3fab295cb2Robert Wapshott else Diagn diag sig
01a939641aeb0a095851921879620c3fab295cb2Robert Wapshott where Diagn diag valid = isValidDecl dec sig emptyContext
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- make a list of formulas for the given signature out of a basic spec
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeFormulas :: BASIC_SPEC -> Sign -> DIAGN [Anno.Named FORMULA]
01a939641aeb0a095851921879620c3fab295cb2Robert WapshottmakeFormulas (Basic_spec items) sig = makeFormulasFromItems items 0 sig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- make a list of named formulas out of a list of annotated items
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeFormulasFromItems :: [Anno.Annoted BASIC_ITEM] -> Int
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> Sign -> DIAGN [Anno.Named FORMULA]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeFormulasFromItems [] _ _ = Diagn [] []
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeFormulasFromItems (i:is) num sig =
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford (Anno.Annoted (Decl_item _) _ _ _) -> makeFormulasFromItems is num sig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (Anno.Annoted (Axiom_item a) _ _ annos) ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let Diagn diagL fs = makeFormulasFromItems is newNum sig
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey in Diagn diagL (f:fs)
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey let Diagn diagL fs = makeFormulasFromItems is num sig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in Diagn (diag ++ diagL) fs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster where Result.Result diag fM = makeNamedFormula a nam annos sig
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster nam = if (label == "") then "Ax_" ++ show num else label
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell newNum = if (label == "") then num + 1 else num
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- make a named formula
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeNamedFormula :: FORMULA -> String -> [Anno.Annotation]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeNamedFormula f nam annos sig =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then Result.Result [] $ Just $ namedF
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster else Result.Result diag Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster where Diagn diag valid = isValidFormula f sig emptyContext
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster namedF = (Anno.makeNamed nam f) {Anno.isAxiom = not isTheorem}
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster isImplies = or $ map Anno.isImplies annos
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster isImplied = or $ map Anno.isImplied annos
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster isTheorem = isImplies || isImplied
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- determines whether a formula is valid w.r.t. a signature and a context
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula :: FORMULA -> Sign -> CONTEXT -> DIAGN Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula T _ _ = Diagn [] True
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula F _ _ = Diagn [] True
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Pred t) sig cont = hasType t Form sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Equality term1 term2) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster case type1M of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Nothing -> Diagn diag1 False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Just type1 -> case type1 of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Univ _ -> hasType term2 type1 sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster _ -> Diagn [noDiscourseTermError term1 type1 cont]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster where Result.Result diag1 type1M = getTermType term1 sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Negation f) sig cont = isValidFormula f sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Conjunction fs) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster andD $ map (\f -> isValidFormula f sig cont) fs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Disjunction fs) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster andD $ map (\f -> isValidFormula f sig cont) fs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Implication f g) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster andD [isValidFormula f sig cont, isValidFormula g sig cont]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Equivalence f g) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster andD [isValidFormula f sig cont, isValidFormula g sig cont]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Forall [] f) sig cont = isValidFormula f sig cont
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtonisValidFormula (Forall (d:ds) f) sig cont =
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington andD [validDecl, validFormula]
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington where validDecl = isValidVarDecl d sig cont
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington validFormula = isValidFormula (Forall ds f) sig (addVarDecl d cont)
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtonisValidFormula (Exists [] f) sig cont = isValidFormula f sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidFormula (Exists (d:ds) f) sig cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster andD [validDecl, validFormula]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster where validDecl = isValidVarDecl d sig cont
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster validFormula = isValidFormula (Exists ds f) sig (addVarDecl d cont)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- SYMBOL LIST AND MAP ANALYSIS
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- creates a symbol map out of a list of symbol map items
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellsymbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result.Result (Map.Map Symbol Symbol)
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellsymbMapAnalysis xs = Result.Result []
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell $ Just $ foldl (\ m x -> Map.union m (makeSymbMap x)) Map.empty xs
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell-- creates a symbol map out of symbol map items
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnellmakeSymbMap :: SYMB_MAP_ITEMS -> Map.Map Symbol Symbol
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellmakeSymbMap (Symb_map_items xs) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster foldl (\ m x -> case x of
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell Symb s -> Map.insert (Symbol s) (Symbol s) m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Symb_map s1 s2 -> Map.insert (Symbol s1) (Symbol s2) m
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell-- creates a symbol list out of a list of symbol items
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellsymbAnalysis :: [SYMB_ITEMS] -> Result.Result [Symbol]
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellsymbAnalysis xs = Result.Result [] $ Just $ concat $ map makeSymbols xs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- creates a symbol list out of symbol item
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeSymbols :: SYMB_ITEMS -> [Symbol]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeSymbols (Symb_items symbs) = map Symbol symbs
bbffed9376e4fad86c443ca698c2fae6e9e81358David Luna-- ERROR MESSAGES
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosternoDiscourseTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosternoDiscourseTermError term t cont =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , Result.diagString = "Term " ++ (show $ pretty term)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ++ " has the non-discourse type " ++ (show $ pretty t)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ++ " in the context " ++ (show $ pretty cont)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ++ " and hence cannot be used in an equality."