{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  CASL/ATC_CASL.der.hs
Description :  generated ShATermConvertible, Json instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(derive Typeable instances)

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json
  for the type(s):
'CASL.Sublogic.CASL_Formulas'
'CASL.Sublogic.SubsortingFeatures'
'CASL.Sublogic.SortGenTotality'
'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.Json.Instances
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)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.Function
import Data.List
import Data.List (isPrefixOf)
import Data.Maybe
import Data.Maybe (fromMaybe)
import GHC.Generics(Generic)
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.SortGenTotality 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 !-}

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

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

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SYMB_OR_MAP
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SYMB_OR_MAP where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SYMB_OR_MAP where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.TYPE
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.TYPE where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.TYPE where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SYMB
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SYMB where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SYMB where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SYMB_KIND
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SYMB_KIND where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SYMB_KIND where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SYMB_MAP_ITEMS
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SYMB_MAP_ITEMS where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SYMB_MAP_ITEMS where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SYMB_ITEMS
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SYMB_ITEMS where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SYMB_ITEMS where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.OP_SYMB
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.OP_SYMB where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.OP_SYMB where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.TERM f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.TERM f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.TERM f) where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.PRED_SYMB
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.PRED_SYMB where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.PRED_SYMB where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.QUANTIFIER
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.QUANTIFIER where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.QUANTIFIER where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.Constraint
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.Constraint where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.Constraint where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.FORMULA f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.FORMULA f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.FORMULA f) where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.Equality
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.Equality where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.Equality where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.Relation
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.Relation where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.Relation where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.Junctor
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.Junctor where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.Junctor where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.VAR_DECL
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.VAR_DECL where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.VAR_DECL where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.COMPONENTS
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.COMPONENTS where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.COMPONENTS where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.ALTERNATIVE
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.ALTERNATIVE where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.ALTERNATIVE where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.DATATYPE_DECL
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.DATATYPE_DECL where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.DATATYPE_DECL where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.PRED_HEAD
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.PRED_HEAD where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.PRED_HEAD where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.PRED_TYPE
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.PRED_TYPE where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.PRED_TYPE where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.PRED_ITEM f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.PRED_ITEM f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.PRED_ITEM f) where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.OP_ATTR f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.OP_ATTR f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.OP_ATTR f) where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.OP_HEAD
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.OP_HEAD where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.OP_HEAD where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.OP_TYPE
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.OP_TYPE where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.OP_TYPE where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.OpKind
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.OpKind where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.OpKind where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.OP_ITEM f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.OP_ITEM f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.OP_ITEM f) where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.SORT_ITEM f)
instance Data.Aeson.ToJSON f => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.SORT_ITEM f) where
instance Data.Aeson.FromJSON f => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.SORT_ITEM f) where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.SIG_ITEMS s f)
instance (Data.Aeson.ToJSON s,
          Data.Aeson.ToJSON f) => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.SIG_ITEMS s f) where
instance (Data.Aeson.FromJSON s,
          Data.Aeson.FromJSON f) => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.SIG_ITEMS s f) where

deriving instance GHC.Generics.Generic CASL.AS_Basic_CASL.SortsKind
instance Data.Aeson.ToJSON CASL.AS_Basic_CASL.SortsKind where
instance Data.Aeson.FromJSON CASL.AS_Basic_CASL.SortsKind where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.BASIC_ITEMS b s f)
instance (Data.Aeson.ToJSON b, Data.Aeson.ToJSON s,
          Data.Aeson.ToJSON f) => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.BASIC_ITEMS b s f) where
instance (Data.Aeson.FromJSON b, Data.Aeson.FromJSON s,
          Data.Aeson.FromJSON f) => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.BASIC_ITEMS b s f) where

deriving instance GHC.Generics.Generic (CASL.AS_Basic_CASL.BASIC_SPEC b s f)
instance (Data.Aeson.ToJSON b, Data.Aeson.ToJSON s,
          Data.Aeson.ToJSON f) => Data.Aeson.ToJSON (CASL.AS_Basic_CASL.BASIC_SPEC b s f) where
