{-# OPTIONS -w -O0 #-}
{- |
Module      :  QBF/ATC_QBF.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):
'Propositional.Sign.Sign'
'QBF.Morphism.Morphism'
'QBF.AS_BASIC_QBF.PREDITEM'
'QBF.AS_BASIC_QBF.BASICSPEC'
'QBF.AS_BASIC_QBF.BASICITEMS'
'QBF.AS_BASIC_QBF.FORMULA'
'QBF.AS_BASIC_QBF.ID'
'QBF.AS_BASIC_QBF.SYMBITEMS'
'QBF.AS_BASIC_QBF.SYMB'
'QBF.AS_BASIC_QBF.SYMBMAPITEMS'
'QBF.AS_BASIC_QBF.SYMBORMAP'
'QBF.Symbol.Symbol'
'QBF.Sublogic.QBFFormulae'
'QBF.Sublogic.QBFSL'
-}

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

module QBF.ATC_QBF () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation as AS_Anno
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Id as Id
import Common.Keywords
import Common.Result
import Control.Monad (unless)
import Data.Maybe (isJust)
import Data.Typeable
import Propositional.Sign
import Propositional.Sign as Sign
import QBF.AS_BASIC_QBF
import QBF.Morphism
import QBF.Morphism as Morphism
import QBF.Sublogic
import QBF.Symbol
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.Lib.State as State
import qualified Common.Result as Result
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Propositional.Sign as Sign
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Morphism as Morphism
import qualified QBF.Symbol as Symbol
import qualified QBF.Tools as Tools

{-! for Propositional.Sign.Sign derive : Typeable !-}
{-! for QBF.Morphism.Morphism derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.PREDITEM derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.BASICSPEC derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.BASICITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.ID derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMBITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMBMAPITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMBORMAP derive : Typeable !-}
{-! for QBF.Symbol.Symbol derive : Typeable !-}
{-! for QBF.Sublogic.QBFFormulae derive : Typeable !-}
{-! for QBF.Sublogic.QBFSL derive : Typeable !-}

{-! for Propositional.Sign.Sign derive : ShATermConvertible !-}
{-! for QBF.Morphism.Morphism derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.PREDITEM derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASICSPEC derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASICITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.ID derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBMAPITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMBORMAP derive : ShATermConvertible !-}
{-! for QBF.Symbol.Symbol derive : ShATermConvertible !-}
{-! for QBF.Sublogic.QBFFormulae derive : ShATermConvertible !-}
{-! for QBF.Sublogic.QBFSL derive : ShATermConvertible !-}

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

_tcSignTc :: TyCon
_tcSignTc = mkTyCon "Propositional.Sign.Sign"
instance Typeable Sign where
    typeOf _ = mkTyConApp _tcSignTc []

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

_tcPREDITEMTc :: TyCon
_tcPREDITEMTc = mkTyCon "QBF.AS_BASIC_QBF.PREDITEM"
instance Typeable PREDITEM where
    typeOf _ = mkTyConApp _tcPREDITEMTc []

_tcBASICSPECTc :: TyCon
_tcBASICSPECTc = mkTyCon "QBF.AS_BASIC_QBF.BASICSPEC"
instance Typeable BASICSPEC where
    typeOf _ = mkTyConApp _tcBASICSPECTc []

_tcBASICITEMSTc :: TyCon
_tcBASICITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.BASICITEMS"
instance Typeable BASICITEMS where
    typeOf _ = mkTyConApp _tcBASICITEMSTc []

_tcFORMULATc :: TyCon
_tcFORMULATc = mkTyCon "QBF.AS_BASIC_QBF.FORMULA"
instance Typeable FORMULA where
    typeOf _ = mkTyConApp _tcFORMULATc []

_tcIDTc :: TyCon
_tcIDTc = mkTyCon "QBF.AS_BASIC_QBF.ID"
instance Typeable ID where
    typeOf _ = mkTyConApp _tcIDTc []

_tcSYMBITEMSTc :: TyCon
_tcSYMBITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.SYMBITEMS"
instance Typeable SYMBITEMS where
    typeOf _ = mkTyConApp _tcSYMBITEMSTc []

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

_tcSYMBMAPITEMSTc :: TyCon
_tcSYMBMAPITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.SYMBMAPITEMS"
instance Typeable SYMBMAPITEMS where
    typeOf _ = mkTyConApp _tcSYMBMAPITEMSTc []

_tcSYMBORMAPTc :: TyCon
_tcSYMBORMAPTc = mkTyCon "QBF.AS_BASIC_QBF.SYMBORMAP"
instance Typeable SYMBORMAP where
    typeOf _ = mkTyConApp _tcSYMBORMAPTc []

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

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

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

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

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

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

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

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

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

_tcMorphismTc :: TyCon
_tcMorphismTc = mkTyCon "QBF.Morphism.Morphism"
instance Typeable Morphism where
    typeOf _ = mkTyConApp _tcMorphismTc []

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

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

_tcQBFSLTc :: TyCon
_tcQBFSLTc = mkTyCon "QBF.Sublogic.QBFSL"
instance Typeable QBFSL where
    typeOf _ = mkTyConApp _tcQBFSLTc []

_tcQBFFormulaeTc :: TyCon
_tcQBFFormulaeTc = mkTyCon "QBF.Sublogic.QBFFormulae"
instance Typeable QBFFormulae where
    typeOf _ = mkTyConApp _tcQBFFormulaeTc []

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

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
