{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

{- |

Module : ./THF/StaticAnalysisTHF.hs

Description : Static analysis for THF

Copyright : (c) A. Tsogias, DFKI Bremen 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Alexis.Tsogias@dfki.de

Stability : provisional

Portability : portable

Static analysis for THF.

NOTE: This implementation covers only THF0!

-}

module THF.StaticAnalysisTHF (basicAnalysis) where

import THF.As as As

import THF.Cons

import THF.Print ()

import THF.Sign

import THF.Poly (type_check)

import THF.Utils (thfTopLevelTypeToType)

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.Result

import Common.ExtSign

import Common.Lib.State

import Common.DocUtils

import Control.Monad

import qualified Data.Map as Map

import qualified Data.Set as Set

{- -----------------------------------------------------------------------------

Questions:

how to handle SysType in isTypeConsistent?

Todo:

find out what fi_domain, fi_predicates and fi_functors are and try

to somehow support them

----------------------------------------------------------------------------- -}

-- The main method for the static analysis

basicAnalysis :: (BasicSpecTHF, SignTHF, GlobalAnnos) ->

Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])

basicAnalysis (bs@(BasicSpecTHF bs1), sig1, _) =

let (diag1, bs2) = filterBS [] bs1

(diag2, sig2, syms) = execState (fillSig bs2) (diag1, sig1, Set.empty)

(diag3, ns) = getSentences bs2 (diag2, [])

in do

type_check (types sig2) (consts sig2) ns

Result (reverse diag3) $ Just (bs, ExtSign sig2 syms, ns)

{- This functions delets all Comments and Includes because they are not needed

for the static analysis

The diagnosis list has a reverted order! -}

filterBS :: [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])

filterBS d [] = (d, [])

filterBS d (t : rt) = case t of

TPTP_Include i -> let ds = mkDiag Warning "Include will be ignored." i

in filterBS (ds : d) rt

TPTP_Comment _ -> filterBS d rt

TPTP_Defined_Comment _ -> filterBS d rt

TPTP_System_Comment _ -> filterBS d rt

TPTP_Header _ -> filterBS d rt

_ -> let (diag, thf) = filterBS d rt

in (diag, t : thf)

-- Append the Signature by the Types and Constants given inside the basic spec

fillSig :: [TPTP_THF] -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()

fillSig [] = return ()

fillSig bs = mapM_ fillSingleType bs >> mapM_ fillSingleConst bs

where

fillSingleType t = case t of

TPTP_THF_Annotated_Formula n fr tf a -> case fr of

Type ->

when (isKind tf) $ case makeKind tf of

Right d -> appandDiag d

Left (k, c) -> insertType c n k a

_ -> return ()

_ -> return ()

fillSingleConst t = case t of

TPTP_THF_Annotated_Formula n fr tf a -> case fr of

Type ->

unless (isKind tf) $ case makeType tf of

Right d -> appandDiag d

Left (ty, c) -> insertConst c n ty a

_ -> return ()

_ -> return ()

{- Append the Diagnosis-List by the given Diagnosis

The new diag will be put on top of the existing list. -}

appandDiag :: Diagnosis -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()

appandDiag d = modify (\ (diag, s, syms) -> (d : diag, s, syms))

-- insert the given type into the Signature

insertType :: Constant -> As.Name -> Kind -> Annotations

-> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()

insertType c n k a = do

(diag, sig, syms) <- get

if sigHasConstSymbol c sig then appandDiag $ mkDiag Error

"Duplicate definition of a symbol as a type constant. Symbol: " c

else

if sigHasTypeSymbol c sig then

unless (sigHasSameKind c k sig) $ appandDiag $

mkDiag Error ("A type with the same identifier"

++ "but another Kind is already inside the signature") c

else do -- everythign is fine

let ti = TypeInfo { typeId = c, typeName = n, typeKind = k

, typeAnno = a }

sym = Symbol { symId = c, symName = n, symType = ST_Type k }

put (diag, sig { types = Map.insert c ti (types sig)

, symbols = Map.insert c sym (symbols sig) }

, Set.insert sym syms)

-- insert the given constant into the Signature

insertConst :: Constant -> As.Name -> Type -> Annotations

-> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()

insertConst c n t a = do

