{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CASL/Sign.hs
Description :  CASL signatures and local environments for basic analysis
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

CASL signatures also serve as local environments for the basic static analysis
-}

module CASL.Sign where

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.ToDoc ()
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.State as State
import Common.Keywords
import Common.Id
import Common.Result
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Prec (mkPrecIntMap, PrecMap)
import Common.Doc
import Common.DocUtils

import Data.Data
import Data.Maybe (fromMaybe)
import Data.List (isPrefixOf)
import Control.Monad (when, unless)

-- constants have empty argument lists
data OpType = OpType {OpType -> OpKind
opKind :: OpKind, OpType -> [SORT]
opArgs :: [SORT], OpType -> SORT
opRes :: SORT}
              deriving (Int -> OpType -> ShowS
[OpType] -> ShowS
OpType -> String
(Int -> OpType -> ShowS)
-> (OpType -> String) -> ([OpType] -> ShowS) -> Show OpType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpType] -> ShowS
$cshowList :: [OpType] -> ShowS
show :: OpType -> String
$cshow :: OpType -> String
showsPrec :: Int -> OpType -> ShowS
$cshowsPrec :: Int -> OpType -> ShowS
Show, OpType -> OpType -> Bool
(OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool) -> Eq OpType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OpType -> OpType -> Bool
$c/= :: OpType -> OpType -> Bool
== :: OpType -> OpType -> Bool
$c== :: OpType -> OpType -> Bool
Eq, Eq OpType
Eq OpType =>
(OpType -> OpType -> Ordering)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> Bool)
-> (OpType -> OpType -> OpType)
-> (OpType -> OpType -> OpType)
-> Ord OpType
OpType -> OpType -> Bool
OpType -> OpType -> Ordering
OpType -> OpType -> OpType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OpType -> OpType -> OpType
$cmin :: OpType -> OpType -> OpType
max :: OpType -> OpType -> OpType
$cmax :: OpType -> OpType -> OpType
>= :: OpType -> OpType -> Bool
$c>= :: OpType -> OpType -> Bool
> :: OpType -> OpType -> Bool
$c> :: OpType -> OpType -> Bool
<= :: OpType -> OpType -> Bool
$c<= :: OpType -> OpType -> Bool
< :: OpType -> OpType -> Bool
$c< :: OpType -> OpType -> Bool
compare :: OpType -> OpType -> Ordering
$ccompare :: OpType -> OpType -> Ordering
$cp1Ord :: Eq OpType
Ord, Typeable, Typeable OpType
Constr
DataType
Typeable OpType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OpType -> c OpType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OpType)
-> (OpType -> Constr)
-> (OpType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OpType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType))
-> ((forall b. Data b => b -> b) -> OpType -> OpType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OpType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OpType -> r)
-> (forall u. (forall d. Data d => d -> u) -> OpType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> OpType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OpType -> m OpType)
-> Data OpType
OpType -> Constr
OpType -> DataType
(forall b. Data b => b -> b) -> OpType -> OpType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> OpType -> u
forall u. (forall d. Data d => d -> u) -> OpType -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
$cOpType :: Constr
$tOpType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapMp :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapM :: (forall d. Data d => d -> m d) -> OpType -> m OpType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OpType -> m OpType
gmapQi :: Int -> (forall d. Data d => d -> u) -> OpType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OpType -> u
gmapQ :: (forall d. Data d => d -> u) -> OpType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OpType -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r
gmapT :: (forall b. Data b => b -> b) -> OpType -> OpType
$cgmapT :: (forall b. Data b => b -> b) -> OpType -> OpType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OpType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OpType)
dataTypeOf :: OpType -> DataType
$cdataTypeOf :: OpType -> DataType
toConstr :: OpType -> Constr
$ctoConstr :: OpType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OpType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OpType -> c OpType
$cp1Data :: Typeable OpType
Data)

-- | result sort added to argument sorts
opSorts :: OpType -> [SORT]
opSorts :: OpType -> [SORT]
opSorts o :: OpType
o = OpType -> SORT
opRes OpType
o SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: OpType -> [SORT]
opArgs OpType
o

mkTotOpType :: [SORT] -> SORT -> OpType
mkTotOpType :: [SORT] -> SORT -> OpType
mkTotOpType = OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Total

sortToOpType :: SORT -> OpType
sortToOpType :: SORT -> OpType
sortToOpType = [SORT] -> SORT -> OpType
mkTotOpType []

isSingleArgOp :: OpType -> Bool
isSingleArgOp :: OpType -> Bool
isSingleArgOp = [SORT] -> Bool
forall a. [a] -> Bool
isSingle ([SORT] -> Bool) -> (OpType -> [SORT]) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> [SORT]
opArgs

data PredType = PredType {PredType -> [SORT]
predArgs :: [SORT]} deriving (Int -> PredType -> ShowS
[PredType] -> ShowS
PredType -> String
(Int -> PredType -> ShowS)
-> (PredType -> String) -> ([PredType] -> ShowS) -> Show PredType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PredType] -> ShowS
$cshowList :: [PredType] -> ShowS
show :: PredType -> String
$cshow :: PredType -> String
showsPrec :: Int -> PredType -> ShowS
$cshowsPrec :: Int -> PredType -> ShowS
Show, PredType -> PredType -> Bool
(PredType -> PredType -> Bool)
-> (PredType -> PredType -> Bool) -> Eq PredType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PredType -> PredType -> Bool
$c/= :: PredType -> PredType -> Bool
== :: PredType -> PredType -> Bool
$c== :: PredType -> PredType -> Bool
Eq, Eq PredType
Eq PredType =>
(PredType -> PredType -> Ordering)
-> (PredType -> PredType -> Bool)
-> (PredType -> PredType -> Bool)
-> (PredType -> PredType -> Bool)
-> (PredType -> PredType -> Bool)
-> (PredType -> PredType -> PredType)
-> (PredType -> PredType -> PredType)
-> Ord PredType
PredType -> PredType -> Bool
PredType -> PredType -> Ordering
PredType -> PredType -> PredType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PredType -> PredType -> PredType
$cmin :: PredType -> PredType -> PredType
max :: PredType -> PredType -> PredType
$cmax :: PredType -> PredType -> PredType
>= :: PredType -> PredType -> Bool
$c>= :: PredType -> PredType -> Bool
> :: PredType -> PredType -> Bool
$c> :: PredType -> PredType -> Bool
<= :: PredType -> PredType -> Bool
$c<= :: PredType -> PredType -> Bool
< :: PredType -> PredType -> Bool
$c< :: PredType -> PredType -> Bool
compare :: PredType -> PredType -> Ordering
$ccompare :: PredType -> PredType -> Ordering
$cp1Ord :: Eq PredType
Ord, Typeable, Typeable PredType
Constr
DataType
Typeable PredType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PredType -> c PredType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PredType)
-> (PredType -> Constr)
-> (PredType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PredType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredType))
-> ((forall b. Data b => b -> b) -> PredType -> PredType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PredType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PredType -> r)
-> (forall u. (forall d. Data d => d -> u) -> PredType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PredType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PredType -> m PredType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PredType -> m PredType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PredType -> m PredType)
-> Data PredType
PredType -> Constr
PredType -> DataType
(forall b. Data b => b -> b) -> PredType -> PredType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredType -> c PredType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PredType -> u
forall u. (forall d. Data d => d -> u) -> PredType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredType -> m PredType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredType -> m PredType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredType -> c PredType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredType)
$cPredType :: Constr
$tPredType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PredType -> m PredType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredType -> m PredType
gmapMp :: (forall d. Data d => d -> m d) -> PredType -> m PredType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredType -> m PredType
gmapM :: (forall d. Data d => d -> m d) -> PredType -> m PredType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredType -> m PredType
gmapQi :: Int -> (forall d. Data d => d -> u) -> PredType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredType -> u
gmapQ :: (forall d. Data d => d -> u) -> PredType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PredType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredType -> r
gmapT :: (forall b. Data b => b -> b) -> PredType -> PredType
$cgmapT :: (forall b. Data b => b -> b) -> PredType -> PredType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PredType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredType)
dataTypeOf :: PredType -> DataType
$cdataTypeOf :: PredType -> DataType
toConstr :: PredType -> Constr
$ctoConstr :: PredType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredType -> c PredType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredType -> c PredType
$cp1Data :: Typeable PredType
Data)

sortToPredType :: SORT -> PredType
sortToPredType :: SORT -> PredType
sortToPredType s :: SORT
s = [SORT] -> PredType
PredType [SORT
s]

isBinPredType :: PredType -> Bool
isBinPredType :: PredType -> Bool
isBinPredType (PredType l :: [SORT]
l) = case [SORT]
l of
  [_, _] -> Bool
True
  _ -> Bool
False

