{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  Isabelle/ATC_Isabelle.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):
'Isabelle.IsaSign.AltSyntax'
'Isabelle.IsaSign.VName'
'Isabelle.IsaSign.QName'
'Isabelle.IsaSign.Indexname'
'Isabelle.IsaSign.IsaClass'
'Isabelle.IsaSign.Typ'
'Isabelle.IsaSign.Continuity'
'Isabelle.IsaSign.TAttr'
'Isabelle.IsaSign.DTyp'
'Isabelle.IsaSign.Term'
'Isabelle.IsaSign.Prop'
'Isabelle.IsaSign.Props'
'Isabelle.IsaSign.Sentence'
'Isabelle.IsaSign.DefEquation'
'Isabelle.IsaSign.FixrecEquation'
'Isabelle.IsaSign.Ctxt'
'Isabelle.IsaSign.Mixfix'
'Isabelle.IsaSign.MixfixTemplate'
'Isabelle.IsaSign.Datatype'
'Isabelle.IsaSign.DatatypeConstructor'
'Isabelle.IsaSign.Domain'
'Isabelle.IsaSign.DomainConstructor'
'Isabelle.IsaSign.DomainConstructorArg'
'Isabelle.IsaSign.Axiom'
'Isabelle.IsaSign.FunSig'
'Isabelle.IsaSign.SetDecl'
'Isabelle.IsaSign.MetaTerm'
'Isabelle.IsaSign.TypeSig'
'Isabelle.IsaSign.BaseSig'
'Isabelle.IsaSign.Sign'
'Isabelle.IsaSign.IsaProof'
'Isabelle.IsaSign.ProofCommand'
'Isabelle.IsaSign.ProofEnd'
'Isabelle.IsaSign.Modifier'
'Isabelle.IsaSign.ProofMethod'
-}

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

module Isabelle.ATC_Isabelle () where

import ATerm.Lib
import Common.Json.Instances
import Common.Utils (splitOn)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List
import GHC.Generics(Generic)
import Isabelle.IsaSign
import qualified Data.Map as Map

{-! for Isabelle.IsaSign.AltSyntax derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.VName derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.QName derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Indexname derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.IsaClass derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Typ derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Continuity derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.TAttr derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.DTyp derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Term derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Prop derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Props derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Sentence derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.DefEquation derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.FixrecEquation derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Ctxt derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Mixfix derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.MixfixTemplate derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Datatype derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.DatatypeConstructor derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Domain derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.DomainConstructor derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.DomainConstructorArg derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Axiom derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.FunSig derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.SetDecl derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.MetaTerm derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.TypeSig derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.BaseSig derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Sign derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.IsaProof derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.ProofCommand derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.ProofEnd derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.Modifier derive : ShATermConvertible !-}
{-! for Isabelle.IsaSign.ProofMethod derive : ShATermConvertible !-}

{-! for Isabelle.IsaSign.AltSyntax derive : Json !-}
{-! for Isabelle.IsaSign.VName derive : Json !-}
{-! for Isabelle.IsaSign.QName derive : Json !-}
{-! for Isabelle.IsaSign.Indexname derive : Json !-}
{-! for Isabelle.IsaSign.IsaClass derive : Json !-}
{-! for Isabelle.IsaSign.Typ derive : Json !-}
{-! for Isabelle.IsaSign.Continuity derive : Json !-}
{-! for Isabelle.IsaSign.TAttr derive : Json !-}
{-! for Isabelle.IsaSign.DTyp derive : Json !-}
{-! for Isabelle.IsaSign.Term derive : Json !-}
{-! for Isabelle.IsaSign.Prop derive : Json !-}
{-! for Isabelle.IsaSign.Props derive : Json !-}
{-! for Isabelle.IsaSign.Sentence derive : Json !-}
{-! for Isabelle.IsaSign.DefEquation derive : Json !-}
{-! for Isabelle.IsaSign.FixrecEquation derive : Json !-}
{-! for Isabelle.IsaSign.Ctxt derive : Json !-}
{-! for Isabelle.IsaSign.Mixfix derive : Json !-}
{-! for Isabelle.IsaSign.MixfixTemplate derive : Json !-}
{-! for Isabelle.IsaSign.Datatype derive : Json !-}
{-! for Isabelle.IsaSign.DatatypeConstructor derive : Json !-}
{-! for Isabelle.IsaSign.Domain derive : Json !-}
{-! for Isabelle.IsaSign.DomainConstructor derive : Json !-}
{-! for Isabelle.IsaSign.DomainConstructorArg derive : Json !-}
{-! for Isabelle.IsaSign.Axiom derive : Json !-}
{-! for Isabelle.IsaSign.FunSig derive : Json !-}
{-! for Isabelle.IsaSign.SetDecl derive : Json !-}
{-! for Isabelle.IsaSign.MetaTerm derive : Json !-}
{-! for Isabelle.IsaSign.TypeSig derive : Json !-}
{-! for Isabelle.IsaSign.BaseSig derive : Json !-}
{-! for Isabelle.IsaSign.Sign derive : Json !-}
{-! for Isabelle.IsaSign.IsaProof derive : Json !-}
{-! for Isabelle.IsaSign.ProofCommand derive : Json !-}
{-! for Isabelle.IsaSign.ProofEnd derive : Json !-}
{-! for Isabelle.IsaSign.Modifier derive : Json !-}
{-! for Isabelle.IsaSign.ProofMethod derive : Json !-}

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

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

instance ShATermConvertible Isabelle.IsaSign.VName where
  toShATermAux :: ATermTable -> VName -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: VName
xv = case VName
xv of
    VName a :: String
a b :: Maybe AltSyntax
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 -> Maybe AltSyntax -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe AltSyntax
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 "VName" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, VName)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "VName" [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, Maybe AltSyntax)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe AltSyntax
b') ->
      (ATermTable
att2, String -> Maybe AltSyntax -> VName
VName String
a' Maybe AltSyntax
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, VName)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.VName" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.QName where
  toShATermAux :: ATermTable -> QName -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: QName
