content: {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE FlexibleInstances #-}
  {- |
  Module      :  ./ATC/Grothendieck.der.hs
  Description :  manually created ShATermConvertible instances
  Copyright   :  (c) Felix Reckers, C. Maeder, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (existential types)
  
  'ShATermConvertible' instances for data types from "Logic.Grothendieck"
  -}
  
  module ATC.Grothendieck where
  
  import Logic.Logic
  import Logic.Comorphism
  import Logic.Grothendieck
  
  import ATerm.AbstractSyntax
  import ATerm.Conversion
  import Common.AS_Annotation
  import Common.GlobalAnnotations
  import Common.Lib.Graph
  import Common.OrderedMap
  import qualified Common.Lib.SizedList as SizedList
  import Common.Result
  
  import ATC.GlobalAnnotations ()
  import ATC.Graph ()
  import ATC.LibName ()
  import Logic.Prover
  import Data.Typeable
  import Data.List
  import qualified Data.IntMap as IntMap
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import ATC.Prover ()
  import ATC.ExtSign ()
  import Static.GTheory
  
  import Control.Monad
  import Control.Concurrent.MVar
  
  {-! for Common.AS_Annotation.SenAttr derive : ShATermLG !-}
  {-! for Common.AS_Annotation.Annoted derive : ShATermLG !-}
  {-! for Logic.Prover.ThmStatus derive : ShATermLG !-}
  {-! for Common.GlobalAnnotations.GlobalAnnos derive : ShATermLG !-}
  {-! for Common.Lib.Graph.Gr derive : ShATermLG !-}
  {-! for Common.Lib.Graph.GrContext derive : ShATermLG !-}
  {-! for Common.OrderedMap.ElemWOrd derive : ShATermLG !-}
  
  atcLogicLookup :: LogicGraph -> String -> String -> AnyLogic
  atcLogicLookup lg s l =
    propagateErrors " atcLogicLookup"
    $ lookupLogic ("ConvertibleLG " ++ s ++ ":") l lg
  
  -- the same class as ShATermConvertible, but allowing a logic graph as input
  class Typeable t => ShATermLG t where
      toShATermLG :: ATermTable -> t -> IO (ATermTable, Int)
      fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, t)
  
  toShATermLG' :: ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
  toShATermLG' att t = do
         k <- mkKey t
         m <- getKey k att
         case m of
           Nothing -> do
             (att1, i) <- toShATermLG att t
             setKey k i att1
           Just i -> return (att, i)
  
  fromShATermLG' :: ShATermLG t => LogicGraph -> Int -> ATermTable
                 -> (ATermTable, t)
  fromShATermLG' lg i att = case getATerm' i att of
          Just d -> (att, d)
          _ -> case fromShATermLG lg i att of
                 (attN, t) -> (setATerm' i t attN, t)
  
  -- generic undecidable instance
  instance {-# OVERLAPS #-} (ShATermConvertible a, Typeable a) => ShATermLG a where
    toShATermLG = toShATermAux
    fromShATermLG _ = fromShATermAux
  
  instance ShATermLG G_basic_spec where
    toShATermLG att0 (G_basic_spec lid basic_spec) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 basic_spec
           return $ addATerm (ShAAppl "G_basic_spec" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_basic_spec" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_basic_spec" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_basic_spec lid i2') }}}
              u -> fromShATermError "G_basic_spec" u
  
  instance ShATermLG G_sign where
    toShATermLG att0 (G_sign lid sign si) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 sign
           (att3, i3) <- toShATermLG' att2 si
           return $ addATerm (ShAAppl "G_sign" [i1, i2, i3] []) att3
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_sign" [i1, i2, i3] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_sign" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  case fromShATermLG' lg i3 att2 of { (att3, i3') ->
                  (att3, G_sign lid i2' i3') }}}}
              u -> fromShATermError "G_sign" u
  
  instance ShATermLG G_symbol where
    toShATermLG att0 (G_symbol lid symbol) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 symbol
           return $ addATerm (ShAAppl "G_symbol" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_symbol" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_symbol" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_symbol lid i2') }}}
              u -> fromShATermError "G_symbol" u
  
  instance (Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) where
    toShATermLG att0 (G_symbolmap lid m) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 m
           return $ addATerm (ShAAppl "G_symbolmap" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_symbolmap" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_symbolmap" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_symbolmap lid i2') }}}
              u -> fromShATermError "G_symbolmap" u
  
  instance (Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) where
    toShATermLG att0 (G_mapofsymbol lid m) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 m
           return $ addATerm (ShAAppl "G_mapofsymbol" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_mapofsymbol" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_mapofsymbol" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_mapofsymbol lid i2') }}}
              u -> fromShATermError "G_mapofsymbol" u
  
  
  instance ShATermLG G_symb_items_list where
    toShATermLG att0 (G_symb_items_list lid symb_items) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 symb_items
           return $ addATerm (ShAAppl "G_symb_items_list" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_symb_items_list" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_symb_items_list" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_symb_items_list lid i2') }}}
              u -> fromShATermError "G_symb_items_list" u
  
  instance ShATermLG G_symb_map_items_list where
    toShATermLG att0 (G_symb_map_items_list lid symb_map_items) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 symb_map_items
           return $ addATerm (ShAAppl "G_symb_map_items_list" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_symb_map_items_list" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_symb_map_items_list" i1'
                  of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_symb_map_items_list lid i2') }}}
              u -> fromShATermError "G_symb_map_items_list" u
  
  instance ShATermLG G_sublogics where
    toShATermLG att0 (G_sublogics lid sublogics) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 sublogics
           return $ addATerm (ShAAppl "G_sublogics" [i1, i2] []) att2
    fromShATermLG lg ix att = case getShATerm ix att of
              ShAAppl "G_sublogics" [i1, i2] _ ->
                  case fromShATermLG' lg i1 att of { (att1, i1') ->
                  case atcLogicLookup lg "G_sublogics" i1' of { Logic lid ->
                  case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                  (att2, G_sublogics lid i2') }}}
              u -> fromShATermError "G_sublogics" u
  
  instance ShATermLG G_morphism where
    toShATermLG att0 (G_morphism lid morphism mi) = do
           (att1, i1) <- toShATermLG' att0 (language_name lid)
           (att2, i2) <- toShATermLG' att1 morphism
           (att3, i3) <- toShATermLG' att2 mi
           return $ addATerm (ShAAppl "G_morphism" [i1, i2, i3] []) att3
    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 {-# OVERLAPS #-} 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
  