{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  TopHybrid/ATC_TopHybrid.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):
'TopHybrid.AS_TopHybrid.TH_BSPEC'
'TopHybrid.AS_TopHybrid.TH_BASIC_ITEM'
'TopHybrid.AS_TopHybrid.TH_FORMULA'
'TopHybrid.AS_TopHybrid.Mor'
'TopHybrid.TopHybridSign.THybridSign'
-}

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

module TopHybrid.ATC_TopHybrid () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.Json.Instances
import Common.Result
import Common.ToXml
import Control.Monad (liftM)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.Monoid ()
import Data.Set
import GHC.Generics(Generic)
import Logic.Logic
import Text.XML.Light
import TopHybrid.AS_TopHybrid
import TopHybrid.TopHybridSign
import Unsafe.Coerce

{-! for TopHybrid.AS_TopHybrid.TH_BSPEC derive : ShATermConvertible !-}
{-! for TopHybrid.AS_TopHybrid.TH_BASIC_ITEM derive : ShATermConvertible !-}
{-! for TopHybrid.AS_TopHybrid.TH_FORMULA derive : ShATermConvertible !-}
{-! for TopHybrid.AS_TopHybrid.Mor derive : ShATermConvertible !-}
{-! for TopHybrid.TopHybridSign.THybridSign derive : ShATermConvertible !-}

{-! for TopHybrid.AS_TopHybrid.TH_BSPEC derive : Json !-}
{-! for TopHybrid.AS_TopHybrid.TH_BASIC_ITEM derive : Json !-}
{-! for TopHybrid.AS_TopHybrid.TH_FORMULA derive : Json !-}
{-! for TopHybrid.AS_TopHybrid.Mor derive : Json !-}
{-! for TopHybrid.TopHybridSign.THybridSign derive : Json !-}

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

instance ShATermConvertible s => ShATermConvertible (TopHybrid.AS_TopHybrid.TH_BSPEC s) where
  toShATermAux :: ATermTable -> TH_BSPEC s -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TH_BSPEC s
xv = case TH_BSPEC s
xv of
    Bspec a :: [TH_BASIC_ITEM]
a b :: s
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TH_BASIC_ITEM] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TH_BASIC_ITEM]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> s -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 s
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 "Bspec" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_BSPEC s)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Bspec" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [TH_BASIC_ITEM])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TH_BASIC_ITEM]
a') ->
      case Int -> ATermTable -> (ATermTable, s)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: s
b') ->
      (ATermTable
att2, [TH_BASIC_ITEM] -> s -> TH_BSPEC s
forall s. [TH_BASIC_ITEM] -> s -> TH_BSPEC s
Bspec [TH_BASIC_ITEM]
a' s
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TH_BSPEC s)
forall a. String -> ShATerm -> a
fromShATermError "TopHybrid.AS_TopHybrid.TH_BSPEC" ShATerm
u

instance ShATermConvertible TopHybrid.AS_TopHybrid.TH_BASIC_ITEM where
  toShATermAux :: ATermTable -> TH_BASIC_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TH_BASIC_ITEM
xv = case TH_BASIC_ITEM
xv of
    Simple_mod_decl a :: [MODALITY]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [MODALITY] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [MODALITY]
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_decl" [Int
a'] []) ATermTable
att1
    Simple_nom_decl a :: [MODALITY]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [MODALITY] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [MODALITY]
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_nom_decl" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_BASIC_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Simple_mod_decl" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [MODALITY])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [MODALITY]
a') ->
      (ATermTable
att1, [MODALITY] -> TH_BASIC_ITEM
Simple_mod_decl [MODALITY]
a') }
    ShAAppl "Simple_nom_decl" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [MODALITY])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [MODALITY]
