{-# OPTIONS -w -O0 #-}
{- |
Module      :  CASL/ATC_CASL.der.hs
Description :  generated ShATermConvertible 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
  for the type(s):
'CASL.Sublogic.CASL_Formulas'
'CASL.Sublogic.SubsortingFeatures'
'CASL.Sublogic.SortGenerationFeatures'
'CASL.Sublogic.CASL_SL'
'CASL.Morphism.RawSymbol'
'CASL.Morphism.Morphism'
'CASL.Morphism.DefMorExt'
'CASL.Sign.OpType'
'CASL.Sign.PredType'
'CASL.Sign.SymbType'
'CASL.Sign.Symbol'
'CASL.Sign.Sign'
'CASL.AS_Basic_CASL.BASIC_SPEC'
'CASL.AS_Basic_CASL.BASIC_ITEMS'
'CASL.AS_Basic_CASL.SortsKind'
'CASL.AS_Basic_CASL.SIG_ITEMS'
'CASL.AS_Basic_CASL.SORT_ITEM'
'CASL.AS_Basic_CASL.OP_ITEM'
'CASL.AS_Basic_CASL.OpKind'
'CASL.AS_Basic_CASL.OP_TYPE'
'CASL.AS_Basic_CASL.OP_HEAD'
'CASL.AS_Basic_CASL.OP_ATTR'
'CASL.AS_Basic_CASL.PRED_ITEM'
'CASL.AS_Basic_CASL.PRED_TYPE'
'CASL.AS_Basic_CASL.PRED_HEAD'
'CASL.AS_Basic_CASL.DATATYPE_DECL'
'CASL.AS_Basic_CASL.ALTERNATIVE'
'CASL.AS_Basic_CASL.COMPONENTS'
'CASL.AS_Basic_CASL.VAR_DECL'
'CASL.AS_Basic_CASL.Junctor'
'CASL.AS_Basic_CASL.Relation'
'CASL.AS_Basic_CASL.Equality'
'CASL.AS_Basic_CASL.FORMULA'
'CASL.AS_Basic_CASL.Constraint'
'CASL.AS_Basic_CASL.QUANTIFIER'
'CASL.AS_Basic_CASL.PRED_SYMB'
'CASL.AS_Basic_CASL.TERM'
'CASL.AS_Basic_CASL.OP_SYMB'
'CASL.AS_Basic_CASL.SYMB_ITEMS'
'CASL.AS_Basic_CASL.SYMB_MAP_ITEMS'
'CASL.AS_Basic_CASL.SYMB_KIND'
'CASL.AS_Basic_CASL.SYMB'
'CASL.AS_Basic_CASL.TYPE'
'CASL.AS_Basic_CASL.SYMB_OR_MAP'
-}

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

module CASL.ATC_CASL () where

import ATC.GlobalAnnotations
import ATerm.Lib
import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Morphism
import CASL.Sign
import CASL.Sublogic
import CASL.ToDoc ()
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.GlobalAnnotations
import Common.Id
import Common.Keywords
import Common.Lattice
import Common.Prec (mkPrecIntMap, PrecMap)
import Common.Result
import Common.Utils (composeMap)
import Control.Monad
import Control.Monad (when, unless, foldM)
import Data.Data
import Data.Function
import Data.List
import Data.List (isPrefixOf)
import Data.Maybe
import Data.Maybe (fromMaybe)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.State as State
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for CASL.Sublogic.CASL_Formulas derive : ShATermConvertible !-}
{-! for CASL.Sublogic.SubsortingFeatures derive : ShATermConvertible !-}
{-! for CASL.Sublogic.SortGenerationFeatures derive : ShATermConvertible !-}
{-! for CASL.Sublogic.CASL_SL derive : ShATermConvertible !-}
{-! for CASL.Morphism.RawSymbol derive : ShATermConvertible !-}
{-! for CASL.Morphism.Morphism derive : ShATermConvertible !-}
{-! for CASL.Morphism.DefMorExt derive : ShATermConvertible !-}
{-! for CASL.Sign.OpType derive : ShATermConvertible !-}
{-! for CASL.Sign.PredType derive : ShATermConvertible !-}
{-! for CASL.Sign.SymbType derive : ShATermConvertible !-}
{-! for CASL.Sign.Symbol derive : ShATermConvertible !-}
{-! for CASL.Sign.Sign derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.BASIC_SPEC derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.BASIC_ITEMS derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SortsKind derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SIG_ITEMS derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SORT_ITEM derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OP_ITEM derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OpKind derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OP_TYPE derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OP_HEAD derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OP_ATTR derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.PRED_ITEM derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.PRED_TYPE derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.PRED_HEAD derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.DATATYPE_DECL derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.ALTERNATIVE derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.COMPONENTS derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.VAR_DECL derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.Junctor derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.Relation derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.Equality derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.FORMULA derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.Constraint derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.QUANTIFIER derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.PRED_SYMB derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.TERM derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.OP_SYMB derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SYMB_KIND derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SYMB derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.TYPE derive : ShATermConvertible !-}
{-! for CASL.AS_Basic_CASL.SYMB_OR_MAP derive : ShATermConvertible !-}

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

