{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : ./TPTP/Sublogic.hs

Description : Data structures representing TPTP sublogics.

Copyright : (c) Eugen Kuksa University of Magdeburg 2017

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>

Stability : provisional

Data structures representing TPTP sublogics.

-}

module TPTP.Sublogic where

import TPTP.AS

import TPTP.Morphism

import TPTP.Sign

import Common.AS_Annotation (item)

import Common.DefaultMorphism

import Data.Data

import qualified Data.Map as Map

import qualified Data.Set as Set

-- | EPR -- Effectively Propositional CNF

data Sublogic = CNF -- Clausal Normal Form

| FOF -- First Order Form

-- | TCF

| TFF -- Typed First Order Form

-- | TFX

| THF -- Typed Higher Order Form

-- | TPI

deriving (Show, Ord, Eq, Data, Typeable)

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

- Special Sublogics

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

top :: Sublogic

top = THF

bottom :: Sublogic

bottom = CNF

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

- Utility functions

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

sublogicName :: Sublogic -> String

sublogicName = show

leastUpperBound :: Sublogic -> Sublogic -> Sublogic

leastUpperBound = max

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

- Determine sublogics

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

sublogicOfUnit :: Sublogic -> () -> Sublogic

sublogicOfUnit minimumSublogic () = minimumSublogic

sublogicOfBaiscSpec :: Sublogic -> BASIC_SPEC -> Sublogic

sublogicOfBaiscSpec minimumSublogic basicSpec = case basicSpec of

Basic_spec annotedTPTPs -> foldr leastUpperBound minimumSublogic $

map (sublogicOfTPTP . item) annotedTPTPs

where

sublogicOfTPTP :: TPTP -> Sublogic

sublogicOfTPTP tptp = case tptp of

TPTP tptp_inputs -> foldr leastUpperBound minimumSublogic $

map sublogicOfTPTPInput tptp_inputs

sublogicOfTPTPInput :: TPTP_input -> Sublogic

sublogicOfTPTPInput tptp_input = case tptp_input of

Annotated_formula annotated_formula ->

sublogicOfSentence minimumSublogic annotated_formula

_ -> minimumSublogic

sublogicOfSentence :: Sublogic -> Sentence -> Sublogic

sublogicOfSentence minimumSublogic sentence = case sentence of

AF_THF_Annotated _ -> leastUpperBound minimumSublogic THF

AF_TFX_Annotated _ -> leastUpperBound minimumSublogic THF

AF_TFF_Annotated _ -> leastUpperBound minimumSublogic TFF

AF_TCF_Annotated _ -> leastUpperBound minimumSublogic TFF

AF_FOF_Annotated _ -> leastUpperBound minimumSublogic FOF

AF_CNF_Annotated _ -> leastUpperBound minimumSublogic CNF

AF_TPI_Annotated _ -> leastUpperBound minimumSublogic THF

sublogicOfSymbol :: Sublogic -> Symbol -> Sublogic

sublogicOfSymbol minimumSublogic _ = minimumSublogic

sublogicOfSign :: Sublogic -> Sign -> Sublogic

sublogicOfSign minimumSublogic sign = case () of

_ | not $ Map.null $ thfTypeConstantMap sign -> THF

_ | not $ Map.null $ thfTypeFunctorMap sign -> THF

_ | not $ Map.null $ thfPredicateMap sign -> THF

_ | not $ Map.null $ thfSubtypeMap sign -> THF

_ | not $ Map.null $ tffTypeConstantMap sign -> TFF

_ | not $ Map.null $ tffTypeFunctorMap sign -> TFF

_ | not $ Map.null $ tffPredicateMap sign -> TFF

_ | not $ Map.null $ tffSubtypeMap sign -> TFF

_ | not $ Set.null $ numberSet sign -> TFF

_ | not $ Map.null $ fofPredicateMap sign -> FOF

_ | not $ Map.null $ fofFunctorMap sign -> FOF

_ -> minimumSublogic

sublogicOfMorphism :: Sublogic -> Morphism -> Sublogic

sublogicOfMorphism minimumSublogic morphism =

leastUpperBound

(sublogicOfSign minimumSublogic $ domOfDefaultMorphism morphism)

(sublogicOfSign minimumSublogic $ codOfDefaultMorphism morphism)

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

- Determine projections

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

-- TODO: complete the projections

projectSublogicBasicSpec :: Sublogic -> BASIC_SPEC -> BASIC_SPEC

projectSublogicBasicSpec _ basicSpec = basicSpec

projectSublogicSign :: Sublogic -> Sign -> Sign

projectSublogicSign _ sign = sign

projectSublogicSentence :: Sublogic -> Sentence -> Sentence

projectSublogicSentence _ sentence = sentence

projectSublogicMorphism :: Sublogic -> Morphism -> Morphism

projectSublogicMorphism _ morphism = morphism

projectSublogicMUnit :: Sublogic -> () -> Maybe ()

projectSublogicMUnit _ = Just

projectSublogicMSymbol :: Sublogic -> Symbol -> Maybe Symbol

projectSublogicMSymbol _ symbol = Just symbol