{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  CoCASL/ATC_CoCASL.der.hs
Description :  generated ShATermConvertible, Json instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(derive Typeable instances)

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json
  for the type(s):
'CoCASL.AS_CoCASL.C_BASIC_ITEM'
'CoCASL.AS_CoCASL.C_SIG_ITEM'
'CoCASL.AS_CoCASL.CODATATYPE_DECL'
'CoCASL.AS_CoCASL.COALTERNATIVE'
'CoCASL.AS_CoCASL.COCOMPONENTS'
'CoCASL.AS_CoCASL.MODALITY'
'CoCASL.AS_CoCASL.C_FORMULA'
'CoCASL.CoCASLSign.CoCASLSign'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
CoCASL/AS_CoCASL.hs
CoCASL/CoCASLSign.hs
-}

module CoCASL.ATC_CoCASL () where

import ATerm.Lib
import CASL.AS_Basic_CASL
import CASL.AS_Basic_CASL (SORT)
import CASL.ATC_CASL
import CASL.Sign
import CoCASL.AS_CoCASL
import CoCASL.CoCASLSign
import Common.AS_Annotation
import Common.Id
import Common.Json.Instances
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import GHC.Generics(Generic)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

{-! for CoCASL.AS_CoCASL.C_BASIC_ITEM derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.C_SIG_ITEM derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.CODATATYPE_DECL derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.COALTERNATIVE derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.COCOMPONENTS derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.MODALITY derive : ShATermConvertible !-}
{-! for CoCASL.AS_CoCASL.C_FORMULA derive : ShATermConvertible !-}
{-! for CoCASL.CoCASLSign.CoCASLSign derive : ShATermConvertible !-}

{-! for CoCASL.AS_CoCASL.C_BASIC_ITEM derive : Json !-}
{-! for CoCASL.AS_CoCASL.C_SIG_ITEM derive : Json !-}
{-! for CoCASL.AS_CoCASL.CODATATYPE_DECL derive : Json !-}
{-! for CoCASL.AS_CoCASL.COALTERNATIVE derive : Json !-}
{-! for CoCASL.AS_CoCASL.COCOMPONENTS derive : Json !-}
{-! for CoCASL.AS_CoCASL.MODALITY derive : Json !-}
{-! for CoCASL.AS_CoCASL.C_FORMULA derive : Json !-}
{-! for CoCASL.CoCASLSign.CoCASLSign derive : Json !-}

-- Generated by DrIFT, look but don't touch!

instance ShATermConvertible CoCASL.AS_CoCASL.C_BASIC_ITEM where
  toShATermAux :: ATermTable -> C_BASIC_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: C_BASIC_ITEM
xv = case C_BASIC_ITEM
xv of
    CoFree_datatype a :: [Annoted CODATATYPE_DECL]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted CODATATYPE_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted CODATATYPE_DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "CoFree_datatype" [Int
a', Int
b'] []) ATermTable
att2
    CoSort_gen a :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
-> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "CoSort_gen" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, C_BASIC_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CoFree_datatype" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted CODATATYPE_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted CODATATYPE_DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted CODATATYPE_DECL] -> Range -> C_BASIC_ITEM
CoFree_datatype [Annoted CODATATYPE_DECL]
a' Range
b') }}
    ShAAppl "CoSort_gen" [a :: Int
a, b :: Int
b] _ ->
      case Int
-> ATermTable
-> (ATermTable, [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> Range -> C_BASIC_ITEM
CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, C_BASIC_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.C_BASIC_ITEM" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.C_SIG_ITEM where
  toShATermAux :: ATermTable -> C_SIG_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: C_SIG_ITEM
xv = case C_SIG_ITEM
xv of
    CoDatatype_items a :: [Annoted CODATATYPE_DECL]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted CODATATYPE_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted CODATATYPE_DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "CoDatatype_items" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, C_SIG_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CoDatatype_items" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted CODATATYPE_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted CODATATYPE_DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted CODATATYPE_DECL] -> Range -> C_SIG_ITEM
CoDatatype_items [Annoted CODATATYPE_DECL]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, C_SIG_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.C_SIG_ITEM" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.CODATATYPE_DECL where
  toShATermAux :: ATermTable -> CODATATYPE_DECL -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CODATATYPE_DECL
xv = case CODATATYPE_DECL
xv of
    CoDatatype_decl a :: SORT
a b :: [Annoted COALTERNATIVE]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Annoted COALTERNATIVE] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Annoted COALTERNATIVE]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "CoDatatype_decl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, CODATATYPE_DECL)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CoDatatype_decl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, [Annoted COALTERNATIVE])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Annoted COALTERNATIVE]
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, SORT -> [Annoted COALTERNATIVE] -> Range -> CODATATYPE_DECL
CoDatatype_decl SORT
a' [Annoted COALTERNATIVE]
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CODATATYPE_DECL)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.CODATATYPE_DECL" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.COALTERNATIVE where
  toShATermAux :: ATermTable -> COALTERNATIVE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: COALTERNATIVE
xv = case COALTERNATIVE
xv of
    Co_construct a :: OpKind
