LustreCheckMatchExpressions (kind2dev@731decdf5fb1.LustreCheckMatchExpressions)

Module LustreCheckMatchExpressions

Checks match expressions for useless (redundant) arms and for non-exhaustive pattern coverage.

Both anomalies are instances of the useful clause problem, decided by the recursive function Urec of Luc Maranget, "Warnings for pattern matching", Journal of Functional Programming 17(3):387-421, 2007, Section 3.1. Lustre patterns (currently) have no or-patterns, so the corresponding cases of the algorithm are omitted. Match scrutinees are always fully evaluated values, so the strict semantics of Section 3 applies; the algorithm is in any case the same one Maranget proves correct for lazy semantics in Section 4.

author Rob Lorch

type error_kind =

| RedundantPattern of LustreAst.pattern
| IncompletePatternMatch

val error_message : error_kind -> string

type error = [

| `LustreCheckMatchExpressionsError of Lib.position * error_kind

]

val is_exhaustive : 
  TypeCheckerContext.tc_context ->
  LustreAst.lustre_type ->
  LustreAst.pattern list ->
  bool

Whether pats leave no value of the scrutinee type unmatched. Used by LustreDesugarMatchBlocks to decide whether a match block's uncovered cases need a fall-through branch.

val check_match_expressions : 
  TypeCheckerContext.tc_context ->
  LustreAst.t ->
  (LustreAst.t, [> error ]) Stdlib.result

Reports redundant match arms and cases where match arms are not exhaustive. Returns the declarations unchanged.