{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  LF/ATC_LF.der.hs
Description :  generated ShATermConvertible, Json instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(derive Typeable instances)

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json
  for the type(s):
'LF.Sign.Symbol'
'LF.Sign.EXP'
'LF.Sign.DEF'
'LF.Sign.Sign'
'LF.Morphism.MorphType'
'LF.Morphism.Morphism'
'LF.AS.BASIC_SPEC'
'LF.AS.BASIC_ITEM'
'LF.AS.SYMB_ITEMS'
'LF.AS.SYMB_MAP_ITEMS'
'LF.AS.SYMB_OR_MAP'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
LF/Sign.hs
LF/Morphism.hs
LF/AS.hs
-}

module LF.ATC_LF () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation
import Common.Doc
import Common.Doc hiding (space)
import Common.DocUtils
import Common.Id
import Common.Json.Instances
import Common.Keywords
import Common.Result
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List
import Data.Maybe
import Data.Maybe (isNothing, fromMaybe)
import GHC.Generics(Generic)
import LF.AS
import LF.Morphism
import LF.Sign
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for LF.Sign.Symbol derive : ShATermConvertible !-}
{-! for LF.Sign.EXP derive : ShATermConvertible !-}
{-! for LF.Sign.DEF derive : ShATermConvertible !-}
{-! for LF.Sign.Sign derive : ShATermConvertible !-}
{-! for LF.Morphism.MorphType derive : ShATermConvertible !-}
{-! for LF.Morphism.Morphism derive : ShATermConvertible !-}
{-! for LF.AS.BASIC_SPEC derive : ShATermConvertible !-}
{-! for LF.AS.BASIC_ITEM derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_ITEMS derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_MAP_ITEMS derive : ShATermConvertible !-}
{-! for LF.AS.SYMB_OR_MAP derive : ShATermConvertible !-}

{-! for LF.Sign.Symbol derive : Json !-}
{-! for LF.Sign.EXP derive : Json !-}
{-! for LF.Sign.DEF derive : Json !-}
{-! for LF.Sign.Sign derive : Json !-}
{-! for LF.Morphism.MorphType derive : Json !-}
{-! for LF.Morphism.Morphism derive : Json !-}
{-! for LF.AS.BASIC_SPEC derive : Json !-}
{-! for LF.AS.BASIC_ITEM derive : Json !-}
{-! for LF.AS.SYMB_ITEMS derive : Json !-}
{-! for LF.AS.SYMB_MAP_ITEMS derive : Json !-}
{-! for LF.AS.SYMB_OR_MAP derive : Json !-}

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

deriving instance GHC.Generics.Generic LF.AS.SYMB_OR_MAP
instance Data.Aeson.ToJSON LF.AS.SYMB_OR_MAP where
instance Data.Aeson.FromJSON LF.AS.SYMB_OR_MAP where

deriving instance GHC.Generics.Generic LF.AS.SYMB_MAP_ITEMS
instance Data.Aeson.ToJSON LF.AS.SYMB_MAP_ITEMS where
instance Data.Aeson.FromJSON LF.AS.SYMB_MAP_ITEMS where

deriving instance GHC.Generics.Generic LF.AS.SYMB_ITEMS
instance Data.Aeson.ToJSON LF.AS.SYMB_ITEMS where
instance Data.Aeson.FromJSON LF.AS.SYMB_ITEMS where

deriving instance GHC.Generics.Generic LF.AS.BASIC_ITEM
instance Data.Aeson.ToJSON LF.AS.BASIC_ITEM where
instance Data.Aeson.FromJSON LF.AS.BASIC_ITEM where

deriving instance GHC.Generics.Generic LF.AS.BASIC_SPEC
instance Data.Aeson.ToJSON LF.AS.BASIC_SPEC where
instance Data.Aeson.FromJSON LF.AS.BASIC_SPEC where

instance ShATermConvertible LF.AS.SYMB_OR_MAP where
  toShATermAux :: ATermTable -> SYMB_OR_MAP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_OR_MAP
xv = case SYMB_OR_MAP
xv of
    Symb a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Symb" [Int
a'] []) ATermTable
att1
    Symb_map a :: String
a b :: String
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 String
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 "Symb_map" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_OR_MAP)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Symb" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> SYMB_OR_MAP
Symb String
a') }
    ShAAppl "Symb_map" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      (ATermTable
att2, String -> String -> SYMB_OR_MAP
Symb_map String
a' String
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_OR_MAP)
forall a. String -> ShATerm -> a
fromShATermError "LF.AS.SYMB_OR_MAP" ShATerm
u

instance ShATermConvertible LF.AS.SYMB_MAP_ITEMS where
  toShATermAux :: ATermTable -> SYMB_MAP_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_MAP_ITEMS
