		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Split-fn-when

A C-to-C transformation to split functions according to some trigger pattern.

Introduction

This transformation traverse finds location in functions which match the provided trigger pattern. When such a pattern is found, the function is split (see split-fn) and the transformation continues looking for further pattern matches. The transformation finishes when no more trigger patterns are found.

General Form

(split-fn-when const-old
               const-new
               :triggers ... ; required
  )

Inputs

const-old

Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a translation unit ensemble. This constant could result from c$::input-files, or from some other transformation.

const-new

Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.

:triggers

A string or string list representing identifiers. A statement matches the trigger pattern if it is a simple function call whose function is an identifier included in this string list. The split-point inferred from such a statement will be immediately before the statement. The first statement of a function will never match the trigger pattern, as splitting in such cases would do nothing. Only top-level statements of a function body will current match a trigger pattern (e.g., statements within an if then/else block will not be considered).
This current representation of a trigger pattern is very limited. It may be expanded in the future to describe various types of expressions at various points in a statement, and causing a split either before or after the statement.