{-# 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 :: LogicGraph -> String -> String -> AnyLogic
atcLogicLookup lg :: LogicGraph
lg s :: String
s l :: String
l =
  String -> Result AnyLogic -> AnyLogic
forall a. String -> Result a -> a
propagateErrors " atcLogicLookup"
  (Result AnyLogic -> AnyLogic) -> Result AnyLogic -> AnyLogic
forall a b. (a -> b) -> a -> b
$ String -> String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic ("ConvertibleLG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":") String
l LogicGraph
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' :: ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' att :: ATermTable
att t :: t
t = do
       Key
k <- t -> IO Key
forall a. Typeable a => a -> IO Key
mkKey t
t
       Maybe Int
m <- Key -> ATermTable -> IO (Maybe Int)
getKey Key
k ATermTable
att
       case Maybe Int
m of
         Nothing -> do
           (att1 :: ATermTable
att1, i :: Int
i) <- ATermTable -> t -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG ATermTable
att t
t
           Key -> Int -> ATermTable -> IO (ATermTable, Int)
setKey Key
k Int
i ATermTable
att1
         Just i :: Int
i -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATermTable
att, Int
i)

fromShATermLG' :: ShATermLG t => LogicGraph -> Int -> ATermTable
               -> (ATermTable, t)
fromShATermLG' :: LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' lg :: LogicGraph
lg i :: Int
i att :: ATermTable
att = case Int -> ATermTable -> Maybe t
forall t. Typeable t => Int -> ATermTable -> Maybe t
getATerm' Int
i ATermTable
att of
        Just d :: t
d -> (ATermTable
att, t
d)
        _ -> case LogicGraph -> Int -> ATermTable -> (ATermTable, t)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG LogicGraph
lg Int
i ATermTable
att of
               (attN :: ATermTable
attN, t :: t
t) -> (Int -> t -> ATermTable -> ATermTable
forall t. Typeable t => Int -> t -> ATermTable -> ATermTable
setATerm' Int
i t
t ATermTable
attN, t
t)

-- generic undecidable instance
instance {-# OVERLAPS #-} (ShATermConvertible a, Typeable a) => ShATermLG a where
  toShATermLG :: ATermTable -> a -> IO (ATermTable, Int)
toShATermLG = ATermTable -> a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATermAux
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, a)
fromShATermLG _ = Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATermAux

instance ShATermLG G_basic_spec where
  toShATermLG :: ATermTable -> G_basic_spec -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_basic_spec lid :: lid
lid basic_spec :: basic_spec
basic_spec) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> basic_spec -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 basic_spec
basic_spec
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_basic_spec" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_basic_spec)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_basic_spec" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_basic_spec" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, basic_spec)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: basic_spec
i2') ->
                (ATermTable
att2, lid -> basic_spec -> G_basic_spec
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> basic_spec -> G_basic_spec
G_basic_spec lid
lid basic_spec
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_basic_spec)
forall a. String -> ShATerm -> a
fromShATermError "G_basic_spec" ShATerm
u

instance ShATermLG G_sign where
  toShATermLG :: ATermTable -> G_sign -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_sign lid :: lid
