{- |
Module      :  ./SoftFOL/Morphism.hs
Description :  Symbol related functions for SoftFOL.
Copyright   :  (c) Klaus Luettich, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Functions for symbols of SoftFOL.
-}

module SoftFOL.Morphism (symOf, symsOfTerm, symbolToId) where

import SoftFOL.Sign

import Common.Id

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Monoid ()

symOf :: Sign -> Set.Set SFSymbol
symOf :: Sign -> Set SFSymbol
symOf sig :: Sign
sig =
    let opSymbs :: Set SFSymbol
opSymbs = [Set SFSymbol] -> Set SFSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SFSymbol] -> Set SFSymbol) -> [Set SFSymbol] -> Set SFSymbol
forall a b. (a -> b) -> a -> b
$ ((SPIdentifier, Set ([SPIdentifier], SPIdentifier))
 -> Set SFSymbol)
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
-> [Set SFSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier, Set ([SPIdentifier], SPIdentifier)) -> Set SFSymbol
toOpSymb ([(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
 -> [Set SFSymbol])
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
-> [Set SFSymbol]
forall a b. (a -> b) -> a -> b
$ Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
 -> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))])
-> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
funcMap Sign
sig
        predSymbs :: Set SFSymbol
predSymbs = [Set SFSymbol] -> Set SFSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SFSymbol] -> Set SFSymbol) -> [Set SFSymbol] -> Set SFSymbol
forall a b. (a -> b) -> a -> b
$ ((SPIdentifier, Set [SPIdentifier]) -> Set SFSymbol)
-> [(SPIdentifier, Set [SPIdentifier])] -> [Set SFSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier, Set [SPIdentifier]) -> Set SFSymbol
toPredSymb ([(SPIdentifier, Set [SPIdentifier])] -> [Set SFSymbol])
-> [(SPIdentifier, Set [SPIdentifier])] -> [Set SFSymbol]
forall a b. (a -> b) -> a -> b
$ Map SPIdentifier (Set [SPIdentifier])
-> [(SPIdentifier, Set [SPIdentifier])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SPIdentifier (Set [SPIdentifier])
 -> [(SPIdentifier, Set [SPIdentifier])])
-> Map SPIdentifier (Set [SPIdentifier])
-> [(SPIdentifier, Set [SPIdentifier])]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
sig
        sortSymbs :: Set SFSymbol
sortSymbs = (SPIdentifier -> SFSymbol) -> Set SPIdentifier -> Set SFSymbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SPIdentifier -> SFSymbol
toSortSymb (Set SPIdentifier -> Set SFSymbol)
-> Set SPIdentifier -> Set SFSymbol
forall a b. (a -> b) -> a -> b
$ Map SPIdentifier (Maybe Generated) -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet (Map SPIdentifier (Maybe Generated) -> Set SPIdentifier)
-> Map SPIdentifier (Maybe Generated) -> Set SPIdentifier
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Maybe Generated)
sortMap Sign
sig
    in [Set SFSymbol] -> Set SFSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set SFSymbol
opSymbs, Set SFSymbol
predSymbs, Set SFSymbol
sortSymbs]

toOpSymb :: (SPIdentifier, Set.Set ([SPIdentifier], SPIdentifier))
         -> Set.Set SFSymbol
toOpSymb :: (SPIdentifier, Set ([SPIdentifier], SPIdentifier)) -> Set SFSymbol
toOpSymb (ident :: SPIdentifier
ident, ts :: Set ([SPIdentifier], SPIdentifier)
ts) = (([SPIdentifier], SPIdentifier) -> SFSymbol)
-> Set ([SPIdentifier], SPIdentifier) -> Set SFSymbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ([SPIdentifier], SPIdentifier) -> SFSymbol
toSymb Set ([SPIdentifier], SPIdentifier)
ts
    where toSymb :: ([SPIdentifier], SPIdentifier) -> SFSymbol
toSymb (args :: [SPIdentifier]
args, res :: SPIdentifier
res) =
             SFSymbol :: SPIdentifier -> SFSymbType -> SFSymbol
SFSymbol { sym_ident :: SPIdentifier
sym_ident = SPIdentifier
ident
                      , sym_type :: SFSymbType
sym_type = [SPIdentifier] -> SPIdentifier -> SFSymbType
SFOpType [SPIdentifier]
args SPIdentifier
res}