xv = case QName
xv of
    QName 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 "QName" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, QName)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "QName" [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] -> QName
QName String
a' [String]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, QName)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.QName" ShATerm
u

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

instance ShATermConvertible Isabelle.IsaSign.IsaClass where
  toShATermAux :: ATermTable -> IsaClass -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: IsaClass
xv = case IsaClass
xv of
    IsaClass 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 "IsaClass" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, IsaClass)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "IsaClass" [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 -> IsaClass
IsaClass String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, IsaClass)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.IsaClass" ShATerm
u

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

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

instance ShATermConvertible Isabelle.IsaSign.TAttr where
  toShATermAux :: ATermTable -> TAttr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TAttr
xv = case TAttr
xv of
    TFun -> (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 "TFun" [] []) ATermTable
att0
    TMet -> (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 "TMet" [] []) ATermTable
att0
    TCon -> (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 "TCon" [] []) ATermTable
att0
    NA -> (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 "NA" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TAttr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TFun" [] _ -> (ATermTable
att0, TAttr
TFun)
    ShAAppl "TMet" [] _ -> (ATermTable
att0, TAttr
TMet)
    ShAAppl "TCon" [] _ -> (ATermTable
att0, TAttr
TCon)
    ShAAppl "NA" [] _ -> (ATermTable
att0, TAttr
NA)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TAttr)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.TAttr" ShATerm
u

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

instance ShATermConvertible Isabelle.IsaSign.Term where
  toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Term
xv = case Term
xv of
    Const a :: VName
