{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Adl/Sign.hs
Description :  ADL signature and sentences
Copyright   :  (c) Stef Joosten, Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

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

-}

module Adl.Sign where

import Adl.As
import Adl.Print ()

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import qualified Common.Lib.Rel as Rel

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

type RelMap = Map.Map Id (Set.Set RelType)

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

emptySign :: Sign
emptySign :: Sign
emptySign = Sign :: RelMap -> Rel Concept -> Sign
Sign
  { rels :: RelMap
rels = RelMap
forall k a. Map k a
Map.empty
  , isas :: Rel Concept
isas = Rel Concept
forall a. Rel a
Rel.empty }

closeSign :: Sign -> Sign
closeSign :: Sign -> Sign
closeSign s :: Sign
s = Sign
s { isas :: Rel Concept
isas = Rel Concept -> Rel Concept
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Concept -> Rel Concept) -> Rel Concept -> Rel Concept
forall a b. (a -> b) -> a -> b
$ Sign -> Rel Concept
isas Sign
s }

isSubSignOf :: Sign -> Sign -> Bool
isSubSignOf :: Sign -> Sign -> Bool
isSubSignOf s1 :: Sign
s1 s2 :: Sign
s2 =
  (Set RelType -> Set RelType -> Bool) -> RelMap -> RelMap -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy Set RelType -> Set RelType -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> RelMap
rels Sign
s1) (Sign -> RelMap
rels Sign
s2)
  Bool -> Bool -> Bool
&& Rel Concept -> Rel Concept -> Bool
forall a. Ord a => Rel a -> Rel a -> Bool
Rel.isSubrelOf (Sign -> Rel Concept
isas Sign
s1) (Sign -> Rel Concept
isas Sign
s2)

signUnion :: Sign -> Sign -> Result Sign
signUnion :: Sign -> Sign -> Result Sign
signUnion s1 :: Sign
s1 s2 :: Sign
s2 = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
s1
  { rels :: RelMap
rels = (Set RelType -> Set RelType -> Set RelType)
-> RelMap -> RelMap -> RelMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set RelType -> Set RelType -> Set RelType
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> RelMap
rels Sign
s1) (Sign -> RelMap
rels Sign
s2)
  , isas :: Rel Concept
isas = Rel Concept -> Rel Concept -> Rel Concept
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (Sign -> Rel Concept
isas Sign
s1) (Sign -> Rel Concept
isas Sign
s2) }

data Symbol
  = Con Concept
  | Rel Relation
    deriving (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, 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, 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)
$cRel :: Constr
$cCon :: 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)

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

sym_kind :: Symbol -> SymbolKind
sym_kind :: Symbol -> SymbolKind
sym_kind (Con _) = SymbolKind
ConK
sym_kind (Rel _) = SymbolKind
RelK


instance Pretty SymbolKind where 
 pretty :: SymbolKind -> Doc
pretty ConK = String -> Doc
text "concept"
 pretty RelK = String -> Doc
text "relation" 

instance GetRange Symbol where
  getRange :: Symbol -> Range
getRange s :: Symbol
s = case Symbol
s of
    Rel r :: Relation
r -> Relation -> Range
forall a. GetRange a => a -> Range
getRange Relation
r
    Con c :: Concept
c -> Concept -> Range
forall a. GetRange a => a -> Range
getRange Concept
c
  rangeSpan :: Symbol -> [Pos]
rangeSpan s :: Symbol
s = case Symbol
s of
    Rel r :: Relation
r -> Relation -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Relation
r
    Con c :: Concept
c -> Concept -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Concept
c

instance Pretty Symbol where
  pretty :: Symbol -> Doc
pretty s :: Symbol
s = case Symbol
s of
    Rel r :: Relation
r -> Relation -> Doc
forall a. Pretty a => a -> Doc
pretty Relation
r
    Con c :: Concept
c -> Concept -> Doc
forall a. Pretty a => a -> Doc
pretty Concept
c

conceptToId :: Concept -> Id
conceptToId :: Concept -> Id
conceptToId c :: Concept
c = case Concept
c of
  C t :: Token
