escjava.vcGeneration.coq
Class TCoqVisitor

java.lang.Object
  escjava.vcGeneration.TVisitor
      escjava.vcGeneration.coq.visitor.ABasicCoqVisitor
          escjava.vcGeneration.coq.visitor.AIntegralVisitor
              escjava.vcGeneration.coq.visitor.AFloatVisitor
                  escjava.vcGeneration.coq.visitor.AArrayOpsVisitor
                      escjava.vcGeneration.coq.visitor.ANotHandledVisitor
                          escjava.vcGeneration.coq.TCoqVisitor

Direct Known Subclasses:

TCoqBoolVisitor

class TCoqVisitor

extends escjava.vcGeneration.coq.visitor.ANotHandledVisitor

In the Coq extension, we differentiate Boolean value and variables from usual Prop. So we have 2 visitors which are coupled.

This is the visitor used for Boolean used as Prop values. This class, the main Coq visitor is divided into smaller parts handling the different domain-specific functions. For instance all the functions on the Int are in the visitor class AIntegralVisitor.

Version:

14/11/2005

Author:

J.Charles based on the work of C.Hurlin

See Also:

escjava.vcGeneration.coq.visitor

Field Summary

Fields inherited from class escjava.vcGeneration.coq.visitor.ABasicCoqVisitor

out, p, tcbv, tcv

Fields inherited from class escjava.vcGeneration.TVisitor

indentation, lib

Constructor Summary

(package private)	TCoqVisitor(java.io.Writer out, CoqProver prover)
protected	TCoqVisitor(java.io.Writer out, TCoqVisitor v, PrettyPrinter ppout, CoqProver p)

Method Summary

void	printBoolEq(TFunction n)
void	visitTAllocLE(TAllocLE n)
void	visitTAllocLT(TAllocLT n)
void	visitTAnyEQ(TAnyEQ n)
void	visitTAnyNE(TAnyNE n)
void	visitTAsElems(TAsElems n)
void	visitTAsField(TAsField n)
void	visitTBoolAnd(TBoolAnd n)
void	visitTBoolean(TBoolean n)
void	visitTBoolEQ(TBoolEQ n)
void	visitTBoolImplies(TBoolImplies n)
void	visitTBoolNE(TBoolNE n)
void	visitTBoolNot(TBoolNot n)
void	visitTBoolOr(TBoolOr n)
void	visitTChar(TChar n)
void	visitTDouble(TDouble n)
void	visitTEClosedTime(TEClosedTime n)
void	visitTFClosedTime(TFClosedTime n)
void	visitTForAll(TForAll n)
void	visitTIsAllocated(TIsAllocated n)
void	visitTMethodCall(TMethodCall call)
void	visitTName(TName n)
void	visitTNull(TNull n)
void	visitTRefEQ(TRefEQ n)
void	visitTRefNE(TRefNE n)
void	visitTRoot(TRoot n)
void	visitTString(TString n)
void	visitTSum(TSum s)
void	visitTTypeEQ(TTypeEQ n)
void	visitTTypeLE(TTypeLE n)
void	visitTTypeNE(TTypeNE n)
void	visitTTypeOf(TTypeOf n)
void	visitTUnset(TUnset n)

Methods inherited from class escjava.vcGeneration.coq.visitor.ANotHandledVisitor

visitTCast, visitTExist, visitTIs, visitTLockLE, visitTLockLT

Methods inherited from class escjava.vcGeneration.coq.visitor.AArrayOpsVisitor

visitTArrayFresh, visitTArrayLength, visitTArrayShapeMore, visitTArrayShapeOne, visitTAsLockSet, visitTIsNewArray, visitTSelect, visitTStore

Methods inherited from class escjava.vcGeneration.coq.visitor.AFloatVisitor

visitTFloat, visitTFloatAdd, visitTFloatDiv, visitTFloatEQ, visitTFloatGE, visitTFloatGT, visitTFloatLE, visitTFloatLT, visitTFloatMod, visitTFloatMul, visitTFloatNE

Methods inherited from class escjava.vcGeneration.coq.visitor.AIntegralVisitor

visitTInt, visitTIntegralAdd, visitTIntegralDiv, visitTIntegralEQ, visitTIntegralGE, visitTIntegralGT, visitTIntegralLE, visitTIntegralLT, visitTIntegralMod, visitTIntegralMul, visitTIntegralNE, visitTIntegralSub

Methods inherited from class escjava.vcGeneration.coq.visitor.ABasicCoqVisitor

binOp, genericFun, genericOp, genericPropOp, propFun, setVisitors, spacedBinOp, unaryGeneric, unaryProp

Methods inherited from class java.lang.Object

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

Constructor Detail

TCoqVisitor

TCoqVisitor(java.io.Writer out,
            CoqProver prover)

TCoqVisitor

protected TCoqVisitor(java.io.Writer out,
                      TCoqVisitor v,
                      PrettyPrinter ppout,
                      CoqProver p)

Method Detail

visitTName

public void visitTName(TName n)
                throws java.io.IOException

Specified by:

visitTName in class TVisitor

Throws:

java.io.IOException

visitTRoot

public void visitTRoot(TRoot n)
                throws java.io.IOException

Specified by:

visitTRoot in class TVisitor

Throws:

java.io.IOException

visitTBoolImplies

public void visitTBoolImplies(TBoolImplies n)
                       throws java.io.IOException

Specified by:

visitTBoolImplies in class TVisitor

