Previous  Up  Next

Module Expressions

module Expressions: sig .. end
This module defines the syntax of expressions, as manipulated by the type-checker. This module also defines various expression-specific manipulation functions, esp. w.r.t. binders.

The definition of expressions


type tag_update_info = SurfaceSyntax.tag_update_info 
type field = SurfaceSyntax.field 
type pattern =
| PVar of Variable.name * TypeCore.location
| PTuple of pattern list
| PConstruct of TypeCore.resolved_datacon * (TypeCore.Field.name * pattern) list
| POpen of TypeCore.var
| PAs of pattern * pattern
| PAny
The type of patterns. We don't have type annotations anymore, they have been transformed into type annotations onto the corresponding expression, i.e. EConstraint nodes.
type rec_flag = SurfaceSyntax.rec_flag =
| Nonrecursive
| Recursive 
type expression =
| EConstraint of expression * TypeCore.typ
| EVar of TypeCore.db_index
| EOpen of TypeCore.var
| EBuiltin of string
| ELet of rec_flag * patexpr list * expression
| EFun of (TypeCore.type_binding * TypeCore.flavor) list * TypeCore.typ * TypeCore.typ
* expression
| EAssign of expression * field * expression
| EAssignTag of expression * TypeCore.resolved_datacon
* tag_update_info
| EAccess of expression * field
| EApply of expression * expression
| ETApply of expression * tapp * Kind.kind
| EMatch of bool * expression * patexpr list
| ETuple of expression list
| EConstruct of TypeCore.resolved_datacon
* (TypeCore.Field.name * expression) list
| EIfThenElse of bool * expression * expression
* expression
| ELocated of expression * TypeCore.location
| EInt of int
| EExplained of expression
| EGive of expression * expression
| ETake of expression * expression
| EOwns of expression * expression
| EFail
This is not very different from SurfaceSyntax.expression. Some nodes such as ESequence have been removed.
type tapp =
| Ordered of TypeCore.typ
| Named of Variable.name * TypeCore.typ 
type patexpr = pattern * expression 
type declaration =
| DMultiple of rec_flag * patexpr list
| DLocated of declaration * TypeCore.location 
type declaration_group = declaration list 
type sig_item = Variable.name * TypeCore.typ 
type toplevel_item =
| DataTypeGroup of TypeCore.data_type_group
| ValueDeclarations of declaration_group
| PermDeclaration of sig_item 
type implementation = toplevel_item list 
type interface = toplevel_item list

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 : expression
The () (unit) expression.
val p_unit : pattern
The () (unit) pattern.
val eunloc : expression -> expression
Remove any ELocated node in front of an expression.

Substitution functions for types.


val tsubst_toplevel_items : TypeCore.typ ->
       TypeCore.db_index ->
       toplevel_item list -> toplevel_item list
val tpsubst_expr : TypeCore.env ->
       TypeCore.typ ->
       TypeCore.var -> expression -> expression

Substitution functions for expressions.


val esubst_toplevel_items : expression ->
       TypeCore.db_index ->
       toplevel_item list -> toplevel_item list
val epsubst : TypeCore.env ->
       expression ->
       TypeCore.var -> expression -> expression

Binding functions


type substitution_kit = {
   subst_type :TypeCore.typ -> TypeCore.typ;
   subst_expr :expression -> expression;
   subst_decl :declaration list -> declaration list;
   subst_pat :pattern list -> pattern list;
   vars :TypeCore.var 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 ->
       rec_flag ->
       (pattern * expression) list ->
       TypeCore.env * (pattern * 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.