{-# OPTIONS -w -O0 #-}
{- |
Module      :  CommonLogic/ATC_CommonLogic.der.hs
Description :  generated ShATermConvertible instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

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

Automatic derivation of instances via DrIFT-rule ShATermConvertible
  for the type(s):
'CommonLogic.AS_CommonLogic.BASIC_SPEC'
'CommonLogic.AS_CommonLogic.BASIC_ITEMS'
'CommonLogic.AS_CommonLogic.TEXT_META'
'CommonLogic.AS_CommonLogic.TEXT'
'CommonLogic.AS_CommonLogic.PHRASE'
'CommonLogic.AS_CommonLogic.COMMENT'
'CommonLogic.AS_CommonLogic.MODULE'
'CommonLogic.AS_CommonLogic.IMPORTATION'
'CommonLogic.AS_CommonLogic.SENTENCE'
'CommonLogic.AS_CommonLogic.QUANT'
'CommonLogic.AS_CommonLogic.BOOL_SENT'
'CommonLogic.AS_CommonLogic.AndOr'
'CommonLogic.AS_CommonLogic.ImplEq'
'CommonLogic.AS_CommonLogic.ATOM'
'CommonLogic.AS_CommonLogic.TERM'
'CommonLogic.AS_CommonLogic.TERM_SEQ'
'CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK'
'CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS'
'CommonLogic.AS_CommonLogic.SYMB_OR_MAP'
'CommonLogic.AS_CommonLogic.SYMB_ITEMS'
'CommonLogic.Sign.Sign'
'CommonLogic.Symbol.Symbol'
'CommonLogic.Morphism.Morphism'
'CommonLogic.Sublogic.CLTextType'
'CommonLogic.Sublogic.CommonLogicSL'
-}

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

module CommonLogic.ATC_CommonLogic () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation (Annoted (..))
import Common.Doc
import Common.DocUtils
import Common.IRI
import Common.Id
import Common.Id as Id
import Common.Keywords
import Common.Result
import CommonLogic.AS_CommonLogic
import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Morphism
import CommonLogic.Morphism as Morphism
import CommonLogic.Sign
import CommonLogic.Sign as Sign
import CommonLogic.Sublogic
import CommonLogic.Symbol
import CommonLogic.Tools
import Control.Monad (unless)
import Data.Data
import Data.Function
import Data.List (isPrefixOf)
import Data.Set (Set)
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified CommonLogic.Sign as Sign
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for CommonLogic.AS_CommonLogic.BASIC_SPEC derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.BASIC_ITEMS derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.TEXT_META derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.TEXT derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.PHRASE derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.COMMENT derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.MODULE derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.IMPORTATION derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.SENTENCE derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.QUANT derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.BOOL_SENT derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.AndOr derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.ImplEq derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.ATOM derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.TERM derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.TERM_SEQ derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.SYMB_OR_MAP derive : ShATermConvertible !-}
{-! for CommonLogic.AS_CommonLogic.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for CommonLogic.Sign.Sign derive : ShATermConvertible !-}
{-! for CommonLogic.Symbol.Symbol derive : ShATermConvertible !-}
{-! for CommonLogic.Morphism.Morphism derive : ShATermConvertible !-}
{-! for CommonLogic.Sublogic.CLTextType derive : ShATermConvertible !-}
{-! for CommonLogic.Sublogic.CommonLogicSL derive : ShATermConvertible !-}

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

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

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_mapN a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Symb_mapN" [a', b', c'] []) att3
    Symb_mapS a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Symb_mapS" [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_mapN" [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_mapN a' b' c') }}}
    ShAAppl "Symb_mapS" [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_mapS a' b' c') }}}
    u -> fromShATermError "SYMB_OR_MAP" u

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

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

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

instance ShATermConvertible TERM where
  toShATermAux att0 xv = case xv of
    Name_term a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Name_term" [a'] []) att1
    Funct_term a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Funct_term" [a', b', c'] []) att3
    Comment_term a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Comment_term" [a', b', c'] []) att3
    That_term a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "That_term" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Name_term" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Name_term a') }
    ShAAppl "Funct_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, Funct_term a' b' c') }}}
    ShAAppl "Comment_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, Comment_term a' b' c') }}}
    ShAAppl "That_term" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, That_term a' b') }}
    u -> fromShATermError "TERM" u

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

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

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

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

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

