{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  QBF/ATC_QBF.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):
'Propositional.Sign.Sign'
'QBF.Morphism.Morphism'
'QBF.AS_BASIC_QBF.PREDITEM'
'QBF.AS_BASIC_QBF.BASICSPEC'
'QBF.AS_BASIC_QBF.BASICITEMS'
'QBF.AS_BASIC_QBF.FORMULA'
'QBF.AS_BASIC_QBF.ID'
'QBF.AS_BASIC_QBF.SYMBITEMS'
'QBF.AS_BASIC_QBF.SYMB'
'QBF.AS_BASIC_QBF.SYMBMAPITEMS'
'QBF.AS_BASIC_QBF.SYMBORMAP'
'QBF.Symbol.Symbol'
'QBF.Sublogic.QBFFormulae'
'QBF.Sublogic.QBFSL'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
Propositional/Sign.hs
QBF/Morphism.hs
QBF/AS_BASIC_QBF.hs
QBF/Symbol.hs
QBF/Sublogic.hs
-}

module QBF.ATC_QBF () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation as AS_Anno
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Id as Id
import Common.Json.Instances
import Common.Keywords
import Common.Result
import Control.Monad (unless)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.Maybe (isJust)
import GHC.Generics(Generic)
import Propositional.Sign
import Propositional.Sign as Sign
import QBF.AS_BASIC_QBF
import QBF.Morphism
import QBF.Morphism as Morphism
import QBF.Sublogic
import QBF.Symbol
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.Lib.State as State
import qualified Common.Result as Result
import qualified Control.Monad.Fail as Fail
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Propositional.Sign as Sign
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Morphism as Morphism
import qualified QBF.Symbol as Symbol
import qualified QBF.Tools as Tools

{-! for Propositional.Sign.Sign derive : ShATermConvertible !-}
{-! for QBF.Morphism.Morphism derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.PREDITEM derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASICSPEC derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASICITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.ID derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBMAPITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBORMAP derive : ShATermConvertible !-}
{-! for QBF.Symbol.Symbol derive : ShATermConvertible !-}
{-! for QBF.Sublogic.QBFFormulae derive : ShATermConvertible !-}
{-! for QBF.Sublogic.QBFSL derive : ShATermConvertible !-}

{-! for Propositional.Sign.Sign derive : Json !-}
{-! for QBF.Morphism.Morphism derive : Json !-}
{-! for QBF.AS_BASIC_QBF.PREDITEM derive : Json !-}
{-! for QBF.AS_BASIC_QBF.BASICSPEC derive : Json !-}
{-! for QBF.AS_BASIC_QBF.BASICITEMS derive : Json !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : Json !-}
{-! for QBF.AS_BASIC_QBF.ID derive : Json !-}
{-! for QBF.AS_BASIC_QBF.SYMBITEMS derive : Json !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : Json !-}
{-! for QBF.AS_BASIC_QBF.SYMBMAPITEMS derive : Json !-}
{-! for QBF.AS_BASIC_QBF.SYMBORMAP derive : Json !-}
{-! for QBF.Symbol.Symbol derive : Json !-}
{-! for QBF.Sublogic.QBFFormulae derive : Json !-}
{-! for QBF.Sublogic.QBFSL derive : Json !-}

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

deriving instance GHC.Generics.Generic Propositional.Sign.Sign
instance Data.Aeson.ToJSON Propositional.Sign.Sign where
instance Data.Aeson.FromJSON Propositional.Sign.Sign where

instance ShATermConvertible Propositional.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 "Propositional.Sign.Sign" ShATerm
u

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.SYMBORMAP
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.SYMBORMAP where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.SYMBORMAP where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.SYMBMAPITEMS
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.SYMBMAPITEMS where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.SYMBMAPITEMS where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.SYMB
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.SYMB where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.SYMB where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.SYMBITEMS
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.SYMBITEMS where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.SYMBITEMS where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.ID
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.ID where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.ID where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.FORMULA
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.FORMULA where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.FORMULA where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.BASICITEMS
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.BASICITEMS where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.BASICITEMS where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.BASICSPEC
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.BASICSPEC where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.BASICSPEC where

deriving instance GHC.Generics.Generic QBF.AS_BASIC_QBF.PREDITEM
instance Data.Aeson.ToJSON QBF.AS_BASIC_QBF.PREDITEM where
instance Data.Aeson.FromJSON QBF.AS_BASIC_QBF.PREDITEM where

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

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

instance ShATermConvertible QBF.AS_BASIC_QBF.SYMB where
  toShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB
xv = case SYMB
xv of
    SymbId a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "SymbId" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SymbId" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> SYMB
SymbId Token
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB)
forall a. String -> ShATerm -> a
fromShATermError "QBF.AS_BASIC_QBF.SYMB" ShATerm
u

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

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

instance ShATermConvertible QBF.AS_BASIC_QBF.FORMULA where
  toShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FORMULA
