Previous  Up  Next

Module Expressions

module Expressions: sig .. end
This module defines substitution functions and binding functions on expressions as well as data type groups.

Data type groups


val bind_data_type_group_in_toplevel_items : TypeCore.env ->
       TypeCore.data_type_group ->
       ExpressionsCore.toplevel_item list ->
       TypeCore.env * ExpressionsCore.toplevel_item list * TypeCore.var list *
       (TypeCore.var * Datacon.name * SurfaceSyntax.datacon_info) list
This function processes a data_type_group, and opens the corresponding binders in the toplevel_items that follow. The resulting toplevel_items are returned, as well as the list of vars that have been bound.
val bind_data_type_group_in_expr : TypeCore.env ->
       TypeCore.data_type_group ->
       ExpressionsCore.expression ->
       TypeCore.env * ExpressionsCore.expression * TypeCore.var list *
       (TypeCore.var * Datacon.name * SurfaceSyntax.datacon_info) list
Used by the type-checker to process local type declarations.
val resolve_branch : TypeCore.var -> TypeCore.branch -> TypeCore.branch
Use this to transform the branch from a type_def into something that's suitable for manipulation as a type.

Substitution functions



Of course, we have many more substitution functions, since now all the substitution functions for types have to be extended to expressions and patterns. The naming convention is as follows: Because most of the things are done through the "substitution kit" (see below), most of the variants for substitution functions are *not* exposed to the client code.

Convenience helpers


val e_unit : ExpressionsCore.expression
The () (unit) expression.
val p_unit : ExpressionsCore.pattern
The () (unit) pattern.
val eunloc : ExpressionsCore.expression -> ExpressionsCore.expression
Remove any ELocated node in front of an expression.

Substitution functions for expressions.


val tsubst_expr : TypeCore.typ ->
       int -> ExpressionsCore.expression -> ExpressionsCore.expression

Binding functions


type substitution_kit = {
   subst_type : TypeCore.typ -> TypeCore.typ;
   subst_expr : ExpressionsCore.expression -> ExpressionsCore.expression;
   subst_def : ExpressionsCore.definitions -> ExpressionsCore.definitions;
   subst_toplevel : ExpressionsCore.toplevel_item list -> ExpressionsCore.toplevel_item list;
   subst_pat : ExpressionsCore.pattern list -> ExpressionsCore.pattern list;
   vars : TypeCore.var list;
   names : Variable.name list;
}
To tame the combinatorial explosion, the binding functions in this module return a substitution kit. That is to say, once you've bound type vars or term vars, you're given a set of functions that you can apply on whatever you need to open the binders. You are also given the list of (open) variables.
val bind_evars : TypeCore.env ->
       TypeCore.type_binding list -> TypeCore.env * substitution_kit
Bind a set of term variables (let-bindings).
val bind_vars : TypeCore.env ->
       SurfaceSyntax.type_binding list ->
       TypeCore.env * substitution_kit
Bind a set of type variables (Λ-bindings).
val bind_patexprs : TypeCore.env ->
       ExpressionsCore.rec_flag ->
       (ExpressionsCore.pattern * ExpressionsCore.expression) list ->
       TypeCore.env * (ExpressionsCore.pattern * ExpressionsCore.expression) list *
       substitution_kit
Bind a set of multiple bindings (and keyword). The bindings may be mutually recursive. There is also a set of expressions on the right-hand-side of each = sign. The variables will also be opened there, and this function takes care of doing it properly depending on whether these are recursive bindings or not.

It is then up to the client code to open these variables in the body of the multiple bindings. Consider for instance "let rec x = e1 and y = e2 in e"; this function will correctly open "x" and "y" in "e1" and "e2" but you must use the substitution kit to open "x" and "y" in "e".

module ExprPrinter: sig .. end
Our not-so-pretty printer for expressions.