Grothendieck.hs revision 556f473448dfcceee22afaa89ed7a364489cdbbb
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : manually created ShATermConvertible instances
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Felix Reckers, C. Maeder, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (existential types)
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski'ShATermConvertible' instances for data types from "Logic.Grothendieck"
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiatcLogicLookup :: String -> String -> AnyLogic
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangatcLogicLookup s = lookupLogic_in_LG $ "ShATermConvertible " ++ s ++ ":"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederinstance ShATermConvertible SigId where
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder toShATermAux att0 (SigId a) = do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (att1, a') <- toShATerm' att0 a
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return $ addATerm (ShAAppl "SigId" [a'] []) att1
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder fromShATermAux ix att0 =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder case getShATerm ix att0 of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ShAAppl "SigId" [a] _ ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case fromShATerm' a att0 of { (att1, a') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att1, SigId a') }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder u -> fromShATermError "SigId" u
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance ShATermConvertible MorId where
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich toShATermAux att0 (MorId a) = do
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (att1, a') <- toShATerm' att0 a
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich return $ addATerm (ShAAppl "MorId" [a'] []) att1
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich fromShATermAux ix att0 =
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich case getShATerm ix att0 of
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ShAAppl "MorId" [a] _ ->
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich case fromShATerm' a att0 of { (att1, a') ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att1, MorId a') }
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder u -> fromShATermError "MorId" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible ThId where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder toShATermAux att0 (ThId a) = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (att1, a') <- toShATerm' att0 a
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu return $ addATerm (ShAAppl "ThId" [a'] []) att1
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski fromShATermAux ix att0 =
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski case getShATerm ix att0 of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ShAAppl "ThId" [a] _ ->
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder case fromShATerm' a att0 of { (att1, a') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1, ThId a') }
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder u -> fromShATermError "ThId" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible G_basic_spec where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder toShATermAux att0 (G_basic_spec lid basic_spec) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2,i2) <- toShATerm' att1 basic_spec
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ addATerm (ShAAppl "G_basic_spec" [i1,i2] []) att2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder fromShATermAux ix att =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder case getShATerm ix att of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ShAAppl "G_basic_spec" [i1,i2] _ ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case atcLogicLookup "G_basic_spec" i1' of { Logic lid ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2, G_basic_spec lid i2') }}}
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder u -> fromShATermError "G_basic_spec" u
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance ShATermConvertible G_sign where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski toShATermAux att0 (G_sign lid sign si) = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2,i2) <- toShATerm' att1 sign
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att3,i3) <- toShATerm' att2 si
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ addATerm (ShAAppl "G_sign" [i1,i2,i3] []) att3
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder fromShATermAux ix att =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case getShATerm ix att of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ShAAppl "G_sign" [i1,i2,i3] _ ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder case atcLogicLookup "G_sign" i1' of { Logic lid ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case fromShATerm' i3 att2 of { (att3, i3') ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att3, G_sign lid i2' i3') }}}}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski u -> fromShATermError "G_sign" u
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance ShATermConvertible G_symbol where
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder toShATermAux att0 (G_symbol lid symbol) = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2,i2) <- toShATerm' att1 symbol
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return $ addATerm (ShAAppl "G_symbol" [i1,i2] []) att2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder fromShATermAux ix att =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case getShATerm ix att of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder ShAAppl "G_symbol" [i1,i2] _ ->
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case atcLogicLookup "G_symbol" i1' of { Logic lid ->
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2, G_symbol lid i2') }}}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder u -> fromShATermError "G_symbol" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible G_symb_items_list where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder toShATermAux att0 (G_symb_items_list lid symb_items) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (att2,i2) <- toShATerm' att1 symb_items
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ addATerm (ShAAppl "G_symb_items_list" [i1,i2] []) att2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fromShATermAux ix att =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case getShATerm ix att of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ShAAppl "G_symb_items_list" [i1,i2] _ ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case atcLogicLookup "G_symb_items_list" i1' of { Logic lid ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att2, G_symb_items_list lid i2') }}}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder u -> fromShATermError "G_symb_items_list" u
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance ShATermConvertible G_symb_map_items_list where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder toShATermAux att0 (G_symb_map_items_list lid symb_map_items) = do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2,i2) <- toShATerm' att1 symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ addATerm (ShAAppl "G_symb_map_items_list" [i1,i2] []) att2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fromShATermAux ix att =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case getShATerm ix att of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski ShAAppl "G_symb_map_items_list" [i1,i2] _ ->
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case atcLogicLookup "G_symb_map_items_list" i1'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder of { Logic lid ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att2, G_symb_map_items_list lid i2') }}}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder u -> fromShATermError "G_symb_map_items_list" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible G_sublogics where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder toShATermAux att0 (G_sublogics lid sublogics) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (att2,i2) <- toShATerm' att1 sublogics
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ addATerm (ShAAppl "G_sublogics" [i1,i2] []) att2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fromShATermAux ix att =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case getShATerm ix att of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ShAAppl "G_sublogics" [i1,i2] _ ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case atcLogicLookup "G_sublogics" i1' of { Logic lid ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case fromShATerm' i2 att1 of { (att2, i2') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att2, G_sublogics lid i2') }}}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski u -> fromShATermError "G_sublogics" u
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance ShATermConvertible G_morphism where
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder toShATermAux att0 (G_morphism lid morphism mi) = do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att2,i2) <- toShATerm' att1 morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att3,i3) <- toShATerm' att2 mi
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ addATerm (ShAAppl "G_morphism" [i1,i2,i3] []) att3
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fromShATermAux ix att =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case getShATerm ix att of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ShAAppl "G_morphism" [i1,i2,i3] _ ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case atcLogicLookup "G_morphism" i1' of { Logic lid ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (att3, G_morphism lid i2' i3') }}}}
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder u -> fromShATermError "G_morphism" u
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance ShATermConvertible AnyComorphism where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder toShATermAux att0 (Comorphism cid) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att1,i1) <- toShATerm' att0 (language_name cid)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ addATerm (ShAAppl "Comorphism" [i1] []) att1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fromShATermAux ix att =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case getShATerm ix att of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ShAAppl "Comorphism" [i1] _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (att1, propagateErrors $ lookupComorphism_in_LG i1')}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder u -> fromShATermError "AnyComorphism" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible GMorphism where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder toShATermAux att0 (GMorphism cid sign1 si morphism2 mi) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1,i1) <- toShATerm' att0 (language_name cid)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att2,i2) <- toShATerm' att1 sign1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (att3,i3) <- toShATerm' att2 si
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att4,i4) <- toShATerm' att3 morphism2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att5,i5) <- toShATerm' att4 mi
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder return $ addATerm (ShAAppl "GMorphism" [i1,i2,i3,i4,i5] []) att5
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder fromShATermAux ix att =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case getShATerm ix att of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ShAAppl "GMorphism" [i1,i2,i3,i4,i5] _ ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder case propagateErrors $ lookupComorphism_in_LG i1'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder of { Comorphism cid ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case fromShATerm' i4 att3 of { (att4, i4') ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder case fromShATerm' i5 att4 of { (att5, i5') ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (att5, GMorphism cid i2' i3' i4' i5') }}}}}}
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian Maeder u -> fromShATermError "GMorphism" u
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance ShATermConvertible Grothendieck where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder toShATermAux att0 Grothendieck =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ addATerm (ShAAppl "Grothendieck" [] []) att0
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fromShATermAux ix att = case getShATerm ix att of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ShAAppl "Grothendieck" [] _ -> (att, Grothendieck)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder u -> fromShATermError "Grothendiek" u
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance ShATermConvertible AnyLogic where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski toShATermAux att0 (Logic lid) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ addATerm (ShAAppl "Logic" [i1] []) att1
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder fromShATermAux ix att =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case getShATerm ix att of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ShAAppl "Logic" [i1] _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (att1, atcLogicLookup "AnyLogic" i1') }
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder u -> fromShATermError "AnyLogic" u
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance ShATermConvertible BasicProof where
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder toShATermAux att0 (BasicProof lid p) = do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att2,i2) <- toShATerm' att1 p
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1,i2] []) att2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder toShATermAux att0 o = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att1, i1) <- toShATerm' att0 (show o)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1] []) att1
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder fromShATermAux ix att =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case getShATerm ix att of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder ShAAppl "BasicProof" [i1,i2] _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case atcLogicLookup "BasicProof" i1' of { Logic lid ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (att2, BasicProof lid i2') }}}
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder v@(ShAAppl "BasicProof" [i1] _) ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att1, case i1' of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "Guessed" -> Guessed
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "Conjectured" -> Conjectured
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "Handwritten" -> Handwritten
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> fromShATermError "BasicProof" v)}
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder u -> fromShATermError "BasicProof" u
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance ShATermConvertible G_theory where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder toShATermAux att0 (G_theory lid sign si sens ti) = do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (att2,i2) <- toShATerm' att1 sign
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (att3,i3) <- toShATerm' att2 si
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (att4,i4) <- toShATerm' att3 sens
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (att5,i5) <- toShATerm' att4 ti
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ addATerm (ShAAppl "G_theory" [i1,i2,i3,i4,i5] []) att5
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder fromShATermAux ix att =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case getShATerm ix att of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ShAAppl "G_theory" [i1,i2,i3,i4,i5] _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case atcLogicLookup "G_theory" i1' of { Logic lid ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case fromShATerm' i4 att3 of { (att4, i4') ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case fromShATerm' i5 att4 of { (att5, i5') ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (att5, G_theory lid i2' i3' i4' i5') }}}}}}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder u -> fromShATermError "G_theory" u
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Typeable a => ShATermConvertible (MVar a) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder toShATermAux att0 _ = return $ addATerm (ShAAppl "MVar" [] []) att0
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fromShATermAux ix att = case getShATerm ix att of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ShAAppl "MVar" [] _ -> (att, error "ShATermConvertible MVar")
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder u -> fromShATermError "MVar" u