Copyright	(c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Ewaryst.Schulz@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred

CSL.AS_BASIC_CSL

Description

This module contains the abstract syntax types for EnCL as well as the predefined operator configuration.

Synopsis

Documentation

data EXPRESSION

Datatype for expressions

Constructors

Var Token
Op OPID [EXTPARAM] [EXPRESSION] Range
List [EXPRESSION] Range
Interval Double Double Range
Int APInt Range
Rat APFloat Range

Instances

Eq EXPRESSION
Data EXPRESSION
Ord EXPRESSION
Show EXPRESSION
ShATermConvertible EXPRESSION
GetRange EXPRESSION
Pretty EXPRESSION
Typeable * EXPRESSION
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

data EXTPARAM

Extended Parameter Datatype

Constructors

EP Token String APInt

Instances

Eq EXTPARAM
Data EXTPARAM
Ord EXTPARAM
Show EXTPARAM
ShATermConvertible EXTPARAM
Pretty EXTPARAM
Typeable * EXTPARAM

data BASIC_ITEM

basic items: an operator, extended parameter or variable declaration or an axiom

Constructors

Op_decl OP_ITEM
EP_decl [(Token, EPDomain)]
EP_domdecl [(Token, APInt)]
EP_defval [(Token, APInt)]
Var_decls [VAR_ITEM]
Axiom_item (Annoted CMD)

Instances

Data BASIC_ITEM
Show BASIC_ITEM
ShATermConvertible BASIC_ITEM
GetRange BASIC_ITEM
Pretty BASIC_ITEM
Typeable * BASIC_ITEM

newtype BASIC_SPEC

Constructors

Basic_spec [Annoted BASIC_ITEM]

Instances

Data BASIC_SPEC
Show BASIC_SPEC
ShATermConvertible BASIC_SPEC
Monoid BASIC_SPEC
GetRange BASIC_SPEC
Pretty BASIC_SPEC
Typeable * BASIC_SPEC
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS	Syntax of CSL logic
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for reduce logic
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

data SYMB_ITEMS

symbol lists for hiding

Constructors

Symb_items [SYMB] Range

Instances

Eq SYMB_ITEMS
Data SYMB_ITEMS
Show SYMB_ITEMS
ShATermConvertible SYMB_ITEMS
GetRange SYMB_ITEMS
Pretty SYMB_ITEMS
Typeable * SYMB_ITEMS
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS	Syntax of CSL logic
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for reduce logic
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

newtype SYMB

symbol for identifiers

Constructors

Symb_id Token

Instances

Eq SYMB
Data SYMB
Show SYMB
ShATermConvertible SYMB
GetRange SYMB
Pretty SYMB
Typeable * SYMB

data SYMB_MAP_ITEMS

symbol maps for renamings

Constructors

Symb_map_items [SYMB_OR_MAP] Range

Instances

Eq SYMB_MAP_ITEMS
Data SYMB_MAP_ITEMS
Show SYMB_MAP_ITEMS
ShATermConvertible SYMB_MAP_ITEMS
GetRange SYMB_MAP_ITEMS
Pretty SYMB_MAP_ITEMS
Typeable * SYMB_MAP_ITEMS
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS	Syntax of CSL logic
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for reduce logic
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

data SYMB_OR_MAP

symbol map or renaming (renaming then denotes the identity renaming)

Constructors

Symb SYMB
Symb_map SYMB SYMB Range

Instances

Eq SYMB_OR_MAP
Data SYMB_OR_MAP
Show SYMB_OR_MAP
ShATermConvertible SYMB_OR_MAP
GetRange SYMB_OR_MAP
Pretty SYMB_OR_MAP
Typeable * SYMB_OR_MAP

data OPNAME

Instances

Eq OPNAME
Data OPNAME
Ord OPNAME
Show OPNAME
ShATermConvertible OPNAME
Typeable * OPNAME
ExpressionPrinter (Reader OpInfoNameMap)	An `OpInfoNameMap` can be interpreted as an `ExpressionPrinter`

data OPID

Constructors

OpId OPNAME
OpUser ConstantName

Instances

Eq OPID
Data OPID
Ord OPID
Show OPID
ShATermConvertible OPID
Pretty OPID
Typeable * OPID

data ConstantName

We differentiate between simple constant names and indexed constant names resulting from the extended parameter elimination.

Constructors

SimpleConstant String
ElimConstant String Int

Instances

Eq ConstantName
Data ConstantName
Ord ConstantName
Show ConstantName
ShATermConvertible ConstantName
Pretty ConstantName
Typeable * ConstantName

data OP_ITEM

operator symbol declaration

Constructors

Op_item [Token] Range

Instances

Data OP_ITEM
Show OP_ITEM
ShATermConvertible OP_ITEM
GetRange OP_ITEM
Pretty OP_ITEM
Typeable * OP_ITEM

data VAR_ITEM

variable symbol declaration

Constructors

Var_item [Token] Domain Range

Instances

Data VAR_ITEM
Show VAR_ITEM
ShATermConvertible VAR_ITEM
GetRange VAR_ITEM
Pretty VAR_ITEM
Typeable * VAR_ITEM

data VarDecl

Constructors

VarDecl Token (Maybe Domain)

Instances

Eq VarDecl
Data VarDecl
Ord VarDecl
Show VarDecl
ShATermConvertible VarDecl
Pretty VarDecl
Typeable * VarDecl

data OpDecl

Constructors

OpDecl ConstantName [EXTPARAM] [VarDecl] Range

Instances

Eq OpDecl
Data OpDecl
Ord OpDecl
Show OpDecl
ShATermConvertible OpDecl
Pretty OpDecl
Typeable * OpDecl

data EPDecl

Constructors

EPDecl Token EPDomain (Maybe APInt)

Instances

Eq EPDecl
Data EPDecl
Ord EPDecl
Show EPDecl
ShATermConvertible EPDecl
Pretty EPDecl
Typeable * EPDecl

data EPVal

Extended Parameter value may be an integer or a reference to an EPDomVal. This type is used for the domain specification of EPs (see EPDomain).

Constructors

EPVal APInt
EPConstRef Token

Instances

Eq EPVal
Data EPVal
Ord EPVal
Show EPVal
ShATermConvertible EPVal
Pretty EPVal
Typeable * EPVal

getEPVarRef :: EPVal -> Maybe Token

type Domain = SetOrInterval GroundConstant

type EPDomain = ClosedInterval EPVal

data GroundConstant

Constructors

GCI APInt
GCR APFloat

Instances

Eq GroundConstant
Data GroundConstant
Ord GroundConstant
Show GroundConstant
ShATermConvertible GroundConstant
Continuous GroundConstant
Pretty GroundConstant
Typeable * GroundConstant

cmpFloatToInt :: APFloat -> APInt -> Ordering

data AssDefinition

A constant or function definition

Constructors

ConstDef EXPRESSION
FunDef [String] EXPRESSION

Instances

Eq AssDefinition
Data AssDefinition
Ord AssDefinition
Show AssDefinition
ShATermConvertible AssDefinition
Pretty AssDefinition
Typeable * AssDefinition

data CMD

Constructors

Ass OpDecl EXPRESSION
Cmd String [EXPRESSION]
Sequence [CMD]
Cond [(EXPRESSION, [CMD])]
Repeat EXPRESSION [CMD]

Instances

Eq CMD
Data CMD
Ord CMD
Show CMD
ShATermConvertible CMD
GetRange CMD
Pretty CMD
Typeable * CMD
Sentences CSL CMD Sign Morphism Symbol	Instance of Sentences for reduce logic
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for reduce logic
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

class OperatorState a where

Minimal complete definition

lookupOperator, lookupBinder

Methods

addVar :: a -> String -> a

isVar :: a -> String -> Bool

lookupOperator

Arguments

:: a
-> String	operator name
-> Int	operator arity
-> Either Bool OpInfo

lookupBinder

Arguments

:: a
-> String	binder name
-> Maybe OpInfo

Instances

OperatorState ()
OperatorState (AnnoState st)
OperatorState a => OperatorState (OpVarState a)
OperatorState (OpInfoMap, BindInfoMap)

data OpInfo

Constructors

OpInfo
Fields prec :: Int precedence between 0 and maxPrecedence infx :: Bool True = infix arity :: Int the operator arity foldNAry :: Bool True = fold nary-applications during construction into binary ones opname :: OPNAME The actual operator name bind :: Maybe BindInfo More info for binders

Instances

Eq OpInfo
Data OpInfo
Ord OpInfo
Show OpInfo
ShATermConvertible OpInfo
Typeable * OpInfo
ExpressionPrinter (Reader OpInfoNameMap)	An `OpInfoNameMap` can be interpreted as an `ExpressionPrinter`
OperatorState (OpInfoMap, BindInfoMap)

data BindInfo

Constructors

BindInfo
Fields bindingVarPos :: [Int] argument positions of binding variables boundBodyPos :: [Int] argument positions of bound terms

Instances

Eq BindInfo
Data BindInfo
Ord BindInfo
Show BindInfo
ShATermConvertible BindInfo
Typeable * BindInfo

operatorInfo :: [OpInfo]

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

operatorInfoMap :: OpInfoMap

opInfoMap for the predefined operatorInfo

operatorInfoNameMap :: OpInfoNameMap

opInfoNameMap for the predefined operatorInfo

operatorBindInfoMap :: BindInfoMap

mergeOpArityMap :: Ord a => OpInfoArityMap a -> OpInfoArityMap a -> OpInfoArityMap a

Merges two OpInfoArityMaps together with the first map as default map and the second overwriting the default values

getOpInfoMap :: (OpInfo -> String) -> [OpInfo] -> OpInfoMap

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

getOpInfoNameMap :: [OpInfo] -> OpInfoNameMap

Same as operatorInfoMap but with keys of type OPNAME instead of String

getBindInfoMap :: [OpInfo] -> BindInfoMap

a special map for binders which have to be unique for each name (no different arities).

lookupOpInfo

Arguments

:: OpInfoNameMap
-> OPID	operator id
-> Int	operator arity
-> Either Bool OpInfo

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True.

lookupOpInfoForParsing

Arguments

:: OpInfoMap	map to be used for lookup
-> String	operator name
-> Int	operator arity
-> Either Bool OpInfo

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True. This function is designed for the lookup of operators in not statically analyzed terms. For statically analyzed terms use lookupOpInfo.

lookupBindInfo

Arguments

:: OpInfoNameMap
-> OPID	operator name
-> Int	operator arity
-> Maybe BindInfo

For the given name and arity we lookup an BindInfo, where arity=-1 means flexible arity.

type APInt = Integer

type APFloat = Rational

toFraction :: APFloat -> (Integer, Integer)

fromFraction :: Integer -> Integer -> APFloat

type OpInfoMap = OpInfoArityMap String

type OpInfoNameMap = OpInfoArityMap OPNAME

type BindInfoMap = Map String OpInfo

showOPNAME :: OPNAME -> String

maxPrecedence :: Int

OP_mult
OP_div
OP_plus
OP_minus
OP_neg
OP_pow
OP_fthrt
OP_sqrt
OP_abs
OP_max
OP_min
OP_sign
OP_cos
OP_sin
OP_tan
OP_cot
OP_Pi
OP_reldist
OP_minimize
OP_minloc
OP_maximize
OP_maxloc
OP_factor
OP_approx
OP_divide
OP_factorize
OP_int
OP_rlqe
OP_simplify
OP_solve
OP_neq
OP_lt
OP_leq
OP_eq
OP_gt
OP_geq
OP_convergence
OP_reldistLe
OP_in
OP_undef
OP_failure
OP_false
OP_true
OP_not
OP_and
OP_or
OP_impl
OP_ex
OP_all
OP_hastype
OP_real

Eq InstantiatedConstant
Data InstantiatedConstant
Ord InstantiatedConstant
Show InstantiatedConstant
ShATermConvertible InstantiatedConstant
Pretty InstantiatedConstant
Typeable * InstantiatedConstant

InstantiatedConstant
Fields constName :: ConstantName instantiation :: [EXPRESSION]