instance ShATermConvertible 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 "SYMB_OR_MAP" ShATerm
u

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

instance ShATermConvertible SYMB where
  toShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB
xv = case SYMB
xv of
    Symb_id a :: SORT
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (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
    Qual_id a :: SORT
a b :: TYPE
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Qual_id" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  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, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      (ATermTable
att1, SORT -> SYMB
Symb_id SORT
a') }
    ShAAppl "Qual_id" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, SORT -> TYPE -> Range -> SYMB
Qual_id SORT
a' TYPE
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB)
forall a. String -> ShATerm -> a
fromShATermError "SYMB" ShATerm
u

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

instance ShATermConvertible 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_KIND
a b :: [SYMB_OR_MAP]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SYMB_KIND -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SYMB_KIND
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SYMB_OR_MAP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SYMB_OR_MAP]
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_items" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  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, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SYMB_KIND)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SYMB_KIND
a') ->
      case Int -> ATermTable -> (ATermTable, [SYMB_OR_MAP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SYMB_OR_MAP]
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_KIND -> [SYMB_OR_MAP] -> Range -> SYMB_MAP_ITEMS
Symb_map_items SYMB_KIND
a' [SYMB_OR_MAP]
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_MAP_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "SYMB_MAP_ITEMS" ShATerm
u

instance ShATermConvertible 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_KIND
a b :: [SYMB]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SYMB_KIND -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SYMB_KIND
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_items" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  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, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SYMB_KIND)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SYMB_KIND
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_KIND -> [SYMB] -> Range -> SYMB_ITEMS
Symb_items SYMB_KIND
a' [SYMB]
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "SYMB_ITEMS" ShATerm
u

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

instance ShATermConvertible f => ShATermConvertible (TERM f) where
  toShATermAux :: ATermTable -> TERM f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TERM f
xv = case TERM f
xv of
    Qual_var a :: VAR
a b :: SORT
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VAR -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VAR
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
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 "Qual_var" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Application a :: OP_SYMB
a b :: [TERM f]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OP_SYMB -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OP_SYMB
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TERM f]
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 "Application" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Sorted_term a :: TERM f
a b :: SORT
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
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 "Sorted_term" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Cast a :: TERM f
a b :: SORT
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
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 "Cast" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Conditional a :: TERM f
a b :: FORMULA f
b c :: TERM f
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FORMULA f
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TERM f
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Conditional" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Unparsed_term a :: String
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Unparsed_term" [Int
a', Int
b'] []) ATermTable
att2
    Mixfix_qual_pred a :: PRED_SYMB
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PRED_SYMB -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PRED_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 "Mixfix_qual_pred" [Int
a'] []) ATermTable
att1
    Mixfix_term a :: [TERM f]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TERM f]
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Mixfix_term" [Int
a'] []) ATermTable
att1
    Mixfix_token a :: VAR
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VAR -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VAR
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 "Mixfix_token" [Int
a'] []) ATermTable
att1
    Mixfix_sorted_term a :: SORT
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Mixfix_sorted_term" [Int
a', Int
b'] []) ATermTable
att2
    Mixfix_cast a :: SORT
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Mixfix_cast" [Int
a', Int
b'] []) ATermTable
att2
    Mixfix_parenthesized a :: [TERM f]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TERM f]
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 "Mixfix_parenthesized" [Int
a', Int
b'] []) ATermTable
att2
    Mixfix_bracketed a :: [TERM f]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TERM f]
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 "Mixfix_bracketed" [Int
a', Int
b'] []) ATermTable
att2
    Mixfix_braced a :: [TERM f]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TERM f]
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 "Mixfix_braced" [Int
a', Int
b'] []) ATermTable
att2
    ExtTERM a :: f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 f
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ExtTERM" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TERM f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Qual_var" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, VAR)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: VAR
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
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, VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
a' SORT
b' Range
c') }}}
    ShAAppl "Application" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, OP_SYMB)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OP_SYMB
a') ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [TERM f]
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, OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
a' [TERM f]
b' Range
c') }}}
    ShAAppl "Sorted_term" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
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, TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
a' SORT
b' Range
c') }}}
    ShAAppl "Cast" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
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, TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast TERM f
a' SORT
b' Range
c') }}}
    ShAAppl "Conditional" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FORMULA f
b') ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: TERM f
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
a' FORMULA f
b' TERM f
c' Range
d') }}}}
    ShAAppl "Unparsed_term" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
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, String -> Range -> TERM f
forall f. String -> Range -> TERM f
Unparsed_term String
a' Range
b') }}
    ShAAppl "Mixfix_qual_pred" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, PRED_SYMB)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PRED_SYMB
a') ->
      (ATermTable
att1, PRED_SYMB -> TERM f
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred PRED_SYMB
a') }
    ShAAppl "Mixfix_term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TERM f]
a') ->
      (ATermTable
att1, [TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term [TERM f]
a') }
    ShAAppl "Mixfix_token" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, VAR)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: VAR
a') ->
      (ATermTable
att1, VAR -> TERM f
forall f. VAR -> TERM f
Mixfix_token VAR
a') }
    ShAAppl "Mixfix_sorted_term" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, SORT -> Range -> TERM f
forall f. SORT -> Range -> TERM f
Mixfix_sorted_term SORT
a' Range
b') }}
    ShAAppl "Mixfix_cast" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, SORT -> Range -> TERM f
forall f. SORT -> Range -> TERM f
Mixfix_cast SORT
a' Range
b') }}
    ShAAppl "Mixfix_parenthesized" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TERM f]
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, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f]
a' Range
b') }}
    ShAAppl "Mixfix_bracketed" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TERM f]
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, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_bracketed [TERM f]
a' Range
b') }}
    ShAAppl "Mixfix_braced" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [TERM f]
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, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_braced [TERM f]
a' Range
b') }}
    ShAAppl "ExtTERM" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: f
a') ->
      (ATermTable
att1, f -> TERM f
forall f. f -> TERM f
ExtTERM f
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TERM f)
forall a. String -> ShATerm -> a
fromShATermError "TERM" ShATerm
u

instance ShATermConvertible PRED_SYMB where
  toShATermAux :: ATermTable -> PRED_SYMB -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PRED_SYMB
