{-# OPTIONS -w -O0 #-}
{- |
Module      :  CASL/ATC_CASL.der.hs
Description :  generated Typeable, ShATermConvertible instances
Copyright   :  (c) DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

Automatic derivation of instances via DrIFT-rule Typeable, ShATermConvertible
  for the type(s):
'CASL.Sublogic.CASL_Formulas'
'CASL.Sublogic.SubsortingFeatures'
'CASL.Sublogic.SortGenerationFeatures'
'CASL.Sublogic.CASL_SL'
'CASL.Morphism.RawSymbol'
'CASL.Morphism.Morphism'
'CASL.Morphism.DefMorExt'
'CASL.Sign.OpType'
'CASL.Sign.PredType'
'CASL.Sign.SymbType'
'CASL.Sign.Symbol'
'CASL.Sign.Sign'
'CASL.AS_Basic_CASL.BASIC_SPEC'
'CASL.AS_Basic_CASL.BASIC_ITEMS'
'CASL.AS_Basic_CASL.SortsKind'
'CASL.AS_Basic_CASL.SIG_ITEMS'
'CASL.AS_Basic_CASL.SORT_ITEM'
'CASL.AS_Basic_CASL.OP_ITEM'
'CASL.AS_Basic_CASL.OpKind'
'CASL.AS_Basic_CASL.OP_TYPE'
'CASL.AS_Basic_CASL.OP_HEAD'
'CASL.AS_Basic_CASL.OP_ATTR'
'CASL.AS_Basic_CASL.PRED_ITEM'
'CASL.AS_Basic_CASL.PRED_TYPE'
'CASL.AS_Basic_CASL.PRED_HEAD'
'CASL.AS_Basic_CASL.DATATYPE_DECL'
'CASL.AS_Basic_CASL.ALTERNATIVE'
'CASL.AS_Basic_CASL.COMPONENTS'
'CASL.AS_Basic_CASL.VAR_DECL'
'CASL.AS_Basic_CASL.FORMULA'
'CASL.AS_Basic_CASL.Constraint'
'CASL.AS_Basic_CASL.QUANTIFIER'
'CASL.AS_Basic_CASL.PRED_SYMB'
'CASL.AS_Basic_CASL.TERM'
'CASL.AS_Basic_CASL.OP_SYMB'
'CASL.AS_Basic_CASL.SYMB_ITEMS'
'CASL.AS_Basic_CASL.SYMB_MAP_ITEMS'
'CASL.AS_Basic_CASL.SYMB_KIND'
'CASL.AS_Basic_CASL.SYMB'
'CASL.AS_Basic_CASL.TYPE'
'CASL.AS_Basic_CASL.SYMB_OR_MAP'
-}

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

module CASL.ATC_CASL () where

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

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

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

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

instance ShATermConvertible SYMB_OR_MAP where
  toShATermAux att0 xv = case xv of
    Symb a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Symb" [a'] []) att1
    Symb_map a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Symb_map" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Symb" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Symb a') }
    ShAAppl "Symb_map" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Symb_map a' b' c') }}}
    u -> fromShATermError "SYMB_OR_MAP" u

instance ShATermConvertible TYPE where
  toShATermAux att0 xv = case xv of
    O_type a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "O_type" [a'] []) att1
    P_type a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "P_type" [a'] []) att1
    A_type a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "A_type" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "O_type" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, O_type a') }
    ShAAppl "P_type" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, P_type a') }
    ShAAppl "A_type" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, A_type a') }
    u -> fromShATermError "TYPE" u

instance ShATermConvertible SYMB where
  toShATermAux att0 xv = case xv of
    Symb_id a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Symb_id" [a'] []) att1
    Qual_id a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Qual_id" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Symb_id" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Symb_id a') }
    ShAAppl "Qual_id" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Qual_id a' b' c') }}}
    u -> fromShATermError "SYMB" u

instance ShATermConvertible SYMB_KIND where
  toShATermAux att0 xv = case xv of
    Implicit -> return $ addATerm (ShAAppl "Implicit" [] []) att0
    Sorts_kind -> return $ addATerm (ShAAppl "Sorts_kind" [] []) att0
    Ops_kind -> return $ addATerm (ShAAppl "Ops_kind" [] []) att0
    Preds_kind -> return $ addATerm (ShAAppl "Preds_kind" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Implicit" [] _ -> (att0, Implicit)
    ShAAppl "Sorts_kind" [] _ -> (att0, Sorts_kind)
    ShAAppl "Ops_kind" [] _ -> (att0, Ops_kind)
    ShAAppl "Preds_kind" [] _ -> (att0, Preds_kind)
    u -> fromShATermError "SYMB_KIND" u

instance ShATermConvertible SYMB_MAP_ITEMS where
  toShATermAux att0 xv = case xv of
    Symb_map_items a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Symb_map_items" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Symb_map_items" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Symb_map_items a' b' c') }}}
    u -> fromShATermError "SYMB_MAP_ITEMS" u

instance ShATermConvertible SYMB_ITEMS where
  toShATermAux att0 xv = case xv of
    Symb_items a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Symb_items" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Symb_items" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Symb_items a' b' c') }}}
    u -> fromShATermError "SYMB_ITEMS" u

instance ShATermConvertible OP_SYMB where
  toShATermAux att0 xv = case xv of
    Op_name a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Op_name" [a'] []) att1
    Qual_op_name a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Qual_op_name" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Op_name" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Op_name a') }
    ShAAppl "Qual_op_name" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Qual_op_name a' b' c') }}}
    u -> fromShATermError "OP_SYMB" u

instance ShATermConvertible f => ShATermConvertible (TERM f) where
  toShATermAux att0 xv = case xv of
    Qual_var a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Qual_var" [a', b', c'] []) att3
    Application a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Application" [a', b', c'] []) att3
    Sorted_term a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Sorted_term" [a', b', c'] []) att3
    Cast a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Cast" [a', b', c'] []) att3
    Conditional a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Conditional" [a', b', c', d'] []) att4
    Unparsed_term a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Unparsed_term" [a', b'] []) att2
    Mixfix_qual_pred a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Mixfix_qual_pred" [a'] []) att1
    Mixfix_term a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Mixfix_term" [a'] []) att1
    Mixfix_token a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Mixfix_token" [a'] []) att1
    Mixfix_sorted_term a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Mixfix_sorted_term" [a', b'] []) att2
    Mixfix_cast a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Mixfix_cast" [a', b'] []) att2
    Mixfix_parenthesized a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Mixfix_parenthesized" [a', b'] []) att2
    Mixfix_bracketed a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Mixfix_bracketed" [a', b'] []) att2
    Mixfix_braced a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Mixfix_braced" [a', b'] []) att2
    ExtTERM a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "ExtTERM" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Qual_var" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Qual_var a' b' c') }}}
    ShAAppl "Application" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Application a' b' c') }}}
    ShAAppl "Sorted_term" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Sorted_term a' b' c') }}}
    ShAAppl "Cast" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Cast a' b' c') }}}
    ShAAppl "Conditional" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Conditional a' b' c' d') }}}}
    ShAAppl "Unparsed_term" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Unparsed_term a' b') }}
    ShAAppl "Mixfix_qual_pred" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Mixfix_qual_pred a') }
    ShAAppl "Mixfix_term" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Mixfix_term a') }
    ShAAppl "Mixfix_token" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Mixfix_token a') }
    ShAAppl "Mixfix_sorted_term" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Mixfix_sorted_term a' b') }}
    ShAAppl "Mixfix_cast" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Mixfix_cast a' b') }}
    ShAAppl "Mixfix_parenthesized" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Mixfix_parenthesized a' b') }}
    ShAAppl "Mixfix_bracketed" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Mixfix_bracketed a' b') }}
    ShAAppl "Mixfix_braced" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Mixfix_braced a' b') }}
    ShAAppl "ExtTERM" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, ExtTERM a') }
    u -> fromShATermError "TERM" u

