DevGraph.der.hs revision b03274844ecd270f9e9331f51cc4236a33e2e671
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{- |
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederModule : $Header$
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederDescription : ShATermConvertible instances
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederCopyright : (c) C. Maeder, Uni Bremen 2005-2006
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederMaintainer : maeder@tzi.de
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederStability : provisional
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederPortability : portable
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederderive 'ShATermConvertible' instance
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder for the type(s): 'DGNodeLab' 'DGLinkLab' 'DGRule' 'BasicConsProof' 'ThmLinkStatus' 'DGLinkType' 'Conservativity' 'DGOrigin' 'NodeSig' 'MaybeNode' 'UnitSig' 'ImpUnitSigOrSig' 'ArchSig' 'GlobalEntry' 'DGChange'
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederinstances for 'BasicProof' and 'G_theory' need to be given explicitely
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maedermodule ATC.DevGraph where
f6cea53c107f81a3f3225481f1673452e29c555cChristian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Static.DevGraph
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Logic.Logic
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maederimport Common.ATerm.Lib
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.DynamicUtils
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maederimport ATC.AS_Library()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport ATC.Prover()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport ATC.Grothendieck
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for DGNodeLab derive : ShATermConvertible !-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{-! for DGLinkLab derive : ShATermConvertible !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for DGRule derive : ShATermConvertible !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for BasicConsProof derive : ShATermConvertible !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for ThmLinkStatus derive : ShATermConvertible !-}
1aa11f4e4b984f2a6d6ce9700cbe82283c8d196aChristian Maeder{-! for DGLinkType derive : ShATermConvertible !-}
1aa11f4e4b984f2a6d6ce9700cbe82283c8d196aChristian Maeder{-! for Conservativity derive : ShATermConvertible !-}
1aa11f4e4b984f2a6d6ce9700cbe82283c8d196aChristian Maeder{-! for DGOrigin derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for NodeSig derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for MaybeNode derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for UnitSig derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for ImpUnitSigOrSig derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for ArchSig derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for GlobalEntry derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for DGChange derive : ShATermConvertible !-}
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder{-! for GlobalContext derive : ShATermConvertible !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{-! for DGNodeLab derive : Typeable !-}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder{-! for DGLinkLab derive : Typeable !-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{-! for DGRule derive : Typeable !-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{-! for BasicConsProof derive : Typeable !-}
f6cea53c107f81a3f3225481f1673452e29c555cChristian Maeder{-! for ThmLinkStatus derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for DGLinkType derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for Conservativity derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for DGOrigin derive : Typeable !-}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder{-! for NodeSig derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for MaybeNode derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for UnitSig derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for ImpUnitSigOrSig derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for ArchSig derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for GlobalEntry derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for DGChange derive : Typeable !-}
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder{-! for GlobalContext derive : Typeable !-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder_tc_G_theoryTc :: TyCon
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder_tc_G_theoryTc = mkTyCon "G_theory"
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maederinstance Typeable G_theory where
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder typeOf _ = mkTyConApp _tc_G_theoryTc []
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maederinstance ShATermConvertible BasicProof where
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder toShATermAux att0 (BasicProof lid p) = do
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att2,i2) <- toShATerm' att1 p
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1,i2] []) att2
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder toShATermAux att0 o = do
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att1, i1) <- toShATerm' att0 (show o)
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1] []) att1
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder fromShATermAux ix att =
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder case getShATerm ix att of
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder ShAAppl "BasicProof" [i1,i2] _ ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder case atcLogicLookup "BasicProof" i1' of { Logic lid ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att2, BasicProof lid i2') }}}
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder v@(ShAAppl "BasicProof" [i1] _) ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att1, case i1' of
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder "Guessed" -> Guessed
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder "Conjectured" -> Conjectured
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder "Handwritten" -> Handwritten
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder _ -> fromShATermError "BasicProof" v)}
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder u -> fromShATermError "BasicProof" u
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maederinstance ShATermConvertible G_theory where
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder toShATermAux att0 (G_theory lid sign sens) = do
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
e935c1f2e814bb143017bb25b32ff7a406299d37Christian Maeder (att2,i2) <- toShATerm' att1 sign
(att3,i3) <- toShATerm' att2 sens
return $ addATerm (ShAAppl "G_theory" [i1,i2,i3] []) att3
fromShATermAux ix att =
case getShATerm ix att of
ShAAppl "G_theory" [i1,i2,i3] _ ->
case fromShATerm' i1 att of { (att1, i1') ->
case atcLogicLookup "G_theory" i1' of { Logic lid ->
case fromShATerm' i2 att1 of { (att2, i2') ->
case fromShATerm' i3 att2 of { (att3, i3') ->
(att3, G_theory lid i2' i3') }}}}
u -> fromShATermError "G_theory" u