Module Sarek_ppx_lib.Sarek_tailrec_analysis

Recursion Analysis

type recursion_info = {
  1. ri_name : string;
    (*

    Function name

    *)
  2. ri_is_tail : bool;
    (*

    All recursive calls are in tail position

    *)
  3. ri_max_depth : int option;
    (*

    Bounded depth if detectable

    *)
  4. ri_call_count : int;
    (*

    Number of recursive call sites

    *)
  5. ri_in_loop : bool;
    (*

    Has recursive calls inside loops

    *)
}

Information about a recursive function

val is_self_call : string -> Sarek_typed_ast.texpr -> bool

Check if an expression is a call to the named function

val is_recursive_call : string -> Sarek_typed_ast.texpr -> bool

Check if a function application is a recursive call

val count_recursive_calls : string -> Sarek_typed_ast.texpr -> int

Count recursive calls in an expression

val is_tail_recursive : string -> Sarek_typed_ast.texpr -> bool

Check if all recursive calls are in tail position

val has_recursion_in_loops : string -> Sarek_typed_ast.texpr -> bool

Check if recursive calls occur inside loops

val detect_bounded_depth : string -> Sarek_typed_ast.texpr -> int option

Detect bounded recursion depth from the code structure.

This is a conservative analysis that only returns Some when we can prove the recursion is bounded. Currently disabled as the analysis is too imprecise.

TODO: Implement proper termination analysis that tracks:

  • Which parameter is the "depth" parameter (must increase towards bound)
  • That recursive calls increment that parameter
  • That the bound is reached before max_inline_limit

For now, we only support tail recursion which is transformed to loops.

val analyze_recursion : string -> Sarek_typed_ast.texpr -> recursion_info

Analyze a function for recursion patterns