{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  DFOL/ATC_DFOL.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):
'DFOL.AS_DFOL.BASIC_SPEC'
'DFOL.AS_DFOL.BASIC_ITEM'
'DFOL.AS_DFOL.TYPE'
'DFOL.AS_DFOL.TERM'
'DFOL.AS_DFOL.FORMULA'
'DFOL.AS_DFOL.SYMB_ITEMS'
'DFOL.AS_DFOL.SYMB_MAP_ITEMS'
'DFOL.AS_DFOL.SYMB_OR_MAP'
'DFOL.Sign.KIND'
'DFOL.Sign.CONTEXT'
'DFOL.Sign.Sign'
'DFOL.Morphism.Morphism'
'DFOL.Symbol.Symbol'
-}

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

module DFOL.ATC_DFOL () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.Json.Instances
import Common.Result
import DFOL.AS_DFOL
import DFOL.Morphism
import DFOL.Sign
import DFOL.Symbol
import DFOL.Utils
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List
import GHC.Generics(Generic)
import qualified Common.Result as Result
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for DFOL.AS_DFOL.BASIC_SPEC derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.BASIC_ITEM derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.TYPE derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.TERM derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.FORMULA derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for DFOL.AS_DFOL.SYMB_OR_MAP derive : ShATermConvertible !-}
{-! for DFOL.Sign.KIND derive : ShATermConvertible !-}
{-! for DFOL.Sign.CONTEXT derive : ShATermConvertible !-}
{-! for DFOL.Sign.Sign derive : ShATermConvertible !-}
{-! for DFOL.Morphism.Morphism derive : ShATermConvertible !-}
{-! for DFOL.Symbol.Symbol derive : ShATermConvertible !-}

{-! for DFOL.AS_DFOL.BASIC_SPEC derive : Json !-}
{-! for DFOL.AS_DFOL.BASIC_ITEM derive : Json !-}
{-! for DFOL.AS_DFOL.TYPE derive : Json !-}
{-! for DFOL.AS_DFOL.TERM derive : Json !-}
{-! for DFOL.AS_DFOL.FORMULA derive : Json !-}
{-! for DFOL.AS_DFOL.SYMB_ITEMS derive : Json !-}
{-! for DFOL.AS_DFOL.SYMB_MAP_ITEMS derive : Json !-}
{-! for DFOL.AS_DFOL.SYMB_OR_MAP derive : Json !-}
{-! for DFOL.Sign.KIND derive : Json !-}
{-! for DFOL.Sign.CONTEXT derive : Json !-}
{-! for DFOL.Sign.Sign derive : Json !-}
{-! for DFOL.Morphism.Morphism derive : Json !-}
{-! for DFOL.Symbol.Symbol derive : Json !-}

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

