Module `Smyth.Fill`

val fill : Lang.synthesis_params -> Lang.hole_ctx -> Lang.datatype_ctx -> Lang.hole_filling -> Lang.fill_goal -> (Lang.constraints * Lang.hole_ctx) Nondet.t: fill params delta sigma f g performs type-and-example-directed hole synthesis over the goal defined by g as defined by Figure 8 of the ICFP 2020 paper. Relies on Refine and Branch for the rule Refine-or-Branch and Term_gen for the rule Guess-and-Check.