{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module Framework.ATC_Framework () where
import ATC.AS_Annotation
import ATerm.Lib
import Common.Doc
import Common.DocUtils
import Common.IRI (IRI)
import Common.Id
import Common.Json.Instances
import Common.Keywords
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Framework.AS
import GHC.Generics(Generic)
deriving instance GHC.Generics.Generic Framework.AS.ComorphismDef
instance Data.Aeson.ToJSON Framework.AS.ComorphismDef where
instance Data.Aeson.FromJSON Framework.AS.ComorphismDef where
deriving instance GHC.Generics.Generic Framework.AS.LogicDef
instance Data.Aeson.ToJSON Framework.AS.LogicDef where
instance Data.Aeson.FromJSON Framework.AS.LogicDef where
deriving instance GHC.Generics.Generic Framework.AS.FRAM
instance Data.Aeson.ToJSON Framework.AS.FRAM where
instance Data.Aeson.FromJSON Framework.AS.FRAM where
instance ShATermConvertible Framework.AS.ComorphismDef where
toShATermAux :: ATermTable -> ComorphismDef -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ComorphismDef
xv = case ComorphismDef
xv of
ComorphismDef a :: NAME
a b :: FRAM
b c :: NAME
c d :: NAME
d e :: NAME
e f :: NAME
f g :: NAME
g -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FRAM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FRAM
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 NAME
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 NAME
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 NAME
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 NAME
f
(att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 NAME
g
(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 "ComorphismDef" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
Int
g'] []) ATermTable
att7
fromShATermAux :: Int -> ATermTable -> (ATermTable, ComorphismDef)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ComorphismDef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, FRAM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FRAM
b') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: NAME
c') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: NAME
d') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: NAME
e') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: NAME
f') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
{ (att7 :: ATermTable
att7, g' :: NAME
g') ->
(ATermTable
att7, NAME
-> FRAM -> NAME -> NAME -> NAME -> NAME -> NAME -> ComorphismDef
ComorphismDef NAME
a' FRAM
b' NAME
c' NAME
d' NAME
e' NAME
f' NAME
g') }}}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ComorphismDef)
forall a. String -> ShATerm -> a
fromShATermError "Framework.AS.ComorphismDef" ShATerm
u
instance ShATermConvertible Framework.AS.LogicDef where
toShATermAux :: ATermTable -> LogicDef -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: LogicDef
xv = case LogicDef
xv of
LogicDef a :: NAME
a b :: FRAM
b c :: NAME
c d :: NAME
d e :: NAME
e f :: NAME
f g :: PATTERN_NAME
g -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FRAM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FRAM
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 NAME
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 NAME
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 NAME
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 NAME
f
(att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> PATTERN_NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 PATTERN_NAME
g
(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 "LogicDef" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
Int
g'] []) ATermTable
att7
fromShATermAux :: Int -> ATermTable -> (ATermTable, LogicDef)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "LogicDef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, FRAM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FRAM
b') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: NAME
c') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: NAME
d') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: NAME
e') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: NAME
f') ->
case Int -> ATermTable -> (ATermTable, PATTERN_NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
{ (att7 :: ATermTable
att7, g' :: PATTERN_NAME
g') ->
(ATermTable
att7, NAME
-> FRAM -> NAME -> NAME -> NAME -> NAME -> PATTERN_NAME -> LogicDef
LogicDef NAME
a' FRAM
b' NAME
c' NAME
d' NAME
e' NAME
f' PATTERN_NAME
g') }}}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, LogicDef)
forall a. String -> ShATerm -> a
fromShATermError "Framework.AS.LogicDef" ShATerm
u
instance ShATermConvertible Framework.AS.FRAM where
toShATermAux :: ATermTable -> FRAM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FRAM
xv = case FRAM
xv of
LF -> (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 "LF" [] []) ATermTable
att0
Isabelle -> (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 "Isabelle" [] []) ATermTable
att0
Maude -> (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 "Maude" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, FRAM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "LF" [] _ -> (ATermTable
att0, FRAM
LF)
ShAAppl "Isabelle" [] _ -> (ATermTable
att0, FRAM
Isabelle)
ShAAppl "Maude" [] _ -> (ATermTable
att0, FRAM
Maude)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FRAM)
forall a. String -> ShATerm -> a
fromShATermError "Framework.AS.FRAM" ShATerm
u