{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Fpl/Sign.hs
Description :  signatures for FPL
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

signature extension for FPL to keep track of constructors
-}

module Fpl.Sign where

import Fpl.As

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Keywords
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.ToDoc

import Data.Data
import Data.List
import Data.Ord

boolSort :: Id
boolSort :: Id
boolSort = String -> Id
stringToId "Bool"

trueC :: Id
trueC :: Id
trueC = String -> Id
stringToId String
trueS

falseC :: Id
falseC :: Id
falseC = String -> Id
stringToId String
falseS

boolType :: OpType
boolType :: OpType
boolType = Id -> OpType
sortToOpType Id
boolSort

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

instance Pretty SignExt where
  pretty :: SignExt -> Doc
pretty es :: SignExt
es = let nr :: Range
nr = Range
nullRange in case
         ((Id, OpType) -> (Id, OpType) -> Bool)
-> [(Id, OpType)] -> [[(Id, OpType)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (_, c1 :: OpType
c1) (_, c2 :: OpType
c2) -> OpType -> Id
opRes OpType
c1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== OpType -> Id
opRes OpType
c2)
         ([(Id, OpType)] -> [[(Id, OpType)]])
-> [(Id, OpType)] -> [[(Id, OpType)]]
forall a b. (a -> b) -> a -> b
$ ((Id, OpType) -> (Id, OpType) -> Ordering)
-> [(Id, OpType)] -> [(Id, OpType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Id, OpType) -> Id) -> (Id, OpType) -> (Id, OpType) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (OpType -> Id
opRes (OpType -> Id) -> ((Id, OpType) -> OpType) -> (Id, OpType) -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, OpType) -> OpType
forall a b. (a, b) -> b
snd))
         ([(Id, OpType)] -> [(Id, OpType)])
-> [(Id, OpType)] -> [(Id, OpType)]
forall a b. (a -> b) -> a -> b
$ OpMap -> [(Id, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (OpMap -> [(Id, OpType)]) -> OpMap -> [(Id, OpType)]
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr SignExt
es of
     [] -> Doc
empty
     l :: [[(Id, OpType)]]
l -> String -> Doc
topSigKey (String
sortS String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[(Id, OpType)]] -> String
forall a. [a] -> String
appendS [[(Id, OpType)]]
l) Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepBySemis
       (([(Id, OpType)] -> Doc) -> [[(Id, OpType)]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ g :: [(Id, OpType)]
g -> DATATYPE_DECL -> Doc
printDD
             (Id -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl (OpType -> Id
opRes (OpType -> Id) -> OpType -> Id
forall a b. (a -> b) -> a -> b
$ (Id, OpType) -> OpType
forall a b. (a, b) -> b
snd ((Id, OpType) -> OpType) -> (Id, OpType) -> OpType
forall a b. (a -> b) -> a -> b
$ [(Id, OpType)] -> (Id, OpType)
forall a. [a] -> a
head [(Id, OpType)]
g)
              (((Id, OpType) -> Annoted ALTERNATIVE)
-> [(Id, OpType)] -> [Annoted ALTERNATIVE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, t :: OpType
t) -> ALTERNATIVE -> Annoted ALTERNATIVE
forall a. a -> Annoted a
emptyAnno (ALTERNATIVE -> Annoted ALTERNATIVE)
-> ALTERNATIVE -> Annoted ALTERNATIVE
forall a b. (a -> b) -> a -> b
$
                    OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Total Id
i ((Id -> COMPONENTS) -> [Id] -> [COMPONENTS]
forall a b. (a -> b) -> [a] -> [b]
map Id -> COMPONENTS
Sort ([Id] -> [COMPONENTS]) -> [Id] -> [COMPONENTS]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
t) Range
nr)
               [(Id, OpType)]
g) Range
nr)) [[(Id, OpType)]]
l)

emptyFplSign :: SignExt
emptyFplSign :: SignExt
emptyFplSign = OpMap -> SignExt
SignExt OpMap
forall a b. MapSet a b
MapSet.empty

diffFplSign :: SignExt -> SignExt -> SignExt
diffFplSign :: SignExt -> SignExt -> SignExt
diffFplSign a :: SignExt
a b :: SignExt
b = SignExt
a
  { constr :: OpMap
constr = SignExt -> OpMap
constr SignExt
a OpMap -> OpMap -> OpMap
`diffOpMapSet` SignExt -> OpMap
constr SignExt
b }

addFplSign :: SignExt -> SignExt -> SignExt
addFplSign :: SignExt -> SignExt -> SignExt
addFplSign a :: SignExt
a b :: SignExt
b = SignExt
a
  { constr :: OpMap
constr = OpMap -> OpMap -> OpMap
addOpMapSet (SignExt -> OpMap
constr SignExt
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr SignExt
b }

interFplSign :: SignExt -> SignExt -> SignExt
interFplSign :: SignExt -> SignExt -> SignExt
interFplSign a :: SignExt
a b :: SignExt
b = SignExt
a
  { constr :: OpMap
constr = OpMap -> OpMap -> OpMap
interOpMapSet (SignExt -> OpMap
constr SignExt
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr SignExt
b }

isSubFplSign :: SignExt -> SignExt -> Bool
isSubFplSign :: SignExt -> SignExt -> Bool
isSubFplSign s1 :: SignExt
s1 s2 :: SignExt
s2 = OpMap -> OpMap -> Bool
isSubOpMap (SignExt -> OpMap
constr SignExt
s1) (SignExt -> OpMap
constr SignExt
s2)

type FplSign = Sign TermExt SignExt

addBools :: OpMap -> OpMap
addBools :: OpMap -> OpMap
addBools = Id -> OpType -> OpMap -> OpMap
addOpTo Id
falseC OpType
boolType (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> OpType -> OpMap -> OpMap
addOpTo Id
trueC OpType
boolType

addConsts :: SignExt -> SignExt
addConsts :: SignExt -> SignExt
addConsts s :: SignExt
s = SignExt
s { constr :: OpMap
constr = OpMap -> OpMap
addBools (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr SignExt
s }

addBuiltins :: FplSign -> FplSign
addBuiltins :: FplSign -> FplSign
addBuiltins s :: FplSign
s = FplSign
s { sortRel :: Rel Id
sortRel = Id -> Rel Id -> Rel Id
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey Id
boolSort (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ FplSign -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel FplSign
s
                  , opMap :: OpMap
opMap = OpMap -> OpMap
addBools (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ FplSign -> OpMap
forall f e. Sign f e -> OpMap
opMap FplSign
s
                  , extendedInfo :: SignExt
extendedInfo = SignExt -> SignExt
addConsts (SignExt -> SignExt) -> SignExt -> SignExt
forall a b. (a -> b) -> a -> b
$ FplSign -> SignExt
forall f e. Sign f e -> e
extendedInfo FplSign
s }

delBuiltins :: FplSign -> FplSign
delBuiltins :: FplSign -> FplSign
delBuiltins s :: FplSign
s = (SignExt -> SignExt -> SignExt) -> FplSign -> FplSign -> FplSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig SignExt -> SignExt -> SignExt
diffFplSign FplSign
s (FplSign -> FplSign) -> FplSign -> FplSign
forall a b. (a -> b) -> a -> b
$ FplSign -> FplSign
addBuiltins (FplSign -> FplSign) -> FplSign -> FplSign
forall a b. (a -> b) -> a -> b
$ SignExt -> FplSign
forall e f. e -> Sign f e
emptySign SignExt
emptyFplSign