fmrisc.Syntax
Class Construct

java.lang.Object
  fmrisc.Syntax.Construct

public final class Construct
extends java.lang.Object

Construct abstract syntax trees.

Constructor Summary

Construct()

Method Summary

static AndFormula	andFormula(Expression base1, Expression base2) construct conjunction with components base1 and base2
static ApplicationExpression	applicationExpression(Expression base1, Expression[] base2) construct application of base1 to base2
static ArrayTerm	arrayTerm(TypedIdentifier[] variables, Expression base) construct array term of variables and base term
static ArrayType	arrayType(Type index, Type base) construct array type with denoted index type and base type.
static AtomicType	atomicType(java.lang.String name) construct atomic type with denoted name.
static AxiomDeclaration	axiomDeclaration(FormulaDeclIdentifier name, Expression formula) construct axiom declaration with denoted name and formula
static DividesTerm	dividesTerm(Expression base1, Expression base2) construct quotient with components base1 and base2
static EqualsFormula	equalsFormula(Expression base1, Expression base2) construct equality with components base1 and base2
static EquivalentFormula	equivalentFormula(Expression base1, Expression base2) construct equivalence with components base1 and base2
static ExistsFormula	existsFormula(TypedIdentifier[] variables, Expression base) construct existentially quantifed formula of variables and base formula
static ForallFormula	forallFormula(TypedIdentifier[] variables, Expression base) construct universally quantifed formula of variables and base formula
static FormulaDeclaration	formulaDeclaration(FormulaDeclIdentifier name, Expression formula) construct formula declaration with denoted name and formula.
static FormulaDeclIdentifier	formulaDeclIdentifier(java.lang.String name) construct formula declaration identifier with denoted name.
static FunctionType	functionType(Type[] domain, Type range) construct function type from types domain and range.
static GreaterEqualFormula	greaterEqualFormula(Expression base1, Expression base2) construct greater-than-or-equal formula with components base1 and base2
static GreaterFormula	greaterFormula(Expression base1, Expression base2) construct greater-than formula with components base1 and base2
static IfThenElseExpression	ifThenElseExpression(Expression condition, Expression thenbranch, Expression elsebranch) construct if-then-else expressions from condition, thenbranch, elsebranch.
static ImpliesFormula	impliesFormula(Expression base1, Expression base2) construct implication with components base1 and base2
static LambdaTerm	lambdaTerm(TypedIdentifier[] variables, Expression base) construct lambda term of variables and base term
static LessEqualFormula	lessEqualFormula(Expression base1, Expression base2) construct less-than-or-equal formula with components base1 and base2
static LessFormula	lessFormula(Expression base1, Expression base2) construct less-than formula with components base1 and base2
static LetExpression	letExpression(ValueDeclaration[] declarations, Expression base) construct let expressions of declarations and base expressions
static LetType	letType(TypeDeclaration[] declarations, Type base) construct let type of declarations and base type
static Logical	logical(boolean value) construct logical constant with denoted value.
static MinusTerm	minusTerm(Expression base1, Expression base2) construct difference with components base1 and base2
static NegationTerm	negationTerm(Expression base) construct negation (minus term) of base term
static NotEqualsFormula	notEqualsFormula(Expression base1, Expression base2) construct inequality with components base1 and base2
static NotEquivalentFormula	notEquivalentFormula(Expression base1, Expression base2) construct exclusive disjunction with components base1 and base2
static NotFormula	notFormula(Expression base) construct negation (not formula) of base formula
static Number	number(java.lang.String value) construct number with denoted value.
static OrFormula	orFormula(Expression base1, Expression base2) construct disjunction with components base1 and base2
static PlusTerm	plusTerm(Expression base1, Expression base2) construct binary sum with components base1 and base2
static PowerTerm	powerTerm(Expression base1, Expression base2) construct power term with components base1 and base2
static RecordTerm	recordTerm(ValuedIdentifier[] base) construct record term of base terms
static RecordType	recordType(TypedIdentifier[] base) construct record type with denoted base types.
static Reference	reference(java.lang.String name) construct referenc with denoted name.
static Reference	reference(Symbol symbol) Construct referenc from symbol.
static Reference	reference(TypeDeclIdentifier ident) construct reference from type declaration identifier.
static Reference	reference(ValueDeclIdentifier ident) construct reference from value declaration identifier.
static SelectionTerm	selectionTerm(Expression base1, Selector base2) construct component selection from base1 and base2
static SelectorIdentifier	selectorIdentifier(Reference base) make selector from identifier base
static SelectorIndex	selectorIndex(Expression base) make selector from index expression base
static SelectorNumber	selectorNumber(Number base) make selector from number base
static SubrangeType	subrangeType(Expression from, Expression to) construct subrangetype with denoted bounds.
static SubType	subType(Expression predicate) construct subtype with denoted predicate.
static TimesTerm	timesTerm(Expression base1, Expression base2) construct binary product with components base1 and base2
static TupleTerm	tupleTerm(Expression[] base) construct tuple term of base terms
static TupleType	tupleType(Type[] base) construct tuple type with denoted base types.
static TypeDeclaration	typeDeclaration(TypeDeclIdentifier name, Type type) construct type declaration with denoted name and type.
static TypeDeclIdentifier	typeDeclIdentifier(java.lang.String name) construct type declaration identifier with denoted name.
static TypedIdentifier	typedIdentifier(ValueDeclIdentifier identifier, Type type) construct typed identifier from identifier and type.
static UpdateTerm	updateTerm(Expression base1, Selector[] base2, Expression value) construct component update by index selection from base, base2, and base3
static ValueDeclaration	valueDeclaration(ValueDeclIdentifier name, Type type, Expression value) construct value declaration with denoted name, type and value.
static ValueDeclIdentifier	valueDeclIdentifier(java.lang.String name) construct value declaration identifier with denoted name.
static ValuedIdentifier	valuedIdentifier(Reference identifier, Expression value) construct identifier with value from identifier and value.

