#!/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:
#	doc.tex
#	macros.tex
#	tofc.tex
# This archive created: Tue Nov  7 11:24:45 1989
echo shar: extracting doc.tex '(26073 characters)'
sed 's/^X//' << \SHAR_EOF > doc.tex
X\input macros.tex
X\hbox{}
X\nopagenumbers
X\vfill
X\centerline{\biggfnt SPS Reference Manual}
X\bigskip
X\centerline{SPS Version 1.4 (Chez Scheme Version)}
X\bigskip
X\centerline{Mitchell Wand}
X\bigskip
X\centerline{Northeastern University}
X\bigskip
X\centerline{Mon Apr 17 22:01:21 1989}
X\vfill
X\eject
X\footline={\hss\tenrm\tenrm\folio\hss}	% turn pagenumbers back on
X\pageno=1
X
XThis is the reference manual for the Semantic Prototyping System (SPS).  SPS
Xis a suite of programs, written in Scheme, for rapid prototyping and testing
Xof language definitions written using denotational semantics.  It consists of
Xan ML-style typechecker for a large subset of Scheme, along with an LL(1)
Xparser and transducer generator.
X
X\sectionbegin How To Use the Type-Checker
X
XWhen you define Scheme functions, variables, or constants you may specify
X(what you think is) the type of the expression you are defining.  The
Xtype-checker will compare your type specification with its determination of
Xthe type of the expression being defined.  If your type specification was
Xcorrect, the type-checker updates a type environment, associating the name
Xof the item being defined with the provided type specification.  If it was
Xincorrect, it gives you a message indicating where the two types diverge.
XAfter you have successfully defined a function or variable you may use it
Xjust as you normally would in Scheme.
X
XThe current version of SPS is written in Chez Scheme.  Load it as follows:
XFirst, run Chez Scheme.  Then execute
X\ttctr
X(load ".....top.s")
X\endtt 
Xwhere {\tt ....} is the path name for the
Xdirectory where SPS resides.
X
XIf you intend to use the tools system seriously, it is recommended that you
Xre-boot scheme, loading the types system before dumping.  The resulting heap
Ximage can be loaded by using Chez Scheme with the -h option in the command
Xline.  [details to be inserted here]
X
XUsually the type-checker is used by loading a file of definitions, waiting
Xto see if they type-check properly, and then executing a program.  In the
Xpresent version there is no way to save the information created during the
Xtype-checking of a file so that the file need not be type-checked during
Xfuture loads.  
X
X
X\sectionbegin  Pre-defined Types
X
X\ttnoi
X     (notation:  t0, t1, ..., tn stand for type variables)
X    
XType     Constants    Operations               Remarks
X
Xtriv     triv                                  the one-point set
X
Xbool     true         and, or, not, etc.
X         false
X
Xint                   all the usual things
X
Xsymbol               quote   (quote <symbol>)  Scheme symbols
X
Xstring	any Scheme string (surrounded with double quotes)
X		      all the usual things
X
X(unchecked)	      (unchecked ...anything...)
X			(unchecked ..anything..) is of type (unchecked)
X                              NOTE:  ..anything.. is not typechecked
X
X(-> (seq t1 t2 ... tn) t0)                     this is the type of functions of
X                                               n arguments, of types t1,...,tn,
X                                               producing result of type t0.
X                                               These are produced by the usual
X                                               (lambda (x1 ... xn) e).
X
X(-> (seq t1 ... tn . t) t0)		the type of functions of at least n
X
X				arguments; the first n arguments are of types
X				t1,...,tn, and the remaining arguments may be
X				of any types whatsoever.  The result is of
X				type t0.  Eg, printf is of type (-> (seq
X				string . t) bool).
X
X(list t1)             cons    (-> (seq t1 (list t1)) (list t1))
X                      car     (-> (seq (list t1)) t1) 
X                      cdr     (-> (seq (list t1)) (list t1))
X
X(union t1 t2)
X                      inL     (-> (seq t1) (union t1 t2)) 
X                      inR     (-> (seq t2) (union t1 t2))
X                      union-case  (-> (seq 
X                                       (union t1 t2)
X                                       (-> (seq t1) t3)
X                                       (-> (seq t2) t3))
X                                      t3)
X			Note:  this is rarely used.  Most of the time it is
X			better style to use define-record-type (q.v.) instead.
X                     
X(pair t1 t2)          lson    (-> (seq (pair t1 t2)) t1)
X                      rson    (-> (seq (pair t1 t2)) t2)
X		      pair    (-> (seq t1 t2) (pair t1 t2))
X
X\endtt
X
XFor more goodies, peruse the file {\tt globals.s}.  Besides defining primitive
Xtypes, this file specifies the types of most functions in Chez Scheme that can
Xbe successfully used in type-checked code.  This excludes anything to do with
X{\tt call/cc}, fluids, reals, and {\tt read} (though {\tt read-char} is
Xincluded).  Output functions, such as {\tt print}, {\tt printf}, and {\tt
Xwriteln}, are also included.
X
XIt is possible to define new type constructors, using the commands
X{\tt define-record-type} and {\tt define-type-constructor} (q.v.).
X
X\sectionbegin Type-checker Commands
X
XThe following definitions apply throughout this section.
X
X\ttnoi
X     <type-scheme> ::= <type> | (generic ( <type-var> ... ) <type> )    
X
X     <type> ::=  <name> | ( <name> <type> ... ) 
X                | (-> (seq <type> ... ) <type> )
X                | (-> (seq <type> ... . <type> ) <type> )
X
X     <name> ::= id
X
X     <type-var> ::= id
X
X     <exp> ::= <scheme-expression>
X\endtt
X
X\subsectionbegin Checking expressions and definitions
X
X\ttnoi
X(define-checked <name> <type-scheme> <exp>)
X\endtt
X
XThis is the same as {\tt (define <name> <exp>)} in ordinary Scheme except that
Xthe user must include a specification of the type of {\tt <exp>}.  The
Xtype-checker compares the type defined in {\tt <type-scheme>} with the type it
Xinfers to be the type of {\tt <exp>}.  If they do not match it issues an error
Xmessage.  If they do match, it returns the user to Scheme after first
Xupdating a type environment in which {\tt <name>} is associated with the type
Xdefined in {\tt <type-scheme>}.
X
XNote that {\tt <type-scheme>} may be one of two kinds of expressions.  If {\tt
X<type-exp>} is of the form {\tt (generic ( <type-var> ... ) <type> )} then the
Xobject being defined is of a polymorphic type.  Type variables serve to
Xparameterize the type so that actually a type schema is being described rather
Xthan a type.
X
XExamples:
X
X\ttnoi
X(define-checked myzero?
X  (-> (seq int) bool)
X  (lambda (n) (eq? n 0)))
X
X(define-checked mappend
X  (generic (x)
X    (-> (seq (-> (seq x) (list x))
X	     (list x))
X	(list x)))
X  (lambda (f l)
X    (cond
X      ((null? l) nil)
X      (t (append 
X	   (f (car l))
X	   (mappend f (cdr l)))))))
X\endtt
X
X\ttnoi   
X(check1 <exp>)
X\endtt
X
Xcheck1 prints the type deduced for {\tt <exp>}.  It is useful for playing with
Xsubexpressions to see why they failed, or for introductory playing with the
Xchecker.
X
X
X\subsectionbegin Defining Types
X
X\ttnoi
X(define-type-abbrev <name> <type>)
X\endtt
X
X{\tt define-type-abbrev} is a command to make manipulating types more
Xconvenient for the user.  It defines {\tt <name>} to be an abbreviation for
X{\tt <type>}.  If {\tt <type>} is a complicated expression with several levels
Xof nesting, for instance, it is convenient to call it by a name instead of
Xwriting out the type itself whenever you need to refer to it.
X
XExamples:
X
X\ttnoi
X(define-type-abbrev 3-tuple (pair int (pair int int)))
X(define-type-abbrev object (union int cons))
X(define-type-abbrev cons (pair object object))
X\endtt
X
XThe name and definition of a type-abbrev may be used interchangeably within
Xthe specification of other types.  For example, a function that takes an
Xargument of type {\tt 3-tuple} could be passed a value of type {\tt (pair int
X(pair int int))} if {\tt 3-tuple} was defined in a type-abbrev to be {\tt
X(pair int (pair int int))}.  If two type-abbrev's expand to the same type,
Xthen they are treated as the same type.  In other words, type-abbrev's are
Xtype-checked on the basis of structure equivalence.
X
XType-abbrev's may be recursive and mutually recursive.
XFor example,
X
X\ttnoi
X(define-type-abbrev foo (list bar))
X(define-type-abbrev bar foo)
X    
X(define-type-abbrev alpha (pair int (-> (seq) alpha)))
X(define-type-abbrev omega (pair int omega))
X\endtt
X
XIt may be difficult to actually create an object of type {\tt omega}, however!
X
X\bigskip
X\ttnoi
X(define-record-type
X       (type-constructor-name type-var ...)
X       (constructor-name  (component-type ...))
X       ...)
X\endtt
X
XVery often one wants to build a new type (or type-constructor) which is merely
Xthe sum of products of other types, in other words, a variant-record
Xstructure.  It is possible to build these directly using pair and union, but
Xthe resulting code is quite painful.  {\tt define-record-type} provides a
Xfacility for doing this easily.  One specifies the name of the
Xtype-constructor to be defined and a sequence of variants.  For each variant,
Xone specifies the name of the associated constructor function (which will be
Xglobally defined) and the types of the components for that variant.
X
X{\tt define-record-type} then defines, declares the types, and globally
Xexports all the constructor functions and a case function.  The case function
Xwill have the same name as the type constructor, with ``{\tt -case}''
Xappended.  (Thus if we are defining a record type named {\tt foo}, the case
Xfunction will be called {\tt foo-case}.)  The case function works like {\tt
Xunion-case}: it takes an object of the record type and a sequence of
Xfunctions, one per variant.  It determines which variant the input belongs to
Xand applies the appropriate function (determined positionally, sorry!) to the
Xcomponents.  This facility is much like the standard type definition facility
Xin HOPE or Standard ML.
X
XExamples:
X
X\ttnoi
X;; the real definition of union types:
X(define-record-type (union x y)
X  (inL (x))
X  (inR (y)))
X
X;; how could we not include stacks?
X(define-record-type (stack x)
X   stack-case
X   (empty-stack ())
X   (push-stack (x (stack x))))
X
X;; lists can be done as well:
X(define-record-type (zlist x)
X   (znil ())
X   (zcons (x (zlist x))))
X\endtt
X
XA simple-minded use of these types:
X
X\ttnoi
X(define-checked test-zlist
X   (-> (seq) (list int))
X   (lambda ()
X      (letrec
X	((loop (lambda (x)
X		 (zlist-case x
X		   (lambda () nil)
X		   (lambda (a d) (cons a (loop d)))))))
X	(loop (zcons 1 (zcons 2 (zcons 3 (znil))))))))
X\endtt
X
XThe functions defined by {\tt define-record-type} are made sufficiently generic so
Xthat the checker can deduce that these are {\tt (zlist int)}'s.
X
X\bigskip
X\ttnoi
X(define-type-constructor (<name> <type-var>)
X  <type>				; the representation type
X  ( <procedure-name> <type-scheme> <exp> ) ...)
X\endtt
X    
X{\tt define-type-constructor} is used to define a type constructor for
Xa class of opaque types.  An opaque type is one whose representation is
Xhidden, except to the procedures included in the definition.  Thus values of
Xthe type may be manipulated only using the procedures defined in the
Xdefine-type-constructor expression.
X
X{\tt define-type-constructor} is used either when the representation type is too
Xcomplicated for the use of {\tt define-record-type}, or when there are internal
Xinvariants maintained by the access functions (and thus the access functions
Xof {\tt define-record-type} are inappropriate).
X
XWithin the function and constant definitions associated with a
Xtype-constructor, an object whose type is of the class defined by the
Xtype-constructor may be viewed from two vantage points: external and
Xinternal. The functions "enc" and "dec" transform, respectively, an internal
Xview to an external view and an external view to an internal one.  When
Xviewed externally an object may be manipulated only by the functions
Xassociated with its type.  When viewed internally it is considered to have
Xthe type specified in {\tt <type>}
X
XA type-constructor may be defined recursively--i.e., the
Xrepresentation type may contain
Xthe name of the type-constructor being defined.
X
XExamples:
X
X\ttnoi
X;;; another possible definition of union:
X(define-type-constructor union (x y)
X  (pair symbol (pair x y))
X  (inL (-> (seq x) (union x y))
X       (lambda (v)
X	 (enc (pair 'L (pair v any)))))	; see "any" below.
X  (inR (-> (seq y) (union x y))
X       (lambda (v)
X	 (enc (pair 'R (pair any v)))))
X  (union-case
X    (generic (z) (-> (seq (union x y)
X			  (-> (seq x) z)
X			  (-> (seq y) z))
X		     z)
X    (lambda (l f g)
X      (let ((q (lson (dec l))))
X	(if (eq? q 'L)
X	  (f (lson (rson (dec l))))
X	  (if (eq? q 'R)
X	    (g (rson (rson (dec l))))
X	    (error l)))))))
X
X;;; association lists (a more complicated example)
X(define-type-constructor (alist x)
X  (list (pair symbol x))
X  (alist$ext
X    (generic (x)
X      (-> (seq (alist x) symbol x)
X	  (alist x)))
X    (lambda (l id val)
X      (enc (cons (pair id val) (dec l)))))
X  (alist$bvars
X    (generic (x) 
X      (-> (seq (alist x)) (list symbol)))
X    (lambda (l) (map lson (dec l))))
X  (alist$init
X    (generic (x)
X      (alist x))
X    (enc nil)))
X\endtt
X
X\sectionbegin Grammars
X
XSPS includes a facility for generating and type-checking parsers and
Xtransducers.  Currently, only LL(1) grammars are handled.
X
X\bigskip
X\ttnoi
X(define-grammar <name> <non-terminal> <grammar>)
X\endtt
X
XThis defines a transducer for the given grammar, using the given non-terminal
Xas the starting symbol.  The resulting transducer is named {\tt <name>}.
X
XGrammars are specified as follows:
X
X\ttnoi
X<grammar> ::= (<production> ...)
X<production> ::= (<production-name> (<lhs> <rhs>) <arglist> <body>)
X
X<lhs> ::= <non-terminal>
X<rhs> ::= (<rhs-entry> ...)
X<rhs-entry> ::= <non-terminal> | <terminal>
X<non-terminal> ::= <type-variable>     
X<terminal> ::= (quote <scheme symbol>)
X
X<arglist> ::= (<scheme symbol> ...)
X<body> ::= <scheme expression>
X\endtt
X
XSome terminal and non-terminal symbols are predefined:
X
Xleft and right parens are represented by the terminal symbols {\tt 'lparen} and
X{\tt 'rparen}.
X
X{\tt int} is the non-terminal for integers
X
X{\tt symbol} is the non-terminal for symbols
X
XThe values for phrases of these non-terminals is the integer or
Xsymbol, respectively.
X
XThus the production
X\ttnoi
XTerm ::= (Term + int)
X\endtt
Xwould be coded as {\tt (Term ('lparen Term '+ int 'rparen))}.
X
XThe transducer traverses the abstract syntax tree, pebbling each node with a
Xvalue.  Each symbol or int node gets pebbled with the appropriate symbol or
Xinteger value.  To compute the value for an interior node, the body of the
Xrule is evaluated in an environment in which the names on the arglist are
Xbound to the values of the subtrees at that node.  Thus the names on the
Xarglist should be in one-one correspondence to the nonterminals in the
Xright-hand side of the production.
X
XWhen a define-grammar expression is evaluated, each rule body is typechecked
Xunder the appropriate assumptions about its bound variables.  If all the
Xproductions are type-correct, then an LL(1) parser-generator is invoked to
Xcreate the parsing tables, using the given non-terminal as the starting
Xsymbol.  A lexical scanner is also generated, using the declared terminal
Xsymbols as lexical items.  [See below].  The resulting parser is of type
X{\tt (-> (seq string) <start-symbol>)} .
X
X
XExample:
X
X\ttnoi
X;; binary numerals, in reverse order (sorry)
X
X(define-type-abbrev Num int)
X(define-type-abbrev Digit int)
X
X(define-grammar sdt3 Num
X  (zero
X    (Digit ('a))
X    ()
X    0)
X  (one
X    (Digit ('b))
X    ()
X    1)
X  (empty-number
X    (Num ())
X    ()
X    0)
X  (non-empty-number
X    (Num (Digit Num))
X    (x y)
X    (+ (* 2 y) x)))
X    
X(sdt3 "b b a b") ==> 11
X\endtt
X
X\bigskip
X\ttnoi
X(define-unchecked-grammar <name> <start-symbol> <grammar>)
X\endtt
X
X{\tt define-unchecked-grammar} is like {\tt define-grammar}, except that no
Xtypechecking is done.  The resulting parser is not given a type.
X
X\bigskip
X\ttnoi
X(check-production1 <rule>)
X\endtt
X
XLike {\tt check1}, except that it takes a rule as an argument.  This can be a
Xconvenient way to check the type of a subexpression if you want to make some
Xassumptions about the types of variables, eg.
X
X\ttnoi
X(check-production1 '(hukairz (int (int)) (x) (add1 x)))
X\endtt
X
X[Details on the lexical conventions used by the scanner need to be
X  added here].
X
X\sectionbegin Error Messages
X
XThe type-checker generates a number of error messages, most of which are
Xreadily understandable, such as:
X
X\ttnoi
Xuntyped-identifier
Xwrong-number-of-arguments-to-function
Xwrong-number-of-arguments-to-type-constructor
X\endtt
X
XThe most general (and the most common) error, however, is a simple mismatch
Xof types, where the types deduced for a function and its argument do not
Xagree.  In this case the error message contains the following information:
X
Xline {\tt [1]}:  The name of the object whose type was incorrectly specified.
X
Xline {\tt [2]}:  The expression whose type it was attempting to deduce when the
X           error was detected.  (More below.)
X
Xline {\tt [3]}:  The specific parts of the above two types that fail to match
X
Xline {\tt [4]}:  Some clues about where the error might have occurred.
X
X\ttnoi
X(define-checked foo
X  (-> (seq int) int)
X  (lambda (x) (cons x nil)))
X
X[1]	define-checked: error in foo
X[2]	((type-error: (f00224 (lambda (x)
X	                          (cons x nil))))
X[3]	 ((mismatch: (list (int)) (int))
X[4]	  (reasons: ((cons x nil)) 
X	            ((define-type-abbrev int (int))))))
X\endtt
X
XHere, we had a function whose body was well-typed, but which did not match its
Xspecification.  This was detected by attempting the check the application of a
Xgensym (in this case {\tt f00224}) to the body, where the gensym is set up
Xwith a type whose domain was {\tt (-> (seq int) int)}.  The mismatch was
Xbetween a {\tt (list int)} and an {\tt int}.  Under "reasons:", the checker
Xthen gives two lists of items.  Each item attempts to account for the presence
Xof the possibly-offending type.  In this case, the checker reports that the
Xreason it thought it had a {\tt (list (int))} was that it saw the application
X{\tt (cons x nil)}.  It thought it had an {\tt (int)} because the type
Xvariable int is just an abbreviation for {\tt (int)}.  In general, there may
Xbe many such reasons for a deduction.
X
X[This may not match exactly what the type-checker is currently producing]
X
XA garden-variety type error is almost always a deletion error (such as the
Xomission of an {\tt inL} or {\tt inR}). Because of the way information flows
Xin the analysis of an expression, and because polymorphism allows many
Xexpressions to be well-typed, such an error is often detected only far away
Xfrom its real site.  The error site is almost always at the top-level of one
Xof the reasons suggested by the checker.  The algorithm for keeping track of
Xreasons and reporting them is the subject of a separate paper [Wand, POPL 85].
X
XHere are some additional notes and suggestions on interpreting error messages:
X
X1.  The example is for a {\tt define-checked} with a general mismatch.
XSimilar information is produced by {\tt define-type-constructor} and {\tt
Xdefine-grammar}.  For other errors, similar but less exhaustive information is
Xreported.
X
X2. A type error at an expression of the form {\tt (f00? exp)}, as above,
Xindicates that exp is well-typed, but its type does not match the
Xspecification.
X
X3. Each generic type variable present in a type specified by the user is
Xreplaced by a parenthesized gensym (e.g., {\tt (t00048)} ).  In this case, a
Xmismatch between this type {\tt (t00??)} and some other type indicates that
Xthe expression is not fully generic-- that the indicated type was deduced for
Xthe type that should be generic.
X
X\sectionbegin Interface to unchecked code
X
XSPS includes several facilities to enable the typechecker to interact
Xwith code that is unchecked but trusted.  This is typically done to
Xuse some data representation that is more efficient than that
Xavailable within the typechecker.  (Note that this occurs only rarely!)
X
X\bigskip
X\ttnoi
X(define-unchecked <name> <type-scheme> <exp>)
X\endtt
X
X{\tt define-unchecked} is the same as {\tt (define <name> <exp>)} in Chez
XScheme except that it also directs the type-checker to consider the type
Xdefined in {\tt <type-scheme>} to be the type of {\tt <exp>}.  The
Xtype-checker will do no type-checking of {\tt <exp>}.  Whenever the
Xtype-checker encounters {\tt <name>} in an expression whose type it is trying
Xto infer, it will consider the type that was defined in {\tt <type-scheme>} to
Xbe the type of {\tt <name>}.
X
XExample:
X
X\ttnoi
X(define-unchecked error1
X  (generic (x y) (-> (seq x) y))
X  (lambda (msg) (print "Error: ") (print msg) (reset)))
X\endtt
X
X{\tt define-unchecked} is useful for creating an interface between unchecked
Xportions of a system and checked portions.  For example, if some other part of
Xthe Scheme system wants to use a data representation different from the one
Xused by the type-checker, the interface functions should be defined with {\tt
Xdefine-unchecked}.  Many uses of {\tt define-unchecked} are better done by
Xusing {\tt define-type-constructor} or {\tt define-record-type}, however.
X
X\bigskip
X\ttnoi
X(declare-unchecked <name> ( <type-var> ... ) <type>) 
X\endtt
X
X{\tt declare-unchecked} is similar to {\tt define-unchecked} in that it is a
Xdirective to the type-checker to associate a type with {\tt <name>} without
Xperforming any type-checking.  The syntax of declare-unchecked differs from
Xsome of the other type-checker commands in that it requires a list of type
Xvariables. If {\tt <type>} is not to be generic, an empty list must be
Xincluded as the second argument to declare-unchecked.
X
X{\tt declare-unchecked} takes no {\tt <exp>} argument.  It is usually used to
Xassign a type to a pre-defined Scheme function or a system function.  It can
Xalso be used with a user-defined function or variable if the user provides a
Xseparate Scheme definition of {\tt <name>}, but this is officially deemed to
Xbe bad style.  (Rather, use a {\tt define-unchecked}, which is equivalent to a
X{\tt define} followed by a {\tt declare-unchecked}.)
X
XExample:  
X
X\ttnoi          
X(declare-unchecked append (x)		;this is an entry from globals.s
X  (-> (seq (list x) (list x)) 
X      (list x)))
X\endtt
X
X{\tt declare-unchecked} may also be used to declare the type of a forward
Xreference.
X
XExample:
X
X\ttnoi
X(declare-unchecked even? () (-> (seq int) bool))
X
X(define-checked odd?
X  (-> (seq int) bool)
X  (lambda (x)
X    (if (eq? x 1) 
X      true
X      (if (zero? x)
X	false
X	(even? (1- x))))))
X
X(define-checked even?
X  (-> (seq int) bool)
X  (lambda (y)
X    (if (zero? y) 
X      true
X      (odd? (1- y)))))
X\endtt
X
XThis is also officially deemed to be bad style.  (Use a {\tt letrec} instead)
X
X\bigskip
X\ttnoi
Xany
X\endtt
X
XThis is an identifier which is completely polymorphic.  It is defined by
X
X\ttnoi 
X(define-unchecked any (x) x '*any*)
X\endtt
X
XIt is useful for initializing variables when you don't know enough to write
Xsomething better, as in the union example above.  Since it is a "hole" in the
Xtype system, its use introduces insecurity.  Avoid it when possible.
X
X
X\sectionbegin  Miscellany
X
XIf you are dealing with global variables, remember to declare their types!
XGlobal variables which are assigned to more than once should be monomorphic
X(ie, not generic).  This is a real insecurity in the system.
X
XType abbrev's must be defined before they are referred to within a
Xtype-checker command other than a {\tt define-type-abbrev}.  Type-abbrev's that
Xrefer to other type-abbrev's may be defined in any order.  So if you use
Xtype-abbrev's, put them first!!!  
X
XIt is an error to define type abbrevs to create a ``tight loop'' eg:
X
X\ttnoi
X(define-type-abbrev foo bar)
X(define-type-abbrev bar baz)
X(define-type-abbrev baz foo)
X\endtt
X
X\noindent or
X
X\ttnoi
X(define-type-abbrev jinx jinx)
X\endtt
X
XEach of these two examples contain an illegal cycle.  An illegal cycle is
Xone in which a type-abbrev is ultimately defined to be itself. If you
Xaccidently create such a cycle the type-checker will point it out to you.
X
X{\bf BUG:}  This situation is NOT detected.
X
X
XThere are many legal Scheme programs that will not type-check with this
Xtype-checker. A simple example of a legal Scheme program that is not
Xtype-checkable (nor typeable) using the type-checker is the following:
X
X\ttnoi
X(define-checked iffy
X  (-> (seq int) ?)
X  (lambda (x)
X    (if (zero? x) 0 false)))
X\endtt
X
XThis is because it sometimes returns a boolean and sometimes an integer.
XMany common Lisp functions are of this flavor, eg. {\tt assq}.  Look at
X{\tt alist\$lookup} in {\tt globals.s} to see how this can be fixed.
X
XIn addition, there are legal Scheme programs that will not type-check with
Xthis type-checker even if you correctly specify their types.  Consider the
Xfollowing:
X
X\ttnoi 
X(define-checked confuse (t1)
X  (-> (seq t1) bool)
X  (lambda (w)
X    (let ((exchange 
X	    (lambda (x f)
X	      (f x))))
X      (exchange (exchange w (lambda (y) 3))
X	(lambda (z) true)))))
X\endtt 
X
XThe function confuse as defined above will not type-check with this
Xtype-checker, because our {\tt let} is just a macro for the appropriate
Xlambda-expression, rather than Milner's polymorphic {\tt let}.
X
X{\bf BUG}:  This version still does not do Milner {\tt let}.
X
XAnother explanation is that the type-checker can not infer polymorphic types.
XIf it has been informed that a function (or variable) is polymorphic, then it
Xwill be able treat one instance of the function as having one type and
Xanother as having another type.  If it has not been informed that a function
Xis polymorphic, however, it will insist upon the function having the same
Xtype each time it is called.  In the example above, exchange is polymorphic,
Xyet the type-checker has not been informed of that fact.  If exchange were
Xglobally defined, the polymorphism could be specified, and the resulting
Xredefinition will work:
X
X\ttnoi
X(define-checked exchange1
X  (generic (t1 t2)
X    (-> (seq t1
X	     (-> (seq t1) t2))
X	t2))
X  (lambda (x f) (f x)))
X
X(define-checked confuse1
X  (generic (t1) (-> (seq t1) bool))
X  (lambda (x)
X    (exchange1 (exchange1 x (lambda (y) 3))
X      (lambda (z) true))))
X\endtt
X
XA correct treatment of Milner {\tt let} will be added soon (I hope!).
X
X\vfill\eject
X\pageno=-1
X\makecontents
X\bye
X
X
X
X
SHAR_EOF
if test 26073 -ne "`wc -c doc.tex`"
then
echo shar: error transmitting doc.tex '(should have been 26073 characters)'
fi
echo shar: extracting macros.tex '(8346 characters)'
sed 's/^X//' << \SHAR_EOF > macros.tex
X\font\bigfnt=cmr10 scaled \magstep3
X\font\biggfnt=cmr10 scaled \magstep4
X
X% section/subsection style
X
X% fonts
X
X\font\twelverm=cmr10 at 12pt    % maybe.... mw Tue Oct  7 09:57:34 1986
X
X% page size
X\hsize=5.5 true in
X\vsize=8.5 true in
X
X\voffset=0.0truein  % 1 in vert margin
X\hoffset=0.5 truein % 1.5 in horiz margin
X\parskip=3.0pt plus 1pt 
X
X\newcount\sectionno
X\newcount\subsectionno
X\newcount\subsubsectionno
X\sectionno=0
X\subsectionno=0
X\subsubsectionno=0
X
X\def\secfnt{\twelverm}
X\def\subsecfnt{\twelverm}
X\def\subsubsecfnt{\twelverm}
X
X
X\def\dosectionheader#1#2{
X		    \contents{#2#1}
X		    \message{#1}
X		    \bigskip
X		    \leftline{\secfnt #1}\nobreak
X		    \vskip 6pt plus 1pt minus 1pt
X		    \vskip-\parskip}
X
X
X\def\sectionbegin#1\par{
X                    \global\subsectionno=0
X		    \global\subsubsectionno=0
X		    \global\advance\sectionno by 1
X		    \dosectionheader{\number\sectionno. #1}{}
X		    }
X
X\def\section#1{\global\sectionno=#1 \global\advance\sectionno by -1}
X
X\def\appsectionbegin#1\par{
X                       \global\subsectionno=0
X		       \global\subsubsectionno=0
X		       \dosectionheader{#1}{}
X		       }
X
X\def\subsectionbegin#1\par{
X	\global\subsubsectionno=0
X        \global\advance\subsectionno by 1
X%	\contents{2\enskip\number\sectionno{.}\number\subsectionno #1}
X	\dosectionheader{\number\sectionno{.}\number\subsectionno\ #1}{\enskip}
X	}
X
X\def\appsubsectionbegin#1\par{
X	\global\subsubsectionno=0
X	\dosectionheader{#1}{\enskip}
X	}
X
X\def\subsubsectionbegin#1\par{
X	\global\advance\subsubsectionno by 1
X	\dosectionheader{\number\sectionno{.}\number\subsectionno{.}\number\subsubsectionno\ #1}{\enskip\enskip}
X	}
X
X\def\appsubsubsectionbegin#1\par{
X	\dosectionheader{#1}{\enskip\enskip}
X	}
X
X\def\hangpar{\hangindent=3pc \hangafter=0\noindent}
X
X%\def\ref#1#2\par{\medskip
X%             \hangindent=15pt
X%             \hangafter=1
X%	     \noindent
X%	     %\hbox to 2pc{#1}#2
X%	     \noindent[{#1}]\hfil\break #2
X%	     \medskip}
X
X\def\ref#1{\par\hangindent=2em\hangafter=1\noindent[{#1}]\hfil\break}
X
X\def\monthandyear{\ifcase\month\or
X   January\or February\or March\or April\or May\or June\or
X   July\or August\or September\or October\or November\or December\fi
X   \space\number\year}
X
X\def\date{\number\day\space\ifcase\month\or
X   January\or February\or March\or April\or May\or June\or
X   July\or August\or September\or October\or November\or December\fi
X   \space\number\year}
X
X\def\titlepage#1{\shipout#1}
X
X\def\display#1{\smallskip\centerline{#1}\smallskip\noindent}
X
X\newwrite\tofc
X\immediate\openout\tofc=tofc
X%\def\contents#1{\immediate\write\tofc{\cline{#1}{\number\pageno}}}
X	% this used to be \outer, I don't know why.
X\def\contents#1{\immediate\write\tofc{\cline{#1}{\folio}}} 
X
X                                %% changed to \folio % Fri Mar 13 % 10:21:50
X                                %% 1987 mw 
X
X\def\makecontents{
X	\immediate\closeout\tofc
X%       \headline={\headfont\hfil Contents}
X	\centerline{\bf Table of Contents}
X	\bigskip
X	\input tofc
X	\vfill\eject
X	}	
X%		  \vbox to \vsize{\vfil\vfil\leftline{\bf Table of Contents}
X%		                  \bigskip\input tofc\vfil}}
X
X\def\headfont{\rm}
X\def\cline#1#2{\line{#1\leaderfill#2}}
X
X\def\leaderfill{\leaders\hbox to .5em{\hss.\hss}\hfil}
X
X\def\centercolumn#1{
X	\hbox to \the\hsize{\hss\vbox{\halign{\hfil {##} \hfil\cr #1}}\hss}}
X
X\catcode`\^^I=\active % tab = \space
X\def^^I{\space}
X
X\def\begindisplay{\obeylines\startdisplay}
X{\obeylines\gdef\startdisplay#1
X  {\catcode`|^^M=5$$#1\halign\bgroup\indent##\hfil&&\qquad##\hfil\cr}}
X\def\enddisplay{\crcr\egroup$$}
X
X\catcode`\|=\active
X{\obeylines\gdef|{\ttverbatim\let^^M=\ \let|=\endgroup}}
X
X\chardef\other=12
X\def\fullttverbatim{\begingroup \catcode`\\=\other \catcode`\{=\other
X  \def^^I{\ \ \ \ \ \ \ \ } % tab = 8 spaces
X  \catcode`\}=\other \catcode`\$=\other \catcode`\&=\other
X  \catcode`\#=\other \catcode`\%=\other \catcode`\~=\other
X  \catcode`\_=\other \catcode`\^=\other 
X  \obeyspaces \obeylines \tt}
X{\obeyspaces\gdef {\ }} % \obeyspaces now gives \ , not \space
X
X\def\semittverbatim{\begingroup \catcode`\\=\other
X  \def^^I{\ \ \ \ \ \ \ \ } % tab = 8 spaces
X  \catcode`\&=\other
X  \catcode`\#=\other \catcode`\%=\other \catcode`\~=\other
X  \obeyspaces \obeylines \tt}
X
X\let\ttverbatim=\fullttverbatim
X
X\def\endline{\leavevmode\endgraf}
X
X\def\begintt{$$\let\par=\endline \ttverbatim \parskip=0pt
X  \catcode`\|=0 \rightskip=-5pc \ttfinish}
X{\catcode`\|=0 |catcode`|\=\other % | is temporary escape character
X  |obeylines % end of line is active
X  |gdef|ttfinish#1^^M#2\endtt{#1|vbox{#2}|endgroup$$}}
X
X\def\tti{\let\par=\endline \ttverbatim \parskip=0pt
X  \catcode`\|=0 \rightskip=-5pc \ttifinish}
X
X\def\ttnos{\let\par=\endline \ttverbatim \parskip=0pt
X  \catcode`\|=0 \rightskip=-5pc \ttnosfinish}
X
X\def\beginttnoi{\begintt\parindent=0pt}
X\def\ttnosi{\ttnos\parindent=0pt}
X\def\ttnoi{\tti\parindent=0pt}
X
X\def\ttctr{$$\let\par=\cr \ttverbatim \parskip=0pt
X  \catcode`\|=0 \rightskip=-5pc \ttctrfinish}
X
X{\catcode`\|=0 |catcode`|\=\other % | is temporary escape character
X  |obeylines % end of line is active
X  |gdef|ttifinish#1\endtt{|endline #1 |endline|endgroup|noindent} %
X  |gdef|ttnosfinish#1\endtt{#1|endgroup|noindent} %
X  |gdef|ttctrfinish#1^^M#2\endtt{#1|vbox{|halign{##|hfil|cr#2}}|endgroup$$}}
X
X\def\semitt{\let\ttverbatim=\semittverbatim}
X% Written by Pedro de Rezende [based on Mitchell Wand's twelvepoint.tex]
X% Tue Oct 14 20:51:17 1986
X
X\newskip\ttglue
X
X% eleven-point fonts
X
X\font\elevenrm=cmr10 scaled \magstephalf
X\font\eleventt=cmtt10 scaled \magstephalf
X\font\eleveni=cmmi10 scaled \magstephalf
X\font\elevensy=cmsy10 scaled \magstephalf
X\font\elevenit=cmti10 scaled \magstephalf
X\font\elevenssb=cmssbx10 scaled \magstephalf
X\font\elevenbf=cmbx10 scaled \magstephalf
X\font\elevensl=cmsl10 scaled \magstephalf
X
X% other fonts needed, by family; most others are already in PlainTex
X
X% roman text
X\font\eightrm=cmr8
X\font\sixrm=cmr6	
X
X\font\eighti=cmmi8	% math italic
X\font\seveni=cmmi7
X\font\sixi=cmmi6
X
X\font\eightsy=cmsy8	% math symbol
X\font\sixsy=cmsy6
X\font\sevensy=cmsy7
X\font\fivesy=cmsy5
X
X\font\eightit=cmti8	% text italic
X\font\sevenit=cmti7
X
X\font\eightbf=cmbx8	% bold face (extended)
X\font\sevenbf=cmbx7
X\font\sixbf=cmbx6
X\font\fivebf=cmbx5
X
X% the elevenpoint macro
X
X\def\elevenpoint{%
X \def\rm{\fam0\elevenrm}%
X \def\it{\fam4\elevenit}%
X \textfont\slfam=\elevensl%
X \def\sl{\fam\slfam\elevensl}%
X \def\bf{\fam6\elevenbf}%
X \textfont\ttfam=\eleventt%
X \def\tt{\fam\ttfam\eleventt}%
X \def\ssb{\elevenssb}%
X \parskip 5.5pt plus 2pt
X \tt \ttglue=.5em
X \textfont0=\elevenrm \scriptfont0=\eightrm \scriptscriptfont0=\sixrm
X \textfont1=\eleveni \scriptfont1=\eighti \scriptscriptfont1=\sixi
X \textfont2=\elevensy \scriptfont2=\eightsy \scriptscriptfont2=\sixsy
X \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
X \textfont4=\elevenit \scriptfont4=\eightit \scriptscriptfont4=\sixi
X \textfont6=\elevenbf \scriptfont6=\eightbf \scriptscriptfont6=\sixbf
X \normalbaselineskip 13.2pt
X \abovedisplayskip 13.2pt plus 3.2pt minus 10pt
X \baselineskip 13.2pt
X \abovedisplayshortskip 0pt plus 3.2pt
X \belowdisplayskip 13.2pt plus 3.2pt minus 10pt
X \belowdisplayshortskip 7.8pt plus 3.2pt minus 4.6pt
X \def\strut{{\vrule height9.3pt depth 3.8pt width0pt}}%
X \normalbaselines\rm}
X
X\elevenpoint
X
X\def\rcsinfo$#1${\centerline{\sixrm #1}
X		 \bigskip}
X
X% now put in switch to get back to tenpoint
X
X\font\tenssb=cmssbx10
X\def\tenpoint{%
X \def\rm{\fam0\tenrm}%
X \def\it{\fam4\tenit}%
X \textfont\slfam=\tensl%
X \def\sl{\fam\slfam\tensl}%
X \def\bf{\fam6\tenbf}%
X \textfont\ttfam=\tentt%
X \def\tt{\fam\ttfam\tentt}%
X \def\ssb{\tenssb}%
X \parskip 5pt plus 2pt
X \tt \ttglue=.5em
X \textfont0=\tenrm \scriptfont0=\sevenrm \scriptscriptfont0=\fiverm
X \textfont1=\teni \scriptfont1=\seveni \scriptscriptfont1=\fivei
X \textfont2=\tensy \scriptfont2=\sevensy \scriptscriptfont2=\fivesy
X \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
X \textfont4=\tenit \scriptfont4=\sevenit \scriptscriptfont4=\fivei
X \textfont6=\tenbf \scriptfont6=\sevenbf \scriptscriptfont6=\fivebf
X \normalbaselineskip 12pt
X \abovedisplayskip 12pt plus 3pt minus 9pt
X \baselineskip 12pt
X \abovedisplayshortskip 0pt plus 3pt
X \belowdisplayskip 12pt plus 3pt minus 9pt
X \belowdisplayshortskip 7pt plus 3pt minus 4pt
X \def\strut{{\vrule height8pt depth 3pt width0pt}}%
X \normalbaselines\rm}
X
SHAR_EOF
if test 8346 -ne "`wc -c macros.tex`"
then
echo shar: error transmitting macros.tex '(should have been 8346 characters)'
fi
echo shar: extracting tofc.tex '(797 characters)'
sed 's/^X//' << \SHAR_EOF > tofc.tex
X\hbox to\hsize {1. How To Use the Type-Checker \leaders \hbox to .5em{\hss .\hss }\hfil 1}
X\hbox to\hsize {2. Pre-defined Types \leaders \hbox to .5em{\hss .\hss }\hfil 1}
X\hbox to\hsize {3. Type-checker Commands \leaders \hbox to .5em{\hss .\hss }\hfil 3}
X\hbox to\hsize {\hskip .5em\relax 3{.}1\ Checking expressions and definitions \leaders \hbox to .5em{\hss .\hss }\hfil 3}
X\hbox to\hsize {\hskip .5em\relax 3{.}2\ Defining Types \leaders \hbox to .5em{\hss .\hss }\hfil 4}
X\hbox to\hsize {4. Grammars \leaders \hbox to .5em{\hss .\hss }\hfil 8}
X\hbox to\hsize {5. Error Messages \leaders \hbox to .5em{\hss .\hss }\hfil 10}
X\hbox to\hsize {6. Interface to unchecked code \leaders \hbox to .5em{\hss .\hss }\hfil 12}
X\hbox to\hsize {7. Miscellany \leaders \hbox to .5em{\hss .\hss }\hfil 14}
SHAR_EOF
if test 797 -ne "`wc -c tofc.tex`"
then
echo shar: error transmitting tofc.tex '(should have been 797 characters)'
fi
#	End of shell archive
exit 0