;;
;;  A language-independent module system, suitable for
;;  statically-typed languages.
;;
;;  Based on the code and paper by Xavier Leroy (2000): A modular
;;  module system. Journal of Functional Programming, 10, pp 269-303
;;  doi:10.1017/S0956796800003683
;;
;;
;; 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/>.
;;

(module static-modules
	
	(ident? ident-name ident-stamp ident-create ident-equal? ident-empty ident-add ident-find

	 path? Pident Pdot path-equal? 

	 subst-add subst-path subst-identity

	 typedecl? make-typedecl typedecl-manifest typedecl-kind

	 st-empty st-enter-value st-enter-type st-enter-module
	 st-value-path st-type-path st-module-path st-scope-module 

	 make-core-syntax make-core-typing make-core-scoping
	 core-syntax? core-typing? core-scoping?
         make-mod-syntax make-mod-env make-mod-typing make-mod-scoping

	 
	 make-mod-eval
	 )

	(import scheme chicken)
	(import (only data-structures alist-ref)
		(only extras fprintf pp))

	(require-extension srfi-1 datatype)


;; Section 2.1: Identifiers 


(define-record-type ident
  (make-ident name stamp)
  ident?
  (name   ident-name) 
  (stamp  ident-stamp)
  )

(define-record-printer (ident x out)
  (fprintf out "<~A>" (ident-name x)))

(define-values (ident-create ident-equal? ident-empty ident-add ident-find)
  (let* (
         (currstamp (make-parameter 0))
         (create (lambda (s) (currstamp (+ 1 (currstamp)))
                         (make-ident s (currstamp))))
         (equal (lambda (id1 id2) (= (ident-stamp id1) 
                                     (ident-stamp id2))))
         (empty '())
         (add   (lambda (id data tbl) 
                  (cons (cons id data) tbl)))
         (compare (lambda (x y) (equal? (ident-name x) (ident-name y))))
         (find  (lambda (id1 tbl)
                  (alist-ref id1 tbl compare)))
         )
    (values create equal empty add find)))


;; Section 2.2: Access paths 

(define-datatype path path?
  (Pident (id ident?)) ;; identifier
  (Pdot (p path?) (s string?))) ;; access to a module component

(define-record-printer (path x out)
  (cases path x
	 (Pident (id) (fprintf out "~A" (ident-name id)))
	 (Pdot (p s)  (fprintf out "~A.~A" p s))))

(define (path-equal? p1 p2)
  (cases path p1 
	 (Pident (id1) 
		 (cases path p2
			(Pident (id2) (equal? (ident-name id1) (ident-name id2)))
			(else #f)))
	 (Pdot (r1 field1)
	       (cases path p2
		      (Pdot (r2 field2)
			    (and (path-equal? r1 r2)
				 (equal? field1 field2)))
		      (else #f)))
	 (else #f)))

;; Section 2.3: Substitutions 

(define-values (subst-identity subst-add subst-path)
  (letrec ((identity ident-empty)
	   (add    ident-add)
	   (subst  (lambda (p sub)
		    (cases path p
			   (Pident (id) (or (ident-find id sub) p))
			   (Pdot (root field) (Pdot (subst root sub) field))))))
    (values identity add subst)))

;; Section 2.4: Abstract syntax for the base language 

(define-record-type core-syntax
  (make-core-syntax term? valtype? deftype? kind? make-valtype make-deftype subst-valtype subst-deftype subst-kind)
  core-syntax?
  (term?          cs-term?)
  (valtype?       cs-valtype?)
  (deftype?       cs-deftype?)
  (kind?          cs-kind?)
  (make-valtype   cs-make-valtype)
  (make-deftype   cs-make-deftype)
  (subst-valtype  cs-subst-valtype) 
  (subst-deftype  cs-subst-deftype)
  (subst-kind     cs-subst-kind)
  )


;; Section 2.5: Abstract syntax for the module language 


(define-record-type typedecl
  (make-typedecl kind manifest)
  typedecl?
  (kind      typedecl-kind) 
  (manifest  typedecl-manifest) ;; abstract or manifest type
  )


(define (make-mod-syntax core)

  (define (modsig? x) (every modspec? x))

  (define-datatype modtype modtype?
    (Signature (s modsig?)) ;; sig ... end
    (Functorty (id ident?) (mty1 modtype?) (mty2 modtype?))) ;; functor (X: mty) mty

  (define-datatype modspec modspec?
    (Value_sig  (id ident?) (valtype (cs-valtype? core))) ;; val x: ty
    (Type_sig   (id ident?) (decl typedecl?)) ;; type t :: k [= ty]
    (Module_sig (id ident?) (ty modtype?))) ;; module X: mty

  (define (modstruct? x) (every moddef? x))

  (define-datatype modterm modterm?
    (Modid      (p path?))  ;; X or X.Y.Z
    (Structure  (s modstruct?)) ;; struct ... end
    (Functor    (id ident?) (mty modtype?) (m modterm?)) ;; functor (X: mty) mod
    (Mapply     (m1 modterm?) (m2 modterm?)) ;; mod1 (mod2)
    (Constraint (m modterm?) (mty modtype?)))

  (define-datatype moddef moddef?
    (Value_def  (id ident?) (term (cs-term? core)))
    (Type_def   (id ident?) (kind (cs-kind? core)) 
	        (defty (cs-deftype? core)))
    (Module_def (id ident?) (m modterm?)))



  (define subst-kind (cs-subst-kind core))
  (define subst-deftype (cs-subst-deftype core))
  (define subst-valtype (cs-subst-valtype core))

  (define (subst-typedecl decl sub)
    (let ((manifest (typedecl-manifest decl)))
      (make-typedecl (subst-kind (typedecl-kind decl) sub)
		     (and manifest
			  (subst-deftype manifest sub)))))
			 

  (define (subst-modtype mty sub)
    (cases modtype mty
	   (Signature (sig) 
		      (Signature (map (lambda (x) (subst-modspec x sub)) sig)))
	   (Functorty (id mty1 mty2)
		      (Functorty id (subst-modtype mty1 sub) (subst-modtype mty2 sub)))))

  (define (subst-modspec x sub)
    (cases modspec x
	   (Value_sig (id vty)  (Value_sig id (subst-valtype vty sub)))
	   (Type_sig (id decl)  (Type_sig id (subst-typedecl decl sub)))
	   (Module_sig (id mty) (Module_sig id (subst-modtype mty sub)))))

  (values modtype? Signature Functorty 
	  modspec? Value_sig Type_sig Module_sig
	  modterm? Modid Structure Functor Mapply Constraint
	  moddef? Value_def Type_def Module_def
	  subst-modtype subst-modspec subst-typedecl)

)

;; Section 2.6: The environment structure 

(define (make-mod-env core)
  (let-values ((( modtype? Signature Functorty 
		  modspec? Value_sig Type_sig Module_sig
		  modterm? Modid Structure Functor Mapply Constraint
		  moddef? Value_def Type_def Module_def
		  subst-modtype subst-modspec subst-typedecl )  
		(make-mod-syntax core)))

    (define valtype? (cs-valtype? core))
    (define subst-valtype (cs-subst-valtype core))

    (define-datatype binding binding?
      (Value    (v valtype?))
      (Type     (decl typedecl?))
      (Module_  (t modtype?)))

    (define empty ident-empty)

    (define (add-value id vty env) (ident-add id (Value vty) env))
    (define (add-type id decl env) (ident-add id (Type decl) env))
    (define (add-module id mty env) (ident-add id (Module_ mty) env))

    (define (add-spec item env)
      (cases modspec item 
	     (Value_sig (id vty)  (add-value id vty env))
	     (Type_sig (id decl)  (add-type id decl env))
	     (Module_sig (id mty) (add-module id mty env))))

    (define add-signature  (lambda (sig env) (fold-right add-spec env sig)))

    (define (find p env)
      (cases path p
	     (Pident (id) (ident-find id env))
	     (Pdot (root field)
		   (cases modtype (find-module root env)
			  (Signature (sig) 
				     (find-field root field subst-identity sig))
			  (else (error 'find-field "structure expected in dot access" field))))))
						 
    (define (find-field p field subst lst)
      (if (null? lst)
	  (error 'find-field "No such field in structure" field)
	  (let ((x (car lst)))
	    (cases modspec x
		   (Value_sig (id vty)
			      (if (equal? (ident-name id) field)
				  (Value (subst-valtype vty subst))
				  (find-field p field subst (cdr lst))))

		   (Type_sig (id decl)
			     (if (equal? (ident-name id) field)
				 (Type (subst-typedecl decl subst))
				 (find-field p field
					     (subst-add id (Pdot p (ident-name id)) subst) 
					     (cdr lst))))

		   (Module_sig (id mty)
			       (if (equal? (ident-name id) field)
				   (Module_ (subst-modtype mty subst))
				   (find-field p field
					       (subst-add id (Pdot p (ident-name id)) subst)
					       (cdr lst))))))))

    (define (find-value path env)
      (let ((b (find path env)))
	(if (not b) (error 'find-value "value not found in environment" path))
	(cases binding b
	       (Value (vty) vty)
	       (else (error 'find-value "value field expected" b)))))


    (define (find-type path env)
      (let ((b (find path env)))
	(if (not b) (error 'find-type "type not found in environment" path))
	(cases binding b
	       (Type (decl) decl)
	       (else (error 'find-type "type field expected" b)))))


    (define (find-module path env)
      (let ((b (find path env)))
	(if (not b) (error 'find-module "module not found in environment" path))
	(cases binding b
	       (Module_ (mty) mty)
	       (else (error 'find-module "module field expected" b)))))


    (values binding? empty 
	    add-signature add-module add-type add-spec add-value
	    find-value find-type find-module find
	    )
    
    ))

;; Section 2.7: Type-checking the base language 


(define-record-type core-typing
  (make-core-typing type-term kind-deftype check-valtype check-kind
		    valtype-match deftype-equiv kind-match deftype-of-path)
  core-typing?
  ;; Typing functions 
  (type-term          ct-type-term)
  (kind-deftype       ct-kind-deftype)
  (check-valtype      ct-check-valtype)
  (check-kind         ct-check-kind)
  ;; Type matching functions 
  (valtype-match     ct-valtype-match)
  (deftype-equiv     ct-deftype-equiv)
  (kind-match        ct-kind-match)
  (deftype-of-path   ct-deftype-of-path))

;; Section 2.8: Type-checking the module language 

(define (make-mod-typing cs ct) ;; cs: core-syntax, ct: core-typing

  (define-values (modtype? Signature Functorty 
		     modspec? Value_sig Type_sig Module_sig
		     modterm? Modid Structure Functor Mapply Constraint
		     moddef? Value_def Type_def Module_def
		     subst-modtype subst-modspec subst-typedecl )  
    (make-mod-syntax cs))

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

  (define type-term          (ct-type-term ct))
  (define check-kind         (ct-check-kind ct))
  (define check-valtype      (ct-check-valtype ct))
  (define kind-deftype       (ct-kind-deftype ct))
  (define deftype-equiv      (ct-deftype-equiv ct))
  (define deftype-of-path    (ct-deftype-of-path ct))
  (define kind-match         (ct-kind-match ct))
  (define valtype-match      (ct-valtype-match ct))
  (define subst-valtype      (cs-subst-valtype cs))

  ;; Section 2.9: Matching between module types 
  (define (modtype-match env mty1 mty2)
      (cases modtype mty1
	     (Signature (sig1)
		(cases modtype mty2
		       (Signature (sig2)
				  (let* ((res (pair-signature-components sig1 sig2)) 
					 (paired-components (car res))
					 (subst (cadr res)))
				    (let* ((ext-env (add-signature sig1 env))
					   (spec-match (specification-match ext-env subst) ))
				      (for-each (lambda (p) (spec-match (car p) (cadr p)))
						paired-components))))
		       (else
			(error 'modtype-match "module type mismatch" mty1 mty2))))

	     (Functorty (param1 arg1 res1)
		(cases modtype mty2
  	          (Functorty (param2 arg2 res2)
		    (let* ((subst (subst-add param1 (Pident param2) subst-identity))
			   (res11 (subst-modtype res1 subst)))
		      (modtype-match env arg2 arg1)
		      (modtype-match (add-module param2 arg2 env) res11 res2)))
		  
		  (else
		   (error 'modtype-match "module type mismatch" mty1 mty2))))


	     (else
	      (error 'modtype-match "module type mismatch" mty1 mty2))))
	     

    (define (pair-signature-components sig1 sig2)
      (if  (null? sig2)  (list '() subst-identity)

	   (let ((item2 (car sig2))
		 (rem2  (cdr sig2)))

	     (letrec ((find-matching-component
		       (lambda (x)
			 (if (null? x)
			     (error 'find-matching-component
				    "unmatched signature component" sig1 sig2)
			     (let* ((item1 (car x))
				    (rem1  (cdr x))
				    (res   (cases modspec item1
					     (Value_sig (id1 _)
					       (cases modspec item2
						 (Value_sig (id2 _)
						    (and (equal? (ident-name id1) (ident-name id2))
							 (list id1 id2 item1)))
						 (else #f)))
					     
					     (Type_sig (id1 _) 
				               (cases modspec item2
					         (Type_sig (id2 _)
						   (and (equal? (ident-name id1) (ident-name id2))
							(list id1 id2 item1)))
						 (else #f)))
				  
					     (Module_sig (id1 _)
					       (cases modspec item2
					         (Module_sig (id2 _)
					           (and (equal? (ident-name id1) (ident-name id2))
							(list id1 id2 item1)))
						 (else #f)))
					     
					     (else #f))))
			       
			       (if res res (find-matching-component rem1)))))))

	       (let* ((comp  (find-matching-component sig1))
		      (id1   (car comp))
		      (id2   (cadr comp))
		      (item1 (caddr comp)))

		 (let* ((ps (pair-signature-components sig1 rem2))
			(pairs (car ps))
			(subst (cadr ps)))

		   (list (cons (list item1 item2) pairs)
			 (subst-add id2 (Pident id1) subst))
		   
		   ))
	       ))))
		   
		 
		   
   (define (specification-match env subst)
     (lambda (spec1 spec2)
       (cases modspec spec1
	      (Value_sig (_ vty1)
		(cases modspec spec2 
		  (Value_sig (_ vty2)

		     (if (not (valtype-match env vty1 (subst-valtype vty2 subst)))
			 (error 'specification-match
				"value components do not match"
				spec1 spec2)))
		  (else
		   (error 'specification-match
			  "components do not match"
			  spec1 spec2))))

	      
	      (Type_sig (id decl1)
		(cases modspec spec2 
		  (Type_sig (_ decl2)
		     (if (not (typedecl-match env id decl1 (subst-typedecl decl2 subst)))
			 (error 'specification-match
				"type components do not match"
				spec1 spec2)))
		  (else
		   (error 'specification-match
			  "components do not match"
			  spec1 spec2))))

	      (Module_sig (_ mty1)
		(cases modspec spec2 
		  (Module_sig (_ mty2)
		     (modtype-match env mty1 (subst-modtype mty2 subst)))
		  (else
		   (error 'specification-match
			  "components do not match"
			  spec1 spec2)))))))

	      
			       

    (define (typedecl-match env id decl1 decl2)
      (let ((k1 (typedecl-kind decl1))
	    (k2 (typedecl-kind decl2)))
	(and (kind-match env k1 k2)
	     (let ((m1 (typedecl-manifest decl1))
		   (m2 (typedecl-manifest decl2)))
	       (cond ((and m1 (not m2)) #t)
		     ((and m1 m2)
		      (deftype-equiv env k2 m1 m2))
		     ((and (not m1) m2)
		      (deftype-equiv env k2
			(deftype-of-path (Pident id) k1) m2)))))))

    ;; Section 2.10: Strengthening of module types 

    (define (strengthen-modtype path mty)
      (cases modtype mty 
	     (Signature (sg)   (let ((sig (map (lambda (item) (strengthen-spec path item)) sg)))
				 (Signature sig)))
	     (Functorty (_ _ _) mty)))

    (define (strengthen-spec path item)
      (cases modspec item 
	     (Value_sig (id vty) item)
	     (Type_sig (id decl)
		       (let ((m (or (typedecl-manifest decl)
				    (deftype-of-path (Pdot path (ident-name id)) (typedecl-kind decl)))))
			 (Type_sig id (make-typedecl (typedecl-kind decl) m))))
	     (Module_sig (id mty)
			 (Module_sig id (strengthen-modtype (Pdot path (ident-name id)) mty)))))
    
    ;; Continuation of section 2.8: Type-checking the module language 

    (define (check-modtype env mty)
      (cases modtype mty
	     (Signature (sg) 
			(check-signature env '() sg))
	     (Functorty (param arg res)
			(begin
			  (check-modtype env arg)
			  (check-modtype (add-module param arg env) res)))))

    (define (check-signature env seen sig)
	(if (null? sig)   '()
	    (let ((item (car sig))
		  (rem  (cdr sig)))
	      (cases modspec item
		     (Value_sig (id vty)
			(if (member (ident-name id) seen)
			    (error 'check-signature "repeated value name"
				   (ident-name id))
			    (begin
			      (check-valtype env vty)
			      (check-signature env 
					       (cons (ident-name id) seen) 
					       rem))))

		     (Type_sig (id decl)
			(if (member (ident-name id) seen)
			    (error 'check-signature "repeated type name"
				   (ident-name id))
			    (let ((m (typedecl-manifest decl)))
			      (check-kind env (typedecl-kind decl))
			      (if (not m) '()
				  (if (not (kind-match env (kind-deftype env m) 
						       (typedecl-kind decl)))
				      (error 'check-signature
					     "kind mismatch in manifest type specification"
					     decl)))
			      (check-signature (add-type id decl env)
					       (cons (ident-name id) seen)
					       rem))))

		     (Module_sig (id mty)
			(if (member (ident-name id) seen)
			    (error 'check-signature "repeated module name"
				   (ident-name id))
			    (begin
			      (check-modtype env mty)
			      (check-signature (add-module id mty env)
					       (cons (ident-name id) seen)
					       rem))))
		     ))))


    (define (type-modterm env mt)
      (cases modterm mt

	     (Modid (path)
		    (let ((m (find-module path env)))
		      (strengthen-modtype path m)))
	     
	     (Structure (str)
			(Signature (type-moddef env '() str)))

	     (Functor (param mty body)
		      (begin
			(check-modtype env mty)
			(Functorty param mty
				   (type-modterm (add-module param mty env) body))))

	     (Mapply (funct arg)
		     (cases modterm arg
			    (Modid (path)
			       (cases modtype (type-modterm env funct)
                                 (Functorty (param mty-param mty-res)
				    (let ((mty-arg (type-modterm env arg)))
				      (modtype-match env mty-arg mty-param)
				      (subst-modtype mty-res (subst-add param path subst-identity))))
				 (else (error 'type-modterm 
					      "application of a non-functor" funct))))
			    (else (error 'type-modterm
					 "argument in functor application is not a path to a module"
					 arg))))

	     (Constraint (modl mty)
		(begin
		  (check-modtype env mty)
		  (modtype-match env mty (type-modterm env modl))
		  mty
		  ))
	     ))


    (define (type-moddef env seen struct)
      (if (null? struct) '()
	  (let ((def     (car struct))
		(rem     (cdr struct)))
	    (let* ((res (type-definition env seen def))
		   (sigitem (car res))
		   (seen1   (cadr res)))
	      (cons sigitem (type-moddef (add-spec sigitem env) seen1 rem))))))
	      

    (define (type-definition env seen def)
      (cases moddef def
	     (Value_def (id term)
			(if (member (ident-name id) seen)
			    (error 'type-definition "repeated value name" (ident-name id))
			    (list (Value_sig id (type-term env term))
				  (cons (ident-name id) seen))))
	     
	     (Module_def (id modl)
			 (if (member (ident-name id) seen)
			     (error 'type-definition "repeated module name" (ident-name id))
			     (list (Module_sig id (type-modterm env modl))
				   (cons (ident-name id) seen))))


	     (Type_def  (id kind typ)
			(if (member (ident-name id) seen)
			    (error 'type-definition "repeated type name" (ident-name id))
			    (begin
			      (check-kind env kind)
			      (if (not (kind-match env (kind-deftype env typ) kind))
				  (error 'type-definition "kind mismatch" kind))
			      (list (Type_sig id (make-typedecl kind typ))
				    (cons (ident-name id) seen)))))))

    (values check-modtype check-signature
	    type-modterm type-moddef type-definition)

    )
#|

 Generic ``scoping'' pass for the module language.  This pass is not
described in the article.

  Scoping is the act of associating identifiers with their binding
location.  Here we assume that the parser generates fresh
identifiers (values of type Ident.t) 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. 

|#

;;   A scoping structure is a table recording (name, identifier)
;;   associations for value names, type names and module names.


(define-record-type scoping-table
  (make-scoping-table values types modules)
  scoping-table?
  (values             st-values)
  (types              st-types)
  (modules            st-modules))


(define update-scoping-table
  (let ((unset (list 'unset)))
    (lambda (sc #!key (values unset) (types unset) (modules unset) )
      (make-scoping-table
       (if (eq? values unset) (st-values sc) values)
       (if (eq? types unset) (st-types sc) types)
       (if (eq? modules unset) (st-modules sc) modules)))))

(define-values (st-empty st-enter-value st-enter-type st-enter-module
			 st-value-path st-type-path st-module-path
			 st-scope-module )
  (letrec (
           (empty        (make-scoping-table '() '() '()))
           (enter-value  (lambda (id sc)
                           (update-scoping-table sc
			     values: (cons (list (ident-name id) id) (st-values sc)))))
           (enter-type   (lambda (id sc)
                           (update-scoping-table sc
			     types: (cons (list (ident-name id) id) (st-types sc)))))
           (enter-module  (lambda (id sc)
                            (update-scoping-table sc
			      modules: (cons (list (ident-name id) id) (st-modules sc)))))
           (scope-value   (lambda (id sc)
                            (or (assoc (ident-name id) (st-values sc))
                                (error 'scope-value "unbound value" (ident-name id)))))
           (scope-type    (lambda (id sc)
                            (or (assoc (ident-name id) (st-types sc))
                                (error 'scope-type "unbound type" (ident-name id)))))
           (scope-module  (lambda (id sc)
                            (or (assoc (ident-name id) (st-modules sc))
                                (error 'scope-module "unbound module" (ident-name id)))))
           (scope-path    (lambda (scope-ident)
                            (lambda (p sc)
                              (cases path p
                                     (Pident (id)        (Pident (cadr (scope-ident id sc))))
                                     (Pdot (root field)  (Pdot ((scope-path scope-module) root sc) field))))))
           )
    (let (
          (value-path    (scope-path scope-value))
          (type-path     (scope-path scope-type))
          (module-path   (scope-path scope-module))
          )

      (values empty enter-value  enter-type enter-module
              value-path type-path module-path scope-module)
      ))
  )


;; The scoping pass for the core language 

(define-record-type core-scoping
  (make-core-scoping scope-term scope-valtype scope-deftype scope-kind)
  core-scoping?
  (scope-term     csc-scope-term)
  (scope-valtype  csc-scope-valtype)
  (scope-deftype  csc-scope-deftype)
  (scope-kind     csc-scope-kind))


;; The scoping pass for the module language is then as follows. 

(define (make-mod-scoping cs csc) ;; cs: core-syntax, csc: core-scoping

  (let-values ((( modtype? Signature Functorty 
		  modspec? Value_sig Type_sig Module_sig
		  modterm? Modid Structure Functor Mapply Constraint
		  moddef? Value_def Type_def Module_def
		  subst-modtype subst-modspec subst-typedecl )  
		(make-mod-syntax cs)))
    
    (define scope-kind (csc-scope-kind csc))
    (define scope-deftype (csc-scope-deftype csc))
    (define scope-valtype (csc-scope-valtype csc))
    (define scope-term    (csc-scope-term csc))

    (define (scope-typedecl sc decl)
      (let ((m (typedecl-manifest decl)))
	(make-typedecl (scope-kind sc (typedecl-kind decl))
		       (if (not m) #f (scope-deftype sc m)))))

    (define (scope-modtype sc mty)
      (cases modtype mty
	     (Signature (sg) 
			(Signature (scope-signature sc sg)))
	     (Functorty (id arg res)
			(scope-modtype (st-enter-module id sc) res))))

    (define (scope-signature sc x)
      (if (null? x) '()
	  (let ((rem (cdr x)))
	    (cases modspec (car x)
		   (Value_sig (id vty)
			      (cons (Value_sig id (scope-valtype sc vty))
				    (scope-signature (st-enter-value id sc) rem)))
		   (Type_sig (id decl)
			     (cons (Type_sig id (scope-typedecl sc decl))
				   (scope-signature (st-enter-type id sc) rem)))
		   (Module_sig (id mty)
			       (cons (Module_sig id (scope-modtype sc mty))
				     (scope-signature (st-enter-type id sc) rem)))))))

    (define (scope-modterm sc mt)
      (cases modterm mt
	     (Modid (path)    
		    (Modid (st-module-path path sc)))
	     (Structure (str)  
			(Structure (scope-moddef sc str)))
	     (Functor (id arg body)
		      (Functor id (scope-modtype sc arg)
			       (scope-modterm (st-enter-module id sc) body)))
	     (Mapply (m1 m2) 
		     (Mapply (scope-modterm sc m1) (scope-modterm sc m2)))
	     (Constraint (m mty)
			 (Constraint (scope-modterm sc m)
				     (scope-modtype sc mty)))))

    (define (scope-moddef sc defs)
      (if (null? defs) '()
	  (let ((rem (cdr defs)))
	    (cases moddef (car defs)
		   (Value_def (id v)
			      (cons (Value_def id (scope-term sc v))
				    (scope-moddef (st-enter-value id sc) rem)))
		   (Type_def (id kind dty)
			     (cons (Type_def id (scope-kind sc kind) (scope-deftype sc dty))
				   (scope-moddef (st-enter-type id sc) rem)))
		   (Module_def (id m)
			       (cons (Module_def id (scope-modterm sc m))
				     (scope-moddef (st-enter-module id sc) rem)))))))


    (values scope-typedecl scope-modtype scope-signature scope-modterm scope-moddef)
    ))

;; Support for evaluation

(define (make-mod-eval core-syntax core-eval enter-val)

  (let-values ((( modtype? Signature Functorty 
		  modspec? Value_sig Type_sig Module_sig
		  modterm? Modid Structure Functor Mapply Constraint
		  moddef? Value_def Type_def Module_def
		  subst-modtype subst-modspec subst-typedecl )  
		(make-mod-syntax core-syntax)))
    

    (define-datatype modval modval?
      (Structure_v    (env list?))
      (Mclosure_v     (body modterm?) (env list?))
      )

    (define (path-find-val p env)
      (cases path p
	     (Pident (id)  
		     (ident-find id env))
	     (Pdot (root field)
		   (cases modval (find-module-val root env)
			  (Structure_v (env1) (let ((field1 (or (and (ident? field) field) (ident-create field))))
						(ident-find field1 env1)))
			  (else (error 'path-find-val "structure expected in dot access" p))))))

    (define (find-module-val path env)
      (let ((v (path-find-val path env)))
	(if (not v) (error 'find-module-val "path not found" path))
	(if (not (modval? v)) (error 'find-module-val "module expected" path))
	v))

  (define (eval-modterm t env)
    (cases modterm t
	   (Modid      (p) (find-module-val p env))

	   (Structure  (str)
		       (let* ((env0 env)
			      (env1 (fold eval-moddef env0 str))
			      (menv (lset-difference (lambda (x y) (ident-equal? (car x) (car y))) env1 env0)))
			 (Structure_v menv)))

	   (Functor    (id mty mt)
		       (Mclosure_v t env))

	   (Mapply     (m1 m2)
		       (cases modval (eval-modterm m1 env)
			      (Mclosure_v (t env1) 
				(cases modterm t 
				       (Functor (id mty mt)
					(let* ((v2 (eval-modterm m2 env))
					       (env2 (enter-val id v2 env1)))
					  (eval-modterm mt env2)))
				       (else
					(error 'eval-modterm "functor expected in application" t))))
			      (error 'eval-modterm "module closure expected in application" m1)
			      ))
					
	   (Constraint (m mty) (eval-modterm m env))
	   ))

  (define (eval-moddef d env)
    (cases moddef d
	   (Value_def  (id term)  
		       (enter-val id (core-eval term env) env))

	   (Type_def   (id kind defty)  
		       (enter-val id d env))
		       
	   (Module_def (id mt)
		       (enter-val id (eval-modterm mt env) env))
	   ))

  (values modval? Structure_v Mclosure_v path-find-val find-module-val 
	(lambda (env dlst)
	  (fold eval-moddef env dlst)))

))


)