Module Smyth.Clean

val clean : Lang.hole_ctx -> Lang.hole_filling -> (Lang.hole_name * Lang.exp) list option

clean delta hf first propagates the expressions in the hole-filling hf upward to generate a new hole-filling with no expression holes (except for self-recursive ones, e.g. from the Defer rule defined in Figure 8 of the ICFP 2020 paper). It then removes any unused holes from the resulting hole-filling and returns a list of hole-to-expression bindings.