toPredSymb :: (SPIdentifier, Set.Set [SPIdentifier]) -> Set.Set SFSymbol
toPredSymb :: (SPIdentifier, Set [SPIdentifier]) -> Set SFSymbol
toPredSymb (ident :: SPIdentifier
ident, ts :: Set [SPIdentifier]
ts) = ([SPIdentifier] -> SFSymbol) -> Set [SPIdentifier] -> Set SFSymbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map [SPIdentifier] -> SFSymbol
toSymb Set [SPIdentifier]
ts
    where toSymb :: [SPIdentifier] -> SFSymbol
toSymb args :: [SPIdentifier]
args =
             SFSymbol :: SPIdentifier -> SFSymbType -> SFSymbol
SFSymbol { sym_ident :: SPIdentifier
sym_ident = SPIdentifier
ident
                      , sym_type :: SFSymbType
sym_type = [SPIdentifier] -> SFSymbType
SFPredType [SPIdentifier]
args}

toSortSymb :: SPIdentifier -> SFSymbol
toSortSymb :: SPIdentifier -> SFSymbol
toSortSymb ident :: SPIdentifier
ident = SFSymbol :: SPIdentifier -> SFSymbType -> SFSymbol
SFSymbol { sym_ident :: SPIdentifier
sym_ident = SPIdentifier
ident
                            , sym_type :: SFSymbType
sym_type = SFSymbType
SFSortType}

symbolToId :: SFSymbol -> Id
symbolToId :: SFSymbol -> Id
symbolToId = SPIdentifier -> Id
simpleIdToId (SPIdentifier -> Id)
-> (SFSymbol -> SPIdentifier) -> SFSymbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SFSymbol -> SPIdentifier
sym_ident


idsOfTerm :: SPTerm -> Set.Set SPIdentifier
idsOfTerm :: SPTerm -> Set SPIdentifier
idsOfTerm (SPQuantTerm _ vars :: [SPTerm]
vars f :: SPTerm
f) = SPTerm -> Set SPIdentifier
idsOfTerm SPTerm
f Set SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ [Set SPIdentifier] -> Set SPIdentifier
forall a. Monoid a => [a] -> a
mconcat ((SPTerm -> Set SPIdentifier) -> [SPTerm] -> [Set SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Set SPIdentifier
idsOfTerm [SPTerm]
vars)
idsOfTerm (SPComplexTerm (SPCustomSymbol s :: SPIdentifier
s) args :: [SPTerm]
args) = 
  SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert SPIdentifier
s (Set SPIdentifier -> Set SPIdentifier)
-> Set SPIdentifier -> Set SPIdentifier
forall a b. (a -> b) -> a -> b
$ [Set SPIdentifier] -> Set SPIdentifier
forall a. Monoid a => [a] -> a
mconcat ([Set SPIdentifier] -> Set SPIdentifier)
-> [Set SPIdentifier] -> Set SPIdentifier
forall a b. (a -> b) -> a -> b
$ (SPTerm -> Set SPIdentifier) -> [SPTerm] -> [Set SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Set SPIdentifier
idsOfTerm [SPTerm]
args
idsOfTerm (SPComplexTerm _ args :: [SPTerm]
args) = [Set SPIdentifier] -> Set SPIdentifier
forall a. Monoid a => [a] -> a
mconcat ([Set SPIdentifier] -> Set SPIdentifier)
-> [Set SPIdentifier] -> Set SPIdentifier
forall a b. (a -> b) -> a -> b
$ (SPTerm -> Set SPIdentifier) -> [SPTerm] -> [Set SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map SPTerm -> Set SPIdentifier
idsOfTerm [SPTerm]
args

symsOfTerm :: Sign -> SPTerm -> Set.Set SFSymbol
symsOfTerm :: Sign -> SPTerm -> Set SFSymbol
symsOfTerm sig :: Sign
sig t :: SPTerm
t = (SFSymbol -> Bool) -> Set SFSymbol -> Set SFSymbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter SFSymbol -> Bool
in_term Set SFSymbol
sig_syms
   where sig_syms :: Set SFSymbol
sig_syms = Sign -> Set SFSymbol
symOf Sign
sig
         term_ids :: Set SPIdentifier
term_ids = SPTerm -> Set SPIdentifier
idsOfTerm SPTerm
t
         in_term :: SFSymbol -> Bool
in_term sy :: SFSymbol
sy = SFSymbol -> SPIdentifier
sym_ident SFSymbol
sy SPIdentifier -> Set SPIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SPIdentifier
term_ids