t -> Token -> Id
simpleIdToId Token
t
  _ -> String -> Id
stringToId (Concept -> String
forall a. Show a => a -> String
show Concept
c)

symName :: Symbol -> Id
symName :: Symbol -> Id
symName s :: Symbol
s = case Symbol
s of
  Rel r :: Relation
r -> Token -> Id
simpleIdToId (Token -> Id) -> Token -> Id
forall a b. (a -> b) -> a -> b
$ Relation -> Token
decnm Relation
r
  Con c :: Concept
c -> Concept -> Id
conceptToId Concept
c

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

instance GetRange RawSymbol where
  getRange :: RawSymbol -> Range
getRange r :: RawSymbol
r = case RawSymbol
r of
    Symbol s :: Symbol
s -> Symbol -> Range
forall a. GetRange a => a -> Range
getRange Symbol
s
    AnId i :: Id
i -> Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i
  rangeSpan :: RawSymbol -> [Pos]
rangeSpan r :: RawSymbol
r = case RawSymbol
r of
    Symbol s :: Symbol
s -> Symbol -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Symbol
s
    AnId i :: Id
i -> Id -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Id
i

instance Pretty RawSymbol where
  pretty :: RawSymbol -> Doc
pretty r :: RawSymbol
r = case RawSymbol
r of
    Symbol s :: Symbol
s -> Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s
    AnId i :: Id
i -> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i

symMatch :: Symbol -> RawSymbol -> Bool
symMatch :: Symbol -> RawSymbol -> Bool
symMatch s :: Symbol
s r :: RawSymbol
r = case RawSymbol
r of
  Symbol t :: Symbol
t -> Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
t
  AnId i :: Id
i -> Symbol -> Id
symName Symbol
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i

symOf :: Sign -> Set.Set Symbol
symOf :: Sign -> Set Symbol
symOf = [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Symbol] -> Set Symbol)
-> (Sign -> [Set Symbol]) -> Sign -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Id, Set RelType) -> Set Symbol)
-> [(Id, Set RelType)] -> [Set Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, l :: Set RelType
l) ->
          [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList
            ([Symbol] -> Set Symbol)
-> ([RelType] -> [Symbol]) -> [RelType] -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RelType -> [Symbol]) -> [RelType] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
              (\ y :: RelType
y -> let
                   s :: Concept
s = RelType -> Concept
relSrc RelType
y
                   t :: Concept
t = RelType -> Concept
relTrg RelType
y
                   in [Concept -> Symbol
Con Concept
s, Concept -> Symbol
Con Concept
t, Relation -> Symbol
Rel (Relation -> Symbol) -> Relation -> Symbol
forall a b. (a -> b) -> a -> b
$ Token -> RelType -> Relation
Sgn (Id -> Token
idToSimpleId Id
i) RelType
y])
            ([RelType] -> Set Symbol) -> [RelType] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set RelType -> [RelType]
forall a. Set a -> [a]
Set.toList Set RelType
l)
        ([(Id, Set RelType)] -> [Set Symbol])
-> (Sign -> [(Id, Set RelType)]) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelMap -> [(Id, Set RelType)]
forall k a. Map k a -> [(k, a)]
Map.toList (RelMap -> [(Id, Set RelType)])
-> (Sign -> RelMap) -> Sign -> [(Id, Set RelType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> RelMap
rels

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

instance Pretty Sign where
  pretty :: Sign -> Doc
pretty s :: Sign
s =
    [Doc] -> Doc
vcat ((PatElem -> Doc) -> [PatElem] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PatElem -> Doc
forall a. Pretty a => a -> Doc
pretty ([PatElem] -> [Doc]) -> [PatElem] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Id, Set RelType) -> [PatElem])
-> [(Id, Set RelType)] -> [PatElem]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (i :: Id
i, l :: Set RelType
l) ->
               (RelType -> PatElem) -> [RelType] -> [PatElem]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: RelType
t -> [RangedProp] -> Relation -> Bool -> PatElem
Pm [] (Token -> RelType -> Relation
Sgn (Id -> Token
idToSimpleId Id
i) RelType
t) Bool
False)
               ([RelType] -> [PatElem]) -> [RelType] -> [PatElem]
