c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances #-}

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : ./ATC/Grothendieck.der.hs

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiDescription : manually created ShATermConvertible instances

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

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederMaintainer : Christian.Maeder@dfki.de

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederStability : provisional

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederPortability : non-portable (existential types)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule ATC.Grothendieck where

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Logic.Logic

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Logic.Comorphism

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Logic.Grothendieck

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport ATerm.AbstractSyntax

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport ATerm.Conversion

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.AS_Annotation

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Common.GlobalAnnotations

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Lib.Graph

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.LibName

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.OrderedMap

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport qualified Common.Lib.SizedList as SizedList

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Common.Result

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport ATC.GlobalAnnotations ()

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport ATC.Graph ()

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport ATC.LibName ()

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Logic.Prover

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Data.Typeable

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Data.List

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport qualified Data.IntMap as IntMap

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport qualified Data.Map as Map

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport qualified Data.Set as Set

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport ATC.Prover ()

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport ATC.ExtSign ()

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maederimport Static.GTheory

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Control.Monad

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Control.Concurrent.MVar

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder{-! for Common.AS_Annotation.SenAttr derive : ShATermLG !-}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder{-! for Common.AS_Annotation.Annoted derive : ShATermLG !-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder{-! for Logic.Prover.ThmStatus derive : ShATermLG !-}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder{-! for Common.GlobalAnnotations.GlobalAnnos derive : ShATermLG !-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder{-! for Common.Lib.Graph.Gr derive : ShATermLG !-}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder{-! for Common.Lib.Graph.GrContext derive : ShATermLG !-}

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder{-! for Common.OrderedMap.ElemWOrd derive : ShATermLG !-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder{-! for Common.LibName.LinkPath derive : ShATermLG !-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederatcLogicLookup :: LogicGraph -> String -> String -> AnyLogic

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederatcLogicLookup lg s l =

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder propagateErrors " atcLogicLookup"

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder $ lookupLogic ("ConvertibleLG " ++ s ++ ":") l lg

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- the same class as ShATermConvertible, but allowing a logic graph as input

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederclass Typeable t => ShATermLG t where

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder toShATermLG :: ATermTable -> t -> IO (ATermTable, Int)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, t)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedertoShATermLG' :: ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedertoShATermLG' att t = do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder k <- mkKey t

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder m <- getKey k att

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case m of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> do

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder (att1, i) <- toShATermLG att t

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder setKey k i att1

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just i -> return (att, i)

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederfromShATermLG' :: ShATermLG t => LogicGraph -> Int -> ATermTable

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -> (ATermTable, t)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederfromShATermLG' lg i att = case getATerm' i att of

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Just d -> (att, d)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder _ -> case fromShATermLG lg i att of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (attN, t) -> (setATerm' i t attN, t)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-- generic undecidable instance

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederinstance (ShATermConvertible a, Typeable a) => ShATermLG a where

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder toShATermLG = toShATermAux

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fromShATermLG _ = fromShATermAux

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance ShATermLG G_basic_spec where

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder toShATermLG att0 (G_basic_spec lid basic_spec) = do

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder (att2, i2) <- toShATermLG' att1 basic_spec

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

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder fromShATermLG lg ix att = case getShATerm ix att of

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder case atcLogicLookup lg "G_basic_spec" i1' of { Logic lid ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder (att2, G_basic_spec lid i2') }}}

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder u -> fromShATermError "G_basic_spec" u

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance ShATermLG G_sign where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder toShATermLG att0 (G_sign lid sign si) = do

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, i2) <- toShATermLG' att1 sign

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder (att3, i3) <- toShATermLG' att2 si

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ShAAppl "G_sign" [i1, i2, i3] _ ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case atcLogicLookup lg "G_sign" i1' of { Logic lid ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i3 att2 of { (att3, i3') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att3, G_sign lid i2' i3') }}}}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder u -> fromShATermError "G_sign" u

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance ShATermLG G_symbol where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder toShATermLG att0 (G_symbol lid symbol) = do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, i2) <- toShATermLG' att1 symbol

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return $ addATerm (ShAAppl "G_symbol" [i1, i2] []) att2

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case atcLogicLookup lg "G_symbol" i1' of { Logic lid ->

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, G_symbol lid i2') }}}