instance ShATermConvertible PRED_SYMB where
  toShATermAux att0 xv = case xv of
    Pred_name a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Pred_name" [a'] []) att1
    Qual_pred_name a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Qual_pred_name" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Pred_name" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Pred_name a') }
    ShAAppl "Qual_pred_name" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Qual_pred_name a' b' c') }}}
    u -> fromShATermError "PRED_SYMB" u

instance ShATermConvertible QUANTIFIER where
  toShATermAux att0 xv = case xv of
    Universal -> return $ addATerm (ShAAppl "Universal" [] []) att0
    Existential -> return $ addATerm (ShAAppl "Existential" [] []) att0
    Unique_existential ->
      return $ addATerm (ShAAppl "Unique_existential" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Universal" [] _ -> (att0, Universal)
    ShAAppl "Existential" [] _ -> (att0, Existential)
    ShAAppl "Unique_existential" [] _ -> (att0, Unique_existential)
    u -> fromShATermError "QUANTIFIER" u

instance ShATermConvertible Constraint where
  toShATermAux att0 xv = case xv of
    Constraint a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Constraint" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Constraint" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Constraint a' b' c') }}}
    u -> fromShATermError "Constraint" u

instance ShATermConvertible f => ShATermConvertible (FORMULA f) where
  toShATermAux att0 xv = case xv of
    Quantification a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Quantification" [a', b', c',
                                                   d'] []) att4
    Conjunction a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Conjunction" [a', b'] []) att2
    Disjunction a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Disjunction" [a', b'] []) att2
    Implication a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Implication" [a', b', c', d'] []) att4
    Equivalence a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Equivalence" [a', b', c'] []) att3
    Negation a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Negation" [a', b'] []) att2
    True_atom a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "True_atom" [a'] []) att1
    False_atom a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "False_atom" [a'] []) att1
    Predication a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Predication" [a', b', c'] []) att3
    Definedness a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Definedness" [a', b'] []) att2
    Existl_equation a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Existl_equation" [a', b', c'] []) att3
    Strong_equation a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Strong_equation" [a', b', c'] []) att3
    Membership a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Membership" [a', b', c'] []) att3
    Mixfix_formula a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Mixfix_formula" [a'] []) att1
    Unparsed_formula a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Unparsed_formula" [a', b'] []) att2
    Sort_gen_ax a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Sort_gen_ax" [a', b'] []) att2
    QuantOp a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "QuantOp" [a', b', c'] []) att3
    QuantPred a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "QuantPred" [a', b', c'] []) att3
    ExtFORMULA a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "ExtFORMULA" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Quantification" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Quantification a' b' c' d') }}}}
    ShAAppl "Conjunction" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Conjunction a' b') }}
    ShAAppl "Disjunction" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Disjunction a' b') }}
    ShAAppl "Implication" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Implication a' b' c' d') }}}}
    ShAAppl "Equivalence" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Equivalence a' b' c') }}}
    ShAAppl "Negation" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Negation a' b') }}
    ShAAppl "True_atom" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, True_atom a') }
    ShAAppl "False_atom" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, False_atom a') }
    ShAAppl "Predication" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Predication a' b' c') }}}
    ShAAppl "Definedness" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Definedness a' b') }}
    ShAAppl "Existl_equation" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Existl_equation a' b' c') }}}
    ShAAppl "Strong_equation" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Strong_equation a' b' c') }}}
    ShAAppl "Membership" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Membership a' b' c') }}}
    ShAAppl "Mixfix_formula" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Mixfix_formula a') }
    ShAAppl "Unparsed_formula" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Unparsed_formula a' b') }}
    ShAAppl "Sort_gen_ax" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Sort_gen_ax a' b') }}
    ShAAppl "QuantOp" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, QuantOp a' b' c') }}}
    ShAAppl "QuantPred" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, QuantPred a' b' c') }}}
    ShAAppl "ExtFORMULA" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, ExtFORMULA a') }
    u -> fromShATermError "FORMULA" u