(_, sig, _) <- get

if sigHasTypeSymbol c sig then (appandDiag $ mkDiag Error

"Duplicate definition of a symbol as a type constant. Symbol: " c)

else do

isTypeConsistent t

if sigHasConstSymbol c sig then

unless (sigHasSameType c t sig) $ appandDiag $ mkDiag Error

("A constant with the same identifier but another " ++

"type is already inside the signature") c

else -- everything is fine

let ci = ConstInfo { constId = c, constName = n, constType = t

, constAnno = a }

sym = Symbol { symId = c, symName = n

, symType = ST_Const t }

in do

(diag', sig', syms') <- get

put (diag', sig' { consts = Map.insert c ci (consts sig')

, symbols = Map.insert c sym (symbols sig') }

, Set.insert sym syms')

-- Check if a type symbol is already inside the sig

sigHasTypeSymbol :: Constant -> SignTHF -> Bool

sigHasTypeSymbol c sig = Map.member c (types sig)

{- This Method is ment to be used after sigHasTypeSymbol

Check if a type symbol with the same kind is inside the Sig

If this is not the case me have a problem! -}

sigHasSameKind :: Constant -> Kind -> SignTHF -> Bool

sigHasSameKind c k sig = typeKind (types sig Map.! c) == k

-- Check if a const symbol is already inside the sig

sigHasConstSymbol :: Constant -> SignTHF -> Bool

sigHasConstSymbol c sig = Map.member c (consts sig)

{- This Method is ment to be used after sigHasConstSymbol

Check if a const symbol with the same type is inside the Sig

If this is not the case me have a problem! -}

sigHasSameType :: Constant -> Type -> SignTHF -> Bool

sigHasSameType c t sig = constType (consts sig Map.! c) == t

{- check if all cTypes inside the given Type are elements of the signaure.

Nothing means that everything is fine, otherwise Just diag will be returned. -}

isTypeConsistent :: Type -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()

isTypeConsistent t = do

(_, sig, _) <- get

case t of

MapType t1 t2 -> do

isTypeConsistent t1

isTypeConsistent t2

ParType t1 -> isTypeConsistent t1

CType c -> when (not (sigHasTypeSymbol c sig))

(do

insertType c (N_Atomic_Word c) Kind Null

appandDiag $ mkDiag Warning "Unknown type: " c)

ProdType ts -> mapM_ isTypeConsistent ts

_ -> return ()

-- SType _ -> ... -- how to handle these?

{- -----------------------------------------------------------------------------

Extract the sentences from the basic spec

----------------------------------------------------------------------------- -}

{- Get all sentences from the content of the BasicSpecTH

The diag list has a reverted order. -}

getSentences :: [TPTP_THF] -> ([Diagnosis], [Named THFFormula])

-> ([Diagnosis], [Named THFFormula])

getSentences [] dn = dn

getSentences (t : rt) dn@(d, ns) = case t of

TPTP_THF_Annotated_Formula _ fr _ _ -> case fr of

Type -> getSentences rt dn

Unknown ->

let diag = mkDiag Warning

"THFFormula with role \'unknown\' will be ignored." t

in getSentences rt (diag : d, ns)

Plain ->

let diag = mkDiag Warning

"THFFormula with role \'plain\' will be ignored." t

in getSentences rt (diag : d, ns)

Fi_Domain ->

let diag = mkDiag Warning

"THFFormula with role \'fi_domain\' will be ignored." t

in getSentences rt (diag : d, ns)

Fi_Functors ->

let diag = mkDiag Warning

"THFFormula with role \'fi_functors\' will be ignored." t

in getSentences rt (diag : d, ns)

Fi_Predicates ->

let diag = mkDiag Warning

"THFFormula with role \'fi_predicates\' will be ignored." t

in getSentences rt (diag : d, ns)

Assumption ->

let diag = mkDiag Warning

"THFFormula with role \'assumption\' will be ignored." t

in getSentences rt (diag : d, ns)

_ ->

let (d1, ns1) = getSentences rt dn

in (d1, tptpthfToNS t : ns1)

_ -> getSentences rt dn

{- Precondition: The formulaRole must not be Type, Unknown, Plain, Fi_Domain

Fi_Functors, Fi_Predicates or Assumption

(They are filtered out in getSentences) -}

tptpthfToNS :: TPTP_THF -> Named THFFormula

tptpthfToNS f =

let s = makeNamed (show $ pretty $ nameAF f) (thfFormulaAF f)

t = s { isAxiom = False }

w = s { wasTheorem = True }

in case formulaRoleAF f of

Definition -> s { isDef = True }

Conjecture -> t

Negated_Conjecture -> t

Theorem -> w

Lemma -> w

Hypothesis -> t

_ -> s -- { isAxiom = True, isDef = False, wasTheorem = False }

{- -----------------------------------------------------------------------------

Get the Kind of a type

----------------------------------------------------------------------------- -}

makeKind :: THFFormula -> Either (Kind, Constant) Diagnosis

makeKind t = maybe (Right $ mkDiag Error "Error while parsing the kind of:" t)

Left (thfFormulaToKind t)

thfFormulaToKind :: THFFormula -> Maybe (Kind, Constant)

thfFormulaToKind (T0F_THF_Typed_Const tc) = thfTypedConstToKind tc

thfFormulaToKind _ = Nothing

thfTypedConstToKind :: THFTypedConst -> Maybe (Kind, Constant)

thfTypedConstToKind (T0TC_THF_TypedConst_Par tcp) = thfTypedConstToKind tcp

thfTypedConstToKind (T0TC_Typed_Const c tlt) =

maybe Nothing (\ k -> Just (k, c))

(thfTopLevelTypeToKind tlt)

thfTopLevelTypeToKind :: THFTopLevelType -> Maybe Kind

thfTopLevelTypeToKind tlt = case tlt of

T0TLT_THF_Binary_Type bt -> thfBinaryTypeToKind bt

T0TLT_Defined_Type _ -> Just Kind

_ -> Nothing

thfBinaryTypeToKind :: THFBinaryType -> Maybe Kind

thfBinaryTypeToKind bt = case bt of

T0BT_THF_Binary_Type_Par btp -> thfBinaryTypeToKind btp

_ -> Nothing

{- -----------------------------------------------------------------------------

Get the Type of a constant

----------------------------------------------------------------------------- -}

makeType :: THFFormula -> Either (Type, Constant) Diagnosis

makeType t = maybe (Right $ mkDiag Error "Error while parsing the type of:" t)

Left (thfFormulaToType t)

thfFormulaToType :: THFFormula -> Maybe (Type, Constant)

thfFormulaToType (T0F_THF_Typed_Const tc) = thfTypedConstToType tc

thfFormulaToType _ = Nothing

thfTypedConstToType :: THFTypedConst -> Maybe (Type, Constant)

thfTypedConstToType (T0TC_THF_TypedConst_Par tcp) = thfTypedConstToType tcp

thfTypedConstToType (T0TC_Typed_Const c tlt) =

maybe Nothing (\ t -> Just (t, c))

(thfTopLevelTypeToType tlt)

{- -----------------------------------------------------------------------------

Check if a THFFormula is a Type definition

----------------------------------------------------------------------------- -}

isKind :: THFFormula -> Bool

isKind tf = case tf of

T0F_THF_Typed_Const tc -> thfTypedConstIsKind tc

_ -> False

thfTypedConstIsKind :: THFTypedConst -> Bool

thfTypedConstIsKind tc = case tc of

T0TC_THF_TypedConst_Par tcp -> thfTypedConstIsKind tcp

T0TC_Typed_Const _ tlt -> thfTopLevelTypeIsKind tlt

thfTopLevelTypeIsKind :: THFTopLevelType -> Bool

thfTopLevelTypeIsKind tlt = case tlt of

T0TLT_THF_Binary_Type bt -> thfBinaryTypeIsKind bt

T0TLT_Defined_Type dt -> thfDefinedTypeIsKind dt

_ -> False

thfDefinedTypeIsKind :: DefinedType -> Bool

thfDefinedTypeIsKind dt = case dt of

DT_tType -> True

_ -> False

thfBinaryTypeIsKind :: THFBinaryType -> Bool

thfBinaryTypeIsKind bt = case bt of

T0BT_THF_Binary_Type_Par btp -> thfBinaryTypeIsKind btp

_ -> False