lid sign :: ExtSign sign symbol
sign si :: SigId
si) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> ExtSign sign symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ExtSign sign symbol
sign
         (att3 :: ATermTable
att3, i3 :: Int
i3) <- ATermTable -> SigId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 SigId
si
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_sign" [Int
i1, Int
i2, Int
i3] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_sign)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_sign" [i1 :: Int
i1, i2 :: Int
i2, i3 :: Int
i3] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_sign" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph
-> Int -> ATermTable -> (ATermTable, ExtSign sign symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: ExtSign sign symbol
i2') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, SigId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i3 ATermTable
att2 of { (att3 :: ATermTable
att3, i3' :: SigId
i3') ->
                (ATermTable
att3, lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid ExtSign sign symbol
i2' SigId
i3') }}}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_sign)
forall a. String -> ShATerm -> a
fromShATermError "G_sign" ShATerm
u

instance ShATermLG G_symbol where
  toShATermLG :: ATermTable -> G_symbol -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_symbol lid :: lid
lid symbol :: symbol
symbol) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 symbol
symbol
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_symbol" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symbol)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_symbol" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_symbol" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: symbol
i2') ->
                (ATermTable
att2, lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
lid symbol
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_symbol)
forall a. String -> ShATerm -> a
fromShATermError "G_symbol" ShATerm
u

instance (Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) where
  toShATermLG :: ATermTable -> G_symbolmap a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_symbolmap lid :: lid
lid m :: Map symbol a
m) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> Map symbol a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Map symbol a
m
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_symbolmap" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symbolmap a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_symbolmap" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_symbolmap" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, Map symbol a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: Map symbol a
i2') ->
                (ATermTable
att2, lid -> Map symbol a -> G_symbolmap a
forall a lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map symbol a -> G_symbolmap a
G_symbolmap lid
lid Map symbol a
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_symbolmap a)
forall a. String -> ShATerm -> a
fromShATermError "G_symbolmap" ShATerm
u

instance (Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) where
  toShATermLG :: ATermTable -> G_mapofsymbol a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_mapofsymbol lid :: lid
lid m :: Map a symbol
m) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> Map a symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Map a symbol
m
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_mapofsymbol" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_mapofsymbol a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_mapofsymbol" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_mapofsymbol" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, Map a symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: Map a symbol
i2') ->
                (ATermTable
att2, lid -> Map a symbol -> G_mapofsymbol a
forall a lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map a symbol -> G_mapofsymbol a
G_mapofsymbol lid
lid Map a symbol
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_mapofsymbol a)
forall a. String -> ShATerm -> a
fromShATermError "G_mapofsymbol" ShATerm
u


instance ShATermLG G_symb_items_list where
  toShATermLG :: ATermTable -> G_symb_items_list -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_symb_items_list lid :: lid
lid symb_items :: [symb_items]
symb_items) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> [symb_items] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 [symb_items]
symb_items
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_symb_items_list" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symb_items_list)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_symb_items_list" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_symb_items_list" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, [symb_items])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: [symb_items]
i2') ->
                (ATermTable
att2, lid -> [symb_items] -> G_symb_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_items] -> G_symb_items_list
G_symb_items_list lid
lid [symb_items]
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_symb_items_list)
forall a. String -> ShATerm -> a
fromShATermError "G_symb_items_list" ShATerm
u

instance ShATermLG G_symb_map_items_list where
  toShATermLG :: ATermTable -> G_symb_map_items_list -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_symb_map_items_list lid :: lid
lid symb_map_items :: [symb_map_items]
symb_map_items) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> [symb_map_items] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 [symb_map_items]
symb_map_items
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_symb_map_items_list" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph
-> Int -> ATermTable -> (ATermTable, G_symb_map_items_list)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_symb_map_items_list" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_symb_map_items_list" String
i1'
                of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, [symb_map_items])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: [symb_map_items]
i2') ->
                (ATermTable
att2, lid -> [symb_map_items] -> G_symb_map_items_list
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list lid
lid [symb_map_items]
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_symb_map_items_list)
forall a. String -> ShATerm -> a
fromShATermError "G_symb_map_items_list" ShATerm
u

instance ShATermLG G_sublogics where
  toShATermLG :: ATermTable -> G_sublogics -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_sublogics lid :: lid
