{- |
Module      :  ./SoftFOL/StatAna.hs
Copyright   :  (c) Christian Maeder, Bremen 2015
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian Maeder
Stability   :  provisional
Portability :  portable

-}

module SoftFOL.StatAna (basicAnalysis) where

import Common.AS_Annotation (Named, makeNamed, SenAttr (..))
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import qualified Common.Lib.MapSet as MapSet
import Common.Result

import qualified Data.Map as Map
import qualified Data.Set as Set

import SoftFOL.Sign
import SoftFOL.Morphism

basicAnalysis :: ([TPTP], Sign, GlobalAnnos)
  -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
basicAnalysis :: ([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
basicAnalysis (sp :: [TPTP]
sp, sg :: Sign
sg, _) =
  let ns :: [Named Sentence]
ns = [TPTP] -> [Named Sentence]
toNamedSen [TPTP]
sp
      sig2 :: Sign
sig2 = (Named Sentence -> Sign -> Sign)
-> Sign -> [Named Sentence] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bool -> Set Sentence -> Sentence -> Sign -> Sign
addSyms Bool
True Set Sentence
forall a. Set a
Set.empty (Sentence -> Sign -> Sign)
-> (Named Sentence -> Sentence) -> Named Sentence -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) Sign
sg [Named Sentence]
ns
      sig3 :: Sign
sig3 = if Sign
sig2 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
emptySign then Sign
sig2 else Sign
sig2
           { sortMap :: SortMap
sortMap = SPIdentifier -> Maybe Generated -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
universeSort Maybe Generated
forall a. Maybe a
Nothing (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Sign -> SortMap
sortMap Sign
sig2 }
  in ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TPTP]
sp, Sign -> Set SFSymbol -> ExtSign Sign SFSymbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
sig3 (Set SFSymbol -> ExtSign Sign SFSymbol)
-> Set SFSymbol -> ExtSign Sign SFSymbol
forall a b. (a -> b) -> a -> b
$ Set SFSymbol -> Set SFSymbol -> Set SFSymbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set SFSymbol
symOf Sign
sig3) (Set SFSymbol -> Set SFSymbol) -> Set SFSymbol -> Set SFSymbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set SFSymbol
symOf Sign
sg, [Named Sentence]
ns)

toNamedSen :: [TPTP] -> [Named Sentence]
toNamedSen :: [TPTP] -> [Named Sentence]
toNamedSen = (TPTP -> [Named Sentence]) -> [TPTP] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((TPTP -> [Named Sentence]) -> [TPTP] -> [Named Sentence])
-> (TPTP -> [Named Sentence]) -> [TPTP] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ \ f :: TPTP
f -> case TPTP
f of
           FormAnno _ (Name n :: String
n) r :: Role
r t :: Sentence
t _ -> [
             let sen :: Named Sentence
sen = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
n Sentence
t
             in case Role
r of
                 Axiom -> Named Sentence
sen
                 Hypothesis -> Named Sentence
sen
                 Definition -> Named Sentence
sen { isAxiom :: Bool
isAxiom = Bool
False, isDef :: Bool
isDef = Bool
True}
                 Assumption -> Named Sentence
sen
                 Lemma -> Named Sentence
sen
                 Theorem -> Named Sentence
sen
                 _ -> Named Sentence
sen { isAxiom :: Bool
isAxiom = Bool
False } ]
           _ -> []

formulaSymbols :: [SPSymbol]
formulaSymbols :: [SPSymbol]
formulaSymbols =
  [ SPSymbol
SPOr
  , SPSymbol
SPAnd
  , SPSymbol
SPNot
  , SPSymbol
SPImplies
  , SPSymbol
SPImplied
  , SPSymbol
SPEquiv ]

universeSort :: SPIdentifier
universeSort :: SPIdentifier
universeSort = String -> SPIdentifier
mkSimpleId "U"

addSyms :: Bool -> Set.Set SPTerm -> SPTerm -> Sign -> Sign
addSyms :: Bool -> Set Sentence -> Sentence -> Sign -> Sign
addSyms isFormula :: Bool
isFormula boundVars :: Set Sentence
boundVars t :: Sentence
t sig :: Sign
sig = case Sentence
t of
  SPQuantTerm _ vs :: [Sentence]
vs f :: Sentence
f ->
    Bool -> Set Sentence -> Sentence -> Sign -> Sign
addSyms Bool
True (Set Sentence -> Set Sentence -> Set Sentence
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Sentence
boundVars (Set Sentence -> Set Sentence) -> Set Sentence -> Set Sentence
forall a b. (a -> b) -> a -> b
$ [Sentence] -> Set Sentence
forall a. Ord a => [a] -> Set a
Set.fromList [Sentence]
vs) Sentence
f Sign
sig
  SPComplexTerm ssym :: SPSymbol
ssym args :: [Sentence]
args ->
    let sig2 :: Sign
sig2 = (Sentence -> Sign -> Sign) -> Sign -> [Sentence] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bool -> Set Sentence -> Sentence -> Sign -> Sign
addSyms (SPSymbol -> [SPSymbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SPSymbol
ssym [SPSymbol]
formulaSymbols) Set Sentence
boundVars)
               Sign
sig [Sentence]
args
    in case SPSymbol
ssym of
       SPCustomSymbol sid :: SPIdentifier
sid | Bool -> Bool
not ([Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sentence]
args)
         Bool -> Bool -> Bool
|| Sentence -> Set Sentence -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Sentence
t Set Sentence
boundVars ->
           let pf :: [SPIdentifier]
pf = Int -> SPIdentifier -> [SPIdentifier]
forall a. Int -> a -> [a]
replicate ([Sentence] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sentence]
args) SPIdentifier
universeSort
           in if Bool
isFormula then Sign
sig2
                { predMap :: PredMap
predMap = SPIdentifier -> [SPIdentifier] -> PredMap -> PredMap
forall k a.
(Ord k, Ord a) =>
k -> a -> Map k (Set a) -> Map k (Set a)
MapSet.setInsert SPIdentifier
sid [SPIdentifier]
pf (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign -> PredMap
predMap Sign
sig2 }
           else Sign
sig2
                { funcMap :: FuncMap
funcMap = SPIdentifier
-> ([SPIdentifier], SPIdentifier) -> FuncMap -> FuncMap
forall k a.
(Ord k, Ord a) =>
k -> a -> Map k (Set a) -> Map k (Set a)
MapSet.setInsert SPIdentifier
sid ([SPIdentifier]
pf, SPIdentifier
universeSort)
                  (FuncMap -> FuncMap) -> FuncMap -> FuncMap
forall a b. (a -> b) -> a -> b
$ Sign -> FuncMap
funcMap Sign
sig2 }
       _ -> Sign
sig2