fc816c737e569f135d8e2f79fc83521c85fae667Christian Maeder u -> fromShATermError "G_symbol" u

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance (Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) where

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder toShATermLG att0 (G_symbolmap lid m) = do

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder (att2, i2) <- toShATermLG' att1 m

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder return $ addATerm (ShAAppl "G_symbolmap" [i1, i2] []) att2

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder ShAAppl "G_symbolmap" [i1, i2] _ ->

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case atcLogicLookup lg "G_symbolmap" i1' of { Logic lid ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, G_symbolmap lid i2') }}}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder u -> fromShATermError "G_symbolmap" u

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance (Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) where

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder toShATermLG att0 (G_mapofsymbol lid m) = do

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (att2, i2) <- toShATermLG' att1 m

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder return $ addATerm (ShAAppl "G_mapofsymbol" [i1, i2] []) att2

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ShAAppl "G_mapofsymbol" [i1, i2] _ ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case atcLogicLookup lg "G_mapofsymbol" i1' of { Logic lid ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder (att2, G_mapofsymbol lid i2') }}}

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder u -> fromShATermError "G_mapofsymbol" u

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance ShATermLG G_symb_items_list where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder toShATermLG att0 (G_symb_items_list lid symb_items) = do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, i2) <- toShATermLG' att1 symb_items

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

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

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

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

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

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

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder u -> fromShATermError "G_symb_items_list" u

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederinstance ShATermLG G_symb_map_items_list where

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder toShATermLG att0 (G_symb_map_items_list lid symb_map_items) = do

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (att2, i2) <- toShATermLG' att1 symb_map_items

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

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

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

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case atcLogicLookup lg "G_symb_map_items_list" i1'

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder of { Logic lid ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (att2, G_symb_map_items_list lid i2') }}}

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder u -> fromShATermError "G_symb_map_items_list" u

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederinstance ShATermLG G_sublogics where

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder toShATermLG att0 (G_sublogics lid sublogics) = do

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (att2, i2) <- toShATermLG' att1 sublogics

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return $ addATerm (ShAAppl "G_sublogics" [i1, i2] []) att2

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder fromShATermLG lg ix att = case getShATerm ix att of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ShAAppl "G_sublogics" [i1, i2] _ ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case fromShATermLG' lg i1 att of { (att1, i1') ->

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case atcLogicLookup lg "G_sublogics" i1' of { Logic lid ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder case fromShATermLG' lg i2 att1 of { (att2, i2') ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (att2, G_sublogics lid i2') }}}

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder u -> fromShATermError "G_sublogics" u

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederinstance ShATermLG G_morphism where

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder toShATermLG att0 (G_morphism lid morphism mi) = do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att1, i1) <- toShATermLG' att0 (language_name lid)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (att2, i2) <- toShATermLG' att1 morphism

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder (att3, i3) <- toShATermLG' att2 mi

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fromShATermLG lg ix att = case getShATerm ix att of

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

case fromShATermLG' lg i1 att of { (att1, i1') ->

case atcLogicLookup lg "G_morphism" i1' of { Logic lid ->

case fromShATermLG' lg i2 att1 of { (att2, i2') ->

case fromShATermLG' lg i3 att2 of { (att3, i3') ->

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

u -> fromShATermError "G_morphism" u

instance ShATermLG AnyComorphism where

toShATermLG att0 (Comorphism cid) = do

(att1, i1) <- toShATermLG' att0 (language_name cid)

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

fromShATermLG lg ix att =

case getShATerm ix att of

ShAAppl "Comorphism" [i1] _ ->

case fromShATermLG' lg i1 att of { (att1, i1') ->

