Module Smyth.Lang

type hole_name = int

The type of hole "names," which is used to identify holes for synthesis.

module Hole_map : sig ... end

A map with domain hole_name.

type 'a hole_map = 'a Hole_map.t

An abbreviation for using Hole_maps.

type typ =
| TArr of typ * typ

Arrow type

| TTuple of typ list

Tuple type

| TData of string * typ list

Datatype

| TForall of string * typ

Universal quantification

| TVar of string

Type variable

Expression types.

type pat =
| PVar of string

Variable pattern

| PTuple of pat list

Tuple pattern

| PWildcard

Wildcard pattern

Patterns.

type param =
| PatParam of pat
| TypeParam of string

The types of valid parameters in a function signature.

type exp_arg =
| EAExp of exp
| EAType of typ

The types of valid arguments in a function application.

and exp =
| EFix of string option * param * exp

Fix expressions (name, param, body)

| EApp of bool * exp * exp_arg

Applications (special, head, arg)

| EVar of string

Variables

| ETuple of exp list

Tuples

| EProj of int * int * exp

Tuple projections (n, i, arg)

| ECtor of string * typ list * exp

Constructors (name, type args, arg)

| ECase of exp * (string * (pat * exp)) list

Case expressions (scrutinee, branches)

| EHole of hole_name

Hole expressions

| EAssert of exp * exp

Assertions

| ETypeAnnotation of exp * typ

Type annotations

Expressions.

  • If the "name" field of a fix expression is None, then the fix is a non-recursive lambda.
  • A "special" application is one that has recursion generated by synthesis from Term_gen. This feature is tracked only for end-user purposes; it can be used, for example, in a "recursive window" UI (that only displays recursive solutions) or in benchmarks for the "Top-1R" (etc.) experiments.
type res_arg =
| RARes of res
| RAType of typ

The types of valid arguments in a result function application.

and res =
| RFix of env * string option * param * exp

Fix closures

| RTuple of res list

Tuples

| RCtor of string * res

Constructors

| RHole of env * hole_name

Hole closures

| RApp of res * res_arg

Applications

| RProj of int * int * res

Tuple projections

| RCase of env * res * (string * (pat * exp)) list

Case results

| RCtorInverse of string * res

Inverse constructors

Results.

  • Determinate results: RFix, RTuple, RCtor.
  • Indeterminate results: RHole, RApp, RProj, RCase, RCtorInverse.
and env = (string * res) list * (string * typ) list

Environments: (result bindings, type variable bindings).

type bind_spec =
| NoSpec
| Rec of string
| Arg of string
| Dec of string

Binding specifications.

type type_binding = string * (typ * bind_spec)

Type bindings for type contexts.

type poly_binding = string

Polymorphic name "bindings" for type contexts (just the name of the variable is needed in the type context).

type type_ctx = type_binding list * poly_binding list

Type contexts.

type datatype_ctx = (string * (string list * (string * typ) list)) list

Datatype contexts.

type hole_ctx = (hole_name * (type_ctx * typ * string option * int)) list

Hole contexts: (hole name, type context, typ, decrease requirement, match depth). The "decrease requirement", if present, is a function that expressions must be decreasing on to fill the hole in question.

type value =
| VTuple of value list

Tuples

| VCtor of string * value

Constructors

"Simple" values.

type example =
| ExTuple of example list

Tuples

| ExCtor of string * example

Constructors

| ExInputOutput of value * example

Input-output examples

| ExTop

Top (wildcard) examples

Examples.

type world = env * example

Example constraints, also known as "worlds."

type worlds = world list

Multiple example constraints (worlds).

type hole_filling = exp hole_map

Hole fillings.

type unsolved_constraints = worlds hole_map

Unfilled holes, also known as "unsolved constraints."

type constraints = hole_filling * unsolved_constraints

Constraints.

type resumption_assertion = res * value

Resumption assertions, as defined in Figure 7.

type resumption_assertions = resumption_assertion list

Multiple resumption assertions.

type gen_goal = type_ctx * typ * string option

Term generation ("guessing") goals.

type synthesis_goal = gen_goal * worlds

Basic synthesis goals.

type fill_goal = hole_name * synthesis_goal

Full notion of synthesis goals, including a hole name.

type synthesis_params = {
max_scrutinee_size : int;
max_match_depth : int;
max_term_size : int;
}

Parameters for synthesis.