forall a b. (a -> b) -> a -> b
$ Set RelType -> [RelType]
forall a. Set a -> [a]
Set.toList Set RelType
l) ([(Id, Set RelType)] -> [PatElem])
-> [(Id, Set RelType)] -> [PatElem]
forall a b. (a -> b) -> a -> b
$ RelMap -> [(Id, Set RelType)]
forall k a. Map k a -> [(k, a)]
Map.toList (RelMap -> [(Id, Set RelType)]) -> RelMap -> [(Id, Set RelType)]
forall a b. (a -> b) -> a -> b
$ Sign -> RelMap
rels Sign
s)
    Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (((Concept, Concept) -> Doc) -> [(Concept, Concept)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c1 :: Concept
c1, c2 :: Concept
c2) -> PatElem -> Doc
forall a. Pretty a => a -> Doc
pretty (PatElem -> Doc) -> PatElem -> Doc
forall a b. (a -> b) -> a -> b
$ Concept -> Concept -> PatElem
Pg Concept
c1 Concept
c2)
              ([(Concept, Concept)] -> [Doc])
-> (Rel Concept -> [(Concept, Concept)]) -> Rel Concept -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Concept -> [(Concept, Concept)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel Concept -> [(Concept, Concept)])
-> (Rel Concept -> Rel Concept)
-> Rel Concept
-> [(Concept, Concept)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Concept -> Rel Concept
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel Concept -> Rel Concept)
-> (Rel Concept -> Rel Concept) -> Rel Concept -> Rel Concept
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Concept -> Rel Concept
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Concept -> [Doc]) -> Rel Concept -> [Doc]
forall a b. (a -> b) -> a -> b
$ Sign -> Rel Concept
isas Sign
s)

data Sen
  = DeclProp Relation RangedProp
  | Assertion (Maybe RuleKind) Rule
    deriving (Sen -> Sen -> Bool
(Sen -> Sen -> Bool) -> (Sen -> Sen -> Bool) -> Eq Sen
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sen -> Sen -> Bool
$c/= :: Sen -> Sen -> Bool
== :: Sen -> Sen -> Bool
$c== :: Sen -> Sen -> Bool
Eq, Eq Sen
Eq Sen =>
(Sen -> Sen -> Ordering)
-> (Sen -> Sen -> Bool)
-> (Sen -> Sen -> Bool)
-> (Sen -> Sen -> Bool)
-> (Sen -> Sen -> Bool)
-> (Sen -> Sen -> Sen)
-> (Sen -> Sen -> Sen)
-> Ord Sen
Sen -> Sen -> Bool
Sen -> Sen -> Ordering
Sen -> Sen -> Sen
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 :: Sen -> Sen -> Sen
$cmin :: Sen -> Sen -> Sen
max :: Sen -> Sen -> Sen
$cmax :: Sen -> Sen -> Sen
>= :: Sen -> Sen -> Bool
$c>= :: Sen -> Sen -> Bool
> :: Sen -> Sen -> Bool
$c> :: Sen -> Sen -> Bool
<= :: Sen -> Sen -> Bool
$c<= :: Sen -> Sen -> Bool
< :: Sen -> Sen -> Bool
$c< :: Sen -> Sen -> Bool
compare :: Sen -> Sen -> Ordering
$ccompare :: Sen -> Sen -> Ordering
$cp1Ord :: Eq Sen
Ord, Int -> Sen -> ShowS
[Sen] -> ShowS
Sen -> String
(Int -> Sen -> ShowS)
-> (Sen -> String) -> ([Sen] -> ShowS) -> Show Sen
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sen] -> ShowS
$cshowList :: [Sen] -> ShowS
show :: Sen -> String
$cshow :: Sen -> String
showsPrec :: Int -> Sen -> ShowS
$cshowsPrec :: Int -> Sen -> ShowS
Show, Typeable, Typeable Sen
Constr
DataType
Typeable Sen =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sen -> c Sen)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sen)
-> (Sen -> Constr)
-> (Sen -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sen))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sen))
-> ((forall b. Data b => b -> b) -> Sen -> Sen)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sen -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sen -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sen -> m Sen)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sen -> m Sen)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sen -> m Sen)
-> Data Sen
Sen -> Constr
Sen -> DataType
(forall b. Data b => b -> b) -> Sen -> Sen
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sen -> c Sen
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sen
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) -> Sen -> u
forall u. (forall d. Data d => d -> u) -> Sen -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sen -> m Sen
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sen -> m Sen
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sen
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sen -> c Sen
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sen)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sen)
$cAssertion :: Constr
$cDeclProp :: Constr
$tSen :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sen -> m Sen
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sen -> m Sen
gmapMp :: (forall d. Data d => d -> m d) -> Sen -> m Sen
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sen -> m Sen
gmapM :: (forall d. Data d => d -> m d) -> Sen -> m Sen
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sen -> m Sen
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sen -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sen -> u
gmapQ :: (forall d. Data d => d -> u) -> Sen -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sen -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r
gmapT :: (forall b. Data b => b -> b) -> Sen -> Sen
$cgmapT :: (forall b. Data b => b -> b) -> Sen -> Sen
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sen)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sen)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sen)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sen)
dataTypeOf :: Sen -> DataType
$cdataTypeOf :: Sen -> DataType
toConstr :: Sen -> Constr
$ctoConstr :: Sen -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sen
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sen
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sen -> c Sen
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sen -> c Sen
$cp1Data :: Typeable Sen
Data)

