{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Framework/AS.hs
Description :  Abstract syntax for logic definitions
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module Framework.AS where

import Common.Id
import Common.IRI (IRI)
import Common.Doc
import Common.DocUtils
import Common.Keywords

import Data.Data

type NAME = IRI
type SIG_NAME = IRI
type MORPH_NAME = IRI
type PATTERN_NAME = Token

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

data LogicDef = LogicDef
  { -- the name of the object logic
    LogicDef -> NAME
newlogicName :: NAME,
    -- the framework used for defining the object logic
    LogicDef -> FRAM
meta :: FRAM,
    {- name of the morphism specifying the sentences and truth judgement of the
       object logic -}
    LogicDef -> NAME
syntax :: MORPH_NAME,
    -- name of the morphism specifying the model category of the object logic
    LogicDef -> NAME
models :: MORPH_NAME,
    -- the foundation used to construct the model theory of the object logic
    LogicDef -> NAME
foundation :: SIG_NAME,
    -- name of the morphism specifying the proof category of the object logic
    LogicDef -> NAME
proofs :: MORPH_NAME,
    -- name of the pattern specifying the signature category of the object logic
    LogicDef -> PATTERN_NAME
patterns :: PATTERN_NAME
  } deriving (Int -> LogicDef -> ShowS
[LogicDef] -> ShowS
LogicDef -> String
(Int -> LogicDef -> ShowS)
-> (LogicDef -> String) -> ([LogicDef] -> ShowS) -> Show LogicDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LogicDef] -> ShowS
$cshowList :: [LogicDef] -> ShowS
show :: LogicDef -> String
$cshow :: LogicDef -> String
showsPrec :: Int -> LogicDef -> ShowS
$cshowsPrec :: Int -> LogicDef -> ShowS
Show, LogicDef -> LogicDef -> Bool
(LogicDef -> LogicDef -> Bool)
-> (LogicDef -> LogicDef -> Bool) -> Eq LogicDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LogicDef -> LogicDef -> Bool
$c/= :: LogicDef -> LogicDef -> Bool
== :: LogicDef -> LogicDef -> Bool
$c== :: LogicDef -> LogicDef -> Bool
Eq, Eq LogicDef
Eq LogicDef =>
(LogicDef -> LogicDef -> Ordering)
-> (LogicDef -> LogicDef -> Bool)
-> (LogicDef -> LogicDef -> Bool)
-> (LogicDef -> LogicDef -> Bool)
-> (LogicDef -> LogicDef -> Bool)
-> (LogicDef -> LogicDef -> LogicDef)
-> (LogicDef -> LogicDef -> LogicDef)
-> Ord LogicDef
LogicDef -> LogicDef -> Bool
LogicDef -> LogicDef -> Ordering
LogicDef -> LogicDef -> LogicDef
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 :: LogicDef -> LogicDef -> LogicDef
$cmin :: LogicDef -> LogicDef -> LogicDef
max :: LogicDef -> LogicDef -> LogicDef
$cmax :: LogicDef -> LogicDef -> LogicDef
>= :: LogicDef -> LogicDef -> Bool
$c>= :: LogicDef -> LogicDef -> Bool
> :: LogicDef -> LogicDef -> Bool
$c> :: LogicDef -> LogicDef -> Bool
<= :: LogicDef -> LogicDef -> Bool
$c<= :: LogicDef -> LogicDef -> Bool
< :: LogicDef -> LogicDef -> Bool
$c< :: LogicDef -> LogicDef -> Bool
compare :: LogicDef -> LogicDef -> Ordering
$ccompare :: LogicDef -> LogicDef -> Ordering
$cp1Ord :: Eq LogicDef
Ord, Typeable, Typeable LogicDef
Constr
DataType
Typeable LogicDef =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LogicDef -> c LogicDef)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LogicDef)
-> (LogicDef -> Constr)
-> (LogicDef -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LogicDef))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicDef))
-> ((forall b. Data b => b -> b) -> LogicDef -> LogicDef)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LogicDef -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LogicDef -> r)
-> (forall u. (forall d. Data d => d -> u) -> LogicDef -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LogicDef -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef)
-> Data LogicDef
LogicDef -> Constr
LogicDef -> DataType
(forall b. Data b => b -> b) -> LogicDef -> LogicDef
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicDef -> c LogicDef
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicDef
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) -> LogicDef -> u
forall u. (forall d. Data d => d -> u) -> LogicDef -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicDef
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicDef -> c LogicDef
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LogicDef)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicDef)
$cLogicDef :: Constr
$tLogicDef :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
gmapMp :: (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
gmapM :: (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
gmapQi :: Int -> (forall d. Data d => d -> u) -> LogicDef -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LogicDef -> u
gmapQ :: (forall d. Data d => d -> u) -> LogicDef -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LogicDef -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicDef -> r
gmapT :: (forall b. Data b => b -> b) -> LogicDef -> LogicDef
$cgmapT :: (forall b. Data b => b -> b) -> LogicDef -> LogicDef
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicDef)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicDef)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LogicDef)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LogicDef)
dataTypeOf :: LogicDef -> DataType
$cdataTypeOf :: LogicDef -> DataType
toConstr :: LogicDef -> Constr
$ctoConstr :: LogicDef -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicDef
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicDef
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicDef -> c LogicDef
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicDef -> c LogicDef
$cp1Data :: Typeable LogicDef
Data)