lid sublogics :: sublogics
sublogics) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> sublogics -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 sublogics
sublogics
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_sublogics" [Int
i1, Int
i2] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_sublogics)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_sublogics" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_sublogics" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, sublogics)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: sublogics
i2') ->
                (ATermTable
att2, lid -> sublogics -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics lid
lid sublogics
i2') }}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_sublogics)
forall a. String -> ShATerm -> a
fromShATermError "G_sublogics" ShATerm
u

instance ShATermLG G_morphism where
  toShATermLG :: ATermTable -> G_morphism -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_morphism lid :: lid
lid morphism :: morphism
morphism mi :: MorId
mi) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> morphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 morphism
morphism
         (att3 :: ATermTable
att3, i3 :: Int
i3) <- ATermTable -> MorId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 MorId
mi
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_morphism" [Int
i1, Int
i2, Int
i3] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_morphism)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_morphism" [i1 :: Int
i1, i2 :: Int
i2, i3 :: Int
i3] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_morphism" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, morphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: morphism
i2') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, MorId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i3 ATermTable
att2 of { (att3 :: ATermTable
att3, i3' :: MorId
i3') ->
                (ATermTable
att3, lid -> morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism lid
lid morphism
i2' MorId
i3') }}}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_morphism)
forall a. String -> ShATerm -> a
fromShATermError "G_morphism" ShATerm
u

instance ShATermLG AnyComorphism where
  toShATermLG :: ATermTable -> AnyComorphism -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (Comorphism cid :: cid
cid) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Comorphism" [Int
i1] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AnyComorphism)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att =
         case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "Comorphism" [i1 :: Int
i1] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                (ATermTable
att1, String -> Result AnyComorphism -> AnyComorphism
forall a. String -> Result a -> a
propagateErrors "ATC.Grothendieck.AnyComorphism"
                (Result AnyComorphism -> AnyComorphism)
-> Result AnyComorphism -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ String -> LogicGraph -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyComorphism
lookupComorphism String
i1' LogicGraph
lg)}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AnyComorphism)
forall a. String -> ShATerm -> a
fromShATermError "AnyComorphism" ShATerm
u

instance ShATermLG GMorphism where
  toShATermLG :: ATermTable -> GMorphism -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (GMorphism cid :: cid
cid sign1 :: ExtSign sign1 symbol1
sign1 si :: SigId
si morphism2 :: morphism2
morphism2 mi :: MorId
mi) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> ExtSign sign1 symbol1 -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ExtSign sign1 symbol1
sign1
         (att3 :: ATermTable
att3, i3 :: Int
i3) <- ATermTable -> SigId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 SigId
si
         (att4 :: ATermTable
att4, i4 :: Int
i4) <- ATermTable -> morphism2 -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 morphism2
morphism2
         (att5 :: ATermTable
att5, i5 :: Int
i5) <- ATermTable -> MorId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 MorId
mi
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "GMorphism" [Int
i1, Int
i2, Int
i3, Int
i4, Int
i5] []) ATermTable
att5
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att =
         case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "GMorphism" [i1 :: Int
i1, i2 :: Int
i2, i3 :: Int
i3, i4 :: Int
i4, i5 :: Int
i5] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case String -> Result AnyComorphism -> AnyComorphism
forall a. String -> Result a -> a
propagateErrors "ATC.Grothendieck.GMorphism"
                  (Result AnyComorphism -> AnyComorphism)