instance ShATermConvertible VAR_DECL where
  toShATermAux att0 xv = case xv of
    Var_decl a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Var_decl" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Var_decl" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Var_decl a' b' c') }}}
    u -> fromShATermError "VAR_DECL" u

instance ShATermConvertible COMPONENTS where
  toShATermAux att0 xv = case xv of
    Cons_select a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Cons_select" [a', b', c', d'] []) att4
    Sort a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Sort" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Cons_select" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Cons_select a' b' c' d') }}}}
    ShAAppl "Sort" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Sort a') }
    u -> fromShATermError "COMPONENTS" u

instance ShATermConvertible ALTERNATIVE where
  toShATermAux att0 xv = case xv of
    Alt_construct a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Alt_construct" [a', b', c',
                                                  d'] []) att4
    Subsorts a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Subsorts" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Alt_construct" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Alt_construct a' b' c' d') }}}}
    ShAAppl "Subsorts" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Subsorts a' b') }}
    u -> fromShATermError "ALTERNATIVE" u

instance ShATermConvertible DATATYPE_DECL where
  toShATermAux att0 xv = case xv of
    Datatype_decl a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Datatype_decl" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Datatype_decl" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Datatype_decl a' b' c') }}}
    u -> fromShATermError "DATATYPE_DECL" u

instance ShATermConvertible PRED_HEAD where
  toShATermAux att0 xv = case xv of
    Pred_head a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Pred_head" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Pred_head" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Pred_head a' b') }}
    u -> fromShATermError "PRED_HEAD" u

instance ShATermConvertible PRED_TYPE where
  toShATermAux att0 xv = case xv of
    Pred_type a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Pred_type" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Pred_type" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Pred_type a' b') }}
    u -> fromShATermError "PRED_TYPE" u

instance ShATermConvertible f => ShATermConvertible (PRED_ITEM f) where
  toShATermAux att0 xv = case xv of
    Pred_decl a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Pred_decl" [a', b', c'] []) att3
    Pred_defn a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Pred_defn" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Pred_decl" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Pred_decl a' b' c') }}}
    ShAAppl "Pred_defn" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Pred_defn a' b' c' d') }}}}
    u -> fromShATermError "PRED_ITEM" u

