Module Smyth.Lang
type 'a hole_map
= 'a Hole_map.t
An abbreviation for using
Hole_map
s.
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.
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.
- If the "name" field of a fix expression is
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
.
- Determinate results:
and env
= (string * res) list * (string * typ) list
Environments:
(result bindings, type variable bindings)
.
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 example
=
|
ExTuple of example list
Tuples
|
ExCtor of string * example
Constructors
|
ExInputOutput of value * example
Input-output examples
|
ExTop
Top (wildcard) examples
Examples.
type worlds
= world list
Multiple example constraints (worlds).
type constraints
= hole_filling * unsolved_constraints
Constraints.
type resumption_assertions
= resumption_assertion list
Multiple resumption assertions.
type fill_goal
= hole_name * synthesis_goal
Full notion of synthesis goals, including a hole name.