(att1, propagateErrors "ATC.Grothendieck.AnyComorphism"

$ lookupComorphism i1' lg)}

u -> fromShATermError "AnyComorphism" u

instance ShATermLG GMorphism where

toShATermLG att0 (GMorphism cid sign1 si morphism2 mi) = do

(att1, i1) <- toShATermLG' att0 (language_name cid)

(att2, i2) <- toShATermLG' att1 sign1

(att3, i3) <- toShATermLG' att2 si

(att4, i4) <- toShATermLG' att3 morphism2

(att5, i5) <- toShATermLG' att4 mi

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

fromShATermLG lg ix att =

case getShATerm ix att of

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

case fromShATermLG' lg i1 att of { (att1, i1') ->

case propagateErrors "ATC.Grothendieck.GMorphism"

$ lookupComorphism i1' lg of { Comorphism cid ->

case fromShATermLG' lg i2 att1 of { (att2, i2') ->

case fromShATermLG' lg i3 att2 of { (att3, i3') ->

case fromShATermLG' lg i4 att3 of { (att4, i4') ->

case fromShATermLG' lg i5 att4 of { (att5, i5') ->

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

u -> fromShATermError "GMorphism" u

instance ShATermLG AnyLogic where

toShATermLG att0 (Logic lid) = do

(att1, i1) <- toShATermLG' att0 (language_name lid)

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

fromShATermLG lg ix att = case getShATerm ix att of

ShAAppl "Logic" [i1] _ ->

case fromShATermLG' lg i1 att of { (att1, i1') ->

(att1, atcLogicLookup lg "AnyLogic" i1') }

u -> fromShATermError "AnyLogic" u

instance ShATermLG BasicProof where

toShATermLG att0 (BasicProof lid p) = do

(att1, i1) <- toShATermLG' att0 (language_name lid)

(att2, i2) <- toShATermLG' att1 p

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

toShATermLG att0 o = do

(att1, i1) <- toShATermLG' att0 (show o)

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

fromShATermLG lg ix att = case getShATerm ix att of

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

case fromShATermLG' lg i1 att of { (att1, i1') ->

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

case fromShATermLG' lg i2 att1 of { (att2, i2') ->

(att2, BasicProof lid i2') }}}

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

case fromShATermLG' lg i1 att of { (att1, i1') ->

(att1, case i1' of

"Guessed" -> Guessed

"Conjectured" -> Conjectured

"Handwritten" -> Handwritten

_ -> fromShATermError "BasicProof" v)}

u -> fromShATermError "BasicProof" u

instance (ShATermLG a) => ShATermLG (Maybe a) where

toShATermLG att mb = case mb of

Nothing -> return $ addATerm (ShAAppl "N" [] []) att

Just x -> do

