Scalarizer (Averest)

Scalarizer Module

Namespace: Averest.Transform
Assembly: Averest.dll

Eliminate compound data types (arrays and tuples). - expressions of type (Qtup tyL) are reduced to TupOfExprL[e1,...,en] - select expressions only have constant indices After the reduction, array access and tuple access can be also transformed to new variable names, which is needed to completely eliminate the types from the system description. There are two different algorithms for the expansion of compound types on left-hand sides: The first way makes case distinctions on the index expressions by enumerating the possible indices. The second approach enumerates the possible letues of the variables that occur in the index expressions, which is more efficient, since the knowledge that some variables are fixed to a certain constant is propagated by the substitution(instead of repeating useless case distinctions).

Functions and values

Function or value	Description
`EliminateCompound` Full Usage: `EliminateCompound` Returns: `SystemTrans`	Returns: `SystemTrans`
`PresetCompoundReads` Full Usage: `PresetCompoundReads` Returns: `SystemTrans`	Returns: `SystemTrans`
`PresetCompoundReadsInSpecifications` Full Usage: `PresetCompoundReadsInSpecifications` Returns: `SystemTrans`	Returns: `SystemTrans`
`PresetCompoundReadsInSystemPart` Full Usage: `PresetCompoundReadsInSystemPart` Returns: `SystemPartTrans`	Returns: `SystemPartTrans`
`PresetCompoundWrites` Full Usage: `PresetCompoundWrites` Returns: `SystemTrans`	Returns: `SystemTrans`
`PresetCompoundWritesInSystemPart` Full Usage: `PresetCompoundWritesInSystemPart` Returns: `SystemPartTrans`	Returns: `SystemPartTrans`
`Scalarize` Full Usage: `Scalarize` Returns: `SystemTrans`	scalarize Returns: `SystemTrans`
`elimArrExpr expr` Full Usage: `elimArrExpr expr` Parameters: expr : `'a` Returns: `'b`	expr : `'a` Returns: `'b`
`elimBoolExpr boolMap boolExpr` Full Usage: `elimBoolExpr boolMap boolExpr` Parameters: boolMap : `Map<BoolExpr, 'a>` boolExpr : `BoolExpr` Returns: `'a option`	boolMap : `Map<BoolExpr, 'a>` boolExpr : `BoolExpr` Returns: `'a option`
`elimBtvExpr btvMap btvExpr` Full Usage: `elimBtvExpr btvMap btvExpr` Parameters: btvMap : `Map<BtvExpr, 'a>` btvExpr : `BtvExpr` Returns: `'a option`	btvMap : `Map<BtvExpr, 'a>` btvExpr : `BtvExpr` Returns: `'a option`
`elimDecl (qn, decl)` Full Usage: `elimDecl (qn, decl)` Parameters: qn : `QName` decl : `Decl` Returns: `(QName * Decl) list`	qn : `QName` decl : `Decl` Returns: `(QName * Decl) list`
`elimEquations iface` Full Usage: `elimEquations iface` Parameters: iface : `(QName * Decl) list` Returns: `(LhsExpr * LhsExpr) list`	iface : `(QName * Decl) list` Returns: `(LhsExpr * LhsExpr) list`
`elimIntExpr intMap intExpr` Full Usage: `elimIntExpr intMap intExpr` Parameters: intMap : `Map<IntExpr, 'a>` intExpr : `IntExpr` Returns: `'a option`	intMap : `Map<IntExpr, 'a>` intExpr : `IntExpr` Returns: `'a option`
`elimLhsExpr lhsMap lhsExpr` Full Usage: `elimLhsExpr lhsMap lhsExpr` Parameters: lhsMap : `Map<LhsExpr, 'a>` lhsExpr : `LhsExpr` Returns: `'a option`	lhsMap : `Map<LhsExpr, 'a>` lhsExpr : `LhsExpr` Returns: `'a option`
`elimMapping lhsL` Full Usage: `elimMapping lhsL` Parameters: lhsL : `(LhsExpr * LhsExpr) list` Returns: `ExprMapping`	lhsL : `(LhsExpr * LhsExpr) list` Returns: `ExprMapping`
`elimNatExpr natMap natExpr` Full Usage: `elimNatExpr natMap natExpr` Parameters: natMap : `Map<NatExpr, 'a>` natExpr : `NatExpr` Returns: `'a option`	natMap : `Map<NatExpr, 'a>` natExpr : `NatExpr` Returns: `'a option`
`elimRealExpr realMap realExpr` Full Usage: `elimRealExpr realMap realExpr` Parameters: realMap : `Map<RealExpr, 'a>` realExpr : `RealExpr` Returns: `'a option`	realMap : `Map<RealExpr, 'a>` realExpr : `RealExpr` Returns: `'a option`
`elimTupExpr expr` Full Usage: `elimTupExpr expr` Parameters: expr : `'a` Returns: `'b`	expr : `'a` Returns: `'b`
`isBool (arg1, e)` Full Usage: `isBool (arg1, e)` Parameters: arg0 : `'a` e : `LhsExpr` Returns: `bool`	arg0 : `'a` e : `LhsExpr` Returns: `bool`
`isBtv (arg1, e)` Full Usage: `isBtv (arg1, e)` Parameters: arg0 : `'a` e : `LhsExpr` Returns: `bool`	arg0 : `'a` e : `LhsExpr` Returns: `bool`
`isInt (arg1, e)` Full Usage: `isInt (arg1, e)` Parameters: arg0 : `'a` e : `LhsExpr` Returns: `bool`	arg0 : `'a` e : `LhsExpr` Returns: `bool`
`isNat (arg1, e)` Full Usage: `isNat (arg1, e)` Parameters: arg0 : `'a` e : `LhsExpr` Returns: `bool`	arg0 : `'a` e : `LhsExpr` Returns: `bool`
`isReal (arg1, e)` Full Usage: `isReal (arg1, e)` Parameters: arg0 : `'a` e : `LhsExpr` Returns: `bool`	arg0 : `'a` e : `LhsExpr` Returns: `bool`
`scalarizedCell cell` Full Usage: `scalarizedCell cell` Parameters: cell : `LhsExpr` Returns: `LhsExpr`	cell : `LhsExpr` Returns: `LhsExpr`
`splayArrWrite (grd, act)` Full Usage: `splayArrWrite (grd, act)` Parameters: grd : `BoolExpr` act : `Action` Returns: `(BoolExpr * Action) list`	grd : `BoolExpr` act : `Action` Returns: `(BoolExpr * Action) list`
`toBool (lhs, lhs')` Full Usage: `toBool (lhs, lhs')` Parameters: lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `BoolExpr * BoolExpr`	lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `BoolExpr * BoolExpr`
`toBtv (lhs, lhs')` Full Usage: `toBtv (lhs, lhs')` Parameters: lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `BtvExpr * BtvExpr`	lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `BtvExpr * BtvExpr`
`toInt (lhs, lhs')` Full Usage: `toInt (lhs, lhs')` Parameters: lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `IntExpr * IntExpr`	lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `IntExpr * IntExpr`
`toNat (lhs, lhs')` Full Usage: `toNat (lhs, lhs')` Parameters: lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `NatExpr * NatExpr`	lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `NatExpr * NatExpr`
`toReal (lhs, lhs')` Full Usage: `toReal (lhs, lhs')` Parameters: lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `RealExpr * RealExpr`	lhs : `LhsExpr` lhs' : `LhsExpr` Returns: `RealExpr * RealExpr`