AifIO (Averest)

AifIO Module

Namespace: Averest.Systems
Assembly: Averest.dll

writes AIF data structure to a given output stream or file

Functions and values

Function or value	Description
`BL2Lit bl` Full Usage: `BL2Lit bl` Parameters: bl : `bool list` Returns: `string`	bl : `bool list` Returns: `string`
`Bool2Lit b` Full Usage: `Bool2Lit b` Parameters: b : `bool` Returns: `string`	b : `bool` Returns: `string`
`GetRootDir modName pkgName dirName` Full Usage: `GetRootDir modName pkgName dirName` Parameters: modName : `'a` pkgName : `string` dirName : `string` Returns: `string`	determine the root of the library relative to module modName of package pkgName located in directory dirName modName : `'a` pkgName : `string` dirName : `string` Returns: `string`
`ILimit2Lit (strI, midI, endI)` Full Usage: `ILimit2Lit (strI, midI, endI)` Parameters: strI : `bool` midI : `bool` endI : `bool` Returns: `string`	strI : `bool` midI : `bool` endI : `bool` Returns: `string`
`Int2Lit i` Full Usage: `Int2Lit i` Parameters: i : `int` Returns: `string`	i : `int` Returns: `string`
`PrnXMLAIFModule aif` Full Usage: `PrnXMLAIFModule aif` Parameters: aif : `AIFModule` Returns: `PrnDrv -> unit`	aif : `AIFModule` Returns: `PrnDrv -> unit`
`PrnXMLAIFSystem aif` Full Usage: `PrnXMLAIFSystem aif` Parameters: aif : `AIFSystem` Returns: `PrnDrv -> unit`	aif : `AIFSystem` Returns: `PrnDrv -> unit`
`PrnXMLAbbrevTable abbrevs` Full Usage: `PrnXMLAbbrevTable abbrevs` Parameters: abbrevs : `AbbrevTable` Returns: `PrnDrv -> unit`	abbrevs : `AbbrevTable` Returns: `PrnDrv -> unit`
`PrnXMLAbbreviation (dfn, qn)` Full Usage: `PrnXMLAbbreviation (dfn, qn)` Parameters: dfn : `BoolExpr option` qn : `QName` Returns: `PrnDrv -> unit`	dfn : `BoolExpr option` qn : `QName` Returns: `PrnDrv -> unit`
`PrnXMLAbbrevs a` Full Usage: `PrnXMLAbbrevs a` Parameters: a : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`	a : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`
`PrnXMLAbsenceReaction a` Full Usage: `PrnXMLAbsenceReaction a` Parameters: a : `AbsReaction` Returns: `PrnDrv -> unit`	a : `AbsReaction` Returns: `PrnDrv -> unit`
`PrnXMLAbsenceReactions arL` Full Usage: `PrnXMLAbsenceReactions arL` Parameters: arL : `AbsReaction list` Returns: `PrnDrv -> unit`	arL : `AbsReaction list` Returns: `PrnDrv -> unit`
`PrnXMLAccept accept` Full Usage: `PrnXMLAccept accept` Parameters: accept : `SpecExpr` Returns: `PrnDrv -> unit`	accept : `SpecExpr` Returns: `PrnDrv -> unit`
`PrnXMLAction action` Full Usage: `PrnXMLAction action` Parameters: action : `Action` Returns: `PrnDrv -> unit`	action : `Action` Returns: `PrnDrv -> unit`
`PrnXMLArg arg` Full Usage: `PrnXMLArg arg` Parameters: arg : `(Expr * BoolExpr) option` Returns: `PrnDrv -> unit`	arg : `(Expr * BoolExpr) option` Returns: `PrnDrv -> unit`
`PrnXMLArrCase (t1, t2)` Full Usage: `PrnXMLArrCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `ArrExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `ArrExpr` Returns: `PrnDrv -> unit`
`PrnXMLArrExpr arrExpr` Full Usage: `PrnXMLArrExpr arrExpr` Parameters: arrExpr : `ArrExpr` Returns: `PrnDrv -> unit`	arrExpr : `ArrExpr` Returns: `PrnDrv -> unit`
`PrnXMLAssertions a` Full Usage: `PrnXMLAssertions a` Parameters: a : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`	a : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`
`PrnXMLAssumptions asL` Full Usage: `PrnXMLAssumptions asL` Parameters: asL : `QName list` Returns: `PrnDrv -> unit`	asL : `QName list` Returns: `PrnDrv -> unit`
`PrnXMLBoolCase (t1, t2)` Full Usage: `PrnXMLBoolCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BoolExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `BoolExpr` Returns: `PrnDrv -> unit`
`PrnXMLBoolExpr boolExpr` Full Usage: `PrnXMLBoolExpr boolExpr` Parameters: boolExpr : `BoolExpr` Returns: `PrnDrv -> unit`	boolExpr : `BoolExpr` Returns: `PrnDrv -> unit`
`PrnXMLBtvCase (t1, t2)` Full Usage: `PrnXMLBtvCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `BtvExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `BtvExpr` Returns: `PrnDrv -> unit`
`PrnXMLBtvExpr btvExpr` Full Usage: `PrnXMLBtvExpr btvExpr` Parameters: btvExpr : `BtvExpr` Returns: `PrnDrv -> unit`	btvExpr : `BtvExpr` Returns: `PrnDrv -> unit`
`PrnXMLContext c` Full Usage: `PrnXMLContext c` Parameters: c : `CompileContext` Returns: `PrnDrv -> unit`	c : `CompileContext` Returns: `PrnDrv -> unit`
`PrnXMLControlFlow cf` Full Usage: `PrnXMLControlFlow cf` Parameters: cf : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`	cf : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`
`PrnXMLControlledVars cvL` Full Usage: `PrnXMLControlledVars cvL` Parameters: cvL : `QName list` Returns: `PrnDrv -> unit`	cvL : `QName list` Returns: `PrnDrv -> unit`
`PrnXMLDataFlow df` Full Usage: `PrnXMLDataFlow df` Parameters: df : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`	df : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`
`PrnXMLDeclaration (qn, decl)` Full Usage: `PrnXMLDeclaration (qn, decl)` Parameters: qn : `QName` decl : `Decl` Returns: `PrnDrv -> unit`	qn : `QName` decl : `Decl` Returns: `PrnDrv -> unit`
`PrnXMLDepth b` Full Usage: `PrnXMLDepth b` Parameters: b : `Behavior` Returns: `PrnDrv -> unit`	b : `Behavior` Returns: `PrnDrv -> unit`
`PrnXMLDepthCall c` Full Usage: `PrnXMLDepthCall c` Parameters: c : `DepthCall` Returns: `PrnDrv -> unit`	c : `DepthCall` Returns: `PrnDrv -> unit`
`PrnXMLDepthCalls dpthCD` Full Usage: `PrnXMLDepthCalls dpthCD` Parameters: dpthCD : `DepthCall list` Returns: `PrnDrv -> unit`	dpthCD : `DepthCall list` Returns: `PrnDrv -> unit`
`PrnXMLDimension dim` Full Usage: `PrnXMLDimension dim` Parameters: dim : `int` Returns: `PrnDrv -> unit`	dim : `int` Returns: `PrnDrv -> unit`
`PrnXMLDrivers driverL` Full Usage: `PrnXMLDrivers driverL` Parameters: driverL : `SystemPart list` Returns: `PrnDrv -> unit`	driverL : `SystemPart list` Returns: `PrnDrv -> unit`
`PrnXMLExpr expr` Full Usage: `PrnXMLExpr expr` Parameters: expr : `Expr` Returns: `PrnDrv -> unit`	expr : `Expr` Returns: `PrnDrv -> unit`
`PrnXMLFairness fairness` Full Usage: `PrnXMLFairness fairness` Parameters: fairness : `Set<BoolExpr>` Returns: `PrnDrv -> unit`	fairness : `Set<BoolExpr>` Returns: `PrnDrv -> unit`
`PrnXMLFixEq (sign, qn, phi)` Full Usage: `PrnXMLFixEq (sign, qn, phi)` Parameters: sign : `FixSign` qn : `QName` phi : `SpecExpr` Returns: `PrnDrv -> unit`	sign : `FixSign` qn : `QName` phi : `SpecExpr` Returns: `PrnDrv -> unit`
`PrnXMLGrdAction (grd, act)` Full Usage: `PrnXMLGrdAction (grd, act)` Parameters: grd : `BoolExpr` act : `Action` Returns: `PrnDrv -> unit`	grd : `BoolExpr` act : `Action` Returns: `PrnDrv -> unit`
`PrnXMLGrdActionList gaL` Full Usage: `PrnXMLGrdActionList gaL` Parameters: gaL : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`	gaL : `(BoolExpr * Action) list` Returns: `PrnDrv -> unit`
`PrnXMLInitial init` Full Usage: `PrnXMLInitial init` Parameters: init : `BoolExpr` Returns: `PrnDrv -> unit`	init : `BoolExpr` Returns: `PrnDrv -> unit`
`PrnXMLIntCase (t1, t2)` Full Usage: `PrnXMLIntCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `IntExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `IntExpr` Returns: `PrnDrv -> unit`
`PrnXMLIntExpr intExpr` Full Usage: `PrnXMLIntExpr intExpr` Parameters: intExpr : `IntExpr` Returns: `PrnDrv -> unit`	intExpr : `IntExpr` Returns: `PrnDrv -> unit`
`PrnXMLInterface decls` Full Usage: `PrnXMLInterface decls` Parameters: decls : `(QName * Decl) list` Returns: `PrnDrv -> unit`	decls : `(QName * Decl) list` Returns: `PrnDrv -> unit`
`PrnXMLLhsExpr lhsExpr` Full Usage: `PrnXMLLhsExpr lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `PrnDrv -> unit`	lhsExpr : `LhsExpr` Returns: `PrnDrv -> unit`
`PrnXMLLocals decls` Full Usage: `PrnXMLLocals decls` Parameters: decls : `(QName * Decl) list` Returns: `PrnDrv -> unit`	decls : `(QName * Decl) list` Returns: `PrnDrv -> unit`
`PrnXMLNatCase (t1, t2)` Full Usage: `PrnXMLNatCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `NatExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `NatExpr` Returns: `PrnDrv -> unit`
`PrnXMLNatExpr natExpr` Full Usage: `PrnXMLNatExpr natExpr` Parameters: natExpr : `NatExpr` Returns: `PrnDrv -> unit`	natExpr : `NatExpr` Returns: `PrnDrv -> unit`
`PrnXMLProofGoal pg` Full Usage: `PrnXMLProofGoal pg` Parameters: pg : `ProofGoal` Returns: `PrnDrv -> unit`	pg : `ProofGoal` Returns: `PrnDrv -> unit`
`PrnXMLQName qname` Full Usage: `PrnXMLQName qname` Parameters: qname : `QName` Returns: `PrnDrv -> unit`	qname : `QName` Returns: `PrnDrv -> unit`
`PrnXMLQType qtype` Full Usage: `PrnXMLQType qtype` Parameters: qtype : `QType` Returns: `PrnDrv -> unit`	qtype : `QType` Returns: `PrnDrv -> unit`
`PrnXMLRealCase (t1, t2)` Full Usage: `PrnXMLRealCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `RealExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `RealExpr` Returns: `PrnDrv -> unit`
`PrnXMLRealExpr realExpr` Full Usage: `PrnXMLRealExpr realExpr` Parameters: realExpr : `RealExpr` Returns: `PrnDrv -> unit`	realExpr : `RealExpr` Returns: `PrnDrv -> unit`
`PrnXMLSelection (grd, qn)` Full Usage: `PrnXMLSelection (grd, qn)` Parameters: grd : `BoolExpr` qn : `QName` Returns: `PrnDrv -> unit`	grd : `BoolExpr` qn : `QName` Returns: `PrnDrv -> unit`
`PrnXMLSpecExpr specExpr` Full Usage: `PrnXMLSpecExpr specExpr` Parameters: specExpr : `SpecExpr` Returns: `PrnDrv -> unit`	specExpr : `SpecExpr` Returns: `PrnDrv -> unit`
`PrnXMLSpecification spec` Full Usage: `PrnXMLSpecification spec` Parameters: spec : `Specification` Returns: `PrnDrv -> unit`	spec : `Specification` Returns: `PrnDrv -> unit`
`PrnXMLSpecifications specL` Full Usage: `PrnXMLSpecifications specL` Parameters: specL : `Specification list` Returns: `PrnDrv -> unit`	specL : `Specification list` Returns: `PrnDrv -> unit`
`PrnXMLStatevar var` Full Usage: `PrnXMLStatevar var` Parameters: var : `Index` Returns: `PrnDrv -> unit`	var : `Index` Returns: `PrnDrv -> unit`
`PrnXMLStatevars vL` Full Usage: `PrnXMLStatevars vL` Parameters: vL : `int list` Returns: `PrnDrv -> unit`	vL : `int list` Returns: `PrnDrv -> unit`
`PrnXMLSurface b` Full Usage: `PrnXMLSurface b` Parameters: b : `Behavior` Returns: `PrnDrv -> unit`	b : `Behavior` Returns: `PrnDrv -> unit`
`PrnXMLSurfaceCall c` Full Usage: `PrnXMLSurfaceCall c` Parameters: c : `SurfaceCall` Returns: `PrnDrv -> unit`	c : `SurfaceCall` Returns: `PrnDrv -> unit`
`PrnXMLSurfaceCalls surfaceCalls` Full Usage: `PrnXMLSurfaceCalls surfaceCalls` Parameters: surfaceCalls : `SurfaceCall list` Returns: `PrnDrv -> unit`	surfaceCalls : `SurfaceCall list` Returns: `PrnDrv -> unit`
`PrnXMLSystemPart part` Full Usage: `PrnXMLSystemPart part` Parameters: part : `SystemPart` Returns: `PrnDrv -> unit`	part : `SystemPart` Returns: `PrnDrv -> unit`
`PrnXMLSystemPartOption partOption` Full Usage: `PrnXMLSystemPartOption partOption` Parameters: partOption : `SystemPart option` Returns: `PrnDrv -> unit`	partOption : `SystemPart option` Returns: `PrnDrv -> unit`
`PrnXMLTransEq tr` Full Usage: `PrnXMLTransEq tr` Parameters: tr : `TransEqu` Returns: `PrnDrv -> unit`	tr : `TransEqu` Returns: `PrnDrv -> unit`
`PrnXMLTransEqs eqL` Full Usage: `PrnXMLTransEqs eqL` Parameters: eqL : `Set<TransEqu>` Returns: `PrnDrv -> unit`	eqL : `Set<TransEqu>` Returns: `PrnDrv -> unit`
`PrnXMLTransRel trans` Full Usage: `PrnXMLTransRel trans` Parameters: trans : `BoolExpr` Returns: `PrnDrv -> unit`	trans : `BoolExpr` Returns: `PrnDrv -> unit`
`PrnXMLTransfer tf` Full Usage: `PrnXMLTransfer tf` Parameters: tf : `Transfer` Returns: `PrnDrv -> unit`	tf : `Transfer` Returns: `PrnDrv -> unit`
`PrnXMLTransfers transfers` Full Usage: `PrnXMLTransfers transfers` Parameters: transfers : `Transfer list` Returns: `PrnDrv -> unit`	transfers : `Transfer list` Returns: `PrnDrv -> unit`
`PrnXMLTupCase (t1, t2)` Full Usage: `PrnXMLTupCase (t1, t2)` Parameters: t1 : `BoolExpr` t2 : `TupExpr` Returns: `PrnDrv -> unit`	t1 : `BoolExpr` t2 : `TupExpr` Returns: `PrnDrv -> unit`
`PrnXMLTupExpr tupExpr` Full Usage: `PrnXMLTupExpr tupExpr` Parameters: tupExpr : `TupExpr` Returns: `PrnDrv -> unit`	tupExpr : `TupExpr` Returns: `PrnDrv -> unit`
`ReadLibraryModule libRoot qname prefixQNames` Full Usage: `ReadLibraryModule libRoot qname prefixQNames` Parameters: libRoot : `string` qname : `QName` prefixQNames : `Map<QName, Decl> -> QName -> QName` Returns: `AIFModule`	read module from XML file libRoot : `string` qname : `QName` prefixQNames : `Map<QName, Decl> -> QName -> QName` Returns: `AIFModule`
`ReadModule filename prefixQNames` Full Usage: `ReadModule filename prefixQNames` Parameters: filename : `string` prefixQNames : `Map<QName, Decl> -> QName -> QName` Returns: `AIFModule`	read module from XML file filename : `string` prefixQNames : `Map<QName, Decl> -> QName -> QName` Returns: `AIFModule`
`ReadSystem filename` Full Usage: `ReadSystem filename` Parameters: filename : `string` Returns: `AIFSystem`	read system from XML file filename : `string` Returns: `AIFSystem`
`Storage2Lit storage` Full Usage: `Storage2Lit storage` Parameters: storage : `Storage` Returns: `string`	storage : `Storage` Returns: `string`
`VerifTask2Lit task` Full Usage: `VerifTask2Lit task` Parameters: task : `VerifTask` Returns: `string`	task : `VerifTask` Returns: `string`
`WriteModule filename aif` Full Usage: `WriteModule filename aif` Parameters: filename : `string` aif : `AIFModule`	filename : `string` aif : `AIFModule`
`WriteSystem filename aif` Full Usage: `WriteSystem filename aif` Parameters: filename : `string` aif : `AIFSystem`	filename : `string` aif : `AIFSystem`
`curFile` Full Usage: `curFile` Returns: `string ref`	internal name of current input file Returns: `string ref`
`last_token` Full Usage: `last_token` Returns: `token ref`	internal context information for parser errors Returns: `token ref`
`log` Full Usage: `log` Returns: `string -> unit`	Returns: `string -> unit`
`logLevel` Full Usage: `logLevel` Returns: `int -> string -> unit`	Returns: `int -> string -> unit`
`log_token lb` Full Usage: `log_token lb` Parameters: lb : `LexBuffer<char>` Returns: `token`	internal context information for parser errors lb : `LexBuffer<char>` Returns: `token`