xv = case FORMULA
xv of
    FalseAtom a :: Range
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Range
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 "FalseAtom" [Int
a'] []) ATermTable
att1
    TrueAtom a :: Range
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Range
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 "TrueAtom" [Int
a'] []) ATermTable
att1
    Predication a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "Predication" [Int
a'] []) ATermTable
att1
    Negation a :: FORMULA
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 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 "Negation" [Int
a', Int
b'] []) ATermTable
att2
    Conjunction a :: [FORMULA]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [FORMULA] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [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 "Conjunction" [Int
a', Int
b'] []) ATermTable
att2
    Disjunction a :: [FORMULA]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [FORMULA] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [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 "Disjunction" [Int
a', Int
b'] []) ATermTable
att2
    Implication a :: FORMULA
a b :: FORMULA
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FORMULA
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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 "Implication" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Equivalence a :: FORMULA
a b :: FORMULA
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FORMULA
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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 "Equivalence" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    ForAll a :: [Token]
a b :: FORMULA
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Token] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Token]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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 "ForAll" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Exists a :: [Token]
a b :: FORMULA
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Token] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Token]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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 "Exists" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FalseAtom" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Range
a') ->
      (ATermTable
att1, Range -> FORMULA
FalseAtom Range
a') }
    ShAAppl "TrueAtom" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Range
a') ->
      (ATermTable
att1, Range -> FORMULA
TrueAtom Range
a') }
    ShAAppl "Predication" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> FORMULA
Predication Token
a') }
    ShAAppl "Negation" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: 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, FORMULA -> Range -> FORMULA
Negation FORMULA
a' Range
b') }}
    ShAAppl "Conjunction" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [FORMULA])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [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, [FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
a' Range
b') }}
    ShAAppl "Disjunction" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [FORMULA])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [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, [FORMULA] -> Range -> FORMULA
Disjunction [FORMULA]
a' Range
b') }}
    ShAAppl "Implication" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FORMULA
a') ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
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, FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
a' FORMULA
b' Range
c') }}}
    ShAAppl "Equivalence" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FORMULA
a') ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
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, FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
a' FORMULA
b' Range
c') }}}
    ShAAppl "ForAll" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [Token])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Token]
a') ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
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, [Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
a' FORMULA
b' Range
c') }}}
    ShAAppl "Exists" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [Token])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Token]
a') ->
      case Int -> ATermTable -> (ATermTable, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
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, [Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
a' FORMULA
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "QBF.AS_BASIC_QBF.FORMULA" ShATerm
u

instance ShATermConvertible QBF.AS_BASIC_QBF.BASICITEMS where
  toShATermAux :: ATermTable -> BASICITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASICITEMS
xv = case BASICITEMS
xv of
    PredDecl a :: PREDITEM
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PREDITEM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PREDITEM
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 "PredDecl" [Int
a'] []) ATermTable
att1
    AxiomItems a :: [Annoted FORMULA]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted FORMULA] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted 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 "AxiomItems" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASICITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PredDecl" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, PREDITEM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PREDITEM
a') ->
      (ATermTable
att1, PREDITEM -> BASICITEMS
PredDecl PREDITEM
a') }
    ShAAppl "AxiomItems" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted FORMULA])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted FORMULA]
a') ->
      (ATermTable
att1, [Annoted FORMULA] -> BASICITEMS
AxiomItems [Annoted FORMULA]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASICITEMS)
forall a. String -> ShATerm -> a
fromShATermError "QBF.AS_BASIC_QBF.BASICITEMS" ShATerm
u

instance ShATermConvertible QBF.AS_BASIC_QBF.BASICSPEC where
  toShATermAux :: ATermTable -> BASICSPEC -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASICSPEC
xv = case BASICSPEC
xv of
    BasicSpec a :: [Annoted BASICITEMS]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted BASICITEMS] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted BASICITEMS]
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 "BasicSpec" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASICSPEC)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "BasicSpec" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted BASICITEMS])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted BASICITEMS]
a') ->
      (ATermTable
att1, [Annoted BASICITEMS] -> BASICSPEC
BasicSpec [Annoted BASICITEMS]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASICSPEC)
forall a. String -> ShATerm -> a
fromShATermError "QBF.AS_BASIC_QBF.BASICSPEC" ShATerm
u

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

instance ShATermConvertible QBF.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 "QBF.Morphism.Morphism" ShATerm
u

deriving instance GHC.Generics.Generic QBF.Morphism.Morphism
instance Data.Aeson.ToJSON QBF.Morphism.Morphism where
instance Data.Aeson.FromJSON QBF.Morphism.Morphism where

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

instance ShATermConvertible QBF.Sublogic.QBFSL where
  toShATermAux :: ATermTable -> QBFSL -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: QBFSL
xv = case QBFSL
xv of
    QBFSL a :: QBFFormulae
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QBFFormulae -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QBFFormulae
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 "QBFSL" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, QBFSL)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "QBFSL" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, QBFFormulae)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QBFFormulae
a') ->
      (ATermTable
att1, QBFFormulae -> QBFSL
QBFSL QBFFormulae
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, QBFSL)
forall a. String -> ShATerm -> a
fromShATermError "QBF.Sublogic.QBFSL" ShATerm
u

deriving instance GHC.Generics.Generic QBF.Sublogic.QBFFormulae
instance Data.Aeson.ToJSON QBF.Sublogic.QBFFormulae where
instance Data.Aeson.FromJSON QBF.Sublogic.QBFFormulae where

deriving instance GHC.Generics.Generic QBF.Sublogic.QBFSL
instance Data.Aeson.ToJSON QBF.Sublogic.QBFSL where
instance Data.Aeson.FromJSON QBF.Sublogic.QBFSL where

deriving instance GHC.Generics.Generic QBF.Symbol.Symbol
instance Data.Aeson.ToJSON QBF.Symbol.Symbol where
instance Data.Aeson.FromJSON QBF.Symbol.Symbol where

instance ShATermConvertible QBF.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 "QBF.Symbol.Symbol" ShATerm
u