TCoqBoolVisitor (ESCTools)

Class

Use

Tree

Index

Help

ESC/Java2
© 2003,2004,2005,2006 David Cok and Joseph Kiniry
© 2005,2006 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

escjava.vcGeneration.coq
Class TCoqBoolVisitor

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
                              escjava.vcGeneration.coq.TCoqBoolVisitor

public class TCoqBoolVisitor
extends TCoqVisitor

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 specific values.

Version:: 14/11/2005
Author:: J.Charles

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)`	`TCoqBoolVisitor(java.io.Writer out, TCoqVisitor v, PrettyPrinter o, CoqProver p)` Constructor of the couple TCoqVisitor/TCoqBoolVisitor.

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)` Boolean value seen as a prop boolean value: `True` or `False`.
`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)` Boolean variables that are used within a prop should be translated in the form `myvar = true`
`void`	`visitTNull(TNull n)`
`void`	`visitTRefEQ(TRefEQ n)`
`void`	`visitTRefNE(TRefNE n)`
`void`	`visitTRoot(TRoot n)`
`void`	`visitTSelect(TSelect 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, 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