{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module CommonLogic.ATC_CommonLogic () where
import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation (Annoted (..))
import Common.Doc
import Common.DocUtils
import Common.IRI
import Common.Id
import Common.Id as Id
import Common.Json.Instances
import Common.Keywords
import Common.Result
import CommonLogic.AS_CommonLogic
import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Morphism
import CommonLogic.Morphism as Morphism
import CommonLogic.Sign
import CommonLogic.Sign as Sign
import CommonLogic.Sublogic
import CommonLogic.Symbol
import CommonLogic.Tools
import Control.Monad (unless)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.Function
import Data.List (isPrefixOf)
import Data.Set (Set)
import GHC.Generics(Generic)
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified CommonLogic.Sign as Sign
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set
instance ShATermConvertible CommonLogic.AS_CommonLogic.BASIC_SPEC where
toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_SPEC
xv = case BASIC_SPEC
xv of
Basic_spec a :: [Annoted BASIC_ITEMS]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted BASIC_ITEMS] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted BASIC_ITEMS]
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Basic_spec" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Basic_spec" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Annoted BASIC_ITEMS])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Annoted BASIC_ITEMS]
a') ->
(ATermTable
att1, [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec [Annoted BASIC_ITEMS]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.BASIC_SPEC" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.BASIC_ITEMS where
toShATermAux :: ATermTable -> BASIC_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_ITEMS
xv = case BASIC_ITEMS
xv of
Axiom_items a :: [Annoted TEXT_META]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted TEXT_META] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted TEXT_META]
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 "Axiom_items" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Axiom_items" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Annoted TEXT_META])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Annoted TEXT_META]
a') ->
(ATermTable
att1, [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items [Annoted TEXT_META]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.BASIC_ITEMS" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.TEXT_META where
toShATermAux :: ATermTable -> TEXT_META -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TEXT_META
xv = case TEXT_META
xv of
Text_meta a :: TEXT
a b :: Maybe IRI
b c :: Maybe (Set NAME)
c d :: [PrefixMapping]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TEXT
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe IRI -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe IRI
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe (Set NAME) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe (Set NAME)
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [PrefixMapping] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [PrefixMapping]
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 "Text_meta" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, TEXT_META)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Text_meta" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, TEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TEXT
a') ->
case Int -> ATermTable -> (ATermTable, Maybe IRI)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Maybe IRI
b') ->
case Int -> ATermTable -> (ATermTable, Maybe (Set NAME))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Maybe (Set NAME)
c') ->
case Int -> ATermTable -> (ATermTable, [PrefixMapping])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [PrefixMapping]
d') ->
(ATermTable
att4, TEXT
-> Maybe IRI -> Maybe (Set NAME) -> [PrefixMapping] -> TEXT_META
Text_meta TEXT
a' Maybe IRI
b' Maybe (Set NAME)
c' [PrefixMapping]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TEXT_META)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.TEXT_META" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.TEXT where
toShATermAux :: ATermTable -> TEXT -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TEXT
xv = case TEXT
xv of
Text a :: [PHRASE]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [PHRASE] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [PHRASE]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "Text" [Int
a', Int
b'] []) ATermTable
att2
Named_text a :: NAME
a b :: TEXT
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TEXT
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Named_text" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, TEXT)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Text" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [PHRASE])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [PHRASE]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [PHRASE] -> Range -> TEXT
Text [PHRASE]
a' Range
b') }}
ShAAppl "Named_text" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, TEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: TEXT
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, NAME -> TEXT -> Range -> TEXT
Named_text NAME
a' TEXT
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TEXT)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.TEXT" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.PHRASE where
toShATermAux :: ATermTable -> PHRASE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PHRASE
xv = case PHRASE
xv of
Module a :: MODULE
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MODULE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 MODULE
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 "Module" [Int
a'] []) ATermTable
att1
Sentence a :: SENTENCE
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SENTENCE
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 "Sentence" [Int
a'] []) ATermTable
att1
Importation a :: IMPORTATION
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IMPORTATION -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 IMPORTATION
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 "Importation" [Int
a'] []) ATermTable
att1
Comment_text a :: COMMENT
a b :: TEXT
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> COMMENT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 COMMENT
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TEXT
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Comment_text" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, PHRASE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Module" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, MODULE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: MODULE
a') ->
(ATermTable
att1, MODULE -> PHRASE
Module MODULE
a') }
ShAAppl "Sentence" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SENTENCE
a') ->
(ATermTable
att1, SENTENCE -> PHRASE
Sentence SENTENCE
a') }
ShAAppl "Importation" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, IMPORTATION)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: IMPORTATION
a') ->
(ATermTable
att1, IMPORTATION -> PHRASE
Importation IMPORTATION
a') }
ShAAppl "Comment_text" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, COMMENT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: COMMENT
a') ->
case Int -> ATermTable -> (ATermTable, TEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: TEXT
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, COMMENT -> TEXT -> Range -> PHRASE
Comment_text COMMENT
a' TEXT
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PHRASE)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.PHRASE" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.COMMENT where
toShATermAux :: ATermTable -> COMMENT -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: COMMENT
xv = case COMMENT
xv of
Comment a :: String
a b :: Range
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "Comment" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, COMMENT)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Comment" [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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, String -> Range -> COMMENT
Comment String
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, COMMENT)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.COMMENT" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.MODULE where
toShATermAux :: ATermTable -> MODULE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: MODULE
xv = case MODULE
xv of
Mod a :: NAME
a b :: TEXT
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TEXT
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Mod" [Int
a', Int
b', Int
c'] []) ATermTable
att3
Mod_ex a :: NAME
a b :: [NAME]
b c :: TEXT
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [NAME] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [NAME]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TEXT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TEXT
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
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 "Mod_ex" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, MODULE)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Mod" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, TEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: TEXT
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, NAME -> TEXT -> Range -> MODULE
Mod NAME
a' TEXT
b' Range
c') }}}
ShAAppl "Mod_ex" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, [NAME])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [NAME]
b') ->
case Int -> ATermTable -> (ATermTable, TEXT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TEXT
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, NAME -> [NAME] -> TEXT -> Range -> MODULE
Mod_ex NAME
a' [NAME]
b' TEXT
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MODULE)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.MODULE" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.IMPORTATION where
toShATermAux :: ATermTable -> IMPORTATION -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: IMPORTATION
xv = case IMPORTATION
xv of
Imp_name a :: NAME
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
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 "Imp_name" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, IMPORTATION)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Imp_name" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
(ATermTable
att1, NAME -> IMPORTATION
Imp_name NAME
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, IMPORTATION)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.IMPORTATION" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.SENTENCE where
toShATermAux :: ATermTable -> SENTENCE -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SENTENCE
xv = case SENTENCE
xv of
Quant_sent a :: QUANT
a b :: [NAME_OR_SEQMARK]
b c :: SENTENCE
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> QUANT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 QUANT
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [NAME_OR_SEQMARK] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [NAME_OR_SEQMARK]
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
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
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 "Quant_sent" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
Bool_sent a :: BOOL_SENT
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BOOL_SENT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 BOOL_SENT
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "Bool_sent" [Int
a', Int
b'] []) ATermTable
att2
Atom_sent a :: ATOM
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ATOM -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ATOM
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "Atom_sent" [Int
a', Int
b'] []) ATermTable
att2
Comment_sent a :: COMMENT
a b :: SENTENCE
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> COMMENT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 COMMENT
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SENTENCE
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Comment_sent" [Int
a', Int
b', Int
c'] []) ATermTable
att3
Irregular_sent a :: SENTENCE
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SENTENCE
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "Irregular_sent" [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 "Quant_sent" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, QUANT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: QUANT
a') ->
case Int -> ATermTable -> (ATermTable, [NAME_OR_SEQMARK])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [NAME_OR_SEQMARK]
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') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
a' [NAME_OR_SEQMARK]
b' SENTENCE
c' Range
d') }}}}
ShAAppl "Bool_sent" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, BOOL_SENT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: BOOL_SENT
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, BOOL_SENT -> Range -> SENTENCE
Bool_sent BOOL_SENT
a' Range
b') }}
ShAAppl "Atom_sent" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, ATOM)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ATOM
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, ATOM -> Range -> SENTENCE
Atom_sent ATOM
a' Range
b') }}
ShAAppl "Comment_sent" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, COMMENT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: COMMENT
a') ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: SENTENCE
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, COMMENT -> SENTENCE -> Range -> SENTENCE
Comment_sent COMMENT
a' SENTENCE
b' Range
c') }}}
ShAAppl "Irregular_sent" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SENTENCE
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, SENTENCE -> Range -> SENTENCE
Irregular_sent SENTENCE
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SENTENCE)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.SENTENCE" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.QUANT where
toShATermAux :: ATermTable -> QUANT -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: QUANT
xv = case QUANT
xv of
Universal -> (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 "Universal" [] []) ATermTable
att0
Existential -> (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 "Existential" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, QUANT)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Universal" [] _ -> (ATermTable
att0, QUANT
Universal)
ShAAppl "Existential" [] _ -> (ATermTable
att0, QUANT
Existential)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, QUANT)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.QUANT" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.BOOL_SENT where
toShATermAux :: ATermTable -> BOOL_SENT -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BOOL_SENT
xv = case BOOL_SENT
xv of
Junction a :: AndOr
a b :: [SENTENCE]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> AndOr -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 AndOr
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SENTENCE] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SENTENCE]
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 "Junction" [Int
a', Int
b'] []) ATermTable
att2
Negation a :: SENTENCE
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SENTENCE
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 "Negation" [Int
a'] []) ATermTable
att1
BinOp a :: ImplEq
a b :: SENTENCE
b c :: SENTENCE
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ImplEq -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ImplEq
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SENTENCE
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 "BinOp" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, BOOL_SENT)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Junction" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, AndOr)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: AndOr
a') ->
case Int -> ATermTable -> (ATermTable, [SENTENCE])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [SENTENCE]
b') ->
(ATermTable
att2, AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
a' [SENTENCE]
b') }}
ShAAppl "Negation" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SENTENCE
a') ->
(ATermTable
att1, SENTENCE -> BOOL_SENT
Negation SENTENCE
a') }
ShAAppl "BinOp" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, ImplEq)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ImplEq
a') ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: SENTENCE
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, ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
a' SENTENCE
b' SENTENCE
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BOOL_SENT)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.BOOL_SENT" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.AndOr where
toShATermAux :: ATermTable -> AndOr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AndOr
xv = case AndOr
xv of
Conjunction -> (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 "Conjunction" [] []) ATermTable
att0
Disjunction -> (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 "Disjunction" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, AndOr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Conjunction" [] _ -> (ATermTable
att0, AndOr
Conjunction)
ShAAppl "Disjunction" [] _ -> (ATermTable
att0, AndOr
Disjunction)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AndOr)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.AndOr" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.ImplEq where
toShATermAux :: ATermTable -> ImplEq -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ImplEq
xv = case ImplEq
xv of
Implication -> (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 "Implication" [] []) ATermTable
att0
Biconditional -> (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 "Biconditional" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, ImplEq)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Implication" [] _ -> (ATermTable
att0, ImplEq
Implication)
ShAAppl "Biconditional" [] _ -> (ATermTable
att0, ImplEq
Biconditional)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ImplEq)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.ImplEq" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.ATOM where
toShATermAux :: ATermTable -> ATOM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ATOM
xv = case ATOM
xv of
Equation 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 "Equation" [Int
a', Int
b'] []) ATermTable
att2
Atom a :: TERM
a b :: [TERM_SEQ]
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_SEQ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TERM_SEQ]
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 "Atom" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, ATOM)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Equation" [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 -> ATOM
Equation TERM
a' TERM
b') }}
ShAAppl "Atom" [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_SEQ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [TERM_SEQ]
b') ->
(ATermTable
att2, TERM -> [TERM_SEQ] -> ATOM
Atom TERM
a' [TERM_SEQ]
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ATOM)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.ATOM" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.TERM where
toShATermAux :: ATermTable -> TERM -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TERM
xv = case TERM
xv of
Name_term a :: NAME
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
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 "Name_term" [Int
a'] []) ATermTable
att1
Funct_term a :: TERM
a b :: [TERM_SEQ]
b c :: Range
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_SEQ] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TERM_SEQ]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Funct_term" [Int
a', Int
b', Int
c'] []) ATermTable
att3
Comment_term a :: TERM
a b :: COMMENT
b c :: Range
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 -> COMMENT -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 COMMENT
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Comment_term" [Int
a', Int
b', Int
c'] []) ATermTable
att3
That_term a :: SENTENCE
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SENTENCE -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SENTENCE
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
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 "That_term" [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 "Name_term" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
(ATermTable
att1, NAME -> TERM
Name_term NAME
a') }
ShAAppl "Funct_term" [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_SEQ])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [TERM_SEQ]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
a' [TERM_SEQ]
b' Range
c') }}}
ShAAppl "Comment_term" [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, COMMENT)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: COMMENT
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, TERM -> COMMENT -> Range -> TERM
Comment_term TERM
a' COMMENT
b' Range
c') }}}
ShAAppl "That_term" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, SENTENCE)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SENTENCE
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, SENTENCE -> Range -> TERM
That_term SENTENCE
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TERM)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.TERM" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.TERM_SEQ where
toShATermAux :: ATermTable -> TERM_SEQ -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TERM_SEQ
xv = case TERM_SEQ
xv of
Term_seq 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_seq" [Int
a'] []) ATermTable
att1
Seq_marks a :: NAME
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
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 "Seq_marks" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TERM_SEQ)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Term_seq" [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 -> TERM_SEQ
Term_seq TERM
a') }
ShAAppl "Seq_marks" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
(ATermTable
att1, NAME -> TERM_SEQ
Seq_marks NAME
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TERM_SEQ)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.TERM_SEQ" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK where
toShATermAux :: ATermTable -> NAME_OR_SEQMARK -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: NAME_OR_SEQMARK
xv = case NAME_OR_SEQMARK
xv of
Name a :: NAME
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
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 "Name" [Int
a'] []) ATermTable
att1
SeqMark a :: NAME
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
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 "SeqMark" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, NAME_OR_SEQMARK)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Name" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
(ATermTable
att1, NAME -> NAME_OR_SEQMARK
Name NAME
a') }
ShAAppl "SeqMark" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
(ATermTable
att1, NAME -> NAME_OR_SEQMARK
SeqMark NAME
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, NAME_OR_SEQMARK)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS where
toShATermAux :: ATermTable -> SYMB_MAP_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_MAP_ITEMS
xv = case SYMB_MAP_ITEMS
xv of
Symb_map_items a :: [SYMB_OR_MAP]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SYMB_OR_MAP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SYMB_OR_MAP]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Symb_map_items" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_MAP_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb_map_items" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [SYMB_OR_MAP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [SYMB_OR_MAP]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [SYMB_OR_MAP] -> Range -> SYMB_MAP_ITEMS
Symb_map_items [SYMB_OR_MAP]
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_MAP_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.SYMB_OR_MAP where
toShATermAux :: ATermTable -> SYMB_OR_MAP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_OR_MAP
xv = case SYMB_OR_MAP
xv of
Symb a :: NAME_OR_SEQMARK
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME_OR_SEQMARK -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME_OR_SEQMARK
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Symb" [Int
a'] []) ATermTable
att1
Symb_mapN a :: NAME
a b :: NAME
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 NAME
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Symb_mapN" [Int
a', Int
b', Int
c'] []) ATermTable
att3
Symb_mapS a :: NAME
a b :: NAME
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NAME
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NAME -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 NAME
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
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 "Symb_mapS" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_OR_MAP)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, NAME_OR_SEQMARK)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME_OR_SEQMARK
a') ->
(ATermTable
att1, NAME_OR_SEQMARK -> SYMB_OR_MAP
Symb NAME_OR_SEQMARK
a') }
ShAAppl "Symb_mapN" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: NAME
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, NAME -> NAME -> Range -> SYMB_OR_MAP
Symb_mapN NAME
a' NAME
b' Range
c') }}}
ShAAppl "Symb_mapS" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NAME
a') ->
case Int -> ATermTable -> (ATermTable, NAME)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: NAME
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, NAME -> NAME -> Range -> SYMB_OR_MAP
Symb_mapS NAME
a' NAME
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_OR_MAP)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.SYMB_OR_MAP" ShATerm
u
instance ShATermConvertible CommonLogic.AS_CommonLogic.SYMB_ITEMS where
toShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SYMB_ITEMS
xv = case SYMB_ITEMS
xv of
Symb_items a :: [NAME_OR_SEQMARK]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [NAME_OR_SEQMARK] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [NAME_OR_SEQMARK]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Symb_items" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb_items" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [NAME_OR_SEQMARK])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [NAME_OR_SEQMARK]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [NAME_OR_SEQMARK] -> Range -> SYMB_ITEMS
Symb_items [NAME_OR_SEQMARK]
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SYMB_ITEMS)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.AS_CommonLogic.SYMB_ITEMS" ShATerm
u
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.BASIC_SPEC
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.BASIC_SPEC where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.BASIC_SPEC where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.BASIC_ITEMS
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.BASIC_ITEMS where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.BASIC_ITEMS where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.TEXT_META
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.TEXT_META where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.TEXT_META where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.TEXT
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.TEXT where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.TEXT where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.PHRASE
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.PHRASE where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.PHRASE where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.COMMENT
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.COMMENT where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.COMMENT where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.MODULE
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.MODULE where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.MODULE where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.IMPORTATION
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.IMPORTATION where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.IMPORTATION where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.SENTENCE
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.SENTENCE where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.SENTENCE where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.QUANT
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.QUANT where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.QUANT where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.BOOL_SENT
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.BOOL_SENT where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.BOOL_SENT where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.AndOr
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.AndOr where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.AndOr where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.ImplEq
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.ImplEq where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.ImplEq where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.ATOM
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.ATOM where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.ATOM where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.TERM
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.TERM where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.TERM where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.TERM_SEQ
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.TERM_SEQ where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.TERM_SEQ where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.NAME_OR_SEQMARK where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.SYMB_MAP_ITEMS where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.SYMB_OR_MAP
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.SYMB_OR_MAP where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.SYMB_OR_MAP where
deriving instance GHC.Generics.Generic CommonLogic.AS_CommonLogic.SYMB_ITEMS
instance Data.Aeson.ToJSON CommonLogic.AS_CommonLogic.SYMB_ITEMS where
instance Data.Aeson.FromJSON CommonLogic.AS_CommonLogic.SYMB_ITEMS where
instance ShATermConvertible CommonLogic.Morphism.Morphism where
toShATermAux :: ATermTable -> Morphism -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Morphism
xv = case Morphism
xv of
Morphism a :: Sign
a b :: Sign
b c :: Map Id Id
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sign
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sign
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Map Id Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Map Id Id
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 "Morphism" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Morphism" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sign
a') ->
case Int -> ATermTable -> (ATermTable, Sign)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sign
b') ->
case Int -> ATermTable -> (ATermTable, Map Id Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Map Id Id
c') ->
(ATermTable
att3, Sign -> Sign -> Map Id Id -> Morphism
Morphism Sign
a' Sign
b' Map Id Id
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.Morphism.Morphism" ShATerm
u
deriving instance GHC.Generics.Generic CommonLogic.Morphism.Morphism
instance Data.Aeson.ToJSON CommonLogic.Morphism.Morphism where
instance Data.Aeson.FromJSON CommonLogic.Morphism.Morphism where
instance ShATermConvertible CommonLogic.Sign.Sign where
toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
Sign a :: Set Id
a b :: Set Id
b c :: Set Id
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Set Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Set Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Set Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Set Id
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Set Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Set Id
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sign" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Sign" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Set Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Set Id
a') ->
case Int -> ATermTable -> (ATermTable, Set Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Set Id
b') ->
case Int -> ATermTable -> (ATermTable, Set Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Set Id
c') ->
(ATermTable
att3, Set Id -> Set Id -> Set Id -> Sign
Sign Set Id
a' Set Id
b' Set Id
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.Sign.Sign" ShATerm
u
deriving instance GHC.Generics.Generic CommonLogic.Sign.Sign
instance Data.Aeson.ToJSON CommonLogic.Sign.Sign where
instance Data.Aeson.FromJSON CommonLogic.Sign.Sign where
instance ShATermConvertible CommonLogic.Sublogic.CLTextType where
toShATermAux :: ATermTable -> CLTextType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CLTextType
xv = case CLTextType
xv of
Propositional -> (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 "Propositional" [] []) ATermTable
att0
FirstOrder -> (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 "FirstOrder" [] []) ATermTable
att0
Impredicative -> (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 "Impredicative" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, CLTextType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Propositional" [] _ -> (ATermTable
att0, CLTextType
Propositional)
ShAAppl "FirstOrder" [] _ -> (ATermTable
att0, CLTextType
FirstOrder)
ShAAppl "Impredicative" [] _ -> (ATermTable
att0, CLTextType
Impredicative)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CLTextType)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.Sublogic.CLTextType" ShATerm
u
instance ShATermConvertible CommonLogic.Sublogic.CommonLogicSL where
toShATermAux :: ATermTable -> CommonLogicSL -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CommonLogicSL
xv = case CommonLogicSL
xv of
CommonLogicSL a :: CLTextType
a b :: Bool
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> CLTextType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 CLTextType
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 "CommonLogicSL" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, CommonLogicSL)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "CommonLogicSL" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, CLTextType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: CLTextType
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, CLTextType -> Bool -> CommonLogicSL
CommonLogicSL CLTextType
a' Bool
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CommonLogicSL)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.Sublogic.CommonLogicSL" ShATerm
u
deriving instance GHC.Generics.Generic CommonLogic.Sublogic.CLTextType
instance Data.Aeson.ToJSON CommonLogic.Sublogic.CLTextType where
instance Data.Aeson.FromJSON CommonLogic.Sublogic.CLTextType where
deriving instance GHC.Generics.Generic CommonLogic.Sublogic.CommonLogicSL
instance Data.Aeson.ToJSON CommonLogic.Sublogic.CommonLogicSL where
instance Data.Aeson.FromJSON CommonLogic.Sublogic.CommonLogicSL where
deriving instance GHC.Generics.Generic CommonLogic.Symbol.Symbol
instance Data.Aeson.ToJSON CommonLogic.Symbol.Symbol where
instance Data.Aeson.FromJSON CommonLogic.Symbol.Symbol where
instance ShATermConvertible CommonLogic.Symbol.Symbol where
toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symbol
xv = case Symbol
xv of
Symbol a :: Id
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
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 "Symbol" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symbol" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
(ATermTable
att1, Id -> Symbol
Symbol Id
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symbol)
forall a. String -> ShATerm -> a
fromShATermError "CommonLogic.Symbol.Symbol" ShATerm
u