1. miniML
    1. Description
    2. miniML library
      1. Predicates
      2. Term constructors
      3. Type constructors
      4. Module system definitions
      5. Language environment initialization
    3. miniMLsyntax library
    4. miniMLparse library
    5. miniMLeval library
      1. Predicates
      2. Value constructors
      3. Evaluation
    6. Example interpreter
    7. Version History
    8. License

miniML

Description

The libraries in the miniML egg provide a parser, 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 for type checking and evaluation defined in the static-modules library.

miniML library

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:

[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 tycon type ...

Module system definitions

Definitions for the static-modules API:

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.

The following types and constants are currently included:

Type 'a -> 'b
Type 'a * 'b
Type 'a list
Type real
Type nat
Type bool
Type label
Type string
Type bot
Constant false : bool
Constant true : bool
Constant empty : bot
Constants add sub mul div : nat -> nat -> nat
Constants == <> < <= > >= : nat -> nat -> bool
Constant pair : 'a -> 'b -> 'a * 'b
Constant fst : 'a * 'b -> 'a
Constant snd : 'a * 'b -> 'b
Constant null : 'a list
Constant cons : 'a -> a' list -> 'a list
Constant head : a' list -> 'a
Constant tail : a' list -> 'a list
Constant cond : bool -> 'a -> 'a -> 'a

miniMLsyntax library

The miniMLsyntax library contains mini-ML module syntax constructors defined with static-modules:

modtype? Signature Functorty
modspec? Value_sig Type_sig Module_sig
modterm? Modid Structure Functor Mapply Constraint
moddef? Value_def Type_def Module_def

miniMLparse library

[procedure] parse:: PORT-OR-STRING -> MODDEF LIST

Given a port or a string, the parse procedure parses the given text, and returns a list of mini-ML module definitions.

miniMLeval library

The miniMLeval library provides support for mini-ML evaluation.

Predicates

[procedure] MLvalue?:: OBJECT -> BOOL

Returns #t if the given object is a mini-ML value, #f otherwise. The following values are supported:

Value constructors

Const_v constant
constants
Closure_v term env
closures
Prim_v procedure
invocations of primitive procedures
Tuple_v slots
tuples (represented as Scheme lists)

Evaluation

[procedure] core-eval-cbv:: TERM * VALUE-ENV -> VALUE

Given a mini-ML term and value environment, evaluates the term using a call-by-value strategy and returns the resulting value.

[procedure] eval-cbv-initialize:: ENTER-VAL -> VALUE-ENV

Initializes a given evaluation environment with the primitives of the mini-ML language.

[procedure] mod-eval-cbv:: MODTERM -> VALUE-ENV

A module definition evaluator based on core-eval-cbv and static-modules.

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

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