{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./VSE/As.hs
Description :  abstract syntax of VSE programs and dynamic logic
Copyright   :  (c) C. Maeder, DFKI 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

CASL extention to VSE programs and dynamic logic
as described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
Bruno Langenstein's API description
-}

module VSE.As where

import Data.Char
import Data.Data
import qualified Data.Map as Map
import Control.Monad (foldM)

import Common.AS_Annotation
import Common.Id
import Common.Doc
import Common.DocUtils
import Common.Result
import Common.LibName
import Common.Utils (number)

import CASL.AS_Basic_CASL
import CASL.ToDoc

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

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

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

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

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

instance GetRange Procdecls where
  getRange :: Procdecls -> Range
getRange (Procdecls _ r :: Range
r) = Range
r

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

-- | attach a nullRange
mkRanged :: a -> Ranged a
mkRanged :: a -> Ranged a
mkRanged a :: a
a = a -> Range -> Ranged a
forall a. a -> Range -> Ranged a
Ranged a
a Range
nullRange

-- | programs with ranges
type Program = Ranged PlainProgram

-- | programs based on restricted terms and formulas
data PlainProgram =
    Abort
  | Skip
  | Assign VAR (TERM ())
  | Call (FORMULA ()) -- ^ a procedure call as predication
  | Return (TERM ())
  | Block [VAR_DECL] Program
  | Seq Program Program
  | If (FORMULA ()) Program Program
  | While (FORMULA ()) Program
    deriving (Int -> PlainProgram -> ShowS
[PlainProgram] -> ShowS
PlainProgram -> String
(Int -> PlainProgram -> ShowS)
-> (PlainProgram -> String)
-> ([PlainProgram] -> ShowS)
-> Show PlainProgram
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PlainProgram] -> ShowS
$cshowList :: [PlainProgram] -> ShowS
show :: PlainProgram -> String
$cshow :: PlainProgram -> String
showsPrec :: Int -> PlainProgram -> ShowS
$cshowsPrec :: Int -> PlainProgram -> ShowS
Show, PlainProgram -> PlainProgram -> Bool
(PlainProgram -> PlainProgram -> Bool)
-> (PlainProgram -> PlainProgram -> Bool) -> Eq PlainProgram
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PlainProgram -> PlainProgram -> Bool
$c/= :: PlainProgram -> PlainProgram -> Bool
== :: PlainProgram -> PlainProgram -> Bool
$c== :: PlainProgram -> PlainProgram -> Bool
Eq, Eq PlainProgram
Eq PlainProgram =>
(PlainProgram -> PlainProgram -> Ordering)
-> (PlainProgram -> PlainProgram -> Bool)
-> (PlainProgram -> PlainProgram -> Bool)
-> (PlainProgram -> PlainProgram -> Bool)
-> (PlainProgram -> PlainProgram -> Bool)
-> (PlainProgram -> PlainProgram -> PlainProgram)
-> (PlainProgram -> PlainProgram -> PlainProgram)
-> Ord PlainProgram
PlainProgram -> PlainProgram -> Bool
PlainProgram -> PlainProgram -> Ordering
PlainProgram -> PlainProgram -> PlainProgram
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 :: PlainProgram -> PlainProgram -> PlainProgram
$cmin :: PlainProgram -> PlainProgram -> PlainProgram
max :: PlainProgram -> PlainProgram -> PlainProgram
$cmax :: PlainProgram -> PlainProgram -> PlainProgram
>= :: PlainProgram -> PlainProgram -> Bool
$c>= :: PlainProgram -> PlainProgram -> Bool
> :: PlainProgram -> PlainProgram -> Bool
$c> :: PlainProgram -> PlainProgram -> Bool
<= :: PlainProgram -> PlainProgram -> Bool
$c<= :: PlainProgram -> PlainProgram -> Bool
< :: PlainProgram -> PlainProgram -> Bool
$c< :: PlainProgram -> PlainProgram -> Bool
compare :: PlainProgram -> PlainProgram -> Ordering
$ccompare :: PlainProgram -> PlainProgram -> Ordering
$cp1Ord :: Eq PlainProgram
Ord, Typeable, Typeable PlainProgram
Constr
DataType
Typeable PlainProgram =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PlainProgram -> c PlainProgram)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PlainProgram)
-> (PlainProgram -> Constr)
-> (PlainProgram -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PlainProgram))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PlainProgram))
-> ((forall b. Data b => b -> b) -> PlainProgram -> PlainProgram)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r)
-> (forall u. (forall d. Data d => d -> u) -> PlainProgram -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PlainProgram -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram)
-> Data PlainProgram
PlainProgram -> Constr
PlainProgram -> DataType
(forall b. Data b => b -> b) -> PlainProgram -> PlainProgram
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlainProgram -> c PlainProgram
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PlainProgram
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) -> PlainProgram -> u
forall u. (forall d. Data d => d -> u) -> PlainProgram -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PlainProgram
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlainProgram -> c PlainProgram
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PlainProgram)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PlainProgram)
$cWhile :: Constr
$cIf :: Constr
$cSeq :: Constr
$cBlock :: Constr
$cReturn :: Constr
$cCall :: Constr
$cAssign :: Constr
$cSkip :: Constr
$cAbort :: Constr
$tPlainProgram :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
gmapMp :: (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
gmapM :: (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
gmapQi :: Int -> (forall d. Data d => d -> u) -> PlainProgram -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PlainProgram -> u
gmapQ :: (forall d. Data d => d -> u) -> PlainProgram -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PlainProgram -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlainProgram -> r
gmapT :: (forall b. Data b => b -> b) -> PlainProgram -> PlainProgram
$cgmapT :: (forall b. Data b => b -> b) -> PlainProgram -> PlainProgram
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PlainProgram)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PlainProgram)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PlainProgram)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PlainProgram)
dataTypeOf :: PlainProgram -> DataType
$cdataTypeOf :: PlainProgram -> DataType
toConstr :: PlainProgram -> Constr
$ctoConstr :: PlainProgram -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PlainProgram
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PlainProgram
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlainProgram -> c PlainProgram
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlainProgram -> c PlainProgram
$cp1Data :: Typeable PlainProgram
Data)