Throws:

java.io.IOException

visitTBoolAnd

public void visitTBoolAnd(TBoolAnd n)
                   throws java.io.IOException

Specified by:

visitTBoolAnd in class TVisitor

Throws:

java.io.IOException

visitTBoolOr

public void visitTBoolOr(TBoolOr n)
                  throws java.io.IOException

Specified by:

visitTBoolOr in class TVisitor

Throws:

java.io.IOException

visitTBoolNot

public void visitTBoolNot(TBoolNot n)
                   throws java.io.IOException

Specified by:

visitTBoolNot in class TVisitor

Throws:

java.io.IOException

visitTBoolEQ

public void visitTBoolEQ(TBoolEQ n)
                  throws java.io.IOException

Specified by:

visitTBoolEQ in class TVisitor

Throws:

java.io.IOException

printBoolEq

public void printBoolEq(TFunction n)
                 throws java.io.IOException

Throws:

java.io.IOException

visitTBoolNE

public void visitTBoolNE(TBoolNE n)
                  throws java.io.IOException

Specified by:

visitTBoolNE in class TVisitor

Throws:

java.io.IOException

visitTAllocLT

public void visitTAllocLT(TAllocLT n)
                   throws java.io.IOException

Specified by:

visitTAllocLT in class TVisitor

Throws:

java.io.IOException

visitTAllocLE

public void visitTAllocLE(TAllocLE n)
                   throws java.io.IOException

Specified by:

visitTAllocLE in class TVisitor

Throws:

java.io.IOException

visitTAnyEQ

public void visitTAnyEQ(TAnyEQ n)
                 throws java.io.IOException

Specified by:

visitTAnyEQ in class TVisitor

Throws:

java.io.IOException

visitTAnyNE

public void visitTAnyNE(TAnyNE n)
                 throws java.io.IOException

Specified by:

visitTAnyNE in class TVisitor

Throws:

java.io.IOException

visitTRefEQ

public void visitTRefEQ(TRefEQ n)
                 throws java.io.IOException

Specified by:

visitTRefEQ in class TVisitor

Throws:

java.io.IOException

visitTRefNE

public void visitTRefNE(TRefNE n)
                 throws java.io.IOException

Specified by:

visitTRefNE in class TVisitor

Throws:

java.io.IOException

visitTTypeEQ

public void visitTTypeEQ(TTypeEQ n)
                  throws java.io.IOException

Specified by:

visitTTypeEQ in class TVisitor

Throws:

java.io.IOException

visitTTypeNE

public void visitTTypeNE(TTypeNE n)
                  throws java.io.IOException

Specified by:

visitTTypeNE in class TVisitor

Throws:

java.io.IOException

visitTTypeLE

public void visitTTypeLE(TTypeLE n)
                  throws java.io.IOException

Specified by:

visitTTypeLE in class TVisitor

Throws:

java.io.IOException

visitTTypeOf

public void visitTTypeOf(TTypeOf n)
                  throws java.io.IOException

Specified by:

visitTTypeOf in class TVisitor

Throws:

java.io.IOException

visitTForAll

public void visitTForAll(TForAll n)
                  throws java.io.IOException

Specified by:

visitTForAll in class TVisitor

Throws:

java.io.IOException

visitTIsAllocated

public void visitTIsAllocated(TIsAllocated n)
                       throws java.io.IOException

Specified by:

visitTIsAllocated in class TVisitor

Throws:

java.io.IOException

visitTEClosedTime

public void visitTEClosedTime(TEClosedTime n)
                       throws java.io.IOException

Specified by:

visitTEClosedTime in class TVisitor

Throws:

java.io.IOException

visitTFClosedTime

public void visitTFClosedTime(TFClosedTime n)
                       throws java.io.IOException

Specified by:

visitTFClosedTime in class TVisitor

Throws:

java.io.IOException

visitTAsElems

public void visitTAsElems(TAsElems n)
                   throws java.io.IOException

Specified by:

visitTAsElems in class TVisitor

Throws:

java.io.IOException

visitTAsField

public void visitTAsField(TAsField n)
                   throws java.io.IOException

Specified by:

visitTAsField in class TVisitor

Throws:

java.io.IOException

visitTString

public void visitTString(TString n)
                  throws java.io.IOException

Specified by:

visitTString in class TVisitor

Throws:

java.io.IOException

visitTBoolean

public void visitTBoolean(TBoolean n)
                   throws java.io.IOException

Specified by:

visitTBoolean in class TVisitor

Throws:

java.io.IOException

visitTChar

public void visitTChar(TChar n)
                throws java.io.IOException

Specified by:

visitTChar in class TVisitor

Throws:

java.io.IOException

visitTDouble

public void visitTDouble(TDouble n)
                  throws java.io.IOException

Specified by:

visitTDouble in class TVisitor

Throws:

java.io.IOException

visitTNull

public void visitTNull(TNull n)
                throws java.io.IOException

Specified by:

visitTNull in class TVisitor

Throws:

java.io.IOException

visitTMethodCall

public void visitTMethodCall(TMethodCall call)
                      throws java.io.IOException

Specified by:

visitTMethodCall in class TVisitor

Throws:

java.io.IOException

visitTUnset

public void visitTUnset(TUnset n)
                 throws java.io.IOException

Specified by:

visitTUnset in class TVisitor

Throws:

java.io.IOException

visitTSum

public void visitTSum(TSum s)

Specified by:

visitTSum in class TVisitor