Module Smyth.Constraints

Deletes and returns the minimum element of a hole map (such as a Lang.unsolved_constraints).

The empty unevaluation constraint.

from_hole_filling hf creates a new unevaluation constraint consisting of the hole filling hf and no unfilled holes.

from_unsolved_constraints us creates a new unevaluation constraint consisting of the unfilled holes us and no hole filling.

solved_singleton h e creates a new unevaluation constraint consisting of the singleton hole filling h -> e and no unfilled holes.

solved_singleton h x creates a new unevaluation constraint consisting of the singleton unfilled hole h -> x and no hole filling.

Syntactically merges a list of hole fillings, failing if a hole is bound to two syntactically unequal expressions.

Syntactically merges a list of unfilled holes.

Syntactically merges a list of unevaluation constraints using merge_solved and merge_unsolved.

Unevaluation constraint satisfaction as defined by Figure 5 of the ICFP 2020 paper.

satisfies hf ks checks if a hole filling hf satisfies a set of uenvaluation constraints ks using Example.exp_satisfies (i.e., the notion of "ground truth" satisfaction).