-- | alternative variable declaration
data VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range
  deriving (Int -> VarDecl -> ShowS
[VarDecl] -> ShowS
VarDecl -> String
(Int -> VarDecl -> ShowS)
-> (VarDecl -> String) -> ([VarDecl] -> ShowS) -> Show VarDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarDecl] -> ShowS
$cshowList :: [VarDecl] -> ShowS
show :: VarDecl -> String
$cshow :: VarDecl -> String
showsPrec :: Int -> VarDecl -> ShowS
$cshowsPrec :: Int -> VarDecl -> ShowS
Show, Typeable, Typeable VarDecl
Constr
DataType
Typeable VarDecl =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> VarDecl -> c VarDecl)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c VarDecl)
-> (VarDecl -> Constr)
-> (VarDecl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c VarDecl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl))
-> ((forall b. Data b => b -> b) -> VarDecl -> VarDecl)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> VarDecl -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> VarDecl -> r)
-> (forall u. (forall d. Data d => d -> u) -> VarDecl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> VarDecl -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl)
-> Data VarDecl
VarDecl -> Constr
VarDecl -> DataType
(forall b. Data b => b -> b) -> VarDecl -> VarDecl
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDecl -> c VarDecl
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDecl
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) -> VarDecl -> u
forall u. (forall d. Data d => d -> u) -> VarDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDecl -> c VarDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VarDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl)
$cVarDecl :: Constr
$tVarDecl :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
gmapMp :: (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
gmapM :: (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDecl -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> VarDecl -> u
gmapQ :: (forall d. Data d => d -> u) -> VarDecl -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> VarDecl -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VarDecl -> r
gmapT :: (forall b. Data b => b -> b) -> VarDecl -> VarDecl
$cgmapT :: (forall b. Data b => b -> b) -> VarDecl -> VarDecl
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c VarDecl)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VarDecl)
dataTypeOf :: VarDecl -> DataType
$cdataTypeOf :: VarDecl -> DataType
toConstr :: VarDecl -> Constr
$ctoConstr :: VarDecl -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VarDecl
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDecl -> c VarDecl
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VarDecl -> c VarDecl
$cp1Data :: Typeable VarDecl
Data)