instance (Data.Aeson.FromJSON b, Data.Aeson.FromJSON s,
          Data.Aeson.FromJSON f) => Data.Aeson.FromJSON (CASL.AS_Basic_CASL.BASIC_SPEC b s f) where

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

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.TYPE" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SYMB" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SYMB_KIND" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SYMB_MAP_ITEMS" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SYMB_ITEMS" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OP_SYMB" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.TERM" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.PRED_SYMB" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.QUANTIFIER" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.Constraint" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.FORMULA" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.Equality" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.Relation" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.Junctor" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.VAR_DECL" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.COMPONENTS" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.ALTERNATIVE" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.DATATYPE_DECL" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.PRED_HEAD" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.PRED_TYPE" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.PRED_ITEM" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OP_ATTR" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OP_HEAD" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OP_TYPE" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OpKind" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.OP_ITEM" ShATerm
u

instance ShATermConvertible f => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SORT_ITEM" ShATerm
u

instance (ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SIG_ITEMS" ShATerm
u

instance ShATermConvertible CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.SortsKind" ShATerm
u

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.BASIC_ITEMS" ShATerm
u

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (CASL.AS_Basic_CASL.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 "CASL.AS_Basic_CASL.BASIC_SPEC" ShATerm
u

deriving instance GHC.Generics.Generic (CASL.Morphism.DefMorExt e)
instance Data.Aeson.ToJSON e => Data.Aeson.ToJSON (CASL.Morphism.DefMorExt e) where
instance Data.Aeson.FromJSON e => Data.Aeson.FromJSON (CASL.Morphism.DefMorExt e) where

deriving instance GHC.Generics.Generic (CASL.Morphism.Morphism f e m)
instance (Data.Aeson.ToJSON f, Data.Aeson.ToJSON e,
          Data.Aeson.ToJSON m) => Data.Aeson.ToJSON (CASL.Morphism.Morphism f e m) where
instance (Data.Aeson.FromJSON f, Data.Aeson.FromJSON e,
          Data.Aeson.FromJSON m) => Data.Aeson.FromJSON (CASL.Morphism.Morphism f e m) where

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

instance ShATermConvertible e => ShATermConvertible (CASL.Morphism.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 "CASL.Morphism.DefMorExt" ShATerm
u

instance (ShATermConvertible f, ShATermConvertible e,
          ShATermConvertible m) => ShATermConvertible (CASL.Morphism.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
      { (att2 :: ATermTable
att2, b' :: Sign f e
b') ->
      case Int -> ATermTable -> (ATermTable, Sort_map)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Sort_map
c') ->
      case Int -> ATermTable -> (ATermTable, Op_map)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Op_map
d') ->
      case Int -> ATermTable -> (ATermTable, Pred_map)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Pred_map
e') ->
      case Int -> ATermTable -> (ATermTable, m)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: m
f') ->
      (ATermTable
att6, Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
forall f e m.
Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
Morphism Sign f e
a' Sign f e
b' Sort_map
c' Op_map
d' Pred_map
e' m
f') }}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism f e m)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Morphism.Morphism" ShATerm
u

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

instance ShATermConvertible CASL.Sign.OpType where
  toShATermAux :: ATermTable -> OpType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OpType
xv = case OpType
xv of
    OpType a :: OpKind
a b :: [SORT]
b c :: SORT
c -> 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
      (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 "OpType" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, OpType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "OpType" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      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') ->
      (ATermTable
att3, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
a' [SORT]
b' SORT
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OpType)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Sign.OpType" ShATerm
u

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

instance ShATermConvertible CASL.Sign.SymbType where
  toShATermAux :: ATermTable -> SymbType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbType
xv = case SymbType
xv of
    SortAsItemType -> (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 "SortAsItemType" [] []) ATermTable
att0
    SubsortAsItemType 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 "SubsortAsItemType" [Int
a'] []) ATermTable
att1
    OpAsItemType a :: OpType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpType
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 "OpAsItemType" [Int
a'] []) ATermTable
att1
    PredAsItemType a :: PredType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PredType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PredType
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 "PredAsItemType" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SortAsItemType" [] _ -> (ATermTable
att0, SymbType
SortAsItemType)
    ShAAppl "SubsortAsItemType" [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 -> SymbType
SubsortAsItemType SORT
a') }
    ShAAppl "OpAsItemType" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, OpType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: OpType
a') ->
      (ATermTable
att1, OpType -> SymbType
OpAsItemType OpType
a') }
    ShAAppl "PredAsItemType" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, PredType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PredType
a') ->
      (ATermTable
att1, PredType -> SymbType
PredAsItemType PredType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbType)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Sign.SymbType" ShATerm
u

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

instance (ShATermConvertible f,
          ShATermConvertible e) => ShATermConvertible (CASL.Sign.Sign f e) where
  toShATermAux :: ATermTable -> Sign f e -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign f e
xv = case Sign f e
xv of
    Sign a :: Rel SORT
a b :: Maybe (Rel SORT)
b c :: Set SORT
c d :: OpMap
d e :: OpMap
e f :: PredMap
f g :: Map VAR SORT
g h :: [Named (FORMULA f)]
h i :: Set Symbol
i j :: [Diagnosis]
j k :: AnnoMap
k l :: GlobalAnnos
l m :: e
m -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Rel SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Rel SORT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe (Rel SORT) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe (Rel SORT)
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Set SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Set SORT
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> OpMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 OpMap
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> OpMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 OpMap
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> PredMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 PredMap
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Map VAR SORT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Map VAR SORT
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> [Named (FORMULA f)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att7 [Named (FORMULA f)]
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Set Symbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att8 Set Symbol
i
      (att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> [Diagnosis] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att9 [Diagnosis]
j
      (att11 :: ATermTable
att11, k' :: Int
k') <- ATermTable -> AnnoMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att10 AnnoMap
k
      (att12 :: ATermTable
att12, l' :: Int
l') <- ATermTable -> GlobalAnnos -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att11 GlobalAnnos
l
      (att13 :: ATermTable
att13, m' :: Int
m') <- ATermTable -> e -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att12 e
m
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sign" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g', Int
h',
                                         Int
i', Int
j', Int
k', Int
l', Int
m'] []) ATermTable
att13
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign f e)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sign" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h, i :: Int
i, j :: Int
j, k :: Int
k, l :: Int
l, m :: Int
m] _ ->
      case Int -> ATermTable -> (ATermTable, Rel SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Rel SORT
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe (Rel SORT))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe (Rel SORT)
b') ->
      case Int -> ATermTable -> (ATermTable, Set SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Set SORT
c') ->
      case Int -> ATermTable -> (ATermTable, OpMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: OpMap
d') ->
      case Int -> ATermTable -> (ATermTable, OpMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: OpMap
e') ->
      case Int -> ATermTable -> (ATermTable, PredMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: PredMap
f') ->
      case Int -> ATermTable -> (ATermTable, Map VAR SORT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Map VAR SORT
g') ->
      case Int -> ATermTable -> (ATermTable, [Named (FORMULA f)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: [Named (FORMULA f)]
h') ->
      case Int -> ATermTable -> (ATermTable, Set Symbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: Set Symbol
i') ->
      case Int -> ATermTable -> (ATermTable, [Diagnosis])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
j ATermTable
att9 of
      { (att10 :: ATermTable
att10, j' :: [Diagnosis]
j') ->
      case Int -> ATermTable -> (ATermTable, AnnoMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
k ATermTable
att10 of
      { (att11 :: ATermTable
att11, k' :: AnnoMap
k') ->
      case Int -> ATermTable -> (ATermTable, GlobalAnnos)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
l ATermTable
att11 of
      { (att12 :: ATermTable
att12, l' :: GlobalAnnos
l') ->
      case Int -> ATermTable -> (ATermTable, e)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
m ATermTable
att12 of
      { (att13 :: ATermTable
att13, m' :: e
m') ->
      (ATermTable
att13, Rel SORT
-> Maybe (Rel SORT)
-> Set SORT
-> OpMap
-> OpMap
-> PredMap
-> Map VAR SORT
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
forall f e.
Rel SORT
-> Maybe (Rel SORT)
-> Set SORT
-> OpMap
-> OpMap
-> PredMap
-> Map VAR SORT
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
Sign Rel SORT
a' Maybe (Rel SORT)
b' Set SORT
c' OpMap
d' OpMap
e' PredMap
f' Map VAR SORT
g' [Named (FORMULA f)]
h' Set Symbol
i' [Diagnosis]
j' AnnoMap
k' GlobalAnnos
l' e
m') }}}}}}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign f e)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Sign.Sign" ShATerm
u

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

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

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

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

deriving instance GHC.Generics.Generic (CASL.Sign.Sign f e)
instance (Data.Aeson.ToJSON f,
          Data.Aeson.ToJSON e) => Data.Aeson.ToJSON (CASL.Sign.Sign f e) where
instance (Data.Aeson.FromJSON f,
          Data.Aeson.FromJSON e) => Data.Aeson.FromJSON (CASL.Sign.Sign f e) where

deriving instance GHC.Generics.Generic (CASL.Sublogic.CASL_SL a)
instance Data.Aeson.ToJSON a => Data.Aeson.ToJSON (CASL.Sublogic.CASL_SL a) where
instance Data.Aeson.FromJSON a => Data.Aeson.FromJSON (CASL.Sublogic.CASL_SL a) where

deriving instance GHC.Generics.Generic CASL.Sublogic.SortGenerationFeatures
instance Data.Aeson.ToJSON CASL.Sublogic.SortGenerationFeatures where
instance Data.Aeson.FromJSON CASL.Sublogic.SortGenerationFeatures where

deriving instance GHC.Generics.Generic CASL.Sublogic.SortGenTotality
instance Data.Aeson.ToJSON CASL.Sublogic.SortGenTotality where
instance Data.Aeson.FromJSON CASL.Sublogic.SortGenTotality where

deriving instance GHC.Generics.Generic CASL.Sublogic.SubsortingFeatures
instance Data.Aeson.ToJSON CASL.Sublogic.SubsortingFeatures where
instance Data.Aeson.FromJSON CASL.Sublogic.SubsortingFeatures where

deriving instance GHC.Generics.Generic CASL.Sublogic.CASL_Formulas
instance Data.Aeson.ToJSON CASL.Sublogic.CASL_Formulas where
instance Data.Aeson.FromJSON CASL.Sublogic.CASL_Formulas where

instance ShATermConvertible a => ShATermConvertible (CASL.Sublogic.CASL_SL a) where
  toShATermAux :: ATermTable -> CASL_SL a -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CASL_SL a
xv = case CASL_SL a
xv of
    CASL_SL a :: SubsortingFeatures
a b :: Bool
b c :: SortGenerationFeatures
c d :: Bool
d e :: Bool
e f :: CASL_Formulas
f g :: Bool
g h :: a
h -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SubsortingFeatures -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SubsortingFeatures
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
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SortGenerationFeatures -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SortGenerationFeatures
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Bool
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Bool
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> CASL_Formulas -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 CASL_Formulas
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Bool
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att7 a
h
      (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 "CASL_SL" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g',
                                            Int
h'] []) ATermTable
att8
  fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_SL a)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "CASL_SL" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h] _ ->
      case Int -> ATermTable -> (ATermTable, SubsortingFeatures)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SubsortingFeatures
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') ->
      case Int -> ATermTable -> (ATermTable, SortGenerationFeatures)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SortGenerationFeatures
c') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Bool
e') ->
      case Int -> ATermTable -> (ATermTable, CASL_Formulas)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: CASL_Formulas
f') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Bool
g') ->
      case Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: a
h') ->
      (ATermTable
att8, SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
forall a.
SubsortingFeatures
-> Bool
-> SortGenerationFeatures
-> Bool
-> Bool
-> CASL_Formulas
-> Bool
-> a
-> CASL_SL a
CASL_SL SubsortingFeatures
a' Bool
b' SortGenerationFeatures
c' Bool
d' Bool
e' CASL_Formulas
f' Bool
g' a
h') }}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CASL_SL a)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Sublogic.CASL_SL" ShATerm
u

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

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

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

instance ShATermConvertible CASL.Sublogic.CASL_Formulas where
  toShATermAux :: ATermTable -> CASL_Formulas -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CASL_Formulas
xv = case CASL_Formulas
xv of
    Atomic -> (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 "Atomic" [] []) ATermTable
att0
    Horn -> (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 "Horn" [] []) ATermTable
att0
    GHorn -> (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 "GHorn" [] []) ATermTable
att0
    Prenex -> (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 "Prenex" [] []) ATermTable
att0
    FOL -> (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 "FOL" [] []) ATermTable
att0
    SOL -> (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 "SOL" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_Formulas)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Atomic" [] _ -> (ATermTable
att0, CASL_Formulas
Atomic)
    ShAAppl "Horn" [] _ -> (ATermTable
att0, CASL_Formulas
Horn)
    ShAAppl "GHorn" [] _ -> (ATermTable
att0, CASL_Formulas
GHorn)
    ShAAppl "Prenex" [] _ -> (ATermTable
att0, CASL_Formulas
Prenex)
    ShAAppl "FOL" [] _ -> (ATermTable
att0, CASL_Formulas
FOL)
    ShAAppl "SOL" [] _ -> (ATermTable
att0, CASL_Formulas
SOL)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CASL_Formulas)
forall a. String -> ShATerm -> a
fromShATermError "CASL.Sublogic.CASL_Formulas" ShATerm
u