d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder{- |

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederModule : $Header$

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederDescription : Static analysis for first-order logic with dependent types (DFOL)

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederMaintainer : k.sojakova@jacobs-university.de

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederStability : experimental

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian MaederPortability : portable

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder-}

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maedermodule DFOL.Analysis_DFOL

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder (

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder basicAnalysis -- static analysis of basic specifications

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder , symbAnalysis -- static analysis for symbols lists

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder , symbMapAnalysis -- static analysis for symbol map lists

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder ) where

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport DFOL.Utils

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport DFOL.AS_DFOL

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport DFOL.Sign

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport DFOL.Symbol

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport Common.DocUtils

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport Common.ExtSign

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport Common.GlobalAnnotations

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport Common.Id

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport Data.Maybe

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport qualified Common.Result as Result

ad0b6d89fd72f0db461bfa6b43699157b6d2daf7Christian Maederimport qualified Common.AS_Annotation as Anno

8561bd2b32a5bfb81f18760fc9c221ddd0365031Christian Maederimport qualified Data.Set as Set

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maederimport qualified Data.Map as Map

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder

215f5ca60813ce24c2ad4c89e66e975e621dde83Christian Maeder-- BASIC SPEC ANALYSIS

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian MaederbasicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian Maeder Result.Result (BASIC_SPEC, ExtSign Sign Symbol, [Anno.Named FORMULA])

a9bb88c51c6cffa4be78fa8ddd15029831ac2596Christian MaederbasicAnalysis (bs, sig, _) =

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder if errs

d16796d2e67b21942cb8869a2bd7727b0c49f602Christian Maeder then Result.Result diag Nothing

215f5ca60813ce24c2ad4c89e66e975e621dde83Christian Maeder else Result.Result [] $ Just (bs, ExtSign newSig declaredSyms, formulae)

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian Maeder where Diagn diag1 newSig = makeSig bs sig

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian Maeder Diagn diag2 formulae = makeFormulas bs newSig

a9bb88c51c6cffa4be78fa8ddd15029831ac2596Christian Maeder declaredSyms = Set.map Symbol

dc2ce67f56f9d4507503cc2a24f2646c7f2adf6dChristian Maeder $ Set.difference (getSymbols newSig) (getSymbols sig)

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian Maeder diag = diag1 ++ diag2

dc2ce67f56f9d4507503cc2a24f2646c7f2adf6dChristian Maeder errs = Result.hasErrors diag

add3ebffeda5101eae1f7a952bf7a75382a6a5e4Christian Maeder

-- SIGNATURES

-- make a new signature out of a basic spec and an input signature

makeSig :: BASIC_SPEC -> Sign -> DIAGN Sign

makeSig (Basic_spec items) sig = addItemsToSig items sig

-- adds a list of annotated basic items to an input signature

addItemsToSig :: [Anno.Annoted BASIC_ITEM] -> Sign -> DIAGN Sign

addItemsToSig [] sig = Diagn [] sig

addItemsToSig (i:is) sig =

case i of

(Anno.Annoted (Axiom_item _) _ _ _) -> addItemsToSig is sig

(Anno.Annoted (Decl_item d) _ _ _) ->

if (Result.hasErrors diag)

then Diagn diag sig

else addItemsToSig is newSig

where Diagn diag newSig = addDeclToSig d sig

-- adds a declaration to an existing signature

addDeclToSig :: DECL -> Sign -> DIAGN Sign

addDeclToSig dec sig = if valid

then Diagn [] $ addSymbolDecl dec sig

else Diagn diag sig

where Diagn diag valid = isValidDecl dec sig emptyContext

-- FORMULAS

-- make a list of formulas for the given signature out of a basic spec

makeFormulas :: BASIC_SPEC -> Sign -> DIAGN [Anno.Named FORMULA]

makeFormulas (Basic_spec items) sig = makeFormulasFromItems items 0 sig

-- make a list of named formulas out of a list of annotated items

makeFormulasFromItems :: [Anno.Annoted BASIC_ITEM] -> Int

-> Sign -> DIAGN [Anno.Named FORMULA]

makeFormulasFromItems [] _ _ = Diagn [] []

makeFormulasFromItems (i:is) num sig =

case i of

(Anno.Annoted (Decl_item _) _ _ _) -> makeFormulasFromItems is num sig

(Anno.Annoted (Axiom_item a) _ _ annos) ->

case fM of

