Safe Haskell	Trustworthy
Language	Haskell2010

Embedder.Isabelle.Syntax

Synopsis

textS :: String -> Doc ann
bar :: [Doc ann] -> Doc ann
andS :: String
($+$) :: Doc ann -> Doc ann -> Doc ann
tyAnn :: Doc ann -> Doc ann -> Doc ann
printCon :: Text -> [Doc ann] -> Doc ann
type TName = Text
data Typ
- = Type {
  - typeId :: TName
  - typeArgs :: [Typ]
  }
- | TBuiltin {
  - typeB :: TyBuiltin
  - typeArgs :: [Typ]
  }
- | TNum {
  - typeN :: Int
  }
- | TVar {
  - typeId :: TName
  }
data TypSig = TypSig {
- typSigArgs :: [Typ]
- typeSigCod :: Typ
}
tyAtomic :: Typ -> Bool
printType :: Typ -> Doc ann
printTyTuple :: [Typ] -> Doc ann
pTyArg :: Typ -> Doc ann
printType' :: TName -> [Typ] -> Doc ann
printTBuiltin :: TyBuiltin -> [Typ] -> Doc ann
isTuple :: Text -> Bool
printTypSig :: TypSig -> Doc ann
data DTyp
- = Hide {
  - typ :: Typ
  }
- | Disp {
  - typ :: Typ
  }
type VName = Text
data QName = QName {
- qname :: Text
- qualifiers :: [Text]
}
data Term
- = LitString Text
- | LitNum Integer
- | LitWord Int Integer
- | LitVec [Term]
- | Free {
  - termName :: VName
  }
- | Prim {
  - primId :: RWUserOp
  }
- | Abs {
  - absVars :: [VName]
  - termId :: Term
  }
- | App {
  - funId :: Term
  - argIds :: [Term]
  }
- | If {
  - ifId :: Term
  - thenId :: Term
  - elseId :: Term
  }
- | Case {
  - termId :: Term
  - caseSubst :: [(Pttrn, Term)]
  }
- | Let {
  - letSubst :: [(Pttrn, Term)]
  - inId :: Term
  }
- | IsaEq {
  - firstTerm :: Term
  - secondTerm :: Term
  }
- | Tuplex [Term]
- | List [Term]
- | RecordVal [(Text, Term)]
- | RecordUpdate Term [(Text, Term)]
- | RecordSel Text Term
- | TypAnnTerm {
  - termId :: Term
  - typAnn :: Typ
  }
atomic :: Term -> Bool
selfGroup :: Term -> Bool
pArg :: Term -> Doc ann
infixBuiltinList :: [Builtin]
infixRWUserOpList :: [RWUserOp]
prefixBuiltinList :: [Builtin]
prefixRWUserOpList :: [RWUserOp]
isInfix :: RWUserOp -> Bool
isPrefix :: RWUserOp -> Bool
textListRWOp :: [(RWUserOp, Text)]
printApp :: Term -> [Term] -> Doc ann
rwOpText :: RWUserOp -> Text
pOp :: RWUserOp -> [Term] -> Doc ann
printApp' :: Term -> [Term] -> Doc ann
printTuple :: Pretty a => [a] -> Doc ann
prettyTerm :: Term -> Doc ann
data Pttrn
- = PttrnWildCard (Maybe Typ)
- | PttrnVar VName (Maybe Typ)
- | PttrnCon VName (Maybe Typ) [Pttrn]
- | PttrnTuple (Maybe Typ) [Pttrn]
- | PttrnAs (Maybe Typ) Pttrn VName
- | PttrnRecord (Maybe Typ) [(Text, Pttrn)]
data DatatypeConstructor = DatatypeConstructor {
- constructorName :: Text
- constructorArgs :: [Typ]
}
printDatatypeConstructor :: DatatypeConstructor -> Doc ann
data Decl
- = Datatype {
  - datatypeName :: Text
  - datatypeTVars :: [TName]
  - datatypeConstructors :: [DatatypeConstructor]
  }
