Grothendieck.der.hs

{-# LANGUAGE UndecidableInstances #-}
{- |
Module      :  $Header$
Description :  manually created ShATermConvertible instances
Copyright   :  (c) Felix Reckers, C. Maeder, Uni Bremen 2002-2006
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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.LibName
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 !-}
{-! for Common.LibName.LinkPath derive : ShATermLG !-}

atcLogicLookup :: LogicGraph -> String -> String -> AnyLogic
atcLogicLookup lg s l =
  propagateErrors $ 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 ShATermConvertible 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 $ 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 $ 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 sign si sens ti) = do
         (att1,i1) <- toShATermLG' att0 (language_name lid)
         (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,i2,i3,i4,i5] []) att5
  fromShATermLG lg ix att =
         case getShATerm ix att of
            ShAAppl "G_theory" [i1,i2,i3,i4,i5] _ ->
                case fromShATermLG' lg i1 att of { (att1, i1') ->
                case atcLogicLookup lg "G_theory" i1' of { Logic lid ->
                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 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