data ComorphismDef = ComorphismDef
  { -- the name of the comorphism
    ComorphismDef -> NAME
newcomorphismName :: NAME,
    -- the framework used for defining the comorphism
    ComorphismDef -> FRAM
metaC :: FRAM,
    -- name of the source logic
    ComorphismDef -> NAME
source :: SIG_NAME,
    -- name of the target logic
    ComorphismDef -> NAME
target :: SIG_NAME,
    {- name of the morphism between the syntax of the source logic and
       the syntax of the target logic -}
    ComorphismDef -> NAME
syntaxC :: MORPH_NAME,
    {- name of the morphism between the model category of the source logic and
       the model category of the target logic -}
    ComorphismDef -> NAME
modelC :: MORPH_NAME,
    {- name of the morphism between the proof category of the source logic and
       the proof category of the target logic -}
    ComorphismDef -> NAME
proofC :: MORPH_NAME
  } deriving (Int -> ComorphismDef -> ShowS
[ComorphismDef] -> ShowS
ComorphismDef -> String
(Int -> ComorphismDef -> ShowS)
-> (ComorphismDef -> String)
-> ([ComorphismDef] -> ShowS)
-> Show ComorphismDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ComorphismDef] -> ShowS
$cshowList :: [ComorphismDef] -> ShowS
show :: ComorphismDef -> String
$cshow :: ComorphismDef -> String
showsPrec :: Int -> ComorphismDef -> ShowS
$cshowsPrec :: Int -> ComorphismDef -> ShowS
Show, ComorphismDef -> ComorphismDef -> Bool
(ComorphismDef -> ComorphismDef -> Bool)
-> (ComorphismDef -> ComorphismDef -> Bool) -> Eq ComorphismDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComorphismDef -> ComorphismDef -> Bool
$c/= :: ComorphismDef -> ComorphismDef -> Bool
== :: ComorphismDef -> ComorphismDef -> Bool
$c== :: ComorphismDef -> ComorphismDef -> Bool
Eq, Eq ComorphismDef
Eq ComorphismDef =>
(ComorphismDef -> ComorphismDef -> Ordering)
-> (ComorphismDef -> ComorphismDef -> Bool)
-> (ComorphismDef -> ComorphismDef -> Bool)
-> (ComorphismDef -> ComorphismDef -> Bool)
-> (ComorphismDef -> ComorphismDef -> Bool)
-> (ComorphismDef -> ComorphismDef -> ComorphismDef)
-> (ComorphismDef -> ComorphismDef -> ComorphismDef)
-> Ord ComorphismDef
ComorphismDef -> ComorphismDef -> Bool
ComorphismDef -> ComorphismDef -> Ordering
ComorphismDef -> ComorphismDef -> ComorphismDef
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 :: ComorphismDef -> ComorphismDef -> ComorphismDef
$cmin :: ComorphismDef -> ComorphismDef -> ComorphismDef
max :: ComorphismDef -> ComorphismDef -> ComorphismDef
$cmax :: ComorphismDef -> ComorphismDef -> ComorphismDef
>= :: ComorphismDef -> ComorphismDef -> Bool
$c>= :: ComorphismDef -> ComorphismDef -> Bool
> :: ComorphismDef -> ComorphismDef -> Bool
$c> :: ComorphismDef -> ComorphismDef -> Bool
<= :: ComorphismDef -> ComorphismDef -> Bool
$c<= :: ComorphismDef -> ComorphismDef -> Bool
< :: ComorphismDef -> ComorphismDef -> Bool
$c< :: ComorphismDef -> ComorphismDef -> Bool
compare :: ComorphismDef -> ComorphismDef -> Ordering
$ccompare :: ComorphismDef -> ComorphismDef -> Ordering
$cp1Ord :: Eq ComorphismDef
Ord, Typeable, Typeable ComorphismDef
Constr
DataType
Typeable ComorphismDef =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ComorphismDef)
-> (ComorphismDef -> Constr)
-> (ComorphismDef -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ComorphismDef))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ComorphismDef))
-> ((forall b. Data b => b -> b) -> ComorphismDef -> ComorphismDef)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r)
-> (forall u. (forall d. Data d => d -> u) -> ComorphismDef -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ComorphismDef -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef)
-> Data ComorphismDef
ComorphismDef -> Constr
ComorphismDef -> DataType
(forall b. Data b => b -> b) -> ComorphismDef -> ComorphismDef
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ComorphismDef
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) -> ComorphismDef -> u
forall u. (forall d. Data d => d -> u) -> ComorphismDef -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ComorphismDef
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ComorphismDef)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ComorphismDef)
$cComorphismDef :: Constr
$tComorphismDef :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
gmapMp :: (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
gmapM :: (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
gmapQi :: Int -> (forall d. Data d => d -> u) -> ComorphismDef -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ComorphismDef -> u
gmapQ :: (forall d. Data d => d -> u) -> ComorphismDef -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ComorphismDef -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r
gmapT :: (forall b. Data b => b -> b) -> ComorphismDef -> ComorphismDef
$cgmapT :: (forall b. Data b => b -> b) -> ComorphismDef -> ComorphismDef
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ComorphismDef)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ComorphismDef)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ComorphismDef)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ComorphismDef)
dataTypeOf :: ComorphismDef -> DataType
$cdataTypeOf :: ComorphismDef -> DataType
toConstr :: ComorphismDef -> Constr
$ctoConstr :: ComorphismDef -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ComorphismDef
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ComorphismDef
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef
$cp1Data :: Typeable ComorphismDef
Data)