instance ShATermConvertible f => ShATermConvertible (OP_ATTR f) where
  toShATermAux att0 xv = case xv of
    Assoc_op_attr -> return $ addATerm (ShAAppl "Assoc_op_attr" [] []) att0
    Comm_op_attr -> return $ addATerm (ShAAppl "Comm_op_attr" [] []) att0
    Idem_op_attr -> return $ addATerm (ShAAppl "Idem_op_attr" [] []) att0
    Unit_op_attr a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Unit_op_attr" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Assoc_op_attr" [] _ -> (att0, Assoc_op_attr)
    ShAAppl "Comm_op_attr" [] _ -> (att0, Comm_op_attr)
    ShAAppl "Idem_op_attr" [] _ -> (att0, Idem_op_attr)
    ShAAppl "Unit_op_attr" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Unit_op_attr a') }
    u -> fromShATermError "OP_ATTR" u

instance ShATermConvertible OP_HEAD where
  toShATermAux att0 xv = case xv of
    Op_head a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Op_head" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Op_head" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Op_head a' b' c' d') }}}}
    u -> fromShATermError "OP_HEAD" u

instance ShATermConvertible OP_TYPE where
  toShATermAux att0 xv = case xv of
    Op_type a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Op_type" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Op_type" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Op_type a' b' c' d') }}}}
    u -> fromShATermError "OP_TYPE" u

instance ShATermConvertible OpKind where
  toShATermAux att0 xv = case xv of
    Total -> return $ addATerm (ShAAppl "Total" [] []) att0
    Partial -> return $ addATerm (ShAAppl "Partial" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Total" [] _ -> (att0, Total)
    ShAAppl "Partial" [] _ -> (att0, Partial)
    u -> fromShATermError "OpKind" u

instance ShATermConvertible f => ShATermConvertible (OP_ITEM f) where
  toShATermAux att0 xv = case xv of
    Op_decl a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Op_decl" [a', b', c', d'] []) att4
    Op_defn a b c d -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      return $ addATerm (ShAAppl "Op_defn" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Op_decl" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Op_decl a' b' c' d') }}}}
    ShAAppl "Op_defn" [a, b, c, d] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      (att4, Op_defn a' b' c' d') }}}}
    u -> fromShATermError "OP_ITEM" u

instance ShATermConvertible f => ShATermConvertible (SORT_ITEM f) where
  toShATermAux att0 xv = case xv of
    Sort_decl a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Sort_decl" [a', b'] []) att2
    Subsort_decl a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Subsort_decl" [a', b', c'] []) att3
    Subsort_defn a b c d e -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      (att5, e') <- toShATerm' att4 e
      return $ addATerm (ShAAppl "Subsort_defn" [a', b', c', d',
                                                 e'] []) att5
    Iso_decl a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Iso_decl" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Sort_decl" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Sort_decl a' b') }}
    ShAAppl "Subsort_decl" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Subsort_decl a' b' c') }}}
    ShAAppl "Subsort_defn" [a, b, c, d, e] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      case fromShATerm' e att4 of
      { (att5, e') ->
      (att5, Subsort_defn a' b' c' d' e') }}}}}
    ShAAppl "Iso_decl" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Iso_decl a' b') }}
    u -> fromShATermError "SORT_ITEM" u

instance (ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (SIG_ITEMS s f) where
  toShATermAux att0 xv = case xv of
    Sort_items a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Sort_items" [a', b', c'] []) att3
    Op_items a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Op_items" [a', b'] []) att2
    Pred_items a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Pred_items" [a', b'] []) att2
    Datatype_items a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Datatype_items" [a', b', c'] []) att3
    Ext_SIG_ITEMS a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Ext_SIG_ITEMS" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Sort_items" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Sort_items a' b' c') }}}
    ShAAppl "Op_items" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Op_items a' b') }}
    ShAAppl "Pred_items" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Pred_items a' b') }}
    ShAAppl "Datatype_items" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Datatype_items a' b' c') }}}
    ShAAppl "Ext_SIG_ITEMS" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Ext_SIG_ITEMS a') }
    u -> fromShATermError "SIG_ITEMS" u

instance ShATermConvertible SortsKind where
  toShATermAux att0 xv = case xv of
    NonEmptySorts -> return $ addATerm (ShAAppl "NonEmptySorts" [] []) att0
    PossiblyEmptySorts ->
      return $ addATerm (ShAAppl "PossiblyEmptySorts" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "NonEmptySorts" [] _ -> (att0, NonEmptySorts)
    ShAAppl "PossiblyEmptySorts" [] _ -> (att0, PossiblyEmptySorts)
    u -> fromShATermError "SortsKind" u

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f) where
  toShATermAux att0 xv = case xv of
    Sig_items a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Sig_items" [a'] []) att1
    Free_datatype a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Free_datatype" [a', b', c'] []) att3
    Sort_gen a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Sort_gen" [a', b'] []) att2
    Var_items a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Var_items" [a', b'] []) att2
    Local_var_axioms a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Local_var_axioms" [a', b', c'] []) att3
    Axiom_items a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Axiom_items" [a', b'] []) att2
    Ext_BASIC_ITEMS a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Ext_BASIC_ITEMS" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Sig_items" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Sig_items a') }
    ShAAppl "Free_datatype" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Free_datatype a' b' c') }}}
    ShAAppl "Sort_gen" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Sort_gen a' b') }}
    ShAAppl "Var_items" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Var_items a' b') }}
    ShAAppl "Local_var_axioms" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, Local_var_axioms a' b' c') }}}
    ShAAppl "Axiom_items" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Axiom_items a' b') }}
    ShAAppl "Ext_BASIC_ITEMS" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Ext_BASIC_ITEMS a') }
    u -> fromShATermError "BASIC_ITEMS" u