instance GetRange Sen where
  getRange :: Sen -> Range
getRange s :: Sen
s = case Sen
s of
    DeclProp _ p :: RangedProp
p -> RangedProp -> Range
forall a. GetRange a => a -> Range
getRange RangedProp
p
    Assertion _ r :: Rule
r -> Rule -> Range
forall a. GetRange a => a -> Range
getRange Rule
r
  rangeSpan :: Sen -> [Pos]
rangeSpan s :: Sen
s = case Sen
s of
    DeclProp r :: Relation
r p :: RangedProp
p -> [[Pos]] -> [Pos]
joinRanges [Relation -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Relation
r, RangedProp -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RangedProp
p]
    Assertion _ r :: Rule
r -> Rule -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Rule
r

instance Pretty Sen where
  pretty :: Sen -> Doc
pretty s :: Sen
s = case Sen
s of
    DeclProp r :: Relation
r p :: RangedProp
p -> PatElem -> Doc
forall a. Pretty a => a -> Doc
pretty (PatElem -> Doc) -> PatElem -> Doc
forall a b. (a -> b) -> a -> b
$ [RangedProp] -> Relation -> Bool -> PatElem
Pm [RangedProp
p] Relation
r Bool
False
    Assertion _ r :: Rule
r -> PatElem -> Doc
forall a. Pretty a => a -> Doc
pretty (PatElem -> Doc) -> PatElem -> Doc
forall a b. (a -> b) -> a -> b
$ RuleHeader -> Rule -> PatElem
Pr RuleHeader
Always Rule
r

printNSen :: Named Sen -> Doc
printNSen :: Named Sen -> Doc
printNSen ns :: Named Sen
ns = let
   s :: Sen
s = Named Sen -> Sen
forall s a. SenAttr s a -> s
sentence Named Sen
ns
   n :: String
n = Named Sen -> String
forall s a. SenAttr s a -> a
senAttr Named Sen
ns
   d :: Doc
d = Sen -> Doc
forall a. Pretty a => a -> Doc
pretty Sen
s
   in case Sen
s of
   Assertion (Just k :: RuleKind
k) r :: Rule
r ->
     PatElem -> Doc
forall a. Pretty a => a -> Doc
pretty (PatElem -> Doc) -> PatElem -> Doc
forall a b. (a -> b) -> a -> b
$ RuleHeader -> Rule -> PatElem
Pr (RuleKind -> Token -> RuleHeader
RuleHeader RuleKind
k (Token -> RuleHeader) -> Token -> RuleHeader
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
n) Rule
r
   _ -> Doc
d Doc -> Doc -> Doc
<+> String -> Doc
text ("-- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n)