{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module Temporal.ATC_Temporal () where
import ATerm.Lib
import CASL.ATC_CASL
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Id as Id
import Common.Json.Instances
import Common.Result
import Control.Monad (unless)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import GHC.Generics(Generic)
import Temporal.AS_BASIC_Temporal
import Temporal.Morphism
import Temporal.Sign
import Temporal.Sign as Sign
import Temporal.Symbol
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Temporal.AS_BASIC_Temporal as AS_BASIC
import qualified Temporal.Morphism as Morphism
import qualified Temporal.Sign as Sign
deriving instance GHC.Generics.Generic Temporal.AS_BASIC_Temporal.SYMB_MAP_ITEMS
instance Data.Aeson.ToJSON Temporal.AS_BASIC_Temporal.SYMB_MAP_ITEMS where
instance Data.Aeson.FromJSON Temporal.AS_BASIC_Temporal.SYMB_MAP_ITEMS where
deriving instance GHC.Generics.Generic Temporal.AS_BASIC_Temporal.SYMB
instance Data.Aeson.ToJSON Temporal.AS_BASIC_Temporal.SYMB where
instance Data.Aeson.FromJSON Temporal.AS_BASIC_Temporal.SYMB where
deriving instance GHC.Generics.Generic Temporal.AS_BASIC_Temporal.SYMB_ITEMS
instance Data.Aeson.ToJSON Temporal.AS_BASIC_Temporal.SYMB_ITEMS where
instance Data.Aeson.FromJSON Temporal.AS_BASIC_Temporal.SYMB_ITEMS where
deriving instance GHC.Generics.Generic Temporal.AS_BASIC_Temporal.FORMULA
instance Data.Aeson.ToJSON Temporal.AS_BASIC_Temporal.FORMULA where
instance Data.Aeson.FromJSON Temporal.AS_BASIC_Temporal.FORMULA where
deriving instance GHC.Generics.Generic Temporal.AS_BASIC_Temporal.BASIC_SPEC
instance Data.Aeson.ToJSON Temporal.AS_BASIC_Temporal.BASIC_SPEC where
instance Data.Aeson.FromJSON Temporal.AS_BASIC_Temporal.BASIC_SPEC where
instance ShATermConvertible Temporal.AS_BASIC_Temporal.SYMB_MAP_ITEMS where
toShATermAux :: ATermTable -> SYMB_MAP_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_MAP_ITEMS
xv = case SYMB_MAP_ITEMS
xv of
Symb_map_items -> (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 "Symb_map_items" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_MAP_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb_map_items" [] _ -> (ATermTable
att0, SYMB_MAP_ITEMS
Symb_map_items)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_MAP_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.AS_BASIC_Temporal.SYMB_MAP_ITEMS" ShATerm
u
instance ShATermConvertible Temporal.AS_BASIC_Temporal.SYMB where
toShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB
xv = case SYMB
xv of
Symb_id -> (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 "Symb_id" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb_id" [] _ -> (ATermTable
att0, SYMB
Symb_id)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.AS_BASIC_Temporal.SYMB" ShATerm
u
instance ShATermConvertible Temporal.AS_BASIC_Temporal.SYMB_ITEMS where
toShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_ITEMS
xv = case SYMB_ITEMS
xv of
Symb_items -> (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 "Symb_items" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb_items" [] _ -> (ATermTable
att0, SYMB_ITEMS
Symb_items)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.AS_BASIC_Temporal.SYMB_ITEMS" ShATerm
u
instance ShATermConvertible Temporal.AS_BASIC_Temporal.FORMULA where
toShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FORMULA
xv = case FORMULA
xv of
Formula -> (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 "Formula" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Formula" [] _ -> (ATermTable
att0, FORMULA
Formula)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.AS_BASIC_Temporal.FORMULA" ShATerm
u
instance ShATermConvertible Temporal.AS_BASIC_Temporal.BASIC_SPEC where
toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_SPEC
xv = case BASIC_SPEC
xv of
Basic_spec -> (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 "Basic_spec" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Basic_spec" [] _ -> (ATermTable
att0, BASIC_SPEC
Basic_spec)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.AS_BASIC_Temporal.BASIC_SPEC" ShATerm
u
instance ShATermConvertible Temporal.Morphism.Morphism where
toShATermAux :: ATermTable -> Morphism -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Morphism
xv = case Morphism
xv of
Morphism a :: Sign
a b :: Sign
b c :: Map Id Id
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sign
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sign
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Map Id Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Map Id Id
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 "Morphism" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Morphism" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sign
a') ->
case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sign
b') ->
case Int -> ATermTable -> (ATermTable, Map Id Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Map Id Id
c') ->
(ATermTable
att3, Sign -> Sign -> Map Id Id -> Morphism
Morphism Sign
a' Sign
b' Map Id Id
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.Morphism.Morphism" ShATerm
u
deriving instance GHC.Generics.Generic Temporal.Morphism.Morphism
instance Data.Aeson.ToJSON Temporal.Morphism.Morphism where
instance Data.Aeson.FromJSON Temporal.Morphism.Morphism where
deriving instance GHC.Generics.Generic Temporal.Sign.Sign
instance Data.Aeson.ToJSON Temporal.Sign.Sign where
instance Data.Aeson.FromJSON Temporal.Sign.Sign where
instance ShATermConvertible Temporal.Sign.Sign where
toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
Sign a :: Set Id
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Set Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Set 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 "Sign" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Sign" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Set Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Set Id
a') ->
(ATermTable
att1, Set Id -> Sign
Sign Set Id
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.Sign.Sign" ShATerm
u
deriving instance GHC.Generics.Generic Temporal.Symbol.Symbol
instance Data.Aeson.ToJSON Temporal.Symbol.Symbol where
instance Data.Aeson.FromJSON Temporal.Symbol.Symbol where
instance ShATermConvertible Temporal.Symbol.Symbol where
toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symbol
xv = case Symbol
xv of
Symbol 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 "Symbol" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symbol" [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 -> Symbol
Symbol Id
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symbol)
forall a. String -> ShATerm -> a
fromShATermError "Temporal.Symbol.Symbol" ShATerm
u