{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./THF/Logic_THF.hs
Description :  Instance of class Logic for THF.
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
               (c) Jonathan von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable (imports Logic)

Instance of class Logic for THF.
-}

module THF.Logic_THF where

import ATC.ProofTree ()

import Common.DefaultMorphism
import Common.ProofTree

import Data.Monoid ()
import Data.Map (isSubmapOf)
import qualified Data.Map (toList, foldr)
import qualified Data.Set (fromList)

import Logic.Logic

import THF.ATC_THF ()
import THF.Cons
import THF.As (THFFormula, TPTP_THF (..))
import THF.StaticAnalysisTHF
import THF.ProveLeoII
import THF.ProveIsabelle
import THF.ProveSatallax
import THF.Sign
import THF.Print
import THF.ParseTHF
import qualified THF.Sublogic as SL
import THF.Poly (getSymbols)
import THF.Utils (toId)

-- TODO implement more instance methods

data THF = THF deriving Int -> THF -> ShowS
[THF] -> ShowS
THF -> String
(Int -> THF -> ShowS)
-> (THF -> String) -> ([THF] -> ShowS) -> Show THF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [THF] -> ShowS
$cshowList :: [THF] -> ShowS
show :: THF -> String
$cshow :: THF -> String
showsPrec :: Int -> THF -> ShowS
$cshowsPrec :: Int -> THF -> ShowS
Show

instance Language THF where
    description :: THF -> String
description _ =
        "THF is a language for Higher Order Logic from the TPTP standard.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        "For further information please refer to" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        "http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"

instance Semigroup BasicSpecTHF where
    (BasicSpecTHF l1 :: [TPTP_THF]
l1) <> :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF
<> (BasicSpecTHF l2 :: [TPTP_THF]
l2) =
        [TPTP_THF] -> BasicSpecTHF
BasicSpecTHF ([TPTP_THF] -> BasicSpecTHF) -> [TPTP_THF] -> BasicSpecTHF
forall a b. (a -> b) -> a -> b
$ [TPTP_THF]
l1 [TPTP_THF] -> [TPTP_THF] -> [TPTP_THF]
forall a. [a] -> [a] -> [a]
++ [TPTP_THF]
l2
instance Monoid BasicSpecTHF where
    mempty :: BasicSpecTHF
mempty = [TPTP_THF] -> BasicSpecTHF
BasicSpecTHF []

instance Logic.Logic.Syntax THF BasicSpecTHF SymbolTHF () () where
    parse_basic_spec :: THF -> Maybe (PrefixMap -> AParser st BasicSpecTHF)
parse_basic_spec THF = (PrefixMap -> AParser st BasicSpecTHF)
-> Maybe (PrefixMap -> AParser st BasicSpecTHF)
forall a. a -> Maybe a
Just (\ _ -> ([TPTP_THF] -> BasicSpecTHF)
-> ParsecT String (AnnoState st) Identity [TPTP_THF]
-> AParser st BasicSpecTHF
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TPTP_THF] -> BasicSpecTHF
BasicSpecTHF ParsecT String (AnnoState st) Identity [TPTP_THF]
forall st. CharParser st [TPTP_THF]
parseTHF)
    -- remaining default implementations are fine!

instance Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF where
    map_sen :: THF -> MorphismTHF -> THFFormula -> Result THFFormula
map_sen THF _ = THFFormula -> Result THFFormula
forall (m :: * -> *) a. Monad m => a -> m a
return
    print_named :: THF -> Named THFFormula -> Doc
print_named THF = Maybe FormulaRole -> Named THFFormula -> Doc
printNamedSentenceTHF Maybe FormulaRole
forall a. Maybe a
Nothing
    symsOfSen :: THF -> SignTHF -> THFFormula -> [SymbolTHF]
symsOfSen THF = SignTHF -> THFFormula -> [SymbolTHF]
getSymbols
    sym_name :: THF -> SymbolTHF -> Id
sym_name THF = Constant -> Id
toId (Constant -> Id) -> (SymbolTHF -> Constant) -> SymbolTHF -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolTHF -> Constant
symId
    symKind :: THF -> SymbolTHF -> String
symKind THF s :: SymbolTHF
s = case SymbolTHF -> SymbolType
symType SymbolTHF
s of
                     ST_Type _ -> "type"
                     ST_Const _ -> "constant"
    sym_of :: THF -> SignTHF -> [Set SymbolTHF]