toVarDecl :: [VAR_DECL] -> [VarDecl]
toVarDecl :: [VAR_DECL] -> [VarDecl]
toVarDecl = (VAR_DECL -> [VarDecl]) -> [VAR_DECL] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  (\ (Var_decl vs :: [VAR]
vs s :: SORT
s r :: Range
r) -> (VAR -> VarDecl) -> [VAR] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> VAR -> SORT -> Maybe (TERM ()) -> Range -> VarDecl
VarDecl VAR
v SORT
s Maybe (TERM ())
forall a. Maybe a
Nothing Range
r) [VAR]
vs)

addInits :: [VarDecl] -> Program -> ([VarDecl], Program)
addInits :: [VarDecl] -> Program -> ([VarDecl], Program)
addInits vs :: [VarDecl]
vs p :: Program
p = case [VarDecl]
vs of
  vd :: VarDecl
vd@(VarDecl v :: VAR
v s :: SORT
s Nothing z :: Range
z) : r :: [VarDecl]
r -> case Program -> PlainProgram
forall a. Ranged a -> a
unRanged Program
p of
      Seq (Ranged (Assign av :: VAR
av t :: TERM ()
t) _) p2 :: Program
p2 | VAR
v VAR -> VAR -> Bool
forall a. Eq a => a -> a -> Bool
== VAR
av
          -> let (rs :: [VarDecl]
rs, q :: Program
q) = [VarDecl] -> Program -> ([VarDecl], Program)
addInits [VarDecl]
r Program
p2
             in (VAR -> SORT -> Maybe (TERM ()) -> Range -> VarDecl
VarDecl VAR
v SORT
s (TERM () -> Maybe (TERM ())
forall a. a -> Maybe a
Just TERM ()
t) Range
z VarDecl -> [VarDecl] -> [VarDecl]
forall a. a -> [a] -> [a]
: [VarDecl]
rs, Program
q)
      _ -> let (rs :: [VarDecl]
rs, q :: Program
q) = [VarDecl] -> Program -> ([VarDecl], Program)
addInits [VarDecl]
r Program
p
           in (VarDecl
vd VarDecl -> [VarDecl] -> [VarDecl]
forall a. a -> [a] -> [a]
: [VarDecl]
rs, Program
q)
  _ -> ([VarDecl]
vs, Program
p)

