Module Smyth

module Branch : sig ... end

Type-and-example-directed branching, as defined in Figure 9 of the ICFP 2020 paper.

module Clean : sig ... end

Hole context cleanup.

module Constraints : sig ... end

Hole fillings, unfilled holes (unsolved constraints), and unevaluation constraints.

module Debug : sig ... end

Debugging utilities.

module Desugar : sig ... end

Helper module for constructing Lang.exp values.

module Endpoint : sig ... end

Endpoints for clients using the Smyth library.

module Env : sig ... end

Evaluation environments.

module Eval : sig ... end

Live evaluation and resumption, as defined in Figure 4 of the ICFP 2020 paper.

module Example : sig ... end

Example helpers and "ground truth" example satisfaction.

module Exp : sig ... end

Expression helpers.

module Fill : sig ... end

Type-and-example-directed hole synthesis, as defined in Figure 8 of the ICFP 2020 paper.

module Fresh : sig ... end

Manages fresh (unique) hole names.

module Lang : sig ... end

The syntax of Core Smyth, as defined in Figure 3 of the ICFP 2020 paper.

module Log : sig ... end

Logging utilities.

module Nondet : sig ... end

Nondeterministic computations via collections semantics.

module Params : sig ... end

Synthesis and system parameters.

module Parse : sig ... end

Parsing of surface-level syntax.

module Pat : sig ... end

Pattern helpers.

module Post_parse : sig ... end

Functions to be called after the corresponding functions in Parse.

module Pretty : sig ... end

Pretty-printing.

module Rank : sig ... end

Ranking algorithms for synthesis solutions.

module Refine : sig ... end

Type-and-example-directed refinement, as defined in Figure 9 of the ICFP 2020 paper.

module Res : sig ... end

Result helpers.

module Solve : sig ... end

Constraint solving, as defined in Figure 8 of the ICFP 2020 paper.

module Sugar : sig ... end

Helper module for deconstructing Lang.exp values.

module Term_gen : sig ... end

Efficient type-directed guessing consistent with Figure 17 of the ICFP 2020 paper (Appendix A).

module Timer : sig ... end

A collection of timers used to cut off program execution early.

module Type : sig ... end

Type helpers and type-checking.

module Type_ctx : sig ... end

Type contexts.

module Uneval : sig ... end

Live bidirectional example checking via live unevaluation, as defined in Figure 6 of the ICFP 2020 paper.