instance (ShATermConvertible b, ShATermConvertible s,
          ShATermConvertible f) => ShATermConvertible (BASIC_SPEC b s f) where
  toShATermAux att0 xv = case xv of
    Basic_spec a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Basic_spec" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Basic_spec" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Basic_spec a') }
    u -> fromShATermError "BASIC_SPEC" u

_tcSYMB_OR_MAPTc :: TyCon
_tcSYMB_OR_MAPTc = mkTyCon "CASL.AS_Basic_CASL.SYMB_OR_MAP"
instance Typeable SYMB_OR_MAP where
    typeOf _ = mkTyConApp _tcSYMB_OR_MAPTc []

_tcTYPETc :: TyCon
_tcTYPETc = mkTyCon "CASL.AS_Basic_CASL.TYPE"
instance Typeable TYPE where
    typeOf _ = mkTyConApp _tcTYPETc []

_tcSYMBTc :: TyCon
_tcSYMBTc = mkTyCon "CASL.AS_Basic_CASL.SYMB"
instance Typeable SYMB where
    typeOf _ = mkTyConApp _tcSYMBTc []

_tcSYMB_KINDTc :: TyCon
_tcSYMB_KINDTc = mkTyCon "CASL.AS_Basic_CASL.SYMB_KIND"
instance Typeable SYMB_KIND where
    typeOf _ = mkTyConApp _tcSYMB_KINDTc []

_tcSYMB_MAP_ITEMSTc :: TyCon
_tcSYMB_MAP_ITEMSTc = mkTyCon "CASL.AS_Basic_CASL.SYMB_MAP_ITEMS"
instance Typeable SYMB_MAP_ITEMS where
    typeOf _ = mkTyConApp _tcSYMB_MAP_ITEMSTc []

_tcSYMB_ITEMSTc :: TyCon
_tcSYMB_ITEMSTc = mkTyCon "CASL.AS_Basic_CASL.SYMB_ITEMS"
instance Typeable SYMB_ITEMS where
    typeOf _ = mkTyConApp _tcSYMB_ITEMSTc []

_tcOP_SYMBTc :: TyCon
_tcOP_SYMBTc = mkTyCon "CASL.AS_Basic_CASL.OP_SYMB"
instance Typeable OP_SYMB where
    typeOf _ = mkTyConApp _tcOP_SYMBTc []

_tcTERMTc :: TyCon
_tcTERMTc = mkTyCon "CASL.AS_Basic_CASL.TERM"
instance Typeable1 TERM where
    typeOf1 _ = mkTyConApp _tcTERMTc []

_tcPRED_SYMBTc :: TyCon
_tcPRED_SYMBTc = mkTyCon "CASL.AS_Basic_CASL.PRED_SYMB"
instance Typeable PRED_SYMB where
    typeOf _ = mkTyConApp _tcPRED_SYMBTc []

_tcQUANTIFIERTc :: TyCon
_tcQUANTIFIERTc = mkTyCon "CASL.AS_Basic_CASL.QUANTIFIER"
instance Typeable QUANTIFIER where
    typeOf _ = mkTyConApp _tcQUANTIFIERTc []

_tcConstraintTc :: TyCon
_tcConstraintTc = mkTyCon "CASL.AS_Basic_CASL.Constraint"
instance Typeable Constraint where
    typeOf _ = mkTyConApp _tcConstraintTc []

_tcFORMULATc :: TyCon
_tcFORMULATc = mkTyCon "CASL.AS_Basic_CASL.FORMULA"
instance Typeable1 FORMULA where
    typeOf1 _ = mkTyConApp _tcFORMULATc []

_tcVAR_DECLTc :: TyCon
_tcVAR_DECLTc = mkTyCon "CASL.AS_Basic_CASL.VAR_DECL"
instance Typeable VAR_DECL where
    typeOf _ = mkTyConApp _tcVAR_DECLTc []

_tcCOMPONENTSTc :: TyCon
_tcCOMPONENTSTc = mkTyCon "CASL.AS_Basic_CASL.COMPONENTS"
instance Typeable COMPONENTS where
    typeOf _ = mkTyConApp _tcCOMPONENTSTc []

