{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module Maude.ATC_Maude () where
import ATC.AS_Annotation
import ATerm.Lib
import Common.Doc
import Common.Doc (specBraces, text)
import Common.Doc (vcat)
import Common.Doc hiding (empty)
import Common.DocUtils (Pretty (..))
import Common.Id (Id, mkId, mkSimpleId, GetRange, getRange, nullRange)
import Common.Id (mkSimpleId, GetRange)
import Common.Id hiding (Id)
import Common.Json.Instances
import Common.Lib.Rel (Rel)
import Common.Result (Result)
import Common.Utils (nubOrd)
import Control.Monad (unless)
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List (partition)
import Data.Map (Map)
import Data.Maybe (fromJust)
import Data.Set (Set)
import GHC.Generics(Generic)
import Maude.AS_Maude
import Maude.Meta
import Maude.Meta.HasName
import Maude.Morphism
import Maude.Printing ()
import Maude.Sentence
import Maude.Sentence (Sentence)
import Maude.Sign
import Maude.Sign (Sign, kindRel, KindRel)
import Maude.Symbol
import Maude.Util
import qualified Common.Doc as Doc
import qualified Common.Lib.Rel as Rel
import qualified Control.Monad.Fail as Fail
import qualified Data.Foldable as Fold
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Maude.Sentence as Sen
import qualified Maude.Sign as Sign
deriving instance GHC.Generics.Generic Maude.AS_Maude.OpId
instance Data.Aeson.ToJSON Maude.AS_Maude.OpId where
instance Data.Aeson.FromJSON Maude.AS_Maude.OpId where
deriving instance GHC.Generics.Generic Maude.AS_Maude.LabelId
instance Data.Aeson.ToJSON Maude.AS_Maude.LabelId where
instance Data.Aeson.FromJSON Maude.AS_Maude.LabelId where
deriving instance GHC.Generics.Generic Maude.AS_Maude.ModId
instance Data.Aeson.ToJSON Maude.AS_Maude.ModId where
instance Data.Aeson.FromJSON Maude.AS_Maude.ModId where
deriving instance GHC.Generics.Generic Maude.AS_Maude.ViewId
instance Data.Aeson.ToJSON Maude.AS_Maude.ViewId where
instance Data.Aeson.FromJSON Maude.AS_Maude.ViewId where
deriving instance GHC.Generics.Generic Maude.AS_Maude.ParamId
instance Data.Aeson.ToJSON Maude.AS_Maude.ParamId where
instance Data.Aeson.FromJSON Maude.AS_Maude.ParamId where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Kind
instance Data.Aeson.ToJSON Maude.AS_Maude.Kind where
instance Data.Aeson.FromJSON Maude.AS_Maude.Kind where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Sort
instance Data.Aeson.ToJSON Maude.AS_Maude.Sort where
instance Data.Aeson.FromJSON Maude.AS_Maude.Sort where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Type
instance Data.Aeson.ToJSON Maude.AS_Maude.Type where
instance Data.Aeson.FromJSON Maude.AS_Maude.Type where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Term
instance Data.Aeson.ToJSON Maude.AS_Maude.Term where
instance Data.Aeson.FromJSON Maude.AS_Maude.Term where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Hook
instance Data.Aeson.ToJSON Maude.AS_Maude.Hook where
instance Data.Aeson.FromJSON Maude.AS_Maude.Hook where
deriving instance GHC.Generics.Generic Maude.AS_Maude.StmntAttr
instance Data.Aeson.ToJSON Maude.AS_Maude.StmntAttr where
instance Data.Aeson.FromJSON Maude.AS_Maude.StmntAttr where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Attr
instance Data.Aeson.ToJSON Maude.AS_Maude.Attr where
instance Data.Aeson.FromJSON Maude.AS_Maude.Attr where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Condition
instance Data.Aeson.ToJSON Maude.AS_Maude.Condition where
instance Data.Aeson.FromJSON Maude.AS_Maude.Condition where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Rule
instance Data.Aeson.ToJSON Maude.AS_Maude.Rule where
instance Data.Aeson.FromJSON Maude.AS_Maude.Rule where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Equation
instance Data.Aeson.ToJSON Maude.AS_Maude.Equation where
instance Data.Aeson.FromJSON Maude.AS_Maude.Equation where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Membership
instance Data.Aeson.ToJSON Maude.AS_Maude.Membership where
instance Data.Aeson.FromJSON Maude.AS_Maude.Membership where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Operator
instance Data.Aeson.ToJSON Maude.AS_Maude.Operator where
instance Data.Aeson.FromJSON Maude.AS_Maude.Operator where
deriving instance GHC.Generics.Generic Maude.AS_Maude.SubsortDecl
instance Data.Aeson.ToJSON Maude.AS_Maude.SubsortDecl where
instance Data.Aeson.FromJSON Maude.AS_Maude.SubsortDecl where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Import
instance Data.Aeson.ToJSON Maude.AS_Maude.Import where
instance Data.Aeson.FromJSON Maude.AS_Maude.Import where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Statement
instance Data.Aeson.ToJSON Maude.AS_Maude.Statement where
instance Data.Aeson.FromJSON Maude.AS_Maude.Statement where
deriving instance GHC.Generics.Generic Maude.AS_Maude.ToPartRenaming
instance Data.Aeson.ToJSON Maude.AS_Maude.ToPartRenaming where
instance Data.Aeson.FromJSON Maude.AS_Maude.ToPartRenaming where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Renaming
instance Data.Aeson.ToJSON Maude.AS_Maude.Renaming where
instance Data.Aeson.FromJSON Maude.AS_Maude.Renaming where
deriving instance GHC.Generics.Generic Maude.AS_Maude.ModExp
instance Data.Aeson.ToJSON Maude.AS_Maude.ModExp where
instance Data.Aeson.FromJSON Maude.AS_Maude.ModExp where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Parameter
instance Data.Aeson.ToJSON Maude.AS_Maude.Parameter where
instance Data.Aeson.FromJSON Maude.AS_Maude.Parameter where
deriving instance GHC.Generics.Generic Maude.AS_Maude.View
instance Data.Aeson.ToJSON Maude.AS_Maude.View where
instance Data.Aeson.FromJSON Maude.AS_Maude.View where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Module
instance Data.Aeson.ToJSON Maude.AS_Maude.Module where
instance Data.Aeson.FromJSON Maude.AS_Maude.Module where
deriving instance GHC.Generics.Generic Maude.AS_Maude.Spec
instance Data.Aeson.ToJSON Maude.AS_Maude.Spec where
instance Data.Aeson.FromJSON Maude.AS_Maude.Spec where
deriving instance GHC.Generics.Generic Maude.AS_Maude.MaudeText
instance Data.Aeson.ToJSON Maude.AS_Maude.MaudeText where
instance Data.Aeson.FromJSON Maude.AS_Maude.MaudeText where
instance ShATermConvertible Maude.AS_Maude.OpId where
toShATermAux :: ATermTable -> OpId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OpId
xv = case OpId
xv of
OpId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "OpId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, OpId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "OpId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> OpId
OpId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OpId)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.OpId" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.LabelId where
toShATermAux :: ATermTable -> LabelId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: LabelId
xv = case LabelId
xv of
LabelId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "LabelId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, LabelId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "LabelId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> LabelId
LabelId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, LabelId)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.LabelId" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.ModId where
toShATermAux :: ATermTable -> ModId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ModId
xv = case ModId
xv of
ModId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "ModId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, ModId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ModId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> ModId
ModId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ModId)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.ModId" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.ViewId where
toShATermAux :: ATermTable -> ViewId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ViewId
xv = case ViewId
xv of
ViewId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "ViewId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, ViewId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ViewId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> ViewId
ViewId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ViewId)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.ViewId" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.ParamId where
toShATermAux :: ATermTable -> ParamId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ParamId
xv = case ParamId
xv of
ParamId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "ParamId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, ParamId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ParamId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> ParamId
ParamId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ParamId)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.ParamId" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Kind where
toShATermAux :: ATermTable -> Kind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Kind
xv = case Kind
xv of
KindId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "KindId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Kind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "KindId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Kind
KindId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Kind)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Kind" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Sort where
toShATermAux :: ATermTable -> Sort -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sort
xv = case Sort
xv of
SortId a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "SortId" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Sort)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SortId" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Sort
SortId Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sort)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Sort" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Type where
toShATermAux :: ATermTable -> Type -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Type
xv = case Type
xv of
TypeSort a :: Sort
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sort
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 "TypeSort" [Int
a'] []) ATermTable
att1
TypeKind a :: Kind
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Kind
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 "TypeKind" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Type)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TypeSort" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sort
a') ->
(ATermTable
att1, Sort -> Type
TypeSort Sort
a') }
ShAAppl "TypeKind" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Kind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Kind
a') ->
(ATermTable
att1, Kind -> Type
TypeKind Kind
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Type)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Type" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Term where
toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Term
xv = case Term
xv of
Const a :: Qid
a b :: Type
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Type
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Const" [Int
a', Int
b'] []) ATermTable
att2
Var a :: Qid
a b :: Type
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Type
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 "Var" [Int
a', Int
b'] []) ATermTable
att2
Apply a :: Qid
a b :: [Term]
b c :: Type
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Term] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Term]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Type
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 "Apply" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Term)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Const" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Type
b') ->
(ATermTable
att2, Qid -> Type -> Term
Const Qid
a' Type
b') }}
ShAAppl "Var" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Type
b') ->
(ATermTable
att2, Qid -> Type -> Term
Var Qid
a' Type
b') }}
ShAAppl "Apply" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Term]
b') ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Type
c') ->
(ATermTable
att3, Qid -> [Term] -> Type -> Term
Apply Qid
a' [Term]
b' Type
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Term)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Term" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Hook where
toShATermAux :: ATermTable -> Hook -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Hook
xv = case Hook
xv of
IdHook a :: Qid
a b :: [Qid]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Qid] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Qid]
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 "IdHook" [Int
a', Int
b'] []) ATermTable
att2
OpHook a :: Qid
a b :: Qid
b c :: [Qid]
c d :: Qid
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Qid
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Qid] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Qid]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Qid
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 "OpHook" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
TermHook a :: Qid
a b :: Term
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "TermHook" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Hook)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "IdHook" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, [Qid])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Qid]
b') ->
(ATermTable
att2, Qid -> [Qid] -> Hook
IdHook Qid
a' [Qid]
b') }}
ShAAppl "OpHook" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Qid
b') ->
case Int -> ATermTable -> (ATermTable, [Qid])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Qid]
c') ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Qid
d') ->
(ATermTable
att4, Qid -> Qid -> [Qid] -> Qid -> Hook
OpHook Qid
a' Qid
b' [Qid]
c' Qid
d') }}}}
ShAAppl "TermHook" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
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, Qid -> Term -> Hook
TermHook Qid
a' Term
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Hook)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Hook" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.StmntAttr where
toShATermAux :: ATermTable -> StmntAttr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: StmntAttr
xv = case StmntAttr
xv of
Label a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "Label" [Int
a'] []) ATermTable
att1
Metadata 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 "Metadata" [Int
a'] []) ATermTable
att1
Owise -> (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 "Owise" [] []) ATermTable
att0
Nonexec -> (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 "Nonexec" [] []) ATermTable
att0
Print a :: [Qid]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Qid] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Qid]
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 "Print" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, StmntAttr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Label" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> StmntAttr
Label Qid
a') }
ShAAppl "Metadata" [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 -> StmntAttr
Metadata String
a') }
ShAAppl "Owise" [] _ -> (ATermTable
att0, StmntAttr
Owise)
ShAAppl "Nonexec" [] _ -> (ATermTable
att0, StmntAttr
Nonexec)
ShAAppl "Print" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Qid])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Qid]
a') ->
(ATermTable
att1, [Qid] -> StmntAttr
Print [Qid]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, StmntAttr)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.StmntAttr" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Attr where
toShATermAux :: ATermTable -> Attr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Attr
xv = case Attr
xv of
Assoc -> (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 "Assoc" [] []) ATermTable
att0
Comm -> (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 "Comm" [] []) ATermTable
att0
Idem -> (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 "Idem" [] []) ATermTable
att0
Iter -> (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 "Iter" [] []) ATermTable
att0
Id 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 "Id" [Int
a'] []) ATermTable
att1
LeftId 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 "LeftId" [Int
a'] []) ATermTable
att1
RightId 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 "RightId" [Int
a'] []) ATermTable
att1
Strat 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 "Strat" [Int
a'] []) ATermTable
att1
Memo -> (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 "Memo" [] []) ATermTable
att0
Prec 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 "Prec" [Int
a'] []) ATermTable
att1
Gather a :: [Qid]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Qid] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Qid]
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 "Gather" [Int
a'] []) ATermTable
att1
Format a :: [Qid]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Qid] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Qid]
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 "Format" [Int
a'] []) ATermTable
att1
Ctor -> (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 "Ctor" [] []) ATermTable
att0
Config -> (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 "Config" [] []) ATermTable
att0
Object -> (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 "Object" [] []) ATermTable
att0
Msg -> (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 "Msg" [] []) ATermTable
att0
Frozen 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 "Frozen" [Int
a'] []) ATermTable
att1
Poly 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 "Poly" [Int
a'] []) ATermTable
att1
Special a :: [Hook]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Hook] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Hook]
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 "Special" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Attr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Assoc" [] _ -> (ATermTable
att0, Attr
Assoc)
ShAAppl "Comm" [] _ -> (ATermTable
att0, Attr
Comm)
ShAAppl "Idem" [] _ -> (ATermTable
att0, Attr
Idem)
ShAAppl "Iter" [] _ -> (ATermTable
att0, Attr
Iter)
ShAAppl "Id" [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 -> Attr
Id Term
a') }
ShAAppl "LeftId" [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 -> Attr
LeftId Term
a') }
ShAAppl "RightId" [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 -> Attr
RightId Term
a') }
ShAAppl "Strat" [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] -> Attr
Strat [Int]
a') }
ShAAppl "Memo" [] _ -> (ATermTable
att0, Attr
Memo)
ShAAppl "Prec" [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 -> Attr
Prec Int
a') }
ShAAppl "Gather" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Qid])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Qid]
a') ->
(ATermTable
att1, [Qid] -> Attr
Gather [Qid]
a') }
ShAAppl "Format" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Qid])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Qid]
a') ->
(ATermTable
att1, [Qid] -> Attr
Format [Qid]
a') }
ShAAppl "Ctor" [] _ -> (ATermTable
att0, Attr
Ctor)
ShAAppl "Config" [] _ -> (ATermTable
att0, Attr
Config)
ShAAppl "Object" [] _ -> (ATermTable
att0, Attr
Object)
ShAAppl "Msg" [] _ -> (ATermTable
att0, Attr
Msg)
ShAAppl "Frozen" [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] -> Attr
Frozen [Int]
a') }
ShAAppl "Poly" [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] -> Attr
Poly [Int]
a') }
ShAAppl "Special" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Hook])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Hook]
a') ->
(ATermTable
att1, [Hook] -> Attr
Special [Hook]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Attr)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Attr" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Condition where
toShATermAux :: ATermTable -> Condition -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Condition
xv = case Condition
xv of
EqCond 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 "EqCond" [Int
a', Int
b'] []) ATermTable
att2
MbCond a :: Term
a b :: Sort
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 -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sort
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 "MbCond" [Int
a', Int
b'] []) ATermTable
att2
MatchCond 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 "MatchCond" [Int
a', Int
b'] []) ATermTable
att2
RwCond 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 "RwCond" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Condition)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "EqCond" [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 -> Condition
EqCond Term
a' Term
b') }}
ShAAppl "MbCond" [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, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sort
b') ->
(ATermTable
att2, Term -> Sort -> Condition
MbCond Term
a' Sort
b') }}
ShAAppl "MatchCond" [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 -> Condition
MatchCond Term
a' Term
b') }}
ShAAppl "RwCond" [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 -> Condition
RwCond Term
a' Term
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Condition)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Condition" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Rule where
toShATermAux :: ATermTable -> Rule -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Rule
xv = case Rule
xv of
Rl a :: Term
a b :: Term
b c :: [Condition]
c d :: [StmntAttr]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Condition] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Condition]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [StmntAttr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [StmntAttr]
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 "Rl" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, Rule)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Rl" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Term
b') ->
case Int -> ATermTable -> (ATermTable, [Condition])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Condition]
c') ->
case Int -> ATermTable -> (ATermTable, [StmntAttr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [StmntAttr]
d') ->
(ATermTable
att4, Term -> Term -> [Condition] -> [StmntAttr] -> Rule
Rl Term
a' Term
b' [Condition]
c' [StmntAttr]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Rule)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Rule" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Equation where
toShATermAux :: ATermTable -> Equation -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Equation
xv = case Equation
xv of
Eq a :: Term
a b :: Term
b c :: [Condition]
c d :: [StmntAttr]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Condition] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Condition]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [StmntAttr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [StmntAttr]
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 "Eq" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, Equation)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Eq" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Term
b') ->
case Int -> ATermTable -> (ATermTable, [Condition])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Condition]
c') ->
case Int -> ATermTable -> (ATermTable, [StmntAttr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [StmntAttr]
d') ->
(ATermTable
att4, Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
a' Term
b' [Condition]
c' [StmntAttr]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Equation)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Equation" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Membership where
toShATermAux :: ATermTable -> Membership -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Membership
xv = case Membership
xv of
Mb a :: Term
a b :: Sort
b c :: [Condition]
c d :: [StmntAttr]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sort
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Condition] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Condition]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [StmntAttr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [StmntAttr]
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 "Mb" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, Membership)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Mb" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sort
b') ->
case Int -> ATermTable -> (ATermTable, [Condition])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Condition]
c') ->
case Int -> ATermTable -> (ATermTable, [StmntAttr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [StmntAttr]
d') ->
(ATermTable
att4, Term -> Sort -> [Condition] -> [StmntAttr] -> Membership
Mb Term
a' Sort
b' [Condition]
c' [StmntAttr]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Membership)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Membership" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Operator where
toShATermAux :: ATermTable -> Operator -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Operator
xv = case Operator
xv of
Op a :: OpId
a b :: [Type]
b c :: Type
c d :: [Attr]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Type] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Type]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Type
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Attr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Attr]
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 "Op" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, Operator)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Op" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, OpId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpId
a') ->
case Int -> ATermTable -> (ATermTable, [Type])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Type]
b') ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Type
c') ->
case Int -> ATermTable -> (ATermTable, [Attr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [Attr]
d') ->
(ATermTable
att4, OpId -> [Type] -> Type -> [Attr] -> Operator
Op OpId
a' [Type]
b' Type
c' [Attr]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Operator)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Operator" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.SubsortDecl where
toShATermAux :: ATermTable -> SubsortDecl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SubsortDecl
xv = case SubsortDecl
xv of
Subsort a :: Sort
a b :: Sort
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sort
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sort
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 "Subsort" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, SubsortDecl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Subsort" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sort
a') ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sort
b') ->
(ATermTable
att2, Sort -> Sort -> SubsortDecl
Subsort Sort
a' Sort
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SubsortDecl)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.SubsortDecl" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Import where
toShATermAux :: ATermTable -> Import -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Import
xv = case Import
xv of
Including a :: ModExp
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
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 "Including" [Int
a'] []) ATermTable
att1
Extending a :: ModExp
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
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 "Extending" [Int
a'] []) ATermTable
att1
Protecting a :: ModExp
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
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 "Protecting" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Import)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Including" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
(ATermTable
att1, ModExp -> Import
Including ModExp
a') }
ShAAppl "Extending" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
(ATermTable
att1, ModExp -> Import
Extending ModExp
a') }
ShAAppl "Protecting" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
(ATermTable
att1, ModExp -> Import
Protecting ModExp
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Import)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Import" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Statement where
toShATermAux :: ATermTable -> Statement -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Statement
xv = case Statement
xv of
ImportStmnt a :: Import
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Import -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Import
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 "ImportStmnt" [Int
a'] []) ATermTable
att1
SortStmnt a :: Sort
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sort
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 "SortStmnt" [Int
a'] []) ATermTable
att1
SubsortStmnt a :: SubsortDecl
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SubsortDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SubsortDecl
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 "SubsortStmnt" [Int
a'] []) ATermTable
att1
OpStmnt a :: Operator
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Operator -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Operator
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 "OpStmnt" [Int
a'] []) ATermTable
att1
EqStmnt a :: Equation
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Equation -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Equation
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 "EqStmnt" [Int
a'] []) ATermTable
att1
MbStmnt a :: Membership
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Membership -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Membership
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 "MbStmnt" [Int
a'] []) ATermTable
att1
RlStmnt a :: Rule
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Rule -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Rule
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 "RlStmnt" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Statement)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ImportStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Import)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Import
a') ->
(ATermTable
att1, Import -> Statement
ImportStmnt Import
a') }
ShAAppl "SortStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sort
a') ->
(ATermTable
att1, Sort -> Statement
SortStmnt Sort
a') }
ShAAppl "SubsortStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, SubsortDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SubsortDecl
a') ->
(ATermTable
att1, SubsortDecl -> Statement
SubsortStmnt SubsortDecl
a') }
ShAAppl "OpStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Operator)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Operator
a') ->
(ATermTable
att1, Operator -> Statement
OpStmnt Operator
a') }
ShAAppl "EqStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Equation)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Equation
a') ->
(ATermTable
att1, Equation -> Statement
EqStmnt Equation
a') }
ShAAppl "MbStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Membership)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Membership
a') ->
(ATermTable
att1, Membership -> Statement
MbStmnt Membership
a') }
ShAAppl "RlStmnt" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Rule)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Rule
a') ->
(ATermTable
att1, Rule -> Statement
RlStmnt Rule
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Statement)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Statement" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.ToPartRenaming where
toShATermAux :: ATermTable -> ToPartRenaming -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ToPartRenaming
xv = case ToPartRenaming
xv of
To a :: OpId
a b :: [Attr]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Attr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Attr]
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 "To" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, ToPartRenaming)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "To" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, OpId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpId
a') ->
case Int -> ATermTable -> (ATermTable, [Attr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Attr]
b') ->
(ATermTable
att2, OpId -> [Attr] -> ToPartRenaming
To OpId
a' [Attr]
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ToPartRenaming)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.ToPartRenaming" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Renaming where
toShATermAux :: ATermTable -> Renaming -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Renaming
xv = case Renaming
xv of
SortRenaming a :: Sort
a b :: Sort
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sort
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Sort
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 "SortRenaming" [Int
a', Int
b'] []) ATermTable
att2
LabelRenaming a :: LabelId
a b :: LabelId
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LabelId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 LabelId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> LabelId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 LabelId
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 "LabelRenaming" [Int
a', Int
b'] []) ATermTable
att2
OpRenaming1 a :: OpId
a b :: ToPartRenaming
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ToPartRenaming -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ToPartRenaming
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 "OpRenaming1" [Int
a', Int
b'] []) ATermTable
att2
OpRenaming2 a :: OpId
a b :: [Type]
b c :: Type
c d :: ToPartRenaming
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Type] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Type]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Type
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> ToPartRenaming -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 ToPartRenaming
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 "OpRenaming2" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
TermMap 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 "TermMap" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Renaming)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SortRenaming" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sort
a') ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Sort
b') ->
(ATermTable
att2, Sort -> Sort -> Renaming
SortRenaming Sort
a' Sort
b') }}
ShAAppl "LabelRenaming" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, LabelId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: LabelId
a') ->
case Int -> ATermTable -> (ATermTable, LabelId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: LabelId
b') ->
(ATermTable
att2, LabelId -> LabelId -> Renaming
LabelRenaming LabelId
a' LabelId
b') }}
ShAAppl "OpRenaming1" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, OpId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpId
a') ->
case Int -> ATermTable -> (ATermTable, ToPartRenaming)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: ToPartRenaming
b') ->
(ATermTable
att2, OpId -> ToPartRenaming -> Renaming
OpRenaming1 OpId
a' ToPartRenaming
b') }}
ShAAppl "OpRenaming2" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, OpId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpId
a') ->
case Int -> ATermTable -> (ATermTable, [Type])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Type]
b') ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Type
c') ->
case Int -> ATermTable -> (ATermTable, ToPartRenaming)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: ToPartRenaming
d') ->
(ATermTable
att4, OpId -> [Type] -> Type -> ToPartRenaming -> Renaming
OpRenaming2 OpId
a' [Type]
b' Type
c' ToPartRenaming
d') }}}}
ShAAppl "TermMap" [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 -> Renaming
TermMap Term
a' Term
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Renaming)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Renaming" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.ModExp where
toShATermAux :: ATermTable -> ModExp -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ModExp
xv = case ModExp
xv of
ModExp a :: ModId
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModId
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 "ModExp" [Int
a'] []) ATermTable
att1
SummationModExp a :: ModExp
a b :: ModExp
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ModExp
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 "SummationModExp" [Int
a', Int
b'] []) ATermTable
att2
RenamingModExp a :: ModExp
a b :: [Renaming]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Renaming] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Renaming]
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 "RenamingModExp" [Int
a', Int
b'] []) ATermTable
att2
InstantiationModExp a :: ModExp
a b :: [ViewId]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModExp
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [ViewId] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [ViewId]
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 "InstantiationModExp" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, ModExp)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ModExp" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, ModId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModId
a') ->
(ATermTable
att1, ModId -> ModExp
ModExp ModId
a') }
ShAAppl "SummationModExp" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: ModExp
b') ->
(ATermTable
att2, ModExp -> ModExp -> ModExp
SummationModExp ModExp
a' ModExp
b') }}
ShAAppl "RenamingModExp" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
case Int -> ATermTable -> (ATermTable, [Renaming])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Renaming]
b') ->
(ATermTable
att2, ModExp -> [Renaming] -> ModExp
RenamingModExp ModExp
a' [Renaming]
b') }}
ShAAppl "InstantiationModExp" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModExp
a') ->
case Int -> ATermTable -> (ATermTable, [ViewId])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [ViewId]
b') ->
(ATermTable
att2, ModExp -> [ViewId] -> ModExp
InstantiationModExp ModExp
a' [ViewId]
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ModExp)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.ModExp" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Parameter where
toShATermAux :: ATermTable -> Parameter -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Parameter
xv = case Parameter
xv of
Parameter a :: Sort
a b :: ModExp
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Sort -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Sort
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ModExp
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 "Parameter" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Parameter)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Parameter" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Sort)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Sort
a') ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: ModExp
b') ->
(ATermTable
att2, Sort -> ModExp -> Parameter
Parameter Sort
a' ModExp
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Parameter)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Parameter" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.View where
toShATermAux :: ATermTable -> View -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: View
xv = case View
xv of
View a :: ModId
a b :: ModExp
b c :: ModExp
c d :: [Renaming]
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 ModExp
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> ModExp -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 ModExp
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Renaming] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Renaming]
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 "View" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, View)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "View" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, ModId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModId
a') ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: ModExp
b') ->
case Int -> ATermTable -> (ATermTable, ModExp)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: ModExp
c') ->
case Int -> ATermTable -> (ATermTable, [Renaming])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [Renaming]
d') ->
(ATermTable
att4, ModId -> ModExp -> ModExp -> [Renaming] -> View
View ModId
a' ModExp
b' ModExp
c' [Renaming]
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, View)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.View" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Module where
toShATermAux :: ATermTable -> Module -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Module
xv = case Module
xv of
Module a :: ModId
a b :: [Parameter]
b c :: [Statement]
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ModId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ModId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Parameter] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Parameter]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Statement] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Statement]
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 "Module" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Module)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Module" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, ModId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: ModId
a') ->
case Int -> ATermTable -> (ATermTable, [Parameter])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Parameter]
b') ->
case Int -> ATermTable -> (ATermTable, [Statement])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Statement]
c') ->
(ATermTable
att3, ModId -> [Parameter] -> [Statement] -> Module
Module ModId
a' [Parameter]
b' [Statement]
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Module)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Module" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.Spec where
toShATermAux :: ATermTable -> Spec -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Spec
xv = case Spec
xv of
SpecMod 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 "SpecMod" [Int
a'] []) ATermTable
att1
SpecTh 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 "SpecTh" [Int
a'] []) ATermTable
att1
SpecView a :: View
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> View -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 View
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 "SpecView" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Spec)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SpecMod" [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 -> Spec
SpecMod Module
a') }
ShAAppl "SpecTh" [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 -> Spec
SpecTh Module
a') }
ShAAppl "SpecView" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, View)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: View
a') ->
(ATermTable
att1, View -> Spec
SpecView View
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Spec)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.Spec" ShATerm
u
instance ShATermConvertible Maude.AS_Maude.MaudeText where
toShATermAux :: ATermTable -> MaudeText -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: MaudeText
xv = case MaudeText
xv of
MaudeText 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 "MaudeText" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, MaudeText)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "MaudeText" [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 -> MaudeText
MaudeText String
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MaudeText)
forall a. String -> ShATerm -> a
fromShATermError "Maude.AS_Maude.MaudeText" ShATerm
u
instance ShATermConvertible Maude.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 :: SortMap
c d :: SortMap
d e :: SortMap
e f :: SortMap
f -> 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 -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SortMap
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 SortMap
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 SortMap
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 SortMap
f
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Morphism" [Int
a', Int
b', Int
c', Int
d', Int
e',
Int
f'] []) ATermTable
att6
fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Morphism" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
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, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: SortMap
c') ->
case Int -> ATermTable -> (ATermTable, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: SortMap
d') ->
case Int -> ATermTable -> (ATermTable, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: SortMap
e') ->
case Int -> ATermTable -> (ATermTable, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: SortMap
f') ->
(ATermTable
att6, Sign
-> Sign -> SortMap -> SortMap -> SortMap -> SortMap -> Morphism
Morphism Sign
a' Sign
b' SortMap
c' SortMap
d' SortMap
e' SortMap
f') }}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Morphism)
forall a. String -> ShATerm -> a
fromShATermError "Maude.Morphism.Morphism" ShATerm
u
deriving instance GHC.Generics.Generic Maude.Morphism.Morphism
instance Data.Aeson.ToJSON Maude.Morphism.Morphism where
instance Data.Aeson.FromJSON Maude.Morphism.Morphism where
instance ShATermConvertible Maude.Sentence.Sentence where
toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sentence
xv = case Sentence
xv of
Membership a :: Membership
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Membership -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Membership
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 "Membership" [Int
a'] []) ATermTable
att1
Equation a :: Equation
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Equation -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Equation
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 "Equation" [Int
a'] []) ATermTable
att1
Rule a :: Rule
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Rule -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Rule
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 "Rule" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Membership" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Membership)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Membership
a') ->
(ATermTable
att1, Membership -> Sentence
Membership Membership
a') }
ShAAppl "Equation" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Equation)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Equation
a') ->
(ATermTable
att1, Equation -> Sentence
Equation Equation
a') }
ShAAppl "Rule" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Rule)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Rule
a') ->
(ATermTable
att1, Rule -> Sentence
Rule Rule
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sentence)
forall a. String -> ShATerm -> a
fromShATermError "Maude.Sentence.Sentence" ShATerm
u
deriving instance GHC.Generics.Generic Maude.Sentence.Sentence
instance Data.Aeson.ToJSON Maude.Sentence.Sentence where
instance Data.Aeson.FromJSON Maude.Sentence.Sentence where
instance ShATermConvertible Maude.Sign.Sign where
toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
Sign a :: SortSet
a b :: SortSet
b c :: SubsortRel
c d :: OpMap
d e :: Sentences
e f :: SortMap
f -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SortSet -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SortSet
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SortSet -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SortSet
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SubsortRel -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SubsortRel
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> OpMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 OpMap
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Sentences -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Sentences
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 SortMap
f
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sign" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f'] []) ATermTable
att6
fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Sign" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
case Int -> ATermTable -> (ATermTable, SortSet)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SortSet
a') ->
case Int -> ATermTable -> (ATermTable, SortSet)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: SortSet
b') ->
case Int -> ATermTable -> (ATermTable, SubsortRel)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: SubsortRel
c') ->
case Int -> ATermTable -> (ATermTable, OpMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: OpMap
d') ->
case Int -> ATermTable -> (ATermTable, Sentences)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Sentences
e') ->
case Int -> ATermTable -> (ATermTable, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: SortMap
f') ->
(ATermTable
att6, SortSet
-> SortSet -> SubsortRel -> OpMap -> Sentences -> SortMap -> Sign
Sign SortSet
a' SortSet
b' SubsortRel
c' OpMap
d' Sentences
e' SortMap
f') }}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "Maude.Sign.Sign" ShATerm
u
deriving instance GHC.Generics.Generic Maude.Sign.Sign
instance Data.Aeson.ToJSON Maude.Sign.Sign where
instance Data.Aeson.FromJSON Maude.Sign.Sign where
instance ShATermConvertible Maude.Symbol.Symbol where
toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symbol
xv = case Symbol
xv of
Sort a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "Sort" [Int
a'] []) ATermTable
att1
Kind a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "Kind" [Int
a'] []) ATermTable
att1
Labl a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "Labl" [Int
a'] []) ATermTable
att1
Operator a :: Qid
a b :: [Symbol]
b c :: Symbol
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Symbol] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Symbol]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Symbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Symbol
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 "Operator" [Int
a', Int
b', Int
c'] []) ATermTable
att3
OpWildcard a :: Qid
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Qid -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Qid
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 "OpWildcard" [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 "Sort" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Symbol
Sort Qid
a') }
ShAAppl "Kind" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Symbol
Kind Qid
a') }
ShAAppl "Labl" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Symbol
Labl Qid
a') }
ShAAppl "Operator" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
case Int -> ATermTable -> (ATermTable, [Symbol])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Symbol]
b') ->
case Int -> ATermTable -> (ATermTable, Symbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Symbol
c') ->
(ATermTable
att3, Qid -> [Symbol] -> Symbol -> Symbol
Operator Qid
a' [Symbol]
b' Symbol
c') }}}
ShAAppl "OpWildcard" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Qid)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Qid
a') ->
(ATermTable
att1, Qid -> Symbol
OpWildcard Qid
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symbol)
forall a. String -> ShATerm -> a
fromShATermError "Maude.Symbol.Symbol" ShATerm
u
instance ShATermConvertible Maude.Symbol.SymbolKind where
toShATermAux :: ATermTable -> SymbolKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbolKind
xv = case SymbolKind
xv of
SortK -> (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 "SortK" [] []) ATermTable
att0
KindK -> (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 "KindK" [] []) ATermTable
att0
LablK -> (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 "LablK" [] []) ATermTable
att0
OpK -> (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 "OpK" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbolKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SortK" [] _ -> (ATermTable
att0, SymbolKind
SortK)
ShAAppl "KindK" [] _ -> (ATermTable
att0, SymbolKind
KindK)
ShAAppl "LablK" [] _ -> (ATermTable
att0, SymbolKind
LablK)
ShAAppl "OpK" [] _ -> (ATermTable
att0, SymbolKind
OpK)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbolKind)
forall a. String -> ShATerm -> a
fromShATermError "Maude.Symbol.SymbolKind" ShATerm
u
deriving instance GHC.Generics.Generic Maude.Symbol.Symbol
instance Data.Aeson.ToJSON Maude.Symbol.Symbol where
instance Data.Aeson.FromJSON Maude.Symbol.Symbol where
deriving instance GHC.Generics.Generic Maude.Symbol.SymbolKind
instance Data.Aeson.ToJSON Maude.Symbol.SymbolKind where
instance Data.Aeson.FromJSON Maude.Symbol.SymbolKind where