sym_of THF s :: SignTHF
s = [[SymbolTHF] -> Set SymbolTHF
forall a. Ord a => [a] -> Set a
Data.Set.fromList ([SymbolTHF] -> Set SymbolTHF)
-> (SignTHF -> [SymbolTHF]) -> SignTHF -> Set SymbolTHF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Constant, SymbolTHF) -> SymbolTHF)
-> [(Constant, SymbolTHF)] -> [SymbolTHF]
forall a b. (a -> b) -> [a] -> [b]
map (Constant, SymbolTHF) -> SymbolTHF
forall a b. (a, b) -> b
snd ([(Constant, SymbolTHF)] -> [SymbolTHF])
-> (SignTHF -> [(Constant, SymbolTHF)]) -> SignTHF -> [SymbolTHF]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Constant SymbolTHF -> [(Constant, SymbolTHF)]
forall k a. Map k a -> [(k, a)]
Data.Map.toList (Map Constant SymbolTHF -> [(Constant, SymbolTHF)])
-> (SignTHF -> Map Constant SymbolTHF)
-> SignTHF
-> [(Constant, SymbolTHF)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignTHF -> Map Constant SymbolTHF
symbols (SignTHF -> Set SymbolTHF) -> SignTHF -> Set SymbolTHF
forall a b. (a -> b) -> a -> b
$ SignTHF
s]
    {- negation THF _ =
    other default implementations are fine -}

instance StaticAnalysis THF BasicSpecTHF THFFormula () ()
               SignTHF MorphismTHF SymbolTHF () where
    basic_analysis :: THF
-> Maybe
     ((BasicSpecTHF, SignTHF, GlobalAnnos)
      -> Result
           (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]))
basic_analysis THF = ((BasicSpecTHF, SignTHF, GlobalAnnos)
 -> Result
      (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]))
-> Maybe
     ((BasicSpecTHF, SignTHF, GlobalAnnos)
      -> Result
           (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]))
forall a. a -> Maybe a
Just (BasicSpecTHF, SignTHF, GlobalAnnos)
-> Result
     (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
basicAnalysis
    empty_signature :: THF -> SignTHF
empty_signature THF = SignTHF
emptySign
    signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF
signature_union THF = SignTHF -> SignTHF -> Result SignTHF
sigUnion
    signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF
signatureDiff THF = SignTHF -> SignTHF -> Result SignTHF
sigDiff
    intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF
intersection THF = SignTHF -> SignTHF -> Result SignTHF
sigIntersect
    is_subsig :: THF -> SignTHF -> SignTHF -> Bool
is_subsig THF s1 :: SignTHF
s1 s2 :: SignTHF
s2 = Map Constant TypeInfo -> Map Constant TypeInfo -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Data.Map.isSubmapOf (SignTHF -> Map Constant TypeInfo
types SignTHF
s1) (SignTHF -> Map Constant TypeInfo
types SignTHF
s2) Bool -> Bool -> Bool
&&
                          Map Constant ConstInfo -> Map Constant ConstInfo -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Data.Map.isSubmapOf (SignTHF -> Map Constant ConstInfo
consts SignTHF
s1) (SignTHF -> Map Constant ConstInfo
consts SignTHF
s2)
    subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF
subsig_inclusion THF = SignTHF -> SignTHF -> Result MorphismTHF
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion

{- In order to find the LeoII prover there must be an entry in the
PATH environment variable leading to the leo executable
(The executable leo.opt is not supported. In this case there should be a link
called leo, or something like that.) -}
instance Logic THF SL.THFSl BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree where
    all_sublogics :: THF -> [THFSl]
all_sublogics THF = [THFSl]
SL.sublogics_all
    stability :: THF -> Stability
stability THF = Stability
Testing
    provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree]
provers THF =
      [ Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
leoIIProver, Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
isaProver, Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
nitpickProver, Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
refuteProver, Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
sledgehammerProver
      , Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
satallaxProver ]

-- Sublogics

instance SemiLatticeWithTop SL.THFSl where
 lub :: THFSl -> THFSl -> THFSl
lub = THFSl -> THFSl -> THFSl
SL.joinSL
 top :: THFSl
top = THFSl
SL.tHF

instance MinSublogic SL.THFSl BasicSpecTHF where
 minSublogic :: BasicSpecTHF -> THFSl
minSublogic (BasicSpecTHF xs :: [TPTP_THF]
xs) = (TPTP_THF -> THFSl -> THFSl) -> THFSl -> [TPTP_THF] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
SL.joinSL (THFSl -> THFSl -> THFSl)
-> (TPTP_THF -> THFSl) -> TPTP_THF -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (\ x :: TPTP_THF
x -> case TPTP_THF
x of
     TPTP_THF_Annotated_Formula _ _ f :: THFFormula
f _ -> THFFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFFormula
f
     _ -> THFSl
SL.tHF0
    )) THFSl
SL.tHF0 [TPTP_THF]
xs