_tcALTERNATIVETc :: TyCon
_tcALTERNATIVETc = mkTyCon "CASL.AS_Basic_CASL.ALTERNATIVE"
instance Typeable ALTERNATIVE where
    typeOf _ = mkTyConApp _tcALTERNATIVETc []

_tcDATATYPE_DECLTc :: TyCon
_tcDATATYPE_DECLTc = mkTyCon "CASL.AS_Basic_CASL.DATATYPE_DECL"
instance Typeable DATATYPE_DECL where
    typeOf _ = mkTyConApp _tcDATATYPE_DECLTc []

_tcPRED_HEADTc :: TyCon
_tcPRED_HEADTc = mkTyCon "CASL.AS_Basic_CASL.PRED_HEAD"
instance Typeable PRED_HEAD where
    typeOf _ = mkTyConApp _tcPRED_HEADTc []

_tcPRED_TYPETc :: TyCon
_tcPRED_TYPETc = mkTyCon "CASL.AS_Basic_CASL.PRED_TYPE"
instance Typeable PRED_TYPE where
    typeOf _ = mkTyConApp _tcPRED_TYPETc []

_tcPRED_ITEMTc :: TyCon
_tcPRED_ITEMTc = mkTyCon "CASL.AS_Basic_CASL.PRED_ITEM"
instance Typeable1 PRED_ITEM where
    typeOf1 _ = mkTyConApp _tcPRED_ITEMTc []

_tcOP_ATTRTc :: TyCon
_tcOP_ATTRTc = mkTyCon "CASL.AS_Basic_CASL.OP_ATTR"
instance Typeable1 OP_ATTR where
    typeOf1 _ = mkTyConApp _tcOP_ATTRTc []

_tcOP_HEADTc :: TyCon
_tcOP_HEADTc = mkTyCon "CASL.AS_Basic_CASL.OP_HEAD"
instance Typeable OP_HEAD where
    typeOf _ = mkTyConApp _tcOP_HEADTc []

_tcOP_TYPETc :: TyCon
_tcOP_TYPETc = mkTyCon "CASL.AS_Basic_CASL.OP_TYPE"
instance Typeable OP_TYPE where
    typeOf _ = mkTyConApp _tcOP_TYPETc []

_tcOpKindTc :: TyCon
_tcOpKindTc = mkTyCon "CASL.AS_Basic_CASL.OpKind"
instance Typeable OpKind where
    typeOf _ = mkTyConApp _tcOpKindTc []

_tcOP_ITEMTc :: TyCon
_tcOP_ITEMTc = mkTyCon "CASL.AS_Basic_CASL.OP_ITEM"
instance Typeable1 OP_ITEM where
    typeOf1 _ = mkTyConApp _tcOP_ITEMTc []

_tcSORT_ITEMTc :: TyCon
_tcSORT_ITEMTc = mkTyCon "CASL.AS_Basic_CASL.SORT_ITEM"
instance Typeable1 SORT_ITEM where
    typeOf1 _ = mkTyConApp _tcSORT_ITEMTc []

_tcSIG_ITEMSTc :: TyCon
_tcSIG_ITEMSTc = mkTyCon "CASL.AS_Basic_CASL.SIG_ITEMS"
instance Typeable2 SIG_ITEMS where
    typeOf2 _ = mkTyConApp _tcSIG_ITEMSTc []

_tcSortsKindTc :: TyCon
_tcSortsKindTc = mkTyCon "CASL.AS_Basic_CASL.SortsKind"
instance Typeable SortsKind where
    typeOf _ = mkTyConApp _tcSortsKindTc []

_tcBASIC_ITEMSTc :: TyCon
_tcBASIC_ITEMSTc = mkTyCon "CASL.AS_Basic_CASL.BASIC_ITEMS"
instance Typeable3 BASIC_ITEMS where
    typeOf3 _ = mkTyConApp _tcBASIC_ITEMSTc []

_tcBASIC_SPECTc :: TyCon
_tcBASIC_SPECTc = mkTyCon "CASL.AS_Basic_CASL.BASIC_SPEC"
instance Typeable3 BASIC_SPEC where
    typeOf3 _ = mkTyConApp _tcBASIC_SPECTc []

instance ShATermConvertible e => ShATermConvertible (DefMorExt e) where
  toShATermAux att0 xv = case xv of
    DefMorExt a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "DefMorExt" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "DefMorExt" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, DefMorExt a') }
    u -> fromShATermError "DefMorExt" u

