#!/bin/sh
#	This is a shell archive.
#	Run the file through sh to extract its contents.
# shar:	Shell Archiver
#	Run the following text with /bin/sh to create:
#	top.s
#	chez-support.s
#	data-structures.s
#	mgu.s
#	check-exp.s
# This archive created: Tue Nov  7 11:24:42 1989
echo shar: extracting top.s '(918 characters)'
sed 's/^X//' << \SHAR_EOF > top.s
X;;; top.s  
X
X;;; boot loader for SPS
X;;; Thu Nov 10 14:49:52 1988
X
X(define spsdir "/fiona/csfaculty/wand/sps/new/")
X
X(define sload
X  (lambda (name)
X    (load (string-append spsdir name))))
X
X(sload "chez-support.s")			; chez scheme specific
X					; functions.
X
X(sload "data-structures.s")		; definitions of data
X					; structures, etc.
X
X(sload "mgu.s")				; the unifier
X
X(sload "check-exp.s")			; the basic typechecking algorithm.
X
X(sload "defining-forms.s")		; define-checked, etc.
X
X(sload "type-constructors.s")		; define-record-type,
X					; define-type-constructor.
X
X(sload "globals.s")			; types for Scheme globals and
X					; standard constructors
X
X
X(sload "scanner.s")                      ; interpreter for lexical
X					; scanners
X
X(sload "ll-parsers.s")                   ; LL parser generator and
X					; interpreter
X
X(sload "grammars.s")                     ; define-grammar,
X					; define-unchecked-grammar. 
X
X
SHAR_EOF
if test 918 -ne "`wc -c top.s`"
then
echo shar: error transmitting top.s '(should have been 918 characters)'
fi
echo shar: extracting chez-support.s '(493 characters)'
sed 's/^X//' << \SHAR_EOF > chez-support.s
X;;; Auxiliary functions for simulating random Scheme84 calls in Chez
X;;; Scheme
X
X(define (ptime) (list (cpu-time) 0))		; 2nd component should
X						; be gc-time.
X
X(define checker-time 0)
X
X(define mgu-time (cons 0 nil))
X
X(define ctime
X  (lambda ()
X    (append (ptime) (list checker-time (car mgu-time)))))
X
X(define syntactic-extension?
X  (lambda (symbol)
X    (getprop symbol '*expander*)))
X
X(define report-error
X  (lambda (msg)
X    (pretty-print msg)
X    (reset)))
X
X(define gen-fcn-sym gensym)
SHAR_EOF
if test 493 -ne "`wc -c chez-support.s`"
then
echo shar: error transmitting chez-support.s '(should have been 493 characters)'
fi
echo shar: extracting data-structures.s '(6948 characters)'
sed 's/^X//' << \SHAR_EOF > data-structures.s
X;;; Data Structures for SPS
X
X;;; Created Sat Nov  5 10:31:43 1988
X
X;;; ****************************************************************
X
X;;; Types
X
X;;; should have explicit syntax for these.
X
X;;; type ::= atom | (constructor . args)
X
X(define gen-type-var gensym)		; this should be a little cleverer
X(define var? atom?)  ;; this should be typevar? (maybe?)
X
X(define type->constructor car)
X(define type->args  cdr)
X
X(define make-type
X  (lambda (constructor args) (cons constructor args)))
X
X(define make-functional-type
X  (lambda (arg-types result-type)
X    `(-> (seq . ,arg-types) ,result-type)))
X
X;;; ****************************************************************
X
X;;; Type Schemes
X
X;;; type-scheme ::= (quantified-variables type)
X;;; quantified-variables ::= list of type variables free in the type.
X
X;;; (make-type-scheme typevars type)
X;;; (type-scheme->generics type-scheme)
X;;; (type-scheme->type type-scheme)
X;;; (subst-gensyms-for-generics type-scheme)  --returns a type
X;;; (external-type->type-scheme external-type) 
X
X(define make-type-scheme
X  (lambda (typevars type) (list typevars type)))
X(define type-scheme->generics car)
X(define type-scheme->type     cadr)
X
X(define subst-gensyms-for-generics
X  (lambda (type-scheme) 
X    (let* ((generics (type-scheme->generics type-scheme)) 
X	   (type-exp (type-scheme->type type-scheme))
X	   (newvars (mapcar (lambda (x) (gen-type-var)) generics))
X	   (table (ext-ribcage generics newvars nil)))
X      (letrec ((loop
X		(lambda (x)
X		  (cond ((null? x) x)
X			((and (atom? x) (memq x generics))
X			 (car (assq-ribcage x table)))
X			((atom? x)  x)
X			(else  (cons (loop (car x)) (loop (cdr x))))))))
X	(loop type-exp)))))
X
X
X(define subst-consts-for-generics
X  (lambda (type-scheme) 
X    (let* ((generics (type-scheme->generics type-scheme)) 
X	   (type-exp (type-scheme->type type-scheme))
X	   (newconsts
X	     (mapcar
X	       (lambda (x) (make-type (gen-type-var) '()))
X	       generics))
X	   (table (ext-ribcage generics newconsts nil)))
X      (letrec ((loop
X		 (lambda (x)
X		   (cond ((null? x) x)
X		     ((and (atom? x) (memq x generics))
X		      (car (assq-ribcage x table)))
X		     ((atom? x)  x)
X		     (else  (cons (loop (car x)) (loop (cdr x))))))))
X	(loop type-exp)))))
X
X;;; external-type->type-scheme takes an external type (possibly of the form)
X;;; (generic (x) ...) and converts it into a type scheme.
X
X(define external-type->type-scheme
X  (lambda (external-type) 
X    (cond
X      [(var? external-type)
X	(make-type-scheme '() external-type)]
X      [(eq? (car external-type) 'generic)
X       (make-type-scheme (cadr external-type) (caddr external-type))]
X      [else
X	(make-type-scheme '() external-type)])))
X
X;;; ****************************************************************
X
X;;; type environments.
X
X;;; maps type variables to type expressions (what about quantifiers?
X;;; they are only in type hypotheses.)
X
X;;; Operations:
X;;; isbound? var env
X;;; is-locally-bound? var env
X;;; lookup-typevar var env
X;;; empty-type-env          --added Sat Nov  5 10:35:24 1988
X;;; extend-type-env var type env --added Sat Nov  5 10:36:52 1988
X
X;;; bad-typevar? var   -- a mystery
X
X(define bad-typevar? (lambda (x) #f))	; a stub
X
X;;; current representation:  a-list (passable to assq) -- nil defaults
X;;; to global-type-env.
X;;; global-type-env is another a-list.
X
X(define empty-type-env '())
X
X(define extend-type-env
X  (lambda (var type env)
X    (cons (cons var type) env)))
X
X(define isbound?
X  (lambda (var env)
X    (or (assq var env) (assq var global-type-env))))
X
X(define is-locally-bound? assq)
X
X(define lookup-typevar
X  (lambda (var env)
X    (let ((pair (assq var env)))
X      (if pair
X	  (cdr pair)
X	  (cdr (assq var global-type-env))))))
X
X;;; global type environment
X
X(define global-type-env '())
X
X(define initialize-global-type-env!
X  (lambda ()
X    (set! global-type-env '())))
X
X(define extend-global-type-env!
X  (lambda (var type)
X    (set! global-type-env (cons (cons var type) global-type-env))))
X
X;;; ****************************************************************
X
X;;; Ribcages
X
X;;; Operations:
X
X;;; empty-ribcage
X;;; (ext-ribcage vbles vals env)
X;;; (assq-ribcage var ribcage)  --returns list with value in car, or
X;;; else #f  -- this should be changed to take success and failure
X;;; continuations, and return value (not list) to the success continuation.
X
X(define empty-ribcage '())
X
X(define ext-ribcage
X  (lambda (vbles vals env)
X    (cons (cons vbles vals) env)))
X
X(define assq-ribcage
X  (lambda (var env)
X    (if (null? env)
X	#f
X	(letrec ((loop
X		  (lambda (vars cells)
X		    (if (null? vars)
X			(assq-ribcage var (cdr env))
X			(if (eq? var (car vars))
X			    cells
X			    (loop (cdr vars) (cdr cells)))))))
X	  (loop (caar env) (cdar env))))))
X
X;;; ****************************************************************
X
X;;; Type Hypotheses (or Assumptions or Prefixes)
X
X;;; type-hypotheses simulates a function from variables to type-schemes
X
X;;; Operations:
X
X;;; empty-prefix
X
X;;; (ext-prefix list-of-type-variables list-of-typeschemes prefix)
X;;; (lookup-symbol-type variable type-hypotheses failure-continuation)
X
X;;; Representation:
X
X;;; type-hypotheses ::= ribcage of type-schemes;  empty ribcage
X;;; means global type assumptions.  
X
X;;; assq-ribcage sucks, and should be replaced by something sensible.
X
X
X(define empty-prefix empty-ribcage)
X
X(define ext-prefix
X  (lambda (vbles schemes p)
X    (ext-ribcage vbles schemes p)))
X
X(define lookup-symbol-type
X  (lambda (var p fail)		; p is a ribcage
X    (let
X      ((ans (assq-ribcage var p))); assq-ribcage returns cell w/ data in car
X      (if ans 
X	  (subst-gensyms-for-generics (car ans))
X	  (let
X	    ((ans (lookup-global-type var)))
X	    (if ans
X		(subst-gensyms-for-generics ans)
X		(fail `(untyped-identifier ,var))))))))
X
X
X; this may be bogus:
X(define lookup-in-prefix assq-ribcage)
X
X
X;;; ****************************************************************
X
X;;; global-prefix
X
X;;; lookup-global-type returns type-scheme, else #f.
X;;; use of putprop and getprop is not RRRS, but is chez-scheme specific.
X
X;;; the following two are bogus if we use property lists:
X
X(define global-prefix empty-ribcage)	
X(define initialize-global-prefix!
X  (lambda () (set! global-prefix empty-ribcage)))
X
X(define lookup-global-type
X  (lambda (var) (getprop var 'global-type)))
X
X(define change-global-prefix!
X  (lambda (var type-scheme)
X    (putprop var 'global-type type-scheme)))
X
X;;; ****************************************************************
X
X;;; Checker-result
X
X;;; checker-result ::= (type type-env)
X
X;;; may need to return (type generic-vbles type-env) to accomodate LET
X;;; properly?? 
X
X(define make-checker-result
X  (lambda (type type-env) (list type type-env)))
X
X(define checker-result->type  car)
X(define checker-result->env   cadr)
X
X;;; ****************************************************************
X
X;;; Source terms (expressions, forms, etc.)
X
X(define make-application
X  (lambda (fn-exp arg-exps) (cons fn-exp arg-exps)))
SHAR_EOF
if test 6948 -ne "`wc -c data-structures.s`"
then
echo shar: error transmitting data-structures.s '(should have been 6948 characters)'
fi
echo shar: extracting mgu.s '(4389 characters)'
sed 's/^X//' << \SHAR_EOF > mgu.s
X;;; -*-Scheme-*-
X;;;
X;;; mgu algorithms
X;;;
X
X;;; 30 Oct 88 identified major structures and code to be fixed -- mw
X;;;  (with help from margaret)
X
X;;; Revision 1.6  85/01/11  15:08:49  mw
X
X;;; Revision 1.1  83/08/25  14:49:08  mw
X;;; Initial revision
X
X;;;; Most General Unifier
X
X;; (declare (usual-integrations)) ;; for C-scheme
X
X;;; ****************************************************************
X
X;;; seen-list : a list of nodes, without duplications.  This is
X;;; obsolescent, and will be eliminated when we use congruence.
X
X(define seen? memq)
X
X(define add-to-seen
X  (lambda (x l)
X    (if (memq x l)
X	l
X	(cons x l))))
X
X;;; ****************************************************************
X
X;;; mgu:  calls mgu-body wrapped in a timer.  Need to replace by
X;;; uniform instrumentation package.
X
X;;; Arguments:
X;;; t1, t2 -- type expressions, with free variables
X;;; env   -- a type env
X;;; succeed -- continuation for success, expects a type env
X;;; fail -- continuation for failure, expects a message.
X
X(define mgu
X  (lambda (t1 t2 env succeed fail)
X    (let ((start (ptime)))
X      (mgu-body t1 t2 env
X		(lambda (x) (update-mgu-clock! start) (succeed x))
X		(lambda (x) (update-mgu-clock! start) (fail x))))))
X
X(define update-mgu-clock!
X  (lambda (start)
X    (set-car! mgu-time (+ (car mgu-time)
X			  (- (- (car (ptime)) (car start))
X			     (- (cadr (ptime)) (cadr start)))))))
X
X;;; ****************************************************************
X
X;;; mgu-body.  Does main work of mgu.  
X
X(define mgu-body
X  (lambda (t1 t2 env succeed fail)
X    (letrec ((loop
X	       (lambda (t1 seen1 t2 seen2 env succeed)
X		 (cond ((and (eq? t1 t2)
X			     (not (bad-typevar? t1))
X			     (not (bad-typevar? t2)))
X			(succeed env))
X		   ((var? t1)
X		    (cond ((isbound? t1 env)
X			   (if (and (seen? t1 seen1)
X				    (var? t2)
X				    (seen? t2 seen2))
X			     (compare-looping-structures t1 t2 env
X			       succeed fail)
X			     (loop (lookup-typevar t1 env)
X				   (add-to-seen t1 seen1)
X				   t2 seen2 env succeed)))
X		      ((and (var? t2) (isbound? t2 env))
X		       (loop t1 seen1 (lookup-typevar t2 env)
X			 (add-to-seen t2 seen2) env succeed))
X		      ((bad-typevar? t1)  (fail `(undefined-type: ,t1)))
X		      ((bad-typevar? t2)  (fail `(undefined-type: ,t2)))
X		      (else  (succeed (extend-type-env t1 t2 env)))))
X		   ((var? t2)
X		    (loop t2 seen2 t1 seen1 env succeed))
X		   ((not (eq? (type->constructor t1) (type->constructor t2)))
X		    (fail `(mismatch: ,t1 ,t2)))
X		   (else
X		     (letrec ((inner	; loop thru subterms
X				(lambda (l1 l2 env)
X				  (if (null? l1)
X				    (succeed env)
X				    (loop (car l1) seen1 (car l2) seen2 env
X				      (lambda (env)
X					(inner (cdr l1)
X					       (cdr l2)
X					       env)))))))
X		       (cond ((eq? (type->constructor t1) 'seq)
X			      (unify-seq-tails
X				(type->args t1) (type->args t2) inner env
X				fail succeed))
X			 ((eq? (length t1) (length t2))
X			  (inner (type->args t1) (type->args t2) env))
X			 (else
X			   (fail `(wrong-no-of-args-to-constructor:
X				    ,t1 ,t2))))))))))
X      (loop t1 nil t2 nil env succeed))))
X
X;;; compare-looping-structures is known to be buggy, but will be
X;;; replaced when we go to congruence closure algorithm.
X
X(define compare-looping-structures
X  (lambda (t1 t2 env succeed fail)
X    (letrec ((loop
X	      (lambda (t1 t2)
X		(cond ((var? t1)  (loop (lookup-typevar t1 env) t2))
X		      ((var? t2)  (loop t1 (lookup-typevar t2 env)))
X		      ((eq? (car t1) (car t2))  (succeed env))
X		      (else  (fail `(unmatched-loop: ,t1 ,t2)))))))
X      (loop t1 t2))))
X
X(define unify-seq-tails
X  (lambda (l1 l2 inner env fail succeed)
X    (cond ((and l1 (atom? l1))
X	   (cond ((isbound? l1 env)
X		  (unify-seq-tails (lookup-typevar l1 env) l2 inner env
X				   fail succeed))
X		 ((bad-typevar? l1)
X		  (fail `(undefined-type: ,l1)))
X		 ((bad-typevar? l2)
X		  (fail `(undefined-type: ,l2)))
X		 ((eq? l1 l2)
X		  (succeed env))
X		 (else
X		  (succeed (cons (cons l1 l2) env)))))
X	  ((and l2 (atom? l2))
X	   (unify-seq-tails l2 l1 inner env fail succeed))
X	  ((eq? (length l1) (length l2))
X	   (inner l1 l2 env))
X	  (else
X	   (fail `(wrong-no-of-args-to-function: ,l1 ,l2))))))
X
X(define test-mgu
X  (lambda (t1 t2)
X    (mgu t1 t2 empty-type-env
X      (lambda (x) x)
X      (lambda (msg) (printf "mgu failed: ~s" msg)))))
X
X(define mgu-test1
X  (lambda ()
X    (test-mgu '(-> (seq int) int) '(-> (seq x) y))))
SHAR_EOF
if test 4389 -ne "`wc -c mgu.s`"
then
echo shar: error transmitting mgu.s '(should have been 4389 characters)'
fi
echo shar: extracting check-exp.s '(5781 characters)'
sed 's/^X//' << \SHAR_EOF > check-exp.s
X;;; -*-Scheme-*-
X;;;
X;;; Kernel typechecker algorithm
X;;;
X
X;;; 30 Oct 88 -- identified major data structures and commented code
X;;; to be changed. mw, with help from margmon
X
X;;; Revision 1.9  85/02/14  12:23:58  mw
X
X;;; Revision 1.7  83/09/05  15:10:53  mw
X;;; revised to work without compat file
X;;; 
X;;; Revision 1.6  83/08/26  14:48:49  mw
X;;;
X;;; Revision 1.1  83/08/18  10:35:38  mw
X;;; Initial revision
X
X;;; CSchemeism:
X
X;(declare (usual-integrations))
X
X;;; ****************************************************************
X
X;;; Setup for calling checker
X
X;;; checker:  
X;;; takes arguments:
X
X;;; p -- prefix associating types with variables (type hypotheses)  
X;;; form -- the form to be checked
X;;; env -- type environment (typevars -> types)
X;;; fail -- what to do if you fail (a continuation)
X
X;;; checker calls checker-body inside a timing device.  This should be
X;;; replaced with something standardized.
X
X(define checker 
X  (lambda (p form env fail)
X    (let* ((start-time (ptime))
X	   (res (checker-body p form env fail))
X	   (end (ptime)))
X      (set! checker-time 
X	    (+ checker-time 
X	       (- (- (car end) (car start-time))
X		  (- (cadr end) (cadr start-time)))))
X      res)))
X
X;;; checker-body
X;;; takes arguments:
X
X;;; p -- prefix associating types with variables (type hypotheses)  
X;;; form -- the form to be checked
X;;; env -- type environment (typevars -> types)
X;;; fail -- continuation to be invoked on failure.  Expects an error message.
X
X;;; returns:
X;;; checker-result ::= (type type-env)
X
X;;; may need to return (type generic-vbles type-env) to accomodate LET properly??
X
X(define checker-body
X  (lambda (p form env fail)
X    (let ((unify
X	    (lambda (t1 t2 form)
X	      ;; destructively update env
X	      (set! env 
X		(mgu t1 t2 env (lambda (env) env)
X		  (lambda (failmsg)
X		    (fail `((type-error ,form)
X			    (bad-types:
X			      ,(expand-type-exp t1 env)
X			      ,(expand-type-exp t2 env))
X			    ,failmsg))))))))
X      (let ((ans
X	      (letrec ((loop
X			 (lambda (p form)
X			   (if *trace-loop?*
X			     (printf "checker loop: ~s~%" form))
X			   (cond ((number? form)  'int)
X			     ((string? form)  'string)
X			     ((null? form) (lookup-symbol-type 'nil p fail))
X			     ((symbol? form) (lookup-symbol-type form p fail))
X			     ((eq? (car form) 'lambda)
X					;(lambda vars forms ...)
X			      (let* ((beta*
X				       (mapcar
X					 (lambda (x)
X					   (make-type-scheme
X					     '()
X					     (gen-type-var)))
X					 (cadr form)))
X				     (rho (loop (ext-prefix (cadr form) 
X						  beta*
X						  p)
X						(cons 'begin (cddr form)))))
X				(make-functional-type
X				  (map type-scheme->type beta*)
X				  rho)))
X			     ((memq (car form) '(fix rec))
X					;(fix v form1)
X			      (let* ((beta (make-type-scheme '()
X					     (gen-type-var)))
X				     (rho (loop (ext-prefix (list (cadr form))
X						  (list beta)
X						  p)
X						(caddr form)))
X				     (beta (type-scheme->type beta)))
X				(unify beta rho form)
X				beta))
X			     ((and
X				(eq? (car form) 'quote)
X				(symbol? (cadr form)))
X			      'symbol)
X			     ((eq? (car form) 'unchecked)  '(unchecked))
X			     ((eq? (car form) 'list)
X			      ;; no way to specify "many arguments,
X			      ;; all of the same type", so have to
X			      ;; simulate the macro-expansion.
X			      (if (null? (cdr form))
X				(loop p 'nil)
X				(loop p `(cons ,(cadr form)
X					       (list ,@(cddr form))))))
X			     ((eq? (car form) 'begin)
X			      (if (null? (cddr form))
X				(loop p (cadr form))
X				(car 
X				  (last-pair
X				    (mapcar (lambda (exp) (loop p exp))
X				      (cdr form))))))
X			     ((and (symbol? (car form))
X				   (syntactic-extension? (car form))
X				   ;; patch for Chez expand-once macros:
X				   (not (memq (car form) '(if set!))))
X			      (loop p (expand-once form)))
X			     (else	;must be an application
X			       (let ((beta (gen-type-var))
X				     (rho (loop p (car form)))
X				     (sigma* ; type the arguments
X				       (mapcar (lambda (form1) (loop p form1))
X					 (cdr form))))
X				 (unify rho
X					(make-functional-type sigma* beta)
X					form)
X				 beta))))))
X		(loop p form))))
X	(list ans env)))))
X		
X(define *trace-loop?* #f)
X
X;;; ****************************************************************
X
X;;; check0 -- take a form and pretty-print its type.
X
X(define check0
X  (lambda (form)
X    (pretty-print (checker empty-prefix form empty-type-env report-error))))
X
X;;; check1 -- like check0, but cleverer about printing the answers:
X;;; it expands the type abbrevs in its answer.  
X
X(define check1 
X  (lambda (form) 
X    (let ((ans (checker empty-prefix form empty-type-env report-error)))
X      (pretty-print
X	(expand-type-exp
X	  (checker-result->type ans)
X	  (checker-result->env ans))))))
X
X
X;;; expand-type-exp:
X;;; takes: type-expression and type-env.  Returns a list structure
X;;; with bound type variables replaced by their values, checks for
X;;; looping types and does something appropriate.  The resulting list
X;;; structure should give a nice printable form of the type.
X
X;;; It really does not do a very good job on looping types.
X
X;;; This will probably be rewritten when we get to congruence rep,
X;;; since we can then be awhole lot cleverer about recognizing
X;;; abbreviations. 
X
X(define expand-type-exp
X  (lambda (exp env)
X    (letrec ((loop
X	      (lambda (exp seen)
X		(if (symbol? exp)
X		    (cond ((memq exp seen)
X			   (list 'loop: (lookup-typevar exp env)))
X			  ((is-locally-bound? exp env)
X			   (loop (lookup-typevar exp env) (cons exp seen)))
X			  (else  exp))
X		    (cons (car exp)
X			  (letrec ((inner
X				    (lambda (l)
X				      (cond ((null? l)  nil)
X					    ((symbol? l)  (loop l seen))
X					    (else
X					     (cons (loop (car l) seen)
X						   (inner (cdr l))))))))
X			    (inner (cdr exp))))))))
X      (loop exp nil))))
X
X
SHAR_EOF
if test 5781 -ne "`wc -c check-exp.s`"
then
echo shar: error transmitting check-exp.s '(should have been 5781 characters)'
fi
#	End of shell archive
exit 0