Methods inherited from class java.lang.Object

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

Constructor Detail

Construct

public Construct()

Method Detail

reference

public static Reference reference(java.lang.String name)

construct referenc with denoted name.

Parameters:

name - the name of the reference

Returns:

the reference

reference

public static Reference reference(Symbol symbol)

Construct referenc from symbol.

Parameters:

symbol - the symbol

Returns:

the reference

reference

public static Reference reference(ValueDeclIdentifier ident)

construct reference from value declaration identifier.

Parameters:

ident - the name of the reference

Returns:

the reference

reference

public static Reference reference(TypeDeclIdentifier ident)

construct reference from type declaration identifier.

Parameters:

ident - the name of the reference

Returns:

the reference

valueDeclIdentifier

public static ValueDeclIdentifier valueDeclIdentifier(java.lang.String name)

construct value declaration identifier with denoted name.

Parameters:

name - the name of the identifier

Returns:

the declaration identifier (with a new and unique internal name and an associated value symbol)

typeDeclIdentifier

public static TypeDeclIdentifier typeDeclIdentifier(java.lang.String name)

construct type declaration identifier with denoted name.

Parameters:

name - the name of the identifier

Returns:

the declaration identifier (with a new and unique internal name and an associated type symbol)

formulaDeclIdentifier

public static FormulaDeclIdentifier formulaDeclIdentifier(java.lang.String name)

construct formula declaration identifier with denoted name.

Parameters:

name - the name of the identifier

Returns:

the declaration identifier (with a new and unique internal name and an associated formula symbol)

typedIdentifier

public static TypedIdentifier typedIdentifier(ValueDeclIdentifier identifier,
                                              Type type)

construct typed identifier from identifier and type.

Parameters:

identifier - the identifier

type - its type

Returns:

the typed identifier

valuedIdentifier

public static ValuedIdentifier valuedIdentifier(Reference identifier,
                                                Expression value)

construct identifier with value from identifier and value.

Parameters:

identifier - the identifier

value - its value

Returns:

the identifier with value

number

public static Number number(java.lang.String value)

construct number with denoted value.

Parameters:

value - the digit representation of the number

Returns:

the number

logical

public static Logical logical(boolean value)