instance (ShATermConvertible f, ShATermConvertible e,
          ShATermConvertible m) => ShATermConvertible (Morphism f e m) where
  toShATermAux att0 xv = case xv of
    Morphism a b c d e f -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      (att5, e') <- toShATerm' att4 e
      (att6, f') <- toShATerm' att5 f
      return $ addATerm (ShAAppl "Morphism" [a', b', c', d', e',
                                             f'] []) att6
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Morphism" [a, b, c, d, e, f] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      case fromShATerm' e att4 of
      { (att5, e') ->
      case fromShATerm' f att5 of
      { (att6, f') ->
      (att6, Morphism a' b' c' d' e' f') }}}}}}
    u -> fromShATermError "Morphism" u

instance ShATermConvertible RawSymbol where
  toShATermAux att0 xv = case xv of
    ASymbol a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "ASymbol" [a'] []) att1
    AKindedSymb a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "AKindedSymb" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "ASymbol" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, ASymbol a') }
    ShAAppl "AKindedSymb" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, AKindedSymb a' b') }}
    u -> fromShATermError "RawSymbol" u

_tcDefMorExtTc :: TyCon
_tcDefMorExtTc = mkTyCon "CASL.Morphism.DefMorExt"
instance Typeable1 DefMorExt where
    typeOf1 _ = mkTyConApp _tcDefMorExtTc []

_tcMorphismTc :: TyCon
_tcMorphismTc = mkTyCon "CASL.Morphism.Morphism"
instance Typeable3 Morphism where
    typeOf3 _ = mkTyConApp _tcMorphismTc []

_tcRawSymbolTc :: TyCon
_tcRawSymbolTc = mkTyCon "CASL.Morphism.RawSymbol"
instance Typeable RawSymbol where
    typeOf _ = mkTyConApp _tcRawSymbolTc []

_tcOpTypeTc :: TyCon
_tcOpTypeTc = mkTyCon "CASL.Sign.OpType"
instance Typeable OpType where
    typeOf _ = mkTyConApp _tcOpTypeTc []

_tcPredTypeTc :: TyCon
_tcPredTypeTc = mkTyCon "CASL.Sign.PredType"
instance Typeable PredType where
    typeOf _ = mkTyConApp _tcPredTypeTc []

_tcSymbTypeTc :: TyCon
_tcSymbTypeTc = mkTyCon "CASL.Sign.SymbType"
instance Typeable SymbType where
    typeOf _ = mkTyConApp _tcSymbTypeTc []

_tcSymbolTc :: TyCon
_tcSymbolTc = mkTyCon "CASL.Sign.Symbol"
instance Typeable Symbol where
    typeOf _ = mkTyConApp _tcSymbolTc []

_tcSignTc :: TyCon
_tcSignTc = mkTyCon "CASL.Sign.Sign"
instance Typeable2 Sign where
    typeOf2 _ = mkTyConApp _tcSignTc []

instance ShATermConvertible OpType where
  toShATermAux att0 xv = case xv of
    OpType a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "OpType" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "OpType" [a, b, c] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      (att3, OpType a' b' c') }}}
    u -> fromShATermError "OpType" u

instance ShATermConvertible PredType where
  toShATermAux att0 xv = case xv of
    PredType a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "PredType" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "PredType" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, PredType a') }
    u -> fromShATermError "PredType" u

instance ShATermConvertible SymbType where
  toShATermAux att0 xv = case xv of
    SortAsItemType -> return $ addATerm (ShAAppl "SortAsItemType" [] []) att0
    SubsortAsItemType a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "SubsortAsItemType" [a'] []) att1
    OpAsItemType a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "OpAsItemType" [a'] []) att1
    PredAsItemType a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "PredAsItemType" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "SortAsItemType" [] _ -> (att0, SortAsItemType)
    ShAAppl "SubsortAsItemType" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, SubsortAsItemType a') }
    ShAAppl "OpAsItemType" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, OpAsItemType a') }
    ShAAppl "PredAsItemType" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, PredAsItemType a') }
    u -> fromShATermError "SymbType" u

instance ShATermConvertible Symbol where
  toShATermAux att0 xv = case xv of
    Symbol a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Symbol" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Symbol" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Symbol a' b') }}
    u -> fromShATermError "Symbol" u

