{-# OPTIONS -w -O0 #-}
{- |
Module      :  ConstraintCASL/ATC_ConstraintCASL.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):
'ConstraintCASL.AS_ConstraintCASL.ConstraintFORMULA'
'ConstraintCASL.AS_ConstraintCASL.RELATION'
'ConstraintCASL.AS_ConstraintCASL.ATOMCONJUNCTION'
'ConstraintCASL.AS_ConstraintCASL.ATOM'
'ConstraintCASL.AS_ConstraintCASL.ConstraintTERM'
-}

{-
  Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
ConstraintCASL/AS_ConstraintCASL.hs
-}

module ConstraintCASL.ATC_ConstraintCASL () where

import ATerm.Lib
import CASL.AS_Basic_CASL
import CASL.ATC_CASL
import Common.Id
import ConstraintCASL.AS_ConstraintCASL
import Data.Typeable

{-! for ConstraintCASL.AS_ConstraintCASL.ConstraintFORMULA derive : Typeable !-}
{-! for ConstraintCASL.AS_ConstraintCASL.RELATION derive : Typeable !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ATOMCONJUNCTION derive : Typeable !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ATOM derive : Typeable !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ConstraintTERM derive : Typeable !-}

{-! for ConstraintCASL.AS_ConstraintCASL.ConstraintFORMULA derive : ShATermConvertible !-}
{-! for ConstraintCASL.AS_ConstraintCASL.RELATION derive : ShATermConvertible !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ATOMCONJUNCTION derive : ShATermConvertible !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ATOM derive : ShATermConvertible !-}
{-! for ConstraintCASL.AS_ConstraintCASL.ConstraintTERM derive : ShATermConvertible !-}

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

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

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

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

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

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

_tcConstraintTERMTc :: TyCon
_tcConstraintTERMTc = mkTyCon "ConstraintCASL.AS_ConstraintCASL.ConstraintTERM"
instance Typeable ConstraintTERM where
    typeOf _ = mkTyConApp _tcConstraintTERMTc []

_tcATOMTc :: TyCon
_tcATOMTc = mkTyCon "ConstraintCASL.AS_ConstraintCASL.ATOM"
instance Typeable ATOM where
    typeOf _ = mkTyConApp _tcATOMTc []

_tcATOMCONJUNCTIONTc :: TyCon
_tcATOMCONJUNCTIONTc = mkTyCon "ConstraintCASL.AS_ConstraintCASL.ATOMCONJUNCTION"
instance Typeable ATOMCONJUNCTION where
    typeOf _ = mkTyConApp _tcATOMCONJUNCTIONTc []

_tcRELATIONTc :: TyCon
_tcRELATIONTc = mkTyCon "ConstraintCASL.AS_ConstraintCASL.RELATION"
instance Typeable RELATION where
    typeOf _ = mkTyConApp _tcRELATIONTc []

_tcConstraintFORMULATc :: TyCon
_tcConstraintFORMULATc = mkTyCon "ConstraintCASL.AS_ConstraintCASL.ConstraintFORMULA"
instance Typeable ConstraintFORMULA where
    typeOf _ = mkTyConApp _tcConstraintFORMULATc []