instance GetRange LogicDef
instance GetRange ComorphismDef

instance Pretty LogicDef where
    pretty :: LogicDef -> Doc
pretty = LogicDef -> Doc
printLogicDef
instance Pretty ComorphismDef where
    pretty :: ComorphismDef -> Doc
pretty = ComorphismDef -> Doc
printComorphismDef
instance Pretty FRAM where
    pretty :: FRAM -> Doc
pretty = FRAM -> Doc
printFram

printLogicDef :: LogicDef -> Doc
printLogicDef :: LogicDef -> Doc
printLogicDef (LogicDef l :: NAME
l ml :: FRAM
ml s :: NAME
s m :: NAME
m f :: NAME
f p :: NAME
p pa :: PATTERN_NAME
pa) =
  [Doc] -> Doc
vcat [ String -> Doc
text String
newlogicS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
l
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
metaS Doc -> Doc -> Doc
<+> FRAM -> Doc
forall a. Pretty a => a -> Doc
pretty FRAM
ml
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
syntaxS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
s
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
modelsS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
m
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
foundationS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
f
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
proofsS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
p
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
patternsS Doc -> Doc -> Doc
<+> PATTERN_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty PATTERN_NAME
pa
       ]

printComorphismDef :: ComorphismDef -> Doc
printComorphismDef :: ComorphismDef -> Doc
printComorphismDef (ComorphismDef c :: NAME
c ml :: FRAM
ml sl :: NAME
sl tl :: NAME
tl s :: NAME
s m :: NAME
m p :: NAME
p) =
  [Doc] -> Doc
vcat [ String -> Doc
text String
newcomorphismS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
c
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
metaS Doc -> Doc -> Doc
<+> FRAM -> Doc
forall a. Pretty a => a -> Doc
pretty FRAM
ml
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
sourceS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
sl
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
targetS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
tl
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
syntaxS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
s
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
modelsS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
m
       , String -> Doc
text " " Doc -> Doc -> Doc
<+> String -> Doc
text String
proofsS Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
p
       ]

printFram :: FRAM -> Doc
printFram :: FRAM -> Doc
printFram LF = String -> Doc
text "LF"
printFram Isabelle = String -> Doc
text "Isabelle"
printFram Maude = String -> Doc
text "Maude"