private void translateLoopInvariantMacros ( Stmt . Loop stmt , WyilFile . Decl . FunctionOrMethod declaration , WyalFile wyalFile ) { // Identifier [ ] prefix = declaration . getQualifiedName ( ) . toName ( ) . getAll ( ) ; Tuple < WyilFile . Expr > loopInvariant = stmt . getInvariant ( ) ; // for ( int i = 0 ; i != loopInvariant . size ( ) ; ++ i ) { WyilFile . Expr clause = loopInvariant . get ( i ) ; Name ident = convert ( declaration . getQualifiedName ( ) , "_loopinvariant_" + clause . getIndex ( ) , declaration . getName ( ) ) ; // Construct fresh environment for this macro. This is necessary to // avoid name clashes with subsequent macros. GlobalEnvironment globalEnvironment = new GlobalEnvironment ( declaration ) ; LocalEnvironment localEnvironment = new LocalEnvironment ( globalEnvironment ) ; WyalFile . VariableDeclaration [ ] vars = generateLoopInvariantParameterDeclarations ( stmt , localEnvironment ) ; WyalFile . Stmt . Block e = translateAsBlock ( clause , localEnvironment . clone ( ) ) ; Named . Macro macro = new Named . Macro ( ident , vars , e ) ; wyalFile . allocate ( macro ) ; } }
Translate the sequence of invariant expressions which constitute the loop invariant of a loop into one or more macros