type OpMap = MapSet.MapSet OP_NAME OpType
type PredMap = MapSet.MapSet PRED_NAME PredType
type AnnoMap = MapSet.MapSet Symbol Annotation

data SymbType = SortAsItemType
              | SubsortAsItemType SORT -- special symbols for xml output
              | OpAsItemType OpType
                {- since symbols do not speak about totality, the totality
                information in OpType has to be ignored -}
              | PredAsItemType PredType
                deriving (Int -> SymbType -> ShowS
[SymbType] -> ShowS
SymbType -> String
(Int -> SymbType -> ShowS)
-> (SymbType -> String) -> ([SymbType] -> ShowS) -> Show SymbType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymbType] -> ShowS
$cshowList :: [SymbType] -> ShowS
show :: SymbType -> String
$cshow :: SymbType -> String
showsPrec :: Int -> SymbType -> ShowS
$cshowsPrec :: Int -> SymbType -> ShowS
Show, SymbType -> SymbType -> Bool
(SymbType -> SymbType -> Bool)
-> (SymbType -> SymbType -> Bool) -> Eq SymbType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymbType -> SymbType -> Bool
$c/= :: SymbType -> SymbType -> Bool
== :: SymbType -> SymbType -> Bool
$c== :: SymbType -> SymbType -> Bool
Eq, Eq SymbType
Eq SymbType =>
(SymbType -> SymbType -> Ordering)
-> (SymbType -> SymbType -> Bool)
-> (SymbType -> SymbType -> Bool)
-> (SymbType -> SymbType -> Bool)
-> (SymbType -> SymbType -> Bool)
-> (SymbType -> SymbType -> SymbType)
-> (SymbType -> SymbType -> SymbType)
-> Ord SymbType
SymbType -> SymbType -> Bool
SymbType -> SymbType -> Ordering
SymbType -> SymbType -> SymbType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SymbType -> SymbType -> SymbType
$cmin :: SymbType -> SymbType -> SymbType
max :: SymbType -> SymbType -> SymbType
$cmax :: SymbType -> SymbType -> SymbType
>= :: SymbType -> SymbType -> Bool
$c>= :: SymbType -> SymbType -> Bool
> :: SymbType -> SymbType -> Bool
$c> :: SymbType -> SymbType -> Bool
<= :: SymbType -> SymbType -> Bool
$c<= :: SymbType -> SymbType -> Bool
< :: SymbType -> SymbType -> Bool
$c< :: SymbType -> SymbType -> Bool
compare :: SymbType -> SymbType -> Ordering
$ccompare :: SymbType -> SymbType -> Ordering
$cp1Ord :: Eq SymbType
Ord, Typeable, Typeable SymbType
Constr
DataType
Typeable SymbType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SymbType -> c SymbType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymbType)
-> (SymbType -> Constr)
-> (SymbType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymbType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType))
-> ((forall b. Data b => b -> b) -> SymbType -> SymbType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymbType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymbType -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymbType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymbType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymbType -> m SymbType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymbType -> m SymbType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymbType -> m SymbType)
-> Data SymbType
SymbType -> Constr
SymbType -> DataType
(forall b. Data b => b -> b) -> SymbType -> SymbType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbType -> c SymbType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SymbType -> u
forall u. (forall d. Data d => d -> u) -> SymbType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymbType -> m SymbType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbType -> m SymbType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbType -> c SymbType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymbType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType)
$cPredAsItemType :: Constr
$cOpAsItemType :: Constr
$cSubsortAsItemType :: Constr
$cSortAsItemType :: Constr
$tSymbType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SymbType -> m SymbType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbType -> m SymbType
gmapMp :: (forall d. Data d => d -> m d) -> SymbType -> m SymbType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymbType -> m SymbType
gmapM :: (forall d. Data d => d -> m d) -> SymbType -> m SymbType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymbType -> m SymbType
gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymbType -> u
gmapQ :: (forall d. Data d => d -> u) -> SymbType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymbType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymbType -> r
gmapT :: (forall b. Data b => b -> b) -> SymbType -> SymbType
$cgmapT :: (forall b. Data b => b -> b) -> SymbType -> SymbType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymbType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymbType)
dataTypeOf :: SymbType -> DataType
$cdataTypeOf :: SymbType -> DataType
toConstr :: SymbType -> Constr
$ctoConstr :: SymbType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymbType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbType -> c SymbType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymbType -> c SymbType
$cp1Data :: Typeable SymbType
Data)

symbolKind :: SymbType -> SYMB_KIND
symbolKind :: SymbType -> SYMB_KIND
symbolKind t :: SymbType
t = case SymbType
t of
  OpAsItemType _ -> SYMB_KIND
Ops_kind
  PredAsItemType _ -> SYMB_KIND
Preds_kind
  _ -> SYMB_KIND
Sorts_kind

data Symbol = Symbol {Symbol -> SORT
symName :: Id, Symbol -> SymbType
symbType :: SymbType}
              deriving (Int -> Symbol -> ShowS
[Symbol] -> ShowS
Symbol -> String
(Int -> Symbol -> ShowS)
-> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symbol] -> ShowS
$cshowList :: [Symbol] -> ShowS
show :: Symbol -> String
$cshow :: Symbol -> String
showsPrec :: Int -> Symbol -> ShowS
$cshowsPrec :: Int -> Symbol -> ShowS
Show, Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq, Eq Symbol
Eq Symbol =>
(Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmax :: Symbol -> Symbol -> Symbol
>= :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c< :: Symbol -> Symbol -> Bool
compare :: Symbol -> Symbol -> Ordering
$ccompare :: Symbol -> Symbol -> Ordering
$cp1Ord :: Eq Symbol
Ord, Typeable, Typeable Symbol
Constr
DataType
Typeable Symbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Symbol -> c Symbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Symbol)
-> (Symbol -> Constr)
-> (Symbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Symbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol))
-> ((forall b. Data b => b -> b) -> Symbol -> Symbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> Symbol -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> Data Symbol
Symbol -> Constr
Symbol -> DataType
(forall b. Data b => b -> b) -> Symbol -> Symbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cSymbol :: Constr
$tSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapMp :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapM :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
$cgmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Symbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
dataTypeOf :: Symbol -> DataType
$cdataTypeOf :: Symbol -> DataType
toConstr :: Symbol -> Constr
$ctoConstr :: Symbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cp1Data :: Typeable Symbol
Data)

instance GetRange Symbol where
    getRange :: Symbol -> Range
getRange = SORT -> Range
forall a. GetRange a => a -> Range
getRange (SORT -> Range) -> (Symbol -> SORT) -> Symbol -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SORT
symName
    rangeSpan :: Symbol -> [Pos]
rangeSpan = SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan (SORT -> [Pos]) -> (Symbol -> SORT) -> Symbol -> [Pos]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SORT
symName

idToSortSymbol :: Id -> Symbol
idToSortSymbol :: SORT -> Symbol
idToSortSymbol idt :: SORT
idt = SORT -> SymbType -> Symbol
Symbol SORT
idt SymbType
SortAsItemType

idToOpSymbol :: Id -> OpType -> Symbol
idToOpSymbol :: SORT -> OpType -> Symbol
idToOpSymbol idt :: SORT
idt = SORT -> SymbType -> Symbol
Symbol SORT
idt (SymbType -> Symbol) -> (OpType -> SymbType) -> OpType -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> SymbType
OpAsItemType

idToPredSymbol :: Id -> PredType -> Symbol
idToPredSymbol :: SORT -> PredType -> Symbol
idToPredSymbol idt :: SORT
idt = SORT -> SymbType -> Symbol
Symbol SORT
idt (SymbType -> Symbol)
-> (PredType -> SymbType) -> PredType -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> SymbType
PredAsItemType

type CASLSign = Sign () ()

