{-# LANGUAGE DeriveDataTypeable #-}
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)
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)
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
| OpAsItemType OpType
| 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 () ()
data Sign f e = Sign
{ Sign f e -> Rel SORT
sortRel :: Rel.Rel SORT
, Sign f e -> Maybe (Rel SORT)
revSortRel :: Maybe (Rel.Rel SORT)
, Sign f e -> Set SORT
emptySortSet :: Set.Set SORT
, Sign f e -> OpMap
opMap :: OpMap
, Sign f e -> OpMap
assocOps :: OpMap
, Sign f e -> PredMap
predMap :: PredMap
, Sign f e -> Map SIMPLE_ID SORT
varMap :: Map.Map SIMPLE_ID SORT
, Sign f e -> [Named (FORMULA f)]
sentences :: [Named (FORMULA f)]
, Sign f e -> Set Symbol
declaredSymbols :: Set.Set Symbol
, Sign f e -> [Diagnosis]
envDiags :: [Diagnosis]
, Sign f e -> AnnoMap
annoMap :: AnnoMap
, Sign f e -> GlobalAnnos
globAnnos :: GlobalAnnos
, 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
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
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 }
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)
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
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
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 }
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)
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)
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)
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 ""
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
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
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"