hets/TPTP/Morphism.hs

{-# 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 i t = Symbol { symbolId = i , symbolType = t }

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

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

mkToken :: Show a => a -> Token
mkToken = mkSimpleId . show

symbolsOfSign :: Sign -> Set.Set Symbol
symbolsOfSign sign = Set.unions [
    Set.map (\ x -> mkSymbol x Sign.Constant) $ constantSet sign
  , Set.map (\ x -> mkSymbol (mkToken x) Sign.Number) $ numberSet sign
  , Set.map (\ x -> mkSymbol x Sign.Proposition) $ propositionSet sign
  , gatherTHFSymbols Sign.TypeConstant $ thfTypeConstantMap sign
  , Set.map (\ x -> mkSymbolFromTFFType x Sign.TypeConstant) $ Map.keysSet $ tffTypeConstantMap sign
  , gatherTHFSymbols Sign.Predicate $ thfPredicateMap sign
  , Set.map (\ x -> mkSymbolFromTFFType x Sign.Predicate) $ Map.keysSet $ tffPredicateMap sign
  , Set.map (\ x -> mkSymbol x Sign.Predicate) $ Map.keysSet $ fofPredicateMap sign
  , gatherTHFSymbols Sign.Function $ thfTypeFunctorMap sign
  , Set.map (\ x -> mkSymbolFromTFFType x Sign.Function) $ Map.keysSet $ tffTypeFunctorMap sign
  ]

symbolToId :: Symbol -> Id
symbolToId = simpleIdToId . symbolId