-> Result AnyComorphism -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ String -> LogicGraph -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyComorphism
lookupComorphism String
i1' LogicGraph
lg of { Comorphism cid :: cid
cid ->
                case LogicGraph
-> Int -> ATermTable -> (ATermTable, ExtSign sign1 symbol1)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: ExtSign sign1 symbol1
i2') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, SigId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i3 ATermTable
att2 of { (att3 :: ATermTable
att3, i3' :: SigId
i3') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, morphism2)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i4 ATermTable
att3 of { (att4 :: ATermTable
att4, i4' :: morphism2
i4') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, MorId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i5 ATermTable
att4 of { (att5 :: ATermTable
att5, i5' :: MorId
i5') ->
                (ATermTable
att5, cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid ExtSign sign1 symbol1
i2' SigId
i3' morphism2
i4' MorId
i5') }}}}}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GMorphism)
forall a. String -> ShATerm -> a
fromShATermError "GMorphism" ShATerm
u

instance ShATermLG AnyLogic where
  toShATermLG :: ATermTable -> AnyLogic -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (Logic lid :: lid
lid) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Logic" [Int
i1] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AnyLogic)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "Logic" [i1 :: Int
i1] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                (ATermTable
att1, LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "AnyLogic" String
i1') }
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AnyLogic)
forall a. String -> ShATerm -> a
fromShATermError "AnyLogic" ShATerm
u

instance ShATermLG BasicProof where
  toShATermLG :: ATermTable -> BasicProof -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (BasicProof lid :: lid
lid p :: ProofStatus proof_tree
p) = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> ProofStatus proof_tree -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ProofStatus proof_tree
p
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BasicProof" [Int
i1, Int
i2] []) ATermTable
att2
  toShATermLG att0 :: ATermTable
att0 o :: BasicProof
o = do
         (att1 :: ATermTable
att1, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (BasicProof -> String
forall a. Show a => a -> String
show BasicProof
o)
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BasicProof" [Int
i1] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, BasicProof)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "BasicProof" [i1 :: Int
i1, i2 :: Int
i2] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "BasicProof" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph
-> Int -> ATermTable -> (ATermTable, ProofStatus proof_tree)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: ProofStatus proof_tree
i2') ->
                (ATermTable
att2, lid -> ProofStatus proof_tree -> BasicProof
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ProofStatus proof_tree -> BasicProof
BasicProof lid
lid ProofStatus proof_tree
i2') }}}
            v :: ShATerm
v@(ShAAppl "BasicProof" [i1 :: Int
i1] _) ->
               case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1 :: ATermTable
att1, i1' :: String
i1') ->
               (ATermTable
att1, case String
i1' of
                 "Guessed" -> BasicProof
Guessed
                 "Conjectured" -> BasicProof
Conjectured
                 "Handwritten" -> BasicProof
Handwritten
                 _ -> String -> ShATerm -> BasicProof
forall a. String -> ShATerm -> a
fromShATermError "BasicProof" ShATerm
v)}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BasicProof)
forall a. String -> ShATerm -> a
fromShATermError "BasicProof" ShATerm
u

instance (ShATermLG a) => ShATermLG (Maybe a) where
  toShATermLG :: ATermTable -> Maybe a -> IO (ATermTable, Int)
toShATermLG att :: ATermTable
att mb :: Maybe a
mb = case Maybe a
mb of
        Nothing -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "N" [] []) ATermTable
att
        Just x :: a
x -> do
          (att1 :: ATermTable
att1, x' :: Int
x') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att a
x
          (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "J" [Int
x'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 =
        case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "N" [] _ -> (ATermTable
att0, Maybe a
forall a. Maybe a
Nothing)
            ShAAppl "J" [a :: Int
a] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: a
a') ->
                    (ATermTable
att1, a -> Maybe a
forall a. a -> Maybe a
Just a
a') }
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Maybe a)
forall a. String -> ShATerm -> a
fromShATermError "Prelude.Maybe" ShATerm
u

instance {-# OVERLAPS #-} ShATermLG a => ShATermLG [a] where
   toShATermLG :: ATermTable -> [a] -> IO (ATermTable, Int)
toShATermLG att :: ATermTable
att ts :: [a]
ts = do
           (att2 :: ATermTable
att2, inds :: [Int]
inds) <- ((ATermTable, [Int]) -> a -> IO (ATermTable, [Int]))
-> (ATermTable, [Int]) -> [a] -> IO (ATermTable, [Int])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (att0 :: ATermTable
att0, l :: [Int]
l) t :: a
t -> do
                    (att1 :: ATermTable
att1, i :: Int
i) <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
t
                    (ATermTable, [Int]) -> IO (ATermTable, [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (ATermTable
att1, Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
l)) (ATermTable
att, []) [a]
ts
           (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm ([Int] -> [Int] -> ShATerm
ShAList ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
inds) []) ATermTable
att2
   fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, [a])
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 =
        case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAList ats :: [Int]
ats _ ->
                (ATermTable -> Int -> (ATermTable, a))
-> ATermTable -> [Int] -> (ATermTable, [a])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL ((Int -> ATermTable -> (ATermTable, a))
-> ATermTable -> Int -> (ATermTable, a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Int -> ATermTable -> (ATermTable, a))
 -> ATermTable -> Int -> (ATermTable, a))
-> (Int -> ATermTable -> (ATermTable, a))
-> ATermTable
-> Int
-> (ATermTable, a)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg ) ATermTable
att0 [Int]
ats
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, [a])
forall a. String -> ShATerm -> a
fromShATermError "[]" ShATerm
u

instance (ShATermLG a, ShATermLG b) => ShATermLG (a, b) where
  toShATermLG :: ATermTable -> (a, b) -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (x :: a
x, y :: b
y) = do
      (att1 :: ATermTable
att1, x' :: Int
x') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
x
      (att2 :: ATermTable
att2, y' :: Int
y') <- ATermTable -> b -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 b
y
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "" [Int
x', Int
y'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, (a, b))
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "" [a :: Int
a, b :: Int
b] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: a
a') ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, b)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of { (att2 :: ATermTable
att2, b' :: b
b') ->
                    (ATermTable
att2, (a
a', b
b'))}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, (a, b))
forall a. String -> ShATerm -> a
fromShATermError "(,)" ShATerm
u

instance (ShATermLG a, ShATermLG b, ShATermLG c) => ShATermLG (a, b, c) where
  toShATermLG :: ATermTable -> (a, b, c) -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (x :: a
x, y :: b
y, z :: c
z) = do
      (att1 :: ATermTable
att1, x' :: Int
x') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
x
      (att2 :: ATermTable
att2, y' :: Int
y') <- ATermTable -> b -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 b
y
      (att3 :: ATermTable
att3, z' :: Int
z') <- ATermTable -> c -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 c
z
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "" [Int
x', Int
y', Int
z'] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, (a, b, c))
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: a
a') ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, b)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of { (att2 :: ATermTable
att2, b' :: b
b') ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, c)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of { (att3 :: ATermTable
att3, c' :: c
c') ->
                    (ATermTable
att3, (a
a', b
b', c
c'))}}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, (a, b, c))
forall a. String -> ShATerm -> a
fromShATermError "(,,)" ShATerm
u

instance (Ord a, ShATermLG a) => ShATermLG (Set.Set a) where
  toShATermLG :: ATermTable -> Set a -> IO (ATermTable, Int)
toShATermLG att :: ATermTable
att set :: Set a
set = do
      (att1 :: ATermTable
att1, i :: Int
i) <- ATermTable -> [a] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att ([a] -> IO (ATermTable, Int)) -> [a] -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
set
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Set" [Int
i] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Set a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 =
        case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "Set" [a :: Int
a] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, [a])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: [a]
a') ->
                    (ATermTable
att1, [a] -> Set a
forall a. [a] -> Set a
Set.fromDistinctAscList [a]
a') }
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Set a)
forall a. String -> ShATerm -> a
fromShATermError "Set.Set" ShATerm
u

instance ShATermLG a => ShATermLG (SizedList.SizedList a) where
  toShATermLG :: ATermTable -> SizedList a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 = ATermTable -> [a] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG ATermTable
att0 ([a] -> IO (ATermTable, Int))
-> (SizedList a -> [a]) -> SizedList a -> IO (ATermTable, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizedList a -> [a]
forall a. SizedList a -> [a]
SizedList.toList
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, SizedList a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case LogicGraph -> Int -> ATermTable -> (ATermTable, [a])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG LogicGraph
lg Int
ix ATermTable
att0 of
    (att :: ATermTable
att, l :: [a]
l) -> (ATermTable
att, [a] -> SizedList a
forall a. [a] -> SizedList a
SizedList.fromList [a]
l)

instance (Ord a, ShATermLG a, ShATermLG b) => ShATermLG (Map.Map a b) where
  toShATermLG :: ATermTable -> Map a b -> IO (ATermTable, Int)
toShATermLG att :: ATermTable
att fm :: Map a b
fm = do
      (att1 :: ATermTable
att1, i :: Int
i) <- ATermTable -> [(a, b)] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att ([(a, b)] -> IO (ATermTable, Int))
-> [(a, b)] -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a b
fm
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Map" [Int
i] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Map a b)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "Map" [a :: Int
a] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, [(a, b)])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: [(a, b)]
a') ->
                    (ATermTable
att1, [(a, b)] -> Map a b
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(a, b)]
a') }
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Map a b)
forall a. String -> ShATerm -> a
fromShATermError "Map.Map" ShATerm
u

instance (ShATermLG a) => ShATermLG (IntMap.IntMap a) where
  toShATermLG :: ATermTable -> IntMap a -> IO (ATermTable, Int)
toShATermLG att :: ATermTable
att fm :: IntMap a
fm = do
      (att1 :: ATermTable
att1, i :: Int
i) <- ATermTable -> [(Int, a)] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att ([(Int, a)] -> IO (ATermTable, Int))
-> [(Int, a)] -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ IntMap a -> [(Int, a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap a
fm
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "IntMap" [Int
i] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, IntMap a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
            ShAAppl "IntMap" [a :: Int
a] _ ->
                    case LogicGraph -> Int -> ATermTable -> (ATermTable, [(Int, a)])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: [(Int, a)]
a') ->
                    (ATermTable
att1, [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromDistinctAscList [(Int, a)]
a') }
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, IntMap a)
forall a. String -> ShATerm -> a
fromShATermError "IntMap.IntMap" ShATerm
u


instance ShATermLG G_theory where
  toShATermLG :: ATermTable -> G_theory -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 (G_theory lid :: lid
lid syn :: Maybe IRI
syn sign :: ExtSign sign symbol
sign si :: SigId
si sens :: ThSens sentence (AnyComorphism, BasicProof)
sens ti :: ThId
ti) = do
         (att1a :: ATermTable
att1a, i1 :: Int
i1) <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
         (att1 :: ATermTable
att1, i1a :: Int
i1a) <- ATermTable -> Maybe IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1a Maybe IRI
syn
         (att2 :: ATermTable
att2, i2 :: Int
i2) <- ATermTable -> ExtSign sign symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ExtSign sign symbol
sign
         (att3 :: ATermTable
att3, i3 :: Int
i3) <- ATermTable -> SigId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 SigId
si
         (att4 :: ATermTable
att4, i4 :: Int
i4) <- ATermTable
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 ThSens sentence (AnyComorphism, BasicProof)
sens
         (att5 :: ATermTable
att5, i5 :: Int
i5) <- ATermTable -> ThId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 ThId
ti
         (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "G_theory" [Int
i1, Int
i1a, Int
i2, Int
i3, Int
i4, Int
i5] [])
                ATermTable
att5
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_theory)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att :: ATermTable
att =
         case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
            ShAAppl "G_theory" [i1 :: Int
i1, i1a :: Int
i1a, i2 :: Int
i2, i3 :: Int
i3, i4 :: Int
i4, i5 :: Int
i5] _ ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1 ATermTable
att of { (att1a :: ATermTable
att1a, i1' :: String
i1') ->
                case LogicGraph -> String -> String -> AnyLogic
atcLogicLookup LogicGraph
lg "G_theory" String
i1' of { Logic lid :: lid
lid ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i1a ATermTable
att1a of { (att1 :: ATermTable
att1, i1a' :: Maybe IRI
i1a') ->
                case LogicGraph
-> Int -> ATermTable -> (ATermTable, ExtSign sign symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i2 ATermTable
att1 of { (att2 :: ATermTable
att2, i2' :: ExtSign sign symbol
i2') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, SigId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i3 ATermTable
att2 of { (att3 :: ATermTable
att3, i3' :: SigId
i3') ->
                case LogicGraph
-> Int
-> ATermTable
-> (ATermTable, ThSens sentence (AnyComorphism, BasicProof))
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i4 ATermTable
att3 of { (att4 :: ATermTable
att4, i4' :: ThSens sentence (AnyComorphism, BasicProof)
i4') ->
                case LogicGraph -> Int -> ATermTable -> (ATermTable, ThId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i5 ATermTable
att4 of { (att5 :: ATermTable
att5, i5' :: ThId
i5') ->
                (ATermTable
att5, lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
i1a' ExtSign sign symbol
i2' SigId
i3' ThSens sentence (AnyComorphism, BasicProof)
i4' ThId
i5') }}}}}}}
            u :: ShATerm
u -> String -> ShATerm -> (ATermTable, G_theory)
forall a. String -> ShATerm -> a
fromShATermError "G_theory" ShATerm
u

instance Typeable a => ShATermConvertible (MVar a) where
    toShATermAux :: ATermTable -> MVar a -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 _ = (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "MVar" [] []) ATermTable
att0
    fromShATermAux :: Int -> ATermTable -> (ATermTable, MVar a)
fromShATermAux ix :: Int
ix att :: ATermTable
att = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att of
        ShAAppl "MVar" [] _ -> (ATermTable
att, String -> MVar a
forall a. HasCallStack => String -> a
error "ShATermConvertible MVar")
        u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MVar a)
forall a. String -> ShATerm -> a
fromShATermError "MVar" ShATerm
u

-- Generated by DrIFT, look but don't touch!

instance ShATermLG a => ShATermLG (Common.AS_Annotation.Annoted a) where
  toShATermLG :: ATermTable -> Annoted a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: Annoted a
xv = case Annoted a
xv of
    Annoted a :: a
a b :: Range
b c :: [Annotation]
c d :: [Annotation]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Range
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Annotation] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 [Annotation]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Annotation] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 [Annotation]
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Annoted" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Annoted a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Annoted" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: a
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Range
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [Annotation])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [Annotation]
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [Annotation])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Annotation]
d') ->
      (ATermTable
att4, a -> Range -> [Annotation] -> [Annotation] -> Annoted a
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted a
a' Range
b' [Annotation]
c' [Annotation]
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Annoted a)
forall a. String -> ShATerm -> a
fromShATermError "Common.AS_Annotation.Annoted" ShATerm
u

instance (ShATermLG s,
          ShATermLG a) => ShATermLG (Common.AS_Annotation.SenAttr s a) where
  toShATermLG :: ATermTable -> SenAttr s a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: SenAttr s a
xv = case SenAttr s a
xv of
    SenAttr a :: a
a b :: Maybe String
b c :: Bool
c d :: Bool
d e :: Bool
e f :: Maybe Bool
f g :: Maybe Id
g h :: String
h i :: Maybe SenOrigin
i j :: s
j -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Maybe String
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Bool
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 Bool
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 Bool
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Maybe Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 Maybe Bool
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Maybe Id -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att6 Maybe Id
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att7 String
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Maybe SenOrigin -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att8 Maybe SenOrigin
i
      (att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> s -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att9 s
j
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SenAttr" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g',
                                            Int
h', Int
i', Int
j'] []) ATermTable
att10
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, SenAttr s a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SenAttr" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h, i :: Int
i, j :: Int
j] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: a
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe String
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Bool
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Bool
e') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: Maybe Bool
f') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe Id)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Maybe Id
g') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: String
h') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe SenOrigin)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: Maybe SenOrigin
i') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, s)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
j ATermTable
att9 of
      { (att10 :: ATermTable
att10, j' :: s
j') ->
      (ATermTable
att10, a
-> Maybe String
-> Bool
-> Bool
-> Bool
-> Maybe Bool
-> Maybe Id
-> String
-> Maybe SenOrigin
-> s
-> SenAttr s a
forall s a.
a
-> Maybe String
-> Bool
-> Bool
-> Bool
-> Maybe Bool
-> Maybe Id
-> String
-> Maybe SenOrigin
-> s
-> SenAttr s a
SenAttr a
a' Maybe String
b' Bool
c' Bool
d' Bool
e' Maybe Bool
f' Maybe Id
g' String
h' Maybe SenOrigin
i' s
j') }}}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SenAttr s a)
forall a. String -> ShATerm -> a
fromShATermError "Common.AS_Annotation.SenAttr" ShATerm
u

instance ShATermLG Common.GlobalAnnotations.GlobalAnnos where
  toShATermLG :: ATermTable -> GlobalAnnos -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: GlobalAnnos
xv = case GlobalAnnos
xv of
    GA a :: PrecedenceGraph
a b :: AssocMap
b c :: DisplayMap
c d :: LiteralAnnos
d e :: LiteralMap
e f :: PrefixMap
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PrecedenceGraph -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 PrecedenceGraph
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> AssocMap -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 AssocMap
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> DisplayMap -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 DisplayMap
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> LiteralAnnos -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 LiteralAnnos
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> LiteralMap -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 LiteralMap
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> PrefixMap -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 PrefixMap
f
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "GA" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f'] []) ATermTable
att6
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalAnnos)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GA" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, PrecedenceGraph)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PrecedenceGraph
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, AssocMap)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: AssocMap
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DisplayMap)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: DisplayMap
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LiteralAnnos)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: LiteralAnnos
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LiteralMap)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: LiteralMap
e') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, PrefixMap)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: PrefixMap
f') ->
      (ATermTable
att6, PrecedenceGraph
-> AssocMap
-> DisplayMap
-> LiteralAnnos
-> LiteralMap
-> PrefixMap
-> GlobalAnnos
GA PrecedenceGraph
a' AssocMap
b' DisplayMap
c' LiteralAnnos
d' LiteralMap
e' PrefixMap
f') }}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GlobalAnnos)
forall a. String -> ShATerm -> a
fromShATermError "Common.GlobalAnnotations.GlobalAnnos" ShATerm
u

instance (ShATermLG a,
          ShATermLG b) => ShATermLG (Common.Lib.Graph.GrContext a b) where
  toShATermLG :: ATermTable -> GrContext a b -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: GrContext a b
xv = case GrContext a b
xv of
    GrContext a :: a
a b :: IntMap [b]
b c :: [b]
c d :: IntMap [b]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 a
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> IntMap [b] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 IntMap [b]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [b] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 [b]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> IntMap [b] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 IntMap [b]
d
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "GrContext" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GrContext a b)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GrContext" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: a
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IntMap [b])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: IntMap [b]
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [b])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [b]
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IntMap [b])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: IntMap [b]
d') ->
      (ATermTable
att4, a -> IntMap [b] -> [b] -> IntMap [b] -> GrContext a b
forall a b. a -> IntMap [b] -> [b] -> IntMap [b] -> GrContext a b
GrContext a
a' IntMap [b]
b' [b]
c' IntMap [b]
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GrContext a b)
forall a. String -> ShATerm -> a
fromShATermError "Common.Lib.Graph.GrContext" ShATerm
u

instance (ShATermLG a,
          ShATermLG b) => ShATermLG (Common.Lib.Graph.Gr a b) where
  toShATermLG :: ATermTable -> Gr a b -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: Gr a b
xv = case Gr a b
xv of
    Gr a :: IntMap (GrContext a b)
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IntMap (GrContext a b) -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IntMap (GrContext a b)
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Gr" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Gr a b)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Gr" [a :: Int
a] _ ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, IntMap (GrContext a b))
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IntMap (GrContext a b)
a') ->
      (ATermTable
att1, IntMap (GrContext a b) -> Gr a b
forall a b. IntMap (GrContext a b) -> Gr a b
Gr IntMap (GrContext a b)
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Gr a b)
forall a. String -> ShATerm -> a
fromShATermError "Common.Lib.Graph.Gr" ShATerm
u

instance ShATermLG a => ShATermLG (Common.OrderedMap.ElemWOrd a) where
  toShATermLG :: ATermTable -> ElemWOrd a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: ElemWOrd a
xv = case ElemWOrd a
xv of
    EWOrd a :: Int
a b :: a
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Int
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 a
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "EWOrd" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ElemWOrd a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "EWOrd" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: a
b') ->
      (ATermTable
att2, Int -> a -> ElemWOrd a
forall a. Int -> a -> ElemWOrd a
EWOrd Int
a' a
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ElemWOrd a)
forall a. String -> ShATerm -> a
fromShATermError "Common.OrderedMap.ElemWOrd" ShATerm
u

instance ShATermLG a => ShATermLG (Logic.Prover.ThmStatus a) where
  toShATermLG :: ATermTable -> ThmStatus a -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: ThmStatus a
xv = case ThmStatus a
xv of
    ThmStatus a :: [a]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [a] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 [a]
a
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ThmStatus" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmStatus a)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ThmStatus" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [a])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [a]
a') ->
      (ATermTable
att1, [a] -> ThmStatus a
forall a. [a] -> ThmStatus a
ThmStatus [a]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ThmStatus a)
forall a. String -> ShATerm -> a
fromShATermError "Logic.Prover.ThmStatus" ShATerm
u