{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./TPTP/Morphism.hs
Description :  Symbol-related functions for TPTP.
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
Portability :  non-portable (imports Logic)

Symbol-related functions for TPTP.
-}

module TPTP.Morphism ( Morphism
                     , symbolsOfSign
                     , symbolToId
                     ) where

import TPTP.AS
import TPTP.Sign as Sign

import Common.DefaultMorphism
import Common.Id
import qualified Data.Map as Map

import Data.Maybe
import qualified Data.Set as Set

type Morphism = DefaultMorphism Sign

mkSymbol :: Token -> SymbolType -> Symbol
mkSymbol :: Token -> SymbolType -> Symbol
mkSymbol i :: Token
i t :: SymbolType
t = Symbol :: Token -> SymbolType -> Symbol
Symbol { symbolId :: Token
symbolId = Token
i , symbolType :: SymbolType
symbolType = SymbolType
t }

gatherTHFSymbols :: SymbolType -> THFTypeDeclarationMap -> Set.Set Symbol
gatherTHFSymbols :: SymbolType -> THFTypeDeclarationMap -> Set Symbol
gatherTHFSymbols symType :: SymbolType
symType = (Maybe Symbol -> Symbol) -> Set (Maybe Symbol) -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Maybe Symbol -> Symbol
forall a. HasCallStack => Maybe a -> a
fromJust (Set (Maybe Symbol) -> Set Symbol)
-> (THFTypeDeclarationMap -> Set (Maybe Symbol))
-> THFTypeDeclarationMap
-> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Symbol -> Bool) -> Set (Maybe Symbol) -> Set (Maybe Symbol)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Maybe Symbol -> Bool
forall a. Maybe a -> Bool
isJust (Set (Maybe Symbol) -> Set (Maybe Symbol))
-> (THFTypeDeclarationMap -> Set (Maybe Symbol))
-> THFTypeDeclarationMap
-> Set (Maybe Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (THFTypeable -> Maybe Symbol)
-> Set THFTypeable -> Set (Maybe Symbol)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: THFTypeable
x -> THFTypeable -> SymbolType -> Maybe Symbol
mkSymbolFromTHFType THFTypeable
x SymbolType
symType) (Set THFTypeable -> Set (Maybe Symbol))
-> (THFTypeDeclarationMap -> Set THFTypeable)
-> THFTypeDeclarationMap
-> Set (Maybe Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFTypeDeclarationMap -> Set THFTypeable
forall k a. Map k a -> Set k
Map.keysSet
  where
    mkSymbolFromTHFType :: THFTypeable -> SymbolType -> Maybe Symbol
    mkSymbolFromTHFType :: THFTypeable -> SymbolType -> Maybe Symbol
mkSymbolFromTHFType x :: THFTypeable
x t :: SymbolType
t = case THFTypeable
x of
      THFTypeConstant c :: Token
c -> Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> Maybe Symbol) -> Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Symbol :: Token -> SymbolType -> Symbol
Symbol { symbolId :: Token
symbolId = Token
c, symbolType :: SymbolType
symbolType = SymbolType
t }
      THFTypeFormula _ -> Maybe Symbol
forall a. Maybe a
Nothing

mkSymbolFromTFFType :: Untyped_atom -> SymbolType -> Symbol
mkSymbolFromTFFType :: Untyped_atom -> SymbolType -> Symbol
mkSymbolFromTFFType x :: Untyped_atom
x t :: SymbolType
t = case Untyped_atom
x of
  UA_constant c :: Token
c -> Symbol :: Token -> SymbolType -> Symbol
Symbol { symbolId :: Token
symbolId = Token
c, symbolType :: SymbolType
symbolType = SymbolType
t }
  UA_system c :: Token
c -> Symbol :: Token -> SymbolType -> Symbol
Symbol { symbolId :: Token
symbolId = Token
c, symbolType :: SymbolType
symbolType = SymbolType
t }

mkToken :: Show a => a -> Token
mkToken :: a -> Token
mkToken = String -> Token
mkSimpleId (String -> Token) -> (a -> String) -> a -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show

