Copyright	(c) University of Cambridge Cambridge England adaption (c) Till Mossakowski Uni Bremen 2002-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Isabelle.IsaSign

Description

Data structures for Isabelle signatures and theories. Adapted from Isabelle.

Synopsis

type TName = String
data AltSyntax = AltSyntax String [Int] Int
data VName = VName {
- new :: String
- altSyn :: Maybe AltSyntax
}
orig :: VName -> String
data QName = QName {
- qname :: String
- qualifiers :: [String]
}
mkQName :: String -> QName
data Indexname = Indexname {
- unindexed :: String
- indexOffset :: Int
}
data IsaClass = IsaClass String
type Sort = [IsaClass]
data Typ
- = Type {
  - typeId :: TName
  - typeSort :: Sort
  - typeArgs :: [Typ]
  }
- | TFree {
  - typeId :: TName
  - typeSort :: Sort
  }
- | TVar {
  - indexname :: Indexname
  - typeSort :: Sort
  }
data Continuity
- = IsCont Bool
- | NotCont
data TAttr
- = TFun
- | TMet
- | TCon
- | NA
data DTyp
- = Hide {
  - typ :: Typ
  - kon :: TAttr
  - arit :: Maybe Int
  }
- | Disp {
  - typ :: Typ
  - kon :: TAttr
  - arit :: Maybe Int
  }
data Term
- = Const {
  - termName :: VName
  - termType :: DTyp
  }
- | Free {
  - termName :: VName
  }
- | Abs {
  - absVar :: Term
  - termId :: Term
  - continuity :: Continuity
  }
- | App {
  - funId :: Term
  - argId :: Term
  - continuity :: Continuity
  }
- | If {
  - ifId :: Term
  - thenId :: Term
  - elseId :: Term
  - continuity :: Continuity
  }
- | Case {
  - termId :: Term
  - caseSubst :: [(Term, Term)]
  }
- | Let {
  - letSubst :: [(Term, Term)]
  - inId :: Term
  }
- | IsaEq {
  - firstTerm :: Term
  - secondTerm :: Term
  }
- | Tuplex [Term] Continuity
- | Set SetDecl
data Prop = Prop {
- prop :: Term
- propPats :: [Term]
}
data Props = Props {
- propsName :: Maybe QName
- propsArgs :: Maybe String
- props :: [Prop]
}
data Sentence
- = Sentence {
  - isSimp :: Bool
  - isRefuteAux :: Bool
  - metaTerm :: MetaTerm
  - thmProof :: Maybe IsaProof
  }
- | Instance {
  - tName :: TName
  - arityArgs :: [Sort]
  - arityRes :: Sort
  - definitions :: [(String, Term)]
  - instProof :: IsaProof
  }
- | ConstDef {
  - senTerm :: Term
  }
- | RecDef {
  - keyword :: Maybe String
  - constName :: VName
  - constType :: Maybe Typ
  - primRecSenTerms :: [Term]
  }
- | TypeDef {
  - newType :: Typ
  - typeDef :: SetDecl
  - nonEmptyPr :: IsaProof
  }
- | Lemmas {
  - lemmaName :: String
  - lemmasList :: [String]
  }
- | Locale {
  - localeName :: QName
  - localeContext :: Ctxt
  - localeParents :: [QName]
  - localeBody :: [Sentence]
  }
- | Class {
  - className :: QName
  - classContext :: Ctxt
  - classParents :: [QName]
  - classBody :: [Sentence]
  }
- | Datatypes [Datatype]
- | Domains [Domain]
- | Consts [(String, Maybe Mixfix, Typ)]
- | TypeSynonym QName (Maybe Mixfix) [String] Typ
- | Axioms [Axiom]
- | Lemma {
  - lemmaTarget :: Maybe QName
  - lemmaContext :: Ctxt
  - lemmaProof :: Maybe String
  - lemmaProps :: [Props]
  }
- | Definition {
  - definitionName :: QName
  - definitionMixfix :: Maybe Mixfix
  - definitionTarget :: Maybe String
  - definitionType :: Typ
  - definitionVars :: [Term]
  - definitionTerm :: Term
  }
- | Fun {
  - funTarget :: Maybe QName
  - funSequential :: Bool
  - funDefault :: Maybe String
  - funDomintros :: Bool
  - funPartials :: Bool
  - funEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
  }
- | Primrec {
  - primrecTarget :: Maybe QName
  - primrecEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
  }
- | Fixrec [(String, Maybe Mixfix, Typ, [FixrecEquation])]
- | Instantiation {
  - instantiationType :: TName
  - instantiationArity :: (Sort, [Sort])
  - instantiationBody :: [Sentence]
  }
- | InstanceProof {
  - instanceProof :: String
  }
- | InstanceArity {
  - instanceTypes :: [TName]
  - instanceArity :: (Sort, [Sort])
  - instanceProof :: String
  }
- | InstanceSubclass {
  - instanceClass :: String
  - instanceRel :: String
  - instanceClass1 :: String
  - instanceProof :: String
  }
- | Subclass {
  - subclassClass :: String
  - subclassTarget :: Maybe QName
  - subclassProof :: String
  }
- | Typedef {
  - typedefName :: QName
  - typedefVars :: [(String, Sort)]
  - typedefMixfix :: Maybe Mixfix
  - typedefMorphisms :: Maybe (QName, QName)
  - typedefTerm :: Term
  - typedefProof :: String
  }
- | Defs {
  - defsUnchecked :: Bool
  - defsOverloaded :: Bool
  - defsEquations :: [DefEquation]
  }
data DefEquation = DefEquation {
- defEquationName :: QName
- defEquationConst :: String
- defEquationConstType :: Typ
- defEquationTerm :: Term
- defEquationArgs :: String
}
data FixrecEquation = FixrecEquation {
- fixrecEquationUnchecked :: Bool
- fixrecEquationPremises :: [Term]
- fixrecEquationPatterns :: [Term]
- fixrecEquationTerm :: Term
}
data Ctxt = Ctxt {
- fixes :: [(String, Maybe Mixfix, Typ)]
- assumes :: [(String, Term)]
}
data Mixfix = Mixfix {
- mixfixNargs :: Int
- mixfixPrio :: Int
- mixfixPretty :: String
- mixfixTemplate :: [MixfixTemplate]
}
data MixfixTemplate
- = Arg Int
- | Str String
- | Break Int
- | Block Int [MixfixTemplate]
data Datatype = Datatype {
- datatypeName :: QName
- datatypeTVars :: [Typ]
- datatypeMixfix :: Maybe Mixfix
- datatypeConstructors :: [DatatypeConstructor]
}
data DatatypeConstructor
- = DatatypeConstructor {
  - constructorName :: QName
  - constructorType :: Typ
  - constructorMixfix :: Maybe Mixfix
  - constructorArgs :: [Typ]
  }
- | DatatypeNoConstructor {
  - constructorArgs :: [Typ]
  }
data Domain = Domain {
- domainName :: QName
- domainTVars :: [Typ]
- domainMixfix :: Maybe Mixfix
- domainConstructors :: [DomainConstructor]
}
data DomainConstructor = DomainConstructor {
- domainConstructorName :: QName
- domainConstructorType :: Typ
- domainConstructorArgs :: [DomainConstructorArg]
}
data DomainConstructorArg = DomainConstructorArg {
- domainConstructorArgSel :: Maybe QName
- domainConstructorArgType :: Typ
- domainConstructorArgLazy :: Bool
}
data Axiom = Axiom {
- axiomName :: QName
- axiomArgs :: String
- axiomTerm :: Term
}
data FunSig = FunSig {
- funSigName :: QName
- funSigType :: Maybe Typ
}
data SetDecl
- = SubSet Term Typ Term
- | FixedSet [Term]
data MetaTerm
- = Term Term
- | Conditional [Term] Term
mkSenAux :: Bool -> MetaTerm -> Sentence
mkSen :: Term -> Sentence
mkCond :: [Term] -> Term -> Sentence
mkRefuteSen :: Term -> Sentence
isRefute :: Sentence -> Bool
type ClassDecl = ([IsaClass], [(String, Term)], [(String, Typ)])
type Classrel = Map IsaClass ClassDecl
type LocaleDecl = ([String], [(String, Term)], [(String, Term)], [(String, Typ, Maybe AltSyntax)])
type Def = (Typ, [(String, Typ)], Term)
type FunDef = (Typ, [([Term], Term)])
type Locales = Map String LocaleDecl
type Defs = Map String Def
type Funs = Map String FunDef
type Arities = Map TName [(IsaClass, [(Typ, Sort)])]
type Abbrs = Map TName ([TName], Typ)
data TypeSig = TySg {
- classrel :: Classrel
- locales :: Locales
- defs :: Defs
- funs :: Funs
- defaultSort :: Sort
- log_types :: [TName]
- univ_witness :: Maybe (Typ, Sort)
- abbrs :: Abbrs
- arities :: Arities
}
emptyTypeSig :: TypeSig
isSubTypeSig :: TypeSig -> TypeSig -> Bool
data BaseSig
- = Main_thy
- | Custom_thy
- | MainHC_thy
- | MainHCPairs_thy
- | HOLCF_thy
- | HsHOLCF_thy
- | HsHOL_thy
- | MHsHOL_thy
- | MHsHOLCF_thy
- | CspHOLComplex_thy
data Sign = Sign {
- theoryName :: String
- header :: Maybe String
- keywords :: [String]
- uses :: [String]
- baseSig :: BaseSig
- imports :: [String]
- tsig :: TypeSig
- constTab :: ConstTab
- domainTab :: DomainTab
- showLemmas :: Bool
}
type ConstTab = Map VName Typ
type DomainTab = [[DomainEntry]]
type DomainEntry = (Typ, [(VName, [Typ])])
emptySign :: Sign
isSubSign :: Sign -> Sign -> Bool
union_tsig :: TypeSig -> TypeSig -> TypeSig
union_sig :: Sign -> Sign -> Sign
data IsaProof = IsaProof {
- proof :: [ProofCommand]
- end :: ProofEnd
}
data ProofCommand
- = Apply [ProofMethod] Bool
- | Using [String]
- | Back
- | Defer Int
- | Prefer Int
- | Refute
data ProofEnd
- = By ProofMethod
- | DotDot
- | Done
- | Oops
- | Sorry
data Modifier
- = No_asm
- | No_asm_simp
- | No_asm_use
data ProofMethod
- = Auto
- | Simp
- | AutoSimpAdd (Maybe Modifier) [String]
- | SimpAdd (Maybe Modifier) [String]
- | Induct Term
- | CaseTac Term
- | SubgoalTac Term
- | Insert [String]
- | Other String
toIsaProof :: ProofEnd -> IsaProof
mkOops :: IsaProof

Documentation

type TName = String Source #

type names

data AltSyntax Source #

Constructors

AltSyntax String [Int] Int

Instances

Instances details

