1. static-modules
    1. Description
    2. Library Procedures
      1. Identifiers
      2. Access paths
      3. Substitutions
      4. Abstract syntax for the base language
      5. Abstract syntax for the module language
      6. Type-checking the base language
      7. Type-checking the module language
      8. Scoping
      9. Evaluation
    3. Version History
    4. License

static-modules

Description

static-modules is a Scheme implementation of the module system described by Xavier Leroy in the paper A Modular Module System.

Library Procedures

Identifiers

[procedure] (ident? X) -> BOOL

Returns #t if X is an identifier, #f otherwise.

[procedure] (ident-name IDENT) -> STRING

Returns the string name associated with the given identifier.

[procedure] (ident-stamp IDENT) -> INT

Returns the unique stamp of the given identifier.

[procedure] (ident-create NAME) -> IDENT

Returns a fresh identifier associated with the given name.

[procedure] (ident-equal? IDENT IDENT) -> BOOL

Returns #t if the stamps of the given identifiers are equal, #f otherwise.

[procedure] (ident-empty) -> IDENV

Returns an empty identifier environment.

[procedure] (ident-add IDENT DATA IDENV) -> IDENV

Adds the given identifier and associated data to the given identifier environment.

[procedure] (ident-find IDENT IDENV) -> DATA

Looks up the given identifier in the given identifier environment and returns the associated data, or #f if not found.

Access paths

We refer to named types, values (variables), and modules either by identifier (if we are in the scope of their binding) or via the dot notation, e.g. M.x to refer to component x of module M. Access paths represent both kinds of references.

[procedure] (path? X) -> BOOL

Returns #t if X is an access path, #f otherwise.

[procedure] (Pident IDENT) -> PATH

Returns a path consisting of the given identifier.

[procedure] (Pdot PATH STRING) -> PATH

Returns an access path for the given path and field.

[procedure] (path-equal? PATH PATH) -> BOOL

Returns #t if the two given paths are equal, #f otherwise.

Substitutions

[procedure] (subst-add IDENT PATH IDENV) -> IDENV

Extends the substition environment with the given identifier and path.

[procedure] (subst-path PATH IDENV) -> PATH

Applies the given substitutions to the given path.

[procedure] (subst-identity) -> IDENV

Returns an empty substitution environment.

Abstract syntax for the base language

[procedure] (make-core-syntax term? valtype? deftype? kind? make-valtype make-deftype subst-valtype subst-deftype subst-kind)

This procedure creates the structure describing base language syntax. The meaning of the fields is as follows:

Abstract syntax for the module language

[procedure] (make-mod-syntax core)

This procedure creates the structure describing module language syntax. core is an object created by make-core-syntax. This procedure returns multiple values with the following meaning:

Type-checking the base language

[procedure] (make-core-typing type-term kind-deftype check-valtype check-kind valtype-match deftype-equiv kind-match deftype-of-path)

This procedure creates the structure describing base language type checking. The meaning of the fields is as follows:

Type-checking the module language

[procedure] (make-mod-typing core-syntax core-typing)

This procedure creates the structure describing module language type checking. core-syntax is an object created by make-core-syntax, and core-typing is an object created by make-core-typing. This procedure returns multiple values with the following meaning:

Scoping

This library implements generic scoping pass for the module language. This pass is not described in the paper.

Scoping is the act of associating identifiers with their binding location. We assume that the parser generates fresh identifiers each time it encounters an occurrence of a lexical identifier in the program, and stores those fresh identifiers in the abstract syntax tree it constructs. The scoping pass rewrites the abstract syntax tree to use identical identifiers at a binding site and at all its usage sites.

[procedure] st-empty

Empty scoping table.

[procedure] (st-enter-value ID SC) -> SC

Enters a value identifier in the given scoping table.

[procedure] (st-enter-type ID SC) -> SC

Enters a type identifier in the given scoping table.

[procedure] (st-enter-module ID SC) -> SC

Enters a module identifier in the given scoping table.

[procedure] (st-value-path PATH SC) -> PATH
[procedure] (st-type-path PATH SC) -> PATH
[procedure] (st-module-path PATH SC) -> PATH
[procedure] (st-scope-module PATH SC) -> PATH

Evaluation

[procedure] (make-mod-eval core-syntax core-eval enter-val)

This procedure creates the structure describing module language type checking. core-syntax is an object created by make-core-syntax, and core-eval is a procedure to evalue core syntactic terms. This procedure returns multiple values with the following meaning:

Version History

License

static-modules is based on the code and paper by Xavier Leroy (2000): A modular module system. Journal of Functional Programming, 10, pp 269-303

Copyright 2010-2013 Ivan Raikov and the Okinawa Institute of
Science and Technology.

This program is free software: you can redistribute it and/or
modify it under the terms of the GNU General Public License as
published by the Free Software Foundation, either version 3 of the
License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

A full copy of the GPL license can be found at
<http://www.gnu.org/licenses/>.