Module `Smyth.Uneval`

val minimal_uneval : bool Stdlib.ref: Whether or not unevaluation should proceed in the "minimal" mode. Minimal mode uses U-Case-Guess and not U-Case; non-minimal mode does the opposite.

val check : Lang.hole_ctx -> Lang.datatype_ctx -> Lang.hole_filling -> Lang.exp -> Lang.worlds -> Lang.constraints Nondet.t: Live bidirectional example checking.

val uneval : Lang.hole_ctx -> Lang.datatype_ctx -> Lang.hole_filling -> Lang.res -> Lang.example -> Lang.constraints Nondet.t: Live unevaluation.

val simplify_assertions : Lang.hole_ctx -> Lang.datatype_ctx -> Lang.resumption_assertions -> Lang.constraints Nondet.t: Assertion simplification, as defined in Figure 7 of the ICFP 2020 paper.