hets -- a heterogenous Specification (CASL) tool setContentsIndex
HasCASL.As
Portability portable
Stability experimental
Maintainer hets@tzi.de
Contents
abstract syntax entities
Description
abstract syntax for HasCASL more liberal than Concrete-Syntax.txt annotations are almost as for CASL
Synopsis
data BasicSpec = BasicSpec [Annoted BasicItem]
data BasicItem
= SigItems SigItems
| ProgItems [Annoted ProgEq] [Pos]
| ClassItems Instance [Annoted ClassItem] [Pos]
| GenVarItems [GenVarDecl] [Pos]
| FreeDatatype [Annoted DatatypeDecl] [Pos]
| GenItems [Annoted SigItems] [Pos]
| AxiomItems [GenVarDecl] [Annoted Term] [Pos]
| Internal [Annoted BasicItem] [Pos]
data SigItems
= TypeItems Instance [Annoted TypeItem] [Pos]
| OpItems OpBrand [Annoted OpItem] [Pos]
data OpBrand
= Pred
| Op
| Fun
data Instance
= Instance
| Plain
data ClassItem = ClassItem ClassDecl [Annoted BasicItem] [Pos]
data ClassDecl = ClassDecl [ClassId] Kind [Pos]
data Variance
= CoVar
| ContraVar
| InVar
data Kind
= Universe [Pos]
| MissingKind
| Downset (Maybe Token) Type Kind [Pos]
| ClassKind ClassId Kind
| Intersection [Kind] [Pos]
| FunKind Kind Kind [Pos]
| ExtKind Kind Variance [Pos]
star :: Kind
starPlus :: Kind
funKind :: Kind
prodKind :: Kind
data TypeItem
= TypeDecl [TypePattern] Kind [Pos]
| SubtypeDecl [TypePattern] Type [Pos]
| IsoDecl [TypePattern] [Pos]
| SubtypeDefn TypePattern Vars Type (Annoted Term) [Pos]
| AliasType TypePattern (Maybe Kind) TypeScheme [Pos]
| Datatype DatatypeDecl
data Vars
= Var Var
| VarTuple [Vars] [Pos]
data TypePattern
= TypePattern TypeId [TypeArg] [Pos]
| TypePatternToken Token
| MixfixTypePattern [TypePattern]
| BracketTypePattern BracketKind [TypePattern] [Pos]
| TypePatternArg TypeArg [Pos]
data Type
= TypeName TypeId Kind Int
| TypeAppl Type Type
| TypeToken Token
| BracketType BracketKind [Type] [Pos]
| KindedType Type Kind [Pos]
| MixfixType [Type]
| LazyType Type [Pos]
| ProductType [Type] [Pos]
| FunType Type Arrow Type [Pos]
mkProductType :: [Type] -> [Pos] -> Type
data Arrow
= FunArr
| PFunArr
| ContFunArr
| PContFunArr
arrowId :: Arrow -> Id
productId :: Id
data Pred = IsIn ClassId [Type]
data Qual t = (:=>) [Pred] t
data TypeScheme = TypeScheme [TypeArg] (Qual Type) [Pos]
simpleTypeScheme :: Type -> TypeScheme
logicalType :: Type
predTypeScheme :: TypeScheme -> TypeScheme
predType :: Type -> Type
data Partiality
= Partial
| Total
data OpItem
= OpDecl [OpId] TypeScheme [OpAttr] [Pos]
| OpDefn OpId [[VarDecl]] TypeScheme Partiality Term [Pos]
data BinOpAttr
= Assoc
| Comm
| Idem
data OpAttr
= BinOpAttr BinOpAttr [Pos]
| UnitOpAttr Term [Pos]
data DatatypeDecl = DatatypeDecl TypePattern Kind [Annoted Alternative] [ClassId] [Pos]
data Alternative
= Constructor UninstOpId [[Component]] Partiality [Pos]
| Subtype [Type] [Pos]
data Component
= Selector UninstOpId Partiality Type SeparatorKind Pos
| NoSelector Type
data Quantifier
= Universal
| Existential
| Unique
data TypeQual
= OfType
| AsType
| InType
data LetBrand
= Let
| Where
data BracketKind
= Parens
| Squares
| Braces
getBrackets :: BracketKind -> (String, String)
data Term
= QualVar Var Type [Pos]
| QualOp OpBrand InstOpId TypeScheme [Pos]
| ResolvedMixTerm Id [Term] [Pos]
| ApplTerm Term Term [Pos]
| TupleTerm [Term] [Pos]
| TypedTerm Term TypeQual Type [Pos]
| QuantifiedTerm Quantifier [GenVarDecl] Term [Pos]
| LambdaTerm [Pattern] Partiality Term [Pos]
| CaseTerm Term [ProgEq] [Pos]
| LetTerm LetBrand [ProgEq] Term [Pos]
| TermToken Token
| MixInTerm Type [Pos]
| MixfixTerm [Term]
| BracketTerm BracketKind [Term] [Pos]
mkTupleTerm :: [Term] -> [Pos] -> Term
data Pattern
= PatternVar VarDecl
| PatternConstr InstOpId TypeScheme [Pos]
| ResolvedMixPattern Id [Pattern] [Pos]
| ApplPattern Pattern Pattern [Pos]
| TuplePattern [Pattern] [Pos]
| TypedPattern Pattern Type [Pos]
| AsPattern Pattern Pattern [Pos]
| PatternToken Token
| BracketPattern BracketKind [Pattern] [Pos]
| MixfixPattern [Pattern]
mkTuplePattern :: [Pattern] -> [Pos] -> Pattern
data ProgEq = ProgEq Pattern Term Pos
data SeparatorKind
= Comma
| Other
data VarDecl = VarDecl Var Type SeparatorKind [Pos]
data TypeArg = TypeArg TypeId Kind SeparatorKind [Pos]
data GenVarDecl
= GenVarDecl VarDecl
| GenTypeVarDecl TypeArg
data OpId = OpId UninstOpId [TypeArg] [Pos]
data InstOpId = InstOpId UninstOpId [Type] [Pos]
type TypeId = Id
type UninstOpId = Id
type Var = Id
type ClassId = Id
abstract syntax entities
data BasicSpec
Constructors
BasicSpec [Annoted BasicItem]
Instances
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
ATermConvertible BasicSpec
Show BasicSpec
Eq BasicSpec
Typeable BasicSpec
Syntax HasCASL BasicSpec SymbItems SymbMapItems
StaticAnalysis HasCASL BasicSpec Term () SymbItems SymbMapItems Env Morphism Symbol RawSymbol
Logic HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
PrettyPrint BasicSpec
data BasicItem
Constructors
SigItems SigItems
ProgItems [Annoted ProgEq] [Pos]
ClassItems Instance [Annoted ClassItem] [Pos]
GenVarItems [GenVarDecl] [Pos]
FreeDatatype [Annoted DatatypeDecl] [Pos]
GenItems [Annoted SigItems] [Pos]
AxiomItems [GenVarDecl] [Annoted Term] [Pos]
Internal [Annoted BasicItem] [Pos]
Instances
ATermConvertible BasicItem
Show BasicItem
Eq BasicItem
PrettyPrint BasicItem
data SigItems
Constructors
TypeItems Instance [Annoted TypeItem] [Pos]
OpItems OpBrand [Annoted OpItem] [Pos]
Instances
ATermConvertible SigItems
Show SigItems
Eq SigItems
PrettyPrint SigItems
data OpBrand
indicator for predicate, operation or function
Constructors
Pred
Op
Fun
Instances
ATermConvertible OpBrand
Show OpBrand
Eq OpBrand
Mergeable OpBrand
PrettyPrint OpBrand
data Instance
indicator in ClassItems and TypeItems
Constructors
Instance
Plain
Instances
ATermConvertible Instance
Show Instance
Eq Instance
PrettyPrint Instance
data ClassItem
Constructors
ClassItem ClassDecl [Annoted BasicItem] [Pos]
Instances
ATermConvertible ClassItem
Show ClassItem
Eq ClassItem
PrettyPrint ClassItem
data ClassDecl
Constructors
ClassDecl [ClassId] Kind [Pos]
Instances
ATermConvertible ClassDecl
Show ClassDecl
Eq ClassDecl
PrettyPrint ClassDecl
data Variance
Constructors
CoVar
ContraVar
InVar
Instances
ATermConvertible Variance
Show Variance
Eq Variance
Ord Variance
PrettyPrint Variance
data Kind
kind or an extended kind
Constructors
Universe [Pos]
MissingKindinitially missing information
Downset (Maybe Token) Type Kind [Pos]plus the derived kind
ClassKind ClassId Kindplus the declared kind
Intersection [Kind] [Pos]with equal raw kinds
FunKind Kind Kind [Pos]only argument may be an ExtKind pos ->
ExtKind Kind Variance [Pos]no InVar pos + or -
Instances
ATermConvertible Kind
Eq Kind
Ord Kind
Show Kind
PosItem Kind
Mergeable Kind
PrettyPrint Kind
star :: Kind
the Universe raw kind
starPlus :: Kind
the ExtKind star CoVar (Type+)
funKind :: Kind
the Kind of the function type
prodKind :: Kind
the Kind of the pair product type
data TypeItem
Constructors
TypeDecl [TypePattern] Kind [Pos]
SubtypeDecl [TypePattern] Type [Pos]
IsoDecl [TypePattern] [Pos]
SubtypeDefn TypePattern Vars Type (Annoted Term) [Pos]
AliasType TypePattern (Maybe Kind) TypeScheme [Pos]
Datatype DatatypeDecl
Instances
ATermConvertible TypeItem
Show TypeItem
Eq TypeItem
PrettyPrint TypeItem
data Vars
a tuple pattern for SubtypeDefn
Constructors
Var Var
VarTuple [Vars] [Pos]
Instances
ATermConvertible Vars
Eq Vars
Show Vars
PosItem Vars
Mergeable Vars
PrettyPrint Vars
data TypePattern
Constructors
TypePattern TypeId [TypeArg] [Pos]
TypePatternToken Token
MixfixTypePattern [TypePattern]
BracketTypePattern BracketKind [TypePattern] [Pos]
TypePatternArg TypeArg [Pos]
Instances
ATermConvertible TypePattern
Show TypePattern
Eq TypePattern
PosItem TypePattern
PrettyPrint TypePattern
data Type
Constructors
TypeName TypeId Kind Int
TypeAppl Type Type
TypeToken Token
BracketType BracketKind [Type] [Pos]
KindedType Type Kind [Pos]
MixfixType [Type]
LazyType Type [Pos]
ProductType [Type] [Pos]
FunType Type Arrow Type [Pos]
Instances
ATermConvertible Type
Eq Type
Ord Type
Show Type
PosItem Type
PrettyPrint Type
Unifiable Type
mkProductType :: [Type] -> [Pos] -> Type
data Arrow
Constructors
FunArr
PFunArr
ContFunArr
PContFunArr
Instances
ATermConvertible Arrow
Show Arrow
Eq Arrow
Ord Arrow
PrettyPrint Arrow
arrowId :: Arrow -> Id
productId :: Id
data Pred
Constructors
IsIn ClassId [Type]
Instances
ATermConvertible Pred
Show Pred
Eq Pred
PrettyPrint Pred
data Qual t
Constructors
(:=>) [Pred] t
Instances
ATermConvertible t => ATermConvertible (Qual t)
Show t => Show (Qual t)
Eq t => Eq (Qual t)
PrettyPrint t => PrettyPrint (Qual t)
data TypeScheme
Constructors
TypeScheme [TypeArg] (Qual Type) [Pos]
Instances
ATermConvertible TypeScheme
Eq TypeScheme
Show TypeScheme
PosItem TypeScheme
PrettyPrint TypeScheme
simpleTypeScheme :: Type -> TypeScheme
logicalType :: Type
predTypeScheme :: TypeScheme -> TypeScheme
predType :: Type -> Type
data Partiality
Constructors
Partial
Total
Instances
ATermConvertible Partiality
Show Partiality
Eq Partiality
PrettyPrint Partiality
data OpItem
Constructors
OpDecl [OpId] TypeScheme [OpAttr] [Pos]
OpDefn OpId [[VarDecl]] TypeScheme Partiality Term [Pos]
Instances
ATermConvertible OpItem
Show OpItem
Eq OpItem
PrettyPrint OpItem
data BinOpAttr
Constructors
Assoc
Comm
Idem
Instances
ATermConvertible BinOpAttr
Show BinOpAttr
Eq BinOpAttr
PrettyPrint BinOpAttr
data OpAttr
Constructors
BinOpAttr BinOpAttr [Pos]
UnitOpAttr Term [Pos]
Instances
ATermConvertible OpAttr
Eq OpAttr
Show OpAttr
Mergeable OpAttr
PrettyPrint OpAttr
data DatatypeDecl
Constructors
DatatypeDecl TypePattern Kind [Annoted Alternative] [ClassId] [Pos]
Instances
ATermConvertible DatatypeDecl
Show DatatypeDecl
Eq DatatypeDecl
PrettyPrint DatatypeDecl
data Alternative
Constructors
Constructor UninstOpId [[Component]] Partiality [Pos]
Subtype [Type] [Pos]
Instances
ATermConvertible Alternative
Eq Alternative
Show Alternative
PrettyPrint Alternative
data Component
Constructors
Selector UninstOpId Partiality Type SeparatorKind Pos
NoSelector Type
Instances
ATermConvertible Component
Eq Component
Show Component
PrettyPrint Component
data Quantifier
Constructors
Universal
Existential
Unique
Instances
ATermConvertible Quantifier
Show Quantifier
Eq Quantifier
PrettyPrint Quantifier
data TypeQual
Constructors
OfType
AsType
InType
Instances
ATermConvertible TypeQual
Show TypeQual
Eq TypeQual
PrettyPrint TypeQual
data LetBrand
Constructors
Let
Where
Instances
ATermConvertible LetBrand
Show LetBrand
Eq LetBrand
data BracketKind
Constructors
Parens
Squares
Braces
Instances
ATermConvertible BracketKind
Show BracketKind
Eq BracketKind
Ord BracketKind
getBrackets :: BracketKind -> (String, String)
data Term
Constructors
QualVar Var Type [Pos]
QualOp OpBrand InstOpId TypeScheme [Pos]
ResolvedMixTerm Id [Term] [Pos]
ApplTerm Term Term [Pos]
TupleTerm [Term] [Pos]
TypedTerm Term TypeQual Type [Pos]
QuantifiedTerm Quantifier [GenVarDecl] Term [Pos]
LambdaTerm [Pattern] Partiality Term [Pos]
CaseTerm Term [ProgEq] [Pos]
LetTerm LetBrand [ProgEq] Term [Pos]
TermToken Token
MixInTerm Type [Pos]
MixfixTerm [Term]
BracketTerm BracketKind [Term] [Pos]
Instances
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
ATermConvertible Term
Eq Term
Show Term
PosItem Term
Typeable Term
Sentences HasCASL Term () Env Morphism Symbol
StaticAnalysis HasCASL BasicSpec Term () SymbItems SymbMapItems Env Morphism Symbol RawSymbol
Logic HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Mergeable Term
PrettyPrint Term
mkTupleTerm :: [Term] -> [Pos] -> Term
data Pattern
Constructors
PatternVar VarDecl
PatternConstr InstOpId TypeScheme [Pos]
ResolvedMixPattern Id [Pattern] [Pos]
ApplPattern Pattern Pattern [Pos]
TuplePattern [Pattern] [Pos]
TypedPattern Pattern Type [Pos]
AsPattern Pattern Pattern [Pos]
PatternToken Token
BracketPattern BracketKind [Pattern] [Pos]
MixfixPattern [Pattern]
Instances
ATermConvertible Pattern
Eq Pattern
Show Pattern
PosItem Pattern
PrettyPrint Pattern
mkTuplePattern :: [Pattern] -> [Pos] -> Pattern
data ProgEq
Constructors
ProgEq Pattern Term Pos
Instances
ATermConvertible ProgEq
Eq ProgEq
Show ProgEq
PrettyPrint ProgEq
data SeparatorKind
Constructors
Comma
Other
Instances
ATermConvertible SeparatorKind
Show SeparatorKind
data VarDecl
Constructors
VarDecl Var Type SeparatorKind [Pos]
Instances
ATermConvertible VarDecl
Eq VarDecl
Show VarDecl
PosItem VarDecl
PrettyPrint VarDecl
data TypeArg
Constructors
TypeArg TypeId Kind SeparatorKind [Pos]
Instances
ATermConvertible TypeArg
Eq TypeArg
Show TypeArg
PosItem TypeArg
PrettyPrint TypeArg
Ord TypeArg
data GenVarDecl
Constructors
GenVarDecl VarDecl
GenTypeVarDecl TypeArg
Instances
ATermConvertible GenVarDecl
Show GenVarDecl
Eq GenVarDecl
PrettyPrint GenVarDecl
data OpId
Constructors
OpId UninstOpId [TypeArg] [Pos]
Instances
ATermConvertible OpId
Show OpId
Eq OpId
PrettyPrint OpId
data InstOpId
Constructors
InstOpId UninstOpId [Type] [Pos]
Instances
ATermConvertible InstOpId
Show InstOpId
Eq InstOpId
PrettyPrint InstOpId
type TypeId = Id
type UninstOpId = Id
type Var = Id
type ClassId = Id
Produced by Haddock version 0.6