a') ->
      (ATermTable
att1, [MODALITY] -> TH_BASIC_ITEM
Simple_nom_decl [MODALITY]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TH_BASIC_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "TopHybrid.AS_TopHybrid.TH_BASIC_ITEM" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (TopHybrid.AS_TopHybrid.TH_FORMULA f) where
  toShATermAux :: ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TH_FORMULA f
xv = case TH_FORMULA f
xv of
    At a :: MODALITY
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "At" [Int
a', Int
b'] []) ATermTable
att2
    Uni a :: MODALITY
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Uni" [Int
a', Int
b'] []) ATermTable
att2
    Exist a :: MODALITY
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Exist" [Int
a', Int
b'] []) ATermTable
att2
    Box a :: MODALITY
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Box" [Int
a', Int
b'] []) ATermTable
att2
    Dia a :: MODALITY
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Dia" [Int
a', Int
b'] []) ATermTable
att2
    UnderLogic a :: f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 f
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 "UnderLogic" [Int
a'] []) ATermTable
att1
    Conjunction a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Conjunction" [Int
a', Int
b'] []) ATermTable
att2
    Disjunction a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Disjunction" [Int
a', Int
b'] []) ATermTable
att2
    Implication a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "Implication" [Int
a', Int
b'] []) ATermTable
att2
    BiImplication a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TH_FORMULA f
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 "BiImplication" [Int
a', Int
b'] []) ATermTable
att2
    Here a :: MODALITY
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODALITY -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODALITY
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 "Here" [Int
a'] []) ATermTable
att1
    Neg a :: TH_FORMULA f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
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 "Neg" [Int
a'] []) ATermTable
att1
    Par a :: TH_FORMULA f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TH_FORMULA f
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 "Par" [Int
a'] []) ATermTable
att1
    TrueA -> (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 "TrueA" [] []) ATermTable
att0
    FalseA -> (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 "FalseA" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_FORMULA f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "At" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
At MODALITY
a' TH_FORMULA f
b') }}
    ShAAppl "Uni" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Uni MODALITY
a' TH_FORMULA f
b') }}
    ShAAppl "Exist" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Exist MODALITY
a' TH_FORMULA f
b') }}
    ShAAppl "Box" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Box MODALITY
a' TH_FORMULA f
b') }}
    ShAAppl "Dia" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Dia MODALITY
a' TH_FORMULA f
b') }}
    ShAAppl "UnderLogic" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: f
a') ->
      (ATermTable
att1, f -> TH_FORMULA f
forall f. f -> TH_FORMULA f
UnderLogic f
a') }
    ShAAppl "Conjunction" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Conjunction TH_FORMULA f
a' TH_FORMULA f
b') }}
    ShAAppl "Disjunction" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Disjunction TH_FORMULA f
a' TH_FORMULA f
b') }}
    ShAAppl "Implication" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Implication TH_FORMULA f
a' TH_FORMULA f
b') }}
    ShAAppl "BiImplication" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TH_FORMULA f
b') ->
      (ATermTable
att2, TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
BiImplication TH_FORMULA f
a' TH_FORMULA f
b') }}
    ShAAppl "Here" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, MODALITY)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MODALITY
a') ->
      (ATermTable
att1, MODALITY -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f
Here MODALITY
a') }
    ShAAppl "Neg" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      (ATermTable
att1, TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Neg TH_FORMULA f
a') }
    ShAAppl "Par" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TH_FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TH_FORMULA f
a') ->
      (ATermTable
att1, TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Par TH_FORMULA f
a') }
    ShAAppl "TrueA" [] _ -> (ATermTable
att0, TH_FORMULA f
forall f. TH_FORMULA f
TrueA)
    ShAAppl "FalseA" [] _ -> (ATermTable
att0, TH_FORMULA f
forall f. TH_FORMULA f
FalseA)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TH_FORMULA f)
forall a. String -> ShATerm -> a
fromShATermError "TopHybrid.AS_TopHybrid.TH_FORMULA" ShATerm
u

instance ShATermConvertible TopHybrid.AS_TopHybrid.Mor where
  toShATermAux :: ATermTable -> Mor -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Mor
xv = case Mor
xv of
    Mor -> (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 "Mor" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Mor)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Mor" [] _ -> (ATermTable
att0, Mor
Mor)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Mor)
forall a. String -> ShATerm -> a
fromShATermError "TopHybrid.AS_TopHybrid.Mor" ShATerm
u

deriving instance GHC.Generics.Generic (TopHybrid.AS_TopHybrid.TH_BSPEC s)
instance Data.Aeson.ToJSON s => Data.Aeson.ToJSON (TopHybrid.AS_TopHybrid.TH_BSPEC s) where
instance Data.Aeson.FromJSON s => Data.Aeson.FromJSON (TopHybrid.AS_TopHybrid.TH_BSPEC s) where

deriving instance GHC.Generics.Generic TopHybrid.AS_TopHybrid.TH_BASIC_ITEM
instance Data.Aeson.ToJSON TopHybrid.AS_TopHybrid.TH_BASIC_ITEM where
instance Data.Aeson.FromJSON TopHybrid.AS_TopHybrid.TH_BASIC_ITEM where

deriving instance GHC.Generics.Generic (TopHybrid.AS_TopHybrid.TH_FORMULA f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (TopHybrid.AS_TopHybrid.TH_FORMULA f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (TopHybrid.AS_TopHybrid.TH_FORMULA f) where

deriving instance GHC.Generics.Generic TopHybrid.AS_TopHybrid.Mor
instance Data.Aeson.ToJSON TopHybrid.AS_TopHybrid.Mor where
instance Data.Aeson.FromJSON TopHybrid.AS_TopHybrid.Mor where

deriving instance GHC.Generics.Generic (TopHybrid.TopHybridSign.THybridSign s)
instance Data.Aeson.ToJSON s => Data.Aeson.ToJSON (TopHybrid.TopHybridSign.THybridSign s) where
instance Data.Aeson.FromJSON s => Data.Aeson.FromJSON (TopHybrid.TopHybridSign.THybridSign s) where

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