abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{- |

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$

09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : manually created ShATermConvertible instances

76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Felix Reckers, C. Maeder, Uni Bremen 2002-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional

76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : non-portable (existential types)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder'ShATermConvertible' instances for data types from "Logic.Grothendieck"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-}

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule ATC.Grothendieck where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Logic.Grothendieck

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.ATerm.Lib

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport Data.Typeable

0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Common.Result

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Comorphisms.LogicList

0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Comorphisms.LogicGraph

d48085f765fca838c1d972d2123601997174583dChristian Maederimport Logic.Logic

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport ATC.Prover ()

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport ATC.ExtSign ()

0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Static.GTheory

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederimport Control.Concurrent.MVar

d48085f765fca838c1d972d2123601997174583dChristian Maeder

76647324ed70f33b95a881b536d883daccf9568dChristian MaederatcLogicLookup :: String -> String -> AnyLogic

d48085f765fca838c1d972d2123601997174583dChristian MaederatcLogicLookup s = lookupLogic_in_LG $ "ShATermConvertible " ++ s ++ ":"

d48085f765fca838c1d972d2123601997174583dChristian Maeder

76647324ed70f33b95a881b536d883daccf9568dChristian Maederinstance ShATermConvertible SigId where

d48085f765fca838c1d972d2123601997174583dChristian Maeder toShATermAux att0 (SigId a) = do

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att1, a') <- toShATerm' att0 a

d48085f765fca838c1d972d2123601997174583dChristian Maeder return $ addATerm (ShAAppl "SigId" [a'] []) att1

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att0 =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att0 of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "SigId" [a] _ ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' a att0 of { (att1, a') ->

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att1, SigId a') }

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder u -> fromShATermError "SigId" u

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder

a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance ShATermConvertible MorId where

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder toShATermAux att0 (MorId a) = do

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att1, a') <- toShATerm' att0 a

d48085f765fca838c1d972d2123601997174583dChristian Maeder return $ addATerm (ShAAppl "MorId" [a'] []) att1

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att0 =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att0 of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "MorId" [a] _ ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' a att0 of { (att1, a') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att1, MorId a') }

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder u -> fromShATermError "MorId" u

a716971174535184da7713ed308423e355a4aa66Christian Maeder

793945d4ac7c0f22760589c87af8e71427c76118Christian Maederinstance ShATermConvertible ThId where

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder toShATermAux att0 (ThId a) = do

5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder (att1, a') <- toShATerm' att0 a

feab655b0275874012c3cf9859064c177860cc70Christian Maeder return $ addATerm (ShAAppl "ThId" [a'] []) att1

f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder fromShATermAux ix att0 =

f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder case getShATerm ix att0 of

f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder ShAAppl "ThId" [a] _ ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder case fromShATerm' a att0 of { (att1, a') ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (att1, ThId a') }

a716971174535184da7713ed308423e355a4aa66Christian Maeder u -> fromShATermError "ThId" u

a716971174535184da7713ed308423e355a4aa66Christian Maeder

5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maederinstance ShATermConvertible G_basic_spec where

a716971174535184da7713ed308423e355a4aa66Christian Maeder toShATermAux att0 (G_basic_spec lid basic_spec) = do

a716971174535184da7713ed308423e355a4aa66Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

a716971174535184da7713ed308423e355a4aa66Christian Maeder (att2,i2) <- toShATerm' att1 basic_spec

a716971174535184da7713ed308423e355a4aa66Christian Maeder return $ addATerm (ShAAppl "G_basic_spec" [i1,i2] []) att2

5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder fromShATermAux ix att =

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder case getShATerm ix att of

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder ShAAppl "G_basic_spec" [i1,i2] _ ->

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder case atcLogicLookup "G_basic_spec" i1' of { Logic lid ->

9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder (att2, G_basic_spec lid i2') }}}

9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder u -> fromShATermError "G_basic_spec" u

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maederinstance ShATermConvertible G_sign where

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder toShATermAux att0 (G_sign lid sign si) = do

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder (att2,i2) <- toShATerm' att1 sign

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder (att3,i3) <- toShATerm' att2 si

ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder return $ addATerm (ShAAppl "G_sign" [i1,i2,i3] []) att3

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ShAAppl "G_sign" [i1,i2,i3] _ ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder case atcLogicLookup "G_sign" i1' of { Logic lid ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (att3, G_sign lid i2' i3') }}}}

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder u -> fromShATermError "G_sign" u

a716971174535184da7713ed308423e355a4aa66Christian Maeder

a716971174535184da7713ed308423e355a4aa66Christian Maederinstance ShATermConvertible G_symbol where

a716971174535184da7713ed308423e355a4aa66Christian Maeder toShATermAux att0 (G_symbol lid symbol) = do

67a14e04c885a87e4273a300eef60e680531088cChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

67a14e04c885a87e4273a300eef60e680531088cChristian Maeder (att2,i2) <- toShATerm' att1 symbol

67a14e04c885a87e4273a300eef60e680531088cChristian Maeder return $ addATerm (ShAAppl "G_symbol" [i1,i2] []) att2

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "G_symbol" [i1,i2] _ ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder case atcLogicLookup "G_symbol" i1' of { Logic lid ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att2, G_symbol lid i2') }}}

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder u -> fromShATermError "G_symbol" u

d48085f765fca838c1d972d2123601997174583dChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maederinstance ShATermConvertible G_symb_items_list where

d48085f765fca838c1d972d2123601997174583dChristian Maeder toShATermAux att0 (G_symb_items_list lid symb_items) = do

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att2,i2) <- toShATerm' att1 symb_items

d48085f765fca838c1d972d2123601997174583dChristian Maeder return $ addATerm (ShAAppl "G_symb_items_list" [i1,i2] []) att2

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "G_symb_items_list" [i1,i2] _ ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case atcLogicLookup "G_symb_items_list" i1' of { Logic lid ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att2, G_symb_items_list lid i2') }}}

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder u -> fromShATermError "G_symb_items_list" u