a b :: DTyp
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> DTyp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 DTyp
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 "Const" [Int
a', Int
b'] []) ATermTable
att2
    Free a :: VName
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VName
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 "Free" [Int
a'] []) ATermTable
att1
    Abs a :: Term
a b :: Term
b c :: Continuity
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Continuity -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Continuity
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 "Abs" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    App a :: Term
a b :: Term
b c :: Continuity
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Continuity -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Continuity
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 "App" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    If a :: Term
a b :: Term
b c :: Term
c d :: Continuity
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Term
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Continuity -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Continuity
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 "If" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Case a :: Term
a b :: [(Term, Term)]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [(Term, Term)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [(Term, Term)]
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 "Case" [Int
a', Int
b'] []) ATermTable
att2
    Let a :: [(Term, Term)]
a b :: Term
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [(Term, Term)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [(Term, Term)]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
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 "Let" [Int
a', Int
b'] []) ATermTable
att2
    IsaEq a :: Term
a b :: Term
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
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 "IsaEq" [Int
a', Int
b'] []) ATermTable
att2
    Tuplex a :: [Term]
a b :: Continuity
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Term] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Term]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Continuity -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Continuity
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 "Tuplex" [Int
a', Int
b'] []) ATermTable
att2
    Set a :: SetDecl
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SetDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SetDecl
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 "Set" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Term)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Const" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, VName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: VName
a') ->
      case Int -> ATermTable -> (ATermTable, DTyp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: DTyp
b') ->
      (ATermTable
att2, VName -> DTyp -> Term
Const VName
a' DTyp
b') }}
    ShAAppl "Free" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, VName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: VName
a') ->
      (ATermTable
att1, VName -> Term
Free VName
a') }
    ShAAppl "Abs" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Term
b') ->
      case Int -> ATermTable -> (ATermTable, Continuity)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Continuity
c') ->
      (ATermTable
att3, Term -> Term -> Continuity -> Term
Abs Term
a' Term
b' Continuity
c') }}}
    ShAAppl "App" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Term
b') ->
      case Int -> ATermTable -> (ATermTable, Continuity)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Continuity
c') ->
      (ATermTable
att3, Term -> Term -> Continuity -> Term
App Term
a' Term
b' Continuity
c') }}}
    ShAAppl "If" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Term
b') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Term
c') ->
      case Int -> ATermTable -> (ATermTable, Continuity)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Continuity
d') ->
      (ATermTable
att4, Term -> Term -> Term -> Continuity -> Term
If Term
a' Term
b' Term
c' Continuity
d') }}}}
    ShAAppl "Case" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      case Int -> ATermTable -> (ATermTable, [(Term, Term)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [(Term, Term)]
b') ->
      (ATermTable
att2, Term -> [(Term, Term)] -> Term
Case Term
a' [(Term, Term)]
b') }}
    ShAAppl "Let" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [(Term, Term)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [(Term, Term)]
a') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Term
b') ->
      (ATermTable
att2, [(Term, Term)] -> Term -> Term
Let [(Term, Term)]
a' Term
b') }}
    ShAAppl "IsaEq" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Term
b') ->
      (ATermTable
att2, Term -> Term -> Term
IsaEq Term
a' Term
b') }}
    ShAAppl "Tuplex" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Term]
a') ->
      case Int -> ATermTable -> (ATermTable, Continuity)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Continuity
b') ->
      (ATermTable
att2, [Term] -> Continuity -> Term
Tuplex [Term]
a' Continuity
b') }}
    ShAAppl "Set" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SetDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SetDecl
a') ->
      (ATermTable
att1, SetDecl -> Term
Set SetDecl
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Term)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Term" ShATerm
u

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

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

instance ShATermConvertible Isabelle.IsaSign.Sentence where
  toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sentence
xv = case Sentence
xv of
    Sentence a :: Bool
a b :: Bool
b c :: MetaTerm
c d :: Maybe IsaProof
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> MetaTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 MetaTerm
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Maybe IsaProof -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Maybe IsaProof
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 "Sentence" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Instance a :: String
a b :: [[IsaClass]]
b c :: [IsaClass]
c d :: [(String, Term)]
d e :: IsaProof
e -> 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 -> [[IsaClass]] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [[IsaClass]]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [IsaClass] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [IsaClass]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [(String, Term)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [(String, Term)]
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> IsaProof -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 IsaProof
e
      (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 "Instance" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
    ConstDef a :: Term
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
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 "ConstDef" [Int
a'] []) ATermTable
att1
    RecDef a :: Maybe String
a b :: VName
b c :: Maybe Typ
c d :: [Term]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> VName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 VName
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Typ
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Term] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Term]
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 "RecDef" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    TypeDef a :: Typ
a b :: SetDecl
b c :: IsaProof
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Typ
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SetDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SetDecl
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> IsaProof -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 IsaProof
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 "TypeDef" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Lemmas 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 "Lemmas" [Int
a', Int
b'] []) ATermTable
att2
    Locale a :: QName
a b :: Ctxt
b c :: [QName]
c d :: [Sentence]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Ctxt -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Ctxt
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [QName] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [QName]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Sentence] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Sentence]
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 "Locale" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Class a :: QName
a b :: Ctxt
b c :: [QName]
c d :: [Sentence]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Ctxt -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Ctxt
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [QName] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [QName]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Sentence] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Sentence]
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 "Class" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Datatypes a :: [Datatype]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Datatype] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Datatype]
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 "Datatypes" [Int
a'] []) ATermTable
att1
    Domains a :: [Domain]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Domain] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Domain]
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 "Domains" [Int
a'] []) ATermTable
att1
    Consts a :: [(String, Maybe Mixfix, Typ)]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [(String, Maybe Mixfix, Typ)] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [(String, Maybe Mixfix, Typ)]
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 "Consts" [Int
a'] []) ATermTable
att1
    TypeSynonym a :: QName
a b :: Maybe Mixfix
b c :: [String]
c d :: Typ
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe Mixfix
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 -> Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Typ
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 "TypeSynonym" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Axioms a :: [Axiom]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Axiom] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Axiom]
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 "Axioms" [Int
a'] []) ATermTable
att1
    Lemma a :: Maybe QName
a b :: Ctxt
b c :: Maybe String
c d :: [Props]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Ctxt -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Ctxt
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe String
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Props] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Props]
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 "Lemma" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
    Definition a :: QName
a b :: Maybe Mixfix
b c :: Maybe String
c d :: Typ
d e :: [Term]
e f :: Term
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe Mixfix
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe String
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Typ
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> [Term] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 [Term]
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 Term
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 "Definition" [Int
a', Int
b', Int
c', Int
d', Int
e',
                                               Int
f'] []) ATermTable
att6
    Fun a :: Maybe QName
a b :: Bool
b c :: Maybe String
c d :: Bool
d e :: Bool
e f :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe String
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Bool
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Bool
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
-> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 [(String, Maybe Mixfix, Typ, [([Term], Term)])]
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 "Fun" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f'] []) ATermTable
att6
    Primrec a :: Maybe QName
a b :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
-> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [(String, Maybe Mixfix, Typ, [([Term], Term)])]
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 "Primrec" [Int
a', Int
b'] []) ATermTable
att2
    Fixrec a :: [(String, Maybe Mixfix, Typ, [FixrecEquation])]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable
-> [(String, Maybe Mixfix, Typ, [FixrecEquation])]
-> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [(String, Maybe Mixfix, Typ, [FixrecEquation])]
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 "Fixrec" [Int
a'] []) ATermTable
att1
    Instantiation a :: String
a b :: ([IsaClass], [[IsaClass]])
b c :: [Sentence]
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 -> ([IsaClass], [[IsaClass]]) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ([IsaClass], [[IsaClass]])
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Sentence] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Sentence]
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 "Instantiation" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    InstanceProof 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 "InstanceProof" [Int
a'] []) ATermTable
att1
    InstanceArity a :: [String]
a b :: ([IsaClass], [[IsaClass]])
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 -> ([IsaClass], [[IsaClass]]) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ([IsaClass], [[IsaClass]])
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 "InstanceArity" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    InstanceSubclass a :: String
a b :: String
b c :: String
c d :: String
d -> 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 -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 String
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 "InstanceSubclass" [Int
a', Int
b', Int
c',
                                                     Int
d'] []) ATermTable
att4
    Subclass a :: String
a b :: Maybe QName
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 -> Maybe QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe QName
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 "Subclass" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    Typedef a :: QName
a b :: [(String, [IsaClass])]
b c :: Maybe Mixfix
c d :: Maybe (QName, QName)
d e :: Term
e f :: String
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [(String, [IsaClass])] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [(String, [IsaClass])]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Mixfix
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Maybe (QName, QName) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Maybe (QName, QName)
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Term
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 String
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 "Typedef" [Int
a', Int
b', Int
c', Int
d', Int
e',
                                            Int
f'] []) ATermTable
att6
    Defs a :: Bool
a b :: Bool
b c :: [DefEquation]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [DefEquation] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [DefEquation]
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 "Defs" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sentence" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      case Int -> ATermTable -> (ATermTable, MetaTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: MetaTerm
c') ->
      case Int -> ATermTable -> (ATermTable, Maybe IsaProof)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Maybe IsaProof
d') ->
      (ATermTable
att4, Bool -> Bool -> MetaTerm -> Maybe IsaProof -> Sentence
Sentence Bool
a' Bool
b' MetaTerm
c' Maybe IsaProof
d') }}}}
    ShAAppl "Instance" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      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, [[IsaClass]])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [[IsaClass]]
b') ->
      case Int -> ATermTable -> (ATermTable, [IsaClass])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [IsaClass]
c') ->
      case Int -> ATermTable -> (ATermTable, [(String, Term)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [(String, Term)]
d') ->
      case Int -> ATermTable -> (ATermTable, IsaProof)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: IsaProof
e') ->
      (ATermTable
att5, String
-> [[IsaClass]]
-> [IsaClass]
-> [(String, Term)]
-> IsaProof
-> Sentence
Instance String
a' [[IsaClass]]
b' [IsaClass]
c' [(String, Term)]
d' IsaProof
e') }}}}}
    ShAAppl "ConstDef" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      (ATermTable
att1, Term -> Sentence
ConstDef Term
a') }
    ShAAppl "RecDef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe String
a') ->
      case Int -> ATermTable -> (ATermTable, VName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: VName
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Typ
c') ->
      case Int -> ATermTable -> (ATermTable, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Term]
d') ->
      (ATermTable
att4, Maybe String -> VName -> Maybe Typ -> [Term] -> Sentence
RecDef Maybe String
a' VName
b' Maybe Typ
c' [Term]
d') }}}}
    ShAAppl "TypeDef" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Typ
a') ->
      case Int -> ATermTable -> (ATermTable, SetDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SetDecl
b') ->
      case Int -> ATermTable -> (ATermTable, IsaProof)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: IsaProof
c') ->
      (ATermTable
att3, Typ -> SetDecl -> IsaProof -> Sentence
TypeDef Typ
a' SetDecl
b' IsaProof
c') }}}
    ShAAppl "Lemmas" [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] -> Sentence
Lemmas String
a' [String]
b') }}
    ShAAppl "Locale" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, Ctxt)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Ctxt
b') ->
      case Int -> ATermTable -> (ATermTable, [QName])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [QName]
c') ->
      case Int -> ATermTable -> (ATermTable, [Sentence])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Sentence]
d') ->
      (ATermTable
att4, QName -> Ctxt -> [QName] -> [Sentence] -> Sentence
Locale QName
a' Ctxt
b' [QName]
c' [Sentence]
d') }}}}
    ShAAppl "Class" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, Ctxt)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Ctxt
b') ->
      case Int -> ATermTable -> (ATermTable, [QName])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [QName]
c') ->
      case Int -> ATermTable -> (ATermTable, [Sentence])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Sentence]
d') ->
      (ATermTable
att4, QName -> Ctxt -> [QName] -> [Sentence] -> Sentence
Class QName
a' Ctxt
b' [QName]
c' [Sentence]
d') }}}}
    ShAAppl "Datatypes" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Datatype])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Datatype]
a') ->
      (ATermTable
att1, [Datatype] -> Sentence
Datatypes [Datatype]
a') }
    ShAAppl "Domains" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Domain])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Domain]
a') ->
      (ATermTable
att1, [Domain] -> Sentence
Domains [Domain]
a') }
    ShAAppl "Consts" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [(String, Maybe Mixfix, Typ)])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [(String, Maybe Mixfix, Typ)]
a') ->
      (ATermTable
att1, [(String, Maybe Mixfix, Typ)] -> Sentence
Consts [(String, Maybe Mixfix, Typ)]
a') }
    ShAAppl "TypeSynonym" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe Mixfix
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, Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Typ
d') ->
      (ATermTable
att4, QName -> Maybe Mixfix -> [String] -> Typ -> Sentence
TypeSynonym QName
a' Maybe Mixfix
b' [String]
c' Typ
d') }}}}
    ShAAppl "Axioms" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Axiom])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Axiom]
a') ->
      (ATermTable
att1, [Axiom] -> Sentence
Axioms [Axiom]
a') }
    ShAAppl "Lemma" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe QName
a') ->
      case Int -> ATermTable -> (ATermTable, Ctxt)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Ctxt
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe String
c') ->
      case Int -> ATermTable -> (ATermTable, [Props])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Props]
d') ->
      (ATermTable
att4, Maybe QName -> Ctxt -> Maybe String -> [Props] -> Sentence
Lemma Maybe QName
a' Ctxt
b' Maybe String
c' [Props]
d') }}}}
    ShAAppl "Definition" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe Mixfix
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe String
c') ->
      case Int -> ATermTable -> (ATermTable, Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Typ
d') ->
      case Int -> ATermTable -> (ATermTable, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: [Term]
e') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: Term
f') ->
      (ATermTable
att6, QName
-> Maybe Mixfix
-> Maybe String
-> Typ
-> [Term]
-> Term
-> Sentence
Definition QName
a' Maybe Mixfix
b' Maybe String
c' Typ
d' [Term]
e' Term
f') }}}}}}
    ShAAppl "Fun" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe QName
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe String
c') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Bool
e') ->
      case Int
-> ATermTable
-> (ATermTable, [(String, Maybe Mixfix, Typ, [([Term], Term)])])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
f') ->
      (ATermTable
att6, Maybe QName
-> Bool
-> Maybe String
-> Bool
-> Bool
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
-> Sentence
Fun Maybe QName
a' Bool
b' Maybe String
c' Bool
d' Bool
e' [(String, Maybe Mixfix, Typ, [([Term], Term)])]
f') }}}}}}
    ShAAppl "Primrec" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe QName
a') ->
      case Int
-> ATermTable
-> (ATermTable, [(String, Maybe Mixfix, Typ, [([Term], Term)])])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
b') ->
      (ATermTable
att2, Maybe QName
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> Sentence
Primrec Maybe QName
a' [(String, Maybe Mixfix, Typ, [([Term], Term)])]
b') }}
    ShAAppl "Fixrec" [a :: Int
a] _ ->
      case Int
-> ATermTable
-> (ATermTable, [(String, Maybe Mixfix, Typ, [FixrecEquation])])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [(String, Maybe Mixfix, Typ, [FixrecEquation])]
a') ->
      (ATermTable
att1, [(String, Maybe Mixfix, Typ, [FixrecEquation])] -> Sentence
Fixrec [(String, Maybe Mixfix, Typ, [FixrecEquation])]
a') }
    ShAAppl "Instantiation" [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, ([IsaClass], [[IsaClass]]))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ([IsaClass], [[IsaClass]])
b') ->
      case Int -> ATermTable -> (ATermTable, [Sentence])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [Sentence]
c') ->
      (ATermTable
att3, String -> ([IsaClass], [[IsaClass]]) -> [Sentence] -> Sentence
Instantiation String
a' ([IsaClass], [[IsaClass]])
b' [Sentence]
c') }}}
    ShAAppl "InstanceProof" [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 -> Sentence
InstanceProof String
a') }
    ShAAppl "InstanceArity" [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, ([IsaClass], [[IsaClass]]))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ([IsaClass], [[IsaClass]])
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] -> ([IsaClass], [[IsaClass]]) -> String -> Sentence
InstanceArity [String]
a' ([IsaClass], [[IsaClass]])
b' String
c') }}}
    ShAAppl "InstanceSubclass" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      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, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: String
d') ->
      (ATermTable
att4, String -> String -> String -> String -> Sentence
InstanceSubclass String
a' String
b' String
c' String
d') }}}}
    ShAAppl "Subclass" [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, Maybe QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe QName
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 -> Maybe QName -> String -> Sentence
Subclass String
a' Maybe QName
b' String
c') }}}
    ShAAppl "Typedef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, [(String, [IsaClass])])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [(String, [IsaClass])]
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Mixfix
c') ->
      case Int -> ATermTable -> (ATermTable, Maybe (QName, QName))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Maybe (QName, QName)
d') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Term
e') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: String
f') ->
      (ATermTable
att6, QName
-> [(String, [IsaClass])]
-> Maybe Mixfix
-> Maybe (QName, QName)
-> Term
-> String
-> Sentence
Typedef QName
a' [(String, [IsaClass])]
b' Maybe Mixfix
c' Maybe (QName, QName)
d' Term
e' String
f') }}}}}}
    ShAAppl "Defs" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      case Int -> ATermTable -> (ATermTable, [DefEquation])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [DefEquation]
c') ->
      (ATermTable
att3, Bool -> Bool -> [DefEquation] -> Sentence
Defs Bool
a' Bool
b' [DefEquation]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sentence)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Sentence" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.DefEquation where
  toShATermAux :: ATermTable -> DefEquation -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DefEquation
xv = case DefEquation
xv of
    DefEquation a :: QName
a b :: String
b c :: Typ
c d :: Term
d e :: String
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
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 -> Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Typ
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Term
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 String
e
      (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 "DefEquation" [Int
a', Int
b', Int
c', Int
d',
                                                Int
e'] []) ATermTable
att5
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DefEquation)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DefEquation" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
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, Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Typ
c') ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Term
d') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: String
e') ->
      (ATermTable
att5, QName -> String -> Typ -> Term -> String -> DefEquation
DefEquation QName
a' String
b' Typ
c' Term
d' String
e') }}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DefEquation)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.DefEquation" ShATerm
u

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

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

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

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

instance ShATermConvertible Isabelle.IsaSign.Datatype where
  toShATermAux :: ATermTable -> Datatype -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Datatype
xv = case Datatype
xv of
    Datatype a :: QName
a b :: [Typ]
b c :: Maybe Mixfix
c d :: [DatatypeConstructor]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Typ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Typ]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Mixfix
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [DatatypeConstructor] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [DatatypeConstructor]
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 "Datatype" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Datatype)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Datatype" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, [Typ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Typ]
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Mixfix
c') ->
      case Int -> ATermTable -> (ATermTable, [DatatypeConstructor])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [DatatypeConstructor]
d') ->
      (ATermTable
att4, QName -> [Typ] -> Maybe Mixfix -> [DatatypeConstructor] -> Datatype
Datatype QName
a' [Typ]
b' Maybe Mixfix
c' [DatatypeConstructor]
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Datatype)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Datatype" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.DatatypeConstructor where
  toShATermAux :: ATermTable -> DatatypeConstructor -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DatatypeConstructor
xv = case DatatypeConstructor
xv of
    DatatypeConstructor a :: QName
a b :: Typ
b c :: Maybe Mixfix
c d :: [Typ]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Typ -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Typ
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Mixfix
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Typ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Typ]
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 "DatatypeConstructor" [Int
a', Int
b', Int
c',
                                                        Int
d'] []) ATermTable
att4
    DatatypeNoConstructor a :: [Typ]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Typ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Typ]
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 "DatatypeNoConstructor" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DatatypeConstructor)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DatatypeConstructor" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, Typ)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Typ
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Mixfix
c') ->
      case Int -> ATermTable -> (ATermTable, [Typ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [Typ]
d') ->
      (ATermTable
att4, QName -> Typ -> Maybe Mixfix -> [Typ] -> DatatypeConstructor
DatatypeConstructor QName
a' Typ
b' Maybe Mixfix
c' [Typ]
d') }}}}
    ShAAppl "DatatypeNoConstructor" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Typ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Typ]
a') ->
      (ATermTable
att1, [Typ] -> DatatypeConstructor
DatatypeNoConstructor [Typ]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DatatypeConstructor)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.DatatypeConstructor" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.Domain where
  toShATermAux :: ATermTable -> Domain -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Domain
xv = case Domain
xv of
    Domain a :: QName
a b :: [Typ]
b c :: Maybe Mixfix
c d :: [DomainConstructor]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Typ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Typ]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe Mixfix -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe Mixfix
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [DomainConstructor] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [DomainConstructor]
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 "Domain" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Domain)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Domain" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, QName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: QName
a') ->
      case Int -> ATermTable -> (ATermTable, [Typ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Typ]
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe Mixfix)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe Mixfix
c') ->
      case Int -> ATermTable -> (ATermTable, [DomainConstructor])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [DomainConstructor]
d') ->
      (ATermTable
att4, QName -> [Typ] -> Maybe Mixfix -> [DomainConstructor] -> Domain
Domain QName
a' [Typ]
b' Maybe Mixfix
c' [DomainConstructor]
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Domain)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Domain" ShATerm
u

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

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

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

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

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

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

instance ShATermConvertible Isabelle.IsaSign.TypeSig where
  toShATermAux :: ATermTable -> TypeSig -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypeSig
xv = case TypeSig
xv of
    TySg a :: Classrel
a b :: Locales
b c :: Defs
c d :: Funs
d e :: [IsaClass]
e f :: [String]
f g :: Maybe (Typ, [IsaClass])
g h :: Abbrs
h i :: Arities
i -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Classrel -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Classrel
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Locales -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Locales
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Defs -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Defs
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Funs -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Funs
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> [IsaClass] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 [IsaClass]
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 [String]
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Maybe (Typ, [IsaClass]) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Maybe (Typ, [IsaClass])
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> Abbrs -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att7 Abbrs
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Arities -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att8 Arities
i
      (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 "TySg" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g', Int
h',
                                         Int
i'] []) ATermTable
att9
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeSig)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TySg" [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] _ ->
      case Int -> ATermTable -> (ATermTable, Classrel)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Classrel
a') ->
      case Int -> ATermTable -> (ATermTable, Locales)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Locales
b') ->
      case Int -> ATermTable -> (ATermTable, Defs)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Defs
c') ->
      case Int -> ATermTable -> (ATermTable, Funs)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Funs
d') ->
      case Int -> ATermTable -> (ATermTable, [IsaClass])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: [IsaClass]
e') ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: [String]
f') ->
      case Int -> ATermTable -> (ATermTable, Maybe (Typ, [IsaClass]))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Maybe (Typ, [IsaClass])
g') ->
      case Int -> ATermTable -> (ATermTable, Abbrs)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: Abbrs
h') ->
      case Int -> ATermTable -> (ATermTable, Arities)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: Arities
i') ->
      (ATermTable
att9, Classrel
-> Locales
-> Defs
-> Funs
-> [IsaClass]
-> [String]
-> Maybe (Typ, [IsaClass])
-> Abbrs
-> Arities
-> TypeSig
TySg Classrel
a' Locales
b' Defs
c' Funs
d' [IsaClass]
e' [String]
f' Maybe (Typ, [IsaClass])
g' Abbrs
h' Arities
i') }}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypeSig)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.TypeSig" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.BaseSig where
  toShATermAux :: ATermTable -> BaseSig -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BaseSig
xv = case BaseSig
xv of
    Main_thy -> (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 "Main_thy" [] []) ATermTable
att0
    Custom_thy -> (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 "Custom_thy" [] []) ATermTable
att0
    MainHC_thy -> (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 "MainHC_thy" [] []) ATermTable
att0
    MainHCPairs_thy -> (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 "MainHCPairs_thy" [] []) ATermTable
att0
    HOLCF_thy -> (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 "HOLCF_thy" [] []) ATermTable
att0
    HsHOLCF_thy -> (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 "HsHOLCF_thy" [] []) ATermTable
att0
    HsHOL_thy -> (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 "HsHOL_thy" [] []) ATermTable
att0
    MHsHOL_thy -> (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 "MHsHOL_thy" [] []) ATermTable
att0
    MHsHOLCF_thy -> (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 "MHsHOLCF_thy" [] []) ATermTable
att0
    CspHOLComplex_thy ->
      (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 "CspHOLComplex_thy" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, BaseSig)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Main_thy" [] _ -> (ATermTable
att0, BaseSig
Main_thy)
    ShAAppl "Custom_thy" [] _ -> (ATermTable
att0, BaseSig
Custom_thy)
    ShAAppl "MainHC_thy" [] _ -> (ATermTable
att0, BaseSig
MainHC_thy)
    ShAAppl "MainHCPairs_thy" [] _ -> (ATermTable
att0, BaseSig
MainHCPairs_thy)
    ShAAppl "HOLCF_thy" [] _ -> (ATermTable
att0, BaseSig
HOLCF_thy)
    ShAAppl "HsHOLCF_thy" [] _ -> (ATermTable
att0, BaseSig
HsHOLCF_thy)
    ShAAppl "HsHOL_thy" [] _ -> (ATermTable
att0, BaseSig
HsHOL_thy)
    ShAAppl "MHsHOL_thy" [] _ -> (ATermTable
att0, BaseSig
MHsHOL_thy)
    ShAAppl "MHsHOLCF_thy" [] _ -> (ATermTable
att0, BaseSig
MHsHOLCF_thy)
    ShAAppl "CspHOLComplex_thy" [] _ -> (ATermTable
att0, BaseSig
CspHOLComplex_thy)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BaseSig)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.BaseSig" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.Sign where
  toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
    Sign a :: String
a b :: Maybe String
b c :: [String]
c d :: [String]
d e :: BaseSig
e f :: [String]
f g :: TypeSig
g h :: ConstTab
h i :: DomainTab
i j :: Bool
j -> 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 -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe 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 -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [String]
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> BaseSig -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 BaseSig
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 [String]
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> TypeSig -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 TypeSig
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> ConstTab -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att7 ConstTab
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> DomainTab -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att8 DomainTab
i
      (att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att9 Bool
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 "Sign" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g', Int
h',
                                         Int
i', Int
j'] []) ATermTable
att10
  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, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h, i :: Int
i, j :: Int
j] _ ->
      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, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe 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, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [String]
d') ->
      case Int -> ATermTable -> (ATermTable, BaseSig)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: BaseSig
e') ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: [String]
f') ->
      case Int -> ATermTable -> (ATermTable, TypeSig)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: TypeSig
g') ->
      case Int -> ATermTable -> (ATermTable, ConstTab)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: ConstTab
h') ->
      case Int -> ATermTable -> (ATermTable, DomainTab)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: DomainTab
i') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
j ATermTable
att9 of
      { (att10 :: ATermTable
att10, j' :: Bool
j') ->
      (ATermTable
att10, String
-> Maybe String
-> [String]
-> [String]
-> BaseSig
-> [String]
-> TypeSig
-> ConstTab
-> DomainTab
-> Bool
-> Sign
Sign String
a' Maybe String
b' [String]
c' [String]
d' BaseSig
e' [String]
f' TypeSig
g' ConstTab
h' DomainTab
i' Bool
j') }}}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Sign" ShATerm
u

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

instance ShATermConvertible Isabelle.IsaSign.ProofCommand where
  toShATermAux :: ATermTable -> ProofCommand -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProofCommand
xv = case ProofCommand
xv of
    Apply a :: [ProofMethod]
a b :: Bool
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [ProofMethod] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [ProofMethod]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
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 "Apply" [Int
a', Int
b'] []) ATermTable
att2
    Using 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 "Using" [Int
a'] []) ATermTable
att1
    Back -> (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 "Back" [] []) ATermTable
att0
    Defer a :: Int
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Int
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 "Defer" [Int
a'] []) ATermTable
att1
    Prefer a :: Int
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Int
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 "Prefer" [Int
a'] []) ATermTable
att1
    Refute -> (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 "Refute" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofCommand)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Apply" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [ProofMethod])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [ProofMethod]
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      (ATermTable
att2, [ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod]
a' Bool
b') }}
    ShAAppl "Using" [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] -> ProofCommand
Using [String]
a') }
    ShAAppl "Back" [] _ -> (ATermTable
att0, ProofCommand
Back)
    ShAAppl "Defer" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      (ATermTable
att1, Int -> ProofCommand
Defer Int
a') }
    ShAAppl "Prefer" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      (ATermTable
att1, Int -> ProofCommand
Prefer Int
a') }
    ShAAppl "Refute" [] _ -> (ATermTable
att0, ProofCommand
Refute)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProofCommand)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.ProofCommand" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.ProofEnd where
  toShATermAux :: ATermTable -> ProofEnd -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProofEnd
xv = case ProofEnd
xv of
    By a :: ProofMethod
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ProofMethod -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ProofMethod
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 "By" [Int
a'] []) ATermTable
att1
    DotDot -> (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 "DotDot" [] []) ATermTable
att0
    Done -> (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 "Done" [] []) ATermTable
att0
    Oops -> (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 "Oops" [] []) ATermTable
att0
    Sorry -> (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 "Sorry" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofEnd)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "By" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, ProofMethod)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: ProofMethod
a') ->
      (ATermTable
att1, ProofMethod -> ProofEnd
By ProofMethod
a') }
    ShAAppl "DotDot" [] _ -> (ATermTable
att0, ProofEnd
DotDot)
    ShAAppl "Done" [] _ -> (ATermTable
att0, ProofEnd
Done)
    ShAAppl "Oops" [] _ -> (ATermTable
att0, ProofEnd
Oops)
    ShAAppl "Sorry" [] _ -> (ATermTable
att0, ProofEnd
Sorry)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProofEnd)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.ProofEnd" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.Modifier where
  toShATermAux :: ATermTable -> Modifier -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Modifier
xv = case Modifier
xv of
    No_asm -> (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 "No_asm" [] []) ATermTable
att0
    No_asm_simp -> (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 "No_asm_simp" [] []) ATermTable
att0
    No_asm_use -> (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 "No_asm_use" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Modifier)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "No_asm" [] _ -> (ATermTable
att0, Modifier
No_asm)
    ShAAppl "No_asm_simp" [] _ -> (ATermTable
att0, Modifier
No_asm_simp)
    ShAAppl "No_asm_use" [] _ -> (ATermTable
att0, Modifier
No_asm_use)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Modifier)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.Modifier" ShATerm
u

instance ShATermConvertible Isabelle.IsaSign.ProofMethod where
  toShATermAux :: ATermTable -> ProofMethod -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProofMethod
xv = case ProofMethod
xv of
    Auto -> (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 "Auto" [] []) ATermTable
att0
    Simp -> (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 "Simp" [] []) ATermTable
att0
    AutoSimpAdd a :: Maybe Modifier
a b :: [String]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe Modifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe Modifier
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 "AutoSimpAdd" [Int
a', Int
b'] []) ATermTable
att2
    SimpAdd a :: Maybe Modifier
a b :: [String]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe Modifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe Modifier
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 "SimpAdd" [Int
a', Int
b'] []) ATermTable
att2
    Induct a :: Term
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
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 "Induct" [Int
a'] []) ATermTable
att1
    CaseTac a :: Term
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
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 "CaseTac" [Int
a'] []) ATermTable
att1
    SubgoalTac a :: Term
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
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 "SubgoalTac" [Int
a'] []) ATermTable
att1
    Insert 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 "Insert" [Int
a'] []) ATermTable
att1
    Other 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 "Other" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofMethod)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Auto" [] _ -> (ATermTable
att0, ProofMethod
Auto)
    ShAAppl "Simp" [] _ -> (ATermTable
att0, ProofMethod
Simp)
    ShAAppl "AutoSimpAdd" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe Modifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe Modifier
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, Maybe Modifier -> [String] -> ProofMethod
AutoSimpAdd Maybe Modifier
a' [String]
b') }}
    ShAAppl "SimpAdd" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe Modifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe Modifier
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, Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
a' [String]
b') }}
    ShAAppl "Induct" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      (ATermTable
att1, Term -> ProofMethod
Induct Term
a') }
    ShAAppl "CaseTac" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      (ATermTable
att1, Term -> ProofMethod
CaseTac Term
a') }
    ShAAppl "SubgoalTac" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      (ATermTable
att1, Term -> ProofMethod
SubgoalTac Term
a') }
    ShAAppl "Insert" [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] -> ProofMethod
Insert [String]
a') }
    ShAAppl "Other" [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 -> ProofMethod
Other String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProofMethod)
forall a. String -> ShATerm -> a
fromShATermError "Isabelle.IsaSign.ProofMethod" ShATerm
u

deriving instance GHC.Generics.Generic Isabelle.IsaSign.AltSyntax
instance Data.Aeson.ToJSON Isabelle.IsaSign.AltSyntax where
instance Data.Aeson.FromJSON Isabelle.IsaSign.AltSyntax where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.VName
instance Data.Aeson.ToJSON Isabelle.IsaSign.VName where
instance Data.Aeson.FromJSON Isabelle.IsaSign.VName where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.QName
instance Data.Aeson.ToJSON Isabelle.IsaSign.QName where
instance Data.Aeson.FromJSON Isabelle.IsaSign.QName where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Indexname
instance Data.Aeson.ToJSON Isabelle.IsaSign.Indexname where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Indexname where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.IsaClass
instance Data.Aeson.ToJSON Isabelle.IsaSign.IsaClass where
instance Data.Aeson.FromJSON Isabelle.IsaSign.IsaClass where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Typ
instance Data.Aeson.ToJSON Isabelle.IsaSign.Typ where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Typ where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Continuity
instance Data.Aeson.ToJSON Isabelle.IsaSign.Continuity where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Continuity where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.TAttr
instance Data.Aeson.ToJSON Isabelle.IsaSign.TAttr where
instance Data.Aeson.FromJSON Isabelle.IsaSign.TAttr where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.DTyp
instance Data.Aeson.ToJSON Isabelle.IsaSign.DTyp where
instance Data.Aeson.FromJSON Isabelle.IsaSign.DTyp where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Term
instance Data.Aeson.ToJSON Isabelle.IsaSign.Term where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Term where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Prop
instance Data.Aeson.ToJSON Isabelle.IsaSign.Prop where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Prop where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Props
instance Data.Aeson.ToJSON Isabelle.IsaSign.Props where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Props where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Sentence
instance Data.Aeson.ToJSON Isabelle.IsaSign.Sentence where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Sentence where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.DefEquation
instance Data.Aeson.ToJSON Isabelle.IsaSign.DefEquation where
instance Data.Aeson.FromJSON Isabelle.IsaSign.DefEquation where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.FixrecEquation
instance Data.Aeson.ToJSON Isabelle.IsaSign.FixrecEquation where
instance Data.Aeson.FromJSON Isabelle.IsaSign.FixrecEquation where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Ctxt
instance Data.Aeson.ToJSON Isabelle.IsaSign.Ctxt where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Ctxt where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Mixfix
instance Data.Aeson.ToJSON Isabelle.IsaSign.Mixfix where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Mixfix where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.MixfixTemplate
instance Data.Aeson.ToJSON Isabelle.IsaSign.MixfixTemplate where
instance Data.Aeson.FromJSON Isabelle.IsaSign.MixfixTemplate where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Datatype
instance Data.Aeson.ToJSON Isabelle.IsaSign.Datatype where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Datatype where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.DatatypeConstructor
instance Data.Aeson.ToJSON Isabelle.IsaSign.DatatypeConstructor where
instance Data.Aeson.FromJSON Isabelle.IsaSign.DatatypeConstructor where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Domain
instance Data.Aeson.ToJSON Isabelle.IsaSign.Domain where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Domain where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.DomainConstructor
instance Data.Aeson.ToJSON Isabelle.IsaSign.DomainConstructor where
instance Data.Aeson.FromJSON Isabelle.IsaSign.DomainConstructor where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.DomainConstructorArg
instance Data.Aeson.ToJSON Isabelle.IsaSign.DomainConstructorArg where
instance Data.Aeson.FromJSON Isabelle.IsaSign.DomainConstructorArg where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Axiom
instance Data.Aeson.ToJSON Isabelle.IsaSign.Axiom where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Axiom where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.FunSig
instance Data.Aeson.ToJSON Isabelle.IsaSign.FunSig where
instance Data.Aeson.FromJSON Isabelle.IsaSign.FunSig where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.SetDecl
instance Data.Aeson.ToJSON Isabelle.IsaSign.SetDecl where
instance Data.Aeson.FromJSON Isabelle.IsaSign.SetDecl where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.MetaTerm
instance Data.Aeson.ToJSON Isabelle.IsaSign.MetaTerm where
instance Data.Aeson.FromJSON Isabelle.IsaSign.MetaTerm where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.TypeSig
instance Data.Aeson.ToJSON Isabelle.IsaSign.TypeSig where
instance Data.Aeson.FromJSON Isabelle.IsaSign.TypeSig where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.BaseSig
instance Data.Aeson.ToJSON Isabelle.IsaSign.BaseSig where
instance Data.Aeson.FromJSON Isabelle.IsaSign.BaseSig where

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

deriving instance GHC.Generics.Generic Isabelle.IsaSign.IsaProof
instance Data.Aeson.ToJSON Isabelle.IsaSign.IsaProof where
instance Data.Aeson.FromJSON Isabelle.IsaSign.IsaProof where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.ProofCommand
instance Data.Aeson.ToJSON Isabelle.IsaSign.ProofCommand where
instance Data.Aeson.FromJSON Isabelle.IsaSign.ProofCommand where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.ProofEnd
instance Data.Aeson.ToJSON Isabelle.IsaSign.ProofEnd where
instance Data.Aeson.FromJSON Isabelle.IsaSign.ProofEnd where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.Modifier
instance Data.Aeson.ToJSON Isabelle.IsaSign.Modifier where
instance Data.Aeson.FromJSON Isabelle.IsaSign.Modifier where

deriving instance GHC.Generics.Generic Isabelle.IsaSign.ProofMethod
instance Data.Aeson.ToJSON Isabelle.IsaSign.ProofMethod where
instance Data.Aeson.FromJSON Isabelle.IsaSign.ProofMethod where