fmrisc.ProofNavigator.Communication

Class OpenMath

java.lang.Object

fmrisc.ProofNavigator.Communication.OpenMath

public final class OpenMath
extends java.lang.Object

Conversion of AST objects (excluding declarations) from/to OpenMath representation. Uses the following OM content dictionaries: - sts, arith1, arith2, relation1, logic1, quant1, fns1, set1, setname1, setname2, interval1. Introduces the non-standard content dictionary "fmrisc" with the following symbols (for which no adequate OM CD symbol seems to exist): - if: conditional expression - let: local binding expression - ldecl: local value declaration - array: array quantifier - record: record expression - select: select expression - tuple: tuple expression - update: update expression - arraytype: array type - recordtype: record type - subtype: subtype. - selident: selection identifier. - selindex: selection index. - selnumber: selection number.

Constructor Summary

Constructors

Constructor and Description
OpenMath()

Method Summary

Methods

Modifier and Type	Method and Description
static Expression	toExpression(nl.tue.win.riaca.openmath.lang.OMObject om) Convert OpenMath expression to AST.
static Identifier	toIdentifier(nl.tue.win.riaca.openmath.lang.OMObject om) Convert OpenMath expression to identifier..
static nl.tue.win.riaca.openmath.lang.OMObject	toOpenMath(AST ast) Convert AST to OpenMath object.
static Type	toType(nl.tue.win.riaca.openmath.lang.OMObject om) Convert OpenMath type to AST.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

OpenMath

public OpenMath()

Method Detail

toOpenMath

public static nl.tue.win.riaca.openmath.lang.OMObject toOpenMath(AST ast)

Convert AST to OpenMath object.

Parameters:

ast - the object in AST representation.

Returns:

the OpenMath representation of the object.

toExpression

public static Expression toExpression(nl.tue.win.riaca.openmath.lang.OMObject om)

Convert OpenMath expression to AST.

Parameters:

om - the expression in OpenMath representatin.

Returns:

the expression as an AST (null in case of error).

toType

public static Type toType(nl.tue.win.riaca.openmath.lang.OMObject om)

Convert OpenMath type to AST.

Parameters:

om - the type in OpenMath representatin.

Returns:

the type as an AST (null in case of error).

toIdentifier

public static Identifier toIdentifier(nl.tue.win.riaca.openmath.lang.OMObject om)

Convert OpenMath expression to identifier..

Parameters:

om - the identifier in AST representation.

Returns:

the OpenMath representation of the identifier.