- | Record {
  - recordName :: Text
  - recordTVars :: [Text]
  - recordFields :: [(Text, Typ)]
  }
- | TypeSynonym Text [Text] Typ
- | Definition {
  - definitionName :: Text
  - definitionType :: TypSig
  - definitionVars :: [Term]
  - definitionTerm :: Term
  }
- | Fun {
  - funEquations :: [(Text, TypSig, [([Pttrn], Term)])]
  }
data Theory = Theory {
- thyName :: Text
- imports :: [Text]
- decls :: [Decl]
}
printDecls :: Theory -> Doc ann
mkHeader :: Theory -> Doc ann
mkFooter :: Theory -> Doc ann

Documentation

textS :: String -> Doc ann Source #

bar :: [Doc ann] -> Doc ann Source #

andS :: String Source #

($+$) :: Doc ann -> Doc ann -> Doc ann Source #

tyAnn :: Doc ann -> Doc ann -> Doc ann Source #

printCon :: Text -> [Doc ann] -> Doc ann Source #

type TName = Text Source #

Names

data Typ Source #

Types

Constructors

Type
Fields typeId :: TName typeArgs :: [Typ]
TBuiltin
Fields typeB :: TyBuiltin typeArgs :: [Typ]
TNum
Fields typeN :: Int
TVar
Fields typeId :: TName

Instances

Instances details

Data Typ Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Show Typ Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> Typ -> ShowS # show :: Typ -> String # showList :: [Typ] -> ShowS #
Eq Typ Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: Typ -> Typ -> Bool # (/=) :: Typ -> Typ -> Bool #
Ord Typ Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Pretty Typ Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: Typ -> Doc ann # prettyList :: [Typ] -> Doc ann

data TypSig Source #

Constructors

TypSig
Fields typSigArgs :: [Typ] typeSigCod :: Typ

Instances

Instances details

Data TypSig Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypSig -> c TypSig # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypSig # toConstr :: TypSig -> Constr # dataTypeOf :: TypSig -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypSig) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypSig) # gmapT :: (forall b. Data b => b -> b) -> TypSig -> TypSig # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r # gmapQ :: (forall d. Data d => d -> u) -> TypSig -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypSig -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypSig -> m TypSig # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypSig -> m TypSig # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypSig -> m TypSig #
Show TypSig Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> TypSig -> ShowS # show :: TypSig -> String # showList :: [TypSig] -> ShowS #
Eq TypSig Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: TypSig -> TypSig -> Bool # (/=) :: TypSig -> TypSig -> Bool #
Ord TypSig Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods compare :: TypSig -> TypSig -> Ordering # (<) :: TypSig -> TypSig -> Bool # (<=) :: TypSig -> TypSig -> Bool # (>) :: TypSig -> TypSig -> Bool # (>=) :: TypSig -> TypSig -> Bool # max :: TypSig -> TypSig -> TypSig # min :: TypSig -> TypSig -> TypSig #
Pretty TypSig Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: TypSig -> Doc ann # prettyList :: [TypSig] -> Doc ann

tyAtomic :: Typ -> Bool Source #

printType :: Typ -> Doc ann Source #

printTyTuple :: [Typ] -> Doc ann Source #

pTyArg :: Typ -> Doc ann Source #

printType' :: TName -> [Typ] -> Doc ann Source #

printTBuiltin :: TyBuiltin -> [Typ] -> Doc ann Source #

isTuple :: Text -> Bool Source #

printTypSig :: TypSig -> Doc ann Source #

data DTyp Source #

Types for Terms

Constructors

Hide
Fields typ :: Typ
Disp
Fields typ :: Typ

Instances

Instances details