Just f ->

let Diagn diagL fs = makeFormulasFromItems is newNum sig

in Diagn diagL (f:fs)

Nothing ->

let Diagn diagL fs = makeFormulasFromItems is num sig

in Diagn (diag ++ diagL) fs

where Result.Result diag fM = makeNamedFormula a nam annos sig

label = Anno.getRLabel i

nam = if (label == "") then "Ax_" ++ show num else label

newNum = if (label == "") then num + 1 else num

-- make a named formula

makeNamedFormula :: FORMULA -> String -> [Anno.Annotation]

-> Sign -> Result.Result (Anno.Named FORMULA)

makeNamedFormula f nam annos sig =

if valid

then Result.Result [] $ Just $ namedF

else Result.Result diag Nothing

where Diagn diag valid = isValidFormula f sig emptyContext

namedF = (Anno.makeNamed nam f) {Anno.isAxiom = not isTheorem}

isImplies = or $ map Anno.isImplies annos

isImplied = or $ map Anno.isImplied annos

isTheorem = isImplies || isImplied

-- determines whether a formula is valid w.r.t. a signature and a context

isValidFormula :: FORMULA -> Sign -> CONTEXT -> DIAGN Bool

isValidFormula T _ _ = Diagn [] True

isValidFormula F _ _ = Diagn [] True

isValidFormula (Pred t) sig cont = hasType t Form sig cont

isValidFormula (Equality term1 term2) sig cont =

case type1M of

Nothing -> Diagn diag1 False

Just type1 -> case type1 of

Univ _ -> hasType term2 type1 sig cont

_ -> Diagn [noDiscourseTermError term1 type1 cont]

False

where Result.Result diag1 type1M = getTermType term1 sig cont

isValidFormula (Negation f) sig cont = isValidFormula f sig cont

isValidFormula (Conjunction fs) sig cont =

andD $ map (\f -> isValidFormula f sig cont) fs

isValidFormula (Disjunction fs) sig cont =

andD $ map (\f -> isValidFormula f sig cont) fs

isValidFormula (Implication f g) sig cont =

andD [isValidFormula f sig cont, isValidFormula g sig cont]

isValidFormula (Equivalence f g) sig cont =

andD [isValidFormula f sig cont, isValidFormula g sig cont]

isValidFormula (Forall [] f) sig cont = isValidFormula f sig cont

isValidFormula (Forall (d:ds) f) sig cont =

andD [validDecl, validFormula]

where validDecl = isValidVarDecl d sig cont

validFormula = isValidFormula (Forall ds f) sig (addVarDecl d cont)

isValidFormula (Exists [] f) sig cont = isValidFormula f sig cont

isValidFormula (Exists (d:ds) f) sig cont =

andD [validDecl, validFormula]

where validDecl = isValidVarDecl d sig cont

validFormula = isValidFormula (Exists ds f) sig (addVarDecl d cont)

-- SYMBOL LIST AND MAP ANALYSIS

-- creates a symbol map out of a list of symbol map items

symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result.Result (Map.Map Symbol Symbol)

symbMapAnalysis xs = Result.Result []

$ Just $ foldl (\ m x -> Map.union m (makeSymbMap x)) Map.empty xs

-- creates a symbol map out of symbol map items

makeSymbMap :: SYMB_MAP_ITEMS -> Map.Map Symbol Symbol

makeSymbMap (Symb_map_items xs) =

foldl (\ m x -> case x of

Symb s -> Map.insert (Symbol s) (Symbol s) m

Symb_map s1 s2 -> Map.insert (Symbol s1) (Symbol s2) m

)

Map.empty

xs

-- creates a symbol list out of a list of symbol items

symbAnalysis :: [SYMB_ITEMS] -> Result.Result [Symbol]

symbAnalysis xs = Result.Result [] $ Just $ concat $ map makeSymbols xs

-- creates a symbol list out of symbol item

makeSymbols :: SYMB_ITEMS -> [Symbol]

makeSymbols (Symb_items symbs) = map Symbol symbs

-- ERROR MESSAGES

noDiscourseTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis

noDiscourseTermError term t cont =

Result.Diag

{ Result.diagKind = Result.Error

, Result.diagString = "Term " ++ (show $ pretty term)

++ " has the non-discourse type " ++ (show $ pretty t)

++ " in the context " ++ (show $ pretty cont)

++ " and hence cannot be used in an equality."

, Result.diagPos = nullRange

}