d48085f765fca838c1d972d2123601997174583dChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maederinstance ShATermConvertible G_symb_map_items_list where

d48085f765fca838c1d972d2123601997174583dChristian Maeder toShATermAux att0 (G_symb_map_items_list lid symb_map_items) = do

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder (att2,i2) <- toShATerm' att1 symb_map_items

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder return $ addATerm (ShAAppl "G_symb_map_items_list" [i1,i2] []) att2

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "G_symb_map_items_list" [i1,i2] _ ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case atcLogicLookup "G_symb_map_items_list" i1'

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder of { Logic lid ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder (att2, G_symb_map_items_list lid i2') }}}

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder u -> fromShATermError "G_symb_map_items_list" u

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederinstance ShATermConvertible G_diagram where

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder toShATermAux att0 (G_diagram lid diagram) = do

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att2,i2) <- toShATerm' att1 diagram

d48085f765fca838c1d972d2123601997174583dChristian Maeder return $ addATerm (ShAAppl "G_diagram" [i1,i2] []) att2

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att =

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "G_diagram" [i1,i2] _ ->

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder case atcLogicLookup "G_diagram" i1' of { Logic lid ->

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att2, G_diagram lid i2') }}}

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder u -> fromShATermError "G_diagram" u

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederinstance ShATermConvertible G_sublogics where

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder toShATermAux att0 (G_sublogics lid sublogics) = do

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att2,i2) <- toShATerm' att1 sublogics

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return $ addATerm (ShAAppl "G_sublogics" [i1,i2] []) att2

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder fromShATermAux ix att =

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case getShATerm ix att of

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ShAAppl "G_sublogics" [i1,i2] _ ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder case atcLogicLookup "G_sublogics" i1' of { Logic lid ->

9a44a07ffc79da9852b6319bd6d9df81efe99809Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att2, G_sublogics lid i2') }}}

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder u -> fromShATermError "G_sublogics" u

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederinstance ShATermConvertible G_morphism where

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder toShATermAux att0 (G_morphism lid morphism mi) = do

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att2,i2) <- toShATerm' att1 morphism

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att3,i3) <- toShATerm' att2 mi

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder return $ addATerm (ShAAppl "G_morphism" [i1,i2,i3] []) att3

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "G_morphism" [i1,i2,i3] _ ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder case atcLogicLookup "G_morphism" i1' of { Logic lid ->

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att3, G_morphism lid i2' i3') }}}}

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder u -> fromShATermError "G_morphism" u

d48085f765fca838c1d972d2123601997174583dChristian Maeder

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederinstance ShATermConvertible AnyComorphism where

d48085f765fca838c1d972d2123601997174583dChristian Maeder toShATermAux att0 (Comorphism cid) = do

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att1,i1) <- toShATerm' att0 (language_name cid)

d48085f765fca838c1d972d2123601997174583dChristian Maeder return $ addATerm (ShAAppl "Comorphism" [i1] []) att1

d48085f765fca838c1d972d2123601997174583dChristian Maeder fromShATermAux ix att =

d48085f765fca838c1d972d2123601997174583dChristian Maeder case getShATerm ix att of

d48085f765fca838c1d972d2123601997174583dChristian Maeder ShAAppl "Comorphism" [i1] _ ->

