{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module CASL_DL.ATC_CASL_DL () where
import ATerm.Lib
import CASL.AS_Basic_CASL
import CASL.ATC_CASL
import CASL_DL.AS_CASL_DL
import CASL_DL.Print_AS ()
import CASL_DL.Sign
import CASL_DL.Sublogics
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Json.Instances
import Control.Exception
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List (union, (\\), isPrefixOf)
import GHC.Generics(Generic)
import qualified Data.Map as Map
instance ShATermConvertible CASL_DL.AS_CASL_DL.CardType where
toShATermAux :: ATermTable -> CardType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CardType
xv = case CardType
xv of
CMin -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CMin" [] []) ATermTable
att0
CMax -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CMax" [] []) ATermTable
att0
CExact -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CExact" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, CardType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "CMin" [] _ -> (ATermTable
att0, CardType
CMin)
ShAAppl "CMax" [] _ -> (ATermTable
att0, CardType
CMax)
ShAAppl "CExact" [] _ -> (ATermTable
att0, CardType
CExact)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CardType)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.AS_CASL_DL.CardType" ShATerm
u
instance ShATermConvertible CASL_DL.AS_CASL_DL.DL_FORMULA where
toShATermAux :: ATermTable -> DL_FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DL_FORMULA
xv = case DL_FORMULA
xv of
Cardinality a :: CardType
a b :: PRED_SYMB
b c :: TERM DL_FORMULA
c d :: TERM DL_FORMULA
d e :: Maybe (FORMULA DL_FORMULA)
e f :: Range
f -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> CardType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 CardType
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PRED_SYMB -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PRED_SYMB
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TERM DL_FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TERM DL_FORMULA
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> TERM DL_FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 TERM DL_FORMULA
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Maybe (FORMULA DL_FORMULA) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Maybe (FORMULA DL_FORMULA)
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 Range
f
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Cardinality" [Int
a', Int
b', Int
c', Int
d', Int
e',
Int
f'] []) ATermTable
att6
fromShATermAux :: Int -> ATermTable -> (ATermTable, DL_FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Cardinality" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
case Int -> ATermTable -> (ATermTable, CardType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: CardType
a') ->
case Int -> ATermTable -> (ATermTable, PRED_SYMB)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: PRED_SYMB
b') ->
case Int -> ATermTable -> (ATermTable, TERM DL_FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TERM DL_FORMULA
c') ->
case Int -> ATermTable -> (ATermTable, TERM DL_FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: TERM DL_FORMULA
d') ->
case Int -> ATermTable -> (ATermTable, Maybe (FORMULA DL_FORMULA))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Maybe (FORMULA DL_FORMULA)
e') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: Range
f') ->
(ATermTable
att6, CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
a' PRED_SYMB
b' TERM DL_FORMULA
c' TERM DL_FORMULA
d' Maybe (FORMULA DL_FORMULA)
e' Range
f') }}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DL_FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.AS_CASL_DL.DL_FORMULA" ShATerm
u
deriving instance GHC.Generics.Generic CASL_DL.AS_CASL_DL.CardType
instance Data.Aeson.ToJSON CASL_DL.AS_CASL_DL.CardType where
instance Data.Aeson.FromJSON CASL_DL.AS_CASL_DL.CardType where
deriving instance GHC.Generics.Generic CASL_DL.AS_CASL_DL.DL_FORMULA
instance Data.Aeson.ToJSON CASL_DL.AS_CASL_DL.DL_FORMULA where
instance Data.Aeson.FromJSON CASL_DL.AS_CASL_DL.DL_FORMULA where
instance ShATermConvertible CASL_DL.Sign.CASL_DLSign where
toShATermAux :: ATermTable -> CASL_DLSign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CASL_DLSign
xv = case CASL_DLSign
xv of
CASL_DLSign a :: Map SIMPLE_ID PropertyType
a b :: [AnnoAppl]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Map SIMPLE_ID PropertyType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Map SIMPLE_ID PropertyType
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [AnnoAppl] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [AnnoAppl]
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CASL_DLSign" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_DLSign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "CASL_DLSign" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Map SIMPLE_ID PropertyType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Map SIMPLE_ID PropertyType
a') ->
case Int -> ATermTable -> (ATermTable, [AnnoAppl])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [AnnoAppl]
b') ->
(ATermTable
att2, Map SIMPLE_ID PropertyType -> [AnnoAppl] -> CASL_DLSign
CASL_DLSign Map SIMPLE_ID PropertyType
a' [AnnoAppl]
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CASL_DLSign)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.Sign.CASL_DLSign" ShATerm
u
instance ShATermConvertible CASL_DL.Sign.PropertyType where
toShATermAux :: ATermTable -> PropertyType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PropertyType
xv = case PropertyType
xv of
AnnoProperty -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AnnoProperty" [] []) ATermTable
att0
OntoProperty -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "OntoProperty" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, PropertyType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "AnnoProperty" [] _ -> (ATermTable
att0, PropertyType
AnnoProperty)
ShAAppl "OntoProperty" [] _ -> (ATermTable
att0, PropertyType
OntoProperty)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PropertyType)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.Sign.PropertyType" ShATerm
u
instance ShATermConvertible CASL_DL.Sign.AnnoAppl where
toShATermAux :: ATermTable -> AnnoAppl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AnnoAppl
xv = case AnnoAppl
xv of
AnnoAppl a :: SIMPLE_ID
a b :: Id
b c :: AnnoLiteral
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SIMPLE_ID -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SIMPLE_ID
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Id
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> AnnoLiteral -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 AnnoLiteral
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AnnoAppl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, AnnoAppl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "AnnoAppl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, SIMPLE_ID)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SIMPLE_ID
a') ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Id
b') ->
case Int -> ATermTable -> (ATermTable, AnnoLiteral)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: AnnoLiteral
c') ->
(ATermTable
att3, SIMPLE_ID -> Id -> AnnoLiteral -> AnnoAppl
AnnoAppl SIMPLE_ID
a' Id
b' AnnoLiteral
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AnnoAppl)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.Sign.AnnoAppl" ShATerm
u
instance ShATermConvertible CASL_DL.Sign.AnnoLiteral where
toShATermAux :: ATermTable -> AnnoLiteral -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AnnoLiteral
xv = case AnnoLiteral
xv of
AL_Term a :: TERM DL_FORMULA
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM DL_FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM DL_FORMULA
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AL_Term" [Int
a'] []) ATermTable
att1
AL_Id a :: Id
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AL_Id" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, AnnoLiteral)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "AL_Term" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TERM DL_FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TERM DL_FORMULA
a') ->
(ATermTable
att1, TERM DL_FORMULA -> AnnoLiteral
AL_Term TERM DL_FORMULA
a') }
ShAAppl "AL_Id" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
(ATermTable
att1, Id -> AnnoLiteral
AL_Id Id
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AnnoLiteral)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.Sign.AnnoLiteral" ShATerm
u
deriving instance GHC.Generics.Generic CASL_DL.Sign.CASL_DLSign
instance Data.Aeson.ToJSON CASL_DL.Sign.CASL_DLSign where
instance Data.Aeson.FromJSON CASL_DL.Sign.CASL_DLSign where
deriving instance GHC.Generics.Generic CASL_DL.Sign.PropertyType
instance Data.Aeson.ToJSON CASL_DL.Sign.PropertyType where
instance Data.Aeson.FromJSON CASL_DL.Sign.PropertyType where
deriving instance GHC.Generics.Generic CASL_DL.Sign.AnnoAppl
instance Data.Aeson.ToJSON CASL_DL.Sign.AnnoAppl where
instance Data.Aeson.FromJSON CASL_DL.Sign.AnnoAppl where
deriving instance GHC.Generics.Generic CASL_DL.Sign.AnnoLiteral
instance Data.Aeson.ToJSON CASL_DL.Sign.AnnoLiteral where
instance Data.Aeson.FromJSON CASL_DL.Sign.AnnoLiteral where
deriving instance GHC.Generics.Generic CASL_DL.Sublogics.CASL_DL_SL
instance Data.Aeson.ToJSON CASL_DL.Sublogics.CASL_DL_SL where
instance Data.Aeson.FromJSON CASL_DL.Sublogics.CASL_DL_SL where
instance ShATermConvertible CASL_DL.Sublogics.CASL_DL_SL where
toShATermAux :: ATermTable -> CASL_DL_SL -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CASL_DL_SL
xv = case CASL_DL_SL
xv of
SROIQ -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SROIQ" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_DL_SL)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SROIQ" [] _ -> (ATermTable
att0, CASL_DL_SL
SROIQ)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CASL_DL_SL)
forall a. String -> ShATerm -> a
fromShATermError "CASL_DL.Sublogics.CASL_DL_SL" ShATerm
u