| Copyright | (c) Christian Maeder and Uni Bremen 2003-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
HasCASL.As
Contents
Description
abstract syntax for HasCASL, more liberal than Concrete-Syntax.txt, annotations are almost as for CASL
- data BasicSpec = BasicSpec [Annoted BasicItem]
- data BasicItem
- data SigItems
- data OpBrand
- isPred :: OpBrand -> Bool
- data Instance
- data ClassItem = ClassItem ClassDecl [Annoted BasicItem] Range
- data ClassDecl = ClassDecl [Id] Kind Range
- data Variance
- data AnyKind a
- type Kind = AnyKind Id
- type RawKind = AnyKind ()
- data TypeItem
- data Vars
- data TypePattern
- data Type
- mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme
- data TypeScheme = TypeScheme [TypeArg] Type Range
- data Partiality
- data OpItem
- data BinOpAttr
- data OpAttr
- data DatatypeDecl = DatatypeDecl TypePattern Kind [Annoted Alternative] [Id] Range
- data Alternative
- = Constructor Id [[Component]] Partiality Range
- | Subtype [Type] Range
- data Component
- data Quantifier
- data TypeQual
- data LetBrand
- data BracketKind
- = Parens
- | Squares
- | Braces
- | NoBrackets
- getBrackets :: BracketKind -> (String, String)
- data InstKind
- data Term
- = QualVar VarDecl
- | QualOp OpBrand PolyId TypeScheme [Type] InstKind Range
- | ApplTerm Term Term Range
- | TupleTerm [Term] Range
- | TypedTerm Term TypeQual Type Range
- | AsPattern VarDecl Term Range
- | QuantifiedTerm Quantifier [GenVarDecl] Term Range
- | LambdaTerm [Term] Partiality Term Range
- | CaseTerm Term [ProgEq] Range
- | LetTerm LetBrand [ProgEq] Term Range
- | ResolvedMixTerm Id [Type] [Term] Range
- | TermToken Token
- | MixTypeTerm TypeQual Type Range
- | MixfixTerm [Term]
- | BracketTerm BracketKind [Term] Range
- data ProgEq = ProgEq Term Term Range
- data PolyId = PolyId Id [TypeArg] Range
- data SeparatorKind
- data VarDecl = VarDecl Id Type SeparatorKind Range
- data VarKind
- data TypeArg = TypeArg Id Variance VarKind RawKind Int SeparatorKind Range
- data GenVarDecl
- data SymbItems = SymbItems SymbKind [Symb] [Annotation] Range
- data SymbMapItems = SymbMapItems SymbKind [SymbOrMap] [Annotation] Range
- data SymbKind
- data Symb = Symb Id (Maybe SymbType) Range
- data SymbType = SymbType TypeScheme
- data SymbOrMap = SymbOrMap Symb (Maybe Symb) Range
- bestRange :: GetRange a => [a] -> Range -> Range
abstract syntax entities with small utility functions
data BasicSpec
annotated basic items
Instances
data BasicItem
the possible items
data SigItems
signature items are types or functions
data OpBrand
indicator for predicate, operation or function
data Instance
indicator in ClassItems and TypeItems
data ClassItem
a class item
data ClassDecl
declaring class identifiers
data Variance
co- or contra- variance indicator
data AnyKind a
(higher) kinds
data TypeItem
the possible type items
data Vars
a tuple pattern for SubtypeDefn
data TypePattern
the lhs of most type items
data Type
types based on variable or constructor names and applications
mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme
change the type within a scheme
data TypeScheme
a type with bound type variables. The bound variables within the scheme should have negative numbers in the order given by the type argument list. The type arguments store proper kinds (including downsets) whereas the kind within the type names are only raw kinds.
Constructors
| TypeScheme [TypeArg] Type Range |
data Partiality
indicator for partial or total functions
data OpItem
function declarations or definitions
data BinOpAttr
attributes without arguments for binary functions
data OpAttr
possible function attributes (including a term as a unit element)
data DatatypeDecl
a polymorphic data type declaration with a deriving clause
Constructors
| DatatypeDecl TypePattern Kind [Annoted Alternative] [Id] Range |
data Alternative
Alternatives are subtypes or a constructor with a list of (curried) tuples as arguments. Only the components of the first tuple can be addressed by the places of the mixfix constructor.
Constructors
| Constructor Id [[Component]] Partiality Range | |
| Subtype [Type] Range |
data Component
A component is a type with on optional (only pre- or postfix) selector function.
Constructors
| Selector Id Partiality Type SeparatorKind Range | |
| NoSelector Type |
data TypeQual
the possibly type annotations of terms
data LetBrand
an indicator of (otherwise equivalent) let or where equations
data BracketKind
the possible kinds of brackets (that should match when parsed)
Constructors
| Parens | |
| Squares | |
| Braces | |
| NoBrackets |
getBrackets :: BracketKind -> (String, String)
the brackets as strings for printing
data InstKind
data Term
The possible terms and patterns. Formulas are also kept as
terms. Local variables and constants are kept separatetly. The variant
ResolvedMixTerm is an intermediate representation for type checking
only.
Constructors
data ProgEq
an equation or a case as pair of a pattern and a term
data PolyId
an identifier with an optional list of type declarations
data SeparatorKind
an indicator if variables were separated by commas or by separate declarations
data VarKind
the kind of a type variable (or a type argument in schemes)
Constructors
| VarKind Kind | |
| Downset Type | |
| MissingKind |
data TypeArg
a (simple) type variable with its kind (or supertype)
symbol data types symbols
data SymbItems
Constructors
| SymbItems SymbKind [Symb] [Annotation] Range |
Instances
data SymbMapItems
mapped symbols
Constructors
| SymbMapItems SymbKind [SymbOrMap] [Annotation] Range |
Instances
data SymbKind
kind of symbols
data Symb
type annotated symbols
data SymbOrMap
mapped symbol