ATC_QBF.hs revision 7a3fe82695aa32657693e05712f84d7f81672f2e
{-# LINE 1 "QBF/ATC_QBF.der.hs" #-}
{-# OPTIONS -w #-}
{- |
Module : QBF/ATC_QBF.der.hs
Description : generated Typeable, ShATermConvertible instances
Copyright : (c) DFKI Bremen 2008
License : similar to LGPL, see HetCATS/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):
-}
{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
dependency files:
-}
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 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.PRED_ITEM derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.BASIC_SPEC derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.BASIC_ITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.ID derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMB_ITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMB_MAP_ITEMS derive : Typeable !-}
{-! for QBF.AS_BASIC_QBF.SYMB_OR_MAP derive : Typeable !-}
{-! for QBF.Symbol.Symbol derive : Typeable !-}
{-! for QBF.Sublogic.PropFormulae derive : Typeable !-}
{-! for QBF.Sublogic.PropSL derive : Typeable !-}
{-! for Propositional.Sign.Sign derive : ShATermConvertible !-}
{-! for QBF.Morphism.Morphism derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.PRED_ITEM derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASIC_SPEC derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.BASIC_ITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.FORMULA derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.ID derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for QBF.AS_BASIC_QBF.SYMB_OR_MAP derive : ShATermConvertible !-}
{-! for QBF.Symbol.Symbol derive : ShATermConvertible !-}
{-! for QBF.Sublogic.PropFormulae derive : ShATermConvertible !-}
{-! for QBF.Sublogic.PropSL derive : ShATermConvertible !-}
{- ? Generated by DrIFT : Look, but Don't Touch. ? -}
-- Imported from other files :-
_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
_tcPRED_ITEMTc :: TyCon
_tcPRED_ITEMTc = mkTyCon "QBF.AS_BASIC_QBF.PRED_ITEM"
instance Typeable PRED_ITEM where
typeOf _ = mkTyConApp _tcPRED_ITEMTc []
_tcBASIC_SPECTc :: TyCon
_tcBASIC_SPECTc = mkTyCon "QBF.AS_BASIC_QBF.BASIC_SPEC"
instance Typeable BASIC_SPEC where
typeOf _ = mkTyConApp _tcBASIC_SPECTc []
_tcBASIC_ITEMSTc :: TyCon
_tcBASIC_ITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.BASIC_ITEMS"
instance Typeable BASIC_ITEMS where
typeOf _ = mkTyConApp _tcBASIC_ITEMSTc []
_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 []
_tcSYMB_ITEMSTc :: TyCon
_tcSYMB_ITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.SYMB_ITEMS"
instance Typeable SYMB_ITEMS where
typeOf _ = mkTyConApp _tcSYMB_ITEMSTc []
_tcSYMBTc :: TyCon
_tcSYMBTc = mkTyCon "QBF.AS_BASIC_QBF.SYMB"
instance Typeable SYMB where
typeOf _ = mkTyConApp _tcSYMBTc []
_tcSYMB_MAP_ITEMSTc :: TyCon
_tcSYMB_MAP_ITEMSTc = mkTyCon "QBF.AS_BASIC_QBF.SYMB_MAP_ITEMS"
instance Typeable SYMB_MAP_ITEMS where
typeOf _ = mkTyConApp _tcSYMB_MAP_ITEMSTc []
_tcSYMB_OR_MAPTc :: TyCon
_tcSYMB_OR_MAPTc = mkTyCon "QBF.AS_BASIC_QBF.SYMB_OR_MAP"
instance Typeable SYMB_OR_MAP where
typeOf _ = mkTyConApp _tcSYMB_OR_MAPTc []
instance ShATermConvertible PRED_ITEM where
toShATermAux att0 xv = case xv of
Pred_item a b -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "Pred_item" [a', b'] []) att2
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Pred_item" [a, b] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
case fromShATerm' b att1 of
{ (att2, b') ->
(att2, Pred_item a' b') }}
u -> fromShATermError "PRED_ITEM" 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 BASIC_ITEMS where
toShATermAux att0 xv = case xv of
Pred_decl a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Pred_decl" [a'] []) att1
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 "Pred_decl" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Pred_decl a') }
ShAAppl "Axiom_items" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Axiom_items a') }
u -> fromShATermError "BASIC_ITEMS" u
instance ShATermConvertible FORMULA where
toShATermAux att0 xv = case xv of
False_atom a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "False_atom" [a'] []) att1
True_atom a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "True_atom" [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
Quantified_ForAll a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Quantified_ForAll" [a', b',
c'] []) att3
Quantified_Exists a b c -> do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
(att3, c') <- toShATerm' att2 c
return $ addATerm (ShAAppl "Quantified_Exists" [a', b',
c'] []) att3
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "False_atom" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, False_atom a') }
ShAAppl "True_atom" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, True_atom 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 "Quantified_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, Quantified_ForAll a' b' c') }}}
ShAAppl "Quantified_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, Quantified_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 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 where
toShATermAux att0 xv = case xv of
Symb_id a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "Symb_id" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "Symb_id" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, Symb_id a') }
u -> fromShATermError "SYMB" 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 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 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 PropSL where
toShATermAux att0 xv = case xv of
PropSL a -> do
(att1, a') <- toShATerm' att0 a
return $ addATerm (ShAAppl "PropSL" [a'] []) att1
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "PropSL" [a] _ ->
case fromShATerm' a att0 of
{ (att1, a') ->
(att1, PropSL a') }
u -> fromShATermError "PropSL" u
instance ShATermConvertible PropFormulae 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 "PropFormulae" u
_tcPropSLTc :: TyCon
_tcPropSLTc = mkTyCon "QBF.Sublogic.PropSL"
instance Typeable PropSL where
typeOf _ = mkTyConApp _tcPropSLTc []
_tcPropFormulaeTc :: TyCon
_tcPropFormulaeTc = mkTyCon "QBF.Sublogic.PropFormulae"
instance Typeable PropFormulae where
typeOf _ = mkTyConApp _tcPropFormulaeTc []
_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