Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(derive Typeable instances)
Safe HaskellNone

Isabelle.ATC_Isabelle

Contents

Description

Orphan instances

ShATermConvertible ProofMethod Source # 

Methods

toShATermAux :: ATermTable -> ProofMethod -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProofMethod] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofMethod)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofMethod])

ShATermConvertible Modifier Source # 

Methods

toShATermAux :: ATermTable -> Modifier -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Modifier] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Modifier)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Modifier])

ShATermConvertible ProofEnd Source # 

Methods

toShATermAux :: ATermTable -> ProofEnd -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProofEnd] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofEnd)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofEnd])

ShATermConvertible ProofCommand Source # 

Methods

toShATermAux :: ATermTable -> ProofCommand -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProofCommand] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofCommand)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofCommand])

ShATermConvertible IsaProof Source # 

Methods

toShATermAux :: ATermTable -> IsaProof -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [IsaProof] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, IsaProof)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [IsaProof])

ShATermConvertible Sign Source # 

Methods

toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])

ShATermConvertible BaseSig Source # 

Methods

toShATermAux :: ATermTable -> BaseSig -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BaseSig] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BaseSig)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BaseSig])

ShATermConvertible TypeSig Source # 

Methods

toShATermAux :: ATermTable -> TypeSig -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TypeSig] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeSig)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeSig])

ShATermConvertible MetaTerm Source # 

Methods

toShATermAux :: ATermTable -> MetaTerm -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [MetaTerm] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, MetaTerm)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [MetaTerm])

ShATermConvertible SetDecl Source # 

Methods

toShATermAux :: ATermTable -> SetDecl -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SetDecl] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SetDecl)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SetDecl])

ShATermConvertible FunSig Source # 

Methods

toShATermAux :: ATermTable -> FunSig -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FunSig] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FunSig)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FunSig])

ShATermConvertible Axiom Source # 

Methods

toShATermAux :: ATermTable -> Axiom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Axiom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Axiom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Axiom])

ShATermConvertible DomainConstructorArg Source # 

Methods

toShATermAux :: ATermTable -> DomainConstructorArg -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DomainConstructorArg] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DomainConstructorArg)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DomainConstructorArg])

ShATermConvertible DomainConstructor Source # 

Methods

toShATermAux :: ATermTable -> DomainConstructor -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DomainConstructor] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DomainConstructor)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DomainConstructor])

ShATermConvertible Domain Source # 

Methods

toShATermAux :: ATermTable -> Domain -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Domain] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Domain)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Domain])

ShATermConvertible DatatypeConstructor Source # 

Methods

toShATermAux :: ATermTable -> DatatypeConstructor -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DatatypeConstructor] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DatatypeConstructor)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DatatypeConstructor])

ShATermConvertible Datatype Source # 

Methods

toShATermAux :: ATermTable -> Datatype -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Datatype] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Datatype)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Datatype])

ShATermConvertible MixfixTemplate Source # 

Methods

toShATermAux :: ATermTable -> MixfixTemplate -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [MixfixTemplate] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, MixfixTemplate)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [MixfixTemplate])

ShATermConvertible Mixfix Source # 

Methods

toShATermAux :: ATermTable -> Mixfix -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Mixfix] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Mixfix)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Mixfix])

ShATermConvertible Ctxt Source # 

Methods

toShATermAux :: ATermTable -> Ctxt -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Ctxt] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Ctxt)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Ctxt])

ShATermConvertible FixrecEquation Source # 

Methods

toShATermAux :: ATermTable -> FixrecEquation -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FixrecEquation] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FixrecEquation)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FixrecEquation])

ShATermConvertible DefEquation Source # 

Methods

toShATermAux :: ATermTable -> DefEquation -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DefEquation] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DefEquation)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefEquation])

ShATermConvertible Sentence Source # 

Methods

toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])

ShATermConvertible Props Source # 

Methods

toShATermAux :: ATermTable -> Props -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Props] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Props)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Props])

ShATermConvertible Prop Source # 

Methods

toShATermAux :: ATermTable -> Prop -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Prop] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Prop)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Prop])

ShATermConvertible Term Source # 

Methods

toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])

ShATermConvertible DTyp Source # 

Methods

toShATermAux :: ATermTable -> DTyp -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DTyp] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DTyp)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DTyp])

ShATermConvertible TAttr Source # 

Methods

toShATermAux :: ATermTable -> TAttr -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TAttr] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TAttr)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TAttr])

ShATermConvertible Continuity Source # 

Methods

toShATermAux :: ATermTable -> Continuity -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Continuity] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Continuity)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Continuity])

ShATermConvertible Typ Source # 

Methods

toShATermAux :: ATermTable -> Typ -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Typ] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Typ)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Typ])

ShATermConvertible IsaClass Source # 

Methods

toShATermAux :: ATermTable -> IsaClass -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [IsaClass] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, IsaClass)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [IsaClass])

ShATermConvertible Indexname Source # 

Methods

toShATermAux :: ATermTable -> Indexname -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Indexname] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Indexname)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Indexname])

ShATermConvertible QName Source # 

Methods

toShATermAux :: ATermTable -> QName -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [QName] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, QName)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [QName])

ShATermConvertible VName Source # 

Methods

toShATermAux :: ATermTable -> VName -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [VName] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, VName)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [VName])

ShATermConvertible AltSyntax Source # 

Methods

toShATermAux :: ATermTable -> AltSyntax -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [AltSyntax] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, AltSyntax)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [AltSyntax])