Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder and Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone




parser for HasCASL kinds, types, terms, patterns and equations


key sign tokens

colT :: AParser st Token

a colon not followed by a question mark

parser for bracketed lists

bracketParser :: AParser st a -> AParser st Token -> AParser st Token -> AParser st Token -> ([a] -> Range -> b) -> AParser st b

a generic bracket parser

mkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b

parser for square brackets

mkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b

parser for braces


parseClassId :: AParser st Kind

parse a simple class name or the type universe as kind

parseSimpleKind :: AParser st Kind

do parseClassId or a kind in parenthessis

parseExtKind :: AParser st (Variance, Kind)

do parseSimpleKind and check for an optional Variance

arrowKind :: (Variance, Kind) -> AParser st Kind

parse a (right associative) function kind for a given argument kind

kind :: AParser st Kind

parse a function kind but reject an extended kind

extKind :: AParser st (Variance, Kind)

parse a function kind but accept an extended kind

type variables

typeKind :: Bool -> [(Id, Variance)] -> [Token] -> AParser st [TypeArg]

makeTypeArgs :: [(Id, Variance)] -> [Token] -> Variance -> VarKind -> Range -> [TypeArg]

add the Kind to all extVar and yield a TypeArg

singleTypeArg :: AParser st TypeArg

a single TypeArg (parsed by typeVars)

parenTypeArg :: AParser st (TypeArg, [Token])

a singleTypeArg put in parentheses

typeArg :: AParser st (TypeArg, [Token])

a singleTypeArg possibly put in parentheses

parse special identifier tokens

type TokenMode = [String]

aToken :: TokenMode -> AParser st Token

parse a Token of an Id (to be declared) but exclude the signs in TokenMode

idToken :: AParser st Token

just aToken only excluding basic HasCASL keywords

type patterns

typePatternToken :: AParser st TypePattern

those (top-level) Tokens (less than idToken) that may appear in TypePatterns as TypePatternToken.

primTypePattern :: AParser st TypePattern

a typePatternToken or something in braces (a typePattern), in square brackets (a typePatternOrId covering compound lists) or parenthesis (typePatternArg)

types a parsed type may also be interpreted as a kind (by the mixfix analysis)

typeToken :: AParser st Type

type tokens with some symbols removed

primTypeOrId :: AParser st Type

TypeTokens within BracketTypes may recusively be idTokens. Parenthesis may group a mixfix type or may be interpreted as a kind later on in a GEN-VAR-DECL.

typeOrId :: AParser st Type

several primTypeOrIds possibly yielding a MixfixType and possibly followed by a kindAnno.

kindAnno :: Type -> AParser st Type

a Kind annotation starting with colT.

primType :: AParser st Type

a typeToken' or a BracketType. Square brackets may contain typeOrId.

lazyType :: AParser st Type

a primType possibly preceded by quMarkT

mixType :: AParser st Type

several lazyTypes (as MixfixType) possibly followed by kindAnno

prodType :: AParser st Type

mixType possibly interspersed with crossT

parseType :: AParser st Type

a (right associativ) function type

arrowT :: AParser st Id

parse one of the four possible Arrows

varDecls and genVarDecls

varDecls :: AParser st [VarDecl]

comma separated var with varDeclType

varDeclType :: [Id] -> [Token] -> AParser st [VarDecl]

a type (parseType) following a colon

makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]

attach the Type to every Var

genVarDecls :: AParser st [GenVarDecl]

either like varDecls or declared type variables. A GenVarDecl may later become a GenTypeVarDecl.


tokenPattern :: TokenMode -> AParser st Term

different legal TermTokens possibly excluding funS or equalS for case or let patterns resp.

typedPattern :: TokenMode -> AParser st Term

a possibly typed (parseType) pattern

asPattern :: TokenMode -> AParser st Term

top-level pattern (possibly AsPattern)

pattern :: AParser st Term

an unrestricted asPattern

myChoice :: [(AParser st Token, a)] -> AParser st (a, Token)

lamDot :: AParser st (Partiality, Token)

a Total or Partial lambda dot

lamPattern :: AParser st [Term]

patterns between lamS and lamDot


tToken :: TokenMode -> AParser st Token

Tokens that may occur in Terms including literals scanFloat, scanString but excluding ifS, whenS and elseS to allow a quantifier after whenS. In case-terms also barS will be excluded on the top-level.

data InMode

how the keyword inS should be treated



next inS belongs to letS


inS is the element test

baseTerm :: (InMode, TokenMode) -> AParser st Term

all Terms that start with a unique keyword

whenTerm :: (InMode, TokenMode) -> AParser st Term

whenS possibly followed by an elseS

ifTerm :: (InMode, TokenMode) -> AParser st Term

ifS possibly followed by thenS and elseS yielding a MixfixTerm

termInParens :: AParser st Term

unrestricted terms including qualified names

varTerm :: AParser st Term

a qualified var

qualOpName :: AParser st Term

a qualified operation (with opBrand)

qualPredName :: AParser st Term

a qualified predicate

typeQual :: InMode -> AParser st (TypeQual, Token)

a qualifier expecting a further Type. inS is rejected for NoIn

qualAndType :: InMode -> AParser st Term

a qualifier plus a subsequent type as mixfix term component

typedTerm :: (InMode, TokenMode) -> AParser st Term

a possibly type qualified (typeQual) primTerm or a baseTerm

mixTerm :: (InMode, TokenMode) -> AParser st Term

several typedTerms yielding a MixfixTerm

hasCaslStartKeywords :: [String]

keywords that start a new item

whereTerm :: (InMode, TokenMode) -> AParser st Term

a mixTerm followed by whereS and equations separated by optSemi

term :: AParser st Term

a whereTerm called with (WithIn, [])

exTerm :: (InMode, TokenMode) -> AParser st Term

a (possibly unique) existential QuantifiedTerm

letTerm :: (InMode, TokenMode) -> AParser st Term

a LetTerm with equalS excluded in patternTermPair (called with NoIn)

patternTermPair :: TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq

a customizable pattern equation