-- | extend CASL formulas by box or diamond formulas and defprocs
data VSEforms =
    Dlformula BoxOrDiamond Program Sentence
  | Defprocs [Defproc]
  | RestrictedConstraint [Constraint] (Map.Map SORT Id) Bool
    deriving (Int -> VSEforms -> ShowS
[VSEforms] -> ShowS
VSEforms -> String
(Int -> VSEforms -> ShowS)
-> (VSEforms -> String) -> ([VSEforms] -> ShowS) -> Show VSEforms
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VSEforms] -> ShowS
$cshowList :: [VSEforms] -> ShowS
show :: VSEforms -> String
$cshow :: VSEforms -> String
showsPrec :: Int -> VSEforms -> ShowS
$cshowsPrec :: Int -> VSEforms -> ShowS
Show, VSEforms -> VSEforms -> Bool
(VSEforms -> VSEforms -> Bool)
-> (VSEforms -> VSEforms -> Bool) -> Eq VSEforms
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VSEforms -> VSEforms -> Bool
$c/= :: VSEforms -> VSEforms -> Bool
== :: VSEforms -> VSEforms -> Bool
$c== :: VSEforms -> VSEforms -> Bool
Eq, Eq VSEforms
Eq VSEforms =>
(VSEforms -> VSEforms -> Ordering)
-> (VSEforms -> VSEforms -> Bool)
-> (VSEforms -> VSEforms -> Bool)
-> (VSEforms -> VSEforms -> Bool)
-> (VSEforms -> VSEforms -> Bool)
-> (VSEforms -> VSEforms -> VSEforms)
-> (VSEforms -> VSEforms -> VSEforms)
-> Ord VSEforms
VSEforms -> VSEforms -> Bool
VSEforms -> VSEforms -> Ordering
VSEforms -> VSEforms -> VSEforms
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 :: VSEforms -> VSEforms -> VSEforms
$cmin :: VSEforms -> VSEforms -> VSEforms
max :: VSEforms -> VSEforms -> VSEforms
$cmax :: VSEforms -> VSEforms -> VSEforms
>= :: VSEforms -> VSEforms -> Bool
$c>= :: VSEforms -> VSEforms -> Bool
> :: VSEforms -> VSEforms -> Bool
$c> :: VSEforms -> VSEforms -> Bool
<= :: VSEforms -> VSEforms -> Bool
$c<= :: VSEforms -> VSEforms -> Bool
< :: VSEforms -> VSEforms -> Bool
$c< :: VSEforms -> VSEforms -> Bool
compare :: VSEforms -> VSEforms -> Ordering
$ccompare :: VSEforms -> VSEforms -> Ordering
$cp1Ord :: Eq VSEforms
Ord, Typeable, Typeable VSEforms
Constr
DataType
Typeable VSEforms =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> VSEforms -> c VSEforms)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c VSEforms)
-> (VSEforms -> Constr)
-> (VSEforms -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c VSEforms))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms))
-> ((forall b. Data b => b -> b) -> VSEforms -> VSEforms)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> VSEforms -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> VSEforms -> r)
-> (forall u. (forall d. Data d => d -> u) -> VSEforms -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> VSEforms -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms)
-> Data VSEforms
VSEforms -> Constr
VSEforms -> DataType
(forall b. Data b => b -> b) -> VSEforms -> VSEforms
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VSEforms -> c VSEforms
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VSEforms
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) -> VSEforms -> u
forall u. (forall d. Data d => d -> u) -> VSEforms -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VSEforms
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VSEforms -> c VSEforms
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VSEforms)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms)
$cRestrictedConstraint :: Constr
$cDefprocs :: Constr
$cDlformula :: Constr
$tVSEforms :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
gmapMp :: (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
gmapM :: (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
gmapQi :: Int -> (forall d. Data d => d -> u) -> VSEforms -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> VSEforms -> u
gmapQ :: (forall d. Data d => d -> u) -> VSEforms -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> VSEforms -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VSEforms -> r
gmapT :: (forall b. Data b => b -> b) -> VSEforms -> VSEforms
$cgmapT :: (forall b. Data b => b -> b) -> VSEforms -> VSEforms
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c VSEforms)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c VSEforms)
dataTypeOf :: VSEforms -> DataType
$cdataTypeOf :: VSEforms -> DataType
toConstr :: VSEforms -> Constr
$ctoConstr :: VSEforms -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VSEforms
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c VSEforms
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VSEforms -> c VSEforms
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VSEforms -> c VSEforms
$cp1Data :: Typeable VSEforms
Data)

type Dlformula = Ranged VSEforms
type Sentence = FORMULA Dlformula

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

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

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

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

emptyProcs :: Procs
emptyProcs :: Procs
emptyProcs = Map SORT Profile -> Procs
Procs Map SORT Profile
forall k a. Map k a
Map.empty

unionProcs :: Procs -> Procs -> Result Procs
unionProcs :: Procs -> Procs -> Result Procs
unionProcs (Procs m1 :: Map SORT Profile
m1) (Procs m2 :: Map SORT Profile
m2) = (Map SORT Profile -> Procs)
-> Result (Map SORT Profile) -> Result Procs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Map SORT Profile -> Procs
Procs (Result (Map SORT Profile) -> Result Procs)
-> Result (Map SORT Profile) -> Result Procs
forall a b. (a -> b) -> a -> b
$
  (Map SORT Profile -> (SORT, Profile) -> Result (Map SORT Profile))
-> Map SORT Profile
-> [(SORT, Profile)]
-> Result (Map SORT Profile)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: Map SORT Profile
m (k :: SORT
k, v :: Profile
v) -> case SORT -> Map SORT Profile -> Maybe Profile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
k Map SORT Profile
m1 of
    Nothing -> Map SORT Profile -> Result (Map SORT Profile)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map SORT Profile -> Result (Map SORT Profile))
-> Map SORT Profile -> Result (Map SORT Profile)
forall a b. (a -> b) -> a -> b
$ SORT -> Profile -> Map SORT Profile -> Map SORT Profile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
k Profile
v Map SORT Profile
m
    Just w :: Profile