instance SublogicName SL.THFSl where
 sublogicName :: THFSl -> String
sublogicName = THFSl -> String
forall a. Show a => a -> String
show

instance MinSublogic SL.THFSl SymbolTHF where
 minSublogic :: SymbolTHF -> THFSl
minSublogic _ = THFSl
SL.tHF0 -- actually implement this!

instance MinSublogic SL.THFSl () where
 minSublogic :: () -> THFSl
minSublogic _ = THFSl
SL.tHF0

instance MinSublogic SL.THFSl SignTHF where
 minSublogic :: SignTHF -> THFSl
minSublogic (Sign tp :: Map Constant TypeInfo
tp c :: Map Constant ConstInfo
c _) = THFSl -> THFSl -> THFSl
forall l. SemiLatticeWithTop l => l -> l -> l
lub ((TypeInfo -> THFSl -> THFSl)
-> THFSl -> Map Constant TypeInfo -> THFSl
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Data.Map.foldr
   (\ t :: TypeInfo
t sl :: THFSl
sl -> THFSl -> THFSl -> THFSl
forall l. SemiLatticeWithTop l => l -> l -> l
lub THFSl
sl (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ Kind -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic (Kind -> THFSl) -> Kind -> THFSl
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Kind
typeKind TypeInfo
t)
   THFSl
SL.tHF0 Map Constant TypeInfo
tp)
  ((ConstInfo -> THFSl -> THFSl)
-> THFSl -> Map Constant ConstInfo -> THFSl
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Data.Map.foldr
   (\ cs :: ConstInfo
cs sl :: THFSl
sl -> THFSl -> THFSl -> THFSl
forall l. SemiLatticeWithTop l => l -> l -> l
lub THFSl
sl (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ Type -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic (Type -> THFSl) -> Type -> THFSl
forall a b. (a -> b) -> a -> b
$ ConstInfo -> Type
constType ConstInfo
cs)
   THFSl
SL.tHF0 Map Constant ConstInfo
c)

instance MinSublogic SL.THFSl Type where
 minSublogic :: Type -> THFSl
minSublogic (ProdType tps :: [Type]
tps) = (Type -> THFSl -> THFSl) -> THFSl -> [Type] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
SL.joinSL (THFSl -> THFSl -> THFSl)
-> (Type -> THFSl) -> Type -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
SL.tHFP [Type]
tps
 minSublogic TType = THFSl
SL.tHF0
 minSublogic OType = THFSl
SL.tHF0
 minSublogic IType = THFSl
SL.tHF0
 minSublogic (MapType t1 :: Type
t1 t2 :: Type
t2) = THFSl -> THFSl -> THFSl
SL.joinSL (Type -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic Type
t1) (Type -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic Type
t2)
 minSublogic (CType _) = THFSl
SL.tHF0
 minSublogic (SType _) = THFSl
SL.tHF0
 minSublogic (VType _) = THFSl
SL.tHF0_P
 minSublogic (ParType t :: Type
t) = Type -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic Type
t

instance MinSublogic SL.THFSl Kind where
 minSublogic :: Kind -> THFSl
minSublogic Kind = THFSl
SL.tHF0

instance MinSublogic SL.THFSl MorphismTHF where
 minSublogic :: MorphismTHF -> THFSl
minSublogic (MkMorphism s1 :: SignTHF
s1 s2 :: SignTHF
s2) = THFSl -> THFSl -> THFSl
forall l. SemiLatticeWithTop l => l -> l -> l
lub (SignTHF -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic SignTHF
s1)
                                            (SignTHF -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic SignTHF
s2)

instance ProjectSublogicM SL.THFSl SymbolTHF where
 projectSublogicM :: THFSl -> SymbolTHF -> Maybe SymbolTHF
projectSublogicM _ _ = Maybe SymbolTHF
forall a. Maybe a
Nothing

instance ProjectSublogicM SL.THFSl () where
 projectSublogicM :: THFSl -> () -> Maybe ()
projectSublogicM _ _ = Maybe ()
forall a. Maybe a
Nothing

instance ProjectSublogic SL.THFSl SignTHF where
 projectSublogic :: THFSl -> SignTHF -> SignTHF
projectSublogic _ i :: SignTHF
i = SignTHF
i

instance ProjectSublogic SL.THFSl MorphismTHF where
 projectSublogic :: THFSl -> MorphismTHF -> MorphismTHF
projectSublogic _ i :: MorphismTHF
i = MorphismTHF
i

instance ProjectSublogic SL.THFSl BasicSpecTHF where
 projectSublogic :: THFSl -> BasicSpecTHF -> BasicSpecTHF
projectSublogic _ i :: BasicSpecTHF
i = BasicSpecTHF
i