{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  HolLight/ATC_HolLight.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):
'HolLight.Sentence.Sentence'
'HolLight.Sign.Sign'
'HolLight.Sublogic.HolLightSL'
'HolLight.Term.HolType'
'HolLight.Term.HolProof'
'HolLight.Term.HolParseType'
'HolLight.Term.HolTermInfo'
'HolLight.Term.Term'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
HolLight/Sentence.hs
HolLight/Sign.hs
HolLight/Sublogic.hs
HolLight/Term.hs
-}

module HolLight.ATC_HolLight () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.Doc
import Common.DocUtils
import Common.Json.Instances
import Common.Result
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.Maybe (fromJust, catMaybes, isNothing)
import Data.Typeable
import GHC.Generics(Generic)
import HolLight.Helper
import HolLight.Helper as Helper
import HolLight.Sentence
import HolLight.Sign
import HolLight.Sublogic
import HolLight.Term
import qualified Data.Char as Char
import qualified Data.Map as Map

{-! for HolLight.Sentence.Sentence derive : ShATermConvertible !-}
{-! for HolLight.Sign.Sign derive : ShATermConvertible !-}
{-! for HolLight.Sublogic.HolLightSL derive : ShATermConvertible !-}
{-! for HolLight.Term.HolType derive : ShATermConvertible !-}
{-! for HolLight.Term.HolProof derive : ShATermConvertible !-}
{-! for HolLight.Term.HolParseType derive : ShATermConvertible !-}
{-! for HolLight.Term.HolTermInfo derive : ShATermConvertible !-}
{-! for HolLight.Term.Term derive : ShATermConvertible !-}

{-! for HolLight.Sentence.Sentence derive : Json !-}
{-! for HolLight.Sign.Sign derive : Json !-}
{-! for HolLight.Sublogic.HolLightSL derive : Json !-}
{-! for HolLight.Term.HolType derive : Json !-}
{-! for HolLight.Term.HolProof derive : Json !-}
{-! for HolLight.Term.HolParseType derive : Json !-}
{-! for HolLight.Term.HolTermInfo derive : Json !-}
{-! for HolLight.Term.Term derive : Json !-}

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

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

instance ShATermConvertible HolLight.Sentence.Sentence where
  toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sentence
xv = case Sentence
xv of
    Sentence a :: Term
a b :: Maybe HolProof
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 -> Maybe HolProof -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe HolProof
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 "Sentence" [Int
a', Int
b'] []) ATermTable
att2
  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] _ ->
      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, Maybe HolProof)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe HolProof
b') ->
      (ATermTable
att2, Term -> Maybe HolProof -> Sentence
Sentence Term
a' Maybe HolProof
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sentence)
forall a. String -> ShATerm -> a
fromShATermError "HolLight.Sentence.Sentence" ShATerm
u

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

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

deriving instance GHC.Generics.Generic HolLight.Sublogic.HolLightSL
instance Data.Aeson.ToJSON HolLight.Sublogic.HolLightSL where
instance Data.Aeson.FromJSON HolLight.Sublogic.HolLightSL where

instance ShATermConvertible HolLight.Sublogic.HolLightSL where
  toShATermAux :: ATermTable -> HolLightSL -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: HolLightSL
xv = case HolLightSL
xv of
    Top -> (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 "Top" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, HolLightSL)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Top" [] _ -> (ATermTable
att0, HolLightSL
Top)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, HolLightSL)
forall a. String -> ShATerm -> a
fromShATermError "HolLight.Sublogic.HolLightSL" ShATerm
u

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

instance ShATermConvertible HolLight.Term.HolProof where
  toShATermAux :: ATermTable -> HolProof -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: HolProof
xv = case HolProof
xv of
    NoProof -> (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 "NoProof" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, HolProof)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "NoProof" [] _ -> (ATermTable
att0, HolProof
NoProof)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, HolProof)
forall a. String -> ShATerm -> a
fromShATermError "HolLight.Term.HolProof" ShATerm
u

instance ShATermConvertible HolLight.Term.HolParseType where
  toShATermAux :: ATermTable -> HolParseType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: HolParseType
xv = case HolParseType
xv of
    Normal -> (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 "Normal" [] []) ATermTable
att0
    PrefixT -> (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 "PrefixT" [] []) ATermTable
att0
    InfixL 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 "InfixL" [Int
a'] []) ATermTable
att1
    InfixR 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 "InfixR" [Int
a'] []) ATermTable
att1
    Binder -> (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 "Binder" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, HolParseType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Normal" [] _ -> (ATermTable
att0, HolParseType
Normal)
    ShAAppl "PrefixT" [] _ -> (ATermTable
att0, HolParseType
PrefixT)
    ShAAppl "InfixL" [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 -> HolParseType
InfixL Int
a') }
    ShAAppl "InfixR" [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 -> HolParseType
InfixR Int
a') }
    ShAAppl "Binder" [] _ -> (ATermTable
att0, HolParseType
Binder)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, HolParseType)
forall a. String -> ShATerm -> a
fromShATermError "HolLight.Term.HolParseType" ShATerm
u

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

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

deriving instance GHC.Generics.Generic HolLight.Term.HolType
instance Data.Aeson.ToJSON HolLight.Term.HolType where
instance Data.Aeson.FromJSON HolLight.Term.HolType where

deriving instance GHC.Generics.Generic HolLight.Term.HolProof
instance Data.Aeson.ToJSON HolLight.Term.HolProof where
instance Data.Aeson.FromJSON HolLight.Term.HolProof where

deriving instance GHC.Generics.Generic HolLight.Term.HolParseType
instance Data.Aeson.ToJSON HolLight.Term.HolParseType where
instance Data.Aeson.FromJSON HolLight.Term.HolParseType where

deriving instance GHC.Generics.Generic HolLight.Term.HolTermInfo
instance Data.Aeson.ToJSON HolLight.Term.HolTermInfo where
instance Data.Aeson.FromJSON HolLight.Term.HolTermInfo where

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