Eq AltSyntax Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: AltSyntax -> AltSyntax -> Bool (/=) :: AltSyntax -> AltSyntax -> Bool
Data AltSyntax Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AltSyntax -> c AltSyntax gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AltSyntax toConstr :: AltSyntax -> Constr dataTypeOf :: AltSyntax -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AltSyntax) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltSyntax) gmapT :: (forall b. Data b => b -> b) -> AltSyntax -> AltSyntax gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AltSyntax -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AltSyntax -> r gmapQ :: (forall d. Data d => d -> u) -> AltSyntax -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AltSyntax -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax
Ord AltSyntax Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: AltSyntax -> AltSyntax -> Ordering (<) :: AltSyntax -> AltSyntax -> Bool (<=) :: AltSyntax -> AltSyntax -> Bool (>) :: AltSyntax -> AltSyntax -> Bool (>=) :: AltSyntax -> AltSyntax -> Bool max :: AltSyntax -> AltSyntax -> AltSyntax min :: AltSyntax -> AltSyntax -> AltSyntax
Show AltSyntax Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> AltSyntax -> ShowS show :: AltSyntax -> String showList :: [AltSyntax] -> ShowS
Generic AltSyntax
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep AltSyntax :: Type -> Type Methods from :: AltSyntax -> Rep AltSyntax x to :: Rep AltSyntax x -> AltSyntax
FromJSON AltSyntax
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser AltSyntax parseJSONList :: Value -> Parser [AltSyntax]
ToJSON AltSyntax
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: AltSyntax -> Value toEncoding :: AltSyntax -> Encoding toJSONList :: [AltSyntax] -> Value toEncodingList :: [AltSyntax] -> Encoding
ShATermConvertible AltSyntax
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> AltSyntax -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [AltSyntax] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, AltSyntax) fromShATermList' :: Int -> ATermTable -> (ATermTable, [AltSyntax])
type Rep AltSyntax
Instance details Defined in Isabelle.ATC_Isabelle type Rep AltSyntax = D1 ('MetaData "AltSyntax" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "AltSyntax" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

data VName Source #

names for values or constants (non-classes and non-types)

Constructors

VName
Fields new :: String name within Isabelle altSyn :: Maybe AltSyntax mixfix template syntax

Instances

Instances details

Eq VName Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: VName -> VName -> Bool (/=) :: VName -> VName -> Bool
Data VName Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VName -> c VName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VName toConstr :: VName -> Constr dataTypeOf :: VName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VName) gmapT :: (forall b. Data b => b -> b) -> VName -> VName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VName -> r gmapQ :: (forall d. Data d => d -> u) -> VName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VName -> m VName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VName -> m VName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VName -> m VName
Ord VName Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: VName -> VName -> Ordering (<) :: VName -> VName -> Bool (<=) :: VName -> VName -> Bool (>) :: VName -> VName -> Bool (>=) :: VName -> VName -> Bool max :: VName -> VName -> VName min :: VName -> VName -> VName
Show VName Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> VName -> ShowS show :: VName -> String showList :: [VName] -> ShowS
Generic VName
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep VName :: Type -> Type Methods from :: VName -> Rep VName x to :: Rep VName x -> VName
FromJSON VName
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser VName parseJSONList :: Value -> Parser [VName]
ToJSON VName
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: VName -> Value toEncoding :: VName -> Encoding toJSONList :: [VName] -> Value toEncodingList :: [VName] -> Encoding
ShATermConvertible VName
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> VName -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [VName] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, VName) fromShATermList' :: Int -> ATermTable -> (ATermTable, [VName])
type Rep VName
Instance details Defined in Isabelle.ATC_Isabelle type Rep VName = D1 ('MetaData "VName" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "VName" 'PrefixI 'True) (S1 ('MetaSel ('Just "new") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "altSyn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe AltSyntax))))

orig :: VName -> String Source #

the original (Haskell) name

data QName Source #

Constructors

QName
Fields qname :: String qualifiers :: [String]

Instances

Instances details

Eq QName Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: QName -> QName -> Bool (/=) :: QName -> QName -> Bool
Data QName Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QName -> c QName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName toConstr :: QName -> Constr dataTypeOf :: QName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName) gmapT :: (forall b. Data b => b -> b) -> QName -> QName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r gmapQ :: (forall d. Data d => d -> u) -> QName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName
Ord QName Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: QName -> QName -> Ordering (<) :: QName -> QName -> Bool (<=) :: QName -> QName -> Bool (>) :: QName -> QName -> Bool (>=) :: QName -> QName -> Bool max :: QName -> QName -> QName min :: QName -> QName -> QName
Show QName Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> QName -> ShowS show :: QName -> String showList :: [QName] -> ShowS
Generic QName
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep QName :: Type -> Type Methods from :: QName -> Rep QName x to :: Rep QName x -> QName
FromJSON QName
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser QName parseJSONList :: Value -> Parser [QName]
ToJSON QName
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: QName -> Value toEncoding :: QName -> Encoding toJSONList :: [QName] -> Value toEncodingList :: [QName] -> Encoding
ShATermConvertible QName
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> QName -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [QName] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, QName) fromShATermList' :: Int -> ATermTable -> (ATermTable, [QName])
type Rep QName
Instance details Defined in Isabelle.ATC_Isabelle type Rep QName = D1 ('MetaData "QName" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "QName" 'PrefixI 'True) (S1 ('MetaSel ('Just "qname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "qualifiers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))

mkQName :: String -> QName Source #

data Indexname Source #

Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.

Constructors

Indexname
Fields unindexed :: String indexOffset :: Int

Instances

Instances details

Eq Indexname Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Indexname -> Indexname -> Bool (/=) :: Indexname -> Indexname -> Bool
Data Indexname Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Indexname -> c Indexname gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Indexname toConstr :: Indexname -> Constr dataTypeOf :: Indexname -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Indexname) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Indexname) gmapT :: (forall b. Data b => b -> b) -> Indexname -> Indexname gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Indexname -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Indexname -> r gmapQ :: (forall d. Data d => d -> u) -> Indexname -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Indexname -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname
Ord Indexname Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Indexname -> Indexname -> Ordering (<) :: Indexname -> Indexname -> Bool (<=) :: Indexname -> Indexname -> Bool (>) :: Indexname -> Indexname -> Bool (>=) :: Indexname -> Indexname -> Bool max :: Indexname -> Indexname -> Indexname min :: Indexname -> Indexname -> Indexname
Show Indexname Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Indexname -> ShowS show :: Indexname -> String showList :: [Indexname] -> ShowS
Generic Indexname
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Indexname :: Type -> Type Methods from :: Indexname -> Rep Indexname x to :: Rep Indexname x -> Indexname
FromJSON Indexname
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Indexname parseJSONList :: Value -> Parser [Indexname]
ToJSON Indexname
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Indexname -> Value toEncoding :: Indexname -> Encoding toJSONList :: [Indexname] -> Value toEncodingList :: [Indexname] -> Encoding
ShATermConvertible Indexname
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Indexname -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Indexname] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Indexname) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Indexname])
type Rep Indexname
Instance details Defined in Isabelle.ATC_Isabelle type Rep Indexname = D1 ('MetaData "Indexname" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Indexname" 'PrefixI 'True) (S1 ('MetaSel ('Just "unindexed") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "indexOffset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

data IsaClass Source #

Constructors

IsaClass String

Instances

Instances details

Eq IsaClass Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: IsaClass -> IsaClass -> Bool (/=) :: IsaClass -> IsaClass -> Bool
Data IsaClass Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsaClass -> c IsaClass gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsaClass toConstr :: IsaClass -> Constr dataTypeOf :: IsaClass -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsaClass) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsaClass) gmapT :: (forall b. Data b => b -> b) -> IsaClass -> IsaClass gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsaClass -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsaClass -> r gmapQ :: (forall d. Data d => d -> u) -> IsaClass -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsaClass -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass
Ord IsaClass Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: IsaClass -> IsaClass -> Ordering (<) :: IsaClass -> IsaClass -> Bool (<=) :: IsaClass -> IsaClass -> Bool (>) :: IsaClass -> IsaClass -> Bool (>=) :: IsaClass -> IsaClass -> Bool max :: IsaClass -> IsaClass -> IsaClass min :: IsaClass -> IsaClass -> IsaClass
Show IsaClass Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> IsaClass -> ShowS show :: IsaClass -> String showList :: [IsaClass] -> ShowS
Generic IsaClass
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep IsaClass :: Type -> Type Methods from :: IsaClass -> Rep IsaClass x to :: Rep IsaClass x -> IsaClass
FromJSON IsaClass
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser IsaClass parseJSONList :: Value -> Parser [IsaClass]
ToJSON IsaClass
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: IsaClass -> Value toEncoding :: IsaClass -> Encoding toJSONList :: [IsaClass] -> Value toEncodingList :: [IsaClass] -> Encoding
ShATermConvertible IsaClass
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> IsaClass -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [IsaClass] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, IsaClass) fromShATermList' :: Int -> ATermTable -> (ATermTable, [IsaClass])
type Rep IsaClass
Instance details Defined in Isabelle.ATC_Isabelle type Rep IsaClass = D1 ('MetaData "IsaClass" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "IsaClass" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

type Sort = [IsaClass] Source #

data Typ Source #

Constructors

Type
Fields typeId :: TName typeSort :: Sort typeArgs :: [Typ]
TFree
Fields typeId :: TName typeSort :: Sort
TVar
Fields indexname :: Indexname typeSort :: Sort

Instances

Instances details

Eq Typ Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Typ -> Typ -> Bool (/=) :: Typ -> Typ -> Bool
Data Typ Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Typ -> c Typ gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Typ toConstr :: Typ -> Constr dataTypeOf :: Typ -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Typ) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ) gmapT :: (forall b. Data b => b -> b) -> Typ -> Typ gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r gmapQ :: (forall d. Data d => d -> u) -> Typ -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Typ -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Typ -> m Typ gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ
Ord Typ Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Typ -> Typ -> Ordering (<) :: Typ -> Typ -> Bool (<=) :: Typ -> Typ -> Bool (>) :: Typ -> Typ -> Bool (>=) :: Typ -> Typ -> Bool max :: Typ -> Typ -> Typ min :: Typ -> Typ -> Typ
Show Typ Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Typ -> ShowS show :: Typ -> String showList :: [Typ] -> ShowS
Generic Typ
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Typ :: Type -> Type Methods from :: Typ -> Rep Typ x to :: Rep Typ x -> Typ
FromJSON Typ
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Typ parseJSONList :: Value -> Parser [Typ]
ToJSON Typ
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Typ -> Value toEncoding :: Typ -> Encoding toJSONList :: [Typ] -> Value toEncodingList :: [Typ] -> Encoding
ShATermConvertible Typ
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Typ -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Typ] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Typ) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Typ])
type Rep Typ
Instance details Defined in Isabelle.ATC_Isabelle type Rep Typ = D1 ('MetaData "Typ" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Type" 'PrefixI 'True) (S1 ('MetaSel ('Just "typeId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TName) :: (S1 ('MetaSel ('Just "typeSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: S1 ('MetaSel ('Just "typeArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Typ]))) :+: (C1 ('MetaCons "TFree" 'PrefixI 'True) (S1 ('MetaSel ('Just "typeId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TName) :: S1 ('MetaSel ('Just "typeSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: C1 ('MetaCons "TVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "indexname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Indexname) :: S1 ('MetaSel ('Just "typeSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort))))

data Continuity Source #

Constructors

IsCont Bool
NotCont

Instances

Instances details

Eq Continuity Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Continuity -> Continuity -> Bool (/=) :: Continuity -> Continuity -> Bool
Data Continuity Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Continuity -> c Continuity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Continuity toConstr :: Continuity -> Constr dataTypeOf :: Continuity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Continuity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Continuity) gmapT :: (forall b. Data b => b -> b) -> Continuity -> Continuity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Continuity -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Continuity -> r gmapQ :: (forall d. Data d => d -> u) -> Continuity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Continuity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity
Ord Continuity Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Continuity -> Continuity -> Ordering (<) :: Continuity -> Continuity -> Bool (<=) :: Continuity -> Continuity -> Bool (>) :: Continuity -> Continuity -> Bool (>=) :: Continuity -> Continuity -> Bool max :: Continuity -> Continuity -> Continuity min :: Continuity -> Continuity -> Continuity
Show Continuity Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Continuity -> ShowS show :: Continuity -> String showList :: [Continuity] -> ShowS
Generic Continuity
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Continuity :: Type -> Type Methods from :: Continuity -> Rep Continuity x to :: Rep Continuity x -> Continuity
FromJSON Continuity
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Continuity parseJSONList :: Value -> Parser [Continuity]
ToJSON Continuity
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Continuity -> Value toEncoding :: Continuity -> Encoding toJSONList :: [Continuity] -> Value toEncodingList :: [Continuity] -> Encoding
ShATermConvertible Continuity
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Continuity -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Continuity] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Continuity) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Continuity])
type Rep Continuity
Instance details Defined in Isabelle.ATC_Isabelle type Rep Continuity = D1 ('MetaData "Continuity" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "IsCont" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "NotCont" 'PrefixI 'False) (U1 :: Type -> Type))

data TAttr Source #

Constructors

TFun
TMet
TCon
NA

Instances

Instances details

Eq TAttr Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: TAttr -> TAttr -> Bool (/=) :: TAttr -> TAttr -> Bool
Data TAttr Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TAttr -> c TAttr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TAttr toConstr :: TAttr -> Constr dataTypeOf :: TAttr -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TAttr) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAttr) gmapT :: (forall b. Data b => b -> b) -> TAttr -> TAttr gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAttr -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAttr -> r gmapQ :: (forall d. Data d => d -> u) -> TAttr -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TAttr -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr
Ord TAttr Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: TAttr -> TAttr -> Ordering (<) :: TAttr -> TAttr -> Bool (<=) :: TAttr -> TAttr -> Bool (>) :: TAttr -> TAttr -> Bool (>=) :: TAttr -> TAttr -> Bool max :: TAttr -> TAttr -> TAttr min :: TAttr -> TAttr -> TAttr
Show TAttr Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> TAttr -> ShowS show :: TAttr -> String showList :: [TAttr] -> ShowS
Generic TAttr
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep TAttr :: Type -> Type Methods from :: TAttr -> Rep TAttr x to :: Rep TAttr x -> TAttr
FromJSON TAttr
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser TAttr parseJSONList :: Value -> Parser [TAttr]
ToJSON TAttr
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: TAttr -> Value toEncoding :: TAttr -> Encoding toJSONList :: [TAttr] -> Value toEncodingList :: [TAttr] -> Encoding
ShATermConvertible TAttr
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> TAttr -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TAttr] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TAttr) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TAttr])
type Rep TAttr
Instance details Defined in Isabelle.ATC_Isabelle type Rep TAttr = D1 ('MetaData "TAttr" "Isabelle.IsaSign" "main" 'False) ((C1 ('MetaCons "TFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TMet" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TCon" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NA" 'PrefixI 'False) (U1 :: Type -> Type)))

data DTyp Source #

Constructors

Hide
Fields typ :: Typ kon :: TAttr arit :: Maybe Int
Disp
Fields typ :: Typ kon :: TAttr arit :: Maybe Int

Instances

Instances details

Eq DTyp Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: DTyp -> DTyp -> Bool (/=) :: DTyp -> DTyp -> Bool
Data DTyp Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DTyp -> c DTyp gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DTyp toConstr :: DTyp -> Constr dataTypeOf :: DTyp -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DTyp) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp) gmapT :: (forall b. Data b => b -> b) -> DTyp -> DTyp gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r gmapQ :: (forall d. Data d => d -> u) -> DTyp -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DTyp -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp
Ord DTyp Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: DTyp -> DTyp -> Ordering (<) :: DTyp -> DTyp -> Bool (<=) :: DTyp -> DTyp -> Bool (>) :: DTyp -> DTyp -> Bool (>=) :: DTyp -> DTyp -> Bool max :: DTyp -> DTyp -> DTyp min :: DTyp -> DTyp -> DTyp
Show DTyp Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> DTyp -> ShowS show :: DTyp -> String showList :: [DTyp] -> ShowS
Generic DTyp
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep DTyp :: Type -> Type Methods from :: DTyp -> Rep DTyp x to :: Rep DTyp x -> DTyp
FromJSON DTyp
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser DTyp parseJSONList :: Value -> Parser [DTyp]
ToJSON DTyp
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: DTyp -> Value toEncoding :: DTyp -> Encoding toJSONList :: [DTyp] -> Value toEncodingList :: [DTyp] -> Encoding
ShATermConvertible DTyp
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> DTyp -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DTyp] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DTyp) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DTyp])
type Rep DTyp
Instance details Defined in Isabelle.ATC_Isabelle type Rep DTyp = D1 ('MetaData "DTyp" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Hide" 'PrefixI 'True) (S1 ('MetaSel ('Just "typ") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: (S1 ('MetaSel ('Just "kon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TAttr) :: S1 ('MetaSel ('Just "arit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))) :+: C1 ('MetaCons "Disp" 'PrefixI 'True) (S1 ('MetaSel ('Just "typ") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: (S1 ('MetaSel ('Just "kon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TAttr) :: S1 ('MetaSel ('Just "arit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))))

data Term Source #

Constructors

Const
Fields termName :: VName termType :: DTyp
Free
Fields termName :: VName
Abs
Fields absVar :: Term termId :: Term continuity :: Continuity
App
Fields funId :: Term argId :: Term continuity :: Continuity
If
Fields ifId :: Term thenId :: Term elseId :: Term continuity :: Continuity
Case
Fields termId :: Term caseSubst :: [(Term, Term)]
Let
Fields letSubst :: [(Term, Term)] inId :: Term
IsaEq
Fields firstTerm :: Term secondTerm :: Term
Tuplex [Term] Continuity
Set SetDecl

Instances

Instances details

Eq Term Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Term -> Term -> Bool (/=) :: Term -> Term -> Bool
Data Term Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term toConstr :: Term -> Constr dataTypeOf :: Term -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) gmapT :: (forall b. Data b => b -> b) -> Term -> Term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term
Ord Term Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Term -> Term -> Ordering (<) :: Term -> Term -> Bool (<=) :: Term -> Term -> Bool (>) :: Term -> Term -> Bool (>=) :: Term -> Term -> Bool max :: Term -> Term -> Term min :: Term -> Term -> Term
Show Term Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Term -> ShowS show :: Term -> String showList :: [Term] -> ShowS
Generic Term
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Term :: Type -> Type Methods from :: Term -> Rep Term x to :: Rep Term x -> Term
FromJSON Term
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Term parseJSONList :: Value -> Parser [Term]
ToJSON Term
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Term -> Value toEncoding :: Term -> Encoding toJSONList :: [Term] -> Value toEncodingList :: [Term] -> Encoding
ShATermConvertible Term
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Term) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])
type Rep Term
Instance details Defined in Isabelle.ATC_Isabelle type Rep Term = D1 ('MetaData "Term" "Isabelle.IsaSign" "main" 'False) (((C1 ('MetaCons "Const" 'PrefixI 'True) (S1 ('MetaSel ('Just "termName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VName) :: S1 ('MetaSel ('Just "termType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DTyp)) :+: C1 ('MetaCons "Free" 'PrefixI 'True) (S1 ('MetaSel ('Just "termName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VName))) :+: (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Just "termId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "continuity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Continuity))) :+: (C1 ('MetaCons "App" 'PrefixI 'True) (S1 ('MetaSel ('Just "funId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Just "argId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "continuity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Continuity))) :+: C1 ('MetaCons "If" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "thenId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :: (S1 ('MetaSel ('Just "elseId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "continuity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Continuity)))))) :+: ((C1 ('MetaCons "Case" 'PrefixI 'True) (S1 ('MetaSel ('Just "termId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "caseSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term, Term)])) :+: C1 ('MetaCons "Let" 'PrefixI 'True) (S1 ('MetaSel ('Just "letSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term, Term)]) :: S1 ('MetaSel ('Just "inId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "IsaEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "firstTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "secondTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "Tuplex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Continuity)) :+: C1 ('MetaCons "Set" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SetDecl))))))

