Module LustreCheckADTDecreases

Static termination check for recursive functions with ADT decreases clauses.

For each recursive call f(args) inside such a function, verifies that t_callee[callee_formals := args] is a strict syntactic subterm of the caller's decreases expression t: exactly a variable bound, at some depth >= 1, by an enclosing match's constructor pattern, matched (transitively) against t itself.

type error_kind =
  1. | NotAStructuralSubterm of LustreAst.expr * LustreAst.expr
    (*

    (callee_measure_after_substitution, caller_measure): the recursive call's substituted measure is not a strict subterm of the caller's.

    *)
  2. | MixedDecreasesKindsInScc of LustreAst.ident list
    (*

    The named functions are mutually recursive but do not all use the same kind of decreases measure (integer vs. algebraic data type).

    *)
  3. | RecursiveCallInContract of LustreAst.ident
    (*

    A recursive function's own contract calls the named function, which belongs to the same recursive group.

    *)
val error_message : error_kind -> string
type error = [
  1. | `LustreCheckADTDecreasesError of Lib.position * error_kind
]
val check : TypeCheckerContext.tc_context -> LustreDesugarADTs.adt_map -> int HString.HStringMap.t -> LustreAst.t -> (LustreAst.t, [> error ]) Stdlib.result

Check all recursive FuncDecls in decls whose decreases clause has a recursive ADT type.