instance ShATermConvertible SENTENCE where
  toShATermAux att0 xv = case xv of
    Quant_sent 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 "Quant_sent" [a', b', c', d'] []) att4
    Bool_sent a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Bool_sent" [a', b'] []) att2
    Atom_sent a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Atom_sent" [a', b'] []) att2
    Comment_sent a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Comment_sent" [a', b', c'] []) att3
    Irregular_sent a b -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      return $ addATerm (ShAAppl "Irregular_sent" [a', b'] []) att2
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Quant_sent" [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, Quant_sent a' b' c' d') }}}}
    ShAAppl "Bool_sent" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Bool_sent a' b') }}
    ShAAppl "Atom_sent" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Atom_sent a' b') }}
    ShAAppl "Comment_sent" [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, Comment_sent a' b' c') }}}
    ShAAppl "Irregular_sent" [a, b] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      case fromShATerm' b att1 of
      { (att2, b') ->
      (att2, Irregular_sent a' b') }}
    u -> fromShATermError "SENTENCE" u

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

instance ShATermConvertible MODULE where
  toShATermAux att0 xv = case xv of
    Mod a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Mod" [a', b', c'] []) att3
    Mod_ex 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 "Mod_ex" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Mod" [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, Mod a' b' c') }}}
    ShAAppl "Mod_ex" [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, Mod_ex a' b' c' d') }}}}
    u -> fromShATermError "MODULE" u

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

instance ShATermConvertible PHRASE where
  toShATermAux att0 xv = case xv of
    Module a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Module" [a'] []) att1
    Sentence a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Sentence" [a'] []) att1
    Importation a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Importation" [a'] []) att1
    Comment_text a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Comment_text" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Module" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Module a') }
    ShAAppl "Sentence" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Sentence a') }
    ShAAppl "Importation" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Importation a') }
    ShAAppl "Comment_text" [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, Comment_text a' b' c') }}}
    u -> fromShATermError "PHRASE" u

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

instance ShATermConvertible TEXT_META where
  toShATermAux att0 xv = case xv of
    Text_meta 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 "Text_meta" [a', b', c', d'] []) att4
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Text_meta" [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, Text_meta a' b' c' d') }}}}
    u -> fromShATermError "TEXT_META" u

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

instance ShATermConvertible BASIC_SPEC 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

instance ShATermConvertible Morphism where
  toShATermAux att0 xv = case xv of
    Morphism a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Morphism" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Morphism" [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, Morphism a' b' c') }}}
    u -> fromShATermError "Morphism" u

instance ShATermConvertible Sign where
  toShATermAux att0 xv = case xv of
    Sign a b c -> do
      (att1, a') <- toShATerm' att0 a
      (att2, b') <- toShATerm' att1 b
      (att3, c') <- toShATerm' att2 c
      return $ addATerm (ShAAppl "Sign" [a', b', c'] []) att3
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Sign" [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, Sign a' b' c') }}}
    u -> fromShATermError "Sign" u

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

instance ShATermConvertible CLTextType where
  toShATermAux att0 xv = case xv of
    Propositional -> return $ addATerm (ShAAppl "Propositional" [] []) att0
    FirstOrder -> return $ addATerm (ShAAppl "FirstOrder" [] []) att0
    Impredicative -> return $ addATerm (ShAAppl "Impredicative" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Propositional" [] _ -> (att0, Propositional)
    ShAAppl "FirstOrder" [] _ -> (att0, FirstOrder)
    ShAAppl "Impredicative" [] _ -> (att0, Impredicative)
    u -> fromShATermError "CLTextType" u

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