data Prop Source #

Constructors

Prop
Fields prop :: Term propPats :: [Term]

Instances

Instances details

Eq Prop Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Prop -> Prop -> Bool (/=) :: Prop -> Prop -> Bool
Data Prop Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Prop -> c Prop gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Prop toConstr :: Prop -> Constr dataTypeOf :: Prop -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Prop) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Prop) gmapT :: (forall b. Data b => b -> b) -> Prop -> Prop gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Prop -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Prop -> r gmapQ :: (forall d. Data d => d -> u) -> Prop -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Prop -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Prop -> m Prop gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Prop -> m Prop gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Prop -> m Prop
Ord Prop Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Prop -> Prop -> Ordering (<) :: Prop -> Prop -> Bool (<=) :: Prop -> Prop -> Bool (>) :: Prop -> Prop -> Bool (>=) :: Prop -> Prop -> Bool max :: Prop -> Prop -> Prop min :: Prop -> Prop -> Prop
Show Prop Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Prop -> ShowS show :: Prop -> String showList :: [Prop] -> ShowS
Generic Prop
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Prop :: Type -> Type Methods from :: Prop -> Rep Prop x to :: Rep Prop x -> Prop
FromJSON Prop
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Prop parseJSONList :: Value -> Parser [Prop]
ToJSON Prop
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Prop -> Value toEncoding :: Prop -> Encoding toJSONList :: [Prop] -> Value toEncodingList :: [Prop] -> Encoding
ShATermConvertible Prop
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Prop -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Prop] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Prop) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Prop])
type Rep Prop
Instance details Defined in Isabelle.ATC_Isabelle type Rep Prop = D1 ('MetaData "Prop" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Prop" 'PrefixI 'True) (S1 ('MetaSel ('Just "prop") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "propPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])))

data Props Source #

Constructors

Props
Fields propsName :: Maybe QName propsArgs :: Maybe String props :: [Prop]

Instances

Instances details

Eq Props Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Props -> Props -> Bool (/=) :: Props -> Props -> Bool
Data Props Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Props -> c Props gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Props toConstr :: Props -> Constr dataTypeOf :: Props -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Props) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Props) gmapT :: (forall b. Data b => b -> b) -> Props -> Props gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Props -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Props -> r gmapQ :: (forall d. Data d => d -> u) -> Props -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Props -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Props -> m Props gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Props -> m Props gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Props -> m Props
Ord Props Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Props -> Props -> Ordering (<) :: Props -> Props -> Bool (<=) :: Props -> Props -> Bool (>) :: Props -> Props -> Bool (>=) :: Props -> Props -> Bool max :: Props -> Props -> Props min :: Props -> Props -> Props
Show Props Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Props -> ShowS show :: Props -> String showList :: [Props] -> ShowS
Generic Props
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Props :: Type -> Type Methods from :: Props -> Rep Props x to :: Rep Props x -> Props
FromJSON Props
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Props parseJSONList :: Value -> Parser [Props]
ToJSON Props
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Props -> Value toEncoding :: Props -> Encoding toJSONList :: [Props] -> Value toEncodingList :: [Props] -> Encoding
ShATermConvertible Props
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Props -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Props] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Props) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Props])
type Rep Props
Instance details Defined in Isabelle.ATC_Isabelle type Rep Props = D1 ('MetaData "Props" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Props" 'PrefixI 'True) (S1 ('MetaSel ('Just "propsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: (S1 ('MetaSel ('Just "propsArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :: S1 ('MetaSel ('Just "props") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]))))

data Sentence Source #

Constructors

Sentence
Fields isSimp :: Bool isRefuteAux :: Bool metaTerm :: MetaTerm thmProof :: Maybe IsaProof
Instance
Fields tName :: TName arityArgs :: [Sort] arityRes :: Sort definitions :: [(String, Term)] Definitons for the instansiation with the name of the sentence (String) instProof :: IsaProof
ConstDef
Fields senTerm :: Term
RecDef
Fields keyword :: Maybe String constName :: VName constType :: Maybe Typ primRecSenTerms :: [Term]
TypeDef
Fields newType :: Typ typeDef :: SetDecl nonEmptyPr :: IsaProof
Lemmas	Isabelle syntax for grouping multiple lemmas in to a single lemma.
Fields lemmaName :: String lemmasList :: [String]
Locale
Fields localeName :: QName localeContext :: Ctxt localeParents :: [QName] localeBody :: [Sentence]
Class
Fields className :: QName classContext :: Ctxt classParents :: [QName] classBody :: [Sentence]
Datatypes [Datatype]
Domains [Domain]
Consts [(String, Maybe Mixfix, Typ)]
TypeSynonym QName (Maybe Mixfix) [String] Typ
Axioms [Axiom]
Lemma
Fields lemmaTarget :: Maybe QName lemmaContext :: Ctxt lemmaProof :: Maybe String lemmaProps :: [Props]
Definition
Fields definitionName :: QName definitionMixfix :: Maybe Mixfix definitionTarget :: Maybe String definitionType :: Typ definitionVars :: [Term] definitionTerm :: Term
Fun
Fields funTarget :: Maybe QName funSequential :: Bool funDefault :: Maybe String funDomintros :: Bool funPartials :: Bool funEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
Primrec
Fields primrecTarget :: Maybe QName primrecEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
Fixrec [(String, Maybe Mixfix, Typ, [FixrecEquation])]
Instantiation
Fields instantiationType :: TName instantiationArity :: (Sort, [Sort]) instantiationBody :: [Sentence]
InstanceProof
Fields instanceProof :: String
InstanceArity
Fields instanceTypes :: [TName] instanceArity :: (Sort, [Sort]) instanceProof :: String
InstanceSubclass
Fields instanceClass :: String instanceRel :: String instanceClass1 :: String instanceProof :: String
Subclass
Fields subclassClass :: String subclassTarget :: Maybe QName subclassProof :: String
Typedef
Fields typedefName :: QName typedefVars :: [(String, Sort)] typedefMixfix :: Maybe Mixfix typedefMorphisms :: Maybe (QName, QName) typedefTerm :: Term typedefProof :: String
Defs
Fields defsUnchecked :: Bool defsOverloaded :: Bool defsEquations :: [DefEquation]

Instances

Instances details

Eq Sentence Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Sentence -> Sentence -> Bool (/=) :: Sentence -> Sentence -> Bool
Data Sentence Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sentence -> c Sentence gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sentence toConstr :: Sentence -> Constr dataTypeOf :: Sentence -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sentence) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence) gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence
Ord Sentence Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Sentence -> Sentence -> Ordering (<) :: Sentence -> Sentence -> Bool (<=) :: Sentence -> Sentence -> Bool (>) :: Sentence -> Sentence -> Bool (>=) :: Sentence -> Sentence -> Bool max :: Sentence -> Sentence -> Sentence min :: Sentence -> Sentence -> Sentence
Show Sentence Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Sentence -> ShowS show :: Sentence -> String showList :: [Sentence] -> ShowS
Generic Sentence
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Sentence :: Type -> Type Methods from :: Sentence -> Rep Sentence x to :: Rep Sentence x -> Sentence
GetRange Sentence Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods getRange :: Sentence -> Range Source # rangeSpan :: Sentence -> [Pos] Source #
FromJSON Sentence
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Sentence parseJSONList :: Value -> Parser [Sentence]
ToJSON Sentence
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Sentence -> Value toEncoding :: Sentence -> Encoding toJSONList :: [Sentence] -> Value toEncodingList :: [Sentence] -> Encoding
ShATermConvertible Sentence
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])
Pretty Sentence Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: Sentence -> Doc Source # pretties :: [Sentence] -> Doc Source #
Sentences Isabelle Sentence Sign IsabelleMorphism () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods map_sen :: Isabelle -> IsabelleMorphism -> Sentence -> Result Sentence Source # simplify_sen :: Isabelle -> Sign -> Sentence -> Sentence Source # negation :: Isabelle -> Sentence -> Maybe Sentence Source # print_sign :: Isabelle -> Sign -> Doc Source # print_named :: Isabelle -> Named Sentence -> Doc Source # sym_of :: Isabelle -> Sign -> [Set ()] Source # mostSymsOf :: Isabelle -> Sign -> [()] Source # symmap_of :: Isabelle -> IsabelleMorphism -> EndoMap () Source # sym_name :: Isabelle -> () -> Id Source # sym_label :: Isabelle -> () -> Maybe String Source # fullSymName :: Isabelle -> () -> String Source # symKind :: Isabelle -> () -> String Source # symsOfSen :: Isabelle -> Sign -> Sentence -> [()] Source # pair_symbols :: Isabelle -> () -> () -> Result () Source #
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source # convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source # qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source # symbol_to_raw :: Isabelle -> () -> () Source # id_to_raw :: Isabelle -> Id -> () Source # matches :: Isabelle -> () -> () -> Bool Source # empty_signature :: Isabelle -> Sign Source # add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source # signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source # signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source # intersection :: Isabelle -> Sign -> Sign -> Result Sign Source # final_union :: Isabelle -> Sign -> Sign -> Result Sign Source # morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source # is_subsig :: Isabelle -> Sign -> Sign -> Bool Source # subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source # generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source # induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source # is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source # is_injective :: Isabelle -> IsabelleMorphism -> Bool Source # theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods base_sig :: Isabelle -> Sign Source # write_logic :: Isabelle -> String -> String Source # write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source # write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source # write_model :: Isabelle -> String -> IsabelleMorphism -> String Source # read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source # write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #
Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source # stability :: Isabelle -> Stability Source # data_logic :: Isabelle -> Maybe AnyLogic Source # top_sublogic :: Isabelle -> () Source # all_sublogics :: Isabelle -> [()] Source # bottomSublogic :: Isabelle -> Maybe () Source # sublogicDimensions :: Isabelle -> [[()]] Source # parseSublogic :: Isabelle -> String -> Maybe () Source # proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source # provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source # default_prover :: Isabelle -> String Source # cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source # conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source # empty_proof_tree :: Isabelle -> () Source # syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: Isabelle -> Maybe OMCD Source # export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: Isabelle -> (Sign, [Sentence]) -> () Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle Methods sourceLogic :: HolLight2Isabelle -> HolLight Source # sourceSublogic :: HolLight2Isabelle -> HolLightSL Source # sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source # minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source # targetLogic :: HolLight2Isabelle -> Isabelle Source # mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source # map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source # map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source # map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source # extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source # is_model_transportable :: HolLight2Isabelle -> Bool Source # has_model_expansion :: HolLight2Isabelle -> Bool Source # is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source # constituents :: HolLight2Isabelle -> [String] Source # isInclusionComorphism :: HolLight2Isabelle -> Bool Source # rps :: HolLight2Isabelle -> Bool Source # eps :: HolLight2Isabelle -> Bool Source # isGTC :: HolLight2Isabelle -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source # sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # minSourceTheory :: CommonLogic2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source # mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source # map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source # map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source # extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source # is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source # has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source # constituents :: CommonLogic2IsabelleHOL -> [String] Source # isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source # rps :: CommonLogic2IsabelleHOL -> Bool Source # eps :: CommonLogic2IsabelleHOL -> Bool Source # isGTC :: CommonLogic2IsabelleHOL -> Bool Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
type Rep Sentence
Instance details Defined in Isabelle.ATC_Isabelle type Rep Sentence = D1 ('MetaData "Sentence" "Isabelle.IsaSign" "main" 'False) ((((C1 ('MetaCons "Sentence" 'PrefixI 'True) ((S1 ('MetaSel ('Just "isSimp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "isRefuteAux") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "metaTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaTerm) :: S1 ('MetaSel ('Just "thmProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe IsaProof)))) :+: (C1 ('MetaCons "Instance" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TName) :: S1 ('MetaSel ('Just "arityArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Sort])) :: (S1 ('MetaSel ('Just "arityRes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: (S1 ('MetaSel ('Just "definitions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Term)]) :: S1 ('MetaSel ('Just "instProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsaProof)))) :+: C1 ('MetaCons "ConstDef" 'PrefixI 'True) (S1 ('MetaSel ('Just "senTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: (C1 ('MetaCons "RecDef" 'PrefixI 'True) ((S1 ('MetaSel ('Just "keyword") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :: S1 ('MetaSel ('Just "constName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VName)) :: (S1 ('MetaSel ('Just "constType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Typ)) :: S1 ('MetaSel ('Just "primRecSenTerms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]))) :+: (C1 ('MetaCons "TypeDef" 'PrefixI 'True) (S1 ('MetaSel ('Just "newType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: (S1 ('MetaSel ('Just "typeDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SetDecl) :: S1 ('MetaSel ('Just "nonEmptyPr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsaProof))) :+: C1 ('MetaCons "Lemmas" 'PrefixI 'True) (S1 ('MetaSel ('Just "lemmaName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "lemmasList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))))) :+: ((C1 ('MetaCons "Locale" 'PrefixI 'True) ((S1 ('MetaSel ('Just "localeName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "localeContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ctxt)) :: (S1 ('MetaSel ('Just "localeParents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :: S1 ('MetaSel ('Just "localeBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Sentence]))) :+: (C1 ('MetaCons "Class" 'PrefixI 'True) ((S1 ('MetaSel ('Just "className") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "classContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ctxt)) :: (S1 ('MetaSel ('Just "classParents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :: S1 ('MetaSel ('Just "classBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Sentence]))) :+: C1 ('MetaCons "Datatypes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Datatype])))) :+: (C1 ('MetaCons "Domains" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Domain])) :+: (C1 ('MetaCons "Consts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Maybe Mixfix, Typ)])) :+: C1 ('MetaCons "TypeSynonym" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ))))))) :+: (((C1 ('MetaCons "Axioms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Axiom])) :+: (C1 ('MetaCons "Lemma" 'PrefixI 'True) ((S1 ('MetaSel ('Just "lemmaTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: S1 ('MetaSel ('Just "lemmaContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ctxt)) :: (S1 ('MetaSel ('Just "lemmaProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :: S1 ('MetaSel ('Just "lemmaProps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Props]))) :+: C1 ('MetaCons "Definition" 'PrefixI 'True) ((S1 ('MetaSel ('Just "definitionName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Just "definitionMixfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix)) :: S1 ('MetaSel ('Just "definitionTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :: (S1 ('MetaSel ('Just "definitionType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: (S1 ('MetaSel ('Just "definitionVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Just "definitionTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))))) :+: (C1 ('MetaCons "Fun" 'PrefixI 'True) ((S1 ('MetaSel ('Just "funTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: (S1 ('MetaSel ('Just "funSequential") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "funDefault") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :: (S1 ('MetaSel ('Just "funDomintros") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "funPartials") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "funEquations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Maybe Mixfix, Typ, [([Term], Term)])])))) :+: (C1 ('MetaCons "Primrec" 'PrefixI 'True) (S1 ('MetaSel ('Just "primrecTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: S1 ('MetaSel ('Just "primrecEquations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Maybe Mixfix, Typ, [([Term], Term)])])) :+: C1 ('MetaCons "Fixrec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Maybe Mixfix, Typ, [FixrecEquation])]))))) :+: ((C1 ('MetaCons "Instantiation" 'PrefixI 'True) (S1 ('MetaSel ('Just "instantiationType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TName) :: (S1 ('MetaSel ('Just "instantiationArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Sort, [Sort])) :: S1 ('MetaSel ('Just "instantiationBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Sentence]))) :+: (C1 ('MetaCons "InstanceProof" 'PrefixI 'True) (S1 ('MetaSel ('Just "instanceProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "InstanceArity" 'PrefixI 'True) (S1 ('MetaSel ('Just "instanceTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TName]) :: (S1 ('MetaSel ('Just "instanceArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Sort, [Sort])) :: S1 ('MetaSel ('Just "instanceProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))) :+: ((C1 ('MetaCons "InstanceSubclass" 'PrefixI 'True) ((S1 ('MetaSel ('Just "instanceClass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "instanceRel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :: (S1 ('MetaSel ('Just "instanceClass1") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "instanceProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: C1 ('MetaCons "Subclass" 'PrefixI 'True) (S1 ('MetaSel ('Just "subclassClass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: (S1 ('MetaSel ('Just "subclassTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: S1 ('MetaSel ('Just "subclassProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "Typedef" 'PrefixI 'True) ((S1 ('MetaSel ('Just "typedefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Just "typedefVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Sort)]) :: S1 ('MetaSel ('Just "typedefMixfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix)))) :: (S1 ('MetaSel ('Just "typedefMorphisms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (QName, QName))) :: (S1 ('MetaSel ('Just "typedefTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "typedefProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: C1 ('MetaCons "Defs" 'PrefixI 'True) (S1 ('MetaSel ('Just "defsUnchecked") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "defsOverloaded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "defsEquations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefEquation]))))))))

data DefEquation Source #

Constructors

DefEquation
Fields defEquationName :: QName defEquationConst :: String defEquationConstType :: Typ defEquationTerm :: Term defEquationArgs :: String

Instances

Instances details

Eq DefEquation Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: DefEquation -> DefEquation -> Bool (/=) :: DefEquation -> DefEquation -> Bool
Data DefEquation Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefEquation -> c DefEquation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefEquation toConstr :: DefEquation -> Constr dataTypeOf :: DefEquation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefEquation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefEquation) gmapT :: (forall b. Data b => b -> b) -> DefEquation -> DefEquation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefEquation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefEquation -> r gmapQ :: (forall d. Data d => d -> u) -> DefEquation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefEquation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation
Ord DefEquation Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: DefEquation -> DefEquation -> Ordering (<) :: DefEquation -> DefEquation -> Bool (<=) :: DefEquation -> DefEquation -> Bool (>) :: DefEquation -> DefEquation -> Bool (>=) :: DefEquation -> DefEquation -> Bool max :: DefEquation -> DefEquation -> DefEquation min :: DefEquation -> DefEquation -> DefEquation
Show DefEquation Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> DefEquation -> ShowS show :: DefEquation -> String showList :: [DefEquation] -> ShowS
Generic DefEquation
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep DefEquation :: Type -> Type Methods from :: DefEquation -> Rep DefEquation x to :: Rep DefEquation x -> DefEquation
FromJSON DefEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser DefEquation parseJSONList :: Value -> Parser [DefEquation]
ToJSON DefEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: DefEquation -> Value toEncoding :: DefEquation -> Encoding toJSONList :: [DefEquation] -> Value toEncodingList :: [DefEquation] -> Encoding
ShATermConvertible DefEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> DefEquation -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefEquation] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefEquation) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefEquation])
type Rep DefEquation
Instance details Defined in Isabelle.ATC_Isabelle type Rep DefEquation = D1 ('MetaData "DefEquation" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "DefEquation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defEquationName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "defEquationConst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :: (S1 ('MetaSel ('Just "defEquationConstType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: (S1 ('MetaSel ('Just "defEquationTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "defEquationArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))

data FixrecEquation Source #

Constructors

FixrecEquation
Fields fixrecEquationUnchecked :: Bool fixrecEquationPremises :: [Term] fixrecEquationPatterns :: [Term] fixrecEquationTerm :: Term

Instances

Instances details

Eq FixrecEquation Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: FixrecEquation -> FixrecEquation -> Bool (/=) :: FixrecEquation -> FixrecEquation -> Bool
Data FixrecEquation Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixrecEquation -> c FixrecEquation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixrecEquation toConstr :: FixrecEquation -> Constr dataTypeOf :: FixrecEquation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixrecEquation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixrecEquation) gmapT :: (forall b. Data b => b -> b) -> FixrecEquation -> FixrecEquation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixrecEquation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixrecEquation -> r gmapQ :: (forall d. Data d => d -> u) -> FixrecEquation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FixrecEquation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation
Ord FixrecEquation Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: FixrecEquation -> FixrecEquation -> Ordering (<) :: FixrecEquation -> FixrecEquation -> Bool (<=) :: FixrecEquation -> FixrecEquation -> Bool (>) :: FixrecEquation -> FixrecEquation -> Bool (>=) :: FixrecEquation -> FixrecEquation -> Bool max :: FixrecEquation -> FixrecEquation -> FixrecEquation min :: FixrecEquation -> FixrecEquation -> FixrecEquation
Show FixrecEquation Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> FixrecEquation -> ShowS show :: FixrecEquation -> String showList :: [FixrecEquation] -> ShowS
Generic FixrecEquation
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep FixrecEquation :: Type -> Type Methods from :: FixrecEquation -> Rep FixrecEquation x to :: Rep FixrecEquation x -> FixrecEquation
FromJSON FixrecEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser FixrecEquation parseJSONList :: Value -> Parser [FixrecEquation]
ToJSON FixrecEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: FixrecEquation -> Value toEncoding :: FixrecEquation -> Encoding toJSONList :: [FixrecEquation] -> Value toEncodingList :: [FixrecEquation] -> Encoding
ShATermConvertible FixrecEquation
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> FixrecEquation -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FixrecEquation] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FixrecEquation) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FixrecEquation])
type Rep FixrecEquation
Instance details Defined in Isabelle.ATC_Isabelle type Rep FixrecEquation = D1 ('MetaData "FixrecEquation" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "FixrecEquation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "fixrecEquationUnchecked") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "fixrecEquationPremises") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])) :: (S1 ('MetaSel ('Just "fixrecEquationPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :*: S1 ('MetaSel ('Just "fixrecEquationTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))

data Ctxt Source #

Constructors

Ctxt
Fields fixes :: [(String, Maybe Mixfix, Typ)] assumes :: [(String, Term)]

Instances

Instances details

Eq Ctxt Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Ctxt -> Ctxt -> Bool (/=) :: Ctxt -> Ctxt -> Bool
Data Ctxt Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ctxt -> c Ctxt gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ctxt toConstr :: Ctxt -> Constr dataTypeOf :: Ctxt -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Ctxt) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctxt) gmapT :: (forall b. Data b => b -> b) -> Ctxt -> Ctxt gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctxt -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctxt -> r gmapQ :: (forall d. Data d => d -> u) -> Ctxt -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Ctxt -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt
Ord Ctxt Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Ctxt -> Ctxt -> Ordering (<) :: Ctxt -> Ctxt -> Bool (<=) :: Ctxt -> Ctxt -> Bool (>) :: Ctxt -> Ctxt -> Bool (>=) :: Ctxt -> Ctxt -> Bool max :: Ctxt -> Ctxt -> Ctxt min :: Ctxt -> Ctxt -> Ctxt
Show Ctxt Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Ctxt -> ShowS show :: Ctxt -> String showList :: [Ctxt] -> ShowS
Generic Ctxt
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Ctxt :: Type -> Type Methods from :: Ctxt -> Rep Ctxt x to :: Rep Ctxt x -> Ctxt
FromJSON Ctxt
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Ctxt parseJSONList :: Value -> Parser [Ctxt]
ToJSON Ctxt
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Ctxt -> Value toEncoding :: Ctxt -> Encoding toJSONList :: [Ctxt] -> Value toEncodingList :: [Ctxt] -> Encoding
ShATermConvertible Ctxt
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Ctxt -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Ctxt] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Ctxt) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Ctxt])
type Rep Ctxt
Instance details Defined in Isabelle.ATC_Isabelle type Rep Ctxt = D1 ('MetaData "Ctxt" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Ctxt" 'PrefixI 'True) (S1 ('MetaSel ('Just "fixes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Maybe Mixfix, Typ)]) :*: S1 ('MetaSel ('Just "assumes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Term)])))

data Mixfix Source #

Constructors

Mixfix
Fields mixfixNargs :: Int mixfixPrio :: Int mixfixPretty :: String mixfixTemplate :: [MixfixTemplate]

Instances

Instances details

Eq Mixfix Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Mixfix -> Mixfix -> Bool (/=) :: Mixfix -> Mixfix -> Bool
Data Mixfix Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Mixfix -> c Mixfix gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Mixfix toConstr :: Mixfix -> Constr dataTypeOf :: Mixfix -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Mixfix) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Mixfix) gmapT :: (forall b. Data b => b -> b) -> Mixfix -> Mixfix gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Mixfix -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Mixfix -> r gmapQ :: (forall d. Data d => d -> u) -> Mixfix -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Mixfix -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix
Ord Mixfix Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Mixfix -> Mixfix -> Ordering (<) :: Mixfix -> Mixfix -> Bool (<=) :: Mixfix -> Mixfix -> Bool (>) :: Mixfix -> Mixfix -> Bool (>=) :: Mixfix -> Mixfix -> Bool max :: Mixfix -> Mixfix -> Mixfix min :: Mixfix -> Mixfix -> Mixfix
Show Mixfix Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Mixfix -> ShowS show :: Mixfix -> String showList :: [Mixfix] -> ShowS
Generic Mixfix
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Mixfix :: Type -> Type Methods from :: Mixfix -> Rep Mixfix x to :: Rep Mixfix x -> Mixfix
FromJSON Mixfix
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Mixfix parseJSONList :: Value -> Parser [Mixfix]
ToJSON Mixfix
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Mixfix -> Value toEncoding :: Mixfix -> Encoding toJSONList :: [Mixfix] -> Value toEncodingList :: [Mixfix] -> Encoding
ShATermConvertible Mixfix
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Mixfix -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Mixfix] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Mixfix) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Mixfix])
type Rep Mixfix
Instance details Defined in Isabelle.ATC_Isabelle type Rep Mixfix = D1 ('MetaData "Mixfix" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Mixfix" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mixfixNargs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "mixfixPrio") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "mixfixPretty") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "mixfixTemplate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [MixfixTemplate]))))

data MixfixTemplate Source #

Constructors

Arg Int
Str String
Break Int
Block Int [MixfixTemplate]

Instances

Instances details

Eq MixfixTemplate Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: MixfixTemplate -> MixfixTemplate -> Bool (/=) :: MixfixTemplate -> MixfixTemplate -> Bool
Data MixfixTemplate Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MixfixTemplate -> c MixfixTemplate gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MixfixTemplate toConstr :: MixfixTemplate -> Constr dataTypeOf :: MixfixTemplate -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MixfixTemplate) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MixfixTemplate) gmapT :: (forall b. Data b => b -> b) -> MixfixTemplate -> MixfixTemplate gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MixfixTemplate -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MixfixTemplate -> r gmapQ :: (forall d. Data d => d -> u) -> MixfixTemplate -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MixfixTemplate -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate
Ord MixfixTemplate Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: MixfixTemplate -> MixfixTemplate -> Ordering (<) :: MixfixTemplate -> MixfixTemplate -> Bool (<=) :: MixfixTemplate -> MixfixTemplate -> Bool (>) :: MixfixTemplate -> MixfixTemplate -> Bool (>=) :: MixfixTemplate -> MixfixTemplate -> Bool max :: MixfixTemplate -> MixfixTemplate -> MixfixTemplate min :: MixfixTemplate -> MixfixTemplate -> MixfixTemplate
Show MixfixTemplate Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> MixfixTemplate -> ShowS show :: MixfixTemplate -> String showList :: [MixfixTemplate] -> ShowS
Generic MixfixTemplate
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep MixfixTemplate :: Type -> Type Methods from :: MixfixTemplate -> Rep MixfixTemplate x to :: Rep MixfixTemplate x -> MixfixTemplate
FromJSON MixfixTemplate
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser MixfixTemplate parseJSONList :: Value -> Parser [MixfixTemplate]
ToJSON MixfixTemplate
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: MixfixTemplate -> Value toEncoding :: MixfixTemplate -> Encoding toJSONList :: [MixfixTemplate] -> Value toEncodingList :: [MixfixTemplate] -> Encoding
ShATermConvertible MixfixTemplate
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> MixfixTemplate -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [MixfixTemplate] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, MixfixTemplate) fromShATermList' :: Int -> ATermTable -> (ATermTable, [MixfixTemplate])
type Rep MixfixTemplate
Instance details Defined in Isabelle.ATC_Isabelle type Rep MixfixTemplate = D1 ('MetaData "MixfixTemplate" "Isabelle.IsaSign" "main" 'False) ((C1 ('MetaCons "Arg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Str" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "Break" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [MixfixTemplate]))))

data Datatype Source #

Constructors

Datatype
Fields datatypeName :: QName datatypeTVars :: [Typ] datatypeMixfix :: Maybe Mixfix datatypeConstructors :: [DatatypeConstructor]

Instances

Instances details

Eq Datatype Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Datatype -> Datatype -> Bool (/=) :: Datatype -> Datatype -> Bool
Data Datatype Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Datatype -> c Datatype gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Datatype toConstr :: Datatype -> Constr dataTypeOf :: Datatype -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Datatype) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Datatype) gmapT :: (forall b. Data b => b -> b) -> Datatype -> Datatype gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Datatype -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Datatype -> r gmapQ :: (forall d. Data d => d -> u) -> Datatype -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Datatype -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype
Ord Datatype Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Datatype -> Datatype -> Ordering (<) :: Datatype -> Datatype -> Bool (<=) :: Datatype -> Datatype -> Bool (>) :: Datatype -> Datatype -> Bool (>=) :: Datatype -> Datatype -> Bool max :: Datatype -> Datatype -> Datatype min :: Datatype -> Datatype -> Datatype
Show Datatype Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Datatype -> ShowS show :: Datatype -> String showList :: [Datatype] -> ShowS
Generic Datatype
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Datatype :: Type -> Type Methods from :: Datatype -> Rep Datatype x to :: Rep Datatype x -> Datatype
FromJSON Datatype
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Datatype parseJSONList :: Value -> Parser [Datatype]
ToJSON Datatype
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Datatype -> Value toEncoding :: Datatype -> Encoding toJSONList :: [Datatype] -> Value toEncodingList :: [Datatype] -> Encoding
ShATermConvertible Datatype
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Datatype -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Datatype] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Datatype) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Datatype])
type Rep Datatype
Instance details Defined in Isabelle.ATC_Isabelle type Rep Datatype = D1 ('MetaData "Datatype" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Datatype" 'PrefixI 'True) ((S1 ('MetaSel ('Just "datatypeName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "datatypeTVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Typ])) :: (S1 ('MetaSel ('Just "datatypeMixfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix)) :*: S1 ('MetaSel ('Just "datatypeConstructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DatatypeConstructor]))))

data DatatypeConstructor Source #

Constructors

DatatypeConstructor
Fields constructorName :: QName constructorType :: Typ constructorMixfix :: Maybe Mixfix constructorArgs :: [Typ]
DatatypeNoConstructor
Fields constructorArgs :: [Typ]

Instances

Instances details

Eq DatatypeConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: DatatypeConstructor -> DatatypeConstructor -> Bool (/=) :: DatatypeConstructor -> DatatypeConstructor -> Bool
Data DatatypeConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DatatypeConstructor -> c DatatypeConstructor gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DatatypeConstructor toConstr :: DatatypeConstructor -> Constr dataTypeOf :: DatatypeConstructor -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DatatypeConstructor) gmapT :: (forall b. Data b => b -> b) -> DatatypeConstructor -> DatatypeConstructor gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r gmapQ :: (forall d. Data d => d -> u) -> DatatypeConstructor -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor
Ord DatatypeConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: DatatypeConstructor -> DatatypeConstructor -> Ordering (<) :: DatatypeConstructor -> DatatypeConstructor -> Bool (<=) :: DatatypeConstructor -> DatatypeConstructor -> Bool (>) :: DatatypeConstructor -> DatatypeConstructor -> Bool (>=) :: DatatypeConstructor -> DatatypeConstructor -> Bool max :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor min :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
Show DatatypeConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> DatatypeConstructor -> ShowS show :: DatatypeConstructor -> String showList :: [DatatypeConstructor] -> ShowS
Generic DatatypeConstructor
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep DatatypeConstructor :: Type -> Type Methods from :: DatatypeConstructor -> Rep DatatypeConstructor x to :: Rep DatatypeConstructor x -> DatatypeConstructor
FromJSON DatatypeConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser DatatypeConstructor parseJSONList :: Value -> Parser [DatatypeConstructor]
ToJSON DatatypeConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: DatatypeConstructor -> Value toEncoding :: DatatypeConstructor -> Encoding toJSONList :: [DatatypeConstructor] -> Value toEncodingList :: [DatatypeConstructor] -> Encoding
ShATermConvertible DatatypeConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> DatatypeConstructor -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DatatypeConstructor] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DatatypeConstructor) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DatatypeConstructor])
type Rep DatatypeConstructor
Instance details Defined in Isabelle.ATC_Isabelle type Rep DatatypeConstructor = D1 ('MetaData "DatatypeConstructor" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "DatatypeConstructor" 'PrefixI 'True) ((S1 ('MetaSel ('Just "constructorName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "constructorType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ)) :: (S1 ('MetaSel ('Just "constructorMixfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix)) :*: S1 ('MetaSel ('Just "constructorArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Typ]))) :+: C1 ('MetaCons "DatatypeNoConstructor" 'PrefixI 'True) (S1 ('MetaSel ('Just "constructorArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Typ])))

data Domain Source #

Constructors

Domain
Fields domainName :: QName domainTVars :: [Typ] domainMixfix :: Maybe Mixfix domainConstructors :: [DomainConstructor]

Instances

Instances details

Eq Domain Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Domain -> Domain -> Bool (/=) :: Domain -> Domain -> Bool
Data Domain Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Domain -> c Domain gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Domain toConstr :: Domain -> Constr dataTypeOf :: Domain -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Domain) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Domain) gmapT :: (forall b. Data b => b -> b) -> Domain -> Domain gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Domain -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Domain -> r gmapQ :: (forall d. Data d => d -> u) -> Domain -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Domain -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Domain -> m Domain gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Domain -> m Domain gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Domain -> m Domain
Ord Domain Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Domain -> Domain -> Ordering (<) :: Domain -> Domain -> Bool (<=) :: Domain -> Domain -> Bool (>) :: Domain -> Domain -> Bool (>=) :: Domain -> Domain -> Bool max :: Domain -> Domain -> Domain min :: Domain -> Domain -> Domain
Show Domain Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Domain -> ShowS show :: Domain -> String showList :: [Domain] -> ShowS
Generic Domain
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Domain :: Type -> Type Methods from :: Domain -> Rep Domain x to :: Rep Domain x -> Domain
FromJSON Domain
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Domain parseJSONList :: Value -> Parser [Domain]
ToJSON Domain
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Domain -> Value toEncoding :: Domain -> Encoding toJSONList :: [Domain] -> Value toEncodingList :: [Domain] -> Encoding
ShATermConvertible Domain
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Domain -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Domain] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Domain) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Domain])
type Rep Domain
Instance details Defined in Isabelle.ATC_Isabelle type Rep Domain = D1 ('MetaData "Domain" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Domain" 'PrefixI 'True) ((S1 ('MetaSel ('Just "domainName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "domainTVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Typ])) :: (S1 ('MetaSel ('Just "domainMixfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Mixfix)) :*: S1 ('MetaSel ('Just "domainConstructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DomainConstructor]))))

data DomainConstructor Source #

Constructors

DomainConstructor
Fields domainConstructorName :: QName domainConstructorType :: Typ domainConstructorArgs :: [DomainConstructorArg]

Instances

Instances details

Eq DomainConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: DomainConstructor -> DomainConstructor -> Bool (/=) :: DomainConstructor -> DomainConstructor -> Bool
Data DomainConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DomainConstructor -> c DomainConstructor gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DomainConstructor toConstr :: DomainConstructor -> Constr dataTypeOf :: DomainConstructor -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DomainConstructor) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DomainConstructor) gmapT :: (forall b. Data b => b -> b) -> DomainConstructor -> DomainConstructor gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructor -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructor -> r gmapQ :: (forall d. Data d => d -> u) -> DomainConstructor -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DomainConstructor -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor
Ord DomainConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: DomainConstructor -> DomainConstructor -> Ordering (<) :: DomainConstructor -> DomainConstructor -> Bool (<=) :: DomainConstructor -> DomainConstructor -> Bool (>) :: DomainConstructor -> DomainConstructor -> Bool (>=) :: DomainConstructor -> DomainConstructor -> Bool max :: DomainConstructor -> DomainConstructor -> DomainConstructor min :: DomainConstructor -> DomainConstructor -> DomainConstructor
Show DomainConstructor Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> DomainConstructor -> ShowS show :: DomainConstructor -> String showList :: [DomainConstructor] -> ShowS
Generic DomainConstructor
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep DomainConstructor :: Type -> Type Methods from :: DomainConstructor -> Rep DomainConstructor x to :: Rep DomainConstructor x -> DomainConstructor
FromJSON DomainConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser DomainConstructor parseJSONList :: Value -> Parser [DomainConstructor]
ToJSON DomainConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: DomainConstructor -> Value toEncoding :: DomainConstructor -> Encoding toJSONList :: [DomainConstructor] -> Value toEncodingList :: [DomainConstructor] -> Encoding
ShATermConvertible DomainConstructor
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> DomainConstructor -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DomainConstructor] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DomainConstructor) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DomainConstructor])
type Rep DomainConstructor
Instance details Defined in Isabelle.ATC_Isabelle type Rep DomainConstructor = D1 ('MetaData "DomainConstructor" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "DomainConstructor" 'PrefixI 'True) (S1 ('MetaSel ('Just "domainConstructorName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Just "domainConstructorType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: S1 ('MetaSel ('Just "domainConstructorArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DomainConstructorArg]))))

data DomainConstructorArg Source #

Constructors

DomainConstructorArg
Fields domainConstructorArgSel :: Maybe QName domainConstructorArgType :: Typ domainConstructorArgLazy :: Bool

Instances

Instances details

Eq DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: DomainConstructorArg -> DomainConstructorArg -> Bool (/=) :: DomainConstructorArg -> DomainConstructorArg -> Bool
Data DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DomainConstructorArg -> c DomainConstructorArg gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DomainConstructorArg toConstr :: DomainConstructorArg -> Constr dataTypeOf :: DomainConstructorArg -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DomainConstructorArg) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DomainConstructorArg) gmapT :: (forall b. Data b => b -> b) -> DomainConstructorArg -> DomainConstructorArg gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructorArg -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructorArg -> r gmapQ :: (forall d. Data d => d -> u) -> DomainConstructorArg -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DomainConstructorArg -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg
Ord DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: DomainConstructorArg -> DomainConstructorArg -> Ordering (<) :: DomainConstructorArg -> DomainConstructorArg -> Bool (<=) :: DomainConstructorArg -> DomainConstructorArg -> Bool (>) :: DomainConstructorArg -> DomainConstructorArg -> Bool (>=) :: DomainConstructorArg -> DomainConstructorArg -> Bool max :: DomainConstructorArg -> DomainConstructorArg -> DomainConstructorArg min :: DomainConstructorArg -> DomainConstructorArg -> DomainConstructorArg
Show DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> DomainConstructorArg -> ShowS show :: DomainConstructorArg -> String showList :: [DomainConstructorArg] -> ShowS
Generic DomainConstructorArg
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep DomainConstructorArg :: Type -> Type Methods from :: DomainConstructorArg -> Rep DomainConstructorArg x to :: Rep DomainConstructorArg x -> DomainConstructorArg
FromJSON DomainConstructorArg
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser DomainConstructorArg parseJSONList :: Value -> Parser [DomainConstructorArg]
ToJSON DomainConstructorArg
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: DomainConstructorArg -> Value toEncoding :: DomainConstructorArg -> Encoding toJSONList :: [DomainConstructorArg] -> Value toEncodingList :: [DomainConstructorArg] -> Encoding
ShATermConvertible DomainConstructorArg
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> DomainConstructorArg -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DomainConstructorArg] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DomainConstructorArg) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DomainConstructorArg])
type Rep DomainConstructorArg
Instance details Defined in Isabelle.ATC_Isabelle type Rep DomainConstructorArg = D1 ('MetaData "DomainConstructorArg" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "DomainConstructorArg" 'PrefixI 'True) (S1 ('MetaSel ('Just "domainConstructorArgSel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :: (S1 ('MetaSel ('Just "domainConstructorArgType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: S1 ('MetaSel ('Just "domainConstructorArgLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data Axiom Source #

Constructors

Axiom
Fields axiomName :: QName axiomArgs :: String axiomTerm :: Term

Instances

Instances details

Eq Axiom Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Axiom -> Axiom -> Bool (/=) :: Axiom -> Axiom -> Bool
Data Axiom Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Axiom -> c Axiom gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Axiom toConstr :: Axiom -> Constr dataTypeOf :: Axiom -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Axiom) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Axiom) gmapT :: (forall b. Data b => b -> b) -> Axiom -> Axiom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r gmapQ :: (forall d. Data d => d -> u) -> Axiom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Axiom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom
Ord Axiom Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Axiom -> Axiom -> Ordering (<) :: Axiom -> Axiom -> Bool (<=) :: Axiom -> Axiom -> Bool (>) :: Axiom -> Axiom -> Bool (>=) :: Axiom -> Axiom -> Bool max :: Axiom -> Axiom -> Axiom min :: Axiom -> Axiom -> Axiom
Show Axiom Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Axiom -> ShowS show :: Axiom -> String showList :: [Axiom] -> ShowS
Generic Axiom
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Axiom :: Type -> Type Methods from :: Axiom -> Rep Axiom x to :: Rep Axiom x -> Axiom
FromJSON Axiom
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Axiom parseJSONList :: Value -> Parser [Axiom]
ToJSON Axiom
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Axiom -> Value toEncoding :: Axiom -> Encoding toJSONList :: [Axiom] -> Value toEncodingList :: [Axiom] -> Encoding
ShATermConvertible Axiom
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Axiom -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Axiom] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Axiom) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Axiom])
type Rep Axiom
Instance details Defined in Isabelle.ATC_Isabelle type Rep Axiom = D1 ('MetaData "Axiom" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Axiom" 'PrefixI 'True) (S1 ('MetaSel ('Just "axiomName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Just "axiomArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "axiomTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))

data FunSig Source #

Constructors

FunSig
Fields funSigName :: QName funSigType :: Maybe Typ

Instances

Instances details

Eq FunSig Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: FunSig -> FunSig -> Bool (/=) :: FunSig -> FunSig -> Bool
Data FunSig Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunSig -> c FunSig gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunSig toConstr :: FunSig -> Constr dataTypeOf :: FunSig -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunSig) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSig) gmapT :: (forall b. Data b => b -> b) -> FunSig -> FunSig gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSig -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSig -> r gmapQ :: (forall d. Data d => d -> u) -> FunSig -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FunSig -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig
Ord FunSig Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: FunSig -> FunSig -> Ordering (<) :: FunSig -> FunSig -> Bool (<=) :: FunSig -> FunSig -> Bool (>) :: FunSig -> FunSig -> Bool (>=) :: FunSig -> FunSig -> Bool max :: FunSig -> FunSig -> FunSig min :: FunSig -> FunSig -> FunSig
Show FunSig Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> FunSig -> ShowS show :: FunSig -> String showList :: [FunSig] -> ShowS
Generic FunSig
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep FunSig :: Type -> Type Methods from :: FunSig -> Rep FunSig x to :: Rep FunSig x -> FunSig
FromJSON FunSig
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser FunSig parseJSONList :: Value -> Parser [FunSig]
ToJSON FunSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: FunSig -> Value toEncoding :: FunSig -> Encoding toJSONList :: [FunSig] -> Value toEncodingList :: [FunSig] -> Encoding
ShATermConvertible FunSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> FunSig -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FunSig] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FunSig) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FunSig])
type Rep FunSig
Instance details Defined in Isabelle.ATC_Isabelle type Rep FunSig = D1 ('MetaData "FunSig" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "FunSig" 'PrefixI 'True) (S1 ('MetaSel ('Just "funSigName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "funSigType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Typ))))

data SetDecl Source #

Constructors

SubSet Term Typ Term	Create a set using a subset. First parameter is the variable Second is the type of the variable third is the formula describing the set comprehension e.g. x Nat "even x" would be produce the isabelle code: {x::Nat . even x}
FixedSet [Term]	A set declared using a list of terms. e.g. {1,2,3} would be Set [1,2,3]

Instances

Instances details

Eq SetDecl Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: SetDecl -> SetDecl -> Bool (/=) :: SetDecl -> SetDecl -> Bool
Data SetDecl Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SetDecl -> c SetDecl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SetDecl toConstr :: SetDecl -> Constr dataTypeOf :: SetDecl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SetDecl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SetDecl) gmapT :: (forall b. Data b => b -> b) -> SetDecl -> SetDecl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SetDecl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SetDecl -> r gmapQ :: (forall d. Data d => d -> u) -> SetDecl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SetDecl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl
Ord SetDecl Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: SetDecl -> SetDecl -> Ordering (<) :: SetDecl -> SetDecl -> Bool (<=) :: SetDecl -> SetDecl -> Bool (>) :: SetDecl -> SetDecl -> Bool (>=) :: SetDecl -> SetDecl -> Bool max :: SetDecl -> SetDecl -> SetDecl min :: SetDecl -> SetDecl -> SetDecl
Show SetDecl Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> SetDecl -> ShowS show :: SetDecl -> String showList :: [SetDecl] -> ShowS
Generic SetDecl
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep SetDecl :: Type -> Type Methods from :: SetDecl -> Rep SetDecl x to :: Rep SetDecl x -> SetDecl
FromJSON SetDecl
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser SetDecl parseJSONList :: Value -> Parser [SetDecl]
ToJSON SetDecl
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: SetDecl -> Value toEncoding :: SetDecl -> Encoding toJSONList :: [SetDecl] -> Value toEncodingList :: [SetDecl] -> Encoding
ShATermConvertible SetDecl
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> SetDecl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SetDecl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SetDecl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SetDecl])
type Rep SetDecl
Instance details Defined in Isabelle.ATC_Isabelle type Rep SetDecl = D1 ('MetaData "SetDecl" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "SubSet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Typ) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "FixedSet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])))

data MetaTerm Source #

Constructors

Term Term
Conditional [Term] Term

Instances

Instances details

Eq MetaTerm Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: MetaTerm -> MetaTerm -> Bool (/=) :: MetaTerm -> MetaTerm -> Bool
Data MetaTerm Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaTerm -> c MetaTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaTerm toConstr :: MetaTerm -> Constr dataTypeOf :: MetaTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaTerm) gmapT :: (forall b. Data b => b -> b) -> MetaTerm -> MetaTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaTerm -> r gmapQ :: (forall d. Data d => d -> u) -> MetaTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm
Ord MetaTerm Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: MetaTerm -> MetaTerm -> Ordering (<) :: MetaTerm -> MetaTerm -> Bool (<=) :: MetaTerm -> MetaTerm -> Bool (>) :: MetaTerm -> MetaTerm -> Bool (>=) :: MetaTerm -> MetaTerm -> Bool max :: MetaTerm -> MetaTerm -> MetaTerm min :: MetaTerm -> MetaTerm -> MetaTerm
Show MetaTerm Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> MetaTerm -> ShowS show :: MetaTerm -> String showList :: [MetaTerm] -> ShowS
Generic MetaTerm
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep MetaTerm :: Type -> Type Methods from :: MetaTerm -> Rep MetaTerm x to :: Rep MetaTerm x -> MetaTerm
FromJSON MetaTerm
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser MetaTerm parseJSONList :: Value -> Parser [MetaTerm]
ToJSON MetaTerm
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: MetaTerm -> Value toEncoding :: MetaTerm -> Encoding toJSONList :: [MetaTerm] -> Value toEncodingList :: [MetaTerm] -> Encoding
ShATermConvertible MetaTerm
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> MetaTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [MetaTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, MetaTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [MetaTerm])
type Rep MetaTerm
Instance details Defined in Isabelle.ATC_Isabelle type Rep MetaTerm = D1 ('MetaData "MetaTerm" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "Conditional" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))

mkSenAux :: Bool -> MetaTerm -> Sentence Source #

mkSen :: Term -> Sentence Source #

mkCond :: [Term] -> Term -> Sentence Source #

mkRefuteSen :: Term -> Sentence Source #

isRefute :: Sentence -> Bool Source #

type ClassDecl = ([IsaClass], [(String, Term)], [(String, Typ)]) Source #

type Classrel = Map IsaClass ClassDecl Source #

type LocaleDecl = ([String], [(String, Term)], [(String, Term)], [(String, Typ, Maybe AltSyntax)]) Source #

type Def = (Typ, [(String, Typ)], Term) Source #

type FunDef = (Typ, [([Term], Term)]) Source #

type Locales = Map String LocaleDecl Source #

type Defs = Map String Def Source #

type Funs = Map String FunDef Source #

type Arities = Map TName [(IsaClass, [(Typ, Sort)])] Source #

type Abbrs = Map TName ([TName], Typ) Source #

data TypeSig Source #

Constructors

TySg
Fields classrel :: Classrel locales :: Locales defs :: Defs funs :: Funs defaultSort :: Sort log_types :: [TName] univ_witness :: Maybe (Typ, Sort) abbrs :: Abbrs arities :: Arities

Instances

Instances details

Eq TypeSig Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: TypeSig -> TypeSig -> Bool (/=) :: TypeSig -> TypeSig -> Bool
Ord TypeSig Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: TypeSig -> TypeSig -> Ordering (<) :: TypeSig -> TypeSig -> Bool (<=) :: TypeSig -> TypeSig -> Bool (>) :: TypeSig -> TypeSig -> Bool (>=) :: TypeSig -> TypeSig -> Bool max :: TypeSig -> TypeSig -> TypeSig min :: TypeSig -> TypeSig -> TypeSig
Show TypeSig Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> TypeSig -> ShowS show :: TypeSig -> String showList :: [TypeSig] -> ShowS
Generic TypeSig
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep TypeSig :: Type -> Type Methods from :: TypeSig -> Rep TypeSig x to :: Rep TypeSig x -> TypeSig
FromJSON TypeSig
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser TypeSig parseJSONList :: Value -> Parser [TypeSig]
ToJSON TypeSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: TypeSig -> Value toEncoding :: TypeSig -> Encoding toJSONList :: [TypeSig] -> Value toEncodingList :: [TypeSig] -> Encoding
ShATermConvertible TypeSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> TypeSig -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeSig] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeSig) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeSig])
type Rep TypeSig
Instance details Defined in Isabelle.ATC_Isabelle type Rep TypeSig = D1 ('MetaData "TypeSig" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "TySg" 'PrefixI 'True) (((S1 ('MetaSel ('Just "classrel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Classrel) :: S1 ('MetaSel ('Just "locales") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Locales)) :: (S1 ('MetaSel ('Just "defs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Defs) :: S1 ('MetaSel ('Just "funs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Funs))) :: ((S1 ('MetaSel ('Just "defaultSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :: S1 ('MetaSel ('Just "log_types") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TName])) :: (S1 ('MetaSel ('Just "univ_witness") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Typ, Sort))) :: (S1 ('MetaSel ('Just "abbrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Abbrs) :: S1 ('MetaSel ('Just "arities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arities))))))

emptyTypeSig :: TypeSig Source #

isSubTypeSig :: TypeSig -> TypeSig -> Bool Source #

data BaseSig Source #

Constructors

Main_thy	main theory of higher order logic (HOL)
Custom_thy
MainHC_thy	extend main theory of HOL logic for HasCASL
MainHCPairs_thy	for HasCASL translation to bool pairs
HOLCF_thy	higher order logic for continuous functions
HsHOLCF_thy	HOLCF for Haskell
HsHOL_thy	HOL for Haskell
MHsHOL_thy
MHsHOLCF_thy
CspHOLComplex_thy

Instances

Instances details

Eq BaseSig Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: BaseSig -> BaseSig -> Bool (/=) :: BaseSig -> BaseSig -> Bool
Ord BaseSig Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: BaseSig -> BaseSig -> Ordering (<) :: BaseSig -> BaseSig -> Bool (<=) :: BaseSig -> BaseSig -> Bool (>) :: BaseSig -> BaseSig -> Bool (>=) :: BaseSig -> BaseSig -> Bool max :: BaseSig -> BaseSig -> BaseSig min :: BaseSig -> BaseSig -> BaseSig
Show BaseSig Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> BaseSig -> ShowS show :: BaseSig -> String showList :: [BaseSig] -> ShowS
Generic BaseSig
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep BaseSig :: Type -> Type Methods from :: BaseSig -> Rep BaseSig x to :: Rep BaseSig x -> BaseSig
FromJSON BaseSig
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser BaseSig parseJSONList :: Value -> Parser [BaseSig]
ToJSON BaseSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: BaseSig -> Value toEncoding :: BaseSig -> Encoding toJSONList :: [BaseSig] -> Value toEncodingList :: [BaseSig] -> Encoding
ShATermConvertible BaseSig
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> BaseSig -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BaseSig] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BaseSig) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BaseSig])
type Rep BaseSig
Instance details Defined in Isabelle.ATC_Isabelle type Rep BaseSig = D1 ('MetaData "BaseSig" "Isabelle.IsaSign" "main" 'False) (((C1 ('MetaCons "Main_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Custom_thy" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MainHC_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MainHCPairs_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HOLCF_thy" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "HsHOLCF_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HsHOL_thy" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MHsHOL_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MHsHOLCF_thy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CspHOLComplex_thy" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Sign Source #

Constructors

Sign
Fields theoryName :: String header :: Maybe String keywords :: [String] uses :: [String] baseSig :: BaseSig imports :: [String] tsig :: TypeSig constTab :: ConstTab domainTab :: DomainTab showLemmas :: Bool

Instances

Instances details

Eq Sign Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Sign -> Sign -> Bool (/=) :: Sign -> Sign -> Bool
Ord Sign Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Sign -> Sign -> Ordering (<) :: Sign -> Sign -> Bool (<=) :: Sign -> Sign -> Bool (>) :: Sign -> Sign -> Bool (>=) :: Sign -> Sign -> Bool max :: Sign -> Sign -> Sign min :: Sign -> Sign -> Sign
Show Sign Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Sign -> ShowS show :: Sign -> String showList :: [Sign] -> ShowS
Generic Sign
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Sign :: Type -> Type Methods from :: Sign -> Rep Sign x to :: Rep Sign x -> Sign
FromJSON Sign
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Sign parseJSONList :: Value -> Parser [Sign]
ToJSON Sign
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Sign -> Value toEncoding :: Sign -> Encoding toJSONList :: [Sign] -> Value toEncodingList :: [Sign] -> Encoding
ShATermConvertible Sign
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])
Pretty Sign Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: Sign -> Doc Source # pretties :: [Sign] -> Doc Source #
Sentences Isabelle Sentence Sign IsabelleMorphism () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods map_sen :: Isabelle -> IsabelleMorphism -> Sentence -> Result Sentence Source # simplify_sen :: Isabelle -> Sign -> Sentence -> Sentence Source # negation :: Isabelle -> Sentence -> Maybe Sentence Source # print_sign :: Isabelle -> Sign -> Doc Source # print_named :: Isabelle -> Named Sentence -> Doc Source # sym_of :: Isabelle -> Sign -> [Set ()] Source # mostSymsOf :: Isabelle -> Sign -> [()] Source # symmap_of :: Isabelle -> IsabelleMorphism -> EndoMap () Source # sym_name :: Isabelle -> () -> Id Source # sym_label :: Isabelle -> () -> Maybe String Source # fullSymName :: Isabelle -> () -> String Source # symKind :: Isabelle -> () -> String Source # symsOfSen :: Isabelle -> Sign -> Sentence -> [()] Source # pair_symbols :: Isabelle -> () -> () -> Result () Source #
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source # convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source # qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source # symbol_to_raw :: Isabelle -> () -> () Source # id_to_raw :: Isabelle -> Id -> () Source # matches :: Isabelle -> () -> () -> Bool Source # empty_signature :: Isabelle -> Sign Source # add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source # signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source # signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source # intersection :: Isabelle -> Sign -> Sign -> Result Sign Source # final_union :: Isabelle -> Sign -> Sign -> Result Sign Source # morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source # is_subsig :: Isabelle -> Sign -> Sign -> Bool Source # subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source # generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source # induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source # is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source # is_injective :: Isabelle -> IsabelleMorphism -> Bool Source # theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods base_sig :: Isabelle -> Sign Source # write_logic :: Isabelle -> String -> String Source # write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source # write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source # write_model :: Isabelle -> String -> IsabelleMorphism -> String Source # read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source # write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #
Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source # stability :: Isabelle -> Stability Source # data_logic :: Isabelle -> Maybe AnyLogic Source # top_sublogic :: Isabelle -> () Source # all_sublogics :: Isabelle -> [()] Source # bottomSublogic :: Isabelle -> Maybe () Source # sublogicDimensions :: Isabelle -> [[()]] Source # parseSublogic :: Isabelle -> String -> Maybe () Source # proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source # provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source # default_prover :: Isabelle -> String Source # cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source # conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source # empty_proof_tree :: Isabelle -> () Source # syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: Isabelle -> Maybe OMCD Source # export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: Isabelle -> (Sign, [Sentence]) -> () Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle Methods sourceLogic :: HolLight2Isabelle -> HolLight Source # sourceSublogic :: HolLight2Isabelle -> HolLightSL Source # sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source # minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source # targetLogic :: HolLight2Isabelle -> Isabelle Source # mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source # map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source # map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source # map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source # extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source # is_model_transportable :: HolLight2Isabelle -> Bool Source # has_model_expansion :: HolLight2Isabelle -> Bool Source # is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source # constituents :: HolLight2Isabelle -> [String] Source # isInclusionComorphism :: HolLight2Isabelle -> Bool Source # rps :: HolLight2Isabelle -> Bool Source # eps :: HolLight2Isabelle -> Bool Source # isGTC :: HolLight2Isabelle -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source # sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # minSourceTheory :: CommonLogic2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source # mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source # map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source # map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source # extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source # is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source # has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source # constituents :: CommonLogic2IsabelleHOL -> [String] Source # isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source # rps :: CommonLogic2IsabelleHOL -> Bool Source # eps :: CommonLogic2IsabelleHOL -> Bool Source # isGTC :: CommonLogic2IsabelleHOL -> Bool Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
type Rep Sign
Instance details Defined in Isabelle.ATC_Isabelle type Rep Sign = D1 ('MetaData "Sign" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "Sign" 'PrefixI 'True) (((S1 ('MetaSel ('Just "theoryName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "header") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))) :: (S1 ('MetaSel ('Just "keywords") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: (S1 ('MetaSel ('Just "uses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Just "baseSig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BaseSig)))) :: ((S1 ('MetaSel ('Just "imports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Just "tsig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSig)) :: (S1 ('MetaSel ('Just "constTab") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstTab) :: (S1 ('MetaSel ('Just "domainTab") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DomainTab) :*: S1 ('MetaSel ('Just "showLemmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))

type ConstTab = Map VName Typ Source #

type DomainTab = [[DomainEntry]] Source #

type DomainEntry = (Typ, [(VName, [Typ])]) Source #

emptySign :: Sign Source #

isSubSign :: Sign -> Sign -> Bool Source #

union_tsig :: TypeSig -> TypeSig -> TypeSig Source #

union_sig :: Sign -> Sign -> Sign Source #

data IsaProof Source #

Constructors

IsaProof
Fields proof :: [ProofCommand] end :: ProofEnd

Instances

Instances details

Eq IsaProof Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: IsaProof -> IsaProof -> Bool (/=) :: IsaProof -> IsaProof -> Bool
Data IsaProof Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsaProof -> c IsaProof gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsaProof toConstr :: IsaProof -> Constr dataTypeOf :: IsaProof -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsaProof) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsaProof) gmapT :: (forall b. Data b => b -> b) -> IsaProof -> IsaProof gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsaProof -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsaProof -> r gmapQ :: (forall d. Data d => d -> u) -> IsaProof -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsaProof -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof
Ord IsaProof Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: IsaProof -> IsaProof -> Ordering (<) :: IsaProof -> IsaProof -> Bool (<=) :: IsaProof -> IsaProof -> Bool (>) :: IsaProof -> IsaProof -> Bool (>=) :: IsaProof -> IsaProof -> Bool max :: IsaProof -> IsaProof -> IsaProof min :: IsaProof -> IsaProof -> IsaProof
Show IsaProof Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> IsaProof -> ShowS show :: IsaProof -> String showList :: [IsaProof] -> ShowS
Generic IsaProof
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep IsaProof :: Type -> Type Methods from :: IsaProof -> Rep IsaProof x to :: Rep IsaProof x -> IsaProof
FromJSON IsaProof
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser IsaProof parseJSONList :: Value -> Parser [IsaProof]
ToJSON IsaProof
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: IsaProof -> Value toEncoding :: IsaProof -> Encoding toJSONList :: [IsaProof] -> Value toEncodingList :: [IsaProof] -> Encoding
ShATermConvertible IsaProof
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> IsaProof -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [IsaProof] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, IsaProof) fromShATermList' :: Int -> ATermTable -> (ATermTable, [IsaProof])
Pretty IsaProof Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: IsaProof -> Doc Source # pretties :: [IsaProof] -> Doc Source #
type Rep IsaProof
Instance details Defined in Isabelle.ATC_Isabelle type Rep IsaProof = D1 ('MetaData "IsaProof" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "IsaProof" 'PrefixI 'True) (S1 ('MetaSel ('Just "proof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProofCommand]) :*: S1 ('MetaSel ('Just "end") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProofEnd)))

data ProofCommand Source #

Constructors

Apply [ProofMethod] Bool	Apply a list of proof methods, which will be applied in sequence withing the apply proof command. The boolean is if the + modifier should be used at the end of the apply proof method. e.g. Apply(A,B,C) True would represent the Isabelle proof command "apply(A,B,C)+"
Using [String]
Back
Defer Int
Prefer Int
Refute

Instances

Instances details

Eq ProofCommand Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: ProofCommand -> ProofCommand -> Bool (/=) :: ProofCommand -> ProofCommand -> Bool
Data ProofCommand Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofCommand -> c ProofCommand gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofCommand toConstr :: ProofCommand -> Constr dataTypeOf :: ProofCommand -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProofCommand) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofCommand) gmapT :: (forall b. Data b => b -> b) -> ProofCommand -> ProofCommand gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofCommand -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofCommand -> r gmapQ :: (forall d. Data d => d -> u) -> ProofCommand -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofCommand -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand
Ord ProofCommand Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: ProofCommand -> ProofCommand -> Ordering (<) :: ProofCommand -> ProofCommand -> Bool (<=) :: ProofCommand -> ProofCommand -> Bool (>) :: ProofCommand -> ProofCommand -> Bool (>=) :: ProofCommand -> ProofCommand -> Bool max :: ProofCommand -> ProofCommand -> ProofCommand min :: ProofCommand -> ProofCommand -> ProofCommand
Show ProofCommand Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> ProofCommand -> ShowS show :: ProofCommand -> String showList :: [ProofCommand] -> ShowS
Generic ProofCommand
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep ProofCommand :: Type -> Type Methods from :: ProofCommand -> Rep ProofCommand x to :: Rep ProofCommand x -> ProofCommand
FromJSON ProofCommand
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser ProofCommand parseJSONList :: Value -> Parser [ProofCommand]
ToJSON ProofCommand
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: ProofCommand -> Value toEncoding :: ProofCommand -> Encoding toJSONList :: [ProofCommand] -> Value toEncodingList :: [ProofCommand] -> Encoding
ShATermConvertible ProofCommand
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> ProofCommand -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProofCommand] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofCommand) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofCommand])
Pretty ProofCommand Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: ProofCommand -> Doc Source # pretties :: [ProofCommand] -> Doc Source #
type Rep ProofCommand
Instance details Defined in Isabelle.ATC_Isabelle type Rep ProofCommand = D1 ('MetaData "ProofCommand" "Isabelle.IsaSign" "main" 'False) ((C1 ('MetaCons "Apply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProofMethod]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: (C1 ('MetaCons "Using" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "Back" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Defer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "Prefer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Refute" 'PrefixI 'False) (U1 :: Type -> Type))))

data ProofEnd Source #

Constructors

By ProofMethod
DotDot
Done
Oops
Sorry

Instances

Instances details

Eq ProofEnd Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: ProofEnd -> ProofEnd -> Bool (/=) :: ProofEnd -> ProofEnd -> Bool
Data ProofEnd Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofEnd -> c ProofEnd gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofEnd toConstr :: ProofEnd -> Constr dataTypeOf :: ProofEnd -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProofEnd) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofEnd) gmapT :: (forall b. Data b => b -> b) -> ProofEnd -> ProofEnd gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofEnd -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofEnd -> r gmapQ :: (forall d. Data d => d -> u) -> ProofEnd -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofEnd -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd
Ord ProofEnd Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: ProofEnd -> ProofEnd -> Ordering (<) :: ProofEnd -> ProofEnd -> Bool (<=) :: ProofEnd -> ProofEnd -> Bool (>) :: ProofEnd -> ProofEnd -> Bool (>=) :: ProofEnd -> ProofEnd -> Bool max :: ProofEnd -> ProofEnd -> ProofEnd min :: ProofEnd -> ProofEnd -> ProofEnd
Show ProofEnd Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> ProofEnd -> ShowS show :: ProofEnd -> String showList :: [ProofEnd] -> ShowS
Generic ProofEnd
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep ProofEnd :: Type -> Type Methods from :: ProofEnd -> Rep ProofEnd x to :: Rep ProofEnd x -> ProofEnd
FromJSON ProofEnd
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser ProofEnd parseJSONList :: Value -> Parser [ProofEnd]
ToJSON ProofEnd
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: ProofEnd -> Value toEncoding :: ProofEnd -> Encoding toJSONList :: [ProofEnd] -> Value toEncodingList :: [ProofEnd] -> Encoding
ShATermConvertible ProofEnd
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> ProofEnd -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProofEnd] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofEnd) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofEnd])
Pretty ProofEnd Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: ProofEnd -> Doc Source # pretties :: [ProofEnd] -> Doc Source #
type Rep ProofEnd
Instance details Defined in Isabelle.ATC_Isabelle type Rep ProofEnd = D1 ('MetaData "ProofEnd" "Isabelle.IsaSign" "main" 'False) ((C1 ('MetaCons "By" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProofMethod)) :+: C1 ('MetaCons "DotDot" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Done" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Oops" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sorry" 'PrefixI 'False) (U1 :: Type -> Type))))

data Modifier Source #

Constructors

No_asm	No_asm means that assumptions are completely ignored.
No_asm_simp	No_asm_simp means that the assumptions are not simplified but are used in the simplification of the conclusion.
No_asm_use	No_asm_use means that the assumptions are simplified but are not used in the simplification of each other or the conclusion.

Instances

Instances details

Eq Modifier Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: Modifier -> Modifier -> Bool (/=) :: Modifier -> Modifier -> Bool
Data Modifier Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Modifier -> c Modifier gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modifier toConstr :: Modifier -> Constr dataTypeOf :: Modifier -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Modifier) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modifier) gmapT :: (forall b. Data b => b -> b) -> Modifier -> Modifier gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modifier -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modifier -> r gmapQ :: (forall d. Data d => d -> u) -> Modifier -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Modifier -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier
Ord Modifier Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: Modifier -> Modifier -> Ordering (<) :: Modifier -> Modifier -> Bool (<=) :: Modifier -> Modifier -> Bool (>) :: Modifier -> Modifier -> Bool (>=) :: Modifier -> Modifier -> Bool max :: Modifier -> Modifier -> Modifier min :: Modifier -> Modifier -> Modifier
Show Modifier Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> Modifier -> ShowS show :: Modifier -> String showList :: [Modifier] -> ShowS
Generic Modifier
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep Modifier :: Type -> Type Methods from :: Modifier -> Rep Modifier x to :: Rep Modifier x -> Modifier
FromJSON Modifier
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser Modifier parseJSONList :: Value -> Parser [Modifier]
ToJSON Modifier
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: Modifier -> Value toEncoding :: Modifier -> Encoding toJSONList :: [Modifier] -> Value toEncodingList :: [Modifier] -> Encoding
ShATermConvertible Modifier
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> Modifier -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Modifier] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Modifier) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Modifier])
Pretty Modifier Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: Modifier -> Doc Source # pretties :: [Modifier] -> Doc Source #
type Rep Modifier
Instance details Defined in Isabelle.ATC_Isabelle type Rep Modifier = D1 ('MetaData "Modifier" "Isabelle.IsaSign" "main" 'False) (C1 ('MetaCons "No_asm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "No_asm_simp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "No_asm_use" 'PrefixI 'False) (U1 :: Type -> Type)))

data ProofMethod Source #

Constructors

Auto	This is a plain auto with no parameters - it is used so often it warents its own constructor
Simp	This is a plain auto with no parameters - it is used so often it warents its own constructor
AutoSimpAdd (Maybe Modifier) [String]	This is an auto where the simpset has been temporarily extended with a listof lemmas, theorems and axioms. An optional modifier can also be used to control how the assumptions are used. It is used so often it warents its own constructor
SimpAdd (Maybe Modifier) [String]	This is a simp where the simpset has been temporarily extended with a listof lemmas, theorems and axioms. An optional modifier can also be used to control how the assumptions are used. It is used so often it warents its own constructor
Induct Term	Induction proof method. This performs induction upon a variable
CaseTac Term	Case_tac proof method. This perfom a case distinction on a term
SubgoalTac Term	Subgoal_tac proof method . Adds a term to the local assumptions and also creates a sub-goal of this term
Insert [String]	Insert proof method. Inserts a lemma or theorem name to the assumptions of the first goal
Other String	Used for proof methods that have not been implemented yet. This includes auto and simp with parameters

Instances

Instances details

Eq ProofMethod Source #
Instance details Defined in Isabelle.IsaSign Methods (==) :: ProofMethod -> ProofMethod -> Bool (/=) :: ProofMethod -> ProofMethod -> Bool
Data ProofMethod Source #
Instance details Defined in Isabelle.IsaSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofMethod -> c ProofMethod gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofMethod toConstr :: ProofMethod -> Constr dataTypeOf :: ProofMethod -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProofMethod) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofMethod) gmapT :: (forall b. Data b => b -> b) -> ProofMethod -> ProofMethod gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofMethod -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofMethod -> r gmapQ :: (forall d. Data d => d -> u) -> ProofMethod -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofMethod -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod
Ord ProofMethod Source #
Instance details Defined in Isabelle.IsaSign Methods compare :: ProofMethod -> ProofMethod -> Ordering (<) :: ProofMethod -> ProofMethod -> Bool (<=) :: ProofMethod -> ProofMethod -> Bool (>) :: ProofMethod -> ProofMethod -> Bool (>=) :: ProofMethod -> ProofMethod -> Bool max :: ProofMethod -> ProofMethod -> ProofMethod min :: ProofMethod -> ProofMethod -> ProofMethod
Show ProofMethod Source #
Instance details Defined in Isabelle.IsaSign Methods showsPrec :: Int -> ProofMethod -> ShowS show :: ProofMethod -> String showList :: [ProofMethod] -> ShowS
Generic ProofMethod
Instance details Defined in Isabelle.ATC_Isabelle Associated Types type Rep ProofMethod :: Type -> Type Methods from :: ProofMethod -> Rep ProofMethod x to :: Rep ProofMethod x -> ProofMethod
FromJSON ProofMethod
Instance details Defined in Isabelle.ATC_Isabelle Methods parseJSON :: Value -> Parser ProofMethod parseJSONList :: Value -> Parser [ProofMethod]
ToJSON ProofMethod
Instance details Defined in Isabelle.ATC_Isabelle Methods toJSON :: ProofMethod -> Value toEncoding :: ProofMethod -> Encoding toJSONList :: [ProofMethod] -> Value toEncodingList :: [ProofMethod] -> Encoding
ShATermConvertible ProofMethod
Instance details Defined in Isabelle.ATC_Isabelle Methods toShATermAux :: ATermTable -> ProofMethod -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProofMethod] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofMethod) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofMethod])
Pretty ProofMethod Source #
Instance details Defined in Isabelle.IsaPrint Methods pretty :: ProofMethod -> Doc Source # pretties :: [ProofMethod] -> Doc Source #
type Rep ProofMethod
Instance details Defined in Isabelle.ATC_Isabelle type Rep ProofMethod = D1 ('MetaData "ProofMethod" "Isabelle.IsaSign" "main" 'False) (((C1 ('MetaCons "Auto" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Simp" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AutoSimpAdd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Modifier)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "SimpAdd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Modifier)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))) :+: ((C1 ('MetaCons "Induct" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "CaseTac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "SubgoalTac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "Insert" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "Other" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))

toIsaProof :: ProofEnd -> IsaProof Source #

mkOops :: IsaProof Source #