xv = case SYMB_MAP_ITEMS
xv of
    Symb_map_items a :: [SYMB_OR_MAP]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SYMB_OR_MAP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SYMB_OR_MAP]
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 "Symb_map_items" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_MAP_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Symb_map_items" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [SYMB_OR_MAP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SYMB_OR_MAP]
a') ->
      (ATermTable
att1, [SYMB_OR_MAP] -> SYMB_MAP_ITEMS
Symb_map_items [SYMB_OR_MAP]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_MAP_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "LF.AS.SYMB_MAP_ITEMS" ShATerm
u

instance ShATermConvertible LF.AS.SYMB_ITEMS where
  toShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_ITEMS
xv = case SYMB_ITEMS
xv of
    Symb_items a :: [String]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [String]
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 "Symb_items" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Symb_items" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [String]
a') ->
      (ATermTable
att1, [String] -> SYMB_ITEMS
Symb_items [String]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "LF.AS.SYMB_ITEMS" ShATerm
u

instance ShATermConvertible LF.AS.BASIC_ITEM where
  toShATermAux :: ATermTable -> BASIC_ITEM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_ITEM
xv = case BASIC_ITEM
xv of
    Decl a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Decl" [Int
a'] []) ATermTable
att1
    Form a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Form" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Decl" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> BASIC_ITEM
Decl String
a') }
    ShAAppl "Form" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> BASIC_ITEM
Form String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_ITEM)
forall a. String -> ShATerm -> a
fromShATermError "LF.AS.BASIC_ITEM" ShATerm
u

instance ShATermConvertible LF.AS.BASIC_SPEC where
  toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_SPEC
xv = case BASIC_SPEC
xv of
    Basic_spec a :: [Annoted BASIC_ITEM]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted BASIC_ITEM] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted BASIC_ITEM]
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 "Basic_spec" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Basic_spec" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Annoted BASIC_ITEM])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Annoted BASIC_ITEM]
a') ->
      (ATermTable
att1, [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec [Annoted BASIC_ITEM]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC)
forall a. String -> ShATerm -> a
fromShATermError "LF.AS.BASIC_SPEC" ShATerm
u

instance ShATermConvertible LF.Morphism.MorphType where
  toShATermAux :: ATermTable -> MorphType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: MorphType
xv = case MorphType
xv of
    Definitional -> (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 "Definitional" [] []) ATermTable
att0
    Postulated -> (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 "Postulated" [] []) ATermTable
att0
    Unknown -> (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 "Unknown" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, MorphType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Definitional" [] _ -> (ATermTable
att0, MorphType
Definitional)
    ShAAppl "Postulated" [] _ -> (ATermTable
att0, MorphType
Postulated)
    ShAAppl "Unknown" [] _ -> (ATermTable
att0, MorphType
Unknown)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MorphType)
forall a. String -> ShATerm -> a
fromShATermError "LF.Morphism.MorphType" ShATerm
u

instance ShATermConvertible LF.Morphism.Morphism where
  toShATermAux :: ATermTable -> Morphism -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Morphism
xv = case Morphism
xv of
    Morphism a :: String
