public class OpSubstitutions extends DepthFirstAdapter
This visitor performs two AST transformations which need to be done in one DFS cause they influence each other when definitions are involved. The reason is that in some cases we cannot decide during preparsing and parsing, if the RHS of a definition is an expression or a substitution. Function and operation calls are syntactically the same in most cases. So we postpone the decision until this DFS is made. The first usage of a definition determines which type is assumed. All other uses need to follow this typing otherwise an error is thrown.
During parsing substitutions that are operation calls without return values
are recognized as AFuncOpSubstitution. These
AFuncOpSubstitution nodes can contain any expression. So the parser
accepts any expression as substitution here.
This visitor checks any AFuncOpSubstitution if the child of the node
is of type AFunctionExpression (i.e. operation call with parameters)
or AIdentifierExpression (i.e. operation call without parameters).
Then the AFuncOpSubstitution node is replaced by a corresponding
AOpSubstitution node.
If the child is any other expression type, a BParseException is
thrown.
Definitions with type Expression are not recognized during parsing. In the
resulting AST they are not distinguishable from normal
AIdentifierExpression or AFunctionExpression nodes.
Therefor this visitor searches AIdentifierExpression and
AFunctionExpression nodes and checks if their name is declared as a
definition. If such a node is found, it is replaced by a new node
ADefinitionExpression.
The visitor keeps track of scoped variables to ensure, that no node of a scoped variable is replaced.
caseAAbstractConstantsContextClause, caseAAbstractConstantsMachineClause, caseAAbstractMachineParseUnit, caseAAddExpression, caseAAnticipatedEventstatus, caseAAnySubstitution, caseAArityExpression, caseAAssertionsMachineClause, caseAAssertionSubstitution, caseAAssignSubstitution, caseAAxiomsContextClause, caseABecomesElementOfSubstitution, caseABecomesSuchSubstitution, caseABinExpression, caseABlockSubstitution, caseABooleanFalseExpression, caseABooleanTrueExpression, caseABoolSetExpression, caseABtreeExpression, caseACardExpression, caseACartesianProductExpression, caseACaseOrSubstitution, caseACaseSubstitution, caseAChoiceOrSubstitution, caseAChoiceSubstitution, caseAClosureExpression, caseACompositionExpression, caseAComprehensionSetExpression, caseAComputationOperation, caseAConcatExpression, caseAConcreteVariablesMachineClause, caseAConjunctPredicate, caseAConstantsContextClause, caseAConstantsMachineClause, caseAConstExpression, caseAConstraintsMachineClause, caseAConstructorFreetypeConstructor, caseAConvergentEventstatus, caseAConversionDefinition, caseAConvertBoolExpression, caseACoupleExpression, caseADefArgpattern, caseADeferredSetSet, caseADefineSubstitution, caseADefinitionExpression, caseADefinitionFileParseUnit, caseADefinitionPredicate, caseADefinitionsMachineClause, caseADefinitionSubstitution, caseADescriptionExpression, caseADescriptionPredicate, caseADescriptionSet, caseADirectProductExpression, caseADisjunctPredicate, caseADivExpression, caseADomainExpression, caseADomainRestrictionExpression, caseADomainSubtractionExpression, caseAElementFreetypeConstructor, caseAEmptySequenceExpression, caseAEmptySetExpression, caseAEnumeratedSetSet, caseAEqualPredicate, caseAEquivalencePredicate, caseAEvent, caseAEventBComprehensionSetExpression, caseAEventBContextParseUnit, caseAEventBFirstProjectionExpression, caseAEventBFirstProjectionV2Expression, caseAEventBIdentityExpression, caseAEventBModelParseUnit, caseAEventBSecondProjectionExpression, caseAEventBSecondProjectionV2Expression, caseAEventsModelClause, caseAExistsPredicate, caseAExpressionDefinition, caseAExpressionDefinitionDefinition, caseAExpressionParseUnit, caseAExpressionsMachineClause, caseAExtendedExprExpression, caseAExtendedPredPredicate, caseAExtendsContextClause, caseAExtendsMachineClause, caseAFalsityPredicate, caseAFatherExpression, caseAFileDefinitionDefinition, caseAFileExpression, caseAFileMachineReference, caseAFin1SubsetExpression, caseAFinitePredicate, caseAFinSubsetExpression, caseAFirstExpression, caseAFirstProjectionExpression, caseAFlooredDivExpression, caseAForallPredicate, caseAForallSubMessageSubstitution, caseAForLoopSubstitution, caseAFreetype, caseAFreetypesMachineClause, caseAFrontExpression, caseAFunctionOperation, caseAGeneralConcatExpression, caseAGeneralIntersectionExpression, caseAGeneralProductExpression, caseAGeneralSumExpression, caseAGeneralUnionExpression, caseAGeneratedParseUnit, caseAGreaterEqualPredicate, caseAGreaterPredicate, caseAIdentityExpression, caseAIfElsifSubstitution, caseAIfPredicatePredicate, caseAIfSubstitution, caseAIfThenElseExpression, caseAImageExpression, caseAImplementationMachineParseUnit, caseAImplicationPredicate, caseAImportPackage, caseAImportsMachineClause, caseAIncludesMachineClause, caseAInferredUnitExpression, caseAInfixExpression, caseAInitialisationMachineClause, caseAInsertFrontExpression, caseAInsertTailExpression, caseAIntegerExpression, caseAIntegerSetExpression, caseAIntersectionExpression, caseAIntervalExpression, caseAIntSetExpression, caseAInvalidOperationsClauseMachineClause, caseAInvalidSubstitution, caseAInvariantMachineClause, caseAInvariantModelClause, caseAIseq1Expression, caseAIseqExpression, caseAIterationExpression, caseALabelPredicate, caseALambdaExpression, caseALastExpression, caseALeftExpression, caseALessEqualPredicate, caseALessPredicate, caseALetExpressionExpression, caseALetPredicatePredicate, caseALetSubstitution, caseALocalOperationsMachineClause, caseAMachineClauseParseUnit, caseAMachineHeader, caseAMachineMachineVariant, caseAMachineReference, caseAMaxExpression, caseAMaxIntExpression, caseAMemberPredicate, caseAMinExpression, caseAMinIntExpression, caseAMinusExpression, caseAMinusOrSetSubtractExpression, caseAMirrorExpression, caseAMissingSemicolonOperation, caseAModelMachineVariant, caseAModuloExpression, caseAMultilineStringExpression, caseAMultiplicationExpression, caseAMultOrCartExpression, caseANat1SetExpression, caseANatSetExpression, caseANatural1SetExpression, caseANaturalSetExpression, caseANegationPredicate, caseANewUnitExpression, caseANotEqualPredicate, caseANotMemberPredicate, caseANotSubsetPredicate, caseANotSubsetStrictPredicate, caseAOperation, caseAOperationAttribute, caseAOperationCallExpression, caseAOperationCallSubstitution, caseAOperationsMachineClause, caseAOperatorExpression, caseAOperatorPredicate, caseAOperatorSubstitution, caseAOppatternParseUnit, caseAOpSubstitution, caseAOrdinaryEventstatus, caseAOverwriteExpression, caseAPackageParseUnit, caseAParallelProductExpression, caseAParallelSubstitution, caseAParseUnitDefinitionParseUnit, caseAPartialBijectionExpression, caseAPartialFunctionExpression, caseAPartialInjectionExpression, caseAPartialSurjectionExpression, caseAPartitionPredicate, caseAPermExpression, caseAPostfixExpression, caseAPow1SubsetExpression, caseAPowerOfExpression, caseAPowSubsetExpression, caseAPreconditionSubstitution, caseAPredecessorExpression, caseAPredicateAttributeOperationAttribute, caseAPredicateDefinition, caseAPredicateDefinitionDefinition, caseAPredicateFunctionPredicate, caseAPredicateIdentifierPredicate, caseAPredicateParseUnit, caseAPredicatesMachineClause, caseAPrefixExpression, caseAPrimedIdentifierExpression, caseAPromotesMachineClause, caseAPropertiesMachineClause, caseAProverComprehensionSetExpression, caseAQuantifiedIntersectionExpression, caseAQuantifiedUnionExpression, caseARangeExpression, caseARangeRestrictionExpression, caseARangeSubtractionExpression, caseARankExpression, caseARecEntry, caseARecExpression, caseARecordFieldExpression, caseAReferencesMachineClause, caseARefinedOperation, caseARefinementMachineParseUnit, caseARefinesModelClause, caseAReflexiveClosureExpression, caseARelationsExpression, caseARestrictFrontExpression, caseARestrictTailExpression, caseAReverseExpression, caseARevExpression, caseARightExpression, caseARingExpression, caseARuleFailSubSubstitution, caseARuleOperation, caseASecondProjectionExpression, caseASeesMachineClause, caseASeesModelClause, caseASelectSubstitution, caseASelectWhenSubstitution, caseASeq1Expression, caseASeqExpression, caseASequenceExtensionExpression, caseASequenceSubstitution, caseASetExtensionExpression, caseASetsContextClause, caseASetsMachineClause, caseASetSubtractionExpression, caseASizeExpression, caseASizetExpression, caseASkipSubstitution, caseASonExpression, caseASonsExpression, caseAStringExpression, caseAStringSetExpression, caseAStructExpression, caseASubsetPredicate, caseASubsetStrictPredicate, caseASubstitutionDefinitionDefinition, caseASubstitutionParseUnit, caseASubstitutionPredicate, caseASubtreeExpression, caseASuccessorExpression, caseASurjectionRelationExpression, caseASymbolicComprehensionSetExpression, caseASymbolicLambdaExpression, caseASystemMachineVariant, caseATailExpression, caseATheoremsContextClause, caseATheoremsModelClause, caseATopExpression, caseATotalBijectionExpression, caseATotalFunctionExpression, caseATotalInjectionExpression, caseATotalRelationExpression, caseATotalSurjectionExpression, caseATotalSurjectionRelationExpression, caseATransFunctionExpression, caseATransRelationExpression, caseATreeExpression, caseATruthPredicate, caseATypeofExpression, caseAUnaryMinusExpression, caseAUndefArgpattern, caseAUnionExpression, caseAUnitAliasParseUnit, caseAUnitExpression, caseAUsesMachineClause, caseAValuesEntry, caseAValuesMachineClause, caseAVariablesMachineClause, caseAVariablesModelClause, caseAVariantModelClause, caseAVarSubstitution, caseAWhileSubstitution, caseAWitness, caseStart, defaultIn, defaultOut, inAAbstractConstantsContextClause, inAAbstractConstantsMachineClause, inAAbstractMachineParseUnit, inAAddExpression, inAAnticipatedEventstatus, inAArityExpression, inAAssertionsMachineClause, inAAssertionSubstitution, inAAssignSubstitution, inAAxiomsContextClause, inABecomesElementOfSubstitution, inABecomesSuchSubstitution, inABinExpression, inABlockSubstitution, inABooleanFalseExpression, inABooleanTrueExpression, inABoolSetExpression, inABtreeExpression, inACardExpression, inACartesianProductExpression, inACaseOrSubstitution, inACaseSubstitution, inAChoiceOrSubstitution, inAChoiceSubstitution, inAClosureExpression, inACompositionExpression, inAComputationOperation, inAConcatExpression, inAConcreteVariablesMachineClause, inAConjunctPredicate, inAConstantsContextClause, inAConstantsMachineClause, inAConstExpression, inAConstraintsMachineClause, inAConstructorFreetypeConstructor, inAConvergentEventstatus, inAConversionDefinition, inAConvertBoolExpression, inACoupleExpression, inADefArgpattern, inADeferredSetSet, inADefineSubstitution, inADefinitionExpression, inADefinitionFileParseUnit, inADefinitionPredicate, inADefinitionsMachineClause, inADefinitionSubstitution, inADescriptionExpression, inADescriptionPredicate, inADescriptionSet, inADirectProductExpression, inADisjunctPredicate, inADivExpression, inADomainExpression, inADomainRestrictionExpression, inADomainSubtractionExpression, inAElementFreetypeConstructor, inAEmptySequenceExpression, inAEmptySetExpression, inAEnumeratedSetSet, inAEqualPredicate, inAEquivalencePredicate, inAEvent, inAEventBComprehensionSetExpression, inAEventBContextParseUnit, inAEventBFirstProjectionExpression, inAEventBFirstProjectionV2Expression, inAEventBIdentityExpression, inAEventBModelParseUnit, inAEventBSecondProjectionExpression, inAEventBSecondProjectionV2Expression, inAEventsModelClause, inAExpressionDefinition, inAExpressionDefinitionDefinition, inAExpressionParseUnit, inAExpressionsMachineClause, inAExtendedExprExpression, inAExtendedPredPredicate, inAExtendsContextClause, inAExtendsMachineClause, inAFalsityPredicate, inAFatherExpression, inAFileDefinitionDefinition, inAFileExpression, inAFileMachineReference, inAFin1SubsetExpression, inAFinitePredicate, inAFinSubsetExpression, inAFirstExpression, inAFirstProjectionExpression, inAFlooredDivExpression, inAForallSubMessageSubstitution, inAForLoopSubstitution, inAFreetype, inAFreetypesMachineClause, inAFrontExpression, inAFuncOpSubstitution, inAFunctionExpression, inAFunctionOperation, inAGeneralConcatExpression, inAGeneralIntersectionExpression, inAGeneralUnionExpression, inAGeneratedParseUnit, inAGreaterEqualPredicate, inAGreaterPredicate, inAIdentifierExpression, inAIdentityExpression, inAIfElsifSubstitution, inAIfPredicatePredicate, inAIfSubstitution, inAIfThenElseExpression, inAImageExpression, inAImplementationMachineParseUnit, inAImplicationPredicate, inAImportPackage, inAImportsMachineClause, inAIncludesMachineClause, inAInferredUnitExpression, inAInfixExpression, inAInitialisationMachineClause, inAInsertFrontExpression, inAInsertTailExpression, inAIntegerExpression, inAIntegerSetExpression, inAIntersectionExpression, inAIntervalExpression, inAIntSetExpression, inAInvalidOperationsClauseMachineClause, inAInvalidSubstitution, inAInvariantMachineClause, inAInvariantModelClause, inAIseq1Expression, inAIseqExpression, inAIterationExpression, inALabelPredicate, inALastExpression, inALeftExpression, inALessEqualPredicate, inALessPredicate, inALetExpressionExpression, inALetPredicatePredicate, inALocalOperationsMachineClause, inAMachineClauseParseUnit, inAMachineHeader, inAMachineMachineVariant, inAMachineReference, inAMaxExpression, inAMaxIntExpression, inAMemberPredicate, inAMinExpression, inAMinIntExpression, inAMinusExpression, inAMinusOrSetSubtractExpression, inAMirrorExpression, inAMissingSemicolonOperation, inAModelMachineVariant, inAModuloExpression, inAMultilineStringExpression, inAMultiplicationExpression, inAMultOrCartExpression, inANat1SetExpression, inANatSetExpression, inANatural1SetExpression, inANaturalSetExpression, inANegationPredicate, inANewUnitExpression, inANotEqualPredicate, inANotMemberPredicate, inANotSubsetPredicate, inANotSubsetStrictPredicate, inAOperation, inAOperationAttribute, inAOperationCallExpression, inAOperationCallSubstitution, inAOperationsMachineClause, inAOperatorExpression, inAOperatorPredicate, inAOperatorSubstitution, inAOppatternParseUnit, inAOpSubstitution, inAOrdinaryEventstatus, inAOverwriteExpression, inAPackageParseUnit, inAParallelProductExpression, inAParallelSubstitution, inAParseUnitDefinitionParseUnit, inAPartialBijectionExpression, inAPartialFunctionExpression, inAPartialInjectionExpression, inAPartialSurjectionExpression, inAPartitionPredicate, inAPermExpression, inAPostfixExpression, inAPow1SubsetExpression, inAPowerOfExpression, inAPowSubsetExpression, inAPreconditionSubstitution, inAPredecessorExpression, inAPredicateAttributeOperationAttribute, inAPredicateDefinition, inAPredicateDefinitionDefinition, inAPredicateFunctionPredicate, inAPredicateIdentifierPredicate, inAPredicateParseUnit, inAPredicatesMachineClause, inAPrefixExpression, inAPrimedIdentifierExpression, inAPromotesMachineClause, inAPropertiesMachineClause, inAProverComprehensionSetExpression, inARangeExpression, inARangeRestrictionExpression, inARangeSubtractionExpression, inARankExpression, inARecEntry, inARecExpression, inARecordFieldExpression, inAReferencesMachineClause, inARefinedOperation, inARefinementMachineParseUnit, inARefinesModelClause, inAReflexiveClosureExpression, inARelationsExpression, inARestrictFrontExpression, inARestrictTailExpression, inAReverseExpression, inARevExpression, inARightExpression, inARingExpression, inARuleFailSubSubstitution, inARuleOperation, inASecondProjectionExpression, inASeesMachineClause, inASeesModelClause, inASelectSubstitution, inASelectWhenSubstitution, inASeq1Expression, inASeqExpression, inASequenceExtensionExpression, inASequenceSubstitution, inASetExtensionExpression, inASetsContextClause, inASetsMachineClause, inASetSubtractionExpression, inASizeExpression, inASizetExpression, inASkipSubstitution, inASonExpression, inASonsExpression, inAStringExpression, inAStringSetExpression, inAStructExpression, inASubsetPredicate, inASubsetStrictPredicate, inASubstitutionDefinitionDefinition, inASubstitutionParseUnit, inASubstitutionPredicate, inASubtreeExpression, inASuccessorExpression, inASurjectionRelationExpression, inASymbolicComprehensionSetExpression, inASymbolicLambdaExpression, inASystemMachineVariant, inATailExpression, inATheoremsContextClause, inATheoremsModelClause, inATopExpression, inATotalBijectionExpression, inATotalFunctionExpression, inATotalInjectionExpression, inATotalRelationExpression, inATotalSurjectionExpression, inATotalSurjectionRelationExpression, inATransFunctionExpression, inATransRelationExpression, inATreeExpression, inATruthPredicate, inATypeofExpression, inAUnaryMinusExpression, inAUndefArgpattern, inAUnionExpression, inAUnitAliasParseUnit, inAUnitExpression, inAUsesMachineClause, inAValuesEntry, inAValuesMachineClause, inAVariablesMachineClause, inAVariablesModelClause, inAVariantModelClause, inAWhileSubstitution, inAWitness, inStart, outAAbstractConstantsContextClause, outAAbstractConstantsMachineClause, outAAbstractMachineParseUnit, outAAddExpression, outAAnticipatedEventstatus, outAArityExpression, outAAssertionsMachineClause, outAAssertionSubstitution, outAAssignSubstitution, outAAxiomsContextClause, outABecomesElementOfSubstitution, outABecomesSuchSubstitution, outABinExpression, outABlockSubstitution, outABooleanFalseExpression, outABooleanTrueExpression, outABoolSetExpression, outABtreeExpression, outACardExpression, outACartesianProductExpression, outACaseOrSubstitution, outACaseSubstitution, outAChoiceOrSubstitution, outAChoiceSubstitution, outAClosureExpression, outACompositionExpression, outAComputationOperation, outAConcatExpression, outAConcreteVariablesMachineClause, outAConjunctPredicate, outAConstantsContextClause, outAConstantsMachineClause, outAConstExpression, outAConstraintsMachineClause, outAConstructorFreetypeConstructor, outAConvergentEventstatus, outAConversionDefinition, outAConvertBoolExpression, outACoupleExpression, outADefArgpattern, outADeferredSetSet, outADefineSubstitution, outADefinitionExpression, outADefinitionFileParseUnit, outADefinitionPredicate, outADefinitionsMachineClause, outADefinitionSubstitution, outADescriptionExpression, outADescriptionPredicate, outADescriptionSet, outADirectProductExpression, outADisjunctPredicate, outADivExpression, outADomainExpression, outADomainRestrictionExpression, outADomainSubtractionExpression, outAElementFreetypeConstructor, outAEmptySequenceExpression, outAEmptySetExpression, outAEnumeratedSetSet, outAEqualPredicate, outAEquivalencePredicate, outAEvent, outAEventBComprehensionSetExpression, outAEventBContextParseUnit, outAEventBFirstProjectionExpression, outAEventBFirstProjectionV2Expression, outAEventBIdentityExpression, outAEventBModelParseUnit, outAEventBSecondProjectionExpression, outAEventBSecondProjectionV2Expression, outAEventsModelClause, outAExpressionDefinition, outAExpressionDefinitionDefinition, outAExpressionParseUnit, outAExpressionsMachineClause, outAExtendedExprExpression, outAExtendedPredPredicate, outAExtendsContextClause, outAExtendsMachineClause, outAFalsityPredicate, outAFatherExpression, outAFileDefinitionDefinition, outAFileExpression, outAFileMachineReference, outAFin1SubsetExpression, outAFinitePredicate, outAFinSubsetExpression, outAFirstExpression, outAFirstProjectionExpression, outAFlooredDivExpression, outAForallSubMessageSubstitution, outAForLoopSubstitution, outAFreetype, outAFreetypesMachineClause, outAFrontExpression, outAFuncOpSubstitution, outAFunctionExpression, outAFunctionOperation, outAGeneralConcatExpression, outAGeneralIntersectionExpression, outAGeneralUnionExpression, outAGeneratedParseUnit, outAGreaterEqualPredicate, outAGreaterPredicate, outAIdentifierExpression, outAIdentityExpression, outAIfElsifSubstitution, outAIfPredicatePredicate, outAIfSubstitution, outAIfThenElseExpression, outAImageExpression, outAImplementationMachineParseUnit, outAImplicationPredicate, outAImportPackage, outAImportsMachineClause, outAIncludesMachineClause, outAInferredUnitExpression, outAInfixExpression, outAInitialisationMachineClause, outAInsertFrontExpression, outAInsertTailExpression, outAIntegerExpression, outAIntegerSetExpression, outAIntersectionExpression, outAIntervalExpression, outAIntSetExpression, outAInvalidOperationsClauseMachineClause, outAInvalidSubstitution, outAInvariantMachineClause, outAInvariantModelClause, outAIseq1Expression, outAIseqExpression, outAIterationExpression, outALabelPredicate, outALastExpression, outALeftExpression, outALessEqualPredicate, outALessPredicate, outALetExpressionExpression, outALetPredicatePredicate, outALocalOperationsMachineClause, outAMachineClauseParseUnit, outAMachineHeader, outAMachineMachineVariant, outAMachineReference, outAMaxExpression, outAMaxIntExpression, outAMemberPredicate, outAMinExpression, outAMinIntExpression, outAMinusExpression, outAMinusOrSetSubtractExpression, outAMirrorExpression, outAMissingSemicolonOperation, outAModelMachineVariant, outAModuloExpression, outAMultilineStringExpression, outAMultiplicationExpression, outAMultOrCartExpression, outANat1SetExpression, outANatSetExpression, outANatural1SetExpression, outANaturalSetExpression, outANegationPredicate, outANewUnitExpression, outANotEqualPredicate, outANotMemberPredicate, outANotSubsetPredicate, outANotSubsetStrictPredicate, outAOperation, outAOperationAttribute, outAOperationCallExpression, outAOperationCallSubstitution, outAOperationsMachineClause, outAOperatorExpression, outAOperatorPredicate, outAOperatorSubstitution, outAOppatternParseUnit, outAOpSubstitution, outAOrdinaryEventstatus, outAOverwriteExpression, outAPackageParseUnit, outAParallelProductExpression, outAParallelSubstitution, outAParseUnitDefinitionParseUnit, outAPartialBijectionExpression, outAPartialFunctionExpression, outAPartialInjectionExpression, outAPartialSurjectionExpression, outAPartitionPredicate, outAPermExpression, outAPostfixExpression, outAPow1SubsetExpression, outAPowerOfExpression, outAPowSubsetExpression, outAPreconditionSubstitution, outAPredecessorExpression, outAPredicateAttributeOperationAttribute, outAPredicateDefinition, outAPredicateDefinitionDefinition, outAPredicateFunctionPredicate, outAPredicateIdentifierPredicate, outAPredicateParseUnit, outAPredicatesMachineClause, outAPrefixExpression, outAPrimedIdentifierExpression, outAPromotesMachineClause, outAPropertiesMachineClause, outAProverComprehensionSetExpression, outARangeExpression, outARangeRestrictionExpression, outARangeSubtractionExpression, outARankExpression, outARecEntry, outARecExpression, outARecordFieldExpression, outAReferencesMachineClause, outARefinedOperation, outARefinementMachineParseUnit, outARefinesModelClause, outAReflexiveClosureExpression, outARelationsExpression, outARestrictFrontExpression, outARestrictTailExpression, outAReverseExpression, outARevExpression, outARightExpression, outARingExpression, outARuleFailSubSubstitution, outARuleOperation, outASecondProjectionExpression, outASeesMachineClause, outASeesModelClause, outASelectSubstitution, outASelectWhenSubstitution, outASeq1Expression, outASeqExpression, outASequenceExtensionExpression, outASequenceSubstitution, outASetExtensionExpression, outASetsContextClause, outASetsMachineClause, outASetSubtractionExpression, outASizeExpression, outASizetExpression, outASkipSubstitution, outASonExpression, outASonsExpression, outAStringExpression, outAStringSetExpression, outAStructExpression, outASubsetPredicate, outASubsetStrictPredicate, outASubstitutionDefinitionDefinition, outASubstitutionParseUnit, outASubstitutionPredicate, outASubtreeExpression, outASuccessorExpression, outASurjectionRelationExpression, outASymbolicComprehensionSetExpression, outASymbolicLambdaExpression, outASystemMachineVariant, outATailExpression, outATheoremsContextClause, outATheoremsModelClause, outATopExpression, outATotalBijectionExpression, outATotalFunctionExpression, outATotalInjectionExpression, outATotalRelationExpression, outATotalSurjectionExpression, outATotalSurjectionRelationExpression, outATransFunctionExpression, outATransRelationExpression, outATreeExpression, outATruthPredicate, outATypeofExpression, outAUnaryMinusExpression, outAUndefArgpattern, outAUnionExpression, outAUnitAliasParseUnit, outAUnitExpression, outAUsesMachineClause, outAValuesEntry, outAValuesMachineClause, outAVariablesMachineClause, outAVariablesModelClause, outAVariantModelClause, outAWhileSubstitution, outAWitness, outStartcaseEOF, caseTAbstractConstants, caseTAbstractVariables, caseTAny, caseTArity, caseTAssert, caseTAssertions, caseTAssign, caseTBe, caseTBegin, caseTBfalse, caseTBin, caseTBool, caseTBoolCast, caseTBtree, caseTCard, caseTCase, caseTChoice, caseTClosure, caseTClosure1, caseTComma, caseTComment, caseTCommentBody, caseTCommentEnd, caseTConc, caseTConcatSequence, caseTConcreteConstants, caseTConcreteVariables, caseTConjunction, caseTConst, caseTConstants, caseTConstraints, caseTDefinitions, caseTDefLiteralPredicate, caseTDefLiteralSubstitution, caseTDirectProduct, caseTDivision, caseTDo, caseTDollar, caseTDom, caseTDomainRestriction, caseTDomainSubtraction, caseTDot, caseTDoubleColon, caseTDoubleEqual, caseTDoubleVerticalBar, caseTEither, caseTElementOf, caseTElse, caseTElsif, caseTEmptySet, caseTEnd, caseTEqual, caseTEquivalence, caseTExists, caseTExpressions, caseTExtends, caseTFalse, caseTFather, caseTFin, caseTFin1, caseTFirst, caseTFnc, caseTForAny, caseTFront, caseTGeneralizedInter, caseTGeneralizedUnion, caseTGreater, caseTGreaterEqual, caseTHexLiteral, caseTId, caseTIdentifierLiteral, caseTIf, caseTImplementation, caseTImplies, caseTImports, caseTIn, caseTIncludes, caseTInclusion, caseTInfix, caseTInitialisation, caseTInsertEndSequence, caseTInsertStartSequence, caseTInt, caseTInteger, caseTIntegerLiteral, caseTIntersection, caseTInterval, caseTInvariant, caseTIpragmaUnit, caseTIseq, caseTIseq1, caseTIterate, caseTKwAbstractConstants, caseTKwAbstractVariables, caseTKwAssertions, caseTKwAttributeIdentifier, caseTKwBody, caseTKwComputation, caseTKwConcreteConstants, caseTKwConcreteVariables, caseTKwConstants, caseTKwConstraints, caseTKwCounterexample, caseTKwDefine, caseTKwDefinition, caseTKwDefinitions, caseTKwDummyValue, caseTKwExpect, caseTKwExpression, caseTKwExpressionOperator, caseTKwExtends, caseTKwFor, caseTKwFormula, caseTKwFreetypes, caseTKwFunction, caseTKwImports, caseTKwIncludes, caseTKwInitialisation, caseTKwInvariant, caseTKwLocalOperations, caseTKwMachineClause, caseTKwOperations, caseTKwOppattern, caseTKwPredicate, caseTKwPredicateAttribute, caseTKwPredicateOperator, caseTKwPromotes, caseTKwProperties, caseTKwReferences, caseTKwRule, caseTKwRuleErrorType, caseTKwRuleFail, caseTKwRuleForAll, caseTKwRulesMachine, caseTKwSees, caseTKwSets, caseTKwSubstitution, caseTKwSubstitutionOperator, caseTKwType, caseTKwUses, caseTKwValue, caseTKwValues, caseTKwVariables, caseTLambda, caseTLast, caseTLeft, caseTLeftBrace, caseTLeftBracket, caseTLeftPar, caseTLess, caseTLessEqual, caseTLet, caseTLineComment, caseTLocalOperations, caseTLogicalOr, caseTMachine, caseTMaplet, caseTMax, caseTMaxInt, caseTMin, caseTMinInt, caseTMinus, caseTMirror, caseTMod, caseTModel, caseTMultilineStringContent, caseTMultilineStringEnd, caseTMultilineStringStart, caseTNat, caseTNat1, caseTNatural, caseTNatural1, caseTNewPragmaUnit, caseTNonInclusion, caseTNot, caseTNotBelonging, caseTNotEqual, caseTOf, caseTOperations, caseTOr, caseTOutputParameters, caseTOverwriteRelation, caseTPartialBijection, caseTPartialFunction, caseTPartialInjection, caseTPartialSurjection, caseTPerm, caseTPi, caseTPlus, caseTPostfix, caseTPow, caseTPow1, caseTPowerOf, caseTPragmaConversion, caseTPragmaDescription, caseTPragmaEnd, caseTPragmaFile, caseTPragmaFreeText, caseTPragmaGenerated, caseTPragmaIdOrString, caseTPragmaImportPackage, caseTPragmaLabel, caseTPragmaPackage, caseTPragmaStart, caseTPragmaSymbolic, caseTPragmaUnit, caseTPragmaUnitAlias, caseTPre, caseTPred, caseTPredicateIdentifier, caseTPredicates, caseTPrefix, caseTPrj1, caseTPrj2, caseTProduct, caseTPromotes, caseTProperties, caseTQuantifiedInter, caseTQuantifiedSet, caseTQuantifiedUnion, caseTRan, caseTRangeRestriction, caseTRangeSubtraction, caseTRank, caseTRec, caseTRefinement, caseTRefines, caseTRel, caseTRestrictHeadSequence, caseTRestrictTailSequence, caseTRev, caseTRight, caseTRightBrace, caseTRightBracket, caseTRightPar, caseTSees, caseTSelect, caseTSemicolon, caseTSeq, caseTSeq1, caseTSetRelation, caseTSets, caseTSetSubtraction, caseTShebang, caseTShebangChar, caseTShebangEnd, caseTSigma, caseTSingleQuotation, caseTSize, caseTSizet, caseTSkip, caseTSlash, caseTSon, caseTSons, caseTStar, caseTStrictInclusion, caseTStrictNonInclusion, caseTString, caseTStringLiteral, caseTStruct, caseTSubtree, caseTSucc, caseTSurjectionRelation, caseTSystem, caseTTail, caseTThen, caseTTilde, caseTTop, caseTTotalBijection, caseTTotalFunction, caseTTotalInjection, caseTTotalRelation, caseTTotalSurjection, caseTTotalSurjectionRelation, caseTTree, caseTTrue, caseTTruthPredicate, caseTUnderscore, caseTUnion, caseTUnitContent, caseTUnitId, caseTUses, caseTValue, caseTVar, caseTVariables, caseTVariant, caseTVerticalBar, caseTWhen, caseTWhere, caseTWhile, caseTWhiteSpace, defaultCase, getIn, getOut, setIn, setOutpublic static void transform(Start start, IDefinitions definitions) throws CheckException
CheckExceptionpublic void caseAFuncOpSubstitution(AFuncOpSubstitution node)
caseAFuncOpSubstitution in interface AnalysiscaseAFuncOpSubstitution in class DepthFirstAdapterpublic void inAExistsPredicate(AExistsPredicate node)
inAExistsPredicate in class DepthFirstAdapterpublic void inAForallPredicate(AForallPredicate node)
inAForallPredicate in class DepthFirstAdapterpublic void inAGeneralSumExpression(AGeneralSumExpression node)
inAGeneralSumExpression in class DepthFirstAdapterpublic void inAGeneralProductExpression(AGeneralProductExpression node)
inAGeneralProductExpression in class DepthFirstAdapterpublic void inALambdaExpression(ALambdaExpression node)
inALambdaExpression in class DepthFirstAdapterpublic void inAComprehensionSetExpression(AComprehensionSetExpression node)
inAComprehensionSetExpression in class DepthFirstAdapterpublic void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node)
inAQuantifiedUnionExpression in class DepthFirstAdapterpublic void inAQuantifiedIntersectionExpression(AQuantifiedIntersectionExpression node)
inAQuantifiedIntersectionExpression in class DepthFirstAdapterpublic void inAAnySubstitution(AAnySubstitution node)
inAAnySubstitution in class DepthFirstAdapterpublic void inALetSubstitution(ALetSubstitution node)
inALetSubstitution in class DepthFirstAdapterpublic void inAVarSubstitution(AVarSubstitution node)
inAVarSubstitution in class DepthFirstAdapterpublic void outAExistsPredicate(AExistsPredicate node)
outAExistsPredicate in class DepthFirstAdapterpublic void outAForallPredicate(AForallPredicate node)
outAForallPredicate in class DepthFirstAdapterpublic void outAGeneralSumExpression(AGeneralSumExpression node)
outAGeneralSumExpression in class DepthFirstAdapterpublic void outAGeneralProductExpression(AGeneralProductExpression node)
outAGeneralProductExpression in class DepthFirstAdapterpublic void outALambdaExpression(ALambdaExpression node)
outALambdaExpression in class DepthFirstAdapterpublic void outAComprehensionSetExpression(AComprehensionSetExpression node)
outAComprehensionSetExpression in class DepthFirstAdapterpublic void outAQuantifiedIntersectionExpression(AQuantifiedIntersectionExpression node)
outAQuantifiedIntersectionExpression in class DepthFirstAdapterpublic void outAQuantifiedUnionExpression(AQuantifiedUnionExpression node)
outAQuantifiedUnionExpression in class DepthFirstAdapterpublic void outAAnySubstitution(AAnySubstitution node)
outAAnySubstitution in class DepthFirstAdapterpublic void outALetSubstitution(ALetSubstitution node)
outALetSubstitution in class DepthFirstAdapterpublic void outAVarSubstitution(AVarSubstitution node)
outAVarSubstitution in class DepthFirstAdapterpublic void caseAIdentifierExpression(AIdentifierExpression node)
caseAIdentifierExpression in interface AnalysiscaseAIdentifierExpression in class DepthFirstAdapterpublic void caseAFunctionExpression(AFunctionExpression node)
caseAFunctionExpression in interface AnalysiscaseAFunctionExpression in class DepthFirstAdapter