instance (ShATermConvertible f,
          ShATermConvertible e) => ShATermConvertible (Sign f e) where
  toShATermAux att0 xv = case xv of
    Sign a b c d e f g h i j k l -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      (att5, e') <- toShATerm' att4 e
      (att6, f') <- toShATerm' att5 f
      (att7, g') <- toShATerm' att6 g
      (att8, h') <- toShATerm' att7 h
      (att9, i') <- toShATerm' att8 i
      (att10, j') <- toShATerm' att9 j
      (att11, k') <- toShATerm' att10 k
      (att12, l') <- toShATerm' att11 l
      return $ addATerm (ShAAppl "Sign" [a', b', c', d', e', f', g', h',
                                         i', j', k', l'] []) att12
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Sign" [a, b, c, d, e, f, g, h, i, j, k, l] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      case fromShATerm' e att4 of
      { (att5, e') ->
      case fromShATerm' f att5 of
      { (att6, f') ->
      case fromShATerm' g att6 of
      { (att7, g') ->
      case fromShATerm' h att7 of
      { (att8, h') ->
      case fromShATerm' i att8 of
      { (att9, i') ->
      case fromShATerm' j att9 of
      { (att10, j') ->
      case fromShATerm' k att10 of
      { (att11, k') ->
      case fromShATerm' l att11 of
      { (att12, l') ->
      (att12, Sign a' b' c' d' e' f' g' h' i' j' k' l') }}}}}}}}}}}}
    u -> fromShATermError "Sign" u

instance ShATermConvertible a => ShATermConvertible (CASL_SL a) where
  toShATermAux att0 xv = case xv of
    CASL_SL a b c d e f g h -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      (att4, d') <- toShATerm' att3 d
      (att5, e') <- toShATerm' att4 e
      (att6, f') <- toShATerm' att5 f
      (att7, g') <- toShATerm' att6 g
      (att8, h') <- toShATerm' att7 h
      return $ addATerm (ShAAppl "CASL_SL" [a', b', c', d', e', f', g',
                                            h'] []) att8
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "CASL_SL" [a, b, c, d, e, f, g, h] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      case fromShATerm' c att2 of
      { (att3, c') ->
      case fromShATerm' d att3 of
      { (att4, d') ->
      case fromShATerm' e att4 of
      { (att5, e') ->
      case fromShATerm' f att5 of
      { (att6, f') ->
      case fromShATerm' g att6 of
      { (att7, g') ->
      case fromShATerm' h att7 of
      { (att8, h') ->
      (att8, CASL_SL a' b' c' d' e' f' g' h') }}}}}}}}
    u -> fromShATermError "CASL_SL" u

instance ShATermConvertible SortGenerationFeatures where
  toShATermAux att0 xv = case xv of
    NoSortGen -> return $ addATerm (ShAAppl "NoSortGen" [] []) att0
    SortGen a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "SortGen" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "NoSortGen" [] _ -> (att0, NoSortGen)
    ShAAppl "SortGen" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, SortGen a' b') }}
    u -> fromShATermError "SortGenerationFeatures" u

instance ShATermConvertible SubsortingFeatures where
  toShATermAux att0 xv = case xv of
    NoSub -> return $ addATerm (ShAAppl "NoSub" [] []) att0
    LocFilSub -> return $ addATerm (ShAAppl "LocFilSub" [] []) att0
    Sub -> return $ addATerm (ShAAppl "Sub" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "NoSub" [] _ -> (att0, NoSub)
    ShAAppl "LocFilSub" [] _ -> (att0, LocFilSub)
    ShAAppl "Sub" [] _ -> (att0, Sub)
    u -> fromShATermError "SubsortingFeatures" u

instance ShATermConvertible CASL_Formulas where
  toShATermAux att0 xv = case xv of
    Atomic -> return $ addATerm (ShAAppl "Atomic" [] []) att0
    Horn -> return $ addATerm (ShAAppl "Horn" [] []) att0
    GHorn -> return $ addATerm (ShAAppl "GHorn" [] []) att0
    FOL -> return $ addATerm (ShAAppl "FOL" [] []) att0
    SOL -> return $ addATerm (ShAAppl "SOL" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Atomic" [] _ -> (att0, Atomic)
    ShAAppl "Horn" [] _ -> (att0, Horn)
    ShAAppl "GHorn" [] _ -> (att0, GHorn)
    ShAAppl "FOL" [] _ -> (att0, FOL)
    ShAAppl "SOL" [] _ -> (att0, SOL)
    u -> fromShATermError "CASL_Formulas" u

_tcCASL_SLTc :: TyCon
_tcCASL_SLTc = mkTyCon "CASL.Sublogic.CASL_SL"
instance Typeable1 CASL_SL where
    typeOf1 _ = mkTyConApp _tcCASL_SLTc []

_tcSortGenerationFeaturesTc :: TyCon
_tcSortGenerationFeaturesTc = mkTyCon "CASL.Sublogic.SortGenerationFeatures"
instance Typeable SortGenerationFeatures where
    typeOf _ = mkTyConApp _tcSortGenerationFeaturesTc []

_tcSubsortingFeaturesTc :: TyCon
_tcSubsortingFeaturesTc = mkTyCon "CASL.Sublogic.SubsortingFeatures"
instance Typeable SubsortingFeatures where
    typeOf _ = mkTyConApp _tcSubsortingFeaturesTc []

_tcCASL_FormulasTc :: TyCon
_tcCASL_FormulasTc = mkTyCon "CASL.Sublogic.CASL_Formulas"
instance Typeable CASL_Formulas where
    typeOf _ = mkTyConApp _tcCASL_FormulasTc []
