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.AsUtils

Description

utility functions and computations of meaningful positions for various data types of the abstract syntax

Synopsis

Documentation

typeUniverseS :: String

the string for the universe type

universeId :: Id

the id of the universe type

universe :: Kind

the type universe

universeWithRange :: Range -> Kind

the type universe

unitTypeS :: String

the name for the Unit type

unitTypeId :: Id

the identifier for the Unit type

redStep :: Type -> Maybe Type

single step beta reduce type abstractions

strippedType :: Type -> Type

eqStrippedType :: Type -> Type -> Bool

getTypeAppl :: Type -> (Type, [Type])

get top-level type constructor and its arguments and beta reduce

getTypeApplAux :: Bool -> Type -> (Type, [Type])

get top-level type constructor and its arguments and beta reduce if True

data Arrow

the builtin function arrows

Constructors

FunArr
PFunArr
ContFunArr
PContFunArr

Instances

Eq Arrow
Ord Arrow
Show Arrow

arrowIdRange :: Range -> Arrow -> Id

arrowId :: Arrow -> Id

construct an infix identifier for a function arrow

isArrow :: Id -> Bool

test for a function identifier

isPartialArrow :: Id -> Bool

test for a partial function identifier

productId :: Int -> Range -> Id

construct a mixfix product identifier with n places

isProductId :: Id -> Bool

test for a product identifier

isProductIdWithArgs :: Id -> Int -> Bool

test for a product identifier

mapKindV :: (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b

map a kind and its variance

mapKind :: (a -> b) -> AnyKind a -> AnyKind b

map a kind and keep variance the same

nonVarRawKind :: RawKind -> RawKind

ignore variances of raw kinds

toRaw :: Kind -> RawKind

compute raw kind (if class ids or no higher kinds)

rStar :: RawKind

the type universe as raw kind

unitType :: Type

the Unit type (name)

unitTypeWithRange :: Range -> Type

the Unit type (name)

lazyTypeId :: Id

the prefix name for lazy types

coKind :: Kind

the kind of the lazy type constructor

lazyTypeConstr :: Type

the lazy type constructor

mkLazyType :: Type -> Type

make a type lazy

mkFunArrType :: Type -> Arrow -> Type -> Type

function type

mkFunArrTypeWithRange :: Range -> Type -> Arrow -> Type -> Type

mkProductType :: [Type] -> Type

construct a product type

mkProductTypeWithRange :: [Type] -> Range -> Type

construct a product type

simpleTypeScheme :: Type -> TypeScheme

convert a type with unbound variables to a scheme

predType :: Range -> Type -> Type

add the unit type as result type or convert a parsed empty tuple to the unit type

predTypeScheme :: Range -> TypeScheme -> TypeScheme

change the type of the scheme to a predType

unPredType :: Type -> (Bool, Type)

check for and remove predicate arrow

isPredType :: Type -> Bool

test if type is a predicate type

unPredTypeScheme :: TypeScheme -> TypeScheme

remove predicate arrow in a type scheme

funKindWithRange3 :: Range -> Kind -> Kind -> Kind -> Kind

funKind3 :: Kind -> Kind -> Kind -> Kind

funKindWithRange :: Range -> Kind

funKind :: Kind

the kind of the function type

mkFunKind :: Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a

construct higher order kind from arguments and result kind

prodKind1 :: Int -> Range -> Kind -> Kind

the Kind of the product type

prodKind :: Int -> Range -> Kind

toType :: Id -> Type

a type name with a universe kind

toFunTypeRange :: Range -> Arrow -> Type

toFunType :: Arrow -> Type

the type name for a function arrow

toProdType :: Int -> Range -> Type

the type name for a function arrow

mkBracketToken :: BracketKind -> Range -> [Token]

the brackets as tokens with positions

mkTupleTerm :: [Term] -> Range -> Term

construct a tuple from non-singleton lists

getTupleArgs :: Term -> Maybe [Term]

try to extract tuple arguments

getAppl :: Term -> Maybe (Id, TypeScheme, [Term])

decompose an ApplTerm into an application of an operation and a list of arguments

splitVars :: [GenVarDecl] -> ([VarDecl], [TypeArg])

split the list of generic variables into values and type variables

extractVars :: Term -> [VarDecl]

extract bindings from an analysed pattern

mkOpTerm :: Id -> TypeScheme -> Term

construct term from id

mkForall :: [GenVarDecl] -> Term -> Term

bind a term

mkApplTerm :: Term -> [Term] -> Term

construct application with curried arguments

addPartiality :: [a] -> Type -> Type

make function arrow partial after some arguments

typeArgToType :: TypeArg -> Type

convert a type argument to a type

patToType :: Id -> [TypeArg] -> RawKind -> Type

convert a parameterized type identifier with a result raw kind to a type application

typeArgsListToRawKind :: [TypeArg] -> RawKind -> RawKind

create the (raw if True) kind from type arguments

typeArgsListToKind :: [TypeArg] -> Kind -> Kind

create the kind from type arguments

getFunType :: Type -> Partiality -> [Type] -> Type

get the type of a constructor with given curried argument types

getSelType :: Type -> Partiality -> Type -> Type

get the type of a selector given the data type as first arguemnt

nonVarTypeArg :: TypeArg -> TypeArg

make type argument non-variant

getTypeVar :: TypeArg -> Id

get the type variable

mkTypeAppl :: Type -> [Type] -> Type

construct application left-associative

toKind :: VarKind -> Kind

get the kind of an analyzed type variable

reparseAsId :: Pretty a => a -> Maybe Id

try to reparse the pretty printed input as an identifier

expected :: Pretty a => a -> a -> String

generate a comparison string