a b :: String
b c :: String
c d :: Sign
d e :: Sign
e f :: MorphType
f g :: Map Symbol EXP
g -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 String
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 String
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Sign
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Sign
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> MorphType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 MorphType
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Map Symbol EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Map Symbol EXP
g
      (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 "Morphism" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
                                             Int
g'] []) ATermTable
att7
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Morphism" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: String
c') ->
      case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Sign
d') ->
      case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Sign
e') ->
      case Int -> ATermTable -> (ATermTable, MorphType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: MorphType
f') ->
      case Int -> ATermTable -> (ATermTable, Map Symbol EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Map Symbol EXP
g') ->
      (ATermTable
att7, String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
a' String
b' String
c' Sign
d' Sign
e' MorphType
f' Map Symbol EXP
g') }}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism)
forall a. String -> ShATerm -> a
fromShATermError "LF.Morphism.Morphism" ShATerm
u

deriving instance GHC.Generics.Generic LF.Morphism.MorphType
instance Data.Aeson.ToJSON LF.Morphism.MorphType where
instance Data.Aeson.FromJSON LF.Morphism.MorphType where

deriving instance GHC.Generics.Generic LF.Morphism.Morphism
instance Data.Aeson.ToJSON LF.Morphism.Morphism where
instance Data.Aeson.FromJSON LF.Morphism.Morphism where

deriving instance GHC.Generics.Generic LF.Sign.Sign
instance Data.Aeson.ToJSON LF.Sign.Sign where
instance Data.Aeson.FromJSON LF.Sign.Sign where

deriving instance GHC.Generics.Generic LF.Sign.DEF
instance Data.Aeson.ToJSON LF.Sign.DEF where
instance Data.Aeson.FromJSON LF.Sign.DEF where

deriving instance GHC.Generics.Generic LF.Sign.EXP
instance Data.Aeson.ToJSON LF.Sign.EXP where
instance Data.Aeson.FromJSON LF.Sign.EXP where

deriving instance GHC.Generics.Generic LF.Sign.Symbol
instance Data.Aeson.ToJSON LF.Sign.Symbol where
instance Data.Aeson.FromJSON LF.Sign.Symbol where

instance ShATermConvertible LF.Sign.Sign where
  toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
    Sign a :: String
a b :: String
b c :: [DEF]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 String
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [DEF] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [DEF]
c
      (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 "Sign" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sign" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      case Int -> ATermTable -> (ATermTable, [DEF])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [DEF]
c') ->
      (ATermTable
att3, String -> String -> [DEF] -> Sign
Sign String
a' String
b' [DEF]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "LF.Sign.Sign" ShATerm
u

instance ShATermConvertible LF.Sign.DEF where
  toShATermAux :: ATermTable -> DEF -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DEF
xv = case DEF
xv of
    Def a :: Symbol
a b :: EXP
b c :: Maybe EXP
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Symbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Symbol
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 EXP
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe EXP
c
      (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 "Def" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DEF)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Def" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Symbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Symbol
a') ->
      case Int -> ATermTable -> (ATermTable, EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: EXP
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe EXP
c') ->
      (ATermTable
att3, Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
a' EXP
b' Maybe EXP
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DEF)
forall a. String -> ShATerm -> a
fromShATermError "LF.Sign.DEF" ShATerm
u

instance ShATermConvertible LF.Sign.EXP where
  toShATermAux :: ATermTable -> EXP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: EXP
xv = case EXP
xv of
    Type -> (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 "Type" [] []) ATermTable
att0
    Var a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
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 "Var" [Int
a'] []) ATermTable
att1
    Const a :: Symbol
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Symbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Symbol
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 "Const" [Int
a'] []) ATermTable
att1
    Appl a :: EXP
a b :: [EXP]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 EXP
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [EXP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [EXP]
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 "Appl" [Int
a', Int
b'] []) ATermTable
att2
    Func a :: [EXP]
a b :: EXP
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [EXP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [EXP]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 EXP
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 "Func" [Int
a', Int
b'] []) ATermTable
att2
    Pi a :: CONTEXT
a b :: EXP
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> CONTEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 CONTEXT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 EXP
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 "Pi" [Int
a', Int
b'] []) ATermTable
att2
    Lamb a :: CONTEXT
a b :: EXP
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> CONTEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 CONTEXT
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> EXP -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 EXP
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 "Lamb" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, EXP)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Type" [] _ -> (ATermTable
att0, EXP
Type)
    ShAAppl "Var" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> EXP
Var String
a') }
    ShAAppl "Const" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Symbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Symbol
a') ->
      (ATermTable
att1, Symbol -> EXP
Const Symbol
a') }
    ShAAppl "Appl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: EXP
a') ->
      case Int -> ATermTable -> (ATermTable, [EXP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [EXP]
b') ->
      (ATermTable
att2, EXP -> [EXP] -> EXP
Appl EXP
a' [EXP]
b') }}
    ShAAppl "Func" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [EXP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [EXP]
a') ->
      case Int -> ATermTable -> (ATermTable, EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: EXP
b') ->
      (ATermTable
att2, [EXP] -> EXP -> EXP
Func [EXP]
a' EXP
b') }}
    ShAAppl "Pi" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, CONTEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: CONTEXT
a') ->
      case Int -> ATermTable -> (ATermTable, EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: EXP
b') ->
      (ATermTable
att2, CONTEXT -> EXP -> EXP
Pi CONTEXT
a' EXP
b') }}
    ShAAppl "Lamb" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, CONTEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: CONTEXT
a') ->
      case Int -> ATermTable -> (ATermTable, EXP)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: EXP
b') ->
      (ATermTable
att2, CONTEXT -> EXP -> EXP
Lamb CONTEXT
a' EXP
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, EXP)
forall a. String -> ShATerm -> a
fromShATermError "LF.Sign.EXP" ShATerm
u

instance ShATermConvertible LF.Sign.Symbol where
  toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symbol
xv = case Symbol
xv of
    Symbol a :: String
a b :: String
b c :: String
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 String
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 String
c
      (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 "Symbol" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Symbol" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: String
c') ->
      (ATermTable
att3, String -> String -> String -> Symbol
Symbol String
a' String
b' String
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symbol)
forall a. String -> ShATerm -> a
fromShATermError "LF.Sign.Symbol" ShATerm
u