construct logical constant with denoted value.

Parameters:

value - the value of the constant

Returns:

the constant

typeDeclaration

public static TypeDeclaration typeDeclaration(TypeDeclIdentifier name,
                                              Type type)

construct type declaration with denoted name and type.

Parameters:

name - the declared name

type - the type associated to the name

Returns:

the type declaration

formulaDeclaration

public static FormulaDeclaration formulaDeclaration(FormulaDeclIdentifier name,
                                                    Expression formula)

construct formula declaration with denoted name and formula.

Parameters:

name - the declared name

formula - the formula associated to the name

Returns:

the formula declaration

axiomDeclaration

public static AxiomDeclaration axiomDeclaration(FormulaDeclIdentifier name,
                                                Expression formula)

construct axiom declaration with denoted name and formula

Parameters:

name - the declared name

formula - the formula associated to the name

Returns:

the formula declaration

valueDeclaration

public static ValueDeclaration valueDeclaration(ValueDeclIdentifier name,
                                                Type type,
                                                Expression value)

construct value declaration with denoted name, type and value.

Parameters:

name - the declared name

type - the type associated to the name

value - the value associated to the name (may be null)

Returns:

the type declaration

functionType

public static FunctionType functionType(Type[] domain,
                                        Type range)

construct function type from types domain and range.

Parameters:

domain - the domain of the type

range - the range of the type

Returns:

the function type

atomicType

public static AtomicType atomicType(java.lang.String name)

construct atomic type with denoted name.

Parameters:

name - the name of the type

Returns:

the atomic type

tupleType

public static TupleType tupleType(Type[] base)

construct tuple type with denoted base types.

Parameters:

base - the base types

Returns:

the tuple type

recordType

public static RecordType recordType(TypedIdentifier[] base)

construct record type with denoted base types.

Parameters:

base - the base types (field:type pairs)

Returns:

the record type

arrayType

public static ArrayType arrayType(Type index,
                                  Type base)

construct array type with denoted index type and base type.

Parameters:

index - the index type of the array

base - the base type of the array

Returns:

the array type

subType

public static SubType subType(Expression predicate)

construct subtype with denoted predicate.

Parameters:

predicate - the predicate defining the subtype

Returns:

the subtype

subrangeType

public static SubrangeType subrangeType(Expression from,
                                        Expression to)

construct subrangetype with denoted bounds.

Parameters:

from - the lower bound

to - the upper bound

Returns:

the subrangetype

letExpression

public static LetExpression letExpression(ValueDeclaration[] declarations,
                                          Expression base)

construct let expressions of declarations and base expressions

Parameters:

declarations - the local bindings in the expressions

base - the base expressions

Returns:

the let expresssions

letType

public static LetType letType(TypeDeclaration[] declarations,
                              Type base)

construct let type of declarations and base type

Parameters:

declarations - the local bindings in the type

base - the base type

Returns:

the let type

ifThenElseExpression

public static IfThenElseExpression ifThenElseExpression(Expression condition,
                                                        Expression thenbranch,
                                                        Expression elsebranch)

construct if-then-else expressions from condition, thenbranch, elsebranch.

Parameters:

condition - the formula deciding which branch is selected

thenbranch - the branch selected if the formula yields true

Returns:

thenbranch the branch selected if the formula yields false

notFormula

public static NotFormula notFormula(Expression base)

construct negation (not formula) of base formula

Parameters:

base - the base formula

Returns:

the negation formula

negationTerm

public static NegationTerm negationTerm(Expression base)

construct negation (minus term) of base term

Parameters:

base - the base term

Returns:

the negation term

tupleTerm

public static TupleTerm tupleTerm(Expression[] base)

construct tuple term of base terms

Parameters:

base - the array of base terms, base.length > 1

Returns:

the tuple term

recordTerm

public static RecordTerm recordTerm(ValuedIdentifier[] base)

construct record term of base terms

Parameters:

base - the array of base terms, base.length > 1

Returns:

the record term

lambdaTerm

public static LambdaTerm lambdaTerm(TypedIdentifier[] variables,
                                    Expression base)