(att1, x') <- toShATermLG' att x

return $ addATerm (ShAAppl "J" [x'] []) att1

fromShATermLG lg ix att0 =

case getShATerm ix att0 of

ShAAppl "N" [] _ -> (att0, Nothing)

ShAAppl "J" [a] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

(att1, Just a') }

u -> fromShATermError "Prelude.Maybe" u

instance ShATermLG a => ShATermLG [a] where

toShATermLG att ts = do

(att2, inds) <- foldM (\ (att0, l) t -> do

(att1, i) <- toShATermLG' att0 t

return (att1, i : l)) (att, []) ts

return $ addATerm (ShAList (reverse inds) []) att2

fromShATermLG lg ix att0 =

case getShATerm ix att0 of

ShAList ats _ ->

mapAccumL (flip $ fromShATermLG' lg ) att0 ats

u -> fromShATermError "[]" u

instance (ShATermLG a, ShATermLG b) => ShATermLG (a, b) where

toShATermLG att0 (x, y) = do

(att1, x') <- toShATermLG' att0 x

(att2, y') <- toShATermLG' att1 y

return $ addATerm (ShAAppl "" [x', y'] []) att2

fromShATermLG lg ix att0 = case getShATerm ix att0 of

ShAAppl "" [a, b] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

case fromShATermLG' lg b att1 of { (att2, b') ->

(att2, (a', b'))}}

u -> fromShATermError "(,)" u

instance (ShATermLG a, ShATermLG b, ShATermLG c) => ShATermLG (a, b, c) where

toShATermLG att0 (x, y, z) = do

(att1, x') <- toShATermLG' att0 x

(att2, y') <- toShATermLG' att1 y

(att3, z') <- toShATermLG' att2 z

return $ addATerm (ShAAppl "" [x', y', z'] []) att3

fromShATermLG lg ix att0 = case getShATerm ix att0 of

ShAAppl "" [a, b, c] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

case fromShATermLG' lg b att1 of { (att2, b') ->

case fromShATermLG' lg c att2 of { (att3, c') ->

(att3, (a', b', c'))}}}

u -> fromShATermError "(,,)" u

instance (Ord a, ShATermLG a) => ShATermLG (Set.Set a) where

toShATermLG att set = do

(att1, i) <- toShATermLG' att $ Set.toList set

return $ addATerm (ShAAppl "Set" [i] []) att1

fromShATermLG lg ix att0 =

case getShATerm ix att0 of

ShAAppl "Set" [a] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

(att1, Set.fromDistinctAscList a') }

u -> fromShATermError "Set.Set" u

instance ShATermLG a => ShATermLG (SizedList.SizedList a) where

toShATermLG att0 = toShATermLG att0 . SizedList.toList

fromShATermLG lg ix att0 = case fromShATermLG lg ix att0 of

(att, l) -> (att, SizedList.fromList l)

instance (Ord a, ShATermLG a, ShATermLG b) => ShATermLG (Map.Map a b) where

toShATermLG att fm = do

(att1, i) <- toShATermLG' att $ Map.toList fm

return $ addATerm (ShAAppl "Map" [i] []) att1

fromShATermLG lg ix att0 = case getShATerm ix att0 of

ShAAppl "Map" [a] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

(att1, Map.fromDistinctAscList a') }

u -> fromShATermError "Map.Map" u

instance (ShATermLG a) => ShATermLG (IntMap.IntMap a) where

toShATermLG att fm = do

(att1, i) <- toShATermLG' att $ IntMap.toList fm

return $ addATerm (ShAAppl "IntMap" [i] []) att1

fromShATermLG lg ix att0 = case getShATerm ix att0 of

ShAAppl "IntMap" [a] _ ->

case fromShATermLG' lg a att0 of { (att1, a') ->

(att1, IntMap.fromDistinctAscList a') }

u -> fromShATermError "IntMap.IntMap" u

instance ShATermLG G_theory where

toShATermLG att0 (G_theory lid syn sign si sens ti) = do

(att1a, i1) <- toShATermLG' att0 (language_name lid)

(att1, i1a) <- toShATermLG' att1a syn

(att2, i2) <- toShATermLG' att1 sign

(att3, i3) <- toShATermLG' att2 si

(att4, i4) <- toShATermLG' att3 sens

(att5, i5) <- toShATermLG' att4 ti

return $ addATerm (ShAAppl "G_theory" [i1, i1a, i2, i3, i4, i5] [])

att5

fromShATermLG lg ix att =

case getShATerm ix att of

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

case fromShATermLG' lg i1 att of { (att1a, i1') ->

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

case fromShATermLG' lg i1a att1a of { (att1, i1a') ->

case fromShATermLG' lg i2 att1 of { (att2, i2') ->

case fromShATermLG' lg i3 att2 of { (att3, i3') ->

case fromShATermLG' lg i4 att3 of { (att4, i4') ->

case fromShATermLG' lg i5 att4 of { (att5, i5') ->

(att5, G_theory lid i1a' i2' i3' i4' i5') }}}}}}}

u -> fromShATermError "G_theory" u

instance Typeable a => ShATermConvertible (MVar a) where

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

fromShATermAux ix att = case getShATerm ix att of

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

u -> fromShATermError "MVar" u