{- | the data type for the basic static analysis to accumulate variables,
sentences, symbols, diagnostics and annotations, that are removed or ignored
when looking at signatures from outside, i.e. during logic-independent
processing. -}
data Sign f e = Sign
    { Sign f e -> Rel SORT
sortRel :: Rel.Rel SORT
    -- ^ every sort is a subsort of itself
    , Sign f e -> Maybe (Rel SORT)
revSortRel :: Maybe (Rel.Rel SORT)
    -- ^ reverse sort relation for more efficient lookup of subsorts
    , Sign f e -> Set SORT
emptySortSet :: Set.Set SORT
    -- ^ a subset of the sort set of possibly empty sorts
    , Sign f e -> OpMap
opMap :: OpMap
    , Sign f e -> OpMap
assocOps :: OpMap -- ^ the subset of associative operators
    , Sign f e -> PredMap
predMap :: PredMap
    , Sign f e -> Map SIMPLE_ID SORT
varMap :: Map.Map SIMPLE_ID SORT -- ^ temporary variables
    , Sign f e -> [Named (FORMULA f)]
sentences :: [Named (FORMULA f)] -- ^ current sentences
    , Sign f e -> Set Symbol
declaredSymbols :: Set.Set Symbol -- ^ introduced or redeclared symbols
    , Sign f e -> [Diagnosis]
envDiags :: [Diagnosis] -- ^ diagnostics for basic spec
    , Sign f e -> AnnoMap
annoMap :: AnnoMap -- ^ annotated symbols
    , Sign f e -> GlobalAnnos
globAnnos :: GlobalAnnos -- ^ global annotations to use
    , Sign f e -> e
extendedInfo :: e
    } deriving (Int -> Sign f e -> ShowS
[Sign f e] -> ShowS
Sign f e -> String
(Int -> Sign f e -> ShowS)
-> (Sign f e -> String) -> ([Sign f e] -> ShowS) -> Show (Sign f e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f e. (Show f, Show e) => Int -> Sign f e -> ShowS
forall f e. (Show f, Show e) => [Sign f e] -> ShowS
forall f e. (Show f, Show e) => Sign f e -> String
showList :: [Sign f e] -> ShowS
$cshowList :: forall f e. (Show f, Show e) => [Sign f e] -> ShowS
show :: Sign f e -> String
$cshow :: forall f e. (Show f, Show e) => Sign f e -> String
showsPrec :: Int -> Sign f e -> ShowS
$cshowsPrec :: forall f e. (Show f, Show e) => Int -> Sign f e -> ShowS
Show, Typeable, Typeable (Sign f e)
Constr
DataType
Typeable (Sign f e) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sign f e -> c (Sign f e))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Sign f e))
-> (Sign f e -> Constr)
-> (Sign f e -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Sign f e)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Sign f e)))
-> ((forall b. Data b => b -> b) -> Sign f e -> Sign f e)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Sign f e -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Sign f e -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sign f e -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sign f e -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e))
-> Data (Sign f e)
Sign f e -> Constr
Sign f e -> DataType
(forall b. Data b => b -> b) -> Sign f e -> Sign f e
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign f e -> c (Sign f e)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sign f e)
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sign f e))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sign f e -> u
forall u. (forall d. Data d => d -> u) -> Sign f e -> [u]
forall f e. (Data f, Data e) => Typeable (Sign f e)
forall f e. (Data f, Data e) => Sign f e -> Constr
forall f e. (Data f, Data e) => Sign f e -> DataType
forall f e.
(Data f, Data e) =>
(forall b. Data b => b -> b) -> Sign f e -> Sign f e
forall f e u.
(Data f, Data e) =>
Int -> (forall d. Data d => d -> u) -> Sign f e -> u
forall f e u.
(Data f, Data e) =>
(forall d. Data d => d -> u) -> Sign f e -> [u]
forall f e r r'.
(Data f, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
forall f e r r'.
(Data f, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
forall f e (m :: * -> *).
(Data f, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
forall f e (m :: * -> *).
(Data f, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
forall f e (c :: * -> *).
(Data f, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sign f e)
forall f e (c :: * -> *).
(Data f, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign f e -> c (Sign f e)
forall f e (t :: * -> *) (c :: * -> *).
(Data f, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Sign f e))
forall f e (t :: * -> * -> *) (c :: * -> *).
(Data f, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sign f e))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sign f e)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign f e -> c (Sign f e)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Sign f e))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sign f e))
$cSign :: Constr
$tSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
$cgmapMo :: forall f e (m :: * -> *).
(Data f, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
gmapMp :: (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
$cgmapMp :: forall f e (m :: * -> *).
(Data f, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
gmapM :: (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
$cgmapM :: forall f e (m :: * -> *).
(Data f, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign f e -> u
$cgmapQi :: forall f e u.
(Data f, Data e) =>
Int -> (forall d. Data d => d -> u) -> Sign f e -> u
gmapQ :: (forall d. Data d => d -> u) -> Sign f e -> [u]
$cgmapQ :: forall f e u.
(Data f, Data e) =>
(forall d. Data d => d -> u) -> Sign f e -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
$cgmapQr :: forall f e r r'.
(Data f, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
$cgmapQl :: forall f e r r'.
(Data f, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sign f e -> r
gmapT :: (forall b. Data b => b -> b) -> Sign f e -> Sign f e
$cgmapT :: forall f e.
(Data f, Data e) =>
(forall b. Data b => b -> b) -> Sign f e -> Sign f e
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sign f e))
$cdataCast2 :: forall f e (t :: * -> * -> *) (c :: * -> *).
(Data f, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sign f e))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Sign f e))
$cdataCast1 :: forall f e (t :: * -> *) (c :: * -> *).
(Data f, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Sign f e))
dataTypeOf :: Sign f e -> DataType
$cdataTypeOf :: forall f e. (Data f, Data e) => Sign f e -> DataType
toConstr :: Sign f e -> Constr
$ctoConstr :: forall f e. (Data f, Data e) => Sign f e -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sign f e)
$cgunfold :: forall f e (c :: * -> *).
(Data f, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sign f e)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign f e -> c (Sign f e)
$cgfoldl :: forall f e (c :: * -> *).
(Data f, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign f e -> c (Sign f e)
$cp1Data :: forall f e. (Data f, Data e) => Typeable (Sign f e)
Data)

sortSet :: Sign f e -> Set.Set SORT
sortSet :: Sign f e -> Set SORT
sortSet = Rel SORT -> Set SORT
forall a. Rel a -> Set a
Rel.keysSet (Rel SORT -> Set SORT)
-> (Sign f e -> Rel SORT) -> Sign f e -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel

-- better ignore assoc flags for equality
instance Eq e => Eq (Sign f e) where
    a :: Sign f e
a == :: Sign f e -> Sign f e -> Bool
== b :: Sign f e
b = Sign f () -> Sign f () -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Sign f e
a {extendedInfo :: ()
extendedInfo = ()} Sign f e
b {extendedInfo :: ()
extendedInfo = ()} Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
      Bool -> Bool -> Bool
&& Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b

instance Ord e => Ord (Sign f e) where
  compare :: Sign f e -> Sign f e -> Ordering
compare a :: Sign f e
a b :: Sign f e
b = (Set SORT, Rel SORT, OpMap, PredMap, e)
-> (Set SORT, Rel SORT, OpMap, PredMap, e) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
    (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
a, Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
a, Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
a, Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
a, Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a)
    (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
b, Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
b, Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
b, Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
b, Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b)

emptySign :: e -> Sign f e
emptySign :: e -> Sign f e
emptySign e :: e
e = Sign :: forall f e.
Rel SORT
-> Maybe (Rel SORT)
-> Set SORT
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID SORT
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
Sign
    { sortRel :: Rel SORT
sortRel = Rel SORT
forall a. Rel a
Rel.empty
    , revSortRel :: Maybe (Rel SORT)
revSortRel = Maybe (Rel SORT)
forall a. Maybe a
Nothing
    , emptySortSet :: Set SORT
emptySortSet = Set SORT
forall a. Set a
Set.empty
    , opMap :: OpMap
opMap = OpMap
forall a b. MapSet a b
MapSet.empty
    , assocOps :: OpMap
assocOps = OpMap
forall a b. MapSet a b
MapSet.empty
    , predMap :: PredMap
predMap = PredMap
forall a b. MapSet a b
MapSet.empty
    , varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty
    , sentences :: [Named (FORMULA f)]
sentences = []
    , declaredSymbols :: Set Symbol
declaredSymbols = Set Symbol
forall a. Set a
Set.empty
    , envDiags :: [Diagnosis]
envDiags = []
    , annoMap :: AnnoMap
annoMap = AnnoMap
forall a b. MapSet a b
MapSet.empty
    , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
    , extendedInfo :: e
extendedInfo = e
e }

embedSign :: e -> Sign f1 e1 -> Sign f e
embedSign :: e -> Sign f1 e1 -> Sign f e
embedSign e :: e
e sign :: Sign f1 e1
sign = (e -> Sign f e
forall e f. e -> Sign f e
emptySign e
e)
    { sortRel :: Rel SORT
sortRel = Sign f1 e1 -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f1 e1
sign
    , opMap :: OpMap
opMap = Sign f1 e1 -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f1 e1
sign
    , assocOps :: OpMap
assocOps = Sign f1 e1 -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f1 e1
sign
    , predMap :: PredMap
predMap = Sign f1 e1 -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f1 e1
sign }

mapForm :: f -> FORMULA f1 -> FORMULA f
mapForm :: f -> FORMULA f1 -> FORMULA f
mapForm c :: f
c = Record f1 (FORMULA f) (TERM f) -> FORMULA f1 -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f1 (FORMULA f) (TERM f) -> FORMULA f1 -> FORMULA f)
-> Record f1 (FORMULA f) (TERM f) -> FORMULA f1 -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (f1 -> f) -> Record f1 (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord (f -> f1 -> f
forall a b. a -> b -> a
const f
c)

mapFORMULA :: FORMULA f1 -> FORMULA f
mapFORMULA :: FORMULA f1 -> FORMULA f
mapFORMULA = f -> FORMULA f1 -> FORMULA f
forall f f1. f -> FORMULA f1 -> FORMULA f
mapForm (f -> FORMULA f1 -> FORMULA f) -> f -> FORMULA f1 -> FORMULA f
forall a b. (a -> b) -> a -> b
$ String -> f
forall a. HasCallStack => String -> a
error "CASL.mapFORMULA"

embedTheory :: (FORMULA f1 -> FORMULA f) -> e
  -> (Sign f1 e1, [Named (FORMULA f1)])
  -> (Sign f e, [Named (FORMULA f)])
embedTheory :: (FORMULA f1 -> FORMULA f)
-> e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedTheory f :: FORMULA f1 -> FORMULA f
f e :: e
e (sign :: Sign f1 e1
sign, sens :: [Named (FORMULA f1)]
sens) =
  (e -> Sign f1 e1 -> Sign f e
forall e f1 e1 f. e -> Sign f1 e1 -> Sign f e
embedSign e
e Sign f1 e1
sign, (Named (FORMULA f1) -> Named (FORMULA f))
-> [Named (FORMULA f1)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f1 -> FORMULA f)
-> Named (FORMULA f1) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed FORMULA f1 -> FORMULA f
f) [Named (FORMULA f1)]
sens)

embedCASLTheory :: e -> (Sign f1 e1, [Named (FORMULA f1)])
  -> (Sign f e, [Named (FORMULA f)])
embedCASLTheory :: e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory = (FORMULA f1 -> FORMULA f)
-> e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
forall f1 f e e1.
(FORMULA f1 -> FORMULA f)
-> e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedTheory FORMULA f1 -> FORMULA f
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA

getSyntaxTable :: Sign f e -> (PrecMap, AssocMap)
getSyntaxTable :: Sign f e -> (PrecMap, AssocMap)
getSyntaxTable sig :: Sign f e
sig = let gannos :: GlobalAnnos
gannos = Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sig
                     in (Rel SORT -> PrecMap
mkPrecIntMap (Rel SORT -> PrecMap) -> Rel SORT -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel SORT
prec_annos GlobalAnnos
gannos, GlobalAnnos -> AssocMap
assoc_annos GlobalAnnos
gannos)

class SignExtension e where
    isSubSignExtension :: e -> e -> Bool

instance SignExtension () where
    isSubSignExtension :: () -> () -> Bool
isSubSignExtension _ _ = Bool
True

-- | proper subsorts (possibly excluding input sort)
subsortsOf :: SORT -> Sign f e -> Set.Set SORT
subsortsOf :: SORT -> Sign f e -> Set SORT
subsortsOf s :: SORT
s e :: Sign f e
e = case Sign f e -> Maybe (Rel SORT)
forall f e. Sign f e -> Maybe (Rel SORT)
revSortRel Sign f e
e of
  Nothing -> Rel SORT -> SORT -> Set SORT
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
e) SORT
s
  Just r :: Rel SORT
r -> Rel SORT -> SORT -> Set SORT
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel SORT
r SORT
s

setRevSortRel :: Sign f e -> Sign f e
setRevSortRel :: Sign f e -> Sign f e
setRevSortRel s :: Sign f e
s = Sign f e
s { revSortRel :: Maybe (Rel SORT)
revSortRel = Rel SORT -> Maybe (Rel SORT)
forall a. a -> Maybe a
Just (Rel SORT -> Maybe (Rel SORT))
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Maybe (Rel SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transpose (Rel SORT -> Maybe (Rel SORT)) -> Rel SORT -> Maybe (Rel SORT)
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
s }

-- | proper supersorts (possibly excluding input sort)
supersortsOf :: SORT -> Sign f e -> Set.Set SORT
supersortsOf :: SORT -> Sign f e -> Set SORT
supersortsOf s :: SORT
s e :: Sign f e
e = Rel SORT -> SORT -> Set SORT
forall a. Ord a => Rel a -> a -> Set a
Rel.succs (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
e) SORT
s

toOP_TYPE :: OpType -> OP_TYPE
toOP_TYPE :: OpType -> OP_TYPE
toOP_TYPE OpType { opArgs :: OpType -> [SORT]
opArgs = [SORT]
args, opRes :: OpType -> SORT
opRes = SORT
res, opKind :: OpType -> OpKind
opKind = OpKind
k } =
    OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
k [SORT]
args SORT
res Range
nullRange

toPRED_TYPE :: PredType -> PRED_TYPE
toPRED_TYPE :: PredType -> PRED_TYPE
toPRED_TYPE PredType { predArgs :: PredType -> [SORT]
predArgs = [SORT]
args } = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
args Range
nullRange

toOpType :: OP_TYPE -> OpType
toOpType :: OP_TYPE -> OpType
toOpType (Op_type k :: OpKind
k args :: [SORT]
args r :: SORT
r _) = OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
k [SORT]
args SORT
r

toPredType :: PRED_TYPE -> PredType
toPredType :: PRED_TYPE -> PredType
toPredType (Pred_type args :: [SORT]
args _) = [SORT] -> PredType
PredType [SORT]
args

instance Pretty OpType where
  pretty :: OpType -> Doc
pretty = OP_TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty (OP_TYPE -> Doc) -> (OpType -> OP_TYPE) -> OpType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> OP_TYPE
toOP_TYPE

instance Pretty PredType where
  pretty :: PredType -> Doc
pretty = PRED_TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty (PRED_TYPE -> Doc) -> (PredType -> PRED_TYPE) -> PredType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> PRED_TYPE
toPRED_TYPE

instance (Show f, Pretty e) => Pretty (Sign f e) where
    pretty :: Sign f e -> Doc
pretty = (e -> Doc) -> Sign f e -> Doc
forall e f. (e -> Doc) -> Sign f e -> Doc
printSign e -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty Symbol where
  pretty :: Symbol -> Doc
pretty sy :: Symbol
sy = let n :: Doc
n = SORT -> Doc
forall a. Pretty a => a -> Doc
pretty (Symbol -> SORT
symName Symbol
sy) in
    case Symbol -> SymbType
symbType Symbol
sy of
       SortAsItemType -> String -> Doc
keyword String
sortS Doc -> Doc -> Doc
<+> Doc
n
       SubsortAsItemType s :: SORT
s -> String -> Doc
keyword String
sortS Doc -> Doc -> Doc
<+> Doc
n Doc -> Doc -> Doc
<+> Doc
less Doc -> Doc -> Doc
<+> SORT -> Doc
forall a. Pretty a => a -> Doc
pretty SORT
s
       PredAsItemType pt :: PredType
pt -> String -> Doc
keyword String
predS Doc -> Doc -> Doc
<+> Doc
n Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> PredType -> Doc
forall a. Pretty a => a -> Doc
pretty PredType
pt
       OpAsItemType ot :: OpType
ot -> String -> Doc
keyword String
opS Doc -> Doc -> Doc
<+> Doc
n Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OpType -> Doc
forall a. Pretty a => a -> Doc
pretty OpType
ot

eqAndSubsorts :: Bool -> Rel.Rel SORT -> ([[SORT]], [(SORT, [SORT])])
eqAndSubsorts :: Bool -> Rel SORT -> ([[SORT]], [(SORT, [SORT])])
eqAndSubsorts groupSubsorts :: Bool
groupSubsorts srel :: Rel SORT
srel = let
  cs :: [Set SORT]
cs = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel SORT
srel
  in ( ([SORT] -> Bool) -> [[SORT]] -> [[SORT]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (Int -> Bool) -> ([SORT] -> Int) -> [SORT] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[SORT]] -> [[SORT]]) -> [[SORT]] -> [[SORT]]
forall a b. (a -> b) -> a -> b
$ (Set SORT -> [SORT]) -> [Set SORT] -> [[SORT]]
forall a b. (a -> b) -> [a] -> [b]
map Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList [Set SORT]
cs
     , Map SORT [SORT] -> [(SORT, [SORT])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SORT [SORT] -> [(SORT, [SORT])])
-> (Rel SORT -> Map SORT [SORT]) -> Rel SORT -> [(SORT, [SORT])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set SORT -> [SORT]) -> Map SORT (Set SORT) -> Map SORT [SORT]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Map SORT (Set SORT) -> Map SORT [SORT])
-> (Rel SORT -> Map SORT (Set SORT)) -> Rel SORT -> Map SORT [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Map SORT (Set SORT)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel SORT -> Map SORT (Set SORT))
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Map SORT (Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.rmNullSets
       (Rel SORT -> Rel SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
groupSubsorts then Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transpose else Rel SORT -> Rel SORT
forall a. a -> a
id)
       (Rel SORT -> Rel SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel SORT -> Rel SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel SORT -> [(SORT, [SORT])]) -> Rel SORT -> [(SORT, [SORT])]
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Rel SORT -> Rel SORT
forall a. Ord a => [Set a] -> Rel a -> Rel a
Rel.collaps [Set SORT]
cs Rel SORT
srel)

