chickadee » miniML

Outdated egg!

This is an egg for CHICKEN 4, the unsupported old release. You're almost certainly looking for the CHICKEN 5 version of this egg, if it exists.

If it does not exist, there may be equivalent functionality provided by another egg; have a look at the egg index. Otherwise, please consider porting this egg to the current version of CHICKEN.

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

constant?:procedure

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)
  • string (strings)
term?procedure

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

core-initialize:procedure

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

parse:procedure

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

MLvalue?:procedure

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

core-eval-cbv:procedure

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

eval-cbv-initialize:procedure

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

mod-eval-cbv:procedure

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

Contents »