{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  Propositional/ATC_Propositional.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'
'Propositional.Morphism.Morphism'
'Propositional.AS_BASIC_Propositional.PRED_ITEM'
'Propositional.AS_BASIC_Propositional.BASIC_SPEC'
'Propositional.AS_BASIC_Propositional.BASIC_ITEMS'
'Propositional.AS_BASIC_Propositional.FORMULA'
'Propositional.AS_BASIC_Propositional.SYMB_ITEMS'
'Propositional.AS_BASIC_Propositional.SYMB'
'Propositional.AS_BASIC_Propositional.SYMB_MAP_ITEMS'
'Propositional.AS_BASIC_Propositional.SYMB_OR_MAP'
'Propositional.Symbol.Symbol'
'Propositional.Sublogic.PropFormulae'
'Propositional.Sublogic.PropSL'
-}

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

module Propositional.ATC_Propositional () 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 GHC.Generics(Generic)
import Propositional.AS_BASIC_Propositional
import Propositional.Morphism
import Propositional.Morphism as Morphism
import Propositional.Sign
import Propositional.Sign as Sign
import Propositional.Sublogic
import Propositional.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.Map as Map
import qualified Data.Set as Set
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Morphism as Morphism
import qualified Propositional.Sign as Sign
import qualified Propositional.Symbol as Symbol
import qualified Propositional.Tools as Tools

{-! for Propositional.Sign.Sign derive : ShATermConvertible !-}
{-! for Propositional.Morphism.Morphism derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.PRED_ITEM derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.BASIC_SPEC derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.BASIC_ITEMS derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.FORMULA derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_OR_MAP derive : ShATermConvertible !-}
{-! for Propositional.Symbol.Symbol derive : ShATermConvertible !-}
{-! for Propositional.Sublogic.PropFormulae derive : ShATermConvertible !-}
{-! for Propositional.Sublogic.PropSL derive : ShATermConvertible !-}

{-! for Propositional.Sign.Sign derive : Json !-}
{-! for Propositional.Morphism.Morphism derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.PRED_ITEM derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.BASIC_SPEC derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.BASIC_ITEMS derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.FORMULA derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_ITEMS derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_MAP_ITEMS derive : Json !-}
{-! for Propositional.AS_BASIC_Propositional.SYMB_OR_MAP derive : Json !-}
{-! for Propositional.Symbol.Symbol derive : Json !-}
{-! for Propositional.Sublogic.PropFormulae derive : Json !-}
{-! for Propositional.Sublogic.PropSL derive : Json !-}

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

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

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

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

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

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

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

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

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

instance ShATermConvertible Propositional.AS_BASIC_Propositional.SYMB_OR_MAP where
  toShATermAux :: ATermTable -> SYMB_OR_MAP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_OR_MAP
xv = case SYMB_OR_MAP
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
    Symb_map 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 "Symb_map" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_OR_MAP)
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 -> SYMB_OR_MAP
Symb SYMB
a') }
    ShAAppl "Symb_map" [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 -> SYMB_OR_MAP
Symb_map SYMB
a' SYMB
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_OR_MAP)
forall a. String -> ShATerm -> a
fromShATermError "Propositional.AS_BASIC_Propositional.SYMB_OR_MAP" ShATerm
u

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

instance ShATermConvertible Propositional.AS_BASIC_Propositional.SYMB where
  toShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB
xv = case SYMB
xv of
    Symb_id 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 "Symb_id" [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 "Symb_id" [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
Symb_id Token
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB)
forall a. String -> ShATerm -> a
fromShATermError "Propositional.AS_BASIC_Propositional.SYMB" ShATerm
u

instance ShATermConvertible Propositional.AS_BASIC_Propositional.SYMB_ITEMS where
  toShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_ITEMS
xv = case SYMB_ITEMS
xv of
    Symb_items 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 "Symb_items" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Symb_items" [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 -> SYMB_ITEMS
Symb_items [SYMB]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "Propositional.AS_BASIC_Propositional.SYMB_ITEMS" ShATerm
u

instance ShATermConvertible Propositional.AS_BASIC_Propositional.FORMULA where
  toShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FORMULA
xv = case FORMULA
xv of
    False_atom 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 "False_atom" [Int
a'] []) ATermTable
att1
    True_atom 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 "True_atom" [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
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "False_atom" [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
False_atom Range
a') }
    ShAAppl "True_atom" [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
True_atom 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') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "Propositional.AS_BASIC_Propositional.FORMULA" ShATerm
u

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

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

instance ShATermConvertible Propositional.AS_BASIC_Propositional.PRED_ITEM where
  toShATermAux :: ATermTable -> PRED_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PRED_ITEM
xv = case PRED_ITEM
xv of
    Pred_item 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 "Pred_item" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Pred_item" [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 -> PRED_ITEM
Pred_item [Token]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PRED_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "Propositional.AS_BASIC_Propositional.PRED_ITEM" ShATerm
u

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

deriving instance GHC.Generics.Generic Propositional.Morphism.Morphism
instance Data.Aeson.ToJSON Propositional.Morphism.Morphism where
instance Data.Aeson.FromJSON Propositional.Morphism.Morphism 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 Propositional.Sign.Sign
instance Data.Aeson.ToJSON Propositional.Sign.Sign where
instance Data.Aeson.FromJSON Propositional.Sign.Sign where

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

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

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

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

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

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