singleAndRelatedSorts :: Rel.Rel SORT -> ([SORT], [[SORT]])
singleAndRelatedSorts :: Rel SORT -> ([SORT], [[SORT]])
singleAndRelatedSorts srel :: Rel SORT
srel = let
  ss :: Set SORT
ss = Rel SORT -> Set SORT
forall a. Rel a -> Set a
Rel.keysSet Rel SORT
srel
  rs :: [Set SORT]
rs = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure
     (Rel SORT -> [Set SORT])
-> (Rel SORT -> Rel SORT) -> Rel SORT -> [Set SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel SORT
srel (Rel SORT -> [Set SORT]) -> Rel SORT -> [Set SORT]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transpose Rel SORT
srel
  is :: Set SORT
is = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
ss (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set SORT]
rs
  in (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
is, (Set SORT -> [SORT]) -> [Set SORT] -> [[SORT]]
forall a b. (a -> b) -> [a] -> [b]
map Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList [Set SORT]
rs)

printSign :: (e -> Doc) -> Sign f e -> Doc
printSign :: (e -> Doc) -> Sign f e -> Doc
printSign fE :: e -> Doc
fE s :: Sign f e
s = let
  printRel :: (SORT, [a]) -> Doc
printRel (supersort :: SORT
supersort, subsorts :: [a]
subsorts) =
            [a] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [a]
subsorts Doc -> Doc -> Doc
<+> String -> Doc
text String
lessS Doc -> Doc -> Doc
<+>
               SORT -> Doc
idDoc SORT
supersort
  esorts :: Set SORT
esorts = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
s
  srel :: Rel SORT
srel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
s
  (es :: [[SORT]]
es, ss :: [(SORT, [SORT])]
ss) = Bool -> Rel SORT -> ([[SORT]], [(SORT, [SORT])])
eqAndSubsorts Bool
True Rel SORT
srel
  nsorts :: Set SORT
nsorts = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
s) Set SORT
esorts in
    (if Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
nsorts then Doc
empty else String -> Doc
text (String
sortS String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+>
       [Doc] -> Doc
sepByCommas ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
nsorts))) Doc -> Doc -> Doc
$+$
    (if Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
esorts then Doc
empty else String -> Doc
text (String
esortS String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+>
       [Doc] -> Doc
sepByCommas ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
esorts))) Doc -> Doc -> Doc
$+$
    (if Rel SORT -> Bool
forall a. Ord a => Rel a -> Bool
Rel.noPairs Rel SORT
srel then Doc
empty
      else String -> Doc
text (String
sortS String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+>
       [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
          ([SORT] -> Doc) -> [[SORT]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Doc] -> Doc
fsep ([Doc] -> Doc) -> ([SORT] -> [Doc]) -> [SORT] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
equals) ([Doc] -> [Doc]) -> ([SORT] -> [Doc]) -> [SORT] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
forall a. Pretty a => a -> Doc
pretty) [[SORT]]
es
         [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((SORT, [SORT]) -> Doc) -> [(SORT, [SORT])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, [SORT]) -> Doc
forall a. Pretty a => (SORT, [a]) -> Doc
printRel [(SORT, [SORT])]
ss))
    Doc -> Doc -> Doc
$+$ Doc -> Doc -> Map SORT (Set OpType) -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
text String
opS) Doc
empty (OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (OpMap -> Map SORT (Set OpType)) -> OpMap -> Map SORT (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
s)
    Doc -> Doc -> Doc
$+$ Doc -> Doc -> Map SORT (Set PredType) -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
text String
predS) Doc
space (PredMap -> Map SORT (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (PredMap -> Map SORT (Set PredType))
-> PredMap -> Map SORT (Set PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
s)
    Doc -> Doc -> Doc
$+$ e -> Doc
fE (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
s)

-- working with Sign

closeSortRel :: Sign f e -> Sign f e
closeSortRel :: Sign f e -> Sign f e
closeSortRel s :: Sign f e
s =
  Sign f e
s { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
s }

nonEmptySortSet :: Sign f e -> Set.Set Id
nonEmptySortSet :: Sign f e -> Set SORT
nonEmptySortSet s :: Sign f e
s = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
s) (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
s

-- op kinds of op types

setOpKind :: OpKind -> OpType -> OpType
setOpKind :: OpKind -> OpType -> OpType
setOpKind k :: OpKind
k o :: OpType
o = OpType
o { opKind :: OpKind
opKind = OpKind
k }

mkPartial :: OpType -> OpType
mkPartial :: OpType -> OpType
mkPartial = OpKind -> OpType -> OpType
setOpKind OpKind
Partial

mkTotal :: OpType -> OpType
mkTotal :: OpType -> OpType
mkTotal = OpKind -> OpType -> OpType
setOpKind OpKind
Total

isTotal :: OpType -> Bool
isTotal :: OpType -> Bool
isTotal = (OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Total) (OpKind -> Bool) -> (OpType -> OpKind) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> OpKind
opKind

isPartial :: OpType -> Bool
isPartial :: OpType -> Bool
isPartial = Bool -> Bool
not (Bool -> Bool) -> (OpType -> Bool) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> Bool
isTotal

makePartial :: Set.Set OpType -> Set.Set OpType
makePartial :: Set OpType -> Set OpType
makePartial = (OpType -> OpType) -> Set OpType -> Set OpType
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic OpType -> OpType
mkPartial

-- | remove (True) or add (False) partial op if it is included as total
rmOrAddParts :: Bool -> Set.Set OpType -> Set.Set OpType
rmOrAddParts :: Bool -> Set OpType -> Set OpType
rmOrAddParts b :: Bool
b s :: Set OpType
s =
  let t :: Set OpType
t = Set OpType -> Set OpType
makePartial (Set OpType -> Set OpType) -> Set OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ (OpType -> Bool) -> Set OpType -> Set OpType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter OpType -> Bool
isTotal Set OpType
s
  in (if Bool
b then Set OpType -> Set OpType -> Set OpType
forall a. Ord a => Set a -> Set a -> Set a
Set.difference else Set OpType -> Set OpType -> Set OpType
forall a. Ord a => Set a -> Set a -> Set a
Set.union) Set OpType
s Set OpType
t

rmOrAddPartsMap :: Bool -> OpMap -> OpMap
rmOrAddPartsMap :: Bool -> OpMap -> OpMap
rmOrAddPartsMap b :: Bool
b = (Set OpType -> Set OpType) -> OpMap -> OpMap
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Bool -> Set OpType -> Set OpType
rmOrAddParts Bool
b)

diffMapSet :: PredMap -> PredMap -> PredMap
diffMapSet :: PredMap -> PredMap -> PredMap
diffMapSet = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference

diffOpMapSet :: OpMap -> OpMap -> OpMap
diffOpMapSet :: OpMap -> OpMap -> OpMap
diffOpMapSet m :: OpMap
m = OpMap -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference OpMap
m (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
False

diffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig dif :: e -> e -> e
dif a :: Sign f e
a b :: Sign f e
b = let s :: Set SORT
s = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
b in
  Sign f e -> Sign f e
forall f e. Sign f e -> Sign f e
closeSortRel Sign f e
a
  { emptySortSet :: Set SORT
emptySortSet = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
s
      (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
b
  , sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.difference (Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
a)
      (Rel SORT -> Rel SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
b
  , opMap :: OpMap
opMap = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
a OpMap -> OpMap -> OpMap
`diffOpMapSet` Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
b
  , assocOps :: OpMap
assocOps = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
a OpMap -> OpMap -> OpMap
`diffOpMapSet` Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
b
  , predMap :: PredMap
predMap = Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
a PredMap -> PredMap -> PredMap
`diffMapSet` Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
b
  , annoMap :: AnnoMap
annoMap = Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
a AnnoMap -> AnnoMap -> AnnoMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
`MapSet.difference` Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
b
  , extendedInfo :: e
extendedInfo = e -> e -> e
dif (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b }
  {- transClosure needed:  {a < b < c} - {a < c; b}
  is not transitive! -}

addOpMapSet :: OpMap -> OpMap -> OpMap
addOpMapSet :: OpMap -> OpMap -> OpMap
addOpMapSet m :: OpMap
m = Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
True (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union OpMap
m

addMapSet :: PredMap -> PredMap -> PredMap
addMapSet :: PredMap -> PredMap -> PredMap
addMapSet = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union

addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig ad :: e -> e -> e
ad a :: Sign f e
a b :: Sign f e
b = let s :: Set SORT
s = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
b in
  Sign f e -> Sign f e
forall f e. Sign f e -> Sign f e
closeSortRel Sign f e
a
  { emptySortSet :: Set SORT
emptySortSet = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
s
      (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
b
  , sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
a) (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
b
  , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
addOpMapSet (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
b
  , assocOps :: OpMap
assocOps = OpMap -> OpMap -> OpMap
addOpMapSet (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
b
  , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
b
  , annoMap :: AnnoMap
annoMap = AnnoMap -> AnnoMap -> AnnoMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union (Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
a) (AnnoMap -> AnnoMap) -> AnnoMap -> AnnoMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
b
  , extendedInfo :: e
extendedInfo = e -> e -> e
ad (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b }

uniteCASLSign :: CASLSign -> CASLSign -> CASLSign
uniteCASLSign :: CASLSign -> CASLSign -> CASLSign
uniteCASLSign = (() -> () -> ()) -> CASLSign -> CASLSign -> CASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig (\ _ _ -> ())

interRel :: (Show a, Ord a) => Rel.Rel a -> Rel.Rel a -> Rel.Rel a
interRel :: Rel a -> Rel a -> Rel a
interRel a :: Rel a
a =
  Set (a, a) -> Rel a
forall a. Ord a => Set (a, a) -> Rel a
Rel.fromSet
  (Set (a, a) -> Rel a) -> (Rel a -> Set (a, a)) -> Rel a -> Rel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (a, a) -> Set (a, a) -> Set (a, a)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (Rel a -> Set (a, a)
forall a. Ord a => Rel a -> Set (a, a)
Rel.toSet Rel a
a) (Set (a, a) -> Set (a, a))
-> (Rel a -> Set (a, a)) -> Rel a -> Set (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel a -> Set (a, a)
forall a. Ord a => Rel a -> Set (a, a)
Rel.toSet

interOpMapSet :: OpMap -> OpMap -> OpMap
interOpMapSet :: OpMap -> OpMap -> OpMap
interOpMapSet m :: OpMap
m = Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
True
   (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.intersection (Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
False OpMap
m) (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
False

interMapSet :: PredMap -> PredMap -> PredMap
interMapSet :: PredMap -> PredMap -> PredMap
interMapSet = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.intersection

interSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig ef :: e -> e -> e
ef a :: Sign f e
a b :: Sign f e
b = let s :: Set SORT
s = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
b in
  Sign f e -> Sign f e
forall f e. Sign f e -> Sign f e
closeSortRel Sign f e
a
  { emptySortSet :: Set SORT
emptySortSet = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
s
      (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
a Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
nonEmptySortSet Sign f e
b
  , sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. (Show a, Ord a) => Rel a -> Rel a -> Rel a
interRel (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
a) (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
b
  , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
interOpMapSet (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
b
  , assocOps :: OpMap
assocOps = OpMap -> OpMap -> OpMap
interOpMapSet (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
b
  , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
interMapSet (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
b
  , annoMap :: AnnoMap
annoMap = AnnoMap -> AnnoMap -> AnnoMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.intersection (Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
a) (AnnoMap -> AnnoMap) -> AnnoMap -> AnnoMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
b
  , extendedInfo :: e
extendedInfo = e -> e -> e
ef (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b }

isSubOpMap :: OpMap -> OpMap -> Bool
isSubOpMap :: OpMap -> OpMap -> Bool
isSubOpMap m :: OpMap
m = (Set OpType -> Set OpType -> Bool)
-> Map SORT (Set OpType) -> Map SORT (Set OpType) -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy (\ s :: Set OpType
s t :: Set OpType
t -> (OpType -> Bool) -> Set OpType -> Bool
forall a. (a -> Bool) -> Set a -> Bool
MapSet.setAll
    (\ e :: OpType
e -> OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
e Set OpType
t Bool -> Bool -> Bool
|| OpType -> Bool
isPartial OpType
e Bool -> Bool -> Bool
&& OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OpType -> OpType
mkTotal OpType
e) Set OpType
t)
    Set OpType
s) (OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
m) (Map SORT (Set OpType) -> Bool)
-> (OpMap -> Map SORT (Set OpType)) -> OpMap -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

isSubMap :: PredMap -> PredMap -> Bool
isSubMap :: PredMap -> PredMap -> Bool
isSubMap = PredMap -> PredMap -> Bool
forall a b. (Ord a, Ord b) => MapSet a b -> MapSet a b -> Bool
MapSet.isSubmapOf

isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig isSubExt :: e -> e -> Bool
isSubExt a :: Sign f e
a b :: Sign f e
b =
  Rel SORT -> Rel SORT -> Bool
forall a. Ord a => Rel a -> Rel a -> Bool
Rel.isSubrelOf (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
a) (Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
b)
         -- ignore empty sort sorts
  Bool -> Bool -> Bool
&& OpMap -> OpMap -> Bool
isSubOpMap (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
a) (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
b)
         -- ignore associativity properties!
  Bool -> Bool -> Bool
&& PredMap -> PredMap -> Bool
isSubMap (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
a) (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
b)
  Bool -> Bool -> Bool
&& e -> e -> Bool
isSubExt (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b)

mapSetToList :: MapSet.MapSet a b -> [(a, b)]
mapSetToList :: MapSet a b -> [(a, b)]
mapSetToList = MapSet a b -> [(a, b)]
forall a b. MapSet a b -> [(a, b)]
MapSet.toPairList

addDiags :: [Diagnosis] -> State.State (Sign f e) ()
addDiags :: [Diagnosis] -> State (Sign f e) ()
addDiags ds :: [Diagnosis]
ds = do
  Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
  Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { envDiags :: [Diagnosis]
envDiags = [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign f e
e }

addAnnoSet :: Annoted a -> Symbol -> State.State (Sign f e) ()
addAnnoSet :: Annoted a -> Symbol -> State (Sign f e) ()
addAnnoSet a :: Annoted a
a s :: Symbol
s = do
  Symbol -> State (Sign f e) ()
forall f e. Symbol -> State (Sign f e) ()
addSymbol Symbol
s
  let v :: Set Annotation
v = Set Annotation -> Set Annotation -> Set Annotation
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([Annotation] -> Set Annotation
forall a. Ord a => [a] -> Set a
Set.fromList ([Annotation] -> Set Annotation) -> [Annotation] -> Set Annotation
forall a b. (a -> b) -> a -> b
$ Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted a
a) (Set Annotation -> Set Annotation)
-> Set Annotation -> Set Annotation
forall a b. (a -> b) -> a -> b
$ [Annotation] -> Set Annotation
forall a. Ord a => [a] -> Set a
Set.fromList ([Annotation] -> Set Annotation) -> [Annotation] -> Set Annotation
forall a b. (a -> b) -> a -> b
$ Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted a
a
  Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Annotation -> Bool
forall a. Set a -> Bool
Set.null Set Annotation
v) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ do
    Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
    Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { annoMap :: AnnoMap
annoMap = (Set Annotation -> Set Annotation) -> Symbol -> AnnoMap -> AnnoMap
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update (Set Annotation -> Set Annotation -> Set Annotation
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Annotation
v) Symbol
s (AnnoMap -> AnnoMap) -> AnnoMap -> AnnoMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
e }

addSymbol :: Symbol -> State.State (Sign f e) ()
addSymbol :: Symbol -> State (Sign f e) ()
addSymbol s :: Symbol
s = do
  Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
  Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put (Sign f e -> State (Sign f e) ())
-> Sign f e -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ Sign f e -> Symbol -> Sign f e
forall e f. Sign e f -> Symbol -> Sign e f
addSymbToDeclSymbs Sign f e
e Symbol
s

addSymbToDeclSymbs :: Sign e f -> Symbol -> Sign e f
addSymbToDeclSymbs :: Sign e f -> Symbol -> Sign e f
addSymbToDeclSymbs cs :: Sign e f
cs sy :: Symbol
sy =
    Sign e f
cs { declaredSymbols :: Set Symbol
declaredSymbols = Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
sy (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign e f -> Set Symbol
forall f e. Sign f e -> Set Symbol
declaredSymbols Sign e f
cs }

addSort :: SortsKind -> Annoted a -> SORT -> State.State (Sign f e) ()
addSort :: SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort sk :: SortsKind
sk a :: Annoted a
a s :: SORT
s = do
  Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
  let r :: Rel SORT
r = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
e
      em :: Set SORT
em = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
e
      known :: Bool
known = SORT -> Rel SORT -> Bool
forall a. Ord a => a -> Rel a -> Bool
Rel.memberKey SORT
s Rel SORT
r
  if Bool
known then [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared sort" SORT
s]
    else do
      Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
s Rel SORT
r }
      [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ SORT -> [Diagnosis]
checkNamePrefix SORT
s
  case SortsKind
sk of
    NonEmptySorts -> Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s Set SORT
em) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ do
        Sign f e
e2 <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
        Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e2 { emptySortSet :: Set SORT
emptySortSet = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.delete SORT
s Set SORT
em }
        [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "redeclared sort as non-empty" SORT
s]
    PossiblyEmptySorts -> if Bool
known then
      [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "non-empty sort remains non-empty" SORT
s]
      else do
        Sign f e
e2 <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
        Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e2 { emptySortSet :: Set SORT
emptySortSet = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
s Set SORT
em }
  Annoted a -> Symbol -> State (Sign f e) ()
forall a f e. Annoted a -> Symbol -> State (Sign f e) ()
addAnnoSet Annoted a
a (Symbol -> State (Sign f e) ()) -> Symbol -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ SORT -> SymbType -> Symbol
Symbol SORT
s SymbType
SortAsItemType

hasSort :: Sign f e -> SORT -> [Diagnosis]
hasSort :: Sign f e -> SORT -> [Diagnosis]
hasSort e :: Sign f e
e s :: SORT
s =
    [ DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown sort" SORT
s
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
e ]

checkSorts :: [SORT] -> State.State (Sign f e) ()
checkSorts :: [SORT] -> State (Sign f e) ()
checkSorts s :: [SORT]
s = do
  Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
  [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> [Diagnosis]) -> [SORT] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign f e -> SORT -> [Diagnosis]
forall f e. Sign f e -> SORT -> [Diagnosis]
hasSort Sign f e
e) [SORT]
s

addSubsort :: SORT -> SORT -> State.State (Sign f e) ()
addSubsort :: SORT -> SORT -> State (Sign f e) ()
addSubsort = Bool -> SORT -> SORT -> State (Sign f e) ()
forall f e. Bool -> SORT -> SORT -> State (Sign f e) ()
addSubsortOrIso Bool
True

addSubsortOrIso :: Bool -> SORT -> SORT -> State.State (Sign f e) ()
addSubsortOrIso :: Bool -> SORT -> SORT -> State (Sign f e) ()
addSubsortOrIso b :: Bool
b super :: SORT
super sub :: SORT
sub = do
  Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [SORT] -> State (Sign f e) ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT
super, SORT
sub]
  Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
  let r :: Rel SORT
r = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
e
  Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { sortRel :: Rel SORT
sortRel = (if Bool
b then Rel SORT -> Rel SORT
forall a. a -> a
id else SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair SORT
super SORT
sub)
                (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair SORT
sub SORT
super Rel SORT
r }
  let p :: Range
p = SORT -> Range
posOfId SORT
sub
      rel :: String
rel = " '" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
sub (if Bool
b then " < " else " = ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
super "'"
  if SORT
super SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sub then [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "void reflexive subsort" SORT
sub]
    else if Bool
b then
      if SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
super SORT
sub Rel SORT
r then
        [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ if SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
sub SORT
super Rel SORT
r
                   then [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning ("sorts are isomorphic" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) Range
p]
                   else [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning ("added subsort cycle by" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) Range
p]
      else Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
sub SORT
super Rel SORT
r)
           (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Hint ("redeclared subsort" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) Range
p]
    else if SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
super SORT
sub Rel SORT
r then
      [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ if SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
sub SORT
super Rel SORT
r
                 then [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Hint ("redeclared isomoprhic sorts" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) Range
p]
                 else [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning ("subsort '" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                  SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
super "' made isomorphic by" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ SORT -> Range
posOfId SORT
super]
    else Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path SORT
sub SORT
super Rel SORT
r)
         (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning ("subsort  '" String -> ShowS
forall a. [a] -> [a] -> [a]
++
           SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
sub "' made isomorphic by" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rel) Range
p]

closeSubsortRel :: State.State (Sign f e) ()
closeSubsortRel :: State (Sign f e) ()
closeSubsortRel =
    do Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
       Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
e }

checkNamePrefix :: Id -> [Diagnosis]
checkNamePrefix :: SORT -> [Diagnosis]
checkNamePrefix i :: SORT
i =
    [ DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "identifier may conflict with generated names" SORT
i
    | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
genNamePrefix (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> ShowS
showId SORT
i ""]

alsoWarning :: String -> String -> Id -> [Diagnosis]
alsoWarning :: String -> String -> SORT -> [Diagnosis]
alsoWarning new :: String
new old :: String
old i :: SORT
i = let is :: String
is = ' ' Char -> ShowS
forall a. a -> [a] -> [a]
: SORT -> ShowS
showId SORT
i "'" in
    [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning ("new '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
new String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
is String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is also known as '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
old String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
is)
     (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ SORT -> Range
posOfId SORT
i]

checkWithMap :: String -> String -> Map.Map Id a -> Id -> [Diagnosis]
checkWithMap :: String -> String -> Map SORT a -> SORT -> [Diagnosis]
checkWithMap s1 :: String
s1 s2 :: String
s2 m :: Map SORT a
m i :: SORT
i = if SORT -> Map SORT a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SORT
i Map SORT a
m then String -> String -> SORT -> [Diagnosis]
alsoWarning String
s1 String
s2 SORT
i else []

checkWithOtherMap :: String -> String -> MapSet.MapSet Id a -> Id -> [Diagnosis]
checkWithOtherMap :: String -> String -> MapSet SORT a -> SORT -> [Diagnosis]
checkWithOtherMap s1 :: String
s1 s2 :: String
s2 = String -> String -> Map SORT (Set a) -> SORT -> [Diagnosis]
forall a. String -> String -> Map SORT a -> SORT -> [Diagnosis]
checkWithMap String
s1 String
s2 (Map SORT (Set a) -> SORT -> [Diagnosis])
-> (MapSet SORT a -> Map SORT (Set a))
-> MapSet SORT a
-> SORT
-> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet SORT a -> Map SORT (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

addVars :: VAR_DECL -> State.State (Sign f e) ()
addVars :: VAR_DECL -> State (Sign f e) ()
addVars (Var_decl vs :: [SIMPLE_ID]
vs s :: SORT
s _) = do
    [SORT] -> State (Sign f e) ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT
s]
    (SIMPLE_ID -> State (Sign f e) ())
-> [SIMPLE_ID] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SORT -> SIMPLE_ID -> State (Sign f e) ()
forall f e. SORT -> SIMPLE_ID -> State (Sign f e) ()
addVar SORT
s) [SIMPLE_ID]
vs

addVar :: SORT -> SIMPLE_ID -> State.State (Sign f e) ()
addVar :: SORT -> SIMPLE_ID -> State (Sign f e) ()
addVar s :: SORT
s v :: SIMPLE_ID
v =
    do Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
State.get
       let m :: Map SIMPLE_ID SORT
m = Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
e
           i :: SORT
i = SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
v
           ds :: [Diagnosis]
ds = case SIMPLE_ID -> Map SIMPLE_ID SORT -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SIMPLE_ID
v Map SIMPLE_ID SORT
m of
                Just _ -> [DiagKind -> String -> SIMPLE_ID -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "known variable shadowed" SIMPLE_ID
v]
                Nothing -> []
       Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
State.put Sign f e
e { varMap :: Map SIMPLE_ID SORT
varMap = SIMPLE_ID -> SORT -> Map SIMPLE_ID SORT -> Map SIMPLE_ID SORT
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SIMPLE_ID
v SORT
s Map SIMPLE_ID SORT
m }
       [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> String -> OpMap -> SORT -> [Diagnosis]
forall a. String -> String -> MapSet SORT a -> SORT -> [Diagnosis]
checkWithOtherMap String
varS String
opS (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
e) SORT
i
                [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> String -> PredMap -> SORT -> [Diagnosis]
forall a. String -> String -> MapSet SORT a -> SORT -> [Diagnosis]
checkWithOtherMap String
varS String
predS (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
e) SORT
i
                [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ SORT -> [Diagnosis]
checkNamePrefix SORT
i

addOpTo :: Id -> OpType -> OpMap -> OpMap
addOpTo :: SORT -> OpType -> OpMap -> OpMap
addOpTo = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert

type VarSet = Set.Set (VAR, SORT)

{- | extract the sort and free variables from an analysed term. The input
signature for free variables is (currently only) used for statements in the
VSE logic. The conversion for boolean terms to formulas is only used for FPL.
-}
class TermExtension f where
  freeVarsOfExt :: Sign f e -> f -> VarSet
  freeVarsOfExt _ = VarSet -> f -> VarSet
forall a b. a -> b -> a
const VarSet
forall a. Set a
Set.empty

  optTermSort :: f -> Maybe SORT
  optTermSort = Maybe SORT -> f -> Maybe SORT
forall a b. a -> b -> a
const Maybe SORT
forall a. Maybe a
Nothing

  sortOfTerm :: f -> SORT
  sortOfTerm = SORT -> Maybe SORT -> SORT
forall a. a -> Maybe a -> a
fromMaybe (String -> SORT
genName "unknown") (Maybe SORT -> SORT) -> (f -> Maybe SORT) -> f -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort

  termToFormula :: TERM f -> Result (FORMULA f)
  termToFormula = Result (FORMULA f) -> TERM f -> Result (FORMULA f)
forall a b. a -> b -> a
const (Result (FORMULA f) -> TERM f -> Result (FORMULA f))
-> Result (FORMULA f) -> TERM f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe (FORMULA f) -> Result (FORMULA f)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe (FORMULA f)
forall a. Maybe a
Nothing

instance TermExtension ()

instance TermExtension f => TermExtension (TERM f) where
  optTermSort :: TERM f -> Maybe SORT
optTermSort = (f -> Maybe SORT) -> TERM f -> Maybe SORT
forall f. (f -> Maybe SORT) -> TERM f -> Maybe SORT
optSortOfTerm f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort

optSortOfTerm :: (f -> Maybe SORT) -> TERM f -> Maybe SORT
optSortOfTerm :: (f -> Maybe SORT) -> TERM f -> Maybe SORT
optSortOfTerm f :: f -> Maybe SORT
f term :: TERM f
term = case TERM f
term of
    Qual_var _ ty :: SORT
ty _ -> SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
ty
    Application (Qual_op_name _ ot :: OP_TYPE
ot _) _ _ -> SORT -> Maybe SORT
forall a. a -> Maybe a
Just (SORT -> Maybe SORT) -> SORT -> Maybe SORT
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ot
    Sorted_term _ ty :: SORT
ty _ -> SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
ty
    Cast _ ty :: SORT
ty _ -> SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
ty
    Conditional t1 :: TERM f
t1 _ _ _ -> (f -> Maybe SORT) -> TERM f -> Maybe SORT
forall f. (f -> Maybe SORT) -> TERM f -> Maybe SORT
optSortOfTerm f -> Maybe SORT
f TERM f
t1
    ExtTERM t :: f
t -> f -> Maybe SORT
f f
t
    _ -> Maybe SORT
forall a. Maybe a
Nothing

mkAxName :: String -> SORT -> SORT -> String
mkAxName :: String -> SORT -> SORT -> String
mkAxName str :: String
str s :: SORT
s s' :: SORT
s' = "ga_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_to_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s'

mkAxNameSingle :: String -> SORT -> String
mkAxNameSingle :: String -> SORT -> String
mkAxNameSingle str :: String
str s :: SORT
s = "ga_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s

mkSortGenName :: [SORT] -> String
mkSortGenName :: [SORT] -> String
mkSortGenName sl :: [SORT]
sl = "ga_generated_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS -> (SORT -> ShowS) -> [SORT] -> ShowS
forall a. ShowS -> (a -> ShowS) -> [a] -> ShowS
showSepList (String -> ShowS
showString "_") SORT -> ShowS
showId [SORT]
sl ""

{- | The sort generation constraint is given a generated name,
built from the sort list -}
toSortGenNamed :: FORMULA f -> [SORT] -> Named (FORMULA f)
toSortGenNamed :: FORMULA f -> [SORT] -> Named (FORMULA f)
toSortGenNamed f :: FORMULA f
f sl :: [SORT]
sl = String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ([SORT] -> String
mkSortGenName [SORT]
sl) FORMULA f
f

getConstructors :: [Named (FORMULA f)] -> Set.Set (Id, OpType)
getConstructors :: [Named (FORMULA f)] -> Set (SORT, OpType)
getConstructors = (Named (FORMULA f) -> Set (SORT, OpType) -> Set (SORT, OpType))
-> Set (SORT, OpType) -> [Named (FORMULA f)] -> Set (SORT, OpType)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: Named (FORMULA f)
f s :: Set (SORT, OpType)
s -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
f of
   Sort_gen_ax cs :: [Constraint]
cs _ -> let
       (_, ops :: [OP_SYMB]
ops, _) = [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax [Constraint]
cs
       in (OP_SYMB -> Set (SORT, OpType) -> Set (SORT, OpType))
-> Set (SORT, OpType) -> [OP_SYMB] -> Set (SORT, OpType)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ o :: OP_SYMB
o -> case OP_SYMB
o of
             Qual_op_name i :: SORT
i t :: OP_TYPE
t _ ->
               (SORT, OpType) -> Set (SORT, OpType) -> Set (SORT, OpType)
forall a. Ord a => a -> Set a -> Set a
Set.insert (SORT
i, OpType -> OpType
mkPartial (OpType -> OpType) -> OpType -> OpType
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
t)
             _ -> Set (SORT, OpType) -> Set (SORT, OpType)
forall a. a -> a
id)
             Set (SORT, OpType)
s [OP_SYMB]
ops
   _ -> Set (SORT, OpType)
s) Set (SORT, OpType)
forall a. Set a
Set.empty

-- | adds a symbol to a given signature
addSymbToSign :: Sign e f -> Symbol -> Result (Sign e f)
addSymbToSign :: Sign e f -> Symbol -> Result (Sign e f)
addSymbToSign sig :: Sign e f
sig sy :: Symbol
sy =
    let addSort' :: Sign f e -> SORT -> Sign f e
addSort' cs :: Sign f e
cs s :: SORT
s =
            Sign f e
cs { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
s (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
cs }
        addToMap' :: MapSet a b -> a -> b -> MapSet a b
addToMap' m :: MapSet a b
m n :: a
n t :: b
t = a -> b -> MapSet a b -> MapSet a b
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert a
n b
t MapSet a b
m
        addOp' :: Sign f e -> SORT -> OpType -> Sign f e
addOp' cs :: Sign f e
cs n :: SORT
n ot :: OpType
ot = Sign f e
cs { opMap :: OpMap
opMap = OpMap -> SORT -> OpType -> OpMap
forall a b. (Ord a, Ord b) => MapSet a b -> a -> b -> MapSet a b
addToMap' (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
cs) SORT
n OpType
ot }
        addPred' :: Sign f e -> SORT -> PredType -> Sign f e
addPred' cs :: Sign f e
cs n :: SORT
n pt :: PredType
pt = Sign f e
cs { predMap :: PredMap
predMap = PredMap -> SORT -> PredType -> PredMap
forall a b. (Ord a, Ord b) => MapSet a b -> a -> b -> MapSet a b
addToMap' (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
cs) SORT
n PredType
pt }
    in do
      let sig' :: Sign e f
sig' = Sign e f -> Symbol -> Sign e f
forall e f. Sign e f -> Symbol -> Sign e f
addSymbToDeclSymbs Sign e f
sig Symbol
sy
          n :: SORT
n = Symbol -> SORT
symName Symbol
sy
      case Symbol -> SymbType
symbType Symbol
sy of
        SortAsItemType -> Sign e f -> Result (Sign e f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign e f -> Result (Sign e f)) -> Sign e f -> Result (Sign e f)
forall a b. (a -> b) -> a -> b
$ Sign e f -> SORT -> Sign e f
forall f e. Sign f e -> SORT -> Sign f e
addSort' Sign e f
sig' SORT
n
        SubsortAsItemType _ -> Sign e f -> Result (Sign e f)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign e f
sig
        PredAsItemType pt :: PredType
pt -> Sign e f -> Result (Sign e f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign e f -> Result (Sign e f)) -> Sign e f -> Result (Sign e f)
forall a b. (a -> b) -> a -> b
$ Sign e f -> SORT -> PredType -> Sign e f
forall f e. Sign f e -> SORT -> PredType -> Sign f e
addPred' Sign e f
sig' SORT
n PredType
pt
        OpAsItemType ot :: OpType
ot -> Sign e f -> Result (Sign e f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign e f -> Result (Sign e f)) -> Sign e f -> Result (Sign e f)
forall a b. (a -> b) -> a -> b
$ Sign e f -> SORT -> OpType -> Sign e f
forall f e. Sign f e -> SORT -> OpType -> Sign f e
addOp' Sign e f
sig' SORT
n OpType
ot


-- The function below belong in a different file. But I put them here for now.
-- dual of a quantifier

dualQuant :: QUANTIFIER -> QUANTIFIER
dualQuant :: QUANTIFIER -> QUANTIFIER
dualQuant q :: QUANTIFIER
q = case QUANTIFIER
q of
 Universal -> QUANTIFIER
Existential
 Existential -> QUANTIFIER
Universal 
 Unique_existential -> String -> QUANTIFIER
forall a. HasCallStack => String -> a
error "unique existential quantifier has no dual" -- should not get here