w -> if Profile
w Profile -> Profile -> Bool
forall a. Eq a => a -> a -> Bool
== Profile
v then Map SORT Profile -> Result (Map SORT Profile)
forall (m :: * -> *) a. Monad m => a -> m a
return Map SORT Profile
m else
      String -> SORT -> Result (Map SORT Profile)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "different union profiles for" SORT
k)
  Map SORT Profile
m1 ([(SORT, Profile)] -> Result (Map SORT Profile))
-> [(SORT, Profile)] -> Result (Map SORT Profile)
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
m2

interProcs :: Procs -> Procs -> Result Procs
interProcs :: Procs -> Procs -> Result Procs
interProcs (Procs m1 :: Map SORT Profile
m1) (Procs m2 :: Map SORT Profile
m2) = (Map SORT Profile -> Procs)
-> Result (Map SORT Profile) -> Result Procs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Map SORT Profile -> Procs
Procs (Result (Map SORT Profile) -> Result Procs)
-> Result (Map SORT Profile) -> Result Procs
forall a b. (a -> b) -> a -> b
$
  (Map SORT Profile -> (SORT, Profile) -> Result (Map SORT Profile))
-> Map SORT Profile
-> [(SORT, Profile)]
-> Result (Map SORT Profile)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: Map SORT Profile
m (k :: SORT
k, v :: Profile
v) -> case SORT -> Map SORT Profile -> Maybe Profile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
k Map SORT Profile
m1 of
    Nothing -> Map SORT Profile -> Result (Map SORT Profile)
forall (m :: * -> *) a. Monad m => a -> m a
return Map SORT Profile
m
    Just w :: Profile
w -> if Profile
w Profile -> Profile -> Bool
forall a. Eq a => a -> a -> Bool
== Profile
v then Map SORT Profile -> Result (Map SORT Profile)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map SORT Profile -> Result (Map SORT Profile))
-> Map SORT Profile -> Result (Map SORT Profile)
forall a b. (a -> b) -> a -> b
$ SORT -> Profile -> Map SORT Profile -> Map SORT Profile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
k Profile
v Map SORT Profile
m else
      String -> SORT -> Result (Map SORT Profile)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "different intersection profiles for" SORT
k)
    Map SORT Profile
forall k a. Map k a
Map.empty ([(SORT, Profile)] -> Result (Map SORT Profile))
-> [(SORT, Profile)] -> Result (Map SORT Profile)
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
m2

diffProcs :: Procs -> Procs -> Procs
diffProcs :: Procs -> Procs -> Procs
diffProcs (Procs m1 :: Map SORT Profile
m1) (Procs m2 :: Map SORT Profile
m2) = Map SORT Profile -> Procs
Procs (Map SORT Profile -> Procs) -> Map SORT Profile -> Procs
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> Map SORT Profile -> Map SORT Profile
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map SORT Profile
m1 Map SORT Profile
m2

isSubProcsMap :: Procs -> Procs -> Bool
isSubProcsMap :: Procs -> Procs -> Bool
isSubProcsMap (Procs m1 :: Map SORT Profile
m1) (Procs m2 :: Map SORT Profile
m2) = (Profile -> Profile -> Bool)
-> Map SORT Profile -> Map SORT Profile -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy Profile -> Profile -> Bool
forall a. Eq a => a -> a -> Bool
(==) Map SORT Profile
m1 Map SORT Profile
m2

-- * Pretty instances

instance Pretty Profile where
  pretty :: Profile -> Doc
pretty (Profile ps :: [Procparam]
ps ores :: Maybe SORT
ores) = [Doc] -> Doc
fsep
    [ [Procparam] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [Procparam]
ps
    , case Maybe SORT
ores of
        Nothing -> Doc
empty
        Just s :: SORT
s -> Doc
funArrow Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s]

instance Pretty Sigentry where
  pretty :: Sigentry -> Doc
pretty (Procedure i :: SORT
i p :: Profile
p _) = [Doc] -> Doc
fsep [SORT -> Doc
idDoc SORT
i, Doc
colon Doc -> Doc -> Doc
<+> Profile -> Doc
forall a. Pretty a => a -> Doc
pretty Profile
p]

