{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module HasCASL.ATC_HasCASL () where
import ATC.GlobalAnnotations
import ATerm.Lib
import Common.AS_Annotation
import Common.AS_Annotation (Named)
import Common.Doc
import Common.DocUtils
import Common.GlobalAnnotations
import Common.Id
import Common.Json.Instances
import Common.Keywords
import Common.Prec
import Common.Result
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import Data.List (partition)
import Data.Maybe
import Data.Ord
import GHC.Generics(Generic)
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.FoldTerm
import HasCASL.FoldType
import HasCASL.Le
import HasCASL.Le as Le
import HasCASL.Sublogic
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.State as State
import qualified Data.Map as Map
import qualified Data.Set as Set
deriving instance GHC.Generics.Generic Common.Prec.PrecMap
instance Data.Aeson.ToJSON Common.Prec.PrecMap where
instance Data.Aeson.FromJSON Common.Prec.PrecMap where
instance ShATermConvertible Common.Prec.PrecMap where
toShATermAux :: ATermTable -> PrecMap -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PrecMap
xv = case PrecMap
xv of
PrecMap a :: Map Id Int
a b :: Int
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Map Id Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Map Id Int
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Int
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "PrecMap" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, PrecMap)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "PrecMap" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Map Id Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Map Id Int
a') ->
case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Int
b') ->
(ATermTable
att2, Map Id Int -> Int -> PrecMap
PrecMap Map Id Int
a' Int
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PrecMap)
forall a. String -> ShATerm -> a
fromShATermError "Common.Prec.PrecMap" ShATerm
u
deriving instance GHC.Generics.Generic HasCASL.As.SymbOrMap
instance Data.Aeson.ToJSON HasCASL.As.SymbOrMap where
instance Data.Aeson.FromJSON HasCASL.As.SymbOrMap where
deriving instance GHC.Generics.Generic HasCASL.As.SymbType
instance Data.Aeson.ToJSON HasCASL.As.SymbType where
instance Data.Aeson.FromJSON HasCASL.As.SymbType where
deriving instance GHC.Generics.Generic HasCASL.As.Symb
instance Data.Aeson.ToJSON HasCASL.As.Symb where
instance Data.Aeson.FromJSON HasCASL.As.Symb where
deriving instance GHC.Generics.Generic HasCASL.As.SymbKind
instance Data.Aeson.ToJSON HasCASL.As.SymbKind where
instance Data.Aeson.FromJSON HasCASL.As.SymbKind where
deriving instance GHC.Generics.Generic HasCASL.As.SymbMapItems
instance Data.Aeson.ToJSON HasCASL.As.SymbMapItems where
instance Data.Aeson.FromJSON HasCASL.As.SymbMapItems where
deriving instance GHC.Generics.Generic HasCASL.As.SymbItems
instance Data.Aeson.ToJSON HasCASL.As.SymbItems where
instance Data.Aeson.FromJSON HasCASL.As.SymbItems where
deriving instance GHC.Generics.Generic HasCASL.As.GenVarDecl
instance Data.Aeson.ToJSON HasCASL.As.GenVarDecl where
instance Data.Aeson.FromJSON HasCASL.As.GenVarDecl where
deriving instance GHC.Generics.Generic HasCASL.As.TypeArg
instance Data.Aeson.ToJSON HasCASL.As.TypeArg where
instance Data.Aeson.FromJSON HasCASL.As.TypeArg where
deriving instance GHC.Generics.Generic HasCASL.As.VarKind
instance Data.Aeson.ToJSON HasCASL.As.VarKind where
instance Data.Aeson.FromJSON HasCASL.As.VarKind where
deriving instance GHC.Generics.Generic HasCASL.As.VarDecl
instance Data.Aeson.ToJSON HasCASL.As.VarDecl where
instance Data.Aeson.FromJSON HasCASL.As.VarDecl where
deriving instance GHC.Generics.Generic HasCASL.As.SeparatorKind
instance Data.Aeson.ToJSON HasCASL.As.SeparatorKind where
instance Data.Aeson.FromJSON HasCASL.As.SeparatorKind where
deriving instance GHC.Generics.Generic HasCASL.As.PolyId
instance Data.Aeson.ToJSON HasCASL.As.PolyId where
instance Data.Aeson.FromJSON HasCASL.As.PolyId where
deriving instance GHC.Generics.Generic HasCASL.As.ProgEq
instance Data.Aeson.ToJSON HasCASL.As.ProgEq where
instance Data.Aeson.FromJSON HasCASL.As.ProgEq where
deriving instance GHC.Generics.Generic HasCASL.As.Term
instance Data.Aeson.ToJSON HasCASL.As.Term where
instance Data.Aeson.FromJSON HasCASL.As.Term where
deriving instance GHC.Generics.Generic HasCASL.As.InstKind
instance Data.Aeson.ToJSON HasCASL.As.InstKind where
instance Data.Aeson.FromJSON HasCASL.As.InstKind where
deriving instance GHC.Generics.Generic HasCASL.As.BracketKind
instance Data.Aeson.ToJSON HasCASL.As.BracketKind where
instance Data.Aeson.FromJSON HasCASL.As.BracketKind where
deriving instance GHC.Generics.Generic HasCASL.As.LetBrand
instance Data.Aeson.ToJSON HasCASL.As.LetBrand where
instance Data.Aeson.FromJSON HasCASL.As.LetBrand where
deriving instance GHC.Generics.Generic HasCASL.As.TypeQual
instance Data.Aeson.ToJSON HasCASL.As.TypeQual where
instance Data.Aeson.FromJSON HasCASL.As.TypeQual where
deriving instance GHC.Generics.Generic HasCASL.As.Quantifier
instance Data.Aeson.ToJSON HasCASL.As.Quantifier where
instance Data.Aeson.FromJSON HasCASL.As.Quantifier where
deriving instance GHC.Generics.Generic HasCASL.As.Component
instance Data.Aeson.ToJSON HasCASL.As.Component where
instance Data.Aeson.FromJSON HasCASL.As.Component where
deriving instance GHC.Generics.Generic HasCASL.As.Alternative
instance Data.Aeson.ToJSON HasCASL.As.Alternative where
instance Data.Aeson.FromJSON HasCASL.As.Alternative where
deriving instance GHC.Generics.Generic HasCASL.As.DatatypeDecl
instance Data.Aeson.ToJSON HasCASL.As.DatatypeDecl where
instance Data.Aeson.FromJSON HasCASL.As.DatatypeDecl where
deriving instance GHC.Generics.Generic HasCASL.As.OpAttr
instance Data.Aeson.ToJSON HasCASL.As.OpAttr where
instance Data.Aeson.FromJSON HasCASL.As.OpAttr where
deriving instance GHC.Generics.Generic HasCASL.As.BinOpAttr
instance Data.Aeson.ToJSON HasCASL.As.BinOpAttr where
instance Data.Aeson.FromJSON HasCASL.As.BinOpAttr where
deriving instance GHC.Generics.Generic HasCASL.As.OpItem
instance Data.Aeson.ToJSON HasCASL.As.OpItem where
instance Data.Aeson.FromJSON HasCASL.As.OpItem where
deriving instance GHC.Generics.Generic HasCASL.As.Partiality
instance Data.Aeson.ToJSON HasCASL.As.Partiality where
instance Data.Aeson.FromJSON HasCASL.As.Partiality where
deriving instance GHC.Generics.Generic HasCASL.As.TypeScheme
instance Data.Aeson.ToJSON HasCASL.As.TypeScheme where
instance Data.Aeson.FromJSON HasCASL.As.TypeScheme where
deriving instance GHC.Generics.Generic HasCASL.As.Type
instance Data.Aeson.ToJSON HasCASL.As.Type where
instance Data.Aeson.FromJSON HasCASL.As.Type where
deriving instance GHC.Generics.Generic HasCASL.As.TypePattern
instance Data.Aeson.ToJSON HasCASL.As.TypePattern where
instance Data.Aeson.FromJSON HasCASL.As.TypePattern where
deriving instance GHC.Generics.Generic HasCASL.As.Vars
instance Data.Aeson.ToJSON HasCASL.As.Vars where
instance Data.Aeson.FromJSON HasCASL.As.Vars where
deriving instance GHC.Generics.Generic HasCASL.As.TypeItem
instance Data.Aeson.ToJSON HasCASL.As.TypeItem where
instance Data.Aeson.FromJSON HasCASL.As.TypeItem where
deriving instance GHC.Generics.Generic (HasCASL.As.AnyKind a)
instance Data.Aeson.ToJSON a => Data.Aeson.ToJSON (HasCASL.As.AnyKind a) where
instance Data.Aeson.FromJSON a => Data.Aeson.FromJSON (HasCASL.As.AnyKind a) where
deriving instance GHC.Generics.Generic HasCASL.As.Variance
instance Data.Aeson.ToJSON HasCASL.As.Variance where
instance Data.Aeson.FromJSON HasCASL.As.Variance where
deriving instance GHC.Generics.Generic HasCASL.As.ClassDecl
instance Data.Aeson.ToJSON HasCASL.As.ClassDecl where
instance Data.Aeson.FromJSON HasCASL.As.ClassDecl where
deriving instance GHC.Generics.Generic HasCASL.As.ClassItem
instance Data.Aeson.ToJSON HasCASL.As.ClassItem where
instance Data.Aeson.FromJSON HasCASL.As.ClassItem where
deriving instance GHC.Generics.Generic HasCASL.As.Instance
instance Data.Aeson.ToJSON HasCASL.As.Instance where
instance Data.Aeson.FromJSON HasCASL.As.Instance where
deriving instance GHC.Generics.Generic HasCASL.As.OpBrand
instance Data.Aeson.ToJSON HasCASL.As.OpBrand where
instance Data.Aeson.FromJSON HasCASL.As.OpBrand where
deriving instance GHC.Generics.Generic HasCASL.As.SigItems
instance Data.Aeson.ToJSON HasCASL.As.SigItems where
instance Data.Aeson.FromJSON HasCASL.As.SigItems where
deriving instance GHC.Generics.Generic HasCASL.As.BasicItem
instance Data.Aeson.ToJSON HasCASL.As.BasicItem where
instance Data.Aeson.FromJSON HasCASL.As.BasicItem where
deriving instance GHC.Generics.Generic HasCASL.As.BasicSpec
instance Data.Aeson.ToJSON HasCASL.As.BasicSpec where
instance Data.Aeson.FromJSON HasCASL.As.BasicSpec where
instance ShATermConvertible HasCASL.As.SymbOrMap where
toShATermAux :: ATermTable -> SymbOrMap -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbOrMap
xv = case SymbOrMap
xv of
SymbOrMap a :: Symb
a b :: Maybe Symb
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Symb -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Symb
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe Symb -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe Symb
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SymbOrMap" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbOrMap)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SymbOrMap" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Symb)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Symb
a') ->
case Int -> ATermTable -> (ATermTable, Maybe Symb)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Maybe Symb
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Symb -> Maybe Symb -> Range -> SymbOrMap
SymbOrMap Symb
a' Maybe Symb
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbOrMap)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SymbOrMap" ShATerm
u
instance ShATermConvertible HasCASL.As.SymbType where
toShATermAux :: ATermTable -> SymbType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbType
xv = case SymbType
xv of
SymbType a :: TypeScheme
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypeScheme -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypeScheme
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 "SymbType" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SymbType" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TypeScheme)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypeScheme
a') ->
(ATermTable
att1, TypeScheme -> SymbType
SymbType TypeScheme
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbType)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SymbType" ShATerm
u
instance ShATermConvertible HasCASL.As.Symb where
toShATermAux :: ATermTable -> Symb -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Symb
xv = case Symb
xv of
Symb a :: Id
a b :: Maybe SymbType
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe SymbType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe SymbType
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Symb" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, Symb)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Symb" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, Maybe SymbType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Maybe SymbType
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Id -> Maybe SymbType -> Range -> Symb
Symb Id
a' Maybe SymbType
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Symb)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Symb" ShATerm
u
instance ShATermConvertible HasCASL.As.SymbKind where
toShATermAux :: ATermTable -> SymbKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbKind
xv = case SymbKind
xv of
Implicit -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Implicit" [] []) ATermTable
att0
SyKtype -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKtype" [] []) ATermTable
att0
SyKsort -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKsort" [] []) ATermTable
att0
SyKfun -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKfun" [] []) ATermTable
att0
SyKop -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKop" [] []) ATermTable
att0
SyKpred -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKpred" [] []) ATermTable
att0
SyKclass -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SyKclass" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Implicit" [] _ -> (ATermTable
att0, SymbKind
Implicit)
ShAAppl "SyKtype" [] _ -> (ATermTable
att0, SymbKind
SyKtype)
ShAAppl "SyKsort" [] _ -> (ATermTable
att0, SymbKind
SyKsort)
ShAAppl "SyKfun" [] _ -> (ATermTable
att0, SymbKind
SyKfun)
ShAAppl "SyKop" [] _ -> (ATermTable
att0, SymbKind
SyKop)
ShAAppl "SyKpred" [] _ -> (ATermTable
att0, SymbKind
SyKpred)
ShAAppl "SyKclass" [] _ -> (ATermTable
att0, SymbKind
SyKclass)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbKind)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SymbKind" ShATerm
u
instance ShATermConvertible HasCASL.As.SymbMapItems where
toShATermAux :: ATermTable -> SymbMapItems -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbMapItems
xv = case SymbMapItems
xv of
SymbMapItems a :: SymbKind
a b :: [SymbOrMap]
b c :: [Annotation]
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SymbKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SymbKind
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SymbOrMap] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SymbOrMap]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Annotation] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Annotation]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SymbMapItems" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbMapItems)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SymbMapItems" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, SymbKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SymbKind
a') ->
case Int -> ATermTable -> (ATermTable, [SymbOrMap])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [SymbOrMap]
b') ->
case Int -> ATermTable -> (ATermTable, [Annotation])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Annotation]
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, SymbKind -> [SymbOrMap] -> [Annotation] -> Range -> SymbMapItems
SymbMapItems SymbKind
a' [SymbOrMap]
b' [Annotation]
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbMapItems)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SymbMapItems" ShATerm
u
instance ShATermConvertible HasCASL.As.SymbItems where
toShATermAux :: ATermTable -> SymbItems -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SymbItems
xv = case SymbItems
xv of
SymbItems a :: SymbKind
a b :: [Symb]
b c :: [Annotation]
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SymbKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SymbKind
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Symb] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Symb]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Annotation] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Annotation]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SymbItems" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbItems)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "SymbItems" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, SymbKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: SymbKind
a') ->
case Int -> ATermTable -> (ATermTable, [Symb])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [Symb]
b') ->
case Int -> ATermTable -> (ATermTable, [Annotation])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Annotation]
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, SymbKind -> [Symb] -> [Annotation] -> Range -> SymbItems
SymbItems SymbKind
a' [Symb]
b' [Annotation]
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SymbItems)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SymbItems" ShATerm
u
instance ShATermConvertible HasCASL.As.GenVarDecl where
toShATermAux :: ATermTable -> GenVarDecl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: GenVarDecl
xv = case GenVarDecl
xv of
GenVarDecl a :: VarDecl
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VarDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VarDecl
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 "GenVarDecl" [Int
a'] []) ATermTable
att1
GenTypeVarDecl a :: TypeArg
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypeArg -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypeArg
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 "GenTypeVarDecl" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, GenVarDecl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "GenVarDecl" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, VarDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: VarDecl
a') ->
(ATermTable
att1, VarDecl -> GenVarDecl
GenVarDecl VarDecl
a') }
ShAAppl "GenTypeVarDecl" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TypeArg)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypeArg
a') ->
(ATermTable
att1, TypeArg -> GenVarDecl
GenTypeVarDecl TypeArg
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GenVarDecl)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.GenVarDecl" ShATerm
u
instance ShATermConvertible HasCASL.As.TypeArg where
toShATermAux :: ATermTable -> TypeArg -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypeArg
xv = case TypeArg
xv of
TypeArg a :: Id
a b :: Variance
b c :: VarKind
c d :: RawKind
d e :: Int
e f :: SeparatorKind
f g :: Range
g -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Variance -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Variance
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> VarKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 VarKind
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> RawKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 RawKind
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Int
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> SeparatorKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 SeparatorKind
f
(att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Range
g
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypeArg" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
Int
g'] []) ATermTable
att7
fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeArg)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TypeArg" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, Variance)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Variance
b') ->
case Int -> ATermTable -> (ATermTable, VarKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: VarKind
c') ->
case Int -> ATermTable -> (ATermTable, RawKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: RawKind
d') ->
case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Int
e') ->
case Int -> ATermTable -> (ATermTable, SeparatorKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: SeparatorKind
f') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
{ (att7 :: ATermTable
att7, g' :: Range
g') ->
(ATermTable
att7, Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
a' Variance
b' VarKind
c' RawKind
d' Int
e' SeparatorKind
f' Range
g') }}}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypeArg)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.TypeArg" ShATerm
u
instance ShATermConvertible HasCASL.As.VarKind where
toShATermAux :: ATermTable -> VarKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: VarKind
xv = case VarKind
xv of
VarKind 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 "VarKind" [Int
a'] []) ATermTable
att1
Downset a :: Type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Type
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 "Downset" [Int
a'] []) ATermTable
att1
MissingKind -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "MissingKind" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, VarKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "VarKind" [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 -> VarKind
VarKind Kind
a') }
ShAAppl "Downset" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Type
a') ->
(ATermTable
att1, Type -> VarKind
Downset Type
a') }
ShAAppl "MissingKind" [] _ -> (ATermTable
att0, VarKind
MissingKind)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, VarKind)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.VarKind" ShATerm
u
instance ShATermConvertible HasCASL.As.VarDecl where
toShATermAux :: ATermTable -> VarDecl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: VarDecl
xv = case VarDecl
xv of
VarDecl a :: Id
a b :: Type
b c :: SeparatorKind
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(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 -> SeparatorKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SeparatorKind
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "VarDecl" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, VarDecl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "VarDecl" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
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, SeparatorKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: SeparatorKind
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
a' Type
b' SeparatorKind
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, VarDecl)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.VarDecl" ShATerm
u
instance ShATermConvertible HasCASL.As.SeparatorKind where
toShATermAux :: ATermTable -> SeparatorKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SeparatorKind
xv = case SeparatorKind
xv of
Comma -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Comma" [] []) ATermTable
att0
Other -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Other" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, SeparatorKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Comma" [] _ -> (ATermTable
att0, SeparatorKind
Comma)
ShAAppl "Other" [] _ -> (ATermTable
att0, SeparatorKind
Other)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SeparatorKind)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.SeparatorKind" ShATerm
u
instance ShATermConvertible HasCASL.As.PolyId where
toShATermAux :: ATermTable -> PolyId -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: PolyId
xv = case PolyId
xv of
PolyId a :: Id
a b :: [TypeArg]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [TypeArg] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TypeArg]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "PolyId" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, PolyId)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "PolyId" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, [TypeArg])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [TypeArg]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Id -> [TypeArg] -> Range -> PolyId
PolyId Id
a' [TypeArg]
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, PolyId)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.PolyId" ShATerm
u
instance ShATermConvertible HasCASL.As.ProgEq where
toShATermAux :: ATermTable -> ProgEq -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ProgEq
xv = case ProgEq
xv of
ProgEq a :: Term
a b :: Term
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ProgEq" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, ProgEq)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ProgEq" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Term
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Term -> Term -> Range -> ProgEq
ProgEq Term
a' Term
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ProgEq)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.ProgEq" ShATerm
u
instance ShATermConvertible HasCASL.As.Term where
toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Term
xv = case Term
xv of
QualVar a :: VarDecl
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VarDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VarDecl
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 "QualVar" [Int
a'] []) ATermTable
att1
QualOp a :: OpBrand
a b :: PolyId
b c :: TypeScheme
c d :: [Type]
d e :: InstKind
e f :: Range
f -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> OpBrand -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 OpBrand
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> PolyId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 PolyId
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TypeScheme -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TypeScheme
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Type] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Type]
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> InstKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 InstKind
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 Range
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 "QualOp" [Int
a', Int
b', Int
c', Int
d', Int
e',
Int
f'] []) ATermTable
att6
ApplTerm a :: Term
a b :: Term
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Term
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ApplTerm" [Int
a', Int
b', Int
c'] []) ATermTable
att3
TupleTerm a :: [Term]
a b :: Range
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TupleTerm" [Int
a', Int
b'] []) ATermTable
att2
TypedTerm a :: Term
a b :: TypeQual
b c :: Type
c d :: Range
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 -> TypeQual -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TypeQual
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypedTerm" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
AsPattern a :: VarDecl
a b :: Term
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> VarDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 VarDecl
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AsPattern" [Int
a', Int
b', Int
c'] []) ATermTable
att3
QuantifiedTerm a :: Quantifier
a b :: [GenVarDecl]
b c :: Term
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Quantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Quantifier
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [GenVarDecl] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [GenVarDecl]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Term
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "QuantifiedTerm" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
LambdaTerm a :: [Term]
a b :: Partiality
b c :: Term
c d :: Range
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 -> Partiality -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Partiality
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Term
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "LambdaTerm" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
CaseTerm a :: Term
a b :: [ProgEq]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [ProgEq] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [ProgEq]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CaseTerm" [Int
a', Int
b', Int
c'] []) ATermTable
att3
LetTerm a :: LetBrand
a b :: [ProgEq]
b c :: Term
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LetBrand -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 LetBrand
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [ProgEq] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [ProgEq]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Term
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "LetTerm" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
ResolvedMixTerm a :: Id
a b :: [Type]
b c :: [Term]
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(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 -> [Term] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Term]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ResolvedMixTerm" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
TermToken a :: Token
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "TermToken" [Int
a'] []) ATermTable
att1
MixTypeTerm a :: TypeQual
a b :: Type
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypeQual -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypeQual
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "MixTypeTerm" [Int
a', Int
b', Int
c'] []) ATermTable
att3
MixfixTerm 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 "MixfixTerm" [Int
a'] []) ATermTable
att1
BracketTerm a :: BracketKind
a b :: [Term]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BracketKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 BracketKind
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BracketTerm" [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 "QualVar" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, VarDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: VarDecl
a') ->
(ATermTable
att1, VarDecl -> Term
QualVar VarDecl
a') }
ShAAppl "QualOp" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
case Int -> ATermTable -> (ATermTable, OpBrand)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: OpBrand
a') ->
case Int -> ATermTable -> (ATermTable, PolyId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: PolyId
b') ->
case Int -> ATermTable -> (ATermTable, TypeScheme)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TypeScheme
c') ->
case Int -> ATermTable -> (ATermTable, [Type])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [Type]
d') ->
case Int -> ATermTable -> (ATermTable, InstKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: InstKind
e') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: Range
f') ->
(ATermTable
att6, OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
a' PolyId
b' TypeScheme
c' [Type]
d' InstKind
e' Range
f') }}}}}}
ShAAppl "ApplTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Term
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Term -> Term -> Range -> Term
ApplTerm Term
a' Term
b' Range
c') }}}
ShAAppl "TupleTerm" [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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [Term] -> Range -> Term
TupleTerm [Term]
a' Range
b') }}
ShAAppl "TypedTerm" [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, TypeQual)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: TypeQual
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
a' TypeQual
b' Type
c' Range
d') }}}}
ShAAppl "AsPattern" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, VarDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: VarDecl
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, VarDecl -> Term -> Range -> Term
AsPattern VarDecl
a' Term
b' Range
c') }}}
ShAAppl "QuantifiedTerm" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Quantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Quantifier
a') ->
case Int -> ATermTable -> (ATermTable, [GenVarDecl])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [GenVarDecl]
b') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Term
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
a' [GenVarDecl]
b' Term
c' Range
d') }}}}
ShAAppl "LambdaTerm" [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, Partiality)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Partiality
b') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Term
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term]
a' Partiality
b' Term
c' Range
d') }}}}
ShAAppl "CaseTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Term
a') ->
case Int -> ATermTable -> (ATermTable, [ProgEq])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [ProgEq]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Term -> [ProgEq] -> Range -> Term
CaseTerm Term
a' [ProgEq]
b' Range
c') }}}
ShAAppl "LetTerm" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, LetBrand)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: LetBrand
a') ->
case Int -> ATermTable -> (ATermTable, [ProgEq])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [ProgEq]
b') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Term
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
a' [ProgEq]
b' Term
c' Range
d') }}}}
ShAAppl "ResolvedMixTerm" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
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, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Term]
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
a' [Type]
b' [Term]
c' Range
d') }}}}
ShAAppl "TermToken" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Token
a') ->
(ATermTable
att1, Token -> Term
TermToken Token
a') }
ShAAppl "MixTypeTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, TypeQual)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypeQual
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
a' Type
b' Range
c') }}}
ShAAppl "MixfixTerm" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Term])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Term]
a') ->
(ATermTable
att1, [Term] -> Term
MixfixTerm [Term]
a') }
ShAAppl "BracketTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, BracketKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: BracketKind
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
a' [Term]
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Term)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Term" ShATerm
u
instance ShATermConvertible HasCASL.As.InstKind where
toShATermAux :: ATermTable -> InstKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: InstKind
xv = case InstKind
xv of
UserGiven -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "UserGiven" [] []) ATermTable
att0
Infer -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Infer" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, InstKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "UserGiven" [] _ -> (ATermTable
att0, InstKind
UserGiven)
ShAAppl "Infer" [] _ -> (ATermTable
att0, InstKind
Infer)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, InstKind)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.InstKind" ShATerm
u
instance ShATermConvertible HasCASL.As.BracketKind where
toShATermAux :: ATermTable -> BracketKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BracketKind
xv = case BracketKind
xv of
Parens -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Parens" [] []) ATermTable
att0
Squares -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Squares" [] []) ATermTable
att0
Braces -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Braces" [] []) ATermTable
att0
NoBrackets -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "NoBrackets" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, BracketKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Parens" [] _ -> (ATermTable
att0, BracketKind
Parens)
ShAAppl "Squares" [] _ -> (ATermTable
att0, BracketKind
Squares)
ShAAppl "Braces" [] _ -> (ATermTable
att0, BracketKind
Braces)
ShAAppl "NoBrackets" [] _ -> (ATermTable
att0, BracketKind
NoBrackets)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BracketKind)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.BracketKind" ShATerm
u
instance ShATermConvertible HasCASL.As.LetBrand where
toShATermAux :: ATermTable -> LetBrand -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: LetBrand
xv = case LetBrand
xv of
Let -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Let" [] []) ATermTable
att0
Where -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Where" [] []) ATermTable
att0
Program -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Program" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, LetBrand)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Let" [] _ -> (ATermTable
att0, LetBrand
Let)
ShAAppl "Where" [] _ -> (ATermTable
att0, LetBrand
Where)
ShAAppl "Program" [] _ -> (ATermTable
att0, LetBrand
Program)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, LetBrand)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.LetBrand" ShATerm
u
instance ShATermConvertible HasCASL.As.TypeQual where
toShATermAux :: ATermTable -> TypeQual -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypeQual
xv = case TypeQual
xv of
OfType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "OfType" [] []) ATermTable
att0
AsType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AsType" [] []) ATermTable
att0
InType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "InType" [] []) ATermTable
att0
Inferred -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Inferred" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeQual)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "OfType" [] _ -> (ATermTable
att0, TypeQual
OfType)
ShAAppl "AsType" [] _ -> (ATermTable
att0, TypeQual
AsType)
ShAAppl "InType" [] _ -> (ATermTable
att0, TypeQual
InType)
ShAAppl "Inferred" [] _ -> (ATermTable
att0, TypeQual
Inferred)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypeQual)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.TypeQual" ShATerm
u
instance ShATermConvertible HasCASL.As.Quantifier where
toShATermAux :: ATermTable -> Quantifier -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Quantifier
xv = case Quantifier
xv of
Universal -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Universal" [] []) ATermTable
att0
Existential -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Existential" [] []) ATermTable
att0
Unique -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Unique" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, Quantifier)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Universal" [] _ -> (ATermTable
att0, Quantifier
Universal)
ShAAppl "Existential" [] _ -> (ATermTable
att0, Quantifier
Existential)
ShAAppl "Unique" [] _ -> (ATermTable
att0, Quantifier
Unique)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Quantifier)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Quantifier" ShATerm
u
instance ShATermConvertible HasCASL.As.Component where
toShATermAux :: ATermTable -> Component -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Component
xv = case Component
xv of
Selector a :: Id
a b :: Partiality
b c :: Type
c d :: SeparatorKind
d e :: Range
e -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Partiality -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Partiality
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 -> SeparatorKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 SeparatorKind
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Range
e
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Selector" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
NoSelector a :: Type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Type
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 "NoSelector" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Component)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Selector" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, Partiality)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Partiality
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, SeparatorKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: SeparatorKind
d') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Range
e') ->
(ATermTable
att5, Id -> Partiality -> Type -> SeparatorKind -> Range -> Component
Selector Id
a' Partiality
b' Type
c' SeparatorKind
d' Range
e') }}}}}
ShAAppl "NoSelector" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Type
a') ->
(ATermTable
att1, Type -> Component
NoSelector Type
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Component)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Component" ShATerm
u
instance ShATermConvertible HasCASL.As.Alternative where
toShATermAux :: ATermTable -> Alternative -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Alternative
xv = case Alternative
xv of
Constructor a :: Id
a b :: [[Component]]
b c :: Partiality
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [[Component]] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [[Component]]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Partiality -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Partiality
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Constructor" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
Subtype a :: [Type]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Type] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Type]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Subtype" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Alternative)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Constructor" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, [[Component]])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [[Component]]
b') ->
case Int -> ATermTable -> (ATermTable, Partiality)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Partiality
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Id -> [[Component]] -> Partiality -> Range -> Alternative
Constructor Id
a' [[Component]]
b' Partiality
c' Range
d') }}}}
ShAAppl "Subtype" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [Type])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Type]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [Type] -> Range -> Alternative
Subtype [Type]
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Alternative)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Alternative" ShATerm
u
instance ShATermConvertible HasCASL.As.DatatypeDecl where
toShATermAux :: ATermTable -> DatatypeDecl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DatatypeDecl
xv = case DatatypeDecl
xv of
DatatypeDecl a :: TypePattern
a b :: Kind
b c :: [Annoted Alternative]
c d :: [Id]
d e :: Range
e -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypePattern -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypePattern
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Kind
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [Annoted Alternative] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [Annoted Alternative]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [Id] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [Id]
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Range
e
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DatatypeDecl" [Int
a', Int
b', Int
c', Int
d',
Int
e'] []) ATermTable
att5
fromShATermAux :: Int -> ATermTable -> (ATermTable, DatatypeDecl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "DatatypeDecl" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
case Int -> ATermTable -> (ATermTable, TypePattern)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypePattern
a') ->
case Int -> ATermTable -> (ATermTable, Kind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Kind
b') ->
case Int -> ATermTable -> (ATermTable, [Annoted Alternative])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [Annoted Alternative]
c') ->
case Int -> ATermTable -> (ATermTable, [Id])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [Id]
d') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Range
e') ->
(ATermTable
att5, TypePattern
-> Kind -> [Annoted Alternative] -> [Id] -> Range -> DatatypeDecl
DatatypeDecl TypePattern
a' Kind
b' [Annoted Alternative]
c' [Id]
d' Range
e') }}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DatatypeDecl)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.DatatypeDecl" ShATerm
u
instance ShATermConvertible HasCASL.As.OpAttr where
toShATermAux :: ATermTable -> OpAttr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OpAttr
xv = case OpAttr
xv of
BinOpAttr a :: BinOpAttr
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BinOpAttr -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 BinOpAttr
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BinOpAttr" [Int
a', Int
b'] []) ATermTable
att2
UnitOpAttr a :: Term
a b :: Range
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "UnitOpAttr" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, OpAttr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "BinOpAttr" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, BinOpAttr)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: BinOpAttr
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, BinOpAttr -> Range -> OpAttr
BinOpAttr BinOpAttr
a' Range
b') }}
ShAAppl "UnitOpAttr" [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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, Term -> Range -> OpAttr
UnitOpAttr Term
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OpAttr)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.OpAttr" ShATerm
u
instance ShATermConvertible HasCASL.As.BinOpAttr where
toShATermAux :: ATermTable -> BinOpAttr -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BinOpAttr
xv = case BinOpAttr
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
fromShATermAux :: Int -> ATermTable -> (ATermTable, BinOpAttr)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Assoc" [] _ -> (ATermTable
att0, BinOpAttr
Assoc)
ShAAppl "Comm" [] _ -> (ATermTable
att0, BinOpAttr
Comm)
ShAAppl "Idem" [] _ -> (ATermTable
att0, BinOpAttr
Idem)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BinOpAttr)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.BinOpAttr" ShATerm
u
instance ShATermConvertible HasCASL.As.OpItem where
toShATermAux :: ATermTable -> OpItem -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: OpItem
xv = case OpItem
xv of
OpDecl a :: [PolyId]
a b :: TypeScheme
b c :: [OpAttr]
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [PolyId] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [PolyId]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TypeScheme -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TypeScheme
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [OpAttr] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [OpAttr]
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "OpDecl" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
OpDefn a :: PolyId
a b :: [[VarDecl]]
b c :: TypeScheme
c d :: Term
d e :: Range
e -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PolyId -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PolyId
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [[VarDecl]] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [[VarDecl]]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TypeScheme -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TypeScheme
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Term
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Range
e
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "OpDefn" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
fromShATermAux :: Int -> ATermTable -> (ATermTable, OpItem)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "OpDecl" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, [PolyId])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [PolyId]
a') ->
case Int -> ATermTable -> (ATermTable, TypeScheme)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: TypeScheme
b') ->
case Int -> ATermTable -> (ATermTable, [OpAttr])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: [OpAttr]
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, [PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId]
a' TypeScheme
b' [OpAttr]
c' Range
d') }}}}
ShAAppl "OpDefn" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
case Int -> ATermTable -> (ATermTable, PolyId)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: PolyId
a') ->
case Int -> ATermTable -> (ATermTable, [[VarDecl]])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [[VarDecl]]
b') ->
case Int -> ATermTable -> (ATermTable, TypeScheme)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TypeScheme
c') ->
case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Term
d') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Range
e') ->
(ATermTable
att5, PolyId -> [[VarDecl]] -> TypeScheme -> Term -> Range -> OpItem
OpDefn PolyId
a' [[VarDecl]]
b' TypeScheme
c' Term
d' Range
e') }}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, OpItem)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.OpItem" ShATerm
u
instance ShATermConvertible HasCASL.As.Partiality where
toShATermAux :: ATermTable -> Partiality -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Partiality
xv = case Partiality
xv of
Partial -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Partial" [] []) ATermTable
att0
Total -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Total" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, Partiality)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Partial" [] _ -> (ATermTable
att0, Partiality
Partial)
ShAAppl "Total" [] _ -> (ATermTable
att0, Partiality
Total)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Partiality)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Partiality" ShATerm
u
instance ShATermConvertible HasCASL.As.TypeScheme where
toShATermAux :: ATermTable -> TypeScheme -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypeScheme
xv = case TypeScheme
xv of
TypeScheme a :: [TypeArg]
a b :: Type
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TypeArg] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TypeArg]
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypeScheme" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeScheme)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TypeScheme" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, [TypeArg])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TypeArg]
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
a' Type
b' Range
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypeScheme)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.TypeScheme" ShATerm
u
instance ShATermConvertible HasCASL.As.Type where
toShATermAux :: ATermTable -> Type -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Type
xv = case Type
xv of
TypeName a :: Id
a b :: RawKind
b c :: Int
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> RawKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 RawKind
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Int
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypeName" [Int
a', Int
b', Int
c'] []) ATermTable
att3
TypeAppl a :: Type
a b :: Type
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Type
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 "TypeAppl" [Int
a', Int
b'] []) ATermTable
att2
ExpandedType a :: Type
a b :: Type
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Type
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 "ExpandedType" [Int
a', Int
b'] []) ATermTable
att2
TypeAbs a :: TypeArg
a b :: Type
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypeArg -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypeArg
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypeAbs" [Int
a', Int
b', Int
c'] []) ATermTable
att3
KindedType a :: Type
a b :: Set Kind
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Type
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Set Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Set Kind
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "KindedType" [Int
a', Int
b', Int
c'] []) ATermTable
att3
TypeToken a :: Token
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "TypeToken" [Int
a'] []) ATermTable
att1
BracketType a :: BracketKind
a b :: [Type]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BracketKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 BracketKind
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BracketType" [Int
a', Int
b', Int
c'] []) ATermTable
att3
MixfixType a :: [Type]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Type] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Type]
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 "MixfixType" [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 "TypeName" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, RawKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: RawKind
b') ->
case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Int
c') ->
(ATermTable
att3, Id -> RawKind -> Int -> Type
TypeName Id
a' RawKind
b' Int
c') }}}
ShAAppl "TypeAppl" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Type
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, Type -> Type -> Type
TypeAppl Type
a' Type
b') }}
ShAAppl "ExpandedType" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Type
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, Type -> Type -> Type
ExpandedType Type
a' Type
b') }}
ShAAppl "TypeAbs" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, TypeArg)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypeArg
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, TypeArg -> Type -> Range -> Type
TypeAbs TypeArg
a' Type
b' Range
c') }}}
ShAAppl "KindedType" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Type
a') ->
case Int -> ATermTable -> (ATermTable, Set Kind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Set Kind
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Type -> Set Kind -> Range -> Type
KindedType Type
a' Set Kind
b' Range
c') }}}
ShAAppl "TypeToken" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Token
a') ->
(ATermTable
att1, Token -> Type
TypeToken Token
a') }
ShAAppl "BracketType" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, BracketKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: BracketKind
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
a' [Type]
b' Range
c') }}}
ShAAppl "MixfixType" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Type])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Type]
a') ->
(ATermTable
att1, [Type] -> Type
MixfixType [Type]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Type)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Type" ShATerm
u
instance ShATermConvertible HasCASL.As.TypePattern where
toShATermAux :: ATermTable -> TypePattern -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypePattern
xv = case TypePattern
xv of
TypePattern a :: Id
a b :: [TypeArg]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [TypeArg] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TypeArg]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypePattern" [Int
a', Int
b', Int
c'] []) ATermTable
att3
TypePatternToken a :: Token
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "TypePatternToken" [Int
a'] []) ATermTable
att1
MixfixTypePattern a :: [TypePattern]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TypePattern] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TypePattern]
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 "MixfixTypePattern" [Int
a'] []) ATermTable
att1
BracketTypePattern a :: BracketKind
a b :: [TypePattern]
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BracketKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 BracketKind
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [TypePattern] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [TypePattern]
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "BracketTypePattern" [Int
a', Int
b',
Int
c'] []) ATermTable
att3
TypePatternArg a :: TypeArg
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypeArg -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypeArg
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypePatternArg" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, TypePattern)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TypePattern" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
case Int -> ATermTable -> (ATermTable, [TypeArg])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [TypeArg]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, Id -> [TypeArg] -> Range -> TypePattern
TypePattern Id
a' [TypeArg]
b' Range
c') }}}
ShAAppl "TypePatternToken" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Token
a') ->
(ATermTable
att1, Token -> TypePattern
TypePatternToken Token
a') }
ShAAppl "MixfixTypePattern" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [TypePattern])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TypePattern]
a') ->
(ATermTable
att1, [TypePattern] -> TypePattern
MixfixTypePattern [TypePattern]
a') }
ShAAppl "BracketTypePattern" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, BracketKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: BracketKind
a') ->
case Int -> ATermTable -> (ATermTable, [TypePattern])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [TypePattern]
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, BracketKind -> [TypePattern] -> Range -> TypePattern
BracketTypePattern BracketKind
a' [TypePattern]
b' Range
c') }}}
ShAAppl "TypePatternArg" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, TypeArg)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypeArg
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, TypeArg -> Range -> TypePattern
TypePatternArg TypeArg
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypePattern)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.TypePattern" ShATerm
u
instance ShATermConvertible HasCASL.As.Vars where
toShATermAux :: ATermTable -> Vars -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Vars
xv = case Vars
xv of
Var a :: Id
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Id -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Id
a
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Var" [Int
a'] []) ATermTable
att1
VarTuple a :: [Vars]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Vars] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Vars]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "VarTuple" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, Vars)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Var" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Id)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Id
a') ->
(ATermTable
att1, Id -> Vars
Var Id
a') }
ShAAppl "VarTuple" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [Vars])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Vars]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [Vars] -> Range -> Vars
VarTuple [Vars]
a' Range
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Vars)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Vars" ShATerm
u
instance ShATermConvertible HasCASL.As.TypeItem where
toShATermAux :: ATermTable -> TypeItem -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TypeItem
xv = case TypeItem
xv of
TypeDecl a :: [TypePattern]
a b :: Kind
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TypePattern] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TypePattern]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Kind
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TypeDecl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
SubtypeDecl a :: [TypePattern]
a b :: Type
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TypePattern] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TypePattern]
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 -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Range
c
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SubtypeDecl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
IsoDecl a :: [TypePattern]
a b :: Range
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TypePattern] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TypePattern]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Range
b
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "IsoDecl" [Int
a', Int
b'] []) ATermTable
att2
SubtypeDefn a :: TypePattern
a b :: Vars
b c :: Type
c d :: Annoted Term
d e :: Range
e -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypePattern -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypePattern
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Vars -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Vars
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 -> Annoted Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Annoted Term
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Range
e
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SubtypeDefn" [Int
a', Int
b', Int
c', Int
d',
Int
e'] []) ATermTable
att5
AliasType a :: TypePattern
a b :: Maybe Kind
b c :: TypeScheme
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TypePattern -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TypePattern
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe Kind
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TypeScheme -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TypeScheme
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AliasType" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
Datatype a :: DatatypeDecl
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DatatypeDecl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DatatypeDecl
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 "Datatype" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeItem)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TypeDecl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, [TypePattern])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TypePattern]
a') ->
case Int -> ATermTable -> (ATermTable, Kind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Kind
b') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, [TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern]
a' Kind
b' Range
c') }}}
ShAAppl "SubtypeDecl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, [TypePattern])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TypePattern]
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, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: Range
c') ->
(ATermTable
att3, [TypePattern] -> Type -> Range -> TypeItem
SubtypeDecl [TypePattern]
a' Type
b' Range
c') }}}
ShAAppl "IsoDecl" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, [TypePattern])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TypePattern]
a') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Range
b') ->
(ATermTable
att2, [TypePattern] -> Range -> TypeItem
IsoDecl [TypePattern]
a' Range
b') }}
ShAAppl "SubtypeDefn" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
case Int -> ATermTable -> (ATermTable, TypePattern)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypePattern
a') ->
case Int -> ATermTable -> (ATermTable, Vars)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Vars
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, Annoted Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Annoted Term
d') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Range
e') ->
(ATermTable
att5, TypePattern -> Vars -> Type -> Annoted Term -> Range -> TypeItem
SubtypeDefn TypePattern
a' Vars
b' Type
c' Annoted Term
d' Range
e') }}}}}
ShAAppl "AliasType" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, TypePattern)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TypePattern
a') ->
case Int -> ATermTable -> (ATermTable, Maybe Kind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Maybe Kind
b') ->
case Int -> ATermTable -> (ATermTable, TypeScheme)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TypeScheme
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, TypePattern -> Maybe Kind -> TypeScheme -> Range -> TypeItem
AliasType TypePattern
a' Maybe Kind
b' TypeScheme
c' Range
d') }}}}
ShAAppl "Datatype" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, DatatypeDecl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: DatatypeDecl
a') ->
(ATermTable
att1, DatatypeDecl -> TypeItem
Datatype DatatypeDecl
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TypeItem)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.TypeItem" ShATerm
u
instance ShATermConvertible a => ShATermConvertible (HasCASL.As.AnyKind a) where
toShATermAux :: ATermTable -> AnyKind a -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AnyKind a
xv = case AnyKind a
xv of
ClassKind a :: a
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 a
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 "ClassKind" [Int
a'] []) ATermTable
att1
FunKind a :: Variance
a b :: AnyKind a
b c :: AnyKind a
c d :: Range
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Variance -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Variance
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> AnyKind a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 AnyKind a
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> AnyKind a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 AnyKind a
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Range
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "FunKind" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, AnyKind a)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "ClassKind" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: a
a') ->
(ATermTable
att1, a -> AnyKind a
forall a. a -> AnyKind a
ClassKind a
a') }
ShAAppl "FunKind" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case Int -> ATermTable -> (ATermTable, Variance)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Variance
a') ->
case Int -> ATermTable -> (ATermTable, AnyKind a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: AnyKind a
b') ->
case Int -> ATermTable -> (ATermTable, AnyKind a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: AnyKind a
c') ->
case Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: Range
d') ->
(ATermTable
att4, Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
a' AnyKind a
b' AnyKind a
c' Range
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AnyKind a)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.AnyKind" ShATerm
u
instance ShATermConvertible HasCASL.As.Variance where
toShATermAux :: ATermTable -> Variance -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Variance
xv = case Variance
xv of
InVar -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "InVar" [] []) ATermTable
att0
CoVar -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "CoVar" [] []) ATermTable
att0
ContraVar -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "ContraVar" [] []) ATermTable
att0
NonVar -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "NonVar" [] []) ATermTable
att0
fromShATermAux :: Int -> ATermTable -> (ATermTable, Variance)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "InVar" [] _ -> (ATermTable
att0, Variance
InVar)
ShAAppl "CoVar" [] _ -> (ATermTable
att0, Variance
CoVar)
ShAAppl "ContraVar" [] _ -> (ATermTable
att0, Variance
ContraVar)
ShAAppl "NonVar" [] _ -> (ATermTable
att0, Variance
NonVar)
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Variance)
forall a. String -> ShATerm -> a
fromShATermError "HasCASL.As.Variance" ShATerm
u
instance ShATermConvertible HasCASL.As.ClassDecl where
toShATermAux :: ATermTable -> ClassDecl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: ClassDecl
xv = case ClassDecl
xv of
ClassDecl a :: [Id]
a b :: Kind
b c :: Range
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Id] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Id]
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Kind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 <