private void translatePreconditionMacros ( WyilFile . Decl . FunctionOrMethod declaration ) { Tuple < WyilFile . Expr > invariants = declaration . getRequires ( ) ; // for ( int i = 0 ; i != invariants . size ( ) ; ++ i ) { // 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 [ ] type = generatePreconditionParameters ( declaration , localEnvironment ) ; // Translate expression itself WyalFile . Stmt . Block clause = translateAsBlock ( invariants . get ( i ) , localEnvironment ) ; // Capture any free variables. This is necessary to deal with any // variable aliases introduced by type test operators. clause = captureFreeVariables ( declaration , globalEnvironment , clause ) ; // Name ident = convert ( declaration . getQualifiedName ( ) , "_requires_" + i , declaration . getName ( ) ) ; WyalFile . Declaration md = new WyalFile . Declaration . Named . Macro ( ident , type , clause ) ; allocate ( md , invariants . get ( i ) . getParent ( WyilFile . Attribute . Span . class ) ) ; } }
Translate the sequence of invariant expressions which constitute the precondition of a function or method into corresponding macro declarations .