instance Pretty Procdecls where
  pretty :: Procdecls -> Doc
pretty (Procdecls l :: [Annoted Sigentry]
l _) = if [Annoted Sigentry] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted Sigentry]
l then Doc
empty else [Doc] -> Doc
fsep
   [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "PROCEDURE" String -> ShowS
forall a. [a] -> [a] -> [a]
++ case [Annoted Sigentry]
l of
        [_] -> ""
        _ -> "S"
   , (Sigentry -> Doc) -> [Annoted Sigentry] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos Sigentry -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted Sigentry]
l ]

instance Pretty Procparam where
  pretty :: Procparam -> Doc
pretty (Procparam m :: Paramkind
m s :: SORT
s) = String -> Doc
text ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Paramkind -> String
forall a. Show a => a -> String
show Paramkind
m) Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s

block :: Doc -> Doc
block :: Doc -> Doc
block d :: Doc
d = [Doc] -> Doc
sep [String -> Doc
text "BEGIN", Doc
d, String -> Doc
text "END"]

prettyProcKind :: ProcKind -> Doc
prettyProcKind :: ProcKind -> Doc
prettyProcKind k :: ProcKind
k = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case ProcKind
k of
  Proc -> "PROCEDURE"
  Func -> "FUNCTION"

assign :: Doc
assign :: Doc
assign = String -> Doc
text ":="

instance Pretty Defproc where
  pretty :: Defproc -> Doc
pretty (Defproc pk :: ProcKind
pk p :: SORT
p ps :: [VAR]
ps pr :: Program
pr _) = [Doc] -> Doc
vcat
    [ ProcKind -> Doc
prettyProcKind ProcKind
pk Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([VAR] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [VAR]
ps)
    , Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
pr ]

instance Pretty a => Pretty (Ranged a) where
  pretty :: Ranged a -> Doc
pretty (Ranged a :: a
a _) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a

instance GetRange (Ranged a) where
  getRange :: Ranged a -> Range
getRange (Ranged _ r :: Range
r) = Range
r

instance FormExtension a => FormExtension (Ranged a) where
  isQuantifierLike :: Ranged a -> Bool
isQuantifierLike (Ranged a :: a
a _) = a -> Bool
forall f. FormExtension f => f -> Bool
isQuantifierLike a
a

instance Pretty VarDecl where
  pretty :: VarDecl -> Doc
pretty (VarDecl v :: VAR
v s :: SORT
s mt :: Maybe (TERM ())
mt _) =
      VAR -> Doc
sidDoc VAR
v Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s Doc -> Doc -> Doc
<+> case Maybe (TERM ())
mt of
      Nothing -> Doc
empty
      Just t :: TERM ()
t -> Doc
assign Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t

instance Pretty PlainProgram where
  pretty :: PlainProgram -> Doc
pretty prg :: PlainProgram
prg = case PlainProgram
prg of
    Abort -> String -> Doc
text "ABORT"
    Skip -> String -> Doc
text "SKIP"
    Assign v :: VAR
v t :: TERM ()
t -> VAR -> Doc
forall a. Pretty a => a -> Doc
pretty VAR
v Doc -> Doc -> Doc
<+> Doc
assign Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
    Call f :: FORMULA ()
f -> FORMULA () -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA ()
f
    Return t :: TERM ()
t -> String -> Doc
text "RETURN" Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
    Block vs :: [VAR_DECL]