Data DTyp Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Show DTyp Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> DTyp -> ShowS # show :: DTyp -> String # showList :: [DTyp] -> ShowS #
Eq DTyp Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: DTyp -> DTyp -> Bool # (/=) :: DTyp -> DTyp -> Bool #
Ord DTyp Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #

type VName = Text Source #

Names

data QName Source #

Names with Qualifiers

Constructors

QName
Fields qname :: Text qualifiers :: [Text]

Instances

Instances details

Data QName Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Show QName Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> QName -> ShowS # show :: QName -> String # showList :: [QName] -> ShowS #
Eq QName Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: QName -> QName -> Bool # (/=) :: QName -> QName -> Bool #
Ord QName Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #

data Term Source #

Constructors

LitString Text
LitNum Integer
LitWord Int Integer
LitVec [Term]
Free
Fields termName :: VName
Prim
Fields primId :: RWUserOp
Abs	lambda abstraction
Fields absVars :: [VName] termId :: Term
App	application
Fields funId :: Term argIds :: [Term]
If
Fields ifId :: Term thenId :: Term elseId :: Term
Case
Fields termId :: Term caseSubst :: [(Pttrn, Term)]
Let
Fields letSubst :: [(Pttrn, Term)] inId :: Term
IsaEq
Fields firstTerm :: Term secondTerm :: Term
Tuplex [Term]
List [Term]
RecordVal [(Text, Term)]
RecordUpdate Term [(Text, Term)]
RecordSel Text Term
TypAnnTerm
Fields termId :: Term typAnn :: Typ

Instances

Instances details

Data Term Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Show Term Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
Eq Term Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Ord Term Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Pretty Term Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: Term -> Doc ann # prettyList :: [Term] -> Doc ann

atomic :: Term -> Bool Source #

selfGroup :: Term -> Bool Source #

pArg :: Term -> Doc ann Source #

infixBuiltinList :: [Builtin] Source #

infixRWUserOpList :: [RWUserOp] Source #

prefixBuiltinList :: [Builtin] Source #

prefixRWUserOpList :: [RWUserOp] Source #

isInfix :: RWUserOp -> Bool Source #

isPrefix :: RWUserOp -> Bool Source #

textListRWOp :: [(RWUserOp, Text)] Source #

printApp :: Term -> [Term] -> Doc ann Source #

rwOpText :: RWUserOp -> Text Source #

pOp :: RWUserOp -> [Term] -> Doc ann Source #

printApp' :: Term -> [Term] -> Doc ann Source #

printTuple :: Pretty a => [a] -> Doc ann Source #

prettyTerm :: Term -> Doc ann Source #

data Pttrn Source #

Constructors

PttrnWildCard (Maybe Typ)
PttrnVar VName (Maybe Typ)
PttrnCon VName (Maybe Typ) [Pttrn]
PttrnTuple (Maybe Typ) [Pttrn]
PttrnAs (Maybe Typ) Pttrn VName
PttrnRecord (Maybe Typ) [(Text, Pttrn)]

Instances

Instances details

Data Pttrn Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pttrn -> c Pttrn # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pttrn # toConstr :: Pttrn -> Constr # dataTypeOf :: Pttrn -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pttrn) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pttrn) # gmapT :: (forall b. Data b => b -> b) -> Pttrn -> Pttrn # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r # gmapQ :: (forall d. Data d => d -> u) -> Pttrn -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pttrn -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn #
Show Pttrn Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> Pttrn -> ShowS # show :: Pttrn -> String # showList :: [Pttrn] -> ShowS #
Eq Pttrn Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: Pttrn -> Pttrn -> Bool # (/=) :: Pttrn -> Pttrn -> Bool #
Ord Pttrn Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods compare :: Pttrn -> Pttrn -> Ordering # (<) :: Pttrn -> Pttrn -> Bool # (<=) :: Pttrn -> Pttrn -> Bool # (>) :: Pttrn -> Pttrn -> Bool # (>=) :: Pttrn -> Pttrn -> Bool # max :: Pttrn -> Pttrn -> Pttrn # min :: Pttrn -> Pttrn -> Pttrn #
Pretty Pttrn Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: Pttrn -> Doc ann # prettyList :: [Pttrn] -> Doc ann

