This module contains functions and data structures for analyzing the data flow among mutually recursive IR functions. The goal is to find arguments that are never changed throughout the computation. One example for such a "constant argument" is the function passed to map.

map f xs = case xs of { [] -> []; (:) x xs' -> (:) (f x) (map f xs') }

The argument f is passed unchanged to map in every recursive call.

Functions with such recursive calls can be declared inside a Section sentence in Coq where the declaration of f is moved outside the declaration of map (see also FreeC.Backend.Coq.Converter.FuncDecl.Rec.WithSections).

Section map_section.
   ⋮
  Variable f : (* … *).
   ⋮
  Definition map (xs : …) := (* … *).
End map_section.

Within the section, map has only one argument xs but can use f normally. Outside the section it appears as if map has an additional argument f. The section aids Coq's to recognize whether recursive functions that use map and have recursive calls in f terminate. See doc/CustomPragmas/DecreasingArgumentPragma.md for details and examples.