a b :: Maybe SORT
b c :: [COCOMPONENTS]
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe SORT
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [COCOMPONENTS] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [COCOMPONENTS]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (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 "Co_construct" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    CoSubsorts a :: [SORT]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "CoSubsorts" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, COALTERNATIVE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Co_construct" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, OpKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpKind
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe SORT
b') ->
      case Int -> ATermTable -> (ATermTable, [COCOMPONENTS])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [COCOMPONENTS]
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, OpKind -> Maybe SORT -> [COCOMPONENTS] -> Range -> COALTERNATIVE
Co_construct OpKind
a' Maybe SORT
b' [COCOMPONENTS]
c' Range
d') }}}}
    ShAAppl "CoSubsorts" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [SORT] -> Range -> COALTERNATIVE
CoSubsorts [SORT]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, COALTERNATIVE)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.COALTERNATIVE" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.COCOMPONENTS where
  toShATermAux :: ATermTable -> COCOMPONENTS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: COCOMPONENTS
xv = case COCOMPONENTS
xv of
    CoSelect a :: [SORT]
a b :: OP_TYPE
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OP_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OP_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "CoSelect" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, COCOMPONENTS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CoSelect" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, OP_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: OP_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, [SORT] -> OP_TYPE -> Range -> COCOMPONENTS
CoSelect [SORT]
a' OP_TYPE
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, COCOMPONENTS)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.COCOMPONENTS" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.MODALITY where
  toShATermAux :: ATermTable -> MODALITY -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: MODALITY
xv = case MODALITY
xv of
    Simple_mod a :: SIMPLE_ID
a -> 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
      (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 "Simple_mod" [Int
a'] []) ATermTable
att1
    Term_mod a :: TERM C_FORMULA
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM C_FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM C_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 "Term_mod" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, MODALITY)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Simple_mod" [a :: Int
a] _ ->
      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') ->
      (ATermTable
att1, SIMPLE_ID -> MODALITY
Simple_mod SIMPLE_ID
a') }
    ShAAppl "Term_mod" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TERM C_FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM C_FORMULA
a') ->
      (ATermTable
att1, TERM C_FORMULA -> MODALITY
Term_mod TERM C_FORMULA
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MODALITY)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.MODALITY" ShATerm
u

instance ShATermConvertible CoCASL.AS_CoCASL.C_FORMULA where
  toShATermAux :: ATermTable -> C_FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: C_FORMULA
xv = case C_FORMULA
xv of
    BoxOrDiamond a :: Bool
a b :: MODALITY
b c :: FORMULA C_FORMULA
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 MODALITY
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FORMULA C_FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FORMULA C_FORMULA
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (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 "BoxOrDiamond" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    CoSort_gen_ax a :: [SORT]
a b :: [OP_SYMB]
b c :: Bool
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [OP_SYMB] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [OP_SYMB]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Bool
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 "CoSort_gen_ax" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, C_FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "BoxOrDiamond" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: MODALITY
b') ->
      case Int -> ATermTable -> (ATermTable, FORMULA C_FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FORMULA C_FORMULA
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
a' MODALITY
b' FORMULA C_FORMULA
c' Range
d') }}}}
    ShAAppl "CoSort_gen_ax" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, [OP_SYMB])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [OP_SYMB]
b') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Bool
c') ->
      (ATermTable
att3, [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
CoSort_gen_ax [SORT]
a' [OP_SYMB]
b' Bool
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, C_FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.AS_CoCASL.C_FORMULA" ShATerm
u

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.C_BASIC_ITEM
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.C_BASIC_ITEM where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.C_BASIC_ITEM where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.C_SIG_ITEM
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.C_SIG_ITEM where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.C_SIG_ITEM where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.CODATATYPE_DECL
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.CODATATYPE_DECL where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.CODATATYPE_DECL where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.COALTERNATIVE
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.COALTERNATIVE where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.COALTERNATIVE where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.COCOMPONENTS
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.COCOMPONENTS where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.COCOMPONENTS where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.MODALITY
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.MODALITY where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.MODALITY where

deriving instance GHC.Generics.Generic CoCASL.AS_CoCASL.C_FORMULA
instance Data.Aeson.ToJSON CoCASL.AS_CoCASL.C_FORMULA where
instance Data.Aeson.FromJSON CoCASL.AS_CoCASL.C_FORMULA where

deriving instance GHC.Generics.Generic CoCASL.CoCASLSign.CoCASLSign
instance Data.Aeson.ToJSON CoCASL.CoCASLSign.CoCASLSign where
instance Data.Aeson.FromJSON CoCASL.CoCASLSign.CoCASLSign where

instance ShATermConvertible CoCASL.CoCASLSign.CoCASLSign where
  toShATermAux :: ATermTable -> CoCASLSign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CoCASLSign
xv = case CoCASLSign
xv of
    CoCASLSign a :: Rel SORT
a b :: Rel SORT
b c :: OpMap
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Rel SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Rel SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Rel SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Rel SORT
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> OpMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 OpMap
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 "CoCASLSign" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, CoCASLSign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CoCASLSign" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Rel SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Rel SORT
a') ->
      case Int -> ATermTable -> (ATermTable, Rel SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Rel SORT
b') ->
      case Int -> ATermTable -> (ATermTable, OpMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: OpMap
c') ->
      (ATermTable
att3, Rel SORT -> Rel SORT -> OpMap -> CoCASLSign
CoCASLSign Rel SORT
a' Rel SORT
b' OpMap
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CoCASLSign)
forall a. String -> ShATerm -> a
fromShATermError "CoCASL.CoCASLSign.CoCASLSign" ShATerm
u