symbolsOfSign :: Sign -> Set.Set Symbol
symbolsOfSign :: Sign -> Set Symbol
symbolsOfSign sign :: Sign
sign = [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [
    (Token -> Symbol) -> Set Token -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Token
x -> Token -> SymbolType -> Symbol
mkSymbol Token
x SymbolType
Sign.Constant) (Set Token -> Set Symbol) -> Set Token -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
constantSet Sign
sign
  , (Number -> Symbol) -> Set Number -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Number
x -> Token -> SymbolType -> Symbol
mkSymbol (Number -> Token
forall a. Show a => a -> Token
mkToken Number
x) SymbolType
Sign.Number) (Set Number -> Set Symbol) -> Set Number -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Number
numberSet Sign
sign
  , (Token -> Symbol) -> Set Token -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Token
x -> Token -> SymbolType -> Symbol
mkSymbol Token
x SymbolType
Sign.Proposition) (Set Token -> Set Symbol) -> Set Token -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
propositionSet Sign
sign
  , SymbolType -> THFTypeDeclarationMap -> Set Symbol
gatherTHFSymbols SymbolType
Sign.TypeConstant (THFTypeDeclarationMap -> Set Symbol)
-> THFTypeDeclarationMap -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> THFTypeDeclarationMap
thfTypeConstantMap Sign
sign
  , (Untyped_atom -> Symbol) -> Set Untyped_atom -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Untyped_atom
x -> Untyped_atom -> SymbolType -> Symbol
mkSymbolFromTFFType Untyped_atom
x SymbolType
Sign.TypeConstant) (Set Untyped_atom -> Set Symbol) -> Set Untyped_atom -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall k a. Map k a -> Set k
Map.keysSet (Map Untyped_atom TFF_top_level_type -> Set Untyped_atom)
-> Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeConstantMap Sign
sign
  , SymbolType -> THFTypeDeclarationMap -> Set Symbol
gatherTHFSymbols SymbolType
Sign.Predicate (THFTypeDeclarationMap -> Set Symbol)
-> THFTypeDeclarationMap -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> THFTypeDeclarationMap
thfPredicateMap Sign
sign
  , (Untyped_atom -> Symbol) -> Set Untyped_atom -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Untyped_atom
x -> Untyped_atom -> SymbolType -> Symbol
mkSymbolFromTFFType Untyped_atom
x SymbolType
Sign.Predicate) (Set Untyped_atom -> Set Symbol) -> Set Untyped_atom -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall k a. Map k a -> Set k
Map.keysSet (Map Untyped_atom TFF_top_level_type -> Set Untyped_atom)
-> Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffPredicateMap Sign
sign
  , (Token -> Symbol) -> Set Token -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Token
x -> Token -> SymbolType -> Symbol
mkSymbol Token
x SymbolType
Sign.Predicate) (Set Token -> Set Symbol) -> Set Token -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Map Token (Set Int) -> Set Token
forall k a. Map k a -> Set k
Map.keysSet (Map Token (Set Int) -> Set Token)
-> Map Token (Set Int) -> Set Token
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set Int)
fofPredicateMap Sign
sign
  , SymbolType -> THFTypeDeclarationMap -> Set Symbol
gatherTHFSymbols SymbolType
Sign.Function (THFTypeDeclarationMap -> Set Symbol)
-> THFTypeDeclarationMap -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> THFTypeDeclarationMap
thfTypeFunctorMap Sign
sign
  , (Untyped_atom -> Symbol) -> Set Untyped_atom -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Untyped_atom
x -> Untyped_atom -> SymbolType -> Symbol
mkSymbolFromTFFType Untyped_atom
x SymbolType
Sign.Function) (Set Untyped_atom -> Set Symbol) -> Set Untyped_atom -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall k a. Map k a -> Set k
Map.keysSet (Map Untyped_atom TFF_top_level_type -> Set Untyped_atom)
-> Map Untyped_atom TFF_top_level_type -> Set Untyped_atom
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeFunctorMap Sign
sign
  ]

symbolToId :: Symbol -> Id
symbolToId :: Symbol -> Id
symbolToId = Token -> Id
simpleIdToId (Token -> Id) -> (Symbol -> Token) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Token
symbolId