vs p :: Program
p -> if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vs then Doc -> Doc
block (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
p else
      let (vds :: [VarDecl]
vds, q :: Program
q) = [VarDecl] -> Program -> ([VarDecl], Program)
addInits ([VAR_DECL] -> [VarDecl]
toVarDecl [VAR_DECL]
vs) Program
p
      in [Doc] -> Doc
sep [ String -> Doc
text "DECLARE"
             , [VarDecl] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [VarDecl]
vds Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
semi
             , Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
q ]
    Seq p1 :: Program
p1 p2 :: Program
p2 -> [Doc] -> Doc
vcat [Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
p1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
semi, Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
p2]
    If f :: FORMULA ()
f t :: Program
t e :: Program
e -> [Doc] -> Doc
sep
      [ String -> Doc
text "IF" Doc -> Doc -> Doc
<+> FORMULA () -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA ()
f
      , String -> Doc
text "THEN" Doc -> Doc -> Doc
<+> Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
t
      , case Program
e of
          Ranged Skip _ -> Doc
empty
          _ -> String -> Doc
text "ELSE" Doc -> Doc -> Doc
<+> Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
e
      , String -> Doc
text "FI" ]
    While f :: FORMULA ()
f p :: Program
p -> [Doc] -> Doc
sep
      [ String -> Doc
text "WHILE" Doc -> Doc -> Doc
<+> FORMULA () -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA ()
f
      , String -> Doc
text "DO" Doc -> Doc -> Doc
<+> Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
p
      , String -> Doc
text "OD" ]

instance FormExtension VSEforms

instance GetRange VSEforms

instance Pretty VSEforms where
  pretty :: VSEforms -> Doc
pretty v :: VSEforms
v = case VSEforms
v of
    Dlformula b :: BoxOrDiamond
b p :: Program
p f :: Sentence
f -> let d :: Doc
d = Program -> Doc
forall a. Pretty a => a -> Doc
pretty Program
p in [Doc] -> Doc
sep
      [ case BoxOrDiamond
b of
         Box -> String -> Doc
text "[:" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text ":]"
         Diamond -> String -> Doc
text "<:" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text ":>"
      , Sentence -> Doc
forall a. Pretty a => a -> Doc
pretty Sentence
f ]
    Defprocs ps :: [Defproc]
ps -> [Defproc] -> Doc
prettyProcdefs [Defproc]
ps
    RestrictedConstraint constrs :: [Constraint]
constrs restr :: Map SORT SORT
restr _b :: Bool
_b ->
       let l :: [Annoted DATATYPE_DECL]
l = [Constraint] -> [Annoted DATATYPE_DECL]
recoverType [Constraint]
constrs
       in [Doc] -> Doc
fsep [ String -> Doc
text "true %[generated type"
               , (DATATYPE_DECL -> Doc) -> [Annoted DATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos (Map SORT SORT -> DATATYPE_DECL -> Doc
printRestrTypedecl Map SORT SORT
restr) [Annoted DATATYPE_DECL]
l
               , String -> Doc
text "]%"]

genSortName :: String -> SORT -> Id
genSortName :: String -> SORT -> SORT
genSortName str :: String
str s :: SORT
s@(Id ts :: [VAR]
ts cs :: [SORT]
cs ps :: Range
ps) = case [SORT]
cs of
  [] -> String -> SORT
genName (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s
  i :: SORT
i : r :: [SORT]
r | SORT -> Bool
isQualName SORT
s -> [VAR] -> [SORT] -> Range -> SORT
Id [VAR]
ts (String -> SORT -> SORT
genSortName String
str SORT
i SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
r) Range
ps
  _ -> [VAR] -> [SORT] -> Range -> SORT
Id [String -> VAR
genToken (String -> VAR) -> String -> VAR
forall a b. (a -> b) -> a -> b
$ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show ([VAR] -> [SORT] -> Range -> SORT
Id [VAR]
ts [] Range
ps)] [SORT]
cs Range
ps

{- since such names are generated out of sentences, the qualification
   of the sort may be misleading -}
gnUniformName :: SORT -> Id
gnUniformName :: SORT -> SORT
gnUniformName = String -> SORT -> SORT
genSortName "uniform_" (SORT -> SORT) -> (SORT -> SORT) -> SORT -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SORT
unQualName

gnRestrName :: SORT -> Id
gnRestrName :: SORT -> SORT
gnRestrName = String -> SORT -> SORT
genSortName "restr_"

gnEqName :: SORT -> Id
gnEqName :: SORT -> SORT
gnEqName = String -> SORT -> SORT
genSortName "eq_"

genVars :: [SORT] -> [(Token, SORT)]
genVars :: [SORT] -> [(VAR, SORT)]
genVars = ((SORT, Int) -> (VAR, SORT)) -> [(SORT, Int)] -> [(VAR, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: SORT
t, n :: Int
n) -> (String -> Int -> VAR
genNumVar "x" Int
n, SORT
t)) ([(SORT, Int)] -> [(VAR, SORT)])
-> ([SORT] -> [(SORT, Int)]) -> [SORT] -> [(VAR, SORT)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> [(SORT, Int)]
forall a. [a] -> [(a, Int)]
number

xVar :: Token
xVar :: VAR
xVar = String -> VAR
genToken "x"

yVar :: Token
yVar :: VAR
yVar = String -> VAR
genToken "y"

printRestrTypedecl :: Map.Map SORT Id -> DATATYPE_DECL -> Doc
printRestrTypedecl :: Map SORT SORT -> DATATYPE_DECL -> Doc
printRestrTypedecl restr :: Map SORT SORT
restr (Datatype_decl s :: SORT
s a :: [Annoted ALTERNATIVE]
a r :: Range
r) =
    let pa :: Annoted ALTERNATIVE -> Doc
pa = (ALTERNATIVE -> Doc) -> Annoted ALTERNATIVE -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted ALTERNATIVE -> Doc
printALTERNATIVE in case [Annoted ALTERNATIVE]
a of
    [] -> Map SORT SORT -> DATATYPE_DECL -> Doc
printRestrTypedecl Map SORT SORT
restr
           (SORT -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl SORT
s [ALTERNATIVE -> Annoted ALTERNATIVE
forall a. a -> Annoted a
emptyAnno (ALTERNATIVE -> Annoted ALTERNATIVE)
-> ALTERNATIVE -> Annoted ALTERNATIVE
forall a b. (a -> b) -> a -> b
$ [SORT] -> Range -> ALTERNATIVE
Subsorts [SORT
s] Range
r] Range
r)
    h :: Annoted ALTERNATIVE
h : t :: [Annoted ALTERNATIVE]
t -> [Doc] -> Doc
sep [SORT -> Doc
idLabelDoc SORT
s, Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
sep
                      ((Doc
equals Doc -> Doc -> Doc
<+> Annoted ALTERNATIVE -> Doc
pa Annoted ALTERNATIVE
h) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                       (Annoted ALTERNATIVE -> Doc) -> [Annoted ALTERNATIVE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
bar Doc -> Doc -> Doc
<+>) (Doc -> Doc)
-> (Annoted ALTERNATIVE -> Doc) -> Annoted ALTERNATIVE -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ALTERNATIVE -> Doc
pa) [Annoted ALTERNATIVE]
t), String -> Doc
text "restricted by",
                   SORT -> Doc
forall a. Pretty a => a -> Doc
pretty (SORT -> Doc) -> SORT -> Doc
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> Map SORT SORT -> SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (SORT -> SORT
gnRestrName SORT
s) SORT
s Map SORT SORT
restr]

prettyProcdefs :: [Defproc] -> Doc
prettyProcdefs :: [Defproc] -> Doc
prettyProcdefs ps :: [Defproc]
ps = [Doc] -> Doc
vcat
  [ String -> Doc
text "DEFPROCS"
  , [Doc] -> Doc
vsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Defproc -> Doc) -> [Defproc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Defproc -> Doc
forall a. Pretty a => a -> Doc
pretty [Defproc]
ps
  , String -> Doc
text "DEFPROCSEND" ]

instance Pretty Procs where
  pretty :: Procs -> Doc
pretty (Procs m :: Map SORT Profile
m) =
    Procdecls -> Doc
forall a. Pretty a => a -> Doc
pretty (Procdecls -> Doc) -> Procdecls -> Doc
forall a b. (a -> b) -> a -> b
$ [Annoted Sigentry] -> Range -> Procdecls
Procdecls
       (((SORT, Profile) -> Annoted Sigentry)
-> [(SORT, Profile)] -> [Annoted Sigentry]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: SORT
i, p :: Profile
p) -> Sigentry -> Annoted Sigentry
forall a. a -> Annoted a
emptyAnno (Sigentry -> Annoted Sigentry) -> Sigentry -> Annoted Sigentry
forall a b. (a -> b) -> a -> b
$ SORT -> Profile -> Range -> Sigentry
Procedure SORT
i Profile
p Range
nullRange) ([(SORT, Profile)] -> [Annoted Sigentry])
-> [(SORT, Profile)] -> [Annoted Sigentry]
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
m)
       Range
nullRange