{-# 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 :: (BasicSpecTHF, SignTHF, GlobalAnnos)
-> Result
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
basicAnalysis (bs :: BasicSpecTHF
bs@(BasicSpecTHF bs1 :: [TPTP_THF]
bs1), sig1 :: SignTHF
sig1, _) =
    let (diag1 :: [Diagnosis]
diag1, bs2 :: [TPTP_THF]
bs2) = [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [] [TPTP_THF]
bs1
        (diag2 :: [Diagnosis]
diag2, sig2 :: SignTHF
sig2, syms :: Set SymbolTHF
syms) = State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> ([Diagnosis], SignTHF, Set SymbolTHF)
-> ([Diagnosis], SignTHF, Set SymbolTHF)
forall s a. State s a -> s -> s
execState ([TPTP_THF] -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSig [TPTP_THF]
bs2) ([Diagnosis]
diag1, SignTHF
sig1, Set SymbolTHF
forall a. Set a
Set.empty)
        (diag3 :: [Diagnosis]
diag3, ns :: [Named THFFormula]
ns) = [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
bs2 ([Diagnosis]
diag2, [])
    in do
     TypeMap
-> ConstMap -> [Named THFFormula] -> Result [[(Token, Type)]]
type_check (SignTHF -> TypeMap
types SignTHF
sig2) (SignTHF -> ConstMap
consts SignTHF
sig2) [Named THFFormula]
ns
     [Diagnosis]
-> Maybe
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
-> Result
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse [Diagnosis]
diag3) (Maybe
   (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
 -> Result
      (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]))
-> Maybe
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
-> Result
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
forall a b. (a -> b) -> a -> b
$ (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
-> Maybe
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
forall a. a -> Maybe a
Just (BasicSpecTHF
bs, SignTHF -> Set SymbolTHF -> ExtSign SignTHF SymbolTHF
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign SignTHF
sig2 Set SymbolTHF
syms, [Named THFFormula]
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 :: [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS d :: [Diagnosis]
d [] = ([Diagnosis]
d, [])
filterBS d :: [Diagnosis]
d (t :: TPTP_THF
t : rt :: [TPTP_THF]
rt) = case TPTP_THF
t of
    TPTP_Include i :: Include
i -> let ds :: Diagnosis
ds = DiagKind -> String -> Include -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "Include will be ignored." Include
i
                      in [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS (Diagnosis
ds Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d) [TPTP_THF]
rt
    TPTP_Comment _ -> [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [Diagnosis]
d [TPTP_THF]
rt
    TPTP_Defined_Comment _ -> [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [Diagnosis]
d [TPTP_THF]
rt
    TPTP_System_Comment _ -> [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [Diagnosis]
d [TPTP_THF]
rt
    TPTP_Header _ -> [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [Diagnosis]
d [TPTP_THF]
rt
    _ -> let (diag :: [Diagnosis]
diag, thf :: [TPTP_THF]
thf) = [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
filterBS [Diagnosis]
d [TPTP_THF]
rt
                               in ([Diagnosis]
diag, TPTP_THF
t TPTP_THF -> [TPTP_THF] -> [TPTP_THF]
forall a. a -> [a] -> [a]
: [TPTP_THF]
thf)

-- Append the Signature by the Types and Constants given inside the basic spec
fillSig :: [TPTP_THF] -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
fillSig :: [TPTP_THF] -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSig [] = () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
fillSig bs :: [TPTP_THF]
bs = (TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> [TPTP_THF] -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSingleType [TPTP_THF]
bs State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> [TPTP_THF] -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSingleConst [TPTP_THF]
bs
    where
        fillSingleType :: TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSingleType t :: TPTP_THF
t = case TPTP_THF
t of
            TPTP_THF_Annotated_Formula n :: Name
n fr :: FormulaRole
fr tf :: THFFormula
tf a :: Annotations
a -> case FormulaRole
fr of
                Type ->
                    Bool
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (THFFormula -> Bool
isKind THFFormula
tf) (State ([Diagnosis], SignTHF, Set SymbolTHF) ()
 -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ case THFFormula -> Either (Kind, Constant) Diagnosis
makeKind THFFormula
tf of
                        Right d :: Diagnosis
d -> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag Diagnosis
d
                        Left (k :: Kind
k, c :: Constant
c) -> Constant
-> Name
-> Kind
-> Annotations
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
insertType Constant
c Name
n Kind
k Annotations
a
                _ -> () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            _ -> () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        fillSingleConst :: TPTP_THF -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
fillSingleConst t :: TPTP_THF
t = case TPTP_THF
t of
            TPTP_THF_Annotated_Formula n :: Name
n fr :: FormulaRole
fr tf :: THFFormula
tf a :: Annotations
a -> case FormulaRole
fr of
                Type ->
                    Bool
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (THFFormula -> Bool
isKind THFFormula
tf) (State ([Diagnosis], SignTHF, Set SymbolTHF) ()
 -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ case THFFormula -> Either (Type, Constant) Diagnosis
makeType THFFormula
tf of
                        Right d :: Diagnosis
d -> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag Diagnosis
d
                        Left (ty :: Type
ty, c :: Constant
c) -> Constant
-> Name
-> Type
-> Annotations
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
insertConst Constant
c Name
n Type
ty Annotations
a
                _ -> () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            _ -> () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
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 :: Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag d :: Diagnosis
d = (([Diagnosis], SignTHF, Set SymbolTHF)
 -> ([Diagnosis], SignTHF, Set SymbolTHF))
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall s. (s -> s) -> State s ()
modify (\ (diag :: [Diagnosis]
diag, s :: SignTHF
s, syms :: Set SymbolTHF
syms) -> (Diagnosis
d Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
diag, SignTHF
s, Set SymbolTHF
syms))

-- insert the given type into the Signature
insertType :: Constant -> As.Name -> Kind -> Annotations
                    -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
insertType :: Constant
-> Name
-> Kind
-> Annotations
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
insertType c :: Constant
c n :: Name
n k :: Kind
k a :: Annotations
a = do
    (diag :: [Diagnosis]
diag, sig :: SignTHF
sig, syms :: Set SymbolTHF
syms) <- State
  ([Diagnosis], SignTHF, Set SymbolTHF)
  ([Diagnosis], SignTHF, Set SymbolTHF)
forall s. State s s
get
    if Constant -> SignTHF -> Bool
sigHasConstSymbol Constant
c SignTHF
sig then Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> Constant -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
        "Duplicate definition of a symbol as a type constant. Symbol: " Constant
c
     else
        if Constant -> SignTHF -> Bool
sigHasTypeSymbol Constant
c SignTHF
sig then
            Bool
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constant -> Kind -> SignTHF -> Bool
sigHasSameKind Constant
c Kind
k SignTHF
sig) (State ([Diagnosis], SignTHF, Set SymbolTHF) ()
 -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$
                DiagKind -> String -> Constant -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("A type with the same identifier"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "but another Kind is already inside the signature") Constant
c
         else do -- everythign is fine
            let ti :: TypeInfo
ti = TypeInfo :: Constant -> Name -> Kind -> Annotations -> TypeInfo
TypeInfo { typeId :: Constant
typeId = Constant
c, typeName :: Name
typeName = Name
n, typeKind :: Kind
typeKind = Kind
k
                              , typeAnno :: Annotations
typeAnno = Annotations
a }
                sym :: SymbolTHF
sym = Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
Symbol { symId :: Constant
symId = Constant
c, symName :: Name
symName = Name
n, symType :: SymbolType
symType = Kind -> SymbolType
ST_Type Kind
k }
            ([Diagnosis], SignTHF, Set SymbolTHF)
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall s. s -> State s ()
put ([Diagnosis]
diag, SignTHF
sig { types :: TypeMap
types = Constant -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c TypeInfo
ti (SignTHF -> TypeMap
types SignTHF
sig)
                           , symbols :: SymbolMap
symbols = Constant -> SymbolTHF -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c SymbolTHF
sym (SignTHF -> SymbolMap
symbols SignTHF
sig) }
                , SymbolTHF -> Set SymbolTHF -> Set SymbolTHF
forall a. Ord a => a -> Set a -> Set a
Set.insert SymbolTHF
sym Set SymbolTHF
syms)

-- insert the given constant into the Signature
insertConst :: Constant -> As.Name -> Type -> Annotations
                    -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
insertConst :: Constant
-> Name
-> Type
-> Annotations
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
insertConst c :: Constant
c n :: Name
n t :: Type
t a :: Annotations
a = do
    (_, sig :: SignTHF
sig, _) <- State
  ([Diagnosis], SignTHF, Set SymbolTHF)
  ([Diagnosis], SignTHF, Set SymbolTHF)
forall s. State s s
get
    if Constant -> SignTHF -> Bool
sigHasTypeSymbol Constant
c SignTHF
sig then (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> Constant -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
        "Duplicate definition of a symbol as a type constant. Symbol: " Constant
c)
    else do
          Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent Type
t
          if Constant -> SignTHF -> Bool
sigHasConstSymbol Constant
c SignTHF
sig then
               Bool
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constant -> Type -> SignTHF -> Bool
sigHasSameType Constant
c Type
t SignTHF
sig) (State ([Diagnosis], SignTHF, Set SymbolTHF) ()
 -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> Constant -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                 ("A constant with the same identifier but another " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  "type is already inside the signature") Constant
c
           else -- everything is fine
                 let ci :: ConstInfo
ci = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo { constId :: Constant
constId = Constant
c, constName :: Name
constName = Name
n, constType :: Type
constType = Type
t
                                    , constAnno :: Annotations
constAnno = Annotations
a }
                     sym :: SymbolTHF
sym = Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
Symbol { symId :: Constant
symId = Constant
c, symName :: Name
symName = Name
n
                                  , symType :: SymbolType
symType = Type -> SymbolType
ST_Const Type
t }
                 in do
                     (diag' :: [Diagnosis]
diag', sig' :: SignTHF
sig', syms' :: Set SymbolTHF
syms') <- State
  ([Diagnosis], SignTHF, Set SymbolTHF)
  ([Diagnosis], SignTHF, Set SymbolTHF)
forall s. State s s
get
                     ([Diagnosis], SignTHF, Set SymbolTHF)
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall s. s -> State s ()
put ([Diagnosis]
diag', SignTHF
sig' { consts :: ConstMap
consts = Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c ConstInfo
ci (SignTHF -> ConstMap
consts SignTHF
sig')
                                      , symbols :: SymbolMap
symbols = Constant -> SymbolTHF -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c SymbolTHF
sym (SignTHF -> SymbolMap
symbols SignTHF
sig') }
                                      , SymbolTHF -> Set SymbolTHF -> Set SymbolTHF
forall a. Ord a => a -> Set a -> Set a
Set.insert SymbolTHF
sym Set SymbolTHF
syms')

-- Check if a type symbol is already inside the sig
sigHasTypeSymbol :: Constant -> SignTHF -> Bool
sigHasTypeSymbol :: Constant -> SignTHF -> Bool
sigHasTypeSymbol c :: Constant
c sig :: SignTHF
sig = Constant -> TypeMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Constant
c (SignTHF -> TypeMap
types SignTHF
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 :: Constant -> Kind -> SignTHF -> Bool
sigHasSameKind c :: Constant
c k :: Kind
k sig :: SignTHF
sig = TypeInfo -> Kind
typeKind (SignTHF -> TypeMap
types SignTHF
sig TypeMap -> Constant -> TypeInfo
forall k a. Ord k => Map k a -> k -> a
Map.! Constant
c) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k

-- Check if a const symbol is already inside the sig
sigHasConstSymbol :: Constant -> SignTHF -> Bool
sigHasConstSymbol :: Constant -> SignTHF -> Bool
sigHasConstSymbol c :: Constant
c sig :: SignTHF
sig = Constant -> ConstMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Constant
c (SignTHF -> ConstMap
consts SignTHF
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 :: Constant -> Type -> SignTHF -> Bool
sigHasSameType c :: Constant
c t :: Type
t sig :: SignTHF
sig = ConstInfo -> Type
constType (SignTHF -> ConstMap
consts SignTHF
sig ConstMap -> Constant -> ConstInfo
forall k a. Ord k => Map k a -> k -> a
Map.! Constant
c) Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
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 :: Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent t :: Type
t = do
 (_, sig :: SignTHF
sig, _) <- State
  ([Diagnosis], SignTHF, Set SymbolTHF)
  ([Diagnosis], SignTHF, Set SymbolTHF)
forall s. State s s
get
 case Type
t of
    MapType t1 :: Type
t1 t2 :: Type
t2 -> do
     Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent Type
t1
     Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent Type
t2
    ParType t1 :: Type
t1 -> Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent Type
t1
    CType c :: Constant
c -> Bool
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Constant -> SignTHF -> Bool
sigHasTypeSymbol Constant
c SignTHF
sig))
               (do
                 Constant
-> Name
-> Kind
-> Annotations
-> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
insertType Constant
c (Constant -> Name
N_Atomic_Word Constant
c) Kind
Kind Annotations
Null
                 Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
appandDiag (Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> Diagnosis -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> Constant -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "Unknown type: " Constant
c)
    ProdType ts :: [Type]
ts -> (Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ())
-> [Type] -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
isTypeConsistent [Type]
ts
    _ -> () -> State ([Diagnosis], SignTHF, Set SymbolTHF) ()
forall (m :: * -> *) a. Monad m => a -> m a
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 :: [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [] dn :: ([Diagnosis], [Named THFFormula])
dn = ([Diagnosis], [Named THFFormula])
dn
getSentences (t :: TPTP_THF
t : rt :: [TPTP_THF]
rt) dn :: ([Diagnosis], [Named THFFormula])
dn@(d :: [Diagnosis]
d, ns :: [Named THFFormula]
ns) = case TPTP_THF
t of
    TPTP_THF_Annotated_Formula _ fr :: FormulaRole
fr _ _ -> case FormulaRole
fr of
        Type -> [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt ([Diagnosis], [Named THFFormula])
dn
        Unknown ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'unknown\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        Plain ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'plain\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        Fi_Domain ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'fi_domain\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        Fi_Functors ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'fi_functors\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        Fi_Predicates ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'fi_predicates\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        Assumption ->
            let diag :: Diagnosis
diag = DiagKind -> String -> TPTP_THF -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                    "THFFormula with role \'assumption\' will be ignored." TPTP_THF
t
            in [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt (Diagnosis
diag Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
d, [Named THFFormula]
ns)
        _ ->
            let (d1 :: [Diagnosis]
d1, ns1 :: [Named THFFormula]
ns1) = [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt ([Diagnosis], [Named THFFormula])
dn
            in ([Diagnosis]
d1, TPTP_THF -> Named THFFormula
tptpthfToNS TPTP_THF
t Named THFFormula -> [Named THFFormula] -> [Named THFFormula]
forall a. a -> [a] -> [a]
: [Named THFFormula]
ns1)
    _ -> [TPTP_THF]
-> ([Diagnosis], [Named THFFormula])
-> ([Diagnosis], [Named THFFormula])
getSentences [TPTP_THF]
rt ([Diagnosis], [Named THFFormula])
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 :: TPTP_THF -> Named THFFormula
tptpthfToNS f :: TPTP_THF
f =
  let s :: Named THFFormula
s = String -> THFFormula -> Named THFFormula
forall a s. a -> s -> SenAttr s a
makeNamed (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ TPTP_THF -> Name
nameAF TPTP_THF
f) (TPTP_THF -> THFFormula
thfFormulaAF TPTP_THF
f)
      t :: Named THFFormula
t = Named THFFormula
s { isAxiom :: Bool
isAxiom = Bool
False }
      w :: Named THFFormula
w = Named THFFormula
s { wasTheorem :: Bool
wasTheorem = Bool
True }
  in case TPTP_THF -> FormulaRole
formulaRoleAF TPTP_THF
f of
    Definition -> Named THFFormula
s { isDef :: Bool
isDef = Bool
True }
    Conjecture -> Named THFFormula
t
    Negated_Conjecture -> Named THFFormula
t
    Theorem -> Named THFFormula
w
    Lemma -> Named THFFormula
w
    Hypothesis -> Named THFFormula
t
    _ -> Named THFFormula
s -- { isAxiom = True, isDef = False, wasTheorem = False }


{- -----------------------------------------------------------------------------
Get the Kind of a type
----------------------------------------------------------------------------- -}

makeKind :: THFFormula -> Either (Kind, Constant) Diagnosis
makeKind :: THFFormula -> Either (Kind, Constant) Diagnosis
makeKind t :: THFFormula
t = Either (Kind, Constant) Diagnosis
-> ((Kind, Constant) -> Either (Kind, Constant) Diagnosis)
-> Maybe (Kind, Constant)
-> Either (Kind, Constant) Diagnosis
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Diagnosis -> Either (Kind, Constant) Diagnosis
forall a b. b -> Either a b
Right (Diagnosis -> Either (Kind, Constant) Diagnosis)
-> Diagnosis -> Either (Kind, Constant) Diagnosis
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> THFFormula -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "Error while parsing the kind of:" THFFormula
t)
                (Kind, Constant) -> Either (Kind, Constant) Diagnosis
forall a b. a -> Either a b
Left (THFFormula -> Maybe (Kind, Constant)
thfFormulaToKind THFFormula
t)

thfFormulaToKind :: THFFormula -> Maybe (Kind, Constant)
thfFormulaToKind :: THFFormula -> Maybe (Kind, Constant)
thfFormulaToKind (T0F_THF_Typed_Const tc :: THFTypedConst
tc) = THFTypedConst -> Maybe (Kind, Constant)
thfTypedConstToKind THFTypedConst
tc
thfFormulaToKind _ = Maybe (Kind, Constant)
forall a. Maybe a
Nothing

thfTypedConstToKind :: THFTypedConst -> Maybe (Kind, Constant)
thfTypedConstToKind :: THFTypedConst -> Maybe (Kind, Constant)
thfTypedConstToKind (T0TC_THF_TypedConst_Par tcp :: THFTypedConst
tcp) = THFTypedConst -> Maybe (Kind, Constant)
thfTypedConstToKind THFTypedConst
tcp
thfTypedConstToKind (T0TC_Typed_Const c :: Constant
c tlt :: THFTopLevelType
tlt) =
            Maybe (Kind, Constant)
-> (Kind -> Maybe (Kind, Constant))
-> Maybe Kind
-> Maybe (Kind, Constant)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe (Kind, Constant)
forall a. Maybe a
Nothing (\ k :: Kind
k -> (Kind, Constant) -> Maybe (Kind, Constant)
forall a. a -> Maybe a
Just (Kind
k, Constant
c))
                (THFTopLevelType -> Maybe Kind
thfTopLevelTypeToKind THFTopLevelType
tlt)

thfTopLevelTypeToKind :: THFTopLevelType -> Maybe Kind
thfTopLevelTypeToKind :: THFTopLevelType -> Maybe Kind
thfTopLevelTypeToKind tlt :: THFTopLevelType
tlt = case THFTopLevelType
tlt of
    T0TLT_THF_Binary_Type bt :: THFBinaryType
bt -> THFBinaryType -> Maybe Kind
thfBinaryTypeToKind THFBinaryType
bt
    T0TLT_Defined_Type _ -> Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
Kind
    _ -> Maybe Kind
forall a. Maybe a
Nothing

thfBinaryTypeToKind :: THFBinaryType -> Maybe Kind
thfBinaryTypeToKind :: THFBinaryType -> Maybe Kind
thfBinaryTypeToKind bt :: THFBinaryType
bt = case THFBinaryType
bt of
    T0BT_THF_Binary_Type_Par btp :: THFBinaryType
btp -> THFBinaryType -> Maybe Kind
thfBinaryTypeToKind THFBinaryType
btp
    _ -> Maybe Kind
forall a. Maybe a
Nothing

{- -----------------------------------------------------------------------------
Get the Type of a constant
----------------------------------------------------------------------------- -}

makeType :: THFFormula -> Either (Type, Constant) Diagnosis
makeType :: THFFormula -> Either (Type, Constant) Diagnosis
makeType t :: THFFormula
t = Either (Type, Constant) Diagnosis
-> ((Type, Constant) -> Either (Type, Constant) Diagnosis)
-> Maybe (Type, Constant)
-> Either (Type, Constant) Diagnosis
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Diagnosis -> Either (Type, Constant) Diagnosis
forall a b. b -> Either a b
Right (Diagnosis -> Either (Type, Constant) Diagnosis)
-> Diagnosis -> Either (Type, Constant) Diagnosis
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> THFFormula -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "Error while parsing the type of:" THFFormula
t)
                (Type, Constant) -> Either (Type, Constant) Diagnosis
forall a b. a -> Either a b
Left (THFFormula -> Maybe (Type, Constant)
thfFormulaToType THFFormula
t)

thfFormulaToType :: THFFormula -> Maybe (Type, Constant)
thfFormulaToType :: THFFormula -> Maybe (Type, Constant)
thfFormulaToType (T0F_THF_Typed_Const tc :: THFTypedConst
tc) = THFTypedConst -> Maybe (Type, Constant)
thfTypedConstToType THFTypedConst
tc
thfFormulaToType _ = Maybe (Type, Constant)
forall a. Maybe a
Nothing

thfTypedConstToType :: THFTypedConst -> Maybe (Type, Constant)
thfTypedConstToType :: THFTypedConst -> Maybe (Type, Constant)
thfTypedConstToType (T0TC_THF_TypedConst_Par tcp :: THFTypedConst
tcp) = THFTypedConst -> Maybe (Type, Constant)
thfTypedConstToType THFTypedConst
tcp
thfTypedConstToType (T0TC_Typed_Const c :: Constant
c tlt :: THFTopLevelType
tlt) =
            Maybe (Type, Constant)
-> (Type -> Maybe (Type, Constant))
-> Maybe Type
-> Maybe (Type, Constant)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe (Type, Constant)
forall a. Maybe a
Nothing (\ t :: Type
t -> (Type, Constant) -> Maybe (Type, Constant)
forall a. a -> Maybe a
Just (Type
t, Constant
c))
                (THFTopLevelType -> Maybe Type
thfTopLevelTypeToType THFTopLevelType
tlt)

{- -----------------------------------------------------------------------------
Check if a THFFormula is a Type definition
----------------------------------------------------------------------------- -}

isKind :: THFFormula -> Bool
isKind :: THFFormula -> Bool
isKind tf :: THFFormula
tf = case THFFormula
tf of
    T0F_THF_Typed_Const tc :: THFTypedConst
tc -> THFTypedConst -> Bool
thfTypedConstIsKind THFTypedConst
tc
    _ -> Bool
False

thfTypedConstIsKind :: THFTypedConst -> Bool
thfTypedConstIsKind :: THFTypedConst -> Bool
thfTypedConstIsKind tc :: THFTypedConst
tc = case THFTypedConst
tc of
    T0TC_THF_TypedConst_Par tcp :: THFTypedConst
tcp -> THFTypedConst -> Bool
thfTypedConstIsKind THFTypedConst
tcp
    T0TC_Typed_Const _ tlt :: THFTopLevelType
tlt -> THFTopLevelType -> Bool
thfTopLevelTypeIsKind THFTopLevelType
tlt

thfTopLevelTypeIsKind :: THFTopLevelType -> Bool
thfTopLevelTypeIsKind :: THFTopLevelType -> Bool
thfTopLevelTypeIsKind tlt :: THFTopLevelType
tlt = case THFTopLevelType
tlt of
    T0TLT_THF_Binary_Type bt :: THFBinaryType
bt -> THFBinaryType -> Bool
thfBinaryTypeIsKind THFBinaryType
bt
    T0TLT_Defined_Type dt :: DefinedType
dt -> DefinedType -> Bool
thfDefinedTypeIsKind DefinedType
dt
    _ -> Bool
False

thfDefinedTypeIsKind :: DefinedType -> Bool
thfDefinedTypeIsKind :: DefinedType -> Bool
thfDefinedTypeIsKind dt :: DefinedType
dt = case DefinedType
dt of
    DT_tType -> Bool
True
    _ -> Bool
False

thfBinaryTypeIsKind :: THFBinaryType -> Bool
thfBinaryTypeIsKind :: THFBinaryType -> Bool
thfBinaryTypeIsKind bt :: THFBinaryType
bt = case THFBinaryType
bt of
    T0BT_THF_Binary_Type_Par btp :: THFBinaryType
btp -> THFBinaryType -> Bool
thfBinaryTypeIsKind THFBinaryType
btp
    _ -> Bool
False