fmrisc.ProofNavigator.Proving

Class Rewriting

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTVisitorBase

fmrisc.ProofNavigator.Proving.Rewriting

All Implemented Interfaces:

ASTVisitor

public final class Rewriting
extends ASTVisitorBase

A visitor for rewriting expressions to a more human-friendly form.

Constructor Summary

Constructors

Constructor and Description
Rewriting()

Method Summary

Modifier and Type	Method and Description
boolean	isCloned() Visitor functions.
static Expression	rewrite(Expression exp) Rewrite expression to more human-friendly form.

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTVisitorBase

visit

Methods inherited from class java.lang.Object

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

Constructor Detail

Rewriting

public Rewriting()

Method Detail

rewrite

public static Expression rewrite(Expression exp)

Rewrite expression to more human-friendly form.

Parameters:

exp - an expression.

Returns:

its rewritten form.

isCloned

public boolean isCloned()

Visitor functions.

Specified by:

isCloned in interface ASTVisitor

Overrides:

isCloned in class ASTVisitorBase

Returns:

false, signalling that the tree is not to be cloned.