data DatatypeConstructor Source #

Constructors

DatatypeConstructor
Fields constructorName :: Text constructorArgs :: [Typ]

Instances

Instances details

Data DatatypeConstructor Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Show DatatypeConstructor Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> DatatypeConstructor -> ShowS # show :: DatatypeConstructor -> String # showList :: [DatatypeConstructor] -> ShowS #
Eq DatatypeConstructor Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: DatatypeConstructor -> DatatypeConstructor -> Bool # (/=) :: DatatypeConstructor -> DatatypeConstructor -> Bool #
Ord DatatypeConstructor Source #
Instance details Defined in Embedder.Isabelle.Syntax 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 #
Pretty DatatypeConstructor Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: DatatypeConstructor -> Doc ann # prettyList :: [DatatypeConstructor] -> Doc ann

printDatatypeConstructor :: DatatypeConstructor -> Doc ann Source #

data Decl Source #

Constructors

Datatype
Fields datatypeName :: Text datatypeTVars :: [TName] datatypeConstructors :: [DatatypeConstructor]
Record
Fields recordName :: Text recordTVars :: [Text] recordFields :: [(Text, Typ)]
TypeSynonym Text [Text] Typ
Definition
Fields definitionName :: Text definitionType :: TypSig definitionVars :: [Term] definitionTerm :: Term
Fun
Fields funEquations :: [(Text, TypSig, [([Pttrn], Term)])]

Instances

Instances details

Data Decl Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Decl -> c Decl # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Decl # toConstr :: Decl -> Constr # dataTypeOf :: Decl -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Decl) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Decl) # gmapT :: (forall b. Data b => b -> b) -> Decl -> Decl # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r # gmapQ :: (forall d. Data d => d -> u) -> Decl -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Decl -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Decl -> m Decl # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Decl -> m Decl # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Decl -> m Decl #
Show Decl Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> Decl -> ShowS # show :: Decl -> String # showList :: [Decl] -> ShowS #
Eq Decl Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: Decl -> Decl -> Bool # (/=) :: Decl -> Decl -> Bool #
Ord Decl Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods compare :: Decl -> Decl -> Ordering # (<) :: Decl -> Decl -> Bool # (<=) :: Decl -> Decl -> Bool # (>) :: Decl -> Decl -> Bool # (>=) :: Decl -> Decl -> Bool # max :: Decl -> Decl -> Decl # min :: Decl -> Decl -> Decl #
Pretty Decl Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: Decl -> Doc ann # prettyList :: [Decl] -> Doc ann

data Theory Source #

Constructors

Theory
Fields thyName :: Text imports :: [Text] decls :: [Decl]

Instances

Instances details

Show Theory Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods showsPrec :: Int -> Theory -> ShowS # show :: Theory -> String # showList :: [Theory] -> ShowS #
Eq Theory Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods (==) :: Theory -> Theory -> Bool # (/=) :: Theory -> Theory -> Bool #
Ord Theory Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods compare :: Theory -> Theory -> Ordering # (<) :: Theory -> Theory -> Bool # (<=) :: Theory -> Theory -> Bool # (>) :: Theory -> Theory -> Bool # (>=) :: Theory -> Theory -> Bool # max :: Theory -> Theory -> Theory # min :: Theory -> Theory -> Theory #
Pretty Theory Source #
Instance details Defined in Embedder.Isabelle.Syntax Methods pretty :: Theory -> Doc ann # prettyList :: [Theory] -> Doc ann

printDecls :: Theory -> Doc ann Source #

mkHeader :: Theory -> Doc ann Source #

mkFooter :: Theory -> Doc ann Source #