You are looking at historical revision 22158 of this page. It may differ significantly from its current revision.

• eggs

miniML

Description

The miniML and miniMLeval libraries provide a type checker and interpreter for the mini-ML language described by Xavier Leroy in the paper A Modular Module System.

The procedures in miniML and miniMLeval are intended to be used with the API defined in the static-modules library.

Library Procedures in miniML

Predicates

[procedure] constant?:: OBJECT -> BOOL

A predicate for constants recognized by the interpreter. OBJECT must be of the form (TYPE VALUE), where value is a Scheme value and type is of the following symbols:

• nat (natural numbers)
• real (real numbers)
• bool (booleans)
• label (symbols)

[procedure] term?

A predicate for a mini-ML term. See the next section for a list of term constructors.

Term constructors

Const constant

constant

Longid path

identifier; see static-modules for a definition of the path type

Function identifier term

function; see static-modules for a definition of the identifier type

Apply term term

function application

Let0 identifier value term

Let-binding

Type constructors

Tvar tyvar

Tcon path type ...

Module system definitions

Definitions for the static-modules API:

• core-syntax
• core-typing
• core-scoping

Language environment initialization

[procedure] core-initialize:: enter-type enter-val -> VOID

Given procedures to add entries to a type environment, creates the constants of the mini-ML language.

Library procedures in miniMLeval

Support for evaluation is provided by the miniMLeval library.

Predicates

[procedure] value?

Value constructors

[procedure] Const_v
[procedure] Closure_v
[procedure] Prim_v
[procedure] Tuple_v

Evaluation

[procedure] core-eval-cbv
[procedure] eval-cbv-initialize
[procedure] mod-eval-cbv

Example interpreter

(require-extension datatype static-modules miniML miniMLsyntax miniMLparse miniMLeval)
(import (only data-structures compose)
 	 (only srfi-1 fold filter member delete-duplicates) 
 (only extras pp fprintf))


(define-values (env-binding? env-empty env-add-signature env-add-module env-add-type env-add-spec env-add-value
	        env-find-value env-find-type env-find-module env-find)
  (make-mod-env core-syntax))

(define-values (scope-typedecl scope-modtype scope-signature scope-modterm scope-moddef)
  (make-mod-scoping core-syntax core-scoping))

(define-values (check-modtype check-signature type-modterm type-moddef type-definition)
  (make-mod-typing core-syntax core-typing))

(define init-scope      (make-parameter st-empty))
(define init-type-env   (make-parameter env-empty))
(define init-eval-env   (make-parameter env-empty))

(define (enter-typedecl id decl)
  (init-scope (st-enter-type id (init-scope)))
  (init-type-env   (env-add-type id decl (init-type-env))))

(define (enter-valtype name ty)
  (let ((id (ident-create name)))
    (init-scope (st-enter-value id (init-scope)))
    (init-type-env   (env-add-value id ty (init-type-env)))))

(define (enter-val name val)
  (let ((id (or (and (ident? name) name) (ident-create name))))
    (init-eval-env (ident-add id val (init-eval-env)))))

(core-initialize enter-typedecl enter-valtype)
(eval-cbv-initialize enter-val)

(define (enter-module id mty)
  (init-scope (st-enter-module id (init-scope)))
  (init-type-env (env-add-module id mty (init-type-env))))

(define (interpreter operand)
  (let ((defs (parse 'miniML (open-input-file operand))))
    (let* ((scoped-defs      (scope-moddef (init-scope) defs))
	    (mty              (type-moddef (init-type-env) '() scoped-defs))
    (type-env         (map (lambda (x) (cases modspec x
					      (Value_sig (id vty) (cons id x))
 					      (Type_sig (id decl) (cons id x))
					      (Module_sig (id mty) (cons id x))
					      )) mty))
    (eval-env         (mod-eval-cbv (init-eval-env) scoped-defs))
    (unified-env      (list scoped-defs 
	 			   (filter (lambda (x) (not (assoc (car x) (init-type-env)))) type-env) 
				   (filter (lambda (x) (not (assoc (car x) (init-eval-env)))) eval-env) ))

	   )
      (pp unified-env)
      )))

(for-each interpreter (command-line-arguments))

Version History

• 1.0 Initial Release

License

miniML 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 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/>.