instance ShATermConvertible DFOL.AS_DFOL.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_ITEM]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted BASIC_ITEM] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted BASIC_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 "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_ITEM])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted BASIC_ITEM]
a') ->
      (ATermTable
att1, [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec [Annoted BASIC_ITEM]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.BASIC_SPEC" ShATerm
u

instance ShATermConvertible DFOL.AS_DFOL.BASIC_ITEM where
  toShATermAux :: ATermTable -> BASIC_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_ITEM
xv = case BASIC_ITEM
xv of
    Decl_item a :: DECL
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DECL -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DECL
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 "Decl_item" [Int
a'] []) ATermTable
att1
    Axiom_item a :: FORMULA
a -> 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
      (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_item" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Decl_item" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DECL)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DECL
a') ->
      (ATermTable
att1, DECL -> BASIC_ITEM
Decl_item DECL
a') }
    ShAAppl "Axiom_item" [a :: Int
a] _ ->
      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') ->
      (ATermTable
att1, FORMULA -> BASIC_ITEM
Axiom_item FORMULA
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.BASIC_ITEM" ShATerm
u

instance ShATermConvertible DFOL.AS_DFOL.TYPE where
  toShATermAux :: ATermTable -> TYPE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TYPE
xv = case TYPE
xv of
    Sort -> (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 "Sort" [] []) ATermTable
att0
    Form -> (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 "Form" [] []) ATermTable
att0
    Univ a :: TERM
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM
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 "Univ" [Int
a'] []) ATermTable
att1
    Func a :: [TYPE]
a b :: TYPE
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TYPE] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TYPE]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TYPE
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 "Func" [Int
a', Int
b'] []) ATermTable
att2
    Pi a :: [DECL]
a b :: TYPE
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TYPE
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 "Pi" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TYPE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sort" [] _ -> (ATermTable
att0, TYPE
Sort)
    ShAAppl "Form" [] _ -> (ATermTable
att0, TYPE
Form)
    ShAAppl "Univ" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TERM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM
a') ->
      (ATermTable
att1, TERM -> TYPE
Univ TERM
a') }
    ShAAppl "Func" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [TYPE])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TYPE]
a') ->
      case Int -> ATermTable -> (ATermTable, TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TYPE
b') ->
      (ATermTable
att2, [TYPE] -> TYPE -> TYPE
Func [TYPE]
a' TYPE
b') }}
    ShAAppl "Pi" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TYPE
b') ->
      (ATermTable
att2, [DECL] -> TYPE -> TYPE
Pi [DECL]
a' TYPE
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TYPE)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.TYPE" ShATerm
u

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

instance ShATermConvertible DFOL.AS_DFOL.FORMULA where
  toShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FORMULA
xv = case FORMULA
xv of
    T -> (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 "T" [] []) ATermTable
att0
    F -> (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 "F" [] []) ATermTable
att0
    Pred a :: TERM
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM
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" [Int
a'] []) ATermTable
att1
    Equality a :: TERM
a b :: TERM
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TERM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TERM
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 "Equality" [Int
a', Int
b'] []) ATermTable
att2
    Negation a :: FORMULA
a -> 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
      (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'] []) ATermTable
att1
    Conjunction a :: [FORMULA]
a -> 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
      (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'] []) ATermTable
att1
    Disjunction a :: [FORMULA]
a -> 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
      (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'] []) ATermTable
att1
    Implication a :: FORMULA
a b :: FORMULA
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 -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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
    Equivalence a :: FORMULA
a b :: FORMULA
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 -> FORMULA -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA
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 "Equivalence" [Int
a', Int
b'] []) ATermTable
att2
    Forall a :: [DECL]
a b :: FORMULA
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [DECL]
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
      (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'] []) ATermTable
att2
    Exists a :: [DECL]
a b :: FORMULA
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [DECL]
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
      (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'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "T" [] _ -> (ATermTable
att0, FORMULA
T)
    ShAAppl "F" [] _ -> (ATermTable
att0, FORMULA
F)
    ShAAppl "Pred" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TERM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM
a') ->
      (ATermTable
att1, TERM -> FORMULA
Pred TERM
a') }
    ShAAppl "Equality" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TERM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM
a') ->
      case Int -> ATermTable -> (ATermTable, TERM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TERM
b') ->
      (ATermTable
att2, TERM -> TERM -> FORMULA
Equality TERM
a' TERM
b') }}
    ShAAppl "Negation" [a :: Int
a] _ ->
      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') ->
      (ATermTable
att1, FORMULA -> FORMULA
Negation FORMULA
a') }
    ShAAppl "Conjunction" [a :: Int
a] _ ->
      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') ->
      (ATermTable
att1, [FORMULA] -> FORMULA
Conjunction [FORMULA]
a') }
    ShAAppl "Disjunction" [a :: Int
a] _ ->
      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') ->
      (ATermTable
att1, [FORMULA] -> FORMULA
Disjunction [FORMULA]
a') }
    ShAAppl "Implication" [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, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
b') ->
      (ATermTable
att2, FORMULA -> FORMULA -> FORMULA
Implication FORMULA
a' FORMULA
b') }}
    ShAAppl "Equivalence" [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, FORMULA)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA
b') ->
      (ATermTable
att2, FORMULA -> FORMULA -> FORMULA
Equivalence FORMULA
a' FORMULA
b') }}
    ShAAppl "Forall" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [DECL]
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') ->
      (ATermTable
att2, [DECL] -> FORMULA -> FORMULA
Forall [DECL]
a' FORMULA
b') }}
    ShAAppl "Exists" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [DECL]
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') ->
      (ATermTable
att2, [DECL] -> FORMULA -> FORMULA
Exists [DECL]
a' FORMULA
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FORMULA)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.FORMULA" ShATerm
u

instance ShATermConvertible DFOL.AS_DFOL.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 :: [NAME]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [NAME] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [NAME]
a
      (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'] []) ATermTable
att1
  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] _ ->
      case Int -> ATermTable -> (ATermTable, [NAME])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [NAME]
a') ->
      (ATermTable
att1, [NAME] -> SYMB_ITEMS
Symb_items [NAME]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.SYMB_ITEMS" ShATerm
u

instance ShATermConvertible DFOL.AS_DFOL.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 -> 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
      (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'] []) ATermTable
att1
  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] _ ->
      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') ->
      (ATermTable
att1, [SYMB_OR_MAP] -> SYMB_MAP_ITEMS
Symb_map_items [SYMB_OR_MAP]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_MAP_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.SYMB_MAP_ITEMS" ShATerm
u

instance ShATermConvertible DFOL.AS_DFOL.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 :: NAME
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
      (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 :: NAME
a b :: NAME
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 NAME
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" [Int
a', Int
b'] []) ATermTable
att2
  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, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NAME
a') ->
      (ATermTable
att1, NAME -> SYMB_OR_MAP
Symb NAME
a') }
    ShAAppl "Symb_map" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NAME
a') ->
      case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: NAME
b') ->
      (ATermTable
att2, NAME -> NAME -> SYMB_OR_MAP
Symb_map NAME
a' NAME
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_OR_MAP)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.AS_DFOL.SYMB_OR_MAP" ShATerm
u

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.BASIC_SPEC
instance Data.Aeson.ToJSON DFOL.AS_DFOL.BASIC_SPEC where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.BASIC_SPEC where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.BASIC_ITEM
instance Data.Aeson.ToJSON DFOL.AS_DFOL.BASIC_ITEM where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.BASIC_ITEM where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.TYPE
instance Data.Aeson.ToJSON DFOL.AS_DFOL.TYPE where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.TYPE where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.TERM
instance Data.Aeson.ToJSON DFOL.AS_DFOL.TERM where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.TERM where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.FORMULA
instance Data.Aeson.ToJSON DFOL.AS_DFOL.FORMULA where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.FORMULA where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.SYMB_ITEMS
instance Data.Aeson.ToJSON DFOL.AS_DFOL.SYMB_ITEMS where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.SYMB_ITEMS where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.SYMB_MAP_ITEMS
instance Data.Aeson.ToJSON DFOL.AS_DFOL.SYMB_MAP_ITEMS where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.SYMB_MAP_ITEMS where

deriving instance GHC.Generics.Generic DFOL.AS_DFOL.SYMB_OR_MAP
instance Data.Aeson.ToJSON DFOL.AS_DFOL.SYMB_OR_MAP where
instance Data.Aeson.FromJSON DFOL.AS_DFOL.SYMB_OR_MAP where

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

instance ShATermConvertible DFOL.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 NAME NAME
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 NAME NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Map NAME NAME
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 NAME NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Map NAME NAME
c') ->
      (ATermTable
att3, Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
a' Sign
b' Map NAME NAME
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.Morphism.Morphism" ShATerm
u

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

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

instance ShATermConvertible DFOL.Sign.Sign where
  toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
    Sign a :: [DECL]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [DECL]
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, [DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [DECL]
a') ->
      (ATermTable
att1, [DECL] -> Sign
Sign [DECL]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.Sign.Sign" ShATerm
u

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

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

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

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

instance ShATermConvertible DFOL.Symbol.Symbol where
  toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symbol
xv = case Symbol
xv of
    Symbol a :: NAME
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
      (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, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NAME
a') ->
      (ATermTable
att1, NAME -> Symbol
Symbol NAME
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symbol)
forall a. String -> ShATerm -> a
fromShATermError "DFOL.Symbol.Symbol" ShATerm
u