construct lambda term of variables and base term

Parameters:

variables - the quantified variables

base - the base term

Returns:

the lambda term

arrayTerm

public static ArrayTerm arrayTerm(TypedIdentifier[] variables,
                                  Expression base)

construct array term of variables and base term

Parameters:

variables - the quantified variables

base - the base term

Returns:

the array term

forallFormula

public static ForallFormula forallFormula(TypedIdentifier[] variables,
                                          Expression base)

construct universally quantifed formula of variables and base formula

Parameters:

variables - the quantified variables

base - the base formula

Returns:

the universally quantified formula

existsFormula

public static ExistsFormula existsFormula(TypedIdentifier[] variables,
                                          Expression base)

construct existentially quantifed formula of variables and base formula

Parameters:

variables - the quantified variables

base - the base formula

Returns:

the existentially quantified formula

andFormula

public static AndFormula andFormula(Expression base1,
                                    Expression base2)

construct conjunction with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

orFormula

public static OrFormula orFormula(Expression base1,
                                  Expression base2)

construct disjunction with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

equivalentFormula

public static EquivalentFormula equivalentFormula(Expression base1,
                                                  Expression base2)

construct equivalence with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

notEquivalentFormula

public static NotEquivalentFormula notEquivalentFormula(Expression base1,
                                                        Expression base2)

construct exclusive disjunction with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

impliesFormula

public static ImpliesFormula impliesFormula(Expression base1,
                                            Expression base2)

construct implication with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

equalsFormula

public static EqualsFormula equalsFormula(Expression base1,
                                          Expression base2)

construct equality with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the expression

notEqualsFormula

public static NotEqualsFormula notEqualsFormula(Expression base1,
                                                Expression base2)

construct inequality with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

plusTerm

public static PlusTerm plusTerm(Expression base1,
                                Expression base2)

construct binary sum with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the term

minusTerm

public static MinusTerm minusTerm(Expression base1,
                                  Expression base2)

construct difference with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the term

timesTerm

public static TimesTerm timesTerm(Expression base1,
                                  Expression base2)

construct binary product with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the term

dividesTerm

public static DividesTerm dividesTerm(Expression base1,
                                      Expression base2)

construct quotient with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the term

powerTerm

public static PowerTerm powerTerm(Expression base1,
                                  Expression base2)

construct power term with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the term

lessFormula

public static LessFormula lessFormula(Expression base1,
                                      Expression base2)

construct less-than formula with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

lessEqualFormula

public static LessEqualFormula lessEqualFormula(Expression base1,
                                                Expression base2)

construct less-than-or-equal formula with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

greaterFormula

public static GreaterFormula greaterFormula(Expression base1,
                                            Expression base2)

construct greater-than formula with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

greaterEqualFormula

public static GreaterEqualFormula greaterEqualFormula(Expression base1,
                                                      Expression base2)

construct greater-than-or-equal formula with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Returns:

the formula

selectorIndex

public static SelectorIndex selectorIndex(Expression base)

make selector from index expression base

Parameters:

base - the selector base

Returns:

the selector

selectorNumber

public static SelectorNumber selectorNumber(Number base)

make selector from number base

Parameters:

base - the selector base

Returns:

the selector

selectorIdentifier

public static SelectorIdentifier selectorIdentifier(Reference base)

make selector from identifier base

Parameters:

base - the selector base

Returns:

the selector

selectionTerm

public static SelectionTerm selectionTerm(Expression base1,
                                          Selector base2)

construct component selection from base1 and base2

Parameters:

base1 - the compound object

base2 - the selector

Returns:

the term

updateTerm

public static UpdateTerm updateTerm(Expression base1,
                                    Selector[] base2,
                                    Expression value)

construct component update by index selection from base, base2, and base3

Parameters:

base1 - the compound object

base2 - the sequence of selectors

value - the update value

Returns:

the term

applicationExpression

public static ApplicationExpression applicationExpression(Expression base1,
                                                          Expression[] base2)

construct application of base1 to base2

Parameters:

base1 - the function/predicate

base2 - the sequence of arguments

Returns:

the expression