{-# OPTIONS -w -O0 #-}
{- |
Module      :  LF/ATC_LF.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):
'LF.Sign.Symbol'
'LF.Sign.EXP'
'LF.Sign.DEF'
'LF.Sign.Sign'
'LF.Morphism.MorphType'
'LF.Morphism.Morphism'
'LF.AS.BASIC_SPEC'
'LF.AS.BASIC_ITEM'
'LF.AS.SYMB_ITEMS'
'LF.AS.SYMB_MAP_ITEMS'
'LF.AS.SYMB_OR_MAP'
-}

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

module LF.ATC_LF () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation
import Common.Doc
import Common.Doc hiding (space)
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Result
import Data.Data
import Data.List
import Data.Maybe
import Data.Maybe (isNothing, fromMaybe)
import LF.AS
import LF.Morphism
import LF.Sign
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for LF.Sign.Symbol derive : ShATermConvertible !-}
{-! for LF.Sign.EXP derive : ShATermConvertible !-}
{-! for LF.Sign.DEF derive : ShATermConvertible !-}
{-! for LF.Sign.Sign derive : ShATermConvertible !-}
{-! for LF.Morphism.MorphType derive : ShATermConvertible !-}
{-! for LF.Morphism.Morphism derive : ShATermConvertible !-}
{-! for LF.AS.BASIC_SPEC derive : ShATermConvertible !-}
{-! for LF.AS.BASIC_ITEM derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_OR_MAP derive : ShATermConvertible !-}

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

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 BASIC_ITEM where
  toShATermAux att0 xv = case xv of
    Decl a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Decl" [a'] []) att1
    Form a -> do
      (att1, a') <- toShATerm' att0 a
      return $ addATerm (ShAAppl "Form" [a'] []) att1
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Decl" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Decl a') }
    ShAAppl "Form" [a] _ ->
      case fromShATerm' a att0 of
      { (att1, a') ->
      (att1, Form a') }
    u -> fromShATermError "BASIC_ITEM" u

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

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

instance ShATermConvertible Morphism where
  toShATermAux att0 xv = case xv of
    Morphism a b c d e f g -> 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
      return $ addATerm (ShAAppl "Morphism" [a', b', c', d', e', f',
                                             g'] []) att7
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Morphism" [a, b, c, d, e, f, g] _ ->
      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') ->
      (att7, Morphism a' b' c' d' e' f' g') }}}}}}}
    u -> fromShATermError "Morphism" u

instance ShATermConvertible MorphType where
  toShATermAux att0 xv = case xv of
    Definitional -> return $ addATerm (ShAAppl "Definitional" [] []) att0
    Postulated -> return $ addATerm (ShAAppl "Postulated" [] []) att0
    Unknown -> return $ addATerm (ShAAppl "Unknown" [] []) att0
  fromShATermAux ix att0 = case getShATerm ix att0 of
    ShAAppl "Definitional" [] _ -> (att0, Definitional)
    ShAAppl "Postulated" [] _ -> (att0, Postulated)
    ShAAppl "Unknown" [] _ -> (att0, Unknown)
    u -> fromShATermError "MorphType" u

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

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

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