7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{-# LANGUAGE DeriveDataTypeable #-}

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- |

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaModule : ./TPTP/Morphism.hs

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaDescription : Symbol-related functions for TPTP.

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaCopyright : (c) Eugen Kuksa University of Magdeburg 2017

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaLicense : GPLv2 or higher, see LICENSE.txt

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaMaintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaStability : provisional

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaPortability : non-portable (imports Logic)

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaSymbol-related functions for TPTP.

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-}

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksamodule TPTP.Morphism ( Morphism

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , symbolsOfSign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , symbolToId

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ) where

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport TPTP.AS

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport TPTP.Sign as Sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Common.DefaultMorphism

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Common.Id

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport qualified Data.Map as Map

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Data.Maybe

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport qualified Data.Set as Set

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksatype Morphism = DefaultMorphism Sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkSymbol :: Token -> SymbolType -> Symbol

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkSymbol i t = Symbol { symbolId = i , symbolType = t }

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksagatherTHFSymbols :: SymbolType -> THFTypeDeclarationMap -> Set.Set Symbol

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksagatherTHFSymbols symType = Set.map fromJust . Set.filter isJust .

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Set.map (\ x -> mkSymbolFromTHFType x symType) . Map.keysSet

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa where

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa mkSymbolFromTHFType :: THFTypeable -> SymbolType -> Maybe Symbol

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa mkSymbolFromTHFType x t = case x of

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTypeConstant c -> Just $ Symbol { symbolId = c, symbolType = t }

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTypeFormula _ -> Nothing

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkSymbolFromTFFType :: Untyped_atom -> SymbolType -> Symbol

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkSymbolFromTFFType x t = case x of

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UA_constant c -> Symbol { symbolId = c, symbolType = t }

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UA_system c -> Symbol { symbolId = c, symbolType = t }

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkToken :: Show a => a -> Token

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksamkToken = mkSimpleId . show

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasymbolsOfSign :: Sign -> Set.Set Symbol

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasymbolsOfSign sign = Set.unions [

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Set.map (\ x -> mkSymbol x Sign.Constant) $ constantSet sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbol (mkToken x) Sign.Number) $ numberSet sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbol x Sign.Proposition) $ propositionSet sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , gatherTHFSymbols Sign.TypeConstant $ thfTypeConstantMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbolFromTFFType x Sign.TypeConstant) $ Map.keysSet $ tffTypeConstantMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , gatherTHFSymbols Sign.Predicate $ thfPredicateMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbolFromTFFType x Sign.Predicate) $ Map.keysSet $ tffPredicateMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbol x Sign.Predicate) $ Map.keysSet $ fofPredicateMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , gatherTHFSymbols Sign.Function $ thfTypeFunctorMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Set.map (\ x -> mkSymbolFromTFFType x Sign.Function) $ Map.keysSet $ tffTypeFunctorMap sign

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ]

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasymbolToId :: Symbol -> Id

7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasymbolToId = simpleIdToId . symbolId