xv = case PRED_SYMB
xv of
    Pred_name a :: SORT
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (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_name" [Int
a'] []) ATermTable
att1
    Qual_pred_name a :: SORT
a b :: PRED_TYPE
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PRED_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PRED_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Qual_pred_name" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_SYMB)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Pred_name" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      (ATermTable
att1, SORT -> PRED_SYMB
Pred_name SORT
a') }
    ShAAppl "Qual_pred_name" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, PRED_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: PRED_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
a' PRED_TYPE
b' Range
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PRED_SYMB)
forall a. String -> ShATerm -> a
fromShATermError "PRED_SYMB" ShATerm
u

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

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

instance ShATermConvertible f => ShATermConvertible (FORMULA f) where
  toShATermAux :: ATermTable -> FORMULA f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FORMULA f
xv = case FORMULA f
xv of
    Quantification a :: QUANTIFIER
a b :: [VAR_DECL]
b c :: FORMULA f
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QUANTIFIER -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QUANTIFIER
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [VAR_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [VAR_DECL]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FORMULA f
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Quantification" [Int
a', Int
b', Int
c',
                                                   Int
d'] []) ATermTable
att4
    Junction a :: Junctor
a b :: [FORMULA f]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Junctor -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Junctor
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [FORMULA f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [FORMULA f]
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 "Junction" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Relation a :: FORMULA f
a b :: Relation
b c :: FORMULA f
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FORMULA f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Relation -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Relation
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FORMULA f
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Relation" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Negation a :: FORMULA f
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FORMULA f
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
    Atom a :: Bool
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> 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 "Atom" [Int
a', Int
b'] []) ATermTable
att2
    Predication a :: PRED_SYMB
a b :: [TERM f]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PRED_SYMB -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PRED_SYMB
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [TERM f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TERM f]
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 "Predication" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Definedness a :: TERM f
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
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 "Definedness" [Int
a', Int
b'] []) ATermTable
att2
    Equation a :: TERM f
a b :: Equality
b c :: TERM f
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Equality -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Equality
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TERM f
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Equation" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Membership a :: TERM f
a b :: SORT
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
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 "Membership" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Mixfix_formula a :: TERM f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Mixfix_formula" [Int
a'] []) ATermTable
att1
    Unparsed_formula a :: String
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Unparsed_formula" [Int
a', Int
b'] []) ATermTable
att2
    Sort_gen_ax a :: [Constraint]
a b :: Bool
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Constraint] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Constraint]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
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 "Sort_gen_ax" [Int
a', Int
b'] []) ATermTable
att2
    QuantOp a :: SORT
a b :: OP_TYPE
b c :: FORMULA f
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OP_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OP_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FORMULA f
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 "QuantOp" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    QuantPred a :: SORT
a b :: PRED_TYPE
b c :: FORMULA f
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PRED_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PRED_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FORMULA f
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 "QuantPred" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    ExtFORMULA a :: f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 f
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ExtFORMULA" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Quantification" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QUANTIFIER)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QUANTIFIER
a') ->
      case Int -> ATermTable -> (ATermTable, [VAR_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [VAR_DECL]
b') ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FORMULA f
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
a' [VAR_DECL]
b' FORMULA f
c' Range
d') }}}}
    ShAAppl "Junction" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Junctor)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Junctor
a') ->
      case Int -> ATermTable -> (ATermTable, [FORMULA f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [FORMULA f]
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, Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
a' [FORMULA f]
b' Range
c') }}}
    ShAAppl "Relation" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FORMULA f
a') ->
      case Int -> ATermTable -> (ATermTable, Relation)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Relation
b') ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FORMULA f
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
a' Relation
b' FORMULA f
c' Range
d') }}}}
    ShAAppl "Negation" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FORMULA f
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 f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA f
a' Range
b') }}
    ShAAppl "Atom" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
a' Range
b') }}
    ShAAppl "Predication" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, PRED_SYMB)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PRED_SYMB
a') ->
      case Int -> ATermTable -> (ATermTable, [TERM f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [TERM f]
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, PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
a' [TERM f]
b' Range
c') }}}
    ShAAppl "Definedness" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
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, TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
a' Range
b') }}
    ShAAppl "Equation" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      case Int -> ATermTable -> (ATermTable, Equality)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Equality
b') ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: TERM f
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
a' Equality
b' TERM f
c' Range
d') }}}}
    ShAAppl "Membership" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
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, TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
a' SORT
b' Range
c') }}}
    ShAAppl "Mixfix_formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      (ATermTable
att1, TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula TERM f
a') }
    ShAAppl "Unparsed_formula" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
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, String -> Range -> FORMULA f
forall f. String -> Range -> FORMULA f
Unparsed_formula String
a' Range
b') }}
    ShAAppl "Sort_gen_ax" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Constraint])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Constraint]
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      (ATermTable
att2, [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
Sort_gen_ax [Constraint]
a' Bool
b') }}
    ShAAppl "QuantOp" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, OP_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: OP_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FORMULA f
c') ->
      (ATermTable
att3, SORT -> OP_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp SORT
a' OP_TYPE
b' FORMULA f
c') }}}
    ShAAppl "QuantPred" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, PRED_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: PRED_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, FORMULA f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FORMULA f
c') ->
      (ATermTable
att3, SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred SORT
a' PRED_TYPE
b' FORMULA f
c') }}}
    ShAAppl "ExtFORMULA" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: f
a') ->
      (ATermTable
att1, f -> FORMULA f
forall f. f -> FORMULA f
ExtFORMULA f
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FORMULA f)
forall a. String -> ShATerm -> a
fromShATermError "FORMULA" ShATerm
u

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

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

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

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

instance ShATermConvertible COMPONENTS where
  toShATermAux :: ATermTable -> COMPONENTS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: COMPONENTS
xv = case COMPONENTS
xv of
    Cons_select a :: OpKind
a b :: [SORT]
b c :: SORT
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SORT]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SORT
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Cons_select" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Sort a :: SORT
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (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" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, COMPONENTS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Cons_select" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, OpKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpKind
a') ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SORT]
b') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SORT
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, OpKind -> [SORT] -> SORT -> Range -> COMPONENTS
Cons_select OpKind
a' [SORT]
b' SORT
c' Range
d') }}}}
    ShAAppl "Sort" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      (ATermTable
att1, SORT -> COMPONENTS
Sort SORT
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, COMPONENTS)
forall a. String -> ShATerm -> a
fromShATermError "COMPONENTS" ShATerm
u

instance ShATermConvertible ALTERNATIVE where
  toShATermAux :: ATermTable -> ALTERNATIVE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ALTERNATIVE
xv = case ALTERNATIVE
xv of
    Alt_construct a :: OpKind
a b :: SORT
b c :: [COMPONENTS]
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [COMPONENTS] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [COMPONENTS]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Alt_construct" [Int
a', Int
b', Int
c',
                                                  Int
d'] []) ATermTable
att4
    Subsorts a :: [SORT]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Subsorts" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ALTERNATIVE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Alt_construct" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, OpKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpKind
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
b') ->
      case Int -> ATermTable -> (ATermTable, [COMPONENTS])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [COMPONENTS]
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, OpKind -> SORT -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
a' SORT
b' [COMPONENTS]
c' Range
d') }}}}
    ShAAppl "Subsorts" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [SORT] -> Range -> ALTERNATIVE
Subsorts [SORT]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ALTERNATIVE)
forall a. String -> ShATerm -> a
fromShATermError "ALTERNATIVE" ShATerm
u

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

instance ShATermConvertible PRED_HEAD where
  toShATermAux :: ATermTable -> PRED_HEAD -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PRED_HEAD
xv = case PRED_HEAD
xv of
    Pred_head a :: [VAR_DECL]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [VAR_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [VAR_DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Pred_head" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_HEAD)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Pred_head" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [VAR_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [VAR_DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [VAR_DECL] -> Range -> PRED_HEAD
Pred_head [VAR_DECL]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PRED_HEAD)
forall a. String -> ShATerm -> a
fromShATermError "PRED_HEAD" ShATerm
u

instance ShATermConvertible PRED_TYPE where
  toShATermAux :: ATermTable -> PRED_TYPE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PRED_TYPE
xv = case PRED_TYPE
xv of
    Pred_type a :: [SORT]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Pred_type" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_TYPE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Pred_type" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PRED_TYPE)
forall a. String -> ShATerm -> a
fromShATermError "PRED_TYPE" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (PRED_ITEM f) where
  toShATermAux :: ATermTable -> PRED_ITEM f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PRED_ITEM f
xv = case PRED_ITEM f
xv of
    Pred_decl a :: [SORT]
a b :: PRED_TYPE
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PRED_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PRED_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Pred_decl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Pred_defn a :: SORT
a b :: PRED_HEAD
b c :: Annoted (FORMULA f)
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PRED_HEAD -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PRED_HEAD
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Annoted (FORMULA f) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Annoted (FORMULA f)
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Pred_defn" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_ITEM f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Pred_decl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, PRED_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: PRED_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
forall f. [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
Pred_decl [SORT]
a' PRED_TYPE
b' Range
c') }}}
    ShAAppl "Pred_defn" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, PRED_HEAD)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: PRED_HEAD
b') ->
      case Int -> ATermTable -> (ATermTable, Annoted (FORMULA f))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Annoted (FORMULA f)
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, SORT -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
forall f.
SORT -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
Pred_defn SORT
a' PRED_HEAD
b' Annoted (FORMULA f)
c' Range
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PRED_ITEM f)
forall a. String -> ShATerm -> a
fromShATermError "PRED_ITEM" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (OP_ATTR f) where
  toShATermAux :: ATermTable -> OP_ATTR f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OP_ATTR f
xv = case OP_ATTR f
xv of
    Assoc_op_attr -> (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 "Assoc_op_attr" [] []) ATermTable
att0
    Comm_op_attr -> (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 "Comm_op_attr" [] []) ATermTable
att0
    Idem_op_attr -> (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 "Idem_op_attr" [] []) ATermTable
att0
    Unit_op_attr a :: TERM f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TERM f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TERM f
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Unit_op_attr" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_ATTR f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Assoc_op_attr" [] _ -> (ATermTable
att0, OP_ATTR f
forall f. OP_ATTR f
Assoc_op_attr)
    ShAAppl "Comm_op_attr" [] _ -> (ATermTable
att0, OP_ATTR f
forall f. OP_ATTR f
Comm_op_attr)
    ShAAppl "Idem_op_attr" [] _ -> (ATermTable
att0, OP_ATTR f
forall f. OP_ATTR f
Idem_op_attr)
    ShAAppl "Unit_op_attr" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, TERM f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TERM f
a') ->
      (ATermTable
att1, TERM f -> OP_ATTR f
forall f. TERM f -> OP_ATTR f
Unit_op_attr TERM f
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OP_ATTR f)
forall a. String -> ShATerm -> a
fromShATermError "OP_ATTR" ShATerm
u

instance ShATermConvertible OP_HEAD where
  toShATermAux :: ATermTable -> OP_HEAD -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OP_HEAD
xv = case OP_HEAD
xv of
    Op_head a :: OpKind
a b :: [VAR_DECL]
b c :: Maybe SORT
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [VAR_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [VAR_DECL]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe SORT
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Op_head" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_HEAD)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Op_head" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, OpKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpKind
a') ->
      case Int -> ATermTable -> (ATermTable, [VAR_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [VAR_DECL]
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe SORT
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, OpKind -> [VAR_DECL] -> Maybe SORT -> Range -> OP_HEAD
Op_head OpKind
a' [VAR_DECL]
b' Maybe SORT
c' Range
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OP_HEAD)
forall a. String -> ShATerm -> a
fromShATermError "OP_HEAD" ShATerm
u

instance ShATermConvertible OP_TYPE where
  toShATermAux :: ATermTable -> OP_TYPE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OP_TYPE
xv = case OP_TYPE
xv of
    Op_type a :: OpKind
a b :: [SORT]
b c :: SORT
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SORT]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SORT
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Op_type" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_TYPE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Op_type" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, OpKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpKind
a') ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SORT]
b') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SORT
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
a' [SORT]
b' SORT
c' Range
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OP_TYPE)
forall a. String -> ShATerm -> a
fromShATermError "OP_TYPE" ShATerm
u

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

instance ShATermConvertible f => ShATermConvertible (OP_ITEM f) where
  toShATermAux :: ATermTable -> OP_ITEM f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OP_ITEM f
xv = case OP_ITEM f
xv of
    Op_decl a :: [SORT]
a b :: OP_TYPE
b c :: [OP_ATTR f]
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OP_TYPE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OP_TYPE
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [OP_ATTR f] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [OP_ATTR f]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Op_decl" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Op_defn a :: SORT
a b :: OP_HEAD
b c :: Annoted (TERM f)
c d :: Range
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OP_HEAD -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OP_HEAD
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Annoted (TERM f) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Annoted (TERM f)
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Op_defn" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_ITEM f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Op_decl" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, OP_TYPE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: OP_TYPE
b') ->
      case Int -> ATermTable -> (ATermTable, [OP_ATTR f])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [OP_ATTR f]
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [SORT]
a' OP_TYPE
b' [OP_ATTR f]
c' Range
d') }}}}
    ShAAppl "Op_defn" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, OP_HEAD)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: OP_HEAD
b') ->
      case Int -> ATermTable -> (ATermTable, Annoted (TERM f))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Annoted (TERM f)
c') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Range
d') ->
      (ATermTable
att4, SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
forall f. SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
Op_defn SORT
a' OP_HEAD
b' Annoted (TERM f)
c' Range
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OP_ITEM f)
forall a. String -> ShATerm -> a
fromShATermError "OP_ITEM" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (SORT_ITEM f) where
  toShATermAux :: ATermTable -> SORT_ITEM f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SORT_ITEM f
xv = case SORT_ITEM f
xv of
    Sort_decl a :: [SORT]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sort_decl" [Int
a', Int
b'] []) ATermTable
att2
    Subsort_decl a :: [SORT]
a b :: SORT
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SORT
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 "Subsort_decl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Subsort_defn a :: SORT
a b :: VAR
b c :: SORT
c d :: Annoted (FORMULA f)
d e :: Range
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> VAR -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 VAR
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SORT
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Annoted (FORMULA f) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Annoted (FORMULA f)
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Range
e
      (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 "Subsort_defn" [Int
a', Int
b', Int
c', Int
d',
                                                 Int
e'] []) ATermTable
att5
    Iso_decl a :: [SORT]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SORT] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SORT]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Iso_decl" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SORT_ITEM f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sort_decl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT]
a' Range
b') }}
    ShAAppl "Subsort_decl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SORT
b') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Range
c') ->
      (ATermTable
att3, [SORT] -> SORT -> Range -> SORT_ITEM f
forall f. [SORT] -> SORT -> Range -> SORT_ITEM f
Subsort_decl [SORT]
a' SORT
b' Range
c') }}}
    ShAAppl "Subsort_defn" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SORT
a') ->
      case Int -> ATermTable -> (ATermTable, VAR)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: VAR
b') ->
      case Int -> ATermTable -> (ATermTable, SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SORT
c') ->
      case Int -> ATermTable -> (ATermTable, Annoted (FORMULA f))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Annoted (FORMULA f)
d') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Range
e') ->
      (ATermTable
att5, SORT -> VAR -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
forall f.
SORT -> VAR -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
Subsort_defn SORT
a' VAR
b' SORT
c' Annoted (FORMULA f)
d' Range
e') }}}}}
    ShAAppl "Iso_decl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SORT])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SORT]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Iso_decl [SORT]
a' Range
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SORT_ITEM f)
forall a. String -> ShATerm -> a
fromShATermError "SORT_ITEM" ShATerm
u

instance (ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (SIG_ITEMS s f) where
  toShATermAux :: ATermTable -> SIG_ITEMS s f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SIG_ITEMS s f
xv = case SIG_ITEMS s f
xv of
    Sort_items a :: SortsKind
a b :: [Annoted (SORT_ITEM f)]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SortsKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SortsKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Annoted (SORT_ITEM f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Annoted (SORT_ITEM f)]
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 "Sort_items" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Op_items a :: [Annoted (OP_ITEM f)]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted (OP_ITEM f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (OP_ITEM f)]
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 "Op_items" [Int
a', Int
b'] []) ATermTable
att2
    Pred_items a :: [Annoted (PRED_ITEM f)]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted (PRED_ITEM f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (PRED_ITEM f)]
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_items" [Int
a', Int
b'] []) ATermTable
att2
    Datatype_items a :: SortsKind
a b :: [Annoted DATATYPE_DECL]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SortsKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SortsKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Annoted DATATYPE_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Annoted DATATYPE_DECL]
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 "Datatype_items" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Ext_SIG_ITEMS a :: s
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> s -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 s
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 "Ext_SIG_ITEMS" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SIG_ITEMS s f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sort_items" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SortsKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SortsKind
a') ->
      case Int -> ATermTable -> (ATermTable, [Annoted (SORT_ITEM f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Annoted (SORT_ITEM f)]
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, SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
a' [Annoted (SORT_ITEM f)]
b' Range
c') }}}
    ShAAppl "Op_items" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted (OP_ITEM f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (OP_ITEM f)]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items [Annoted (OP_ITEM f)]
a' Range
b') }}
    ShAAppl "Pred_items" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted (PRED_ITEM f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (PRED_ITEM f)]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items [Annoted (PRED_ITEM f)]
a' Range
b') }}
    ShAAppl "Datatype_items" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SortsKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SortsKind
a') ->
      case Int -> ATermTable -> (ATermTable, [Annoted DATATYPE_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Annoted DATATYPE_DECL]
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, SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
Datatype_items SortsKind
a' [Annoted DATATYPE_DECL]
b' Range
c') }}}
    ShAAppl "Ext_SIG_ITEMS" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, s)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: s
a') ->
      (ATermTable
att1, s -> SIG_ITEMS s f
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS s
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SIG_ITEMS s f)
forall a. String -> ShATerm -> a
fromShATermError "SIG_ITEMS" ShATerm
u

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

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f) where
  toShATermAux :: ATermTable -> BASIC_ITEMS b s f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_ITEMS b s f
xv = case BASIC_ITEMS b s f
xv of
    Sig_items a :: SIG_ITEMS s f
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SIG_ITEMS s f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SIG_ITEMS s f
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sig_items" [Int
a'] []) ATermTable
att1
    Free_datatype a :: SortsKind
a b :: [Annoted DATATYPE_DECL]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SortsKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SortsKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Annoted DATATYPE_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Annoted DATATYPE_DECL]
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 "Free_datatype" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Sort_gen a :: [Annoted (SIG_ITEMS s f)]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted (SIG_ITEMS s f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (SIG_ITEMS s f)]
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 "Sort_gen" [Int
a', Int
b'] []) ATermTable
att2
    Var_items a :: [VAR_DECL]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [VAR_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [VAR_DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Var_items" [Int
a', Int
b'] []) ATermTable
att2
    Local_var_axioms a :: [VAR_DECL]
a b :: [Annoted (FORMULA f)]
b c :: Range
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [VAR_DECL] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [VAR_DECL]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Annoted (FORMULA f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Annoted (FORMULA f)]
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 "Local_var_axioms" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Axiom_items a :: [Annoted (FORMULA f)]
a b :: Range
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted (FORMULA f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (FORMULA f)]
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 "Axiom_items" [Int
a', Int
b'] []) ATermTable
att2
    Ext_BASIC_ITEMS a :: b
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> b -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 b
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 "Ext_BASIC_ITEMS" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS b s f)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sig_items" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SIG_ITEMS s f)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SIG_ITEMS s f
a') ->
      (ATermTable
att1, SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items SIG_ITEMS s f
a') }
    ShAAppl "Free_datatype" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SortsKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SortsKind
a') ->
      case Int -> ATermTable -> (ATermTable, [Annoted DATATYPE_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Annoted DATATYPE_DECL]
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, SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
Free_datatype SortsKind
a' [Annoted DATATYPE_DECL]
b' Range
c') }}}
    ShAAppl "Sort_gen" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted (SIG_ITEMS s f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (SIG_ITEMS s f)]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen [Annoted (SIG_ITEMS s f)]
a' Range
b') }}
    ShAAppl "Var_items" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [VAR_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [VAR_DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [VAR_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f. [VAR_DECL] -> Range -> BASIC_ITEMS b s f
Var_items [VAR_DECL]
a' Range
b') }}
    ShAAppl "Local_var_axioms" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [VAR_DECL])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [VAR_DECL]
a') ->
      case Int -> ATermTable -> (ATermTable, [Annoted (FORMULA f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Annoted (FORMULA f)]
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, [VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Local_var_axioms [VAR_DECL]
a' [Annoted (FORMULA f)]
b' Range
c') }}}
    ShAAppl "Axiom_items" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted (FORMULA f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (FORMULA f)]
a') ->
      case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      (ATermTable
att2, [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted (FORMULA f)]
a' Range
b') }}
    ShAAppl "Ext_BASIC_ITEMS" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, b)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: b
a') ->
      (ATermTable
att1, b -> BASIC_ITEMS b s f
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS b
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_ITEMS b s f)
forall a. String -> ShATerm -> a
fromShATermError "BASIC_ITEMS" ShATerm
u

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (BASIC_SPEC b s f) where
  toShATermAux :: ATermTable -> BASIC_SPEC b s f -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_SPEC b s f
xv = case BASIC_SPEC b s f
xv of
    Basic_spec a :: [Annoted (BASIC_ITEMS b s f)]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted (BASIC_ITEMS b s f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted (BASIC_ITEMS b s f)]
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Basic_spec" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC b s f)
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 b s f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted (BASIC_ITEMS b s f)]
a') ->
      (ATermTable
att1, [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec [Annoted (BASIC_ITEMS b s f)]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC b s f)
forall a. String -> ShATerm -> a
fromShATermError "BASIC_SPEC" ShATerm
u

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

instance (ShATermConvertible f, ShATermConvertible e,
          ShATermConvertible m) => ShATermConvertible (Morphism f e m) where
  toShATermAux :: ATermTable -> Morphism f e m -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Morphism f e m
xv = case Morphism f e m
xv of
    Morphism a :: Sign f e
a b :: Sign f e
b c :: Sort_map
c d :: Op_map
d e :: Pred_map
e f :: m
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sign f e -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sign f e
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sign f e -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sign f e
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Sort_map -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Sort_map
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Op_map -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Op_map
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Pred_map -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Pred_map
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> m -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 m
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 "Morphism" [Int
a', Int
b', Int
c', Int
d', Int
e',
                                             Int
f'] []) ATermTable
att6
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism f e m)
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, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case Int -> ATermTable -> (ATermTable, Sign f e)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Sign f e
a') ->
      case Int -> ATermTable -> (ATermTable, Sign f e)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of