d48085f765fca838c1d972d2123601997174583dChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (att1, propagateErrors $ lookupComorphism_in_LG i1')}

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder u -> fromShATermError "AnyComorphism" u

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance ShATermConvertible GMorphism where

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder toShATermAux att0 (GMorphism cid sign1 si morphism2 mi) = do

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att1,i1) <- toShATerm' att0 (language_name cid)

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att2,i2) <- toShATerm' att1 sign1

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att3,i3) <- toShATerm' att2 si

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att4,i4) <- toShATerm' att3 morphism2

d48085f765fca838c1d972d2123601997174583dChristian Maeder (att5,i5) <- toShATerm' att4 mi

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder return $ addATerm (ShAAppl "GMorphism" [i1,i2,i3,i4,i5] []) att5

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder fromShATermAux ix att =

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case getShATerm ix att of

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder ShAAppl "GMorphism" [i1,i2,i3,i4,i5] _ ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case propagateErrors $ lookupComorphism_in_LG i1'

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder of { Comorphism cid ->

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case fromShATerm' i4 att3 of { (att4, i4') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case fromShATerm' i5 att4 of { (att5, i5') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att5, GMorphism cid i2' i3' i4' i5') }}}}}}

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder u -> fromShATermError "GMorphism" u

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederinstance ShATermConvertible Grothendieck where

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder toShATermAux att0 Grothendieck =

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder return $ addATerm (ShAAppl "Grothendieck" [] []) att0

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder fromShATermAux ix att = case getShATerm ix att of

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ShAAppl "Grothendieck" [] _ -> (att, Grothendieck)

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder u -> fromShATermError "Grothendiek" u

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederinstance ShATermConvertible AnyLogic where

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder toShATermAux att0 (Logic lid) = do

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return $ addATerm (ShAAppl "Logic" [i1] []) att1

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder fromShATermAux ix att =

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder case getShATerm ix att of

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder ShAAppl "Logic" [i1] _ ->

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder (att1, atcLogicLookup "AnyLogic" i1') }

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder u -> fromShATermError "AnyLogic" u

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederinstance ShATermConvertible BasicProof where

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder toShATermAux att0 (BasicProof lid p) = do

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder (att2,i2) <- toShATerm' att1 p

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1,i2] []) att2

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder toShATermAux att0 o = do

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder (att1, i1) <- toShATerm' att0 (show o)

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder return $ addATerm (ShAAppl "BasicProof" [i1] []) att1

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder fromShATermAux ix att =

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder case getShATerm ix att of

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ShAAppl "BasicProof" [i1,i2] _ ->

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder case atcLogicLookup "BasicProof" i1' of { Logic lid ->

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder (att2, BasicProof lid i2') }}}

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder v@(ShAAppl "BasicProof" [i1] _) ->

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder case fromShATerm' i1 att of { (att1, i1') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att1, case i1' of

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder "Guessed" -> Guessed

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder "Conjectured" -> Conjectured

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder "Handwritten" -> Handwritten

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder _ -> fromShATermError "BasicProof" v)}

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder u -> fromShATermError "BasicProof" u

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederinstance ShATermConvertible G_theory where

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder toShATermAux att0 (G_theory lid sign si sens ti) = do

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder (att1,i1) <- toShATerm' att0 (language_name lid)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att2,i2) <- toShATerm' att1 sign

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att3,i3) <- toShATerm' att2 si

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att4,i4) <- toShATerm' att3 sens

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att5,i5) <- toShATerm' att4 ti

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return $ addATerm (ShAAppl "G_theory" [i1,i2,i3,i4,i5] []) att5

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder fromShATermAux ix att =

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case getShATerm ix att of

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder ShAAppl "G_theory" [i1,i2,i3,i4,i5] _ ->

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case fromShATerm' i1 att of { (att1, i1') ->

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case atcLogicLookup "G_theory" i1' of { Logic lid ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case fromShATerm' i2 att1 of { (att2, i2') ->

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case fromShATerm' i3 att2 of { (att3, i3') ->

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder case fromShATerm' i4 att3 of { (att4, i4') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case fromShATerm' i5 att4 of { (att5, i5') ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (att5, G_theory lid i2' i3' i4' i5') }}}}}}

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder u -> fromShATermError "G_theory" u

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederinstance Typeable a => ShATermConvertible (MVar a) where

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder toShATermAux att0 _ = return $ addATerm (ShAAppl "MVar" [] []) att0

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder fromShATermAux ix att = case getShATerm ix att of

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ShAAppl "MVar" [] _ -> (